theorem Sequences.limsup_eq_lim_sup_tail (x : ℕ → ℝ) (hb : BddAbove (Set.range x)) (hb' : BddBelow (Set.range x)) : Filter.limsup x Filter.atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), x (i + n)

For a bounded real sequence x : ℕ → ℝ, the filter-theoretic limsup along atTop agrees with the textbook definition limsup x = inf_{n} sup_{k ≥ n} x k, here written as ⨅ n, ⨆ i, x (i + n).

This realizes the informal definition: for bounded {xₙ}, limsup xₙ := lim_{n→∞} sup{xₖ : k ≥ n}.

theorem Sequences.convergent_iff_limsup_eq_liminf (x : ℕ → ℝ) (hbdd : BddAbove (Set.range x) ∧ BddBelow (Set.range x)) : (∃ (L : ℝ), Filter.Tendsto x Filter.atTop (nhds L)) ↔ Filter.limsup x Filter.atTop = Filter.liminf x Filter.atTop

A bounded real sequence x : ℕ → ℝ converges to some limit L if and only if its limsup and liminf (along atTop) coincide.

This is the standard characterization: a bounded sequence {xₙ} converges iff liminf xₙ = limsup xₙ.