English
If a not-bounded-ness condition holds for a Real sequence with ENNReal mapping, then there exist rationals a < b such that x_i < a frequently and x_i > b frequently along the filter.
Русский
Если последовательность не ограничена сверху и существует несбалансированное отображение ENNReal, то существуют рациональные a<b такие, что x_i < a часто и x_i > b часто вдоль фильтра.
LaTeX
$$$\\exists a,b \\in \\mathbb{Q},\\ a < b \\land (\\exists^{\\text{Frequently}} i, x_i < a) \\land (\\exists^{\\text{Frequently}} i, b < x_i).$$$
Lean4
theorem exists_upcrossings_of_not_bounded_under {ι : Type*} {l : Filter ι} {x : ι → ℝ}
(hf : liminf (fun i => (Real.nnabs (x i) : ℝ≥0∞)) l ≠ ∞) (hbdd : ¬IsBoundedUnder (· ≤ ·) l fun i => |x i|) :
∃ a b : ℚ, a < b ∧ (∃ᶠ i in l, x i < a) ∧ ∃ᶠ i in l, ↑b < x i :=
by
rw [isBoundedUnder_le_abs, not_and_or] at hbdd
obtain hbdd | hbdd := hbdd
· obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top hf
obtain ⟨q, hq⟩ := exists_rat_gt R
refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
· refine fun hcon => hR ?_
filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
· simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
refine fun hcon => hbdd ↑(q + 1) ?_
filter_upwards [hcon] with x hx using not_lt.1 hx
· obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top' hf
obtain ⟨q, hq⟩ := exists_rat_lt R
refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩
· simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
refine fun hcon => hbdd ↑(q - 1) ?_
filter_upwards [hcon] with x hx using not_lt.1 hx
· refine fun hcon => hR ?_
filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)
