English
Under a<b, the upcrossings count equals a finite sum over k of indicators of whether upperCrossingTime a b f N n ω < N.
Русский
При a<b число восходящих равно конечной сумме по индикаторам условий верхнего времени пересечения.
LaTeX
$$$\\mathrm{upcrossingsBefore}(a,b,f,N,\\omega) = \\sum_{i ∈ \\mathrm{Ico}\\,1,(N+1)} \\mathbf{1}_{\\{n : \\mathrm{upperCrossingTime}(a,b,f,N,n,\\omega) < N\\}}(i).$$$
Lean4
theorem upcrossingsBefore_eq_sum (hab : a < b) :
upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i :=
by
by_cases hN : N = 0
· simp [hN]
rw [← Finset.sum_Ico_consecutive _ (Nat.succ_le_succ zero_le') (Nat.succ_le_succ (upcrossingsBefore_le f ω hab))]
have h₁ :
∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
{n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1 :=
by
rintro k hk
rw [Finset.mem_Ico] at hk
rw [Set.indicator_of_mem]
· rfl
· exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab (Nat.lt_succ_iff.1 hk.2)
have h₂ :
∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
{n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0 :=
by
rintro k hk
rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
rw [Set.indicator_of_notMem]
simp only [Set.mem_setOf_eq, not_lt]
exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le
rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const, smul_eq_mul, mul_one,
smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one, add_zero, add_zero]
