HarmonicityTransferTests

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

Weak harmonicity against smooth tests

Support.IsWeaklyHarmonicOn W v is stated against every H¹₀(W) competitor, while every construction that produces harmonicity — in particular the odd reflection of §4.3 — produces it against smooth compactly supported tests. This file supplies the two bridges between the two formulations, both of which run through the H10Function package's own L² approximation data:

• isWeaklyHarmonicOn_of_contDiff_tests — smooth tests suffice (the direction a construction needs);
• integral_vecDot_euclideanGradient_eq_zero — a smooth function that happens to lie in H¹₀(W) may be used as a competitor with its classical gradient (the direction a consumer needs; the identification of the H10Function's recorded gradient with euclideanGradient is the a.e. uniqueness of weak derivatives on an open set, CoarseGraining's HasWeakPartialDerivOn.ae_eq).

Both are proved by testing coordinate by coordinate and passing to the limit through Hölder's inequality at the pair (2, 2), so the only analytic input is tendsto_setIntegral_mul_of_tendsto_eLpNormTwo, the L² continuity of the tested integral, which is proved here.

References

• CoarseGraining, Homogenization/Sobolev/WeakDerivatives.lean (HasWeakPartialDerivOn.ae_eq, HasWeakPartialDerivOn.of_contDiff), Homogenization/Sobolev/H1/Definitions.lean (the H10Function package).

1. L² continuity of the tested integral

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tendsto_setIntegral_mul_of_tendsto_eLpNormTwo {d : ℕ} {W : Set (HCPolySupport.Vec d)} {h : HCPolySupport.Vec d → ℝ} {f : ℕ → HCPolySupport.Vec d → ℝ} {g : HCPolySupport.Vec d → ℝ} (hh : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict W)) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 (MeasureTheory.volume.restrict W)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict W)) (htend : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => f n x - g x) 2 (MeasureTheory.volume.restrict W)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : HCPolySupport.Vec d) in W, f n x * h x) Filter.atTop (nhds (∫ (x : HCPolySupport.Vec d) in W, g x * h x))

L² continuity of the tested integral. If f n → g in L²(W) and h ∈ L²(W), the paired integrals converge. (This is the p = 2 specialization of the graph-closure engine of OddReflectionGlue, restated publicly here because the tested integral of a gradient pairing needs it once per coordinate.)

2. Coordinate splitting of the tested integral

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_two_fderiv_apply_restrict {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) (j : Fin d) : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => (fderiv ℝ f y) (HCPolySupport.basisVec j)) 2 (MeasureTheory.volume.restrict W)

A smooth compactly supported function's coordinate derivative is in L²(W) for every W.

3. Smooth tests suffice

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_of_contDiff_tests {d : ℕ} {W : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H1Function W) (h : ∀ (φ : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ W → ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (w.grad y) (HCPolySupport.euclideanGradient φ y) = 0) : Support.IsWeaklyHarmonicOn W w

Smooth tests suffice for weak harmonicity.

An H¹(W) function whose Dirichlet first variation vanishes against every smooth compactly supported test supported in W is weakly harmonic on W, i.e. the first variation vanishes against every H¹₀(W) competitor. The proof tests against the H10Function package's own smooth approximants and passes to the limit coordinatewise.

4. Smooth H¹₀ competitors carry their classical gradient

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integral_vecDot_euclideanGradient_eq_zero {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWopen : IsOpen W) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict W)] {v : HCPolySupport.H1Function W} (hv : Support.IsWeaklyHarmonicOn W v) {ψ : HCPolySupport.Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hmem : HCPolySupport.MemH10 W ψ) : ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (v.grad y) (HCPolySupport.euclideanGradient ψ y) = 0

A smooth H¹₀(W) competitor may be tested with its classical gradient.

If ψ is smooth and lies in H¹₀(W), then weak harmonicity of v on W gives the vanishing of the first variation against euclideanGradient ψ. The H10Function witness of MemH10 W ψ carries some weak gradient of ψ; on the open set W it agrees a.e. with the classical one by uniqueness of weak derivatives, and both are locally integrable there.