BoundaryLaneMaxPrinciple

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

The weak maximum principle for the Laplacian on the truncated window

The boundary lane's residual corrector w (draft item 2(ii)) is controlled by

  ‖w‖_{L^∞(V)} ≤ ‖h - ℓ_h‖_{L^∞(∂V ∩ ∂□_m)} ,

which the draft justifies as "the maximum principle for the Laplacian". This module proves that step in the weak (H¹) formulation:

  v weakly harmonic on V,  (v - M)₊ ∈ H¹₀(V)   ⟹   v ≤ M  a.e. on V ,

together with its two-sided form. The proof is the standard energy argument: test the harmonicity against the truncation (v-M)₊, use the Stampacchia chain rule ∇(v-M)₊ = 1_{v>M} ∇v to see that the tested integral is the full Dirichlet energy of the truncation, conclude that the truncation has vanishing gradient, and close with the zero-trace Poincaré inequality.

Why this is the right rendering (and what it costs)

(v - M)₊ ∈ H¹(V) with the Stampacchia gradient is free: CoarseGraining proves it for every H¹ function and every level (exists_h1_max_sub_const, Homogenization/Sobolev/Truncation/Basic.lean). The whole content of the hypothesis HasBoundaryUpperBoundOn is therefore the zero trace of the truncation, which is exactly the weak reading of "v ≤ M on ∂V" — the standard hypothesis of the weak maximum principle, not a proof step in disguise. No pointwise trace operator is used anywhere in this repository, and none is introduced here.

What is not done here

The lane still owes: the construction of the corrector w with the draft's boundary data on ∂V ∩ ∂□_m and ∂V ∩ □_m, and (b) the verification of HasBoundaryUpperBoundOn for that w from the pointwise bound on h - ℓ_h (AffineSplitLift.abs_sub_affineLift_volumeAverage_le).

References

• ABK26, l.excess.decay.good.scales.
• CoarseGraining, Homogenization/Sobolev/Truncation/Basic.lean (exists_h1_max_sub_const) and Homogenization/Sobolev/Foundations/PoincareZeroTrace.lean (H10Function.exists_poincare_constant_of_isOpenBoundedConvexDomain).

1. The weak boundary bound

def Algsuperdiff.Section4.Provider.ExcessDecay.HasBoundaryUpperBoundOn {d : ℕ} (V : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function V) (M : ℝ) : Prop

u ≤ M on ∂V, weakly. The positive part (u - M)₊ lies in H¹₀(V), carrying CoarseGraining's Stampacchia gradient 1_{u>M} ∇u.

The H¹ membership and the gradient formula are unconditional (Homogenization.exists_h1_max_sub_const); the content of this predicate is the zero trace. (Given the first component, the second is forced almost everywhere by uniqueness of weak gradients on an open window; it is bundled so that no consumer has to rerun that argument, not to strengthen the hypothesis.)

Equations

• One or more equations did not get rendered due to their size.

2. The maximum principle

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_le_of_isWeaklyHarmonicOn {d : ℕ} [NeZero d] {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {u : HCPolySupport.H1Function V} {M : ℝ} (hu : Support.IsWeaklyHarmonicOn V u) (hM : HasBoundaryUpperBoundOn V u M) : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, u.toFun y ≤ M

The weak maximum principle for the Laplacian.

A weakly harmonic H¹ function on an open bounded convex window which is ≤ M on the boundary (in the zero-trace sense of HasBoundaryUpperBoundOn) is ≤ M almost everywhere in the window.

3. The two-sided form

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_neg {d : ℕ} {V : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function V} (hu : Support.IsWeaklyHarmonicOn V u) : Support.IsWeaklyHarmonicOn V (-u)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_abs_le_of_isWeaklyHarmonicOn {d : ℕ} [NeZero d] {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {u : HCPolySupport.H1Function V} {M : ℝ} (hu : Support.IsWeaklyHarmonicOn V u) (hupper : HasBoundaryUpperBoundOn V u M) (hlower : HasBoundaryUpperBoundOn V (-u) M) : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, |u.toFun y| ≤ M

The two-sided weak maximum principle. This is the display ‖w‖_{L^∞(V)} ≤ M of the draft's item 2(ii), with M the sup-bound of the boundary data.