PotentialLinftyBound

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

Uniform bounds for resolvents with potential

A bounded nonnegative potential can only improve the maximum-principle estimate. This module records the almost-everywhere absolute bound and its representative-invariant extended L∞ formulation.

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

If the forcing is almost everywhere bounded in absolute value, the normalized potential resolvent has the same bound.