theorem Newton.convolution_sub {n : ℕ} (f₁ f₂ g : (Fin n → ℝ) → ℂ) (hconv₁ : ∀ᵐ (x : Fin n → ℝ), MeasureTheory.Integrable (fun (y : Fin n → ℝ) => f₁ (x - y) * g y) MeasureTheory.volume) (hconv₂ : ∀ᵐ (x : Fin n → ℝ), MeasureTheory.Integrable (fun (y : Fin n → ℝ) => f₂ (x - y) * g y) MeasureTheory.volume) : (fun (x : Fin n → ℝ) => ∫ (a : Fin n → ℝ), (f₁ (x - a) - f₂ (x - a)) * g a) =ᵐ[MeasureTheory.volume] fun (x : Fin n → ℝ) => (∫ (a : Fin n → ℝ), f₁ (x - a) * g a) - ∫ (a : Fin n → ℝ), f₂ (x - a) * g a

theorem Newton.aemeasurable_smul_measure_of_aemeasurable {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) (μ : MeasureTheory.Measure α) (c : ENNReal) (hf : AEMeasurable f μ) : AEMeasurable f (c • μ)

Transport AEMeasurable across a positive scalar multiple of a measure. If f is a.e.-measurable w.r.t. μ, then it is also a.e.-measurable w.r.t. c • μ. This simple helper is used to avoid threading measurability through map equalities.

theorem Newton.scaled_mollifier_L1_norm_one {n : ℕ} (ψ : (Fin n → ℝ) → ℝ) (η : ℝ) (hη : 0 < η) (hψ_int : MeasureTheory.Integrable ψ MeasureTheory.volume) (hψ_norm : ∫ (x : Fin n → ℝ), ψ x = 1) (hψ_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ ψ x) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => η ^ (-↑n) * ψ fun (i : Fin n) => x i / η) 1 MeasureTheory.volume = ENNReal.ofReal 1

For the scaled mollifier ψ_η with ∫ ψ = 1, we have ‖ψ_η‖₁ = 1.

theorem Newton.convolution_diff_bound_L1 {n : ℕ} (f₁ f₂ ψ : (Fin n → ℝ) → ℂ) (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => (∫ (y : Fin n → ℝ), f₁ (x - y) * ψ y) - ∫ (y : Fin n → ℝ), f₂ (x - y) * ψ y) 1 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f₁ x - f₂ x) 1 MeasureTheory.volume * MeasureTheory.eLpNorm ψ 1 MeasureTheory.volume

Bound on difference of convolutions (L¹ case).

‖(g - f₀) * ψ‖₁ ≤ ‖g - f₀‖₁ · ‖ψ‖₁

Corresponds to h_conv_diff_bound in the code.

theorem Newton.mollifier_convolution_diff_L1 {n : ℕ} (g f₀ : (Fin n → ℝ) → ℂ) (ψ : (Fin n → ℝ) → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hf₀ : MeasureTheory.Integrable f₀ MeasureTheory.volume) (hψ_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ ψ x) (hψ_int : ∫ (x : Fin n → ℝ), ψ x = 1) (η : ℝ) : 0 < η → η < 1 → MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => (∫ (y : Fin n → ℝ), g (x - y) * ↑(η ^ (-↑n) * ψ fun (i : Fin n) => y i / η)) - ∫ (y : Fin n → ℝ), f₀ (x - y) * ↑(η ^ (-↑n) * ψ fun (i : Fin n) => y i / η)) 1 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => g x - f₀ x) 1 MeasureTheory.volume

Bound on difference of convolutions with a normalized mollifier (L¹ case).

If ψ is a non-negative mollifier with unit mass, convolution with the scaled ψ does not increase the L¹ distance between two functions.

theorem Newton.convolution_diff_bound_L2 {n : ℕ} (f₁ f₂ ψ : (Fin n → ℝ) → ℂ) (hf₁ : MeasureTheory.MemLp f₁ 2 MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f₂ 2 MeasureTheory.volume) (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => (∫ (y : Fin n → ℝ), f₁ (x - y) * ψ y) - ∫ (y : Fin n → ℝ), f₂ (x - y) * ψ y) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => f₁ x - f₂ x) 2 MeasureTheory.volume * MeasureTheory.eLpNorm ψ 1 MeasureTheory.volume

Bound on difference of convolutions (L² case).

‖(g - f₀) * ψ‖₂ ≤ ‖g - f₀‖₂ · ‖ψ‖₁

L² version of the above, used for L² error bounds.