structure Newton.IsApproximateIdentity {n : ℕ} (ψ : (Fin n → ℝ) → ℝ) : Prop

Approximate identity (mollifier) structure.

A function ψ is a mollifier if it is smooth, compactly supported, normalized, and non-negative.

• smooth : ContDiff ℝ (↑⊤) ψ
• compact_support : HasCompactSupport ψ
• normalized : ∫ (x : Fin n → ℝ), ψ x = 1
• nonneg (x : Fin n → ℝ) : 0 ≤ ψ x
• support_subset : tsupport ψ ⊆ Metric.closedBall 0 1

noncomputable def Newton.scaledMollifier {n : ℕ} (ψ : (Fin n → ℝ) → ℝ) (η : ℝ) : (Fin n → ℝ) → ℝ

Scaled mollifier ψ_η.

ψ_η(x) = η^(-n) ψ(x/η)

Equations

• Newton.scaledMollifier ψ η x = η ^ (-↑n) * ψ fun (i : Fin n) => x i / η

theorem Newton.scaledMollifier_nonneg {n : ℕ} {ψ : (Fin n → ℝ) → ℝ} (hψ_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ ψ x) {η : ℝ} (hη_nonneg : 0 ≤ η) (x : Fin n → ℝ) : 0 ≤ scaledMollifier ψ η x

Nonnegativity of the scaled mollifier when ψ ≥ 0 and η ≥ 0.

theorem Newton.hasCompactSupport_scaledMollifier {n : ℕ} {ψ : (Fin n → ℝ) → ℝ} (hψ : HasCompactSupport ψ) {η : ℝ} (hη_pos : 0 < η) : HasCompactSupport (scaledMollifier ψ η)

Compact support of the scaled mollifier under η > 0.

theorem Newton.tsupport_scaledMollifier_subset {n : ℕ} {ψ : (Fin n → ℝ) → ℝ} (hψ : IsApproximateIdentity ψ) {η : ℝ} (hη_pos : 0 < η) : tsupport (scaledMollifier ψ η) ⊆ Metric.closedBall 0 η

T-support inclusion for the scaled mollifier: it is contained in the ball of radius η.

theorem Newton.integral_scaledMollifier_eq_one {n : ℕ} {ψ : (Fin n → ℝ) → ℝ} (hψ : IsApproximateIdentity ψ) {η : ℝ} (hη_pos : 0 < η) : ∫ (x : Fin n → ℝ), scaledMollifier ψ η x = 1

The total mass of the scaled mollifier is 1.

theorem Newton.core_indicator_eLpNorm_bound {n : ℕ} {p : ENNReal} {coreSet : Set (Fin n → ℝ)} (h_core_meas : MeasurableSet coreSet) {g : (Fin n → ℝ) → ℂ} {δ : ℝ} (h_bound : ∀ᵐ (x : Fin n → ℝ) ∂MeasureTheory.volume.restrict coreSet, ‖g x‖ ≤ δ) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => coreSet.indicator g x) p MeasureTheory.volume ≤ MeasureTheory.volume coreSet ^ (1 / p.toReal) * ENNReal.ofReal δ

theorem Newton.mollifier_converges_continuous {n : ℕ} (f : (Fin n → ℝ) → ℂ) (ψ : (Fin n → ℝ) → ℝ) (hf_cont : Continuous f) (hf_compact : HasCompactSupport f) (hψ : IsApproximateIdentity ψ) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (η : ℝ), 0 < η → η < δ → ∀ (x : Fin n → ℝ), ‖f x - ∫ (y : Fin n → ℝ), f (x - y) * ↑(scaledMollifier ψ η y)‖ < ε

Mollifier convergence for continuous functions.

For f continuous with compact support and ψ an approximate identity: ‖f - f * ψ_η‖_∞ → 0 as η → 0

theorem Newton.eLpNorm_triangle_inequality {n : ℕ} (f g h : (Fin n → ℝ) → ℂ) (p : ENNReal) (hp : 1 ≤ p) (hfg : MeasureTheory.AEStronglyMeasurable (fun (x : Fin n → ℝ) => f x - g x) MeasureTheory.volume) (hgh : MeasureTheory.AEStronglyMeasurable (fun (x : Fin n → ℝ) => g x - h x) MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - h x) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - g x) p MeasureTheory.volume + MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - h x) p MeasureTheory.volume

Triangle inequality for Lp norm.

‖f - h‖_p ≤ ‖f - g‖_p + ‖g - h‖_p

theorem Newton.eLpNorm_triangle_three {n : ℕ} (f g ψ φ : (Fin n → ℝ) → ℂ) (p : ENNReal) (hp : 1 ≤ p) (hfg : MeasureTheory.AEStronglyMeasurable (fun (x : Fin n → ℝ) => f x - g x) MeasureTheory.volume) (hgψ : MeasureTheory.AEStronglyMeasurable (fun (x : Fin n → ℝ) => g x - ψ x) MeasureTheory.volume) (hψφ : MeasureTheory.AEStronglyMeasurable (fun (x : Fin n → ℝ) => ψ x - φ x) MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - φ x) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - g x) p MeasureTheory.volume + MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - ψ x) p MeasureTheory.volume + MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => ψ x - φ x) p MeasureTheory.volume

Three-way triangle inequality (used in proof steps).

‖f - φ‖_p ≤ ‖f - g‖_p + ‖g - ψ‖_p + ‖ψ - φ‖_p

This is used in the paper's Section 4.2 for the error analysis.

theorem Newton.convolution_support_ball_subset {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (R δ : ℝ) (hf_supp : tsupport f ⊆ Metric.closedBall 0 R) (hg_supp : tsupport g ⊆ Metric.closedBall 0 δ) : (tsupport fun (x : Fin n → ℝ) => ∫ (y : Fin n → ℝ), f (x - y) * g y) ⊆ Metric.closedBall 0 (R + δ)

Explicit support bound for convolution.

If supp(f) ⊆ B_R and supp(g) ⊆ B_δ, then supp(f * g) ⊆ B_{R+δ}.

theorem Newton.mollifier_converges_Lp {n : ℕ} (f : (Fin n → ℝ) → ℂ) (ψ : (Fin n → ℝ) → ℝ) (p : ENNReal) (hp : 1 ≤ p) (hp_ne_top : p ≠ ⊤) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hψ : IsApproximateIdentity ψ) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (η : ℝ), 0 < η → η < δ → MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f x - ∫ (y : Fin n → ℝ), f (x - y) * ↑(scaledMollifier ψ η y)) p MeasureTheory.volume < ENNReal.ofReal ε

Mollifier convergence in Lp (general result).

For f ∈ Lp with 1 ≤ p < ∞ and ψ an approximate identity: ‖f - f * ψ_η‖_p → 0 as η → 0