English
For f, N, ω and hab: a<b, we have upperCrossingTime(a,b,f,N,N,ω) = N.
Русский
Для любых f, N, ω и a<b имеет место upperCrossingTime(a,b,f,N,N,ω) = N.
LaTeX
$$$\forall f,N,ω\; (a < b) \Rightarrow upperCrossingTime(a,b,f,N,N,\omega) = N$$$
Lean4
theorem upperCrossingTime_bound_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) : upperCrossingTime a b f N N ω = N :=
by
by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)
· refine le_antisymm upperCrossingTime_le ?_
have hmono :
StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
(Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) :=
by
refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
rw [Nat.lt_pred_iff] at hm
convert Nat.find_min _ hm
convert StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')
· rw [not_lt] at hN'
exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))
