Eventual Exit-Time Localization

This is the localization property for continuous paths.

Let $E$ be a normed additive commutative group, let $X:\Omega\to\mathbb R\to E$, and assume that $s\mapsto X(\omega,s)$ is continuous. For every $t\ge0$, there exists a natural number $K$ such that every integer $k\ge K$ satisfies

Equivalently, any fixed nonnegative time lies strictly before all sufficiently high exit levels. The result supplies a localizing sequence for continuous paths.

Original Lean declaration header

Within namespace LevyStochCalc.Probability. Shown in its original module context. Proof omitted.

theorem exists_lt_exitTime {X : Ω → ℝ → E} {ω : Ω} (hX : Continuous (X ω)) {t : ℝ} (ht : 0 ≤ t) :
    ∃ K : ℕ, ∀ k : ℕ, K ≤ k → (t : WithTop ℝ) < exitTime X (k : ℝ) ω

Module navigation

Module: LevyStochCalc/Probability/ExitTime.

Supporting theorems: exitTime_le_iff.

Previous: norm_le_of_le_exitTime.

Source excerpt, lines 217–218 · Frozen source 408915f.