ExitMeanValueDecomposition

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

The resolvent decomposition at an exit time, read as a discounted exit average

The library splits the discounted occupation of a nonnegative observable at the first exit from an open set U into the occupation before exit -- the killed resolvent -- and the occupation after exit, restarted from the exit location. This file records the second term in the shape the vanishing-shift argument of ExitMeanValueLimit.lean consumes.

• lintegralDiscountedExit is the extended-real discounted exit average, and toReal_lintegralDiscountedExit identifies it with the real discounted exit average of ExitMeanValueLimit.lean for a bounded nonnegative observable.
• eq_killedResolvent_add_lintegralDiscountedExit restates the library decomposition: if the expected discounted occupation of the observable is the function phi at every starting point, then phi x = R^U_lam f (x) + E_x[1_{tau < infinity} e^{-lam tau} phi(X_tau)]. The hypothesis names the whole-space resolvent of the observable; it is discharged by the identification of the process resolvent with the analytic one, which the caller supplies.

noncomputable def DivergenceFormProcess.StoppedDirichlet.lintegralDiscountedExit {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (lam : ℝ) (phi : alpha → ENNReal) (z : alpha) : ENNReal

The extended-real discounted exit average. The expectation of the discounted value of a nonnegative extended observable at the exit position, on the event that the path leaves U.

Equations

• One or more equations did not get rendered due to their size.

theorem DivergenceFormProcess.StoppedDirichlet.toReal_lintegralDiscountedExit {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} (hU : IsOpen U) (lam : ℝ) {psi : alpha → ℝ} (hpsi : Measurable psi) (hpsi0 : ∀ (y : alpha), 0 ≤ psi y) (z : alpha) : (lintegralDiscountedExit P hP U lam (fun (y : alpha) => ENNReal.ofReal (psi y)) z).toReal = discountedExitAverage P hP U lam psi z

The extended-real and the real discounted exit averages agree on a bounded nonnegative observable.

theorem DivergenceFormProcess.StoppedDirichlet.lintegralDiscountedExit_ne_top {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} {lam : ℝ} (hlam : 0 ≤ lam) {phi : alpha → ENNReal} {C : ENNReal} (hC : C ≠ ⊤) (hphi : ∀ (y : alpha), phi y ≤ C) (z : alpha) : lintegralDiscountedExit P hP U lam phi z ≠ ⊤

The discounted exit average of a bounded observable is finite.

theorem DivergenceFormProcess.StoppedDirichlet.discountedExitAverage_add_const_mul {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} (hU : IsOpen U) (lam : ℝ) (hlam : 0 ≤ lam) {psi1 psi2 : alpha → ℝ} (h1 : Measurable psi1) (h2 : Measurable psi2) {M1 M2 : ℝ} (hM1 : ∀ (y : alpha), ‖psi1 y‖ ≤ M1) (hM2 : ∀ (y : alpha), ‖psi2 y‖ ≤ M2) (c : ℝ) (z : alpha) : discountedExitAverage P hP U lam (fun (y : alpha) => psi1 y + c * psi2 y) z = discountedExitAverage P hP U lam psi1 z + c * discountedExitAverage P hP U lam psi2 z

The real discounted exit average is linear. It is a Bochner integral in the observable.

theorem DivergenceFormProcess.StoppedDirichlet.eq_killedResolvent_add_lintegralDiscountedExit {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) {phi : alpha → ENNReal} (hres : ∀ (z : alpha), ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), MarkovProcess.ContinuousPath.pathResolvent lam f eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) z = phi z) (x : alpha) : phi x = MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent P hP U hU lam f x + lintegralDiscountedExit P hP U lam phi x

The resolvent decomposition at the exit time, in discounted-exit form. If the expected discounted occupation of the observable f is phi at every starting point, then the value of phi splits into the killed resolvent of f on U and the discounted exit average of phi.