Existence of a Uniform-Grid Cell

This is a technical fact about the uniform time grid.

Let $T,s\in\mathbb R$ and $m\in\mathbb N$ satisfy $0<T$, $m\ne0$, $0<s$, and $s\le T$. For the grid point

there exists an index $i\in\mathbb N$ such that

Thus every time in $(0,T]$ lies in one of the half-open cells of the uniform partition.

This lemma is reused to locate time points in grid-based arguments.

Original Lean declaration header

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

theorem exists_unifGrid_cell {T : ℝ} (hT : 0 < T) {m : ℕ} (hm0 : m ≠ 0) {s : ℝ}
    (hs : 0 < s) (hsT : s ≤ T) :
    ∃ i : ℕ, i < m ∧ unifGrid T m i < s ∧ s ≤ unifGrid T m (i + 1)

Module navigation

Module: LevyStochCalc/Brownian/ItoFormulaGrid.

Next: integral_abs_add_pow_three_le.

Source excerpt, lines 81–83 · Frozen source 408915f.