HarmonicReplaceBridge

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

From variational to distributional harmonicity

CoarseGraining carries harmonicity only in the variational form: a function whose weak gradient is L^2-orthogonal to the gradients of all H^1_0 competitors, i.e. the Euler-Lagrange identity int_U <grad h, grad psi> = 0. HarmonicWeak carries the distributional form int_U h (Delta psi) = 0 for smooth compactly supported psi. Nothing in either repository connects the two, and the harmonic layer downstream (mean value property, Weyl lemma, interior gradient decay) is stated exclusively for the distributional predicate.

This module supplies the missing bridge. The proof is one integration by parts in the weak sense: the defining identity of the weak partial derivative is applied with the test function d_i psi in the direction i, which converts int_U h (d_i d_i psi) into - int_U (grad h)_i (d_i psi); summing over i turns the Green pairing against Delta psi into minus the Dirichlet pairing against grad psi, which is the hypothesis. No regularity of h beyond H^1 is used, and no boundary term appears because the test function is compactly supported inside U.

The test-class mismatch that this bridge has to absorb is real: the variational identity quantifies over H10Function U, whereas the distributional predicate quantifies over smooth compactly supported functions. The two are reconciled by CoarseGraining's H10Function.ofContDiff, whose weak gradient is the pointwise Euclidean gradient by definitional unfolding.

Contents

• integrableOn_mul_of_memL2On_of_continuous_hasCompactSupport -- the pairing of an L^2 function on U with a continuous compactly supported function is integrable on U.
• isWeaklyHarmonicOn_of_forall_contDiff_integral_vecDot_grad_eq_zero -- the bridge, with the hypothesis quantified over smooth compactly supported test functions.
• isWeaklyHarmonicOn_of_forall_h10Function_integral_vecDot_grad_eq_zero -- the form actually produced by an H^1_0 solve, quantified over H10Function 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_of_memL2On_of_continuous_hasCompactSupport {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u g : HCPolySupport.Vec d → ℝ} (hu : HCPolySupport.MemL2On U u) (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u x * g x) U MeasureTheory.volume

An L^2(U) function paired with a continuous compactly supported function is integrable on U: the second factor lies in L^2(U) because its square is bounded and supported in a compact set.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.isWeaklyHarmonicOn_of_forall_contDiff_integral_vecDot_grad_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (h : HCPolySupport.H1Function U) (hzero : ∀ (ψ : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ U → ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (h.grad x) (HCPolySupport.euclideanGradient ψ x) = 0) : IsWeaklyHarmonicOn U h.toFun

The variational-to-distributional bridge.

If the weak gradient of an H^1(U) function is L^2-orthogonal on U to the Euclidean gradient of every smooth compactly supported test function supported in U, then the function is weakly harmonic on U in the distributional sense of HarmonicWeak.

The proof applies the defining identity of the i-th weak partial derivative to the test function d_i psi, sums over i, and reads off the hypothesis.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.isWeaklyHarmonicOn_of_forall_h10Function_integral_vecDot_grad_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (h : HCPolySupport.H1Function U) (hzero : ∀ (φ : HCPolySupport.H10Function U), ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (h.grad x) (φ.grad x) = 0) : IsWeaklyHarmonicOn U h.toFun

The bridge in the form produced by an H^1_0 solve.

The Euler-Lagrange identity of a Dirichlet problem is stated against H10Function U competitors. Restricting it to the competitors H10Function.ofContDiff built from smooth compactly supported test functions -- whose weak gradient is the pointwise Euclidean gradient -- gives the hypothesis of the previous theorem.