LinftyResolventBound

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

Uniform bounds for the alpha-shifted resolvent

This module records fixed-coefficient analytic L∞ bounds for the normalized alpha-shifted divergence-form resolvent as the zero-potential case of the corresponding bounds with a bounded nonnegative potential. It transports an almost-everywhere absolute bound on scalar L² forcing and records the resulting contraction of the representative-invariant extended L∞ seminorm. No kernel, semigroup, or stochastic-process claim is made here.

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

If the forcing is almost everywhere bounded in absolute value by a nonnegative constant, then the normalized alpha-shifted resolvent has the same almost-everywhere absolute bound.