MollifierScaling

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

Provider: scaled smoothing densities with an explicit sup-norm bound

The decorrelation bound of Algsuperdiff/Section3/Provider/Corrector/MollifiedDecorrelation.lean (integral_normSq_mollify_le_of_covariance_support) is quantified by the sup norm of the smoothing density: for a probability density κ bounded by M,

E[|A_κ X|²] ≤ M · |B_ρ| · E[|X|²].

Using it therefore requires a family of probability densities whose sup norms tend to 0. Algsuperdiff/Section3/Provider/Corrector/Mollification.lean already builds smooth compactly supported probability densities at every scale (Mollifier.ofRadius), but the Mollifier structure records no sup bound. This file supplies the missing bound, with the explicit dimensional constant 1:

• productDensity — the d-fold tensor product of a one-dimensional bump at scale r, i.e. x ↦ ∏ i, φ_r(x i). It is nonnegative, smooth, compactly supported in B_r(0), integrable, of unit mass (integral_productDensity, by Fubini) and bounded by 1 / r ^ d (productDensity_le). It is packaged as a Mollifier by Mollifier.ofProduct.

The product density is recorded in addition to Mollifier.ofRadius because its tensor structure is what makes the telescoping divergence kernel of Algsuperdiff/Section3/Provider/Corrector/DivergenceKernel.lean work: there the same one-dimensional factor scaledBump appears at two different scales.

Disclosure. Nothing in this file realizes any source node. It is a quantitative refinement of the smoothing toolkit and claims no node status.

A scaled one-dimensional bump

noncomputable def Algsuperdiff.Section3.Provider.Corrector.lineBump {r : ℝ} (hr : 0 < r) : ContDiffBump 0

Mathlib's smooth bump function on the line with inner radius r/2 and outer radius r.

Equations

• Algsuperdiff.Section3.Provider.Corrector.lineBump hr = { rIn := r / 2, rOut := r, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

@[simp]

theorem Algsuperdiff.Section3.Provider.Corrector.lineBump_rIn {r : ℝ} (hr : 0 < r) : (lineBump hr).rIn = r / 2

@[simp]

theorem Algsuperdiff.Section3.Provider.Corrector.lineBump_rOut {r : ℝ} (hr : 0 < r) : (lineBump hr).rOut = r

noncomputable def Algsuperdiff.Section3.Provider.Corrector.scaledBump {r : ℝ} (hr : 0 < r) : ℝ → ℝ

The one-dimensional smooth compactly supported probability density at scale r.

Equations

• Algsuperdiff.Section3.Provider.Corrector.scaledBump hr = (Algsuperdiff.Section3.Provider.Corrector.lineBump hr).normed MeasureTheory.volume

theorem Algsuperdiff.Section3.Provider.Corrector.scaledBump_nonneg {r : ℝ} (hr : 0 < r) (t : ℝ) : 0 ≤ scaledBump hr t

theorem Algsuperdiff.Section3.Provider.Corrector.contDiff_scaledBump {r : ℝ} (hr : 0 < r) : ContDiff ℝ (↑⊤) (scaledBump hr)

theorem Algsuperdiff.Section3.Provider.Corrector.continuous_scaledBump {r : ℝ} (hr : 0 < r) : Continuous (scaledBump hr)

theorem Algsuperdiff.Section3.Provider.Corrector.support_scaledBump {r : ℝ} (hr : 0 < r) : Function.support (scaledBump hr) = Metric.ball 0 r

theorem Algsuperdiff.Section3.Provider.Corrector.integral_scaledBump {r : ℝ} (hr : 0 < r) : ∫ (t : ℝ), scaledBump hr t = 1

theorem Algsuperdiff.Section3.Provider.Corrector.scaledBump_eq_zero {r : ℝ} (hr : 0 < r) {t : ℝ} (ht : r ≤ |t|) : scaledBump hr t = 0

The one-dimensional density vanishes outside the interval (-r, r).

theorem Algsuperdiff.Section3.Provider.Corrector.scaledBump_le {r : ℝ} (hr : 0 < r) (t : ℝ) : scaledBump hr t ≤ 1 / r

The sup-norm bound for the one-dimensional density.

The scaled product density on Vec d

noncomputable def Algsuperdiff.Section3.Provider.Corrector.productDensity {r : ℝ} (d : ℕ) (hr : 0 < r) : HCPolySupport.Vec d → ℝ

The scaled product density on Vec d: the d-fold tensor product of the one-dimensional bump at scale r.

Equations

• Algsuperdiff.Section3.Provider.Corrector.productDensity d hr x = ∏ i : Fin d, Algsuperdiff.Section3.Provider.Corrector.scaledBump hr (x i)

theorem Algsuperdiff.Section3.Provider.Corrector.productDensity_nonneg {r : ℝ} (d : ℕ) (hr : 0 < r) (x : HCPolySupport.Vec d) : 0 ≤ productDensity d hr x

theorem Algsuperdiff.Section3.Provider.Corrector.contDiff_productDensity {r : ℝ} (d : ℕ) (hr : 0 < r) : ContDiff ℝ (↑⊤) (productDensity d hr)

theorem Algsuperdiff.Section3.Provider.Corrector.continuous_productDensity {r : ℝ} (d : ℕ) (hr : 0 < r) : Continuous (productDensity d hr)

theorem Algsuperdiff.Section3.Provider.Corrector.productDensity_eq_zero_of_le {r : ℝ} (d : ℕ) (hr : 0 < r) {x : HCPolySupport.Vec d} (hx : r ≤ ‖x‖) : productDensity d hr x = 0

The product density vanishes outside the sup-norm ball of radius r.

theorem Algsuperdiff.Section3.Provider.Corrector.support_productDensity_subset {r : ℝ} (d : ℕ) (hr : 0 < r) : Function.support (productDensity d hr) ⊆ Metric.ball 0 r

theorem Algsuperdiff.Section3.Provider.Corrector.hasCompactSupport_productDensity {r : ℝ} (d : ℕ) (hr : 0 < r) : HasCompactSupport (productDensity d hr)

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_productDensity {r : ℝ} (d : ℕ) (hr : 0 < r) : MeasureTheory.Integrable (productDensity d hr) MeasureTheory.volume

theorem Algsuperdiff.Section3.Provider.Corrector.integral_productDensity {r : ℝ} (d : ℕ) (hr : 0 < r) : ∫ (x : HCPolySupport.Vec d), productDensity d hr x = 1

The product density is a probability density. This is Fubini on the finite product Vec d = Fin d → ℝ.

theorem Algsuperdiff.Section3.Provider.Corrector.productDensity_le {r : ℝ} (d : ℕ) (hr : 0 < r) (x : HCPolySupport.Vec d) : productDensity d hr x ≤ 1 / r ^ d

The sup-norm bound for the product density, with dimensional constant 1: ‖κ_r‖_∞ ≤ r^{-d}.

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

The scaled product density packaged as a Mollifier.

Equations

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