Continuous-Path Exit-Time Characterization

This characterizes the exit time of a continuous path.

Let $E$ be a normed additive commutative group, let $X:\Omega\to\mathbb R\to E$, and fix $\omega\in\Omega$. Assume that the path $s\mapsto X(\omega,s)$ is continuous. For every level $k\in\mathbb R$ and time $t\in\mathbb R$,

Thus the exit time is at most $t$ exactly when the path reaches norm at least $k$ at some point of the closed interval $[0,t]$.

This provides the basic deterministic criterion used to establish stopping-time and localization properties.

Original Lean declaration header

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

theorem exitTime_le_iff {X : Ω → ℝ → E} {ω : Ω} (hX : Continuous (X ω)) (k t : ℝ) :
    exitTime X k ω ≤ (t : WithTop ℝ) ↔ ∃ s ∈ Set.Icc (0 : ℝ) t, k ≤ ‖X ω s‖

Module navigation

Module: LevyStochCalc/Probability/ExitTime.

Next: abs_clamp_sub_le.

Source excerpt, lines 66–67 · Frozen source 408915f.