WeakSubsolution

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

Weak subsolutions and supersolutions

This module defines weak subsolutions and supersolutions for the shifted divergence-form equation on the zero-trace Sobolev carrier. It proves the weak comparison and maximum principles and the resolvent estimate for a nonnegative weak supersolution. All order conclusions are almost-everywhere statements.

def DivergenceFormProcess.Form.IsAlphaShiftedWeakSubsolution {d : ℕ} (a : HCPolySupport.CoeffField d) (U : Set (HCPolySupport.Vec d)) (α : ℝ) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : Prop

A weak subsolution of the alpha-shifted divergence-form equation.

Equations

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

def DivergenceFormProcess.Form.IsAlphaShiftedWeakSupersolution {d : ℕ} (a : HCPolySupport.CoeffField d) (U : Set (HCPolySupport.Vec d)) (α : ℝ) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : Prop

A weak supersolution of the alpha-shifted divergence-form equation.

Equations

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

theorem DivergenceFormProcess.Form.IsAlphaShiftedWeakSolution.isSubsolution {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {α : ℝ} {f : ↥(HCPolySupport.ScalarL2 U)} {u : ZeroTraceSobolev U} (hu : IsAlphaShiftedWeakSolution a U α f u) : IsAlphaShiftedWeakSubsolution a U α f u

Every weak solution is a weak subsolution.

theorem DivergenceFormProcess.Form.IsAlphaShiftedWeakSolution.isSupersolution {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {α : ℝ} {f : ↥(HCPolySupport.ScalarL2 U)} {u : ZeroTraceSobolev U} (hu : IsAlphaShiftedWeakSolution a U α f u) : IsAlphaShiftedWeakSupersolution a U α f u

Every weak solution is a weak supersolution.

theorem DivergenceFormProcess.Form.weakSubsolution_le_weakSupersolution_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam : ℝ} (hα : 0 < α) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {f g : ↥(HCPolySupport.ScalarL2 U)} {u v : ZeroTraceSobolev U} (hu : IsAlphaShiftedWeakSubsolution a U α f u) (hv : IsAlphaShiftedWeakSupersolution a U α g v) (hfg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑f x ≤ ↑↑g x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑(ZeroTraceSobolev.toL2 u) x ≤ ↑↑(ZeroTraceSobolev.toL2 v) x

A weak subsolution is almost everywhere below a weak supersolution when their right-hand sides have the same order.

theorem DivergenceFormProcess.Form.IsAlphaShiftedWeakSupersolution.nonneg_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {g : ↥(HCPolySupport.ScalarL2 U)} {v : ZeroTraceSobolev U} (hv : IsAlphaShiftedWeakSupersolution a U α g v) (hg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑g x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑(ZeroTraceSobolev.toL2 v) x

A weak supersolution with nonnegative right-hand side is nonnegative almost everywhere.

theorem DivergenceFormProcess.Form.resolvent_le_of_weakSupersolution_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {alpha beta lam Lam : ℝ} (hBeta : 0 < beta) (hAlphaBeta : alpha < beta) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (v : ZeroTraceSobolev U) (hv : IsAlphaShiftedWeakSupersolution a U alpha 0 v) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, beta * ↑↑((alphaShiftedResolvent a hBeta hlam hEll) (ZeroTraceSobolev.toL2 v)) x ≤ beta / (beta - alpha) * ↑↑(ZeroTraceSobolev.toL2 v) x

Resolvent estimate for a weak α-supersolution when 0 < β and α < β.