HomMollifyChain

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 S44-J chain, end to end

The composed theorem

Two ingredients together close the Step-3c bridge of Theorem B, and this module performs the composition.

  UniformBoxGaugeBound m s A (∇w)            (the negative-order gradient bound)
      ⟹  [w]_{C^{0,1-s}} ≤ 16 d A            (holderSeminormBoundOn_of_uniformBoxGauge)
      ⟹  3^{-m}‖w‖_{L^∞(□_m)} ≤ 16 d A 3^{-ms}   (ae_linfty_of_uniformBoxGauge_originCube)

• the mollifier calculus supplies: (L), (I), (hLim) for the family W_n = (w ⋆ ψ)_{· + □_n} at the common constant 2 d A.
• the lifting supplies the telescoping estimate (absolute constant 8) and the L^∞ endpoint (constant exactly 1).
• The mollifier is then removed: the Hölder bound is uniform in ψ, and w ⋆ ψ_k → w pointwise at the continuous representative along any bump sequence with shrinking radii (ContDiffBump.convolution_tendsto_right_of_continuous), so the bound passes to the limit (HolderSeminormBoundOn.of_tendsto).

The final constant is 16 · d · A: the absolute 8, the common constant 2 d A. The d is the sup-norm duality of HomMollifyLipschitz; nothing else dimensional enters.

What the consumer must supply

Besides the negative-order gauge on ∇w, the frame items are:

• HasWeakGradientOn Set.univ w G with w integrable and compactly supported and each G · i integrable — for w = u - v ∈ H¹₀(□_m) this is CoarseGraining's H10Function.hasWeakGradientOn_univ_zeroExtension applied to the zero extension, whose MemLp fields give the integrability;
• a continuous representative g =ᵐ w. This is the same representative-level input the lifting already needs for the boundary hypothesis hzero (HomLiftEndpoint), and it is where the a.e.-defined Sobolev object is replaced by a genuine function.

References

• ABK26, Theorem B Step 3.

1. Hölder bounds pass to pointwise limits

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_of_tendsto {d : ℕ} {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : ℕ → HCPolySupport.Vec d → ℝ} {g : HCPolySupport.Vec d → ℝ} (hf : ∀ (k : ℕ), Support.HolderSeminormBoundOn U alpha K (f k)) (hlim : ∀ x ∈ U, Filter.Tendsto (fun (k : ℕ) => f k x) Filter.atTop (nhds (g x))) : Support.HolderSeminormBoundOn U alpha K g

A Hölder bound valid along a pointwise-convergent sequence passes to the limit.

2. The Hölder bound for the mollification

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_convolution_of_uniformBoxGauge {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) (hs0 : 0 < s) (hs2 : s ≤ 1 / 2) {ψ : HCPolySupport.Vec d → ℝ} (hψ : IsMollifierDensity ψ) {U : Set (HCPolySupport.Vec d)} (hdiam : ∀ x ∈ U, ∀ y ∈ U, ‖x - y‖ ≤ 3 ^ ↑m) : Support.HolderSeminormBoundOn U (1 - s) (16 * ↑d * A) (MeasureTheory.convolution w ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

The lifting for the mollified function.

Under the translate-uniform negative gauge of order -s on ∇w, every mollification w ⋆ ψ obeys the Hölder bound of exponent 1 - s at the constant 16 d A, on any set of diameter at most 3^m. The constant does not depend on ψ.

3. Removing the mollifier

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.mollifyBump {d : ℕ} (k : ℕ) : ContDiffBump 0

A shrinking sequence of bump functions on Vec d.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.mollifyBump k = { rIn := 1 / (2 * (↑k + 1)), rOut := 1 / (↑k + 1), rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem Algsuperdiff.Section4.Provider.Homogenization.mollifyBump_rOut {d : ℕ} (k : ℕ) : (mollifyBump k).rOut = 1 / (↑k + 1)

theorem Algsuperdiff.Section4.Provider.Homogenization.tendsto_mollifyBump_rOut {d : ℕ} : Filter.Tendsto (fun (k : ℕ) => (mollifyBump k).rOut) Filter.atTop (nhds 0)

theorem Algsuperdiff.Section4.Provider.Homogenization.isMollifierDensity_mollifyBump {d : ℕ} (k : ℕ) : IsMollifierDensity ((mollifyBump k).normed MeasureTheory.volume)

The normalized bump is a mollifier density.

4. The composed lifting

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_of_uniformBoxGauge {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) (hs0 : 0 < s) (hs2 : s ≤ 1 / 2) {g : HCPolySupport.Vec d → ℝ} (hgc : Continuous g) (hgw : w =ᵐ[MeasureTheory.volume] g) {U : Set (HCPolySupport.Vec d)} (hdiam : ∀ x ∈ U, ∀ y ∈ U, ‖x - y‖ ≤ 3 ^ ↑m) : Support.HolderSeminormBoundOn U (1 - s) (16 * ↑d * A) g

THE S44-J LIFTING, END TO END.

From the translate-uniform negative gauge of order -s on ∇w — the manuscript's ‖∇u - ∇v‖_{W^{-s,∞}(□_m)} bound, at the translate carrier — the continuous representative g of w is Hölder continuous of exponent 1 - s with constant 16 d A, on any set of diameter at most 3^m.

This is the principle that "W^{-s,∞} for the gradient is like C^{0,1-s} for the function") made into a theorem.

5. The L^∞ endpoint, in the shape of the frozen root's clause (C3)

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_linfty_of_uniformBoxGauge_originCube {d : ℕ} [NeZero 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) (hs0 : 0 < s) (hs2 : s ≤ 1 / 2) {g : HCPolySupport.Vec d → ℝ} (hgc : Continuous g) (hgw : w =ᵐ[MeasureTheory.volume] g) (hzero : ∀ y ∈ cubeFaceSet (HCPolySupport.originCube d m), g y = 0) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), 3 ^ (-↑m) * |g x| ≤ 16 * ↑d * A * 3 ^ (-↑m * s)

The Step-3c display, at the origin cube.

From the negative-order gauge on ∇w at the scales n ≤ m, together with the vanishing of the continuous representative on the faces of □_m — the rendering of u - v ∈ H¹₀(□_m) — one obtains

  3^{-m} |g(x)| ≤ 16 d A · 3^{-ms}   for a.e. x ∈ □_m,

which is exactly the shape of the frozen root's clause (C3), the introduction's homogenization estimate, with the explicit constant 16 d.