HarmonicWeakAlgebra

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

Additive algebra of the distributional harmonicity predicate

HarmonicWeak proves that IsWeaklyHarmonicOn is stable under restriction to a subset, under multiplication by a constant, and that constants are weakly harmonic. It does not prove stability under subtraction, and that is the one closure property the nested-recentring route of OscillationTelescope cannot do without: the harmonic increment born at scale j is the difference h_j - h_{j+1} of two harmonic replacements built at consecutive scales, and its harmonicity on the finer cube is what feeds the arbitrary-gap decay.

Subtraction is not formal here. IsWeaklyHarmonicOn U u asserts that the Green pairing int_U u * (Delta psi) vanishes; splitting that pairing requires knowing that each half is separately integrable, which does not follow from the vanishing of the difference. The minimal hypothesis that supplies it is integrability of each summand on U alone: the multiplier Delta psi is continuous with compact support, hence bounded, so a merely integrable function stays integrable after multiplication by it. In the intended application u and v are H^1(U) functions on a bounded cube, for which L^2(U) subset L^1(U) gives the hypothesis for free.

Contents

• integrableOn_mul_euclideanCoordLaplacian -- the Green integrand of an integrable function against a smooth compactly supported test is integrable.
• IsWeaklyHarmonicOn.sub -- closure under subtraction, assuming integrability of the two summands on U.

Portability

This file depends only on Mathlib, on CoarseGraining (Homogenization.*) and on the harmonic 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.integrableOn_mul_euclideanCoordLaplacian {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u ψ : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u x * HCPolySupport.euclideanCoordLaplacian ψ x) U MeasureTheory.volume

The Green integrand of an integrable function is integrable.

The coordinate Laplacian of a smooth compactly supported test function is continuous with compact support, hence bounded; multiplying an integrable function by a bounded measurable one preserves integrability.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.IsWeaklyHarmonicOn.sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u v : HCPolySupport.Vec d → ℝ} (hu : IsWeaklyHarmonicOn U u) (hv : IsWeaklyHarmonicOn U v) (hui : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (hvi : MeasureTheory.IntegrableOn v U MeasureTheory.volume) : IsWeaklyHarmonicOn U fun (x : HCPolySupport.Vec d) => u x - v x

Weak harmonicity is stable under subtraction.

The closure property consumed by the nested-recentring telescope: the harmonic increment h_j - h_{j+1} of two harmonic replacements born at consecutive scales is weakly harmonic on the finer cube, where both are defined.