ExitMeanValueLimit

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

The vanishing-shift limit of the discounted exit average

Let Q be the continuous-path process of a conservative Feller kernel semigroup, let U be an open set with exit time tau, and let psi be a bounded measurable function. The discounted exit average at the shift lam is E_y[1_{tau < infinity} e^{-lam tau} psi(X_tau)] (discountedExitAverage),

the quantity produced by the resolvent decomposition at the first exit from U. This file proves the two facts that turn such a family of identities into the exit mean-value property of StoppedDirichletHarmonic.lean.

• As the shift decreases to zero the discount disappears (tendsto_discountedExitAverage_nhdsGT_zero): the integrands converge pointwise and are bounded by a constant, so dominated convergence applies along nhdsWithin 0 (Ioi 0).
• Consequently, if for every small positive shift the discounted exit average is the difference of psi and some value at the starting point, and those values converge as the shift decreases to zero, then the limit function is represented by the exit distribution (hasExitMeanValueOn_of_tendsto_discountedExitAverage). Only two facts about the process enter: the exit position lies outside U, and the exit time is almost surely finite, which is where the finiteness of the expected exit time is consumed.

A third, unrelated, stability fact is recorded: the exit mean-value property passes to uniform limits (hasExitMeanValueOn_of_forall_approx), because the exit distribution is a subprobability law. This is what a density argument in the boundary data consumes.

Nothing here refers to a generator, and nothing here is specific to the divergence-form setting.

def DivergenceFormProcess.StoppedDirichlet.exitEvent {alpha : Type u_1} [MetricSpace alpha] (U : Set alpha) : Set (MarkovProcess.ContinuousPath alpha)

The event that the path leaves U.

Equations

• DivergenceFormProcess.StoppedDirichlet.exitEvent U = {omega : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U omega < ⊤}

theorem DivergenceFormProcess.StoppedDirichlet.measurableSet_exitEvent {alpha : Type u_1} [MetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {U : Set alpha} (hU : IsOpen U) : MeasurableSet (exitEvent U)

noncomputable def DivergenceFormProcess.StoppedDirichlet.exitDiscount {alpha : Type u_1} [MetricSpace alpha] (U : Set alpha) (lam : ℝ) (omega : MarkovProcess.ContinuousPath alpha) : ℝ

The exponential discount at the exit time.

Equations

• DivergenceFormProcess.StoppedDirichlet.exitDiscount U lam omega = Real.exp (-lam * (MarkovProcess.ContinuousPath.exitTime U omega).toReal)

theorem DivergenceFormProcess.StoppedDirichlet.measurable_exitDiscount {alpha : Type u_1} [MetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {U : Set alpha} (hU : IsOpen U) (lam : ℝ) : Measurable (exitDiscount U lam)

noncomputable def DivergenceFormProcess.StoppedDirichlet.discountedExitIntegrand {alpha : Type u_1} [MetricSpace alpha] (U : Set alpha) (lam : ℝ) (psi : alpha → ℝ) (omega : MarkovProcess.ContinuousPath alpha) : ℝ

The integrand of the discounted exit average: the discounted value of psi 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.measurable_discountedExitIntegrand {alpha : Type u_1} [MetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {U : Set alpha} (hU : IsOpen U) (lam : ℝ) {psi : alpha → ℝ} (hpsi : Measurable psi) : Measurable (discountedExitIntegrand U lam psi)

theorem DivergenceFormProcess.StoppedDirichlet.exitDiscount_nonneg {alpha : Type u_1} [MetricSpace alpha] (U : Set alpha) (lam : ℝ) (omega : MarkovProcess.ContinuousPath alpha) : 0 ≤ exitDiscount U lam omega

theorem DivergenceFormProcess.StoppedDirichlet.exitDiscount_le_one {alpha : Type u_1} [MetricSpace alpha] {U : Set alpha} {lam : ℝ} (hlam : 0 ≤ lam) (omega : MarkovProcess.ContinuousPath alpha) : exitDiscount U lam omega ≤ 1

theorem DivergenceFormProcess.StoppedDirichlet.norm_discountedExitIntegrand_le {alpha : Type u_1} [MetricSpace alpha] {U : Set alpha} {lam : ℝ} (hlam : 0 ≤ lam) {psi : alpha → ℝ} {M : ℝ} (hM : ∀ (y : alpha), ‖psi y‖ ≤ M) (omega : MarkovProcess.ContinuousPath alpha) : ‖discountedExitIntegrand U lam psi omega‖ ≤ M

noncomputable def DivergenceFormProcess.StoppedDirichlet.discountedExitAverage {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 : ℝ) (psi : alpha → ℝ) (y : alpha) : ℝ

The discounted exit average. The expectation of the discounted value of psi 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.tendsto_discountedExitAverage_nhdsGT_zero {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) {psi : alpha → ℝ} (hpsi : Measurable psi) {M : ℝ} (hM : ∀ (y : alpha), ‖psi y‖ ≤ M) (y : alpha) : Filter.Tendsto (fun (lam : ℝ) => discountedExitAverage P hP U lam psi y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (omega : MarkovProcess.ContinuousPath alpha), (exitEvent U).indicator (fun (omega : MarkovProcess.ContinuousPath alpha) => psi (exitPosition U omega)) omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) y))

The discount disappears as the shift decreases to zero. The discounted exit averages converge to the undiscounted average over the paths that leave U.

theorem DivergenceFormProcess.StoppedDirichlet.ae_exitPosition_notMem {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {y : alpha} (hy : y ∈ U) (hwfin : expectedExitTime P hP U y ≠ ⊤) : ∀ᵐ (omega : MarkovProcess.ContinuousPath alpha) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) y, omega ∈ exitEvent U ∧ exitPosition U omega ∉ U

From a starting point of U with a finite expected exit time, the path leaves U almost surely and its exit position lies outside U.

theorem DivergenceFormProcess.StoppedDirichlet.hasExitMeanValueOn_of_tendsto_discountedExitAverage {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {psi : alpha → ℝ} (hpsi : Measurable psi) {M : ℝ} (hM : ∀ (y : alpha), ‖psi y‖ ≤ M) (hwfin : ∀ y ∈ U, expectedExitTime P hP U y ≠ ⊤) {mu : ℝ} (hmu : 0 < mu) (val : ℝ → alpha → ℝ) {h : alpha → ℝ} (hdec : ∀ lam ∈ Set.Ioo 0 mu, ∀ y ∈ U, discountedExitAverage P hP U lam psi y = val lam y) (hoff : ∀ y ∉ U, h y = psi y) (hlim : ∀ y ∈ U, Filter.Tendsto (fun (lam : ℝ) => val lam y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (h y))) : HasExitMeanValueOn P hP U h

The exit mean-value property from a vanishing-shift limit. Suppose that for every small positive shift the discounted exit average of psi is the value of psi at the starting point less a correction, and that the corrected values converge to h as the shift decreases to zero. Then h, which agrees with psi off U, is represented by the exit distribution of U.

theorem DivergenceFormProcess.StoppedDirichlet.hasExitMeanValueOn_of_forall_approx {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) {h : alpha → ℝ} (hh : Measurable h) {M : ℝ} (hM : ∀ (y : alpha), ‖h y‖ ≤ M) (happrox : ∀ eps > 0, ∃ (g : alpha → ℝ), Measurable g ∧ (∃ (C : ℝ), ∀ (y : alpha), ‖g y‖ ≤ C) ∧ HasExitMeanValueOn P hP U g ∧ ∀ (y : alpha), ‖g y - h y‖ ≤ eps) : HasExitMeanValueOn P hP U h

The exit mean-value property passes to uniform limits. A uniform limit of bounded measurable functions represented by the exit distribution is itself represented by it.