ExitMeanValueCube

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

The datum and the path resolvent of an exhaustion cube

The resolvent decomposition at the first exit from an exhaustion cube involves two resolvents of the whole-space process: the one killed on leaving the cube, and the whole-space one read at the exit position. This file supplies the analytic side of the first and settles the second for a nonnegative continuous datum vanishing at infinity.

• lintegral_pathResolvent_c0: the expected discounted occupation of the datum along the paths of the compactified process is the zero extension of the analytic resolvent supplied with the process. At the added point both sides vanish, because that point is absorbing and the observable vanishes there.

Both statements are on the one-point compactification, where the process lives.

The whole-space resolvent along the paths

theorem DivergenceFormProcess.Form.kernelResolvent_onePointLiveExtension_infty {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (lam : ℝ) {f : HCPolySupport.Vec d → ENNReal} (hf : Measurable f) : R.onePointKernelSemigroup.kernelResolvent lam (MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension f) OnePoint.infty = 0

The kernel resolvent of the compactified process vanishes at the added point on an observable that vanishes there: the point is absorbing.

theorem DivergenceFormProcess.Form.lintegral_pathResolvent_c0 {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (lam : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (y : HCPolySupport.Vec d), 0 ≤ g y) (z : OnePoint (HCPolySupport.Vec d)) : ∫⁻ (omega : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), MarkovProcess.ContinuousPath.pathResolvent (↑lam) (MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension fun (y : HCPolySupport.Vec d) => ENNReal.ofReal (g y)) omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) z = MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension (fun (y : HCPolySupport.Vec d) => ENNReal.ofReal (((R.operator lam) g) y)) z

The expected discounted occupation of a continuous datum. Along the paths of the compactified process the expected discounted occupation of the zero extension of a nonnegative continuous datum vanishing at infinity is the zero extension of the analytic resolvent supplied with the process.