English
Let hr ≥ 0, f(0) = 0, and assume the increments |f(i+1) − f(i)| are almost surely bounded by R. Then for every i, almost surely the stopped value at the stopping time leastGE(f, r, i) does not exceed r + R.
Русский
Пусть hr ≥ 0, f(0) = 0, и предположим, что при almost surely выполнено |f(i+1) − f(i)| ≤ R. Тогда для каждого i почти surely имеет место: stoppedValue(f, leastGE(f, r, i)) ≤ r + R.
LaTeX
$$$$\text{Assume } 0 \le r,\ f(0)=0,\ \forall^*\omega\,\partial\mu:\forall i,\ |f(i+1)\omega - f(i)\omega| \le R. \\ \text{Then } \forall i \in \mathbb{N},\; \mu\text{-a.e. } \omega:\ \mathrm{stoppedValue}(f, \mathrm{leastGE}(f,r,i))\,\omega \le r+R.$$$$
Lean4
theorem norm_stoppedValue_leastGE_le (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R)
(i : ℕ) : ∀ᵐ ω ∂μ, stoppedValue f (leastGE f r i) ω ≤ r + R :=
by
filter_upwards [hbdd] with ω hbddω
change f (leastGE f r i ω) ω ≤ r + R
by_cases heq : leastGE f r i ω = 0
· rw [heq, hf0, Pi.zero_apply]
exact add_nonneg hr R.coe_nonneg
· obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero heq
rw [hk, add_comm, ← sub_le_iff_le_add]
have := notMem_of_lt_hitting (hk.symm ▸ k.lt_succ_self : k < leastGE f r i ω) (zero_le _)
simp only [Set.mem_Ici, not_le] at this
exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))
