English
0 ≤ upcrossingStrat(a,b,f,N,n,ω) ≤ 1 for all n, ω.
Русский
0 ≤ upcrossingStrat(a,b,f,N,n,ω) ≤ 1 для всех n, ω.
LaTeX
$$$0 \le upcrossingStrat(a,b,f,N,n,\omega) \le 1$$$
Lean4
theorem upcrossingStrat_le_one : upcrossingStrat a b f N n ω ≤ 1 :=
by
rw [upcrossingStrat, ← Finset.indicator_biUnion_apply]
· exact Set.indicator_le_self' (fun _ _ => zero_le_one) _
intro i _ j _ hij
simp only [Set.Ico_disjoint_Ico]
obtain hij' | hij' := lt_or_gt_of_ne hij
· rw [min_eq_left
(upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
max_eq_right (lowerCrossingTime_mono hij'.le : lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
refine le_trans upperCrossingTime_le_lowerCrossingTime (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))
· rw [min_eq_right
(upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
max_eq_left (lowerCrossingTime_mono hij'.le : lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
refine le_trans upperCrossingTime_le_lowerCrossingTime (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))
