OscillationDecayWeak

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

The arbitrary-gap oscillation decay for a weakly harmonic function

OscillationDecayGap proves the arbitrary-gap decay || grad u - (grad u)_{z + cu_n} ||_{L2bar} <= C (d) 3^{-k} || grad u - c || for a function u that is smooth and harmonic on the coarse cube. The object the argument downstream actually produces is not smooth: a harmonic replacement obtained from an H^1_0 solve is only H^1, hence only weakly harmonic in the sense of HarmonicWeak, and HarmonicWeak cannot bootstrap its own regularity.

This module removes that mismatch. HarmonicMollifyWeyl provides the interior smooth representative of a weakly harmonic function; combined with the proved decay it yields the same estimate for the smooth representative, on cubes one triadic scale inside the harmonicity cube.

What is lost, and why

The mollification consumes one triadic scale: the smooth representative is produced on z + cu_{n+k-1}, not on z + cu_{n+k}, because the mollifying kernel needs room. Two things follow.

• The gap restriction becomes k >= d + 3 instead of k >= d + 2: the proved estimate is applied with gap k - 1.
• The right-hand side measures the deviation on z + cu_{n+k-1}. The decay factor is still written 3^{-k}; the single lost scale is absorbed into the dimensional constant (it multiplies it by 3).

The conclusion is stated for the smooth representative v, together with v = u almost everywhere on z + cu_{n+k-1}. That is the usable form: all the quantities in the estimate are integrals of grad v, and a consumer holding u in H^1 identifies grad v with the weak gradient of u from the almost-everywhere equality. Stating the estimate for euclideanGradient u directly would be vacuous, since the pointwise fderiv of a merely H^1 function carries no information.

Portability

This file depends only on Mathlib and on CoarseGraining (Homogenization.*) and on other files of this same harmonic/oscillation layer. It mentions no object of the manuscript: no model, no cutoff, no shell, no corrector. It is intended to be portable into CoarseGraining by a single mechanical namespace rename.

Contents

• euclideanClosedBall_subset_openCubeAtScale_of_succ -- the one triadic scale of room: a Euclidean ball of radius 3^p around a point of z + cu_p sits inside z + cu_{p+1}.
• exists_gradient_oscillation_gap_decay_of_isWeaklyHarmonicOn -- the decay for a weakly harmonic function, through its smooth representative.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanClosedBall_subset_openCubeAtScale_of_succ {d : ℕ} {z : HCPolySupport.Vec d} {p : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z p) : HCPolySupport.euclideanClosedBall x (3 ^ p) ⊆ HCPolySupport.Book.Ch03.openCubeAtScale z (p + 1)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_gradient_oscillation_gap_decay_of_isWeaklyHarmonicOn {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : HCPolySupport.Vec d → ℝ), MeasureTheory.LocallyIntegrable u MeasureTheory.volume → ∀ (z : HCPolySupport.Vec d) (n : ℤ) (k : ℕ), d + 3 ≤ k → IsWeaklyHarmonicOn (HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k)) u → ∃ (v : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) v ∧ (∀ᵐ (x : HCPolySupport.Vec d), x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k - 1) → v x = u x) ∧ ∀ (c : HCPolySupport.Vec d), √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z n) (HCPolySupport.euclideanGradient v)) ≤ C * 3 ^ (-↑k) * √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k - 1)) (HCPolySupport.euclideanGradient v) c)