Positivity

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

Positivity and normalized alpha-shifted resolvent bounds

This module records fixed-coefficient, bounded-domain maximum-principle estimates for the alpha-shifted divergence-form resolvent on its ScalarL2 carrier. They are the zero-potential case of the corresponding estimates for the resolvent with a bounded nonnegative potential. All conclusions are almost-everywhere statements with respect to volumeMeasureOn U: nonnegative forcing gives a nonnegative resolvent, forcing bounded above by one gives an upper bound of one after multiplication by the shift, and forcing in [0, 1] is preserved by that normalized resolvent. These are analytic L2 results only; this module does not construct a kernel, semigroup, or stochastic process.

theorem DivergenceFormProcess.Form.alphaShiftedResolvent_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) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑((alphaShiftedResolvent a hα hlam hEll) f) x

The α-shifted resolvent preserves nonnegativity almost everywhere. This is the counterpart of the weak maximum principle, which later recovers the same conclusion for weak supersolutions.