Eventual Strict Grid-Stop Bound

This statement gives an eventual strict upper bound for the grid stopping time gridStop.

Let Ω be a type and let τ : Ω → WithTop ℝ. Fix a time t : ℝ with 0 < t and an outcome ω : Ω. Let s : ℝ satisfy 0 < s, s ≤ t, and suppose that the stopping-time value τ ω is strictly less than s regarded as an element of WithTop ℝ. Then, for all sufficiently large natural mesh parameters n, the grid stopping time at t is strictly less than s:

Here “eventually” refers to the filter at the top of ℕ, and the real number s on the right-hand side is coerced into WithTop ℝ. This technical estimate is useful for controlling grid stopping times in limiting arguments for stopped Itô integrals.

Formalization Note: The conclusion is an eventual statement in n, not a claim that the inequality holds for every n. The hypotheses require both t and s to be strictly positive, with s ≤ t, and use the strict inequality τ ω < ↑s in WithTop ℝ.

Original Lean declaration header

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

theorem eventually_gridStop_lt {t : ℝ} (ht : 0 < t) (ω : Ω) {s : ℝ} (hs : 0 < s) (hst : s ≤ t)
    (hτs : τ ω < ((s : ℝ) : WithTop ℝ)) :
    ∀ᶠ n in Filter.atTop, gridStop τ t n ω < ((s : ℝ) : WithTop ℝ)

Module navigation

Module: LevyStochCalc/Brownian/ItoLocality.

Supporting theorems: gridStopAux_le_iff.

Previous: gridStopAux_le_iff · Next: stochasticIntegralBrownian_stopped_eq_of_le.

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