Alphabeta Math

limsup, liminf, and Subsequential Limits

About this page
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 19 results · all verified · 19 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 19 also cleared it.
1 · Prerequisites
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Definition

The extended real line ℝ̄ = ℝ ∪ {-∞, +∞}, its order, and the arithmetic that is left undefined

Lemma

Every subset of ℝ̄ has a least upper bound and a greatest lower bound in ℝ̄, agreeing with the real supremum and infimum on nonempty sets bounded in ℝ

Definition

Convergence in ℝ̄ and the extended subsequential limit set: L ∈ ℝ̄ is an extended subsequential limit when some subsequence converges to L, or diverges to L = ±∞

Definition

Limit superior and limit inferior of a real sequence as infₙ sup_k ≥ n xₖ and supₙ inf_k ≥ n xₖ in ℝ̄

Lemma

The tail suprema of any real sequence are nonincreasing in ℝ̄, so the limit superior exists for every sequence

Lemma

limsup(-xₖ) = -liminf(xₖ), with the reflection of ℝ̄ exchanging ±∞

Lemma

liminf xₖ ≤ limsup xₖ for every real sequence

Lemma

For finite L: L = limsup xₖ iff for every ε > 0 one has xₖ < L + ε eventually and xₖ > L - ε frequently

Theorem

A real sequence converges to L ∈ ℝ iff liminf xₖ = limsup xₖ = L, and diverges to ±∞ iff both equal ±∞

Theorem

The limit superior is itself a subsequential limit in ℝ̄ and is the greatest one

Corollary

The limit inferior is the least subsequential limit in ℝ̄

Theorem

If each yⱼ is a subsequential limit of (xₖ) and yⱼ → y ∈ ℝ, then y is a subsequential limit of (xₖ)

Lemma

If xₖ ≤ yₖ eventually then limsup xₖ ≤ limsup yₖ and liminf xₖ ≤ liminf yₖ

Theorem

limsup(xₖ + yₖ) ≤ limsup xₖ + limsup yₖ whenever the right-hand side is defined in ℝ̄, and dually for liminf

Theorem

For bounded nonnegative sequences, limsup(xₖ yₖ) ≤ (limsup xₖ)(limsup yₖ)

Lemma

n^1/n → 1

Lemma

For every a > 0, a^1/n → 1

Theorem

For aₖ > 0: liminf aₖ₊₁/aₖ ≤ liminf aₖ^1/k ≤ limsup aₖ^1/k ≤ limsup aₖ₊₁/aₖ

Lemma

For every p > 0 and every positive rational α, n^α/(1+p)ⁿ → 0

Lemma

For every real x, xᵏ/k! → 0

Remark

Which extended-real operations this library leaves undefined, and where each limsup statement needs the hypothesis

False statement

FALSE: limsup(xₖ + yₖ) = limsup xₖ + limsup yₖ

False statement

FALSE: limsup aₖ^1/k = limsup aₖ₊₁/aₖ for every positive sequence

Sources