HarmonicReplaceGradient

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

Identifying the Weyl representative's gradient with the weak gradient

OscillationDecayWeak states the per-scale decay for the smooth interior representative v of a weakly harmonic function, because the pointwise fderiv of a merely H^1 function carries no information. The telescope, however, accumulates the mean-square oscillations of the weak gradient of the harmonic replacement, since that is the object the energy estimate controls. This module closes the gap.

The mechanism is uniqueness of weak derivatives. On the open set V where v = h almost everywhere, both euclideanGradient v (because v is smooth) and grad h (by restriction from the larger set) are weak gradients of the same function -- the weak-derivative identity only sees its argument through an integral, so an almost-everywhere change of representative leaves it intact. CoarseGraining's HasWeakPartialDerivOn.ae_eq then identifies them almost everywhere on V, and every mean-square functional in the estimate is an integral, hence blind to the difference.

A second, smaller mismatch is handled here too. The interior Weyl lemma needs a globally locally integrable representative, which an H^1(U) function is not: its values off U are unconstrained. Replacing it by its extension by zero U.indicator h removes the mismatch without changing anything: the weak-harmonicity pairing is an integral over U only.

Contents

• IsWeaklyHarmonicOn.congr_on -- weak harmonicity depends only on the values on the set.
• integrable_indicator_of_memL2On -- the extension by zero of an L^2 function on a finite-measure set is globally integrable.
• HasWeakPartialDerivOn.congr_ae -- the weak-derivative identity is stable under an almost-everywhere change of the differentiated function.
• ae_eq_euclideanGradient_of_ae_eq_of_contDiff -- the identification.
• meanSquareDeviationVecOn_congr_ae, volumeAverageVec_congr_ae, meanSquareOscillationVecOn_congr_ae -- the mean-square functionals are blind to null sets.
• exists_gradient_oscillation_gap_decay_weakGradient -- the payload: the arbitrary-gap decay, stated for the weak gradient of an H^1 weakly harmonic function, which is the form the telescope consumes.

Portability

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

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.IsWeaklyHarmonicOn.congr_on {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u u' : HCPolySupport.Vec d → ℝ} (hu : IsWeaklyHarmonicOn U u) (hU : MeasurableSet U) (heq : ∀ x ∈ U, u' x = u x) : IsWeaklyHarmonicOn U u'

Weak harmonicity on U depends only on the values of the function on U: the defining pairing is an integral over U.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrable_indicator_of_memL2On {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] {u : HCPolySupport.Vec d → ℝ} (hu : HCPolySupport.MemL2On U u) : MeasureTheory.Integrable (U.indicator u) MeasureTheory.volume

The extension by zero of an L^2 function on a finite-measure measurable set is globally integrable, hence globally locally integrable: exactly the hypothesis the interior Weyl lemma imposes on its input.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.HasWeakPartialDerivOn.congr_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} {i : Fin d} {u u' gi : HCPolySupport.Vec d → ℝ} (h : HCPolySupport.HasWeakPartialDerivOn U i u gi) (hae : u' =ᵐ[MeasureTheory.volume.restrict U] u) : HCPolySupport.HasWeakPartialDerivOn U i u' gi

The weak-derivative identity is stable under an almost-everywhere change of the differentiated function: it sees that function only through an integral.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.ae_eq_euclideanGradient_of_ae_eq_of_contDiff {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hVU : V ⊆ U) [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] (h : HCPolySupport.H1Function U) {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 1 v) (hae : v =ᵐ[MeasureTheory.volume.restrict V] h.toFun) : HCPolySupport.euclideanGradient v =ᵐ[MeasureTheory.volume.restrict V] h.grad

Identification of the two gradients.

If a C^1 function v agrees almost everywhere on an open subset V of U with an H^1(U) function h, then the pointwise Euclidean gradient of v agrees almost everywhere on V with the weak gradient of h.

Both fields are weak gradients of the same function on V -- the first because v is C^1, the second by restriction from U followed by the almost-everywhere transport above -- and weak gradients are almost everywhere unique on open sets.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationVecOn_congr_ae {d : ℕ} {V : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hfg : f =ᵐ[MeasureTheory.volume.restrict V] g) (c : HCPolySupport.Vec d) : HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V f c = HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V g c

Mean-square deviation of a vector field is blind to null sets.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.volumeAverageVec_congr_ae {d : ℕ} {V : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hfg : f =ᵐ[MeasureTheory.volume.restrict V] g) : HCPolySupport.volumeAverageVec V f = HCPolySupport.volumeAverageVec V g

The volume average of a vector field is blind to null sets.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareOscillationVecOn_congr_ae {d : ℕ} {V : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hfg : f =ᵐ[MeasureTheory.volume.restrict V] g) : HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V f = HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V g

Mean-square oscillation of a vector field is blind to null sets.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_gradient_oscillation_gap_decay_weakGradient {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : HCPolySupport.Vec d) (n : ℤ) (k : ℕ), d + 3 ≤ k → ∀ (h : HCPolySupport.H1Function (HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k))), IsWeaklyHarmonicOn (HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k)) h.toFun → ∀ (c : HCPolySupport.Vec d), √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z n) h.grad) ≤ C * 3 ^ (-↑k) * √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z (n + ↑k - 1)) h.grad c)

The arbitrary-gap oscillation decay for the weak gradient.

For an H^1 function on the cube z + cu_{n+k} which is weakly harmonic there, the normalized mean-square oscillation of its weak gradient on z + cu_n decays like 3^{-k} relative to the deviation of the same weak gradient on z + cu_{n+k-1}, for every gap k >= d + 3 and every constant c.

This is OscillationDecayWeak's estimate with the smooth interior representative eliminated: the extension by zero supplies the global local integrability that the interior Weyl lemma needs, and the gradient identification above replaces euclideanGradient v by grad h inside both mean-square functionals.