English
For every ω, the upcrossings value is finite if and only if there exists a bound k such that every upcrossingsBefore(a, b, f, N, ω) ≤ k for all N.
Русский
Для каждого элемента пространства график upcrossings(A,B,f,ω) конечен тогда и только тогда существует предел k, такой что для всех N выполняется upcrossingsBefore(a,b,f,N,ω) ≤ k.
LaTeX
$$upcrossings(a,b,f)(ω) < \infty \iff \exists k \in \mathbb{R}_{\ge 0}, \; \forall N, \; upcrossingsBefore(a,b,f,N)(ω) \le k$$
Lean4
theorem upcrossings_lt_top_iff : upcrossings a b f ω < ∞ ↔ ∃ k, ∀ N, upcrossingsBefore a b f N ω ≤ k :=
by
have : upcrossings a b f ω < ∞ ↔ ∃ k : ℝ≥0, upcrossings a b f ω ≤ k :=
by
constructor
· intro h
lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
exact ⟨r, le_rfl⟩
· rintro ⟨k, hk⟩
exact lt_of_le_of_lt hk ENNReal.coe_lt_top
simp_rw [this, upcrossings, iSup_le_iff]
constructor <;> rintro ⟨k, hk⟩
· obtain ⟨m, hm⟩ := exists_nat_ge k
refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩
rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]
· refine ⟨k, fun N => ?_⟩
simp only [ENNReal.coe_natCast, Nat.cast_le, hk N]
