English
If a < b and upcrossingsBefore a b f N ω < n, then the difference stoppedValue(upperCrossingTime) − stoppedValue(lowerCrossingTime) equals zero.
Русский
Если a < b и upcrossingsBefore a b f N ω < n, то разность между остановленным значением верхнего и нижнего времени пересечения равна нулю.
LaTeX
$$$\\mathrm{upcrossingsBefore}(a,b,f,N,\\omega) < n\\Rightarrow \\mathrm{stoppedValue}(f,\\mathrm{upperCrossingTime}(a,b,f,N,n+1,\\omega)) - \\mathrm{stoppedValue}(f,\\mathrm{lowerCrossingTime}(a,b,f,N,n,\\omega)) = 0.$$$
Lean4
theorem sub_eq_zero_of_upcrossingsBefore_lt (hab : a < b) (hn : upcrossingsBefore a b f N ω < n) :
stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0 :=
by
have : N ≤ upperCrossingTime a b f N n ω := by
rw [upcrossingsBefore] at hn
rw [← not_lt]
exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]
