exists_frequently_lt_of_liminf_ne_top

English

If the liminf of the ENNReal-norm of a Real-valued sequence is finite (not ∞), there exists a real bound R such that x_n < R frequently along the filter.

Русский

Если лиминфим последовательности имеет конечное значение, существует такое число R, что x_n < R встречается часто вдоль фильтра.

LaTeX

$$$\\text{liminf}_{l} (|x_n|) < \\infty \\Rightarrow \\exists R, \\text{Frequently}_{l}(x_n < R).$$$

Lean4

theorem exists_frequently_lt_of_liminf_ne_top {ι : Type*} {l : Filter ι} {x : ι → ℝ}
    (hx : liminf (fun n => (Real.nnabs (x n) : ℝ≥0∞)) l ≠ ∞) : ∃ R, ∃ᶠ n in l, x n < R :=
  by
  by_contra h
  simp_rw [not_exists, not_frequently, not_lt] at h
  refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
  simp only [eventually_map, ENNReal.coe_le_coe]
  filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))

Похожие утверждения