AffineSplitHarmonic #

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

The affine split `v = v₀ + w + ℓ_h` and the harmonicity of its pieces #

The replacement draft's item 2 (l.comparison.reduction) defines w as the harmonic function carrying the boundary residual and then sets v₀ := v - w - ℓ_h, asserting that v₀ is harmonic "since ℓ_h is affine, hence harmonic". In the weak (H¹) formulation of this repository that sentence has real content:

  IsWeaklyHarmonicOn V ℓ   ↔   ∀ φ ∈ H¹₀(V),  ∑_i A_i ∫_V ∂_i φ = 0 ,

and ∫_V ∂_i φ = 0 for φ ∈ H¹₀(V) is a genuine lemma: it is the weak divergence theorem for zero-trace functions. This module proves it (from the weak-gradient identity of the constant H¹ function, applied to the approximating sequence bundled in H10Function, plus the L²→L¹ passage on the finite-measure window), derives the harmonicity of affine functions, and proves the split.

Main results #

integral_grad_coord_h10_eq_zero — ∫_V (∇φ)_i = 0 for φ ∈ H¹₀(V).
isWeaklyHarmonicOn_of_grad_const — a constant gradient is weakly harmonic; in particular isWeaklyHarmonicOn_affineLiftH1 for ℓ_h.
isWeaklyHarmonicOn_sub — harmonicity is stable under differences.
exists_affineSplit — the draft's v = v₀ + w + ℓ_h with v₀ harmonic.

What is not done here #

The existence of the residual corrector w (the harmonic function with data h - ℓ_h on ∂V ∩ ∂□_m and 0 on ∂V ∩ □_m) is not constructed: w enters exists_affineSplit as a given weakly harmonic H¹ function, exactly as in the draft's proof, which defines w by solving that Dirichlet problem. Solvability on the truncated window V = (x+□_{n-2}) ∩ □_m is a separate, priced obligation.
The boundary conditions (i) and (ii) of the draft's lemma are not rendered here; only the algebraic/harmonicity half of the split is. The L^∞ bound on w is BoundaryLaneMaxPrinciple.

References #

ABK26, l.excess.decay.good.scales.
CoarseGraining, Homogenization/Sobolev/H1/Definitions.lean (the H10Function approximation package), Homogenization/Sobolev/Foundations/MeanZero.lean (H1Function.const, H1Function.affineOnIsSobolevRegularDomain).

1. The weak divergence theorem for `H¹₀` #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integral_grad_coord_h10_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] (φ : HCPolySupport.H10Function U) (i : Fin d) :

∫ (y : HCPolySupport.Vec d) in U, φ.grad y i = 0

The weak divergence theorem for H¹₀. Each coordinate of the weak gradient of a zero-trace function integrates to zero over the domain.

The proof tests the weak-gradient identity of the constant H¹ function against the smooth compactly supported approximants of φ, and passes to the limit through the L² convergence of the approximate gradients (the H10Function package's tendsto_approx_grad) on the finite-measure window.

2. Affine functions are weakly harmonic #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_of_grad_const {d : ℕ} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] {u : HCPolySupport.H1Function V} {A : HCPolySupport.Vec d} (hgrad : ∀ (y : HCPolySupport.Vec d), u.grad y = A) :

Support.IsWeaklyHarmonicOn V u

An H¹ function with constant weak gradient is weakly harmonic: the tested integral is a finite combination of the vanishing gradient integrals of the test function.

source