ExitTimeChaining

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

Chaining bounds for exit times

A measurable choice from a countable family of open neighbourhoods gives a stopping time sigma on canonical path space: after every restart, sigma is the exit time of the newly selected neighbourhood. This file defines the accumulated time and discounted weight of N such exits. The strong Markov property turns a uniform one-step Laplace bound on a restart region W into its N-th power, which bounds exit from a possibly different set U when the chain covers that exit.

Public declarations:

• ContinuousPath.iteratedStoppingTime;
• ContinuousPath.iteratedStoppingTime_succ';
• ContinuousPath.discountedStoppingWeight;
• ContinuousPath.iteratedStoppingWeight;
• ContinuousPath.iteratedStoppingWeight_eq_discountedStoppingWeight;
• ContinuousPath.measurable_discountedStoppingWeight_stopped;
• ContinuousPath.measurable_discountedStoppingWeight;
• ContinuousPath.measurable_iteratedStoppingWeight;
• IsFellerKernelSemigroup.lintegral_iteratedStoppingWeight_le;
• IsConservative.lintegral_exp_neg_exitTime_le_rho_pow.

The construction does not prove a geometric covering property for any particular family of sets.

noncomputable def Algsuperdiff.Process.ContinuousPath.iteratedStoppingTime {alpha : Type u_1} [TopologicalSpace alpha] (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) : ℕ → MarkovProcess.ContinuousPath alpha → ENNReal

The accumulated time of n successive applications of a path-space stopping rule, restarting the rule after each finite stopping time.

Equations

• One or more equations did not get rendered due to their size.
• Algsuperdiff.Process.ContinuousPath.iteratedStoppingTime sigma 0 x✝ = 0

theorem Algsuperdiff.Process.ContinuousPath.iteratedStoppingTime_succ' {alpha : Type u_1} [TopologicalSpace alpha] (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (n : ℕ) (omega : MarkovProcess.ContinuousPath alpha) : iteratedStoppingTime sigma (n + 1) omega = iteratedStoppingTime sigma n omega + sigma (MarkovProcess.ContinuousPath.shift (WithTop.untopD 0 (iteratedStoppingTime sigma n omega)) omega)

Tail-recursive form of the accumulated stopping time: append the next rule after the first n cycles.

noncomputable def Algsuperdiff.Process.ContinuousPath.discountedStoppingWeight {alpha : Type u_1} [TopologicalSpace alpha] (lam : ℝ) (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (omega : MarkovProcess.ContinuousPath alpha) : ENNReal

The discounted finite-time weight of an extended-real time functional.

Equations

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

noncomputable def Algsuperdiff.Process.ContinuousPath.iteratedStoppingWeight {alpha : Type u_1} [TopologicalSpace alpha] (lam : ℝ) (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) : ℕ → MarkovProcess.ContinuousPath alpha → ENNReal

The product of the discounted finite-time weights along n successive restarts.

Equations

• One or more equations did not get rendered due to their size.
• Algsuperdiff.Process.ContinuousPath.iteratedStoppingWeight lam sigma 0 x✝ = 1

theorem Algsuperdiff.Process.ContinuousPath.iteratedStoppingWeight_eq_discountedStoppingWeight {alpha : Type u_1} [TopologicalSpace alpha] (lam : ℝ) (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (n : ℕ) (omega : MarkovProcess.ContinuousPath alpha) : iteratedStoppingWeight lam sigma n omega = discountedStoppingWeight lam (iteratedStoppingTime sigma n) omega

The recursively defined weight is the discount at the accumulated stopping time, with value zero when one of the successive stopping times is infinite.

theorem Algsuperdiff.Process.ContinuousPath.measurable_discountedStoppingWeight_stopped {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (hsigma : MeasureTheory.IsStoppingTime MarkovProcess.ContinuousPath.canonicalFiltration sigma) (lam : ℝ) : Measurable (discountedStoppingWeight lam sigma)

The discounted finite-time weight of a canonical-filtration stopping time is measurable for its stopped sigma-algebra.

theorem Algsuperdiff.Process.ContinuousPath.measurable_discountedStoppingWeight {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (hsigma : MeasureTheory.IsStoppingTime MarkovProcess.ContinuousPath.canonicalFiltration sigma) (lam : ℝ) : Measurable (discountedStoppingWeight lam sigma)

The discounted finite-time weight of a canonical-filtration stopping time is Borel measurable on path space.

theorem Algsuperdiff.Process.ContinuousPath.measurable_iteratedStoppingWeight {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (hsigma : MeasureTheory.IsStoppingTime MarkovProcess.ContinuousPath.canonicalFiltration sigma) (lam : ℝ) (n : ℕ) : Measurable (iteratedStoppingWeight lam sigma n)

The iterated discounted weight of a canonical-filtration stopping time is Borel measurable on path space.

theorem Algsuperdiff.Process.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.lintegral_iteratedStoppingWeight_le {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) (hK : P.KolmogorovRegular hP) (U : Set alpha) (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (hsigma : MeasureTheory.IsStoppingTime MarkovProcess.ContinuousPath.canonicalFiltration sigma) (lam : ℝ) (rho : ENNReal) (hrho : rho ≠ ⊤) (hsmall : ∀ y ∈ U, ∫⁻ (omega : MarkovProcess.ContinuousPath alpha), ContinuousPath.discountedStoppingWeight lam sigma omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) y ≤ rho) (hstay : ∀ (omega : MarkovProcess.ContinuousPath alpha), omega 0 ∈ U → sigma omega < ⊤ → omega (WithTop.untopD 0 (sigma omega)) ∈ U) (n : ℕ) (x : alpha) (hx : x ∈ U) : ∫⁻ (omega : MarkovProcess.ContinuousPath alpha), ContinuousPath.iteratedStoppingWeight lam sigma n omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x ≤ rho ^ n

A uniform one-step discounted stopping bound compounds geometrically under strong-Markov restarts, provided every finite restart from U remains in U.

theorem Algsuperdiff.Process.SubMarkovKernelSemigroup.IsConservative.lintegral_exp_neg_exitTime_le_rho_pow {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) (hK : P.KolmogorovRegular hP) (W U : Set alpha) (lam : ℝ) (hlam : 0 < lam) (sigma : MarkovProcess.ContinuousPath alpha → ENNReal) (hsigma : MeasureTheory.IsStoppingTime MarkovProcess.ContinuousPath.canonicalFiltration sigma) (rho : ENNReal) (hrho : rho ≠ ⊤) (hsmall : ∀ y ∈ W, ∫⁻ (omega : MarkovProcess.ContinuousPath alpha), ContinuousPath.discountedStoppingWeight lam sigma omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) y ≤ rho) (hstay : ∀ (omega : MarkovProcess.ContinuousPath alpha), omega 0 ∈ W → sigma omega < ⊤ → omega (WithTop.untopD 0 (sigma omega)) ∈ W) (N : ℕ) (x : alpha) (hx : x ∈ W) (hcover : ∀ᵐ (omega : MarkovProcess.ContinuousPath alpha) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x, MarkovProcess.ContinuousPath.exitTime U omega < ⊤ → ContinuousPath.iteratedStoppingTime sigma N omega ≤ MarkovProcess.ContinuousPath.exitTime U omega) : ∫⁻ (omega : MarkovProcess.ContinuousPath alpha), {omega : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U omega < ⊤}.indicator (fun (omega : MarkovProcess.ContinuousPath alpha) => ENNReal.ofReal (Real.exp (-lam * (MarkovProcess.ContinuousPath.exitTime U omega).toReal))) omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x ≤ rho ^ N

Exit-time chaining bound. Suppose sigma encodes a measurable selection of a small neighbourhood at the current state. If its discounted mass is at most rho throughout a restart region W, finite selected exits restart in W, and almost every path from x completes N selected exits no later than its exit from a possibly different set U, then the discounted finite-exit mass from U is at most rho ^ N.