PotentialOrder

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

Order properties of resolvents with potential

This module proves positivity, fixed-potential comparison, normalized upper bounds, and antitonicity with respect to the nonnegative potential.

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

A weak subsolution of the shifted equation with potential.

Equations

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

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

A weak supersolution of the shifted equation with potential.

Equations

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

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

A potential weak solution is a potential weak subsolution.

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

A potential weak solution is a potential weak supersolution.

theorem DivergenceFormProcess.Form.potentialWeakSubsolution_le_weakSupersolution_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam C : ℝ} (hα : 0 < α) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) {f g : ↥(HCPolySupport.ScalarL2 U)} {u v : ZeroTraceSobolev U} (hu : IsPotentialWeakSubsolution a α q U u f) (hv : IsPotentialWeakSupersolution a α q U v g) (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

Potential weak subsolutions lie below potential weak supersolutions when their forcing terms have the same order.

theorem DivergenceFormProcess.Form.potentialResolvent_nonneg_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑((potentialResolvent a hα hlam hEll q hq) f) x

A nonnegative forcing has a nonnegative potential resolvent almost everywhere.

theorem DivergenceFormProcess.Form.potentialResolvent_mono_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f g : ↥(HCPolySupport.ScalarL2 U)) (hfg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑f x ≤ ↑↑g x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑((potentialResolvent a hα hlam hEll q hq) f) x ≤ ↑↑((potentialResolvent a hα hlam hEll q hq) g) x

The potential resolvent preserves almost-everywhere order for fixed coefficients, shift, and potential.

theorem DivergenceFormProcess.Form.alpha_mul_potentialResolvent_le_one_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑f x ≤ 1) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, α * ↑↑((potentialResolvent a hα hlam hEll q hq) f) x ≤ 1

Multiplication by the shift bounds the potential resolvent by one when the forcing is almost everywhere at most one.

theorem DivergenceFormProcess.Form.potentialResolvent_antitone_potential_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam C₁ C₂ : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q₁ q₂ : HCPolySupport.Vec d → ℝ) (hq₁ : IsBoundedNonnegativePotential U q₁ C₁) (hq₂ : IsBoundedNonnegativePotential U q₂ C₂) (hqle : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, q₁ x ≤ q₂ x) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑((potentialResolvent a hα hlam hEll q₂ hq₂) f) x ≤ ↑↑((potentialResolvent a hα hlam hEll q₁ hq₁) f) x

Increasing a bounded nonnegative potential decreases its resolvent on nonnegative forcing.