Resolvent decomposition at an exit time

This file splits the whole-space path resolvent at the first exit time from an open set. The occupation before exit is the killed resolvent; on finite exit, the remaining occupation is the discounted whole-space resolvent restarted from the exit location. The restart step uses the strong Markov property on {exitTime U < ⊤} and is valid for arbitrary nonnegative extended measurable observables.

Main definitions and results: ContinuousPath.pathResolvent, ContinuousPath.measurable_pathResolvent, IsConservative.lintegral_pathResolvent_eq_killedResolvent_univ, and IsFellerKernelSemigroup.lintegral_pathResolvent_eq_killedResolvent_add.

No integrability or almost-sure finiteness of the exit time is asserted.

noncomputable def MarkovProcess.ContinuousPath.pathResolvent {alpha : Type u_1} [MetricSpace alpha] (lam : ℝ) (f : alpha → ENNReal) (omega : ContinuousPath alpha) : ENNReal

The discounted occupation of a nonnegative extended observable along one continuous path.

Equations

• MarkovProcess.ContinuousPath.pathResolvent lam f omega = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-lam * t)) * f (omega t.toNNReal)

theorem MarkovProcess.ContinuousPath.measurable_pathResolvent {alpha : Type u_1} [MetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) : Measurable (pathResolvent lam f)

The path resolvent is measurable when its observable is measurable.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.lintegral_pathResolvent_eq_killedResolvent_univ {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) (x : alpha) : ∫⁻ (omega : ContinuousPath alpha), ContinuousPath.pathResolvent lam f omega ∂(continuousProcess P hP) x = killedResolvent P hP Set.univ ⋯ lam f x

Expected discounted path occupation is the killed resolvent for the whole state space.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.lintegral_pathResolvent_eq_killedResolvent_add {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (U : Set alpha) (hU : IsOpen U) (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) (x : alpha) : ∫⁻ (omega : ContinuousPath alpha), ContinuousPath.pathResolvent lam f omega ∂(IsConservative.continuousProcess P hP) x = IsConservative.killedResolvent P hP U hU lam f x + ∫⁻ (omega : ContinuousPath alpha), {omega : ContinuousPath alpha | ContinuousPath.exitTime U omega < ⊤}.indicator (fun (omega : ContinuousPath alpha) => ENNReal.ofReal (Real.exp (-lam * (ContinuousPath.exitTime U omega).toReal)) * ∫⁻ (eta : ContinuousPath alpha), ContinuousPath.pathResolvent lam f eta ∂(IsConservative.continuousProcess P hP) (omega (WithTop.untopD 0 (ContinuousPath.exitTime U omega)))) omega ∂(IsConservative.continuousProcess P hP) x

Strong-Markov resolvent decomposition at an exit time. The expected discounted path occupation is the killed resolvent plus, on finite exit, the discounted occupation restarted from the exit location. At discount lam = 0 this is the corresponding Green-function decomposition.