HomMollifyLipschitz

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

Theorem B, §4.5, Step 3c: the scale-n Lipschitz estimate (L)

What this module proves

The regularization family of this file is

  W_n:= (w ⋆ ψ)_{· + □_n}    (mollify by `ψ`, then slide the scale-`n` box)

(boxRegularization). Its gradient is computed twice — once for each convolution factor — and each computation is one of the swaps of HomMollifySwap:

• fderiv_convolution_apply_basisVec — ∂_i(w ⋆ ψ) = (∇w)_i ⋆ ψ, the weak gradient swap (S2);
• fderiv_boxRegularization_apply — ∇W_n(x) v = Σ_i v_i ((∇w)_i ⋆ ψ)_{x+□_n}, i.e. the gradient of the sliding average is the sliding average of the gradient, by the box-kernel identity of HomMollifyPairing.

Feeding the averaging swap (S1) and the kernel pairing into the second display gives the gradient bound

  ‖∇W_n(x)‖ ≤ d · A · 3^{-ns}

(norm_fderiv_boxRegularization_le), and the mean value inequality on the convex set Vec d turns it into the obligation

  (L)   |W_n(x) - W_n(y)| ≤ (d · A) · 3^{-ns} · ‖x - y‖.

Where the dimensional constant comes from

The pairing itself costs nothing (HomMollifyPairing, constant 1). The factor d is the only dimensional loss in the whole chain, and it is the sup-norm duality: on Vec d = Fin d → ℝ with the supremum norm, a linear functional v ↦ Σ_i g_i v_i has operator norm Σ_i |g_i| ≤ d · max_i |g_i|, and the gauge controls the maximum. So C(d) = d exactly, and the constant 8 composes to 8 d A.

References

• ABK26, Theorem B Step 3.

1. The mollifier profile

structure Algsuperdiff.Section4.Provider.Homogenization.IsMollifierDensity {d : ℕ} (ψ : HCPolySupport.Vec d → ℝ) : Prop

A mollifier density: a smooth, compactly supported probability density on Vec d. Convolving with it is the smoothing step of the regularization.

• smooth : ContDiff ℝ (↑⊤) ψ
• compactSupport : HasCompactSupport ψ
• nonneg (z : HCPolySupport.Vec d) : 0 ≤ ψ z
• integral_eq_one : ∫ (z : HCPolySupport.Vec d), ψ z = 1

theorem Algsuperdiff.Section4.Provider.Homogenization.IsMollifierDensity.continuous {d : ℕ} {ψ : HCPolySupport.Vec d → ℝ} (h : IsMollifierDensity ψ) : Continuous ψ

theorem Algsuperdiff.Section4.Provider.Homogenization.IsMollifierDensity.integrable {d : ℕ} {ψ : HCPolySupport.Vec d → ℝ} (h : IsMollifierDensity ψ) : MeasureTheory.Integrable ψ MeasureTheory.volume

theorem Algsuperdiff.Section4.Provider.Homogenization.IsMollifierDensity.exists_bound {d : ℕ} {ψ : HCPolySupport.Vec d → ℝ} (h : IsMollifierDensity ψ) : ∃ (C : ℝ), ∀ (t : HCPolySupport.Vec d), ‖ψ t‖ ≤ C

2. The regularization family

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.boxRegularization {d : ℕ} (n : ℤ) (ψ w : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : ℝ

The scale-n regularization of w: mollify by ψ, then take the sliding scale-n box average.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.boxRegularization_def {d : ℕ} (n : ℤ) (ψ w : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : boxRegularization n ψ w x = boxAverage n x (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

theorem Algsuperdiff.Section4.Provider.Homogenization.boxRegularization_eq_convolution {d : ℕ} (n : ℤ) (ψ w : HCPolySupport.Vec d → ℝ) : boxRegularization n ψ w = MeasureTheory.convolution (boxKernel n) (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

The regularization is the convolution of the box kernel with the mollification.

3. The gradient of the mollification

theorem Algsuperdiff.Section4.Provider.Homogenization.contDiff_convolution_mollifier {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwLoc : MeasureTheory.LocallyIntegrable w MeasureTheory.volume) (hψ : IsMollifierDensity ψ) : ContDiff ℝ (↑⊤) (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

The mollification of a locally integrable function by a mollifier density is smooth.

theorem Algsuperdiff.Section4.Provider.Homogenization.hasCompactSupport_convolution_mollifier {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwc : HasCompactSupport w) (hψ : IsMollifierDensity ψ) : HasCompactSupport (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

The mollification of a compactly supported function has compact support.

theorem Algsuperdiff.Section4.Provider.Homogenization.fderiv_convolution_apply_basisVec {d : ℕ} {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Set.univ w G) (hwLoc : MeasureTheory.LocallyIntegrable w MeasureTheory.volume) {ψ : HCPolySupport.Vec d → ℝ} (hψ : IsMollifierDensity ψ) (i : Fin d) (a : HCPolySupport.Vec d) : (fderiv ℝ (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) a) (HCPolySupport.basisVec i) = MeasureTheory.convolution (fun (y : HCPolySupport.Vec d) => G y i) ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume a

∂_i (w ⋆ ψ) = (∇w)_i ⋆ ψ — the weak gradient swap in derivative form.

4. The gradient of the regularization

theorem Algsuperdiff.Section4.Provider.Homogenization.eq_sum_smul_basisVec {d : ℕ} (v : HCPolySupport.Vec d) : v = ∑ i : Fin d, v i • HCPolySupport.basisVec i

Every vector is the sum of its coordinates times the basis vectors.

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_finset_sum {d : ℕ} {n : ℤ} {x : HCPolySupport.Vec d} (c : Fin d → ℝ) (h : Fin d → HCPolySupport.Vec d → ℝ) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (h i) (boxSet n x) MeasureTheory.volume) : (boxAverage n x fun (a : HCPolySupport.Vec d) => ∑ i : Fin d, c i * h i a) = ∑ i : Fin d, c i * boxAverage n x (h i)

The box average is linear over a finite combination of integrable functions.

theorem Algsuperdiff.Section4.Provider.Homogenization.fderiv_boxRegularization_apply {d : ℕ} {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Set.univ w G) (hwLoc : MeasureTheory.LocallyIntegrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hGloc : ∀ (i : Fin d), MeasureTheory.LocallyIntegrable (fun (y : HCPolySupport.Vec d) => G y i) MeasureTheory.volume) {ψ : HCPolySupport.Vec d → ℝ} (hψ : IsMollifierDensity ψ) (n : ℤ) (x v : HCPolySupport.Vec d) : (fderiv ℝ (boxRegularization n ψ w) x) v = ∑ i : Fin d, v i * boxAverage n x (MeasureTheory.convolution (fun (y : HCPolySupport.Vec d) => G y i) ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

The gradient of the regularization. For every direction v,

  ∇W_n(x) v = Σ_i v_i · ((∇w)_i ⋆ ψ)_{x+□_n}.

theorem Algsuperdiff.Section4.Provider.Homogenization.differentiable_boxRegularization {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwLoc : MeasureTheory.LocallyIntegrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hψ : IsMollifierDensity ψ) (n : ℤ) : Differentiable ℝ (boxRegularization n ψ w)

The regularization is differentiable everywhere.

5. The gradient bound and (L)

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_fderiv_boxRegularization_le {d : ℕ} {m : ℤ} {s A : ℝ} {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Set.univ w G) (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hGI : ∀ (i : Fin d), MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => G y i) MeasureTheory.volume) (hgauge : UniformBoxGaugeBound m s A G) {ψ : HCPolySupport.Vec d → ℝ} (hψ : IsMollifierDensity ψ) {n : ℤ} (hn : n ≤ m) (x : HCPolySupport.Vec d) : ‖fderiv ℝ (boxRegularization n ψ w) x‖ ≤ ↑d * A * 3 ^ (-(↑n * s))

The gradient bound. Under the translate-uniform gauge of order -s on ∇w, the scale-n regularization has gradient bounded by d · A · 3^{-ns} everywhere.

The dimensional factor d is the sup-norm duality on Vec d and is the only dimensional loss in the chain; the pairing itself costs nothing.

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_boxRegularization_sub_le {d : ℕ} {m : ℤ} {s A : ℝ} {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Set.univ w G) (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hGI : ∀ (i : Fin d), MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => G y i) MeasureTheory.volume) (hgauge : UniformBoxGaugeBound m s A G) {ψ : HCPolySupport.Vec d → ℝ} (hψ : IsMollifierDensity ψ) {n : ℤ} (hn : n ≤ m) (x y : HCPolySupport.Vec d) : |boxRegularization n ψ w x - boxRegularization n ψ w y| ≤ ↑d * A * 3 ^ (-(↑n * s)) * ‖x - y‖

(L), the Lipschitz obligation.

The scale-n regularization of w is Lipschitz with constant d · A · 3^{-ns}, exactly the shape HomLiftTelescope.holderSeminormBoundOn_of_increments consumes.