Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-26
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.

Limit superior and limit inferior of a real sequence as infnsupknxk\inf_n \sup_{k \ge n} x_k and supninfknxk\sup_n \inf_{k \ge n} x_k in R\overline{\mathbb{R}}

Definition

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences). For nNn \in \mathbb{N} let

Tn  :=  {xk:kN, kn}RT_n \;:=\; \{\, x_k : k \in \mathbb{N},\ k \ge n \,\} \subseteq \mathbb{R}

be the nn-th tail range of (xk)(x_k), a nonempty subset of R\mathbb{R} since xnTnx_n \in T_n. Regard TnT_n as a subset of R\overline{\mathbb{R}} (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined) and put

sn  :=  supTnR,in  :=  infTnR,s_n \;:=\; \sup T_n \in \overline{\mathbb{R}}, \qquad i_n \;:=\; \inf T_n \in \overline{\mathbb{R}},

the supremum and infimum taken in R\overline{\mathbb{R}}, which exist for every nn and for every sequence by Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, agreeing with the real supremum and infimum on nonempty sets bounded in R\mathbb{R}. The limit superior and limit inferior of (xk)(x_k) are then

lim supkxk  :=  inf{sn:nN},lim infkxk  :=  sup{in:nN},\limsup_{k} x_k \;:=\; \inf \{\, s_n : n \in \mathbb{N} \,\}, \qquad \liminf_{k} x_k \;:=\; \sup \{\, i_n : n \in \mathbb{N} \,\},

again taken in R\overline{\mathbb{R}} and again existing by Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, agreeing with the real supremum and infimum on nonempty sets bounded in R\mathbb{R}, since {sn:nN}\{s_n : n \in \mathbb{N}\} and {in:nN}\{i_n : n \in \mathbb{N}\} are subsets of R\overline{\mathbb{R}} on which no hypothesis is needed. Both are elements of R\overline{\mathbb{R}}, and either may be ++\infty or -\infty. The notations lim supkxk\limsup_{k \to \infty} x_k, limkxk\varlimsup_k x_k and limkxk\overline{\lim}_k x_k all denote the first of them elsewhere; this library writes lim supkxk\limsup_k x_k.

Every quantity written here exists, and that is why the extended line was introduced. Each of the four operations above is an application of Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, agreeing with the real supremum and infimum on nonempty sets bounded in R\mathbb{R} to a subset of R\overline{\mathbb{R}} carrying no hypothesis whatever. Written with the real supremum of Complete ordered field (least-upper-bound property) and the real infimum of Every nonempty set bounded below has an infimum instead, the definition would be available only for sequences that are bounded (Lower bound, bounded below, bounded set): supTn\sup T_n needs TnT_n bounded above, and inf{sn}\inf\{s_n\} needs {sn}\{s_n\} nonempty, bounded below, and made of real numbers (Greatest lower bound (infimum)). None of those is automatic, and the discipline recorded in Conventions: sup\sup \emptyset, unbounded sets, and the extended reals forbids papering over the gap with a convention. The extended supremum is a different operation in a different ordered set, and it is total.

Values, when the sequence is bounded. If (xk)(x_k) is bounded, say xkM|x_k| \le M for every kk, then each TnT_n is a nonempty subset of R\mathbb{R} bounded above by MM and below by M-M, so by the agreement clause of Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, agreeing with the real supremum and infimum on nonempty sets bounded in R\mathbb{R} each sns_n and each ini_n is the real supremum or infimum of TnT_n, and lies in [M,M][-M, M]. The family {sn}\{s_n\} is then a nonempty set of reals bounded below by M-M, so lim supkxk\limsup_k x_k is likewise the real infimum of {sn}\{s_n\} and lies in [M,M][-M, M]; dually for lim infkxk\liminf_k x_k. So for a bounded sequence both quantities are ordinary real numbers computed with the ordinary real supremum and infimum, and the extended line is doing no work. It is only for unbounded sequences that the values ±\pm\infty occur.

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources