HomSpineRepLimit

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 continuous representative, PRODUCED

What this module is

The §4.5 spine has ONE irreducible frame item: the existence of a continuous representative of the H¹₀ zero extension of u - v. The print obtains it in the paper by citing u - v ∈ H¹₀(□_m), which for d ≥ 2 does not supply one; the correction records the gap and the suggested print correction. This module carries it out:

  (a)  w ⋆ ψ_k → w   a.e.                      (ae_tendsto_convolution_mollifyBump)
  (b)  each w ⋆ ψ_k is (1-s, 16 d A)-Hölder     (the mollifier chain, ψ-uniform)
  (c)  (a) + (b)  ⟹  w has a continuous representative

Step (a) is Mathlib's ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable; its ratio hypothesis rOut ≤ K · rIn holds for the mollifyBump at K = 2 EXACTLY (rOut = 1/(k+1), rIn = 1/(2(k+1))). Step (b) is the holderSeminormBoundOn_convolution_of_uniformBoxGauge, whose constant does not depend on the mollifier. Step (c) is the scalar precise-representative lemma exists_continuous_ae_eq_of_uniformHolderBall proved here.

Why (c) needs no compactness

The classical route is Arzelà–Ascoli on the closure of the cube. It is not needed: a co-null set is DENSE, and equicontinuity transports the Cauchy property from a dense set to EVERY point,

  |f_k x - f_j x| ≤ 2 K ‖x - z‖^α + |f_k z - f_j z|,

so (f_k x) is Cauchy at every x and the pointwise limit g exists everywhere. g is then Hölder on every ball of radius r by the holderSeminormBoundOn_of_tendsto, hence continuous; and g = w wherever the a.e. convergence holds, hence a.e. No covering, no compactness, no completeness beyond that of ℝ.

Main results

• ae_tendsto_convolution_mollifyBump — step (a), the a.e. mollifier limit;
• exists_continuous_ae_eq_of_uniformHolderBall — step (c), the scalar precise representative from a uniformly Hölder, a.e.-convergent family;
• exists_continuous_ae_eq_of_uniformBoxGauge — THE PRODUCER: the continuous representative from the negative-order gauge on ∇w plus local integrability and compact support ALONE. No representative is assumed.

References

• ABK26, Theorem B Step 3.

1. The a.e. mollifier limit

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_tendsto_convolution_mollifyBump {d : ℕ} {w : HCPolySupport.Vec d → ℝ} (hwI : MeasureTheory.Integrable w MeasureTheory.volume) : ∀ᵐ (x : HCPolySupport.Vec d), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.convolution w ((mollifyBump k).normed MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x) Filter.atTop (nhds (w x))

The a.e. mollification limit.

For an integrable scalar, the mollifications along the shrinking bump family converge almost everywhere. This is Mathlib's Lebesgue-point statement; the only repository-specific input is the radius ratio, which for mollifyBump is rOut = 2 · rIn exactly, so the hypothesis holds at K = 2 with no slack.

2. Hölder bounds and distances

theorem Algsuperdiff.Section4.Provider.Homogenization.dist_lt_of_holderSeminormBoundOn {d : ℕ} {alpha K r eps : ℝ} {h : HCPolySupport.Vec d → ℝ} {z x y : HCPolySupport.Vec d} (hh : Support.HolderSeminormBoundOn (Metric.closedBall z r) alpha K h) (hx : x ∈ Metric.closedBall z r) (hy : y ∈ Metric.closedBall z r) (hmod : K * dist x y ^ alpha < eps) : dist (h x) (h y) < eps

A Hölder bound on a ball, read as a distance estimate.

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_delta_holder_lt {alpha K : ℝ} (halpha : 0 < alpha) {eps : ℝ} (heps : 0 < eps) : ∃ (delta : ℝ), 0 < delta ∧ ∀ (t : ℝ), 0 ≤ t → t < delta → K * t ^ alpha < eps

The modulus of continuity of a Hölder bound. For a positive exponent the map t ↦ K t^α vanishes at 0, so every tolerance is met on a small enough scale.

3. The scalar precise representative

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_continuous_ae_eq_of_uniformHolderBall {d : ℕ} {alpha K r : ℝ} (halpha : 0 < alpha) (hr : 0 < r) {f : ℕ → HCPolySupport.Vec d → ℝ} {w : HCPolySupport.Vec d → ℝ} (hf : ∀ (z : HCPolySupport.Vec d) (k : ℕ), Support.HolderSeminormBoundOn (Metric.closedBall z r) alpha K (f k)) (hae : ∀ᵐ (x : HCPolySupport.Vec d), Filter.Tendsto (fun (k : ℕ) => f k x) Filter.atTop (nhds (w x))) : ∃ (g : HCPolySupport.Vec d → ℝ), Continuous g ∧ w =ᵐ[MeasureTheory.volume] g

THE SCALAR PRECISE REPRESENTATIVE.

A family of scalars that is uniformly Hölder — one exponent α > 0, one constant K, on every closed ball of one fixed radius r > 0 — and converges almost everywhere has a CONTINUOUS limit, defined at every point, which is an everywhere-defined representative of the a.e. limit.

The proof is the equicontinuity transport described in the module docstring: the convergence set is co-null, hence dense; the Hölder bound turns density into the Cauchy property at every point; ℝ is complete.

4. The producer

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_continuous_ae_eq_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 → ℝ), Continuous g ∧ w =ᵐ[MeasureTheory.volume] g

THE PRODUCER — the continuous representative from the gauge alone.

From the translate-uniform negative gauge of order -s on ∇w, together with the frame items the chain already needs (w weakly differentiable on Vec d, integrable, compactly supported, gradient coordinates integrable), the scalar w HAS a continuous representative. Nothing about a representative is assumed: this is the step the manuscript obtains by citing H¹₀ membership, which does not supply it.

The radius is r = 3^m / 2, so that a closed r-ball has diameter at most 3^m and the ψ-uniform Hölder bound applies on it with constant 16 d A.