Mollification

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: mollification along the stationary translation action

The cutoff core of part (i) of l.approximation.stationary.by.local (Algsuperdiff/Section3/Provider/Corrector/PotentialApproximation.lean, ABK26) consumes a stationary field p together with a stationary square-integrable primitive φ whose spatial realizations are smooth and satisfy ∇(realize φ ω) = realize p ω.

This file builds the smoothing operator that produces such primitives. For a mollifier ρ ∈ C_c^∞(ℝᵈ) and a stationary field X on the abstract carrier Ω it defines

mollify ρ X ω := ∫ y, ρ y • X ((-y) +ᵥ ω),

and proves the two facts that make it useful:

• realize_mollify: the spatial realization of mollify ρ X is the honest convolution ρ ⋆ realize X ω (this is the point of the sign convention (-y) +ᵥ ω), so the smoothness of a realization is that of a convolution against ρ, and every L² field has locally integrable realizations for almost every sample (ae_locallyIntegrable_realize);
• memLp_two_mollify: mollification does not leave the stationary L² layer.

Nothing here uses the potential structure; the file is a pure smoothing toolkit over the abstract stationary carrier of Algsuperdiff/Probability/StationaryProjection.lean.

A weighted Cauchy-Schwarz inequality

theorem Algsuperdiff.Section3.Provider.Corrector.sq_weighted_integral_le {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} {ρ g : α → ℝ} (hρ0 : ∀ (a : α), 0 ≤ ρ a) (hρ : MeasureTheory.Integrable ρ ν) (h1 : MeasureTheory.Integrable (fun (a : α) => ρ a * g a) ν) (h2 : MeasureTheory.Integrable (fun (a : α) => ρ a * g a ^ 2) ν) : (∫ (a : α), ρ a * g a ∂ν) ^ 2 ≤ (∫ (a : α), ρ a ∂ν) * ∫ (a : α), ρ a * g a ^ 2 ∂ν

Cauchy-Schwarz against a probability density: for a weight ρ ≥ 0 of unit mass, the square of the weighted mean is at most the weighted mean of the square.

theorem Algsuperdiff.Section3.Provider.Corrector.sq_weighted_integral_le_of_integral_eq_one {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} {ρ g : α → ℝ} (hρ0 : ∀ (a : α), 0 ≤ ρ a) (hρ1 : ∫ (a : α), ρ a ∂ν = 1) (hρ : MeasureTheory.Integrable ρ ν) (h1 : MeasureTheory.Integrable (fun (a : α) => ρ a * g a) ν) (h2 : MeasureTheory.Integrable (fun (a : α) => ρ a * g a ^ 2) ν) : (∫ (a : α), ρ a * g a ∂ν) ^ 2 ≤ ∫ (a : α), ρ a * g a ^ 2 ∂ν

The normalized form of sq_weighted_integral_le for a probability density.

Mollifiers

structure Algsuperdiff.Section3.Provider.Corrector.Mollifier (d : ℕ) : Type

A smooth compactly supported probability density on ℝᵈ, supported in the ball of radius radius about the origin. This is the kernel ρ of the mollification below.

• toFun : HCPolySupport.Vec d → ℝ

  The density itself.

• radius : ℝ

  The scale of the mollifier: the density vanishes outside B_radius(0).

• nonneg (y : HCPolySupport.Vec d) : 0 ≤ self.toFun y

  The density is nonnegative.

• smooth : ContDiff ℝ (↑⊤) self.toFun

  The density is smooth.

• compactSupport : HasCompactSupport self.toFun

  The density is compactly supported.

• integral_eq_one : ∫ (y : HCPolySupport.Vec d), self.toFun y = 1

  The density has unit mass.

• support_subset : Function.support self.toFun ⊆ Metric.ball 0 self.radius

  The density is supported in the ball of radius radius.

theorem Algsuperdiff.Section3.Provider.Corrector.Mollifier.continuous {d : ℕ} (ρ : Mollifier d) : Continuous ρ.toFun

theorem Algsuperdiff.Section3.Provider.Corrector.Mollifier.integrable {d : ℕ} (ρ : Mollifier d) : MeasureTheory.Integrable ρ.toFun MeasureTheory.volume

noncomputable def Algsuperdiff.Section3.Provider.Corrector.Mollifier.ofRadius (d : ℕ) {r : ℝ} (hr : 0 < r) : Mollifier d

The standard mollifier at a positive scale, built from Mathlib's smooth bump functions.

Equations

• One or more equations did not get rendered due to their size.

Mollification of a stationary field

noncomputable def Algsuperdiff.Section3.Provider.Corrector.mollify {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (ρ : HCPolySupport.Vec d → ℝ) (X : Ω → E) (ω : Ω) : E

Mollification of a stationary field along the translation action. The sign convention (-y) +ᵥ ω is chosen so that the spatial realization is literally the convolution ρ ⋆ realize X ω (realize_mollify).

Equations

• Algsuperdiff.Section3.Provider.Corrector.mollify ρ X ω = ∫ (y : HCPolySupport.Vec d), ρ y • X (-y +ᵥ ω)

theorem Algsuperdiff.Section3.Provider.Corrector.realize_mollify {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (ρ : HCPolySupport.Vec d → ℝ) (X : Ω → E) (ω : Ω) : realize (mollify ρ X) ω = MeasureTheory.convolution ρ (realize X ω) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

The realization of a mollified field is a convolution.

Local integrability of realizations

theorem Algsuperdiff.Section3.Provider.Corrector.ae_locallyIntegrable_realize {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] {X : Ω → E} (hXm : MeasureTheory.StronglyMeasurable X) (hX : MeasureTheory.MemLp X 2 μ) : ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.LocallyIntegrable (realize X ω) MeasureTheory.volume

For almost every sample, the spatial realization of a stationary L² field is locally integrable. This is the hypothesis of the convolution smoothness theorems.

Mollification preserves the stationary L² layer

theorem Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_mollify {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : HCPolySupport.Vec d → ℝ} (hρ : Continuous ρ) {X : Ω → E} (hX : MeasureTheory.StronglyMeasurable X) : MeasureTheory.StronglyMeasurable (mollify ρ X)

The mollification of a measurable field is measurable.

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_prod_weighted_comp_vadd {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {ρ : HCPolySupport.Vec d → ℝ} (hρm : Continuous ρ) (hρ : MeasureTheory.Integrable ρ MeasureTheory.volume) {g : Ω → ℝ} (hgm : MeasureTheory.StronglyMeasurable g) (hg : MeasureTheory.Integrable g μ) : MeasureTheory.Integrable (fun (q : Ω × HCPolySupport.Vec d) => ρ q.2 * g (-q.2 +ᵥ q.1)) (μ.prod MeasureTheory.volume)

Joint integrability of (ω, y) ↦ ρ y · g((-y) +ᵥ ω) for an integrable weight ρ and an integrable stationary observable g.

theorem Algsuperdiff.Section3.Provider.Corrector.ae_integrable_weighted_realize {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] {w : HCPolySupport.Vec d → ℝ} (hw0 : ∀ (y : HCPolySupport.Vec d), 0 ≤ w y) (hwc : Continuous w) (hwi : MeasureTheory.Integrable w MeasureTheory.volume) {X : Ω → E} (hXm : MeasureTheory.StronglyMeasurable X) (hX : MeasureTheory.MemLp X 2 μ) : ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => w y * ‖X (-y +ᵥ ω)‖ ^ 2) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => w y * ‖X (-y +ᵥ ω)‖) MeasureTheory.volume

Almost every sample admits the two weighted integrability facts used by the L² bound on a mollification.

theorem Algsuperdiff.Section3.Provider.Corrector.normSq_mollify_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {κ : HCPolySupport.Vec d → ℝ} (hκc : Continuous κ) (hκi : MeasureTheory.Integrable κ MeasureTheory.volume) {X : Ω → E} (hXm : MeasureTheory.StronglyMeasurable X) (hX : MeasureTheory.MemLp X 2 μ) : ∀ᵐ (ω : Ω) ∂μ, ‖mollify κ X ω‖ ^ 2 ≤ (∫ (y : HCPolySupport.Vec d), |κ y|) * ∫ (y : HCPolySupport.Vec d), |κ y| * ‖X (-y +ᵥ ω)‖ ^ 2

The pointwise square bound behind the L² estimates on a mollification.

theorem Algsuperdiff.Section3.Provider.Corrector.memLp_two_mollify {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {κ : HCPolySupport.Vec d → ℝ} (hκc : Continuous κ) (hκi : MeasureTheory.Integrable κ MeasureTheory.volume) {X : Ω → E} (hXm : MeasureTheory.StronglyMeasurable X) (hX : MeasureTheory.MemLp X 2 μ) : MeasureTheory.MemLp (mollify κ X) 2 μ

Mollification preserves the stationary L² layer.

theorem Algsuperdiff.Section3.Provider.Corrector.integral_normSq_mollify_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {κ : HCPolySupport.Vec d → ℝ} (hκc : Continuous κ) (hκi : MeasureTheory.Integrable κ MeasureTheory.volume) {X : Ω → E} (hXm : MeasureTheory.StronglyMeasurable X) (hX : MeasureTheory.MemLp X 2 μ) : ∫ (ω : Ω), ‖mollify κ X ω‖ ^ 2 ∂μ ≤ (∫ (y : HCPolySupport.Vec d), |κ y|) ^ 2 * ∫ (ω : Ω), ‖X ω‖ ^ 2 ∂μ

The L² contraction estimate for mollification: the mollification by a kernel of total mass ‖κ‖₁ has L² norm at most ‖κ‖₁ times that of the field. For a Mollifier the factor is 1.