CruxLowerProcess

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

The process-side lower resolvent comparison

The excessive analytic remainder controls the restart term in the resolvent decomposition at the first exit from a bounded part domain. Consequently the resolvent of the process killed on that domain dominates the continuous zero extension of the part resolvent.

theorem DivergenceFormProcess.Form.onePointKernelResolvent_liveExtension_eq {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (lam : ℝ) {f : HCPolySupport.Vec d → ENNReal} (hf : Measurable f) (x : HCPolySupport.Vec d) : R.onePointKernelSemigroup.kernelResolvent lam (MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension f) ↑x = R.kernelSemigroup.kernelResolvent lam f x

Zero extension at infinity does not change the resolvent at a live starting point: the defect mass at infinity carries the vanishing value of the extension there.