PotentialResolventIdentitiesReg #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The pointwise resolvent identity of the potential resolvent #
The resolvent identity of the potential resolvent is an identity between L²
classes. Because each class has exactly one representative continuous on the
open domain, it becomes an identity at every point of the domain.
The statement is indexed by the interior regularity witness of the potential resolvent.
The pointwise resolvent identity #
theorem
DivergenceFormProcess.Form.potentialResolvent_resolvent_identity_apply
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
{lam Lam : ℝ}
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
{C : ℝ}
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
(mu nu : ↑MarkovProcess.Semigroup.PositiveShift)
(X : ↥(HCPolySupport.ScalarL2 U))
:
(potentialResolvent a ⋯ hlam hEll q hq) X = (potentialResolvent a ⋯ hlam hEll q hq) X + (↑nu - ↑mu) • (potentialResolvent a ⋯ hlam hEll q hq) ((potentialResolvent a ⋯ hlam hEll q hq) X)
The resolvent identity of the potential resolvent, applied to a datum.