Comparison

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

Same-coefficient resolvent comparison

This file records the fixed-coefficient almost-everywhere comparison principle for the shifted resolvent as the zero-potential case of the comparison principle for the resolvent with a bounded nonnegative potential.

The domain, coefficient field, and operator parameters are fixed. This is an almost-everywhere analytic result on ScalarL2 only; it does not compare different coefficient fields or parameters, and it does not construct a sub-Markov family, semigroup, kernel, or process.

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

The alpha-shifted resolvent preserves almost-everywhere order when the coefficient field and all operator parameters are fixed. This is also implied by the later weak comparison principle.