Exit Time Detected on Rational Grid Points

This characterizes a continuous-path exit event using the grid points gridPt.

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. Fix $k\in\mathbb R$ and $t\ge0$. Then

The comparison with the exit time is therefore determined by values of the path at grid points in $[0,t]$, with arbitrarily small loss in the threshold. This form is useful for measurability and stopping-time arguments.

Original Lean declaration header

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

theorem exitTime_le_iff_forall {X : Ω → ℝ → E} {ω : Ω} (hX : Continuous (X ω)) (k : ℝ) {t : ℝ}
    (ht : 0 ≤ t) :
    exitTime X k ω ≤ (t : WithTop ℝ) ↔
      ∀ n : ℕ, ∃ m : ℕ, k - ((n : ℝ) + 1)⁻¹ < ‖X ω (gridPt t m)‖

Module navigation

Module: LevyStochCalc/Probability/ExitTime.

Supporting theorems: abs_clamp_sub_le, exitTime_le_iff.

Previous: abs_clamp_sub_le · Next: norm_le_of_le_exitTime.

Source excerpt, lines 112–115 · Frozen source 408915f.