English
If a<b, then it is not true that both the process visits below a and above b frequently at the same ω.
Русский
Если a<b, то невозможно, чтобы процесс часто посещал значения ниже a и выше b при одном и том же ω одновременно.
LaTeX
$$$\\neg\\Big(\\exists^{\\infty} n: f_n(\\omega) < a \\ \\wedge\\ \\exists^{\\infty} n: b < f_n(\\omega)\\Big).$$$
Lean4
/-- If a stochastic process has bounded upcrossing from below `a` to above `b`,
then it does not frequently visit both below `a` and above `b`. -/
theorem not_frequently_of_upcrossings_lt_top (hab : a < b) (hω : upcrossings a b f ω ≠ ∞) :
¬((∃ᶠ n in atTop, f n ω < a) ∧ ∃ᶠ n in atTop, b < f n ω) :=
by
rw [← lt_top_iff_ne_top, upcrossings_lt_top_iff] at hω
replace hω : ∃ k, ∀ N, upcrossingsBefore a b f N ω < k :=
by
obtain ⟨k, hk⟩ := hω
exact ⟨k + 1, fun N => lt_of_le_of_lt (hk N) k.lt_succ_self⟩
rintro ⟨h₁, h₂⟩
rw [frequently_atTop] at h₁ h₂
refine Classical.not_not.2 hω ?_
push_neg
intro k
induction k with
| zero => simp only [zero_le, exists_const]
| succ k ih =>
obtain ⟨N, hN⟩ := ih
obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N
obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁
exact
⟨N₂ + 1, Nat.succ_le_of_lt <| lt_of_le_of_lt hN (upcrossingsBefore_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩
