ExitTimeHomogenizationJointMoment

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

The normalized exponential moment of an exit time

A uniform bound E_x[τ(U)] ≤ T for the expected exit time, valid from every starting point, normalizes a positive exponential moment of the exit time to 2: at the multiplier K = 38 the survival probability at the horizon K T is at most K⁻¹, and the rate λ is admissible as soon as exp (38 λ T) ≤ 19/10, that is λ ≤ log(19/10)/(38 T).

The uniform bound is only available at the starting points of U, whereas the normalization asks for it at every starting point. The two agree: a process started outside U leaves it at once, so the expected exit time vanishes there.

Main results

• expectedExitTime_le_of_le_on — the uniform bound extended from the starting points of U to every starting point.
• lintegral_exponentialStoppingWeight_exitTime_le_two_of_le_on — the normalized exponential moment from a bound valid on the open set only.

References

• ABK26, the exit-time comparison of Section 5.2.

1. The normalized exponential moment

theorem Algsuperdiff.Section5.Provider.expectedExitTime_le_of_le_on {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hKreg : P.KolmogorovRegular hP) {U : Set alpha} {c : ENNReal} (hbound : ∀ z ∈ U, DivergenceFormProcess.StoppedDirichlet.expectedExitTime P hP U z ≤ c) (z : alpha) : DivergenceFormProcess.StoppedDirichlet.expectedExitTime P hP U z ≤ c

A bound on the open set bounds the expected exit time everywhere. A process started outside the open set leaves it at once.

theorem Algsuperdiff.Section5.Provider.lintegral_exponentialStoppingWeight_exitTime_le_two_of_le_on {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hKreg : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {T : ℝ} (hT : 0 ≤ T) (hbound : ∀ z ∈ U, DivergenceFormProcess.StoppedDirichlet.expectedExitTime P hP U z ≤ ENNReal.ofReal T) {lam : ℝ} (hlam : 0 ≤ lam) (hrate : lam * (38 * T) ≤ Real.log (19 / 10)) (x : alpha) : ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), MarkovProcess.ContinuousPath.exponentialStoppingWeight lam (MarkovProcess.ContinuousPath.exitTime U) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x ≤ 2

The normalized exponential moment of the exit time. If the expected exit time from the open set U is at most T from every point of U, then every rate λ ≥ 0 with 38 λ T ≤ log(19/10) has exponential moment at most 2, from every starting point.