MaximumPrinciple

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

Weak maximum principle with a nonnegative potential

For the equation -div (a grad u) + (alpha + q) u = 0 with alpha > 0 and q >= 0, a solution whose positive part above a nonnegative level has zero trace is bounded by that level. The proof tests the equation with the truncation itself: the elliptic term is nonnegative on the superlevel set and the mass term is bounded below by the square of the truncation.

Main results

• DivergenceFormProcess.Decay.ae_le_of_positivePart_zeroTrace

noncomputable def DivergenceFormProcess.Decay.positivePartTest {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function U} {M : ℝ} (htrace : HCPolySupport.MemH10 U fun (x : HCPolySupport.Vec d) => max (u.toFun x - M) 0) : HCPolySupport.H10Function U

The zero-trace witness of a positive-part truncation, as a test function.

Equations

• DivergenceFormProcess.Decay.positivePartTest htrace = Classical.choose htrace

theorem DivergenceFormProcess.Decay.positivePartTest_toFun {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function U} {M : ℝ} (htrace : HCPolySupport.MemH10 U fun (x : HCPolySupport.Vec d) => max (u.toFun x - M) 0) : (positivePartTest htrace).toFun = fun (x : HCPolySupport.Vec d) => max (u.toFun x - M) 0

The truncation test has the expected value.

theorem DivergenceFormProcess.Decay.positivePartTest_grad_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {u : HCPolySupport.H1Function U} {M : ℝ} (htrace : HCPolySupport.MemH10 U fun (x : HCPolySupport.Vec d) => max (u.toFun x - M) 0) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, (positivePartTest htrace).grad x = {y : HCPolySupport.Vec d | M < u.toFun y}.indicator u.grad x

The truncation test has the expected weak gradient.

theorem DivergenceFormProcess.Decay.ae_le_of_positivePart_zeroTrace {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {a : HCPolySupport.CoeffField d} {lam Lam alpha M : ℝ} {q : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} (halpha : 0 < alpha) (hM : 0 ≤ M) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (hq : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ q x) (hsol : Form.IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => -((alpha + q x) * u.toFun x)) u) (htrace : HCPolySupport.MemH10 U fun (x : HCPolySupport.Vec d) => max (u.toFun x - M) 0) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, u.toFun x ≤ M

Weak maximum principle: a solution of -div (a grad u) + (alpha + q) u = 0 whose positive part above a nonnegative level has zero trace lies below that level almost everywhere.