Grid Stopping Auxiliary Characterization

This is a technical equivalence characterizing the auxiliary grid stopping time gridStopAux.

Let Ω be a type, let τ : Ω → WithTop ℝ be an extended-real-valued stopping-time candidate, let t and a be real and extended-real parameters respectively, let n and k be natural numbers, and let ω : Ω. Then the following are equivalent: gridStopAux τ t n k ω is at most a, and there exists a natural number j such that j ≤ k and the two-valued stopping time stepStop τ (gridPt t n j) ω is at most a.

This auxiliary result rewrites an inequality involving the grid stopping time as a finite existential condition over grid indices, making it reusable in arguments about grid approximations and their order properties.

Formalization Note: The stopping-time values and the parameter a lie in WithTop ℝ, the extended real line, and all inequalities use its order. The statement has no measurability or probability-measure assumptions.

Original Lean declaration header

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

omit [MeasurableSpace Ω] [IsProbabilityMeasure P] in
theorem gridStopAux_le_iff (t : ℝ) (n k : ℕ) (ω : Ω) (a : WithTop ℝ) :
    gridStopAux τ t n k ω ≤ a ↔ ∃ j ≤ k, stepStop τ (gridPt t n j) ω ≤ a

Module navigation

Module: LevyStochCalc/Brownian/ItoLocality.

Next: eventually_gridStop_lt.

Source excerpt, lines 99–101 · Frozen source 408915f.