ScalarWeakMaximumPrinciple

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

The weak maximum principle for the divergence-form equation

Let Y solve -div (a grad Y) = 0 weakly on a bounded convex domain U and let q be an H¹ function of U with Y - q ∈ H¹₀(U); that is, Y and q have the same trace. Then Y is almost everywhere bounded by the pointwise bounds of q.

The proof is the standard energy test at the truncation (Y - M)₊. Three inputs are used:

• the truncation itself, exists_h1_max_sub_const, whose gradient is 1_{Y > M} grad Y;
• the matched-trace truncation memH10_max_sub_matched, which places (Y - M)₊ - (q - M)₊ in H¹₀(U); the second summand vanishes identically because q ≤ M everywhere, so the truncation is itself an admissible test function;
• the zero-trace Poincare inequality, which turns a vanishing gradient into a vanishing value.

Testing the equation against the truncation w gives ∫ (a grad Y) · grad w = 0, and grad w = 1_{Y > M} grad Y makes the integrand equal to (a grad w) · grad w pointwise, whose integral is at least lam ∫ |grad w|² by ellipticity. Hence grad w = 0 almost everywhere, hence w = 0 almost everywhere, which is Y ≤ M almost everywhere.

No shift, no symmetry of the coefficient field and no continuity of any representative is used.

Two structural facts

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.neg {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} (h : IsScalarForcedWeakSolution a U g u) : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => -g x) (-u)

The scalar-forced weak equation is odd. Negating the solution negates the forcing.

The one-sided maximum principle

theorem DivergenceFormProcess.Form.ae_le_of_isScalarForcedWeakSolution_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} [NeZero d] (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {Y : HCPolySupport.H1Function U} (hY : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 0) Y) {q : HCPolySupport.H1Function U} (hq : HCPolySupport.MemH10 U fun (x : HCPolySupport.Vec d) => Y.toFun x - q.toFun x) {M : ℝ} (hM : ∀ (x : HCPolySupport.Vec d), q.toFun x ≤ M) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, Y.toFun x ≤ M

The weak maximum principle, one-sided. A weakly a-harmonic function whose trace is that of a function bounded above by M is almost everywhere bounded above by M.

The two-sided maximum principle

theorem DivergenceFormProcess.Form.ae_abs_le_of_isScalarForcedWeakSolution_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} [NeZero d] (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {Y : HCPolySupport.H1Function U} (hY : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 0) Y) {q : HCPolySupport.H1Function U} (hq : HCPolySupport.MemH10 U fun (x : HCPolySupport.Vec d) => Y.toFun x - q.toFun x) {M : ℝ} (hM : ∀ (x : HCPolySupport.Vec d), |q.toFun x| ≤ M) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |Y.toFun x| ≤ M

The weak maximum principle. A weakly a-harmonic function whose trace is that of a function bounded by M in absolute value is almost everywhere bounded by M in absolute value.