HomMollifyIncrement

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 increment estimate (I) and the limit

What this module proves

The remaining two obligations for the family W_n = (w ⋆ ψ)_{· + □_n} of HomMollifyLipschitz:

• (I) |W_n(x) - W_{n-1}(x)| ≤ 2 d A · 3^{n(1-s)} (abs_boxRegularization_sub_pred_le). The proof is the commuting square of the two sliding averages: (W_n)_{x+□_{n-1}} = (W_{n-1})_{x+□_n} (boxAverage_boxRegularization_comm, associativity and commutativity of the convolution), so both W_n and W_{n-1} are within one Lipschitz displacement of the same quantity, and (L) closes the estimate. No new analytic input is needed: (I) is a consequence of (L).

• (hLim) W_{n-k}(x) → (w ⋆ ψ)(x) as k → ∞, for every x (tendsto_boxRegularization_atTop). The mollification w ⋆ ψ is smooth, so its sliding averages converge to it everywhere by continuity — no Lebesgue differentiation is required.

Both are unconditional given the frame of HomMollifyLipschitz.

The constant

(L) runs at d A and (I) at d A (3^{-1}/2 + 3^{s}/2) ≤ d A (1/6 + 1) ≤ 2 d A on 0 < s ≤ 1/2, so both obligations hold at the common constant 2 d A, which is what the holderSeminormBoundOn_of_increments consumes: the Hölder constant is 8 · (2 d A) = 16 d A.

References

• ABK26, Theorem B Step 3.

1. Elementary box-average identities

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_const {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (c : ℝ) : (boxAverage n x fun (x : HCPolySupport.Vec d) => c) = c

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_sub_const {d : ℕ} {n : ℤ} {x : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → ℝ} (c : ℝ) (hf : MeasureTheory.IntegrableOn f (boxSet n x) MeasureTheory.volume) : (boxAverage n x fun (y : HCPolySupport.Vec d) => f y - c) = boxAverage n x f - c

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_boxAverage_sub_self_le {d : ℕ} {n : ℤ} {x : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → ℝ} {Lip : ℝ} (hLip : 0 ≤ Lip) (hf : MeasureTheory.IntegrableOn f (boxSet n x) MeasureTheory.volume) (hlip : ∀ (a b : HCPolySupport.Vec d), |f a - f b| ≤ Lip * ‖a - b‖) : |boxAverage n x f - f x| ≤ Lip * boxRadius n

A Lipschitz function is within Lip · 3^n/2 of its scale-n box average.

2. The commuting square of two sliding averages

theorem Algsuperdiff.Section4.Provider.Homogenization.boxKernel_norm_le {d : ℕ} (n : ℤ) (t : HCPolySupport.Vec d) : ‖boxKernel n t‖ ≤ ((3 ^ ↑n) ^ d)⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_boxRegularization_comm {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hψ : IsMollifierDensity ψ) (n k : ℤ) (x : HCPolySupport.Vec d) : boxAverage k x (boxRegularization n ψ w) = boxAverage n x (boxRegularization k ψ w)

The commuting square. The scale-k average of the scale-n regularization equals the scale-n average of the scale-k regularization: the two sliding averages commute.

3. Continuity and integrability of the regularization

theorem Algsuperdiff.Section4.Provider.Homogenization.continuous_boxRegularization {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hψ : IsMollifierDensity ψ) (n : ℤ) : Continuous (boxRegularization n ψ w)

theorem Algsuperdiff.Section4.Provider.Homogenization.integrableOn_boxRegularization {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hψ : IsMollifierDensity ψ) (n k : ℤ) (x : HCPolySupport.Vec d) : MeasureTheory.IntegrableOn (boxRegularization n ψ w) (boxSet k x) MeasureTheory.volume

4. (I) The increment estimate

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_boxRegularization_sub_pred_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) (hs2 : s ≤ 1 / 2) {ψ : HCPolySupport.Vec d → ℝ} (hψ : IsMollifierDensity ψ) {n : ℤ} (hn : n ≤ m) (x : HCPolySupport.Vec d) : |boxRegularization n ψ w x - boxRegularization (n - 1) ψ w x| ≤ 2 * ↑d * A * 3 ^ (↑n * (1 - s))

(I), the increment obligation.

Two consecutive regularizations differ by at most 2 d A · 3^{n(1-s)}. The proof uses no analytic input beyond (L): the commuting square places both W_n(x) and W_{n-1}(x) within one Lipschitz displacement of the common quantity (W_n)_{x+□_{n-1}} = (W_{n-1})_{x+□_n}.

5. (hLim) The convergence of the family

theorem Algsuperdiff.Section4.Provider.Homogenization.tendsto_boxRadius_atTop (n : ℤ) : Filter.Tendsto (fun (k : ℕ) => boxRadius (n - ↑k)) Filter.atTop (nhds 0)

The box radii shrink to zero as the scale descends.

theorem Algsuperdiff.Section4.Provider.Homogenization.tendsto_boxRegularization_atTop {d : ℕ} {w ψ : HCPolySupport.Vec d → ℝ} (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hψ : IsMollifierDensity ψ) (n : ℤ) (x : HCPolySupport.Vec d) : Filter.Tendsto (fun (k : ℕ) => boxRegularization (n - ↑k) ψ w x) Filter.atTop (nhds (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x))

(hLim), the convergence obligation. The regularizations converge to the mollification w ⋆ ψ at every point, by continuity of the smooth function w ⋆ ψ — no Lebesgue differentiation is used.