Alphabeta Math
Session-authored (Fable 5 assisted)
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.

limsup, liminf, and Subsequential Limits

1 · Prerequisites

2 · Summary

Objective. Every real sequence has a largest and a smallest thing it keeps coming back to. This page defines those two quantities, proves that they always exist, and shows that their coincidence is exactly convergence. The obstacle is that neither quantity is a real number in general, and the previous pages deliberately refused to pretend otherwise: Conventions: sup\sup \emptyset, unbounded sets, and the extended reals barred the conventions supS=+\sup S = +\infty and inf=+\inf \emptyset = +\infty inside R\mathbb{R}, and promised that a page needing the extended line would introduce it explicitly as a new object rather than quietly enlarging R\mathbb{R}. This is that page, and the promise is discharged in its first two items.

The extended line, built once and used everywhere. The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined adjoins two objects -\infty and ++\infty to R\mathbb{R}, fixes a total order in which they are the least and greatest elements, and defines exactly two partial operations, leaving (+)+()(+\infty) + (-\infty) and 0(±)0 \cdot (\pm\infty) undefined. Nothing about R\mathbb{R} is changed, and no algebraic law is inherited: R\overline{\mathbb{R}} is not a field. What it does have is 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}: every subset of R\overline{\mathbb{R}}, with no hypothesis whatever, has a least upper bound and a greatest lower bound there, agreeing with the real supremum and infimum wherever the latter are defined. That single lemma is what makes the whole page hypothesis free, and fourteen of its items rest on it.

The two quantities. 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}} sets lim supkxk=infnsupknxk\limsup_k x_k = \inf_n \sup_{k \ge n} x_k and lim infkxk=supninfknxk\liminf_k x_k = \sup_n \inf_{k \ge n} x_k, both taken in R\overline{\mathbb{R}}; The tail suprema of any real sequence are nonincreasing in R\overline{\mathbb{R}}, so the limit superior exists for every sequence records that the tail suprema decrease and the tail infima increase, so the outer operations act on monotone families, and that both quantities exist for every sequence, bounded or not. lim sup(xk)=lim inf(xk)\limsup(-x_k) = -\liminf(x_k), with the reflection of R\overline{\mathbb{R}} exchanging ±\pm\infty proves that xxx \mapsto -x exchanges the two, which is what lets every later statement about lim sup\limsup be read off as a statement about lim inf\liminf without a second proof. lim infxklim supxk\liminf x_k \le \limsup x_k for every real sequence puts them in order, and For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently gives the working form in the finite case: L=lim supkxkL = \limsup_k x_k exactly when xkx_k is eventually below L+εL + \varepsilon and frequently above LεL - \varepsilon, for every ε>0\varepsilon > 0. The asymmetry between eventually and frequently is the whole content of the notion.

What they are for. A real sequence converges to LRL \in \mathbb{R} iff lim infxk=lim supxk=L\liminf x_k = \limsup x_k = L, and diverges to ±\pm\infty iff both equal ±\pm\infty is the theorem that justifies the definitions: a sequence converges to a real LL exactly when both quantities equal LL, and diverges to ±\pm\infty exactly when both equal ±\pm\infty. So a question about convergence becomes a question about two quantities that always exist, and a proof of convergence can be assembled from one-sided estimates with no candidate limit in hand. The limit superior is itself a subsequential limit in R\overline{\mathbb{R}} and is the greatest one identifies them intrinsically: lim supkxk\limsup_k x_k is itself a subsequential limit and is the greatest one, with The limit inferior is the least subsequential limit in R\overline{\mathbb{R}} the dual. Both statements live in R\overline{\mathbb{R}}, and they have to: the greatest subsequential limit of an unbounded sequence need not be real, and the finite subsequential limit set may have a greatest element that is not the limit superior. Since the published Subsequential limit of a real sequence, and the subsequential limit set is finite by design, Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty extends it by citation, adding the two divergence clauses without touching what was already fixed. If each yjy_j is a subsequential limit of (xk)(x_k) and yjyRy_j \to y \in \mathbb{R}, then yy is a subsequential limit of (xk)(x_k) completes the picture from the other side: the subsequential limit set contains the limit of every convergent sequence of its own points.

Calculus of the two quantities. If xkykx_k \le y_k eventually then lim supxklim supyk\limsup x_k \le \limsup y_k and lim infxklim infyk\liminf x_k \le \liminf y_k is the comparison principle, lim sup(xk+yk)lim supxk+lim supyk\limsup(x_k + y_k) \le \limsup x_k + \limsup y_k whenever the right-hand side is defined in R\overline{\mathbb{R}}, and dually for lim inf\liminf the subadditivity, with the hypothesis that the right-hand side be defined in R\overline{\mathbb{R}} and not a hypothesis more, and For bounded nonnegative sequences, lim sup(xkyk)(lim supxk)(lim supyk)\limsup(x_k y_k) \le (\limsup x_k)(\limsup y_k) the multiplicative analogue for bounded nonnegative sequences, where both hypotheses are load bearing. Neither inequality can be reversed: FALSE: lim sup(xk+yk)=lim supxk+lim supyk\limsup(x_k + y_k) = \limsup x_k + \limsup y_k records that for the sum, and xk=(1)kx_k = (-1)^k, yk=(1)k+1y_k = (-1)^{k+1} give lim sup(xk+yk)=0<2=lim supxk+lim supyk\limsup(x_k + y_k) = 0 < 2 = \limsup x_k + \limsup y_k and xk=1+(1)kx_k = 1 + (-1)^k, yk=1+(1)k+1y_k = 1 + (-1)^{k+1} give lim sup(xkyk)=0<4\limsup(x_k y_k) = 0 < 4 exhibit strict inequality in each case.

The ratio-to-root chain, and the standard limits. For ak>0a_k > 0: lim infak+1/aklim infak1/klim supak1/klim supak+1/ak\liminf a_{k+1}/a_k \le \liminf a_k^{1/k} \le \limsup a_k^{1/k} \le \limsup a_{k+1}/a_k proves lim infak+1/aklim infak1/klim supak1/klim supak+1/ak\liminf a_{k+1}/a_k \le \liminf a_k^{1/k} \le \limsup a_k^{1/k} \le \limsup a_{k+1}/a_k for a positive sequence. This is the precise sense in which a root criterion dominates a ratio criterion, and it belongs here rather than with series, because it is a statement about lim sup\limsup and nothing else. FALSE: lim supak1/k=lim supak+1/ak\limsup a_k^{1/k} = \limsup a_{k+1}/a_k for every positive sequence shows the outer inequalities are not equalities. The proof needs For every a>0a > 0, a1/n1a^{1/n} \to 1, which with n1/n1n^{1/n} \to 1, For every p>0p > 0 and every positive rational α\alpha, nα/(1+p)n0n^{\alpha}/(1+p)^n \to 0 and For every real xx, xk/k!0x^k/k! \to 0 makes up the four standard limits of elementary analysis; the last two are proved directly from Bernoulli's inequality and the Archimedean property, since continuity of xxαx\mapsto x^\alpha is not available at this point in the reading order; it is proved later in Continuity and derivatives of positive-base real powers.

A note on indices. Sequences here are functions on N\mathbb{N} and N\mathbb{N} contains 00 (Sequences of reals: bounded, eventually, frequently, tails, subsequences). The expressions n1/nn^{1/n}, a1/na^{1/n} and ak1/ka_k^{1/k} are undefined at index 00, so the corresponding statements are made about the shifted families (k+1)1/(k+1)(k+1)^{1/(k+1)}, a1/(k+1)a^{1/(k+1)} and ak+11/(k+1)a_{k+1}^{1/(k+1)}; the expressions nα/(1+p)nn^{\alpha}/(1+p)^n and xk/k!x^k/k! are defined at 00 and are not shifted. Each item says which case it is in.

What is left undefined, and where it bites. Which extended-real operations this library leaves undefined, and where each lim sup\limsup statement needs the hypothesis collects the two gaps in the arithmetic of R\overline{\mathbb{R}}, says why no value could fill them, and goes through the page recording which statements carry a hypothesis because of them and which are unconditional. The short version: everything order-theoretic is hypothesis free, and everything arithmetic is not.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined

Definition

Fix two objects -\infty and ++\infty, distinct from one another and neither of them a real number (The real numbers), and set

R:=R{,+}.\overline{\mathbb{R}} := \mathbb{R} \cup \{-\infty, +\infty\}.

This is a new object, introduced here explicitly with its own order and its own partial arithmetic. It is not an enlargement of the field R\mathbb{R}, and no operation of R\mathbb{R} (Complete ordered field (least-upper-bound property)) is redefined by anything below.

The order. For a,bRa, b \in \overline{\mathbb{R}} declare

ab:a=  or  b=+  or  (a,bR and ab in R),a \le b \quad :\Longleftrightarrow \quad a = -\infty \ \text{ or } \ b = +\infty \ \text{ or } \ \big(a, b \in \mathbb{R} \text{ and } a \le b \text{ in } \mathbb{R}\big),

with R\mathbb{R} ordered as in Order on the reals, and write a<ba < b for "aba \le b and aba \ne b" as usual (Partial order and partially ordered set).

(R,)(\overline{\mathbb{R}}, \le) is a totally ordered set, and the inclusion of R\mathbb{R} preserves and reflects the order. All four checks are immediate from the displayed clauses.

  • Reflexive. For a=±a = \pm\infty one of the first two clauses applies; for aRa \in \mathbb{R} the third does, since aaa \le a in R\mathbb{R}.
  • Antisymmetric. Suppose aba \le b and bab \le a. If a=a = -\infty then bab \le a forces b=b = -\infty, since the clause a=+a = +\infty fails and b,ab, a are not both real. Symmetrically b=b = -\infty forces a=a = -\infty, and a=+a = +\infty or b=+b = +\infty forces the other to be ++\infty. In the one remaining situation aa and bb are both real and antisymmetry is that of R\mathbb{R}.
  • Transitive. Let abca \le b \le c. If a=a = -\infty or c=+c = +\infty the conclusion is one of the first two clauses. Otherwise aa \ne -\infty forces, in aba \le b, either b=+b = +\infty or a,bRa, b \in \mathbb{R}; and c+c \ne +\infty forces, in bcb \le c, either b=b = -\infty or b,cRb, c \in \mathbb{R}. The value b=+b = +\infty is incompatible with the second alternative pair, so bb is real, hence so are aa and cc, and transitivity is that of R\mathbb{R}.
  • Total. If a=a = -\infty or b=+b = +\infty then aba \le b; if b=b = -\infty or a=+a = +\infty then bab \le a; otherwise both are real and the order of R\mathbb{R} is total.
  • Preserved and reflected. For a,bRa, b \in \mathbb{R} the first two clauses fail, so aba \le b in R\overline{\mathbb{R}} says exactly aba \le b in R\mathbb{R}.

In particular -\infty is the least and ++\infty the greatest element of R\overline{\mathbb{R}}, and <x<+-\infty < x < +\infty for every xRx \in \mathbb{R}.

Reflection. Extend negation by

(+):=,():=+,-(+\infty) := -\infty, \qquad -(-\infty) := +\infty,

keeping the field negative on R\mathbb{R}. The resulting map ν:RR\nu : \overline{\mathbb{R}} \to \overline{\mathbb{R}}, ν(a)=a\nu(a) = -a, satisfies ν(ν(a))=a\nu(\nu(a)) = a and

ab    ba(a,bR).a \le b \iff -b \le -a \qquad (a, b \in \overline{\mathbb{R}}).

For aa and bb real this is the elementwise order reversal in R\mathbb{R}: translation invariance (Order is preserved by adding a constant and by adding inequalities) applied with the constant ab-a-b turns a<ba < b into b<a-b < -a and, applied with the constant a+ba+b, turns it back, while a=ba = b holds exactly when a=b-a = -b. In every other case both sides are decided by the first two clauses of the order: a=a = -\infty makes both sides true, as does b=+b = +\infty, and if aa \ne -\infty, b+b \ne +\infty and a,ba, b are not both real then one of a=+a = +\infty, b=b = -\infty holds and both sides are false.

Partial addition. For a,bRa, b \in \overline{\mathbb{R}} the sum a+ba + b is defined by

  • a+ba + b = the field sum, when a,bRa, b \in \mathbb{R};
  • a+b:=+a + b := +\infty when a=+a = +\infty and bb \ne -\infty, or b=+b = +\infty and aa \ne -\infty;
  • a+b:=a + b := -\infty when a=a = -\infty and b+b \ne +\infty, or b=b = -\infty and a+a \ne +\infty;

and the two sums (+)+()(+\infty) + (-\infty) and ()+(+)(-\infty) + (+\infty) are left undefined. Addition is commutative where defined, and

(a+b)=(a)+(b),-(a + b) = (-a) + (-b),

each side being defined exactly when the other is: the excluded pairs {+,}\{+\infty, -\infty\} are exchanged by ν\nu, and the three clauses above are exchanged accordingly.

Partial multiplication. For a,bRa, b \in \overline{\mathbb{R}} the product abab is defined by

  • abab = the field product, when a,bRa, b \in \mathbb{R};
  • ab:=+ab := +\infty when one of a,ba, b is ±\pm\infty, the other is 0\ne 0, and both are >0> 0 or both are <0< 0;
  • ab:=ab := -\infty when one of a,ba, b is ±\pm\infty, the other is 0\ne 0, and one is >0> 0 and the other <0< 0;

and every product with one factor 00 and the other ±\pm\infty is left undefined. The comparisons >0> 0 and <0< 0 here are taken in the order above, under which +>0>+\infty > 0 > -\infty.

Nothing else is defined. There is no subtraction, no division, no exponentiation and no absolute value on R\overline{\mathbb{R}} in this library; where such an expression is wanted it is written out in the two defined operations, and where a case falls in the undefined list the statement carries an explicit hypothesis saying so.

Remarks

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

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}

Statement

Let ARA \subseteq \overline{\mathbb{R}} be any subset of the extended real line (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined) and write AR:=ARA_{\mathbb{R}} := A \cap \mathbb{R}. Then AA has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}} (Upper bound, least upper bound, and strict upper bound), each unique, which we write supA\sup A and infA\inf A with the ambient set always R\overline{\mathbb{R}}. Explicitly:

  • supA=+\sup A = +\infty if +A+\infty \in A, or if ARA_{\mathbb{R}} is not bounded above in R\mathbb{R};
  • supA=\sup A = -\infty if +A+\infty \notin A and AR=A_{\mathbb{R}} = \emptyset;
  • supA\sup A is the real supremum supAR\sup A_{\mathbb{R}} (Complete ordered field (least-upper-bound property)) if +A+\infty \notin A and ARA_{\mathbb{R}} is nonempty and bounded above in R\mathbb{R};

and dually, with -\infty and ++\infty exchanged and "above" replaced by "below", for infA\inf A (Greatest lower bound (infimum), Every nonempty set bounded below has an infimum).

Agreement. If ARA \subseteq \mathbb{R} is nonempty and bounded above in R\mathbb{R} (Lower bound, bounded below, bounded set) then supA\sup A computed in R\overline{\mathbb{R}} is the real number supA\sup A of Complete ordered field (least-upper-bound property); if ARA \subseteq \mathbb{R} is nonempty and bounded below then infA\inf A computed in R\overline{\mathbb{R}} is the real number infA\inf A of Every nonempty set bounded below has an infimum. In particular the notation is unambiguous on the sets for which the real supremum and infimum are defined, and sup=\sup \emptyset = -\infty, inf=+\inf \emptyset = +\infty in R\overline{\mathbb{R}}.

No hypothesis is placed on AA. This is exactly what the real supremum cannot do, and it is why every lim sup\limsup statement on this page holds for every sequence rather than for bounded ones only. It is also not a weakening of the discipline this library keeps around suprema: the operation supplied here is a different operation, taken in a different ordered set, and the agreement clause records exactly where the two coincide.

Facts & Assumptions

Given: A subset ARA \subseteq \overline{\mathbb{R}}, and its real part AR:=ARA_{\mathbb{R}} := A \cap \mathbb{R}.

[L1]

(R,)(\overline{\mathbb{R}}, \le) is a totally ordered set in which -\infty is the least element and ++\infty the greatest, and whose order restricted to R\mathbb{R} is the order of R\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, Partial order and partially ordered set, Order on the reals).

[L2]

Upper and lower bounds in a poset: uu is an upper bound of AA when aua \le u for all aAa \in A, and a least upper bound when moreover uvu \le v for every upper bound vv; dually for lower bounds and greatest lower bounds. Each is unique when it exists, by antisymmetry (Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L3]

Least-upper-bound property of R\mathbb{R}: every nonempty SRS \subseteq \mathbb{R} that is bounded above in R\mathbb{R} has a real least upper bound supS\sup S (Complete ordered field (least-upper-bound property)).

[L4]

Greatest-lower-bound property of R\mathbb{R}: every nonempty SRS \subseteq \mathbb{R} that is bounded below in R\mathbb{R} has a real greatest lower bound infS\inf S (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)).

[L5]

Bounded above and bounded below in R\mathbb{R} mean the existence of a real upper, respectively lower, bound (Lower bound, bounded below, bounded set).

Proof

technique · cases
1.1

Case S1 for the supremum: +A+\infty \in A.

givenassume-case suptop
1.2

Case S2 for the supremum: +A+\infty \notin A and AR=A_{\mathbb{R}} = \emptyset, so that every element of AA equals -\infty.

givenassume-case supbot
1.3

Case S3 for the supremum: +A+\infty \notin A, ARA_{\mathbb{R}} \ne \emptyset, and ARA_{\mathbb{R}} is bounded above in R\mathbb{R}.

givenassume-case supfin
1.4

Case S4 for the supremum: +A+\infty \notin A, ARA_{\mathbb{R}} \ne \emptyset, and ARA_{\mathbb{R}} is not bounded above in R\mathbb{R}.

givenassume-case supunb
1.5

Case I1 for the infimum: A-\infty \in A.

givenassume-case infbot
1.6

Case I2 for the infimum: A-\infty \notin A and AR=A_{\mathbb{R}} = \emptyset, so that every element of AA equals ++\infty.

givenassume-case inftop
1.7

Case I3 for the infimum: A-\infty \notin A, ARA_{\mathbb{R}} \ne \emptyset, and ARA_{\mathbb{R}} is bounded below in R\mathbb{R}.

givenassume-case inffin
1.8

Case I4 for the infimum: A-\infty \notin A, ARA_{\mathbb{R}} \ne \emptyset, and ARA_{\mathbb{R}} is not bounded below in R\mathbb{R}.

givenassume-case infunb
2.1

In case S1 the element ++\infty is an upper bound of AA, being the greatest element of R\overline{\mathbb{R}}; and if vv is any upper bound of AA then +A+\infty \in A gives +v+\infty \le v, whence v=+v = +\infty by antisymmetry. So ++\infty is the least upper bound of AA.

step 1.1L1L2
2.2

In case S2 every element of AA equals -\infty, so -\infty is an upper bound of AA by reflexivity; and v-\infty \le v for every vRv \in \overline{\mathbb{R}}, being the least element. So -\infty is the least upper bound of AA.

step 1.2L1L2
2.3

In case S3 the real number σ:=supAR\sigma := \sup A_{\mathbb{R}} exists, and it is an upper bound of AA in R\overline{\mathbb{R}}: an element of AA is either real, hence lies in ARA_{\mathbb{R}} and satisfies aσa \le \sigma in R\mathbb{R} and so in R\overline{\mathbb{R}}, or equals -\infty, which is σ\le \sigma; the value ++\infty does not occur in AA in this case.

step 1.3L1L3
2.4

In case S4 the element ++\infty is an upper bound of AA; and if vv is an upper bound then vv \ne -\infty, because fixing aARa \in A_{\mathbb{R}}, which is possible in this case, gives ava \le v with aa real and -\infty is below no real, while vv real would make vv a real upper bound of ARA_{\mathbb{R}} and contradict the case hypothesis. So v=+v = +\infty, and ++\infty is the least upper bound of AA.

step 1.4L1L2L5
2.5

In case I1 the element -\infty is a lower bound of AA, being least; and any lower bound ww satisfies ww \le -\infty because A-\infty \in A, whence w=w = -\infty by antisymmetry. So -\infty is the greatest lower bound of AA.

step 1.5L1L2
2.6

In case I2 every element of AA equals ++\infty, so ++\infty is a lower bound of AA by reflexivity, and w+w \le +\infty for every ww. So ++\infty is the greatest lower bound of AA.

step 1.6L1L2
2.7

In case I3 the real number ι:=infAR\iota := \inf A_{\mathbb{R}} exists and is a lower bound of AA in R\overline{\mathbb{R}}: an element of AA is either real, hence in ARA_{\mathbb{R}} and ι\ge \iota, or equals +ι+\infty \ge \iota; the value -\infty does not occur in AA in this case.

step 1.7L1L4
2.8

In case I4 the element -\infty is a lower bound of AA; any lower bound ww satisfies w+w \ne +\infty, because fixing aARa \in A_{\mathbb{R}} gives waw \le a with aa real and ++\infty is above no real, while ww real would be a real lower bound of ARA_{\mathbb{R}} and contradict the case hypothesis. So w=w = -\infty is the greatest lower bound of AA.

step 1.8L1L2L5
3.1

In case S3 let vv be any upper bound of AA and fix aARa \in A_{\mathbb{R}}, which is possible since ARA_{\mathbb{R}} \ne \emptyset. From ava \le v with aa real we get vv \ne -\infty, since -\infty is below no real. If v=+v = +\infty then σv\sigma \le v because ++\infty is greatest. Otherwise vv is real, and it bounds ARA_{\mathbb{R}} above in R\mathbb{R}, so σv\sigma \le v by leastness of the real supremum. Hence σ\sigma is the least upper bound of AA.

step 1.3step 2.3L1L2L3
3.2

In case I3 let ww be a lower bound of AA and fix aARa \in A_{\mathbb{R}}. From waw \le a with aa real we get w+w \ne +\infty. If w=w = -\infty then wιw \le \iota; otherwise ww is real and bounds ARA_{\mathbb{R}} below in R\mathbb{R}, so wιw \le \iota. Hence ι\iota is the greatest lower bound of AA.

step 1.7step 2.7L1L2L4
4.1

The four supremum cases are exhaustive and mutually exclusive: either +A+\infty \in A, which is S1, or not, and then either AR=A_{\mathbb{R}} = \emptyset, which is S2, or ARA_{\mathbb{R}} \ne \emptyset and it is bounded above in R\mathbb{R}, which is S3, or it is not, which is S4. In each case a least upper bound was produced, and it is unique. The same four alternatives with -\infty, ++\infty and "below" in place of ++\infty, -\infty and "above" are I1 to I4, and in each a greatest lower bound was produced.

step 2.1step 2.2step 3.1step 2.4step 2.5step 2.6step 3.2step 2.8L2L5cases: a two-fold split followed by a three-fold splitcases-exhaustive
5.1

The agreement clause follows: a nonempty ARA \subseteq \mathbb{R} bounded above in R\mathbb{R} satisfies +A+\infty \notin A and AR=AA_{\mathbb{R}} = A, so case S3 applies and supA=supAR\sup A = \sup A_{\mathbb{R}} is the real supremum; a nonempty ARA \subseteq \mathbb{R} bounded below satisfies case I3 and infA\inf A is the real infimum; and A=A = \emptyset falls under S2 and I2, giving sup=\sup \emptyset = -\infty and inf=+\inf \emptyset = +\infty.

step 2.3step 3.1step 2.7step 3.2step 4.1L3L4

Remarks

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty

Definition

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and let LRL \in \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). Say that (xk)(x_k) converges to LL in R\overline{\mathbb{R}} when one of the following holds, according to which of the three kinds of element LL is:

Then LL is an extended subsequential limit of (xk)(x_k) when some subsequence of (xk)(x_k) converges to LL in R\overline{\mathbb{R}}: when there is a strictly increasing n:NNn : \mathbb{N} \to \mathbb{N} (Sequences of reals: bounded, eventually, frequently, tails, subsequences) such that (xnj)jN(x_{n_j})_{j \in \mathbb{N}} converges to LL in the sense just given. The extended subsequential limit set of (xk)(x_k) is

SL(x)  :=  {LR:L is an extended subsequential limit of (xk)}R.\overline{\operatorname{SL}}(x) \;:=\; \{\, L \in \overline{\mathbb{R}} : L \text{ is an extended subsequential limit of } (x_k) \,\} \subseteq \overline{\mathbb{R}}.

This extends the published Subsequential limit of a real sequence, and the subsequential limit set and does not replace it. That definition is finite by design: there LL ranges over R\mathbb{R} and SL(x)R\operatorname{SL}(x) \subseteq \mathbb{R}. Its clause is quoted verbatim as the first of the three clauses above, so

SL(x)R=SL(x),\overline{\operatorname{SL}}(x) \cap \mathbb{R} = \operatorname{SL}(x),

immediately from the definitions: a real LL lies in SL(x)\overline{\operatorname{SL}}(x) exactly when some subsequence converges to LL in the sense of Limits and Cauchy sequences of reals, which is exactly the condition LSL(x)L \in \operatorname{SL}(x). The extended set is therefore SL(x)\operatorname{SL}(x) together with at most the two extra points ±\pm\infty, each present exactly when some subsequence diverges to it. Nothing about SL(x)\operatorname{SL}(x) is redefined, and every statement proved about SL(x)\operatorname{SL}(x) elsewhere in the library remains a statement about the same set.

Neither is Divergence to ++\infty and to -\infty reinterpreted. The phrase "xk+x_k \to +\infty" keeps exactly the meaning fixed there, an abbreviation for "for every real MM, eventually xk>Mx_k > M". What is new is only that the phrase is now allowed to appear as one of three clauses in a single definition whose parameter LL ranges over R\overline{\mathbb{R}}, so that the three situations can be quantified over together. In particular the warning recorded there stands: a sequence diverging to ++\infty has no limit in R\mathbb{R}, and none of the rules of Algebra of limits: sums, scalar multiples, products and quotients applies to it.

Remarks

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

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

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

The tail suprema of any real sequence are nonincreasing in R\overline{\mathbb{R}}, so the limit superior exists for every sequence

Statement

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences), with tail ranges TnT_n and extended tail bounds sn=supTns_n = \sup T_n, in=infTni_n = \inf T_n as in 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}}.

  1. Monotonicity of the extended bounds under inclusion. If ABRA \subseteq B \subseteq \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) then supAsupBandinfBinfA,\sup A \le \sup B \qquad \text{and} \qquad \inf B \le \inf A, the four quantities being the extended bounds 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}. No hypothesis is placed on AA or BB; in particular AA may be empty.
  2. The tail bounds are monotone. TmTnT_m \subseteq T_n whenever nmn \le m, and hence smsnandinim(nm).s_m \le s_n \qquad \text{and} \qquad i_n \le i_m \qquad (n \le m). In particular sn+1sns_{n+1} \le s_n and inin+1i_n \le i_{n+1} for every nn, and insni_n \le s_n for every nn.
  3. Existence. lim supkxk\limsup_k x_k and lim infkxk\liminf_k x_k exist in R\overline{\mathbb{R}} for every sequence of reals, bounded or not.

Claim 1 is the tool the rest of this page uses whenever two extended suprema are compared. It is proved here, from the definition of a least upper bound, rather than quoted from the suprema page, for the reason given in the remarks below.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, its tail ranges Tn={xk:kn}T_n = \{x_k : k \ge n\}, and the extended bounds sn=supTns_n = \sup T_n, in=infTni_n = \inf T_n (Sequences of reals: bounded, eventually, frequently, tails, subsequences, 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}}).

[L1]

Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, with no hypothesis on the subset (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}).

[L2]

Least upper bound and greatest lower bound in a poset: supA\sup A is an upper bound of AA that is \le every upper bound of AA, and infA\inf A is a lower bound that is \ge every lower bound; each is unique when it exists (Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L4]

The order on N\mathbb{N} is total and transitive (Order on the natural numbers, \le is a linear order on N\mathbb{N}).

Proof

technique · direct
1.1

Let ABRA \subseteq B \subseteq \overline{\mathbb{R}} be arbitrary. By [L1] the four elements supA\sup A, supB\sup B, infA\inf A, infB\inf B of R\overline{\mathbb{R}} all exist and are uniquely determined.

givenL1L2
1.2

Let nmn \le m in N\mathbb{N}. Every element of TmT_m has the form xkx_k with kmk \ge m, and then knk \ge n by transitivity, so xkTnx_k \in T_n; hence TmTnT_m \subseteq T_n.

givenL4
1.3

For every nn the tail range TnT_n contains xnx_n, so inxni_n \le x_n because ini_n is a lower bound of TnT_n, and xnsnx_n \le s_n because sns_n is an upper bound of TnT_n; transitivity gives insni_n \le s_n.

givenL1L2L3
2.1

Since supB\sup B is an upper bound of BB and ABA \subseteq B, every element of AA is supB\le \sup B, so supB\sup B is an upper bound of AA; as supA\sup A is the least of the upper bounds of AA, this gives supAsupB\sup A \le \sup B. Dually infB\inf B is a lower bound of BB, hence of AA, and as infA\inf A is the greatest of the lower bounds of AA this gives infBinfA\inf B \le \inf A. Claim 1 is proved.

step 1.1L1L2
3.1

Applying claim 1 to the inclusion TmTnT_m \subseteq T_n valid for nmn \le m gives smsns_m \le s_n and inimi_n \le i_m; the special case m=n+1m = n + 1 gives sn+1sns_{n+1} \le s_n and inin+1i_n \le i_{n+1}. Together with insni_n \le s_n this is claim 2.

step 1.2step 1.3step 2.1
4.1

The families {sn:nN}\{s_n : n \in \mathbb{N}\} and {in:nN}\{i_n : n \in \mathbb{N}\} are subsets of R\overline{\mathbb{R}}, so [L1] applies to them with no hypothesis, and lim supkxk=inf{sn}\limsup_k x_k = \inf\{s_n\} and lim infkxk=sup{in}\liminf_k x_k = \sup\{i_n\} exist in R\overline{\mathbb{R}} for every sequence of reals. This is claim 3.

step 3.1L1L2

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

lim sup(xk)=lim inf(xk)\limsup(-x_k) = -\liminf(x_k), with the reflection of R\overline{\mathbb{R}} exchanging ±\pm\infty

Statement

Write A:={a:aA}-A := \{-a : a \in A\} for ARA \subseteq \overline{\mathbb{R}}, with the reflection of The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined, which fixes no point of {,+}\{-\infty, +\infty\} but exchanges the two.

  1. Reflection exchanges the extended bounds. For every ARA \subseteq \overline{\mathbb{R}}, sup(A)=infAandinf(A)=supA,\sup(-A) = -\inf A \qquad \text{and} \qquad \inf(-A) = -\sup A, with the bounds 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} and no hypothesis on AA.
  2. Reflection exchanges lim sup\limsup and lim inf\liminf. For every sequence (xk)(x_k) of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences), lim supk(xk)=lim infkxkandlim infk(xk)=lim supkxk,\limsup_{k}(-x_k) = -\liminf_{k} x_k \qquad \text{and} \qquad \liminf_{k}(-x_k) = -\limsup_{k} x_k, with lim sup\limsup and lim inf\liminf as in 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}}.

Claim 2 is what turns every statement about lim sup\limsup on this page into its dual about lim inf\liminf without a second proof, exactly as the identity infS=sup(S)\inf S = -\sup(-S) does in R\mathbb{R}. The novelty is only that the reflection now has to move the two new points, and it does: (+)=-(+\infty) = -\infty.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, the reflected sequence yk:=xky_k := -x_k, and for ARA \subseteq \overline{\mathbb{R}} the reflected set A={a:aA}-A = \{-a : a \in A\}.

[L1]

Reflection on R\overline{\mathbb{R}}: the map aaa \mapsto -a satisfies (a)=a-(-a) = a and aba \le b if and only if ba-b \le -a, for all a,bRa, b \in \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).

[L2]

Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, with no hypothesis on the subset (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}).

[L3]

Least upper bound and greatest lower bound in a poset, and their uniqueness (Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L4]

Tail ranges Tn={xk:kn}T_n = \{x_k : k \ge n\}, the extended tail bounds sn=supTns_n = \sup T_n and in=infTni_n = \inf T_n, and lim supkxk=inf{sn}\limsup_k x_k = \inf\{s_n\}, lim infkxk=sup{in}\liminf_k x_k = \sup\{i_n\} (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}}).

Proof

technique · direct
1.1

Let ARA \subseteq \overline{\mathbb{R}} be arbitrary. Since (a)=a-(-a) = a for every aa, the map aaa \mapsto -a carries AA onto A-A and A-A onto AA, so (A)=A-(-A) = A; and by [L2] each of supA\sup A, infA\inf A, sup(A)\sup(-A), inf(A)\inf(-A) exists.

givenL1L2
1.2

Let TnT_n and TnT'_n be the tail ranges of (xk)(x_k) and of (yk)=(xk)(y_k) = (-x_k). Since yk=xky_k = -x_k, the set Tn={yk:kn}T'_n = \{y_k : k \ge n\} is exactly Tn-T_n.

givenL4
2.1

The element infA-\inf A is an upper bound of A-A: for aAa \in A we have infAa\inf A \le a, hence ainfA-a \le -\inf A by [L1], and every element of A-A is such a a-a. If vv is any upper bound of A-A, then for aAa \in A we get av-a \le v, hence va-v \le a by [L1], so v-v is a lower bound of AA and therefore vinfA-v \le \inf A, which gives infAv-\inf A \le v by [L1] again. So infA-\inf A is the least upper bound of A-A, that is sup(A)=infA\sup(-A) = -\inf A.

step 1.1L1L2L3
3.1

Applying the identity just proved to the set A-A in place of AA, and using (A)=A-(-A) = A, gives supA=inf(A)\sup A = -\inf(-A); reflecting both sides and using (a)=a-(-a) = a yields inf(A)=supA\inf(-A) = -\sup A. Claim 1 is proved.

step 2.1step 1.1L1
4.1

By claim 1 applied to TnT_n, the nn-th tail supremum of (yk)(y_k) is supTn=sup(Tn)=in\sup T'_n = \sup(-T_n) = -i_n, and its nn-th tail infimum is inf(Tn)=sn\inf(-T_n) = -s_n.

step 1.2step 2.1step 3.1L4
5.1

Hence the family of tail suprema of (yk)(y_k) is {in:nN}={in:nN}\{-i_n : n \in \mathbb{N}\} = -\{i_n : n \in \mathbb{N}\}, so claim 1 applied to {in}\{i_n\} gives lim supk(xk)=inf({in})=sup{in}=lim infkxk\limsup_k(-x_k) = \inf\big(-\{i_n\}\big) = -\sup\{i_n\} = -\liminf_k x_k.

step 4.1step 3.1L4L5
6.1

The same identity applied to the sequence (yk)(y_k), whose reflection is (yk)=(xk)(-y_k) = (x_k) by [L1], reads lim supkxk=lim infk(xk)\limsup_k x_k = -\liminf_k(-x_k); reflecting both sides gives lim infk(xk)=lim supkxk\liminf_k(-x_k) = -\limsup_k x_k. Both parts of claim 2 are proved.

step 5.1L1

Remarks

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

lim infxklim supxk\liminf x_k \le \limsup x_k for every real sequence

Statement

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, its tail ranges Tn={xk:kn}T_n = \{x_k : k \ge n\}, and the extended tail bounds sn=supTns_n = \sup T_n, in=infTni_n = \inf T_n (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}}).

[L1]

Every subset of R\overline{\mathbb{R}} has a least upper bound and a greatest lower bound in R\overline{\mathbb{R}}, an upper bound below every upper bound and a lower bound above every lower bound respectively (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}, Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L2]

Monotonicity of the tail bounds: smsns_m \le s_n and inimi_n \le i_m whenever nmn \le m, and insni_n \le s_n for every nn; both lim supkxk=inf{sn}\limsup_k x_k = \inf\{s_n\} and lim infkxk=sup{in}\liminf_k x_k = \sup\{i_n\} exist (The tail suprema of any real sequence are nonincreasing in R\overline{\mathbb{R}}, so the limit superior exists for every sequence, 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}}).

Proof

technique · direct
1.1

Let m,nNm, n \in \mathbb{N} be arbitrary. The order on N\mathbb{N} is total, so either mnm \le n or nmn \le m; let pp be whichever of mm and nn is the larger, so that mpm \le p and npn \le p.

givenL3choose
2.1

Monotonicity of the tail bounds gives imipi_m \le i_p and spsns_p \le s_n, and ipspi_p \le s_p holds because TpT_p is nonempty; chaining these by transitivity yields imsni_m \le s_n. As mm and nn were arbitrary, every tail infimum is below every tail supremum.

step 1.1L2L4
3.1

Fix nNn \in \mathbb{N}. By step 2.1 the element sns_n is an upper bound of the family {im:mN}\{i_m : m \in \mathbb{N}\}, and lim infkxk\liminf_k x_k is its least upper bound, so lim infkxksn\liminf_k x_k \le s_n.

step 2.1L1L2
4.1

Since nn was arbitrary, lim infkxk\liminf_k x_k is a lower bound of the family {sn:nN}\{s_n : n \in \mathbb{N}\}, and lim supkxk\limsup_k x_k is its greatest lower bound, so lim infkxklim supkxk\liminf_k x_k \le \limsup_k x_k.

step 3.1L1L2

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently

Statement

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and let LRL \in \mathbb{R}, with eventually and frequently as in Sequences of reals: bounded, eventually, frequently, tails, subsequences and lim sup\limsup, lim inf\liminf as in 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}}.

  1. L=lim supkxkL = \limsup_{k} x_k if and only if for every real ε>0\varepsilon > 0 xk<L+ε  eventuallyandxk>Lε  frequently.x_k < L + \varepsilon \ \text{ eventually} \qquad \text{and} \qquad x_k > L - \varepsilon \ \text{ frequently}.
  2. Dually, L=lim infkxkL = \liminf_{k} x_k if and only if for every real ε>0\varepsilon > 0 xk>Lε  eventuallyandxk<L+ε  frequently.x_k > L - \varepsilon \ \text{ eventually} \qquad \text{and} \qquad x_k < L + \varepsilon \ \text{ frequently}.

The hypothesis LRL \in \mathbb{R} is not a restriction that can be lifted. Both conditions are stated with real ε\varepsilon and real L±εL \pm \varepsilon, so neither has a reading at L=±L = \pm\infty; the infinite cases are handled instead by the convergence theorem later on this page. What the lemma does say is that whenever lim supkxk\limsup_k x_k happens to be a real number, it is pinned down by the familiar two-sided test: nothing exceeds it by a fixed positive amount from some index on, and something comes within any fixed positive amount of it arbitrarily late.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, a real number LL, the tail ranges Tn={xk:kn}T_n = \{x_k : k \ge n\}, the extended tail suprema sn=supTns_n = \sup T_n, and Λ:=lim supkxk=inf{sn:nN}\Lambda := \limsup_k x_k = \inf\{s_n : n \in \mathbb{N}\} (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}}).

[L2]

The order on R\overline{\mathbb{R}} is total, so the failure of aba \le b is b<ab < a; it restricts on R\mathbb{R} to the order of R\mathbb{R}; and every real number is <+< +\infty and >> -\infty (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined, Partial order and partially ordered set).

[L3]

A property PP of indices holds eventually when it holds for all kKk \ge K for some KK, and frequently when for every KK it holds for some kKk \ge K (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L5]

Order arithmetic in R\mathbb{R}: for ε>0\varepsilon > 0 one has Lε<L<L+εL - \varepsilon < L < L + \varepsilon, and a<ba < b if and only if b<a-b < -a, both by translation invariance; the order is total, so exactly one of a<ba < b, a=ba = b, b<ab < a holds and a<aa < a is impossible (Order is preserved by adding a constant and by adding inequalities, Ordered field, Complete ordered field (least-upper-bound property)).

[L6]

Reflection exchanges the two quantities: lim supk(xk)=lim infkxk\limsup_k(-x_k) = -\liminf_k x_k and lim infk(xk)=lim supkxk\liminf_k(-x_k) = -\limsup_k x_k (lim sup(xk)=lim inf(xk)\limsup(-x_k) = -\liminf(x_k), with the reflection of R\overline{\mathbb{R}} exchanging ±\pm\infty).

Proof

technique · direct
1.1

For the forward implication of claim 1, assume L=ΛL = \Lambda and let ε>0\varepsilon > 0 be an arbitrary real.

assume-hypL1
1.2

For the converse implication of claim 1, assume that for every real ε>0\varepsilon > 0 the sequence satisfies xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently.

assume-hypL3
2.1

Under the assumption of step 1.1, L+ε>L=ΛL + \varepsilon > L = \Lambda, so L+εL + \varepsilon is not a lower bound of {sn}\{s_n\}, since Λ\Lambda is the greatest lower bound; by totality there is nn with sn<L+εs_n < L + \varepsilon. For every knk \ge n we have xksnx_k \le s_n, hence xk<L+εx_k < L + \varepsilon; so xk<L+εx_k < L + \varepsilon eventually.

step 1.1L1L2L3L5
2.2

Under the assumption of step 1.1, fix nNn \in \mathbb{N}. Then Λsn\Lambda \le s_n because Λ\Lambda is a lower bound of {sn}\{s_n\}, and Lε<L=ΛL - \varepsilon < L = \Lambda, so Lε<snL - \varepsilon < s_n. Hence LεL - \varepsilon is not an upper bound of TnT_n, for an upper bound uu of TnT_n satisfies snus_n \le u; by totality of the order on R\mathbb{R} there is therefore knk \ge n with xk>Lεx_k > L - \varepsilon. As nn was arbitrary, xk>Lεx_k > L - \varepsilon frequently.

step 1.1L1L2L3L5
2.3

Under the assumption of step 1.2, let ε>0\varepsilon > 0 be a real and take NN with xk<L+εx_k < L + \varepsilon for all kNk \ge N. Then L+εL + \varepsilon is an upper bound of TNT_N, so sNL+εs_N \le L + \varepsilon by leastness, and ΛsN\Lambda \le s_N because Λ\Lambda is a lower bound of {sn}\{s_n\}; hence ΛL+ε\Lambda \le L + \varepsilon.

step 1.2L1L2L3
2.4

Under the assumption of step 1.2, let ε>0\varepsilon > 0 be a real and fix nn. There is knk \ge n with xk>Lεx_k > L - \varepsilon, and xksnx_k \le s_n, so Lε<snL - \varepsilon < s_n and in particular LεsnL - \varepsilon \le s_n. As nn was arbitrary, LεL - \varepsilon is a lower bound of {sn}\{s_n\}, so LεΛL - \varepsilon \le \Lambda by greatest-lower-boundedness.

step 1.2L1L2L3
3.1

Taking ε=1\varepsilon = 1 in steps 2.3 and 2.4 gives L1ΛL+1L - 1 \le \Lambda \le L + 1 with L±1L \pm 1 real, so Λ\Lambda is neither ++\infty nor -\infty and is therefore a real number. Suppose Λ>L\Lambda > L and put δ:=ΛL>0\delta := \Lambda - L > 0; choosing a natural m1m \ge 1 with 1/m<δ1/m < \delta and applying step 2.3 with ε=1/m\varepsilon = 1/m gives ΛL+1/m<L+δ=Λ\Lambda \le L + 1/m < L + \delta = \Lambda, which is impossible. Suppose instead Λ<L\Lambda < L and put δ:=LΛ>0\delta := L - \Lambda > 0; choosing m1m \ge 1 with 1/m<δ1/m < \delta and applying step 2.4 with ε=1/m\varepsilon = 1/m gives L1/mΛL - 1/m \le \Lambda, that is δ=LΛ1/m<δ\delta = L - \Lambda \le 1/m < \delta, again impossible. By trichotomy Λ=L\Lambda = L.

step 2.3step 2.4L2L4L5
4.1

Steps 2.1 and 2.2 prove the forward implication of claim 1 and step 3.1 proves its converse, so claim 1 holds.

step 2.1step 2.2step 3.1
5.1

For claim 2, note that L=lim infkxkL = \liminf_k x_k holds exactly when L=lim infkxk=lim supk(xk)-L = -\liminf_k x_k = \limsup_k(-x_k), since negation is injective on R\overline{\mathbb{R}}. Applying claim 1 to the sequence (xk)(-x_k) and the real number L-L, that holds exactly when for every real ε>0\varepsilon > 0 one has xk<L+ε-x_k < -L + \varepsilon eventually and xk>Lε-x_k > -L - \varepsilon frequently. Negating each of the two inequalities reverses it, turning them into xk>Lεx_k > L - \varepsilon eventually and xk<L+εx_k < L + \varepsilon frequently, which is claim 2.

step 4.1L5L6

Remarks

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

A real sequence converges to LRL \in \mathbb{R} iff lim infxk=lim supxk=L\liminf x_k = \limsup x_k = L, and diverges to ±\pm\infty iff both equal ±\pm\infty

Statement

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences), with lim sup\limsup and lim inf\liminf as in 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}}.

  1. For LRL \in \mathbb{R}: (xk)(x_k) converges to LL (Limits and Cauchy sequences of reals) if and only if lim infkxk=lim supkxk=L\liminf_k x_k = \limsup_k x_k = L.
  2. xk+x_k \to +\infty (Divergence to ++\infty and to -\infty) if and only if lim infkxk=lim supkxk=+\liminf_k x_k = \limsup_k x_k = +\infty. Moreover lim infkxk=+\liminf_k x_k = +\infty on its own already forces lim supkxk=+\limsup_k x_k = +\infty.
  3. xkx_k \to -\infty if and only if lim infkxk=lim supkxk=\liminf_k x_k = \limsup_k x_k = -\infty, and lim supkxk=\limsup_k x_k = -\infty on its own already forces lim infkxk=\liminf_k x_k = -\infty.

The three clauses combine into one statement about the extended line: for LRL \in \overline{\mathbb{R}}, the sequence (xk)(x_k) converges to LL in R\overline{\mathbb{R}} (Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty) if and only if

lim infkxk=lim supkxk=L.\liminf_{k} x_k = \limsup_{k} x_k = L .

Since lim infkxklim supkxk\liminf_k x_k \le \limsup_k x_k always (lim infxklim supxk\liminf x_k \le \limsup x_k for every real sequence), the single equation lim infkxk=lim supkxk\liminf_k x_k = \limsup_k x_k is therefore equivalent to convergence in R\overline{\mathbb{R}}, and the common value is the limit. A sequence that neither converges nor diverges to ±\pm\infty is exactly one for which the inequality is strict.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, its tail ranges Tn={xk:kn}T_n = \{x_k : k \ge n\}, the extended tail bounds sn=supTns_n = \sup T_n and in=infTni_n = \inf T_n, and the quantities lim supkxk=inf{sn}\limsup_k x_k = \inf\{s_n\}, lim infkxk=sup{in}\liminf_k x_k = \sup\{i_n\} (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}}).

[L1]

All of sns_n, ini_n, lim supkxk\limsup_k x_k and lim infkxk\liminf_k x_k exist in R\overline{\mathbb{R}} for every sequence; ini_n is the greatest lower bound of TnT_n and lim infkxk\liminf_k x_k the least upper bound of {in}\{i_n\}, with the dual descriptions for sns_n and lim supkxk\limsup_k x_k (The tail suprema of any real sequence are nonincreasing in R\overline{\mathbb{R}}, so the limit superior exists for every sequence, 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}, Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L2]

The order on R\overline{\mathbb{R}} is total, so the failure of aba \le b is b<ab < a; it restricts on R\mathbb{R} to the order of R\mathbb{R}; ++\infty is the greatest element and -\infty the least; and every real is <+< +\infty and >> -\infty (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined, Partial order and partially ordered set).

[L3]

Epsilon characterisation, for a real LL: L=lim supkxkL = \limsup_k x_k exactly when for every real ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently; and L=lim infkxkL = \liminf_k x_k exactly when for every real ε>0\varepsilon > 0 one has xk>Lεx_k > L - \varepsilon eventually and xk<L+εx_k < L + \varepsilon frequently (For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently).

[L4]

lim infkxklim supkxk\liminf_k x_k \le \limsup_k x_k (lim infxklim supxk\liminf x_k \le \limsup x_k for every real sequence).

[L5]

Reflection: lim supk(xk)=lim infkxk\limsup_k(-x_k) = -\liminf_k x_k and lim infk(xk)=lim supkxk\liminf_k(-x_k) = -\limsup_k x_k (lim sup(xk)=lim inf(xk)\limsup(-x_k) = -\liminf(x_k), with the reflection of R\overline{\mathbb{R}} exchanging ±\pm\infty). Also xkx_k \to -\infty if and only if xk+-x_k \to +\infty: the condition xk<Mx_k < M for all kKk \ge K is equivalent to xk>M-x_k > -M for all kKk \ge K by order reversal, and MM runs over all reals exactly when M-M does (Divergence to ++\infty and to -\infty); the order reversal used here is strict, and the form stated in Order is preserved by adding a constant and by adding inequalities is likewise strict, so nothing nonstrict is being borrowed from it.

[L6]

Convergence to a real LL means: for every rational ε>0\varepsilon > 0 there is KK with xkL<ε|x_k - L| < \varepsilon for all kKk \ge K; and the same relation is obtained by testing every real ε>0\varepsilon > 0 instead, since below any positive real lies a positive rational (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences, The rationals embed densely in the reals).

[L7]

Divergence: xk+x_k \to +\infty means that for every real MM there is KK with xk>Mx_k > M for all kKk \ge K (Divergence to ++\infty and to -\infty).

[L8]

Eventually and frequently, and the fact that a property holding eventually holds frequently, since indices beyond any two given thresholds exist by totality of the order on N\mathbb{N}; likewise two properties each holding eventually hold together from the larger threshold on (Sequences of reals: bounded, eventually, frequently, tails, subsequences, \le is a linear order on N\mathbb{N}).

[L9]

Absolute value: for c>0c > 0, a<c|a| < c if and only if c<a<c-c < a < c (Basic properties of the absolute value).

[L10]

Order arithmetic in R\mathbb{R}: 0<10 < 1, so t<t+1t < t + 1 for every real tt, and no real is above every real; adding a constant preserves the order (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1

For the forward implication of claim 1, assume LRL \in \mathbb{R} and that (xk)(x_k) converges to LL.

assume-hypL6
1.2

For the converse implication of claim 1, assume LRL \in \mathbb{R} and lim infkxk=lim supkxk=L\liminf_k x_k = \limsup_k x_k = L.

assume-hypL1
1.3

For the forward implication of claim 2, assume xk+x_k \to +\infty.

assume-hypL7
1.4

For the converse implication of claim 2, assume lim infkxk=+\liminf_k x_k = +\infty.

assume-hypL1
2.1

Under the assumption of step 1.1, let ε>0\varepsilon > 0 be an arbitrary real. Testing convergence at ε\varepsilon gives KK with xkL<ε|x_k - L| < \varepsilon, hence Lε<xk<L+εL - \varepsilon < x_k < L + \varepsilon, for all kKk \ge K. So xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon eventually, and each of the two therefore also holds frequently. Both halves of each characterisation in [L3] are met, so lim supkxk=L\limsup_k x_k = L and lim infkxk=L\liminf_k x_k = L.

step 1.1L3L6L8L9
2.2

Under the assumption of step 1.2, let ε>0\varepsilon > 0 be an arbitrary real. The forward halves of the two characterisations in [L3] give xk<L+εx_k < L + \varepsilon for all kk beyond some K1K_1 and xk>Lεx_k > L - \varepsilon for all kk beyond some K2K_2; beyond the larger of K1K_1 and K2K_2 both hold, so xkL<ε|x_k - L| < \varepsilon there. This holds for every real ε>0\varepsilon > 0, in particular for every rational one, so (xk)(x_k) converges to LL.

step 1.2L3L6L8L9
2.3

Under the assumption of step 1.3, let MM be an arbitrary real and take KK with xk>Mx_k > M for all kKk \ge K. Then MM is a lower bound of TKT_K, so MiKM \le i_K, and iKlim infkxki_K \le \liminf_k x_k because lim infkxk\liminf_k x_k is an upper bound of {in}\{i_n\}; hence Mlim infkxkM \le \liminf_k x_k. Since MM was an arbitrary real, lim infkxk\liminf_k x_k is not -\infty, which lies below every real, and it is not a real tt either, since M=t+1M = t + 1 would give t+1tt + 1 \le t. So lim infkxk=+\liminf_k x_k = +\infty.

step 1.3L1L2L7L10
2.4

Under the assumption of step 1.4, let MM be an arbitrary real. Since sup{in}=+\sup\{i_n\} = +\infty and M<+M < +\infty, the real MM is not an upper bound of {in}\{i_n\}, for otherwise the least upper bound would satisfy +M+\infty \le M; by totality there is nn with in>Mi_n > M. Every knk \ge n satisfies xkin>Mx_k \ge i_n > M, so xk>Mx_k > M eventually. As MM was arbitrary, xk+x_k \to +\infty.

step 1.4L1L2L7
3.1

Steps 2.1 and 2.2 are the two implications of claim 1.

step 2.1step 2.2L3
3.2

For claim 2: if xk+x_k \to +\infty then lim infkxk=+\liminf_k x_k = +\infty by step 2.3, and then +=lim infkxklim supkxk+\infty = \liminf_k x_k \le \limsup_k x_k forces lim supkxk=+\limsup_k x_k = +\infty since ++\infty is the greatest element; conversely if lim infkxk=lim supkxk=+\liminf_k x_k = \limsup_k x_k = +\infty then in particular lim infkxk=+\liminf_k x_k = +\infty and step 2.4 gives xk+x_k \to +\infty. The same use of [L4] is the additional assertion that lim infkxk=+\liminf_k x_k = +\infty alone forces lim supkxk=+\limsup_k x_k = +\infty.

step 2.3step 2.4L2L4
4.1

For claim 3, reflection gives xkx_k \to -\infty exactly when xk+-x_k \to +\infty, which by claim 2 holds exactly when lim infk(xk)=lim supk(xk)=+\liminf_k(-x_k) = \limsup_k(-x_k) = +\infty, that is lim supkxk=lim infkxk=+-\limsup_k x_k = -\liminf_k x_k = +\infty, that is lim supkxk=lim infkxk=\limsup_k x_k = \liminf_k x_k = -\infty; and lim supkxk=\limsup_k x_k = -\infty alone forces lim infkxk\liminf_k x_k \le -\infty, hence lim infkxk=\liminf_k x_k = -\infty, since -\infty is least. Claims 1, 2 and 3 together say that for LRL \in \overline{\mathbb{R}} the sequence converges to LL in R\overline{\mathbb{R}} exactly when lim infkxk=lim supkxk=L\liminf_k x_k = \limsup_k x_k = L, since the three clauses of that definition are convergence to a real LL, divergence to ++\infty and divergence to -\infty.

step 3.1step 3.2L2L4L5

Remarks

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

The limit superior is itself a subsequential limit in R\overline{\mathbb{R}} and is the greatest one

Statement

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and write Λ:=lim supkxkR\Lambda := \limsup_{k} x_k \in \overline{\mathbb{R}} (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}}). Then, with the extended subsequential limit set SL(x)\overline{\operatorname{SL}}(x) of Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty:

  1. ΛSL(x)\Lambda \in \overline{\operatorname{SL}}(x): there is a strictly increasing n:NNn : \mathbb{N} \to \mathbb{N} such that (xnj)(x_{n_j}) converges to Λ\Lambda in R\overline{\mathbb{R}};
  2. LΛL \le \Lambda for every LSL(x)L \in \overline{\operatorname{SL}}(x).

So SL(x)\overline{\operatorname{SL}}(x) is nonempty and has a greatest element, and that element is lim supkxk\limsup_k x_k. In particular every sequence of reals whatever has a subsequence that converges in R\overline{\mathbb{R}}.

The extended set is the right home for this statement, and the real set is not. The finite subsequential limit set SL(x)\operatorname{SL}(x) of Subsequential limit of a real sequence, and the subsequential limit set may be empty, and when it is not it may have a greatest element different from lim supkxk\limsup_k x_k; both failures are exhibited by the dedicated counterexample on the companion page. What is true for SL(x)\operatorname{SL}(x) follows: when Λ\Lambda is a real number, claim 1 puts it in SL(x)\operatorname{SL}(x), since the two sets agree on R\mathbb{R} (Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty), and claim 2 then makes it the greatest element there too.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, its tail ranges Tn={xk:kn}T_n = \{x_k : k \ge n\}, the extended tail suprema sn=supTns_n = \sup T_n, and Λ:=lim supkxk=inf{sn:nN}\Lambda := \limsup_k x_k = \inf\{s_n : n \in \mathbb{N}\} (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}}).

[L2]

The order on R\overline{\mathbb{R}} is total, so the failure of aba \le b is b<ab < a; -\infty is least and ++\infty greatest; every real is <+< +\infty and >> -\infty; and on R\mathbb{R} the order is that of R\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, Partial order and partially ordered set).

[L3]

Epsilon characterisation for a real Λ\Lambda: for every real η>0\eta > 0 one has xk<Λ+ηx_k < \Lambda + \eta eventually and xk>Ληx_k > \Lambda - \eta frequently (For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently).

[L4]

Recursion theorem: for a set AA, an element aAa \in A and a function f:AAf : A \to A there is a unique g:NAg : \mathbb{N} \to A with g0=ag_0 = a and gj+1=f(gj)g_{j+1} = f(g_j) (The recursion theorem).

[L5]

Well-ordering principle: every nonempty subset of N\mathbb{N} has a least element (The well-ordering principle).

[L6]

Index maps: if nj<nj+1n_j < n_{j+1} for every jj then nn is strictly increasing, and then njjn_j \ge j for every jj; the composite (xnj)(x_{n_j}) is a subsequence (A strictly increasing index map satisfies nkkn_k \ge k, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L7]

Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set (Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty); convergence to a real, for which it suffices to produce a threshold for every real ε>0\varepsilon > 0 (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences); divergence to ±\pm\infty (Divergence to ++\infty and to -\infty); and ab<c|a - b| < c if and only if bc<a<b+cb - c < a < b + c for c>0c > 0 (Basic properties of the absolute value).

[L9]

Limits preserve non-strict inequalities: if yjcy_j \le c for all large jj and yjyy_j \to y in R\mathbb{R}, then ycy \le c (Limits preserve non-strict inequalities).

[L10]

Archimedean facts: for every real MM there is a natural p1p \ge 1 with M<p1RM < p \cdot 1_{\mathbb{R}}, and for every real η>0\eta > 0 a natural m1m \ge 1 with 1/m<η1/m < \eta; the canonical naturals satisfy 0n1R0 \le n \cdot 1_{\mathbb{R}} and are increasing in nn, and 0<ab0 < a \le b gives 0<1/b1/a0 < 1/b \le 1/a (Every complete ordered field is Archimedean, For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order).

[L11]

Strictly between any two reals lies a rational, hence a real (The rationals embed densely in the reals).

[L12]

The order on N\mathbb{N} is total and transitive, so any two indices have a common upper bound (Order on the natural numbers, \le is a linear order on N\mathbb{N}).

Proof

technique · constructive
1.1

The element Λ=lim supkxk\Lambda = \limsup_k x_k exists in R\overline{\mathbb{R}}, and exactly one of the following holds: Λ\Lambda is a real number, Λ=+\Lambda = +\infty, or Λ=\Lambda = -\infty.

givenL1L2
1.2

Suppose Λ=+\Lambda = +\infty. Since Λ\Lambda is a lower bound of {sn}\{s_n\}, every nn has +sn+\infty \le s_n and so sn=+s_n = +\infty. Consequently, for every nNn \in \mathbb{N} and every real MM there is knk \ge n with xk>Mx_k > M: otherwise MM would be an upper bound of TnT_n and leastness would give snMs_n \le M, contradicting M<+M < +\infty.

givenL1L2
1.3

Suppose Λ\Lambda is real. Then for every nNn \in \mathbb{N} and every real η>0\eta > 0 there is knk \ge n with xkΛ<η|x_k - \Lambda| < \eta: by [L3] fix KK with xk<Λ+ηx_k < \Lambda + \eta for all kKk \ge K, let KK' be an index at least as large as both nn and KK, and use that xk>Ληx_k > \Lambda - \eta frequently to obtain kKk \ge K' with xk>Ληx_k > \Lambda - \eta; that kk satisfies kKk \ge K, hence also xk<Λ+ηx_k < \Lambda + \eta, and knk \ge n.

givenL3L7L12
1.4

Suppose Λ=\Lambda = -\infty. Then xkx_k \to -\infty by [L8], and the identity map jjj \mapsto j is strictly increasing, so the subsequence (xj)(x_j) of (xk)(x_k) converges to -\infty in R\overline{\mathbb{R}} and ΛSL(x)\Lambda \in \overline{\operatorname{SL}}(x).

givenL6L7L8
1.5

Let LSL(x)L \in \overline{\operatorname{SL}}(x) be arbitrary and fix a strictly increasing n:NNn : \mathbb{N} \to \mathbb{N} such that (xnj)(x_{n_j}) converges to LL in R\overline{\mathbb{R}}; then njjn_j \ge j for every jj.

givenL6L7
2.1

In the case Λ=+\Lambda = +\infty, define f:NNf : \mathbb{N} \to \mathbb{N} by letting f(n)f(n) be the least element of En:={kN:k>n and xk>n1R}E_n := \{\, k \in \mathbb{N} : k > n \text{ and } x_k > n \cdot 1_{\mathbb{R}} \,\}, which is nonempty by step 1.2 applied with the index n+1n+1 and the real M=n1RM = n \cdot 1_{\mathbb{R}}, and let aa be the least element of {k:xk>0}\{\, k : x_k > 0 \,\}, nonempty by step 1.2 with n=0n = 0 and M=0M = 0. Then f(n)>nf(n) > n and xf(n)>n1Rx_{f(n)} > n \cdot 1_{\mathbb{R}} for every nn.

step 1.2L5construct
2.2

In the case Λ\Lambda real, define g:NNg : \mathbb{N} \to \mathbb{N} by letting g(n)g(n) be the least element of Fn:={kN:k>n and xkΛ<1/(n+1)}F_n := \{\, k \in \mathbb{N} : k > n \text{ and } |x_k - \Lambda| < 1/(n+1) \,\}, which is nonempty by step 1.3 applied with the index n+1n+1 and η=1/(n+1)>0\eta = 1/(n+1) > 0, and let bb be the least element of {k:xkΛ<1}\{\, k : |x_k - \Lambda| < 1 \,\}, nonempty by step 1.3 with n=0n = 0 and η=1\eta = 1. Then g(n)>ng(n) > n and xg(n)Λ<1/(n+1)|x_{g(n)} - \Lambda| < 1/(n+1) for every nn.

step 1.3L5L10construct
2.3

If L=L = -\infty then LΛL \le \Lambda, since -\infty is the least element of R\overline{\mathbb{R}}.

step 1.5L2
2.4

If L=+L = +\infty, then for every real MM there is JJ with xnj>Mx_{n_j} > M for all jJj \ge J. Fix nNn \in \mathbb{N} and a real MM, and take jj at least as large as both JJ and nn; then njjnn_j \ge j \ge n, so xnjTnx_{n_j} \in T_n and M<xnjsnM < x_{n_j} \le s_n. As MM was an arbitrary real, sns_n is neither real nor -\infty, so sn=+s_n = +\infty; as nn was arbitrary, Λ=inf{sn}=+\Lambda = \inf\{s_n\} = +\infty and LΛL \le \Lambda.

step 1.5L1L2L7L12
2.5

If LL is real, suppose for the sake of the comparison that Λ<L\Lambda < L. By step 1.1 the element Λ\Lambda is then real or -\infty; choose a real cc with Λ<c<L\Lambda < c < L, taking a rational strictly between Λ\Lambda and LL in the first case and c:=L1c := L - 1 in the second. Since Λ\Lambda is the greatest lower bound of {sn}\{s_n\} and Λ<c\Lambda < c, the element cc is not a lower bound, so there is nn with sn<cs_n < c, and then xksn<cx_k \le s_n < c for every knk \ge n. For jnj \ge n we have njjnn_j \ge j \ge n, hence xnjcx_{n_j} \le c, so LcL \le c by [L9], contradicting c<Lc < L. By totality LΛL \le \Lambda.

step 1.5step 1.1L1L2L9L11
3.1

In the case Λ=+\Lambda = +\infty, the recursion theorem applied to N\mathbb{N}, the element aa and the function ff gives n:NNn : \mathbb{N} \to \mathbb{N} with n0=an_0 = a and nj+1=f(nj)n_{j+1} = f(n_j). Then nj<nj+1n_j < n_{j+1} for every jj, so nn is strictly increasing and njjn_j \ge j; and xnj+1>nj1Rj1Rx_{n_{j+1}} > n_j \cdot 1_{\mathbb{R}} \ge j \cdot 1_{\mathbb{R}} for every jj.

step 2.1L4L6L10
3.2

In the case Λ\Lambda real, the recursion theorem applied to N\mathbb{N}, the element bb and the function gg gives n:NNn : \mathbb{N} \to \mathbb{N} with n0=bn_0 = b and nj+1=g(nj)n_{j+1} = g(n_j). Then nn is strictly increasing with njjn_j \ge j, and xnj+1Λ<1/(nj+1)1/(j+1)|x_{n_{j+1}} - \Lambda| < 1/(n_j + 1) \le 1/(j+1) for every jj.

step 2.2L4L6L10
4.1

In the case Λ=+\Lambda = +\infty, the subsequence (xnj)(x_{n_j}) diverges to ++\infty: given a real MM, take a natural p1p \ge 1 with M<p1RM < p \cdot 1_{\mathbb{R}}; every jp+1j \ge p + 1 satisfies j1pj - 1 \ge p, so step 3.1 applied at j1j - 1 gives xnj>(j1)1Rp1R>Mx_{n_j} > (j-1) \cdot 1_{\mathbb{R}} \ge p \cdot 1_{\mathbb{R}} > M. Hence (xnj)(x_{n_j}) converges to +=Λ+\infty = \Lambda in R\overline{\mathbb{R}} and ΛSL(x)\Lambda \in \overline{\operatorname{SL}}(x).

step 3.1L7L10L12
4.2

In the case Λ\Lambda real, the subsequence (xnj)(x_{n_j}) converges to Λ\Lambda: given a real ε>0\varepsilon > 0, take a natural m1m \ge 1 with 1/m<ε1/m < \varepsilon; every jmj \ge m satisfies j1j \ge 1, so step 3.2 applied at j1j - 1 gives xnjΛ<1/j1/m<ε|x_{n_j} - \Lambda| < 1/j \le 1/m < \varepsilon. Producing such a threshold for every real ε>0\varepsilon > 0 establishes convergence, so (xnj)(x_{n_j}) converges to Λ\Lambda in R\overline{\mathbb{R}} and ΛSL(x)\Lambda \in \overline{\operatorname{SL}}(x).

step 3.2L7L10
5.1

The three cases of step 1.1 are exhaustive, and each produces a subsequence converging to Λ\Lambda in R\overline{\mathbb{R}}: step 4.1 when Λ=+\Lambda = +\infty, step 4.2 when Λ\Lambda is real, and step 1.4 when Λ=\Lambda = -\infty. So ΛSL(x)\Lambda \in \overline{\operatorname{SL}}(x), which is claim 1.

step 4.1step 4.2step 1.4L7
6.1

Steps 2.3, 2.4 and 2.5 cover the three possibilities for an arbitrary LSL(x)L \in \overline{\operatorname{SL}}(x) and give LΛL \le \Lambda in each, which is claim 2. With claim 1 this makes SL(x)\overline{\operatorname{SL}}(x) nonempty with greatest element Λ=lim supkxk\Lambda = \limsup_k x_k.

step 5.1step 2.3step 2.4step 2.5L2discharge-construct

Remarks

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

The limit inferior is the least subsequential limit in R\overline{\mathbb{R}}

Statement

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences). Then lim infkxkSL(x)\liminf_{k} x_k \in \overline{\operatorname{SL}}(x) and lim infkxkL\liminf_{k} x_k \le L for every LSL(x)L \in \overline{\operatorname{SL}}(x) (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}}, Convergence in R\overline{\mathbb{R}} and the extended subsequential limit set: LRL \in \overline{\mathbb{R}} is an extended subsequential limit when some subsequence converges to LL, or diverges to L=±L = \pm\infty).

So the extended subsequential limit set of any real sequence has a least element as well as a greatest one, and the two are lim infkxk\liminf_k x_k and lim supkxk\limsup_k x_k respectively (The limit superior is itself a subsequential limit in R\overline{\mathbb{R}} and is the greatest one). Every extended subsequential limit lies between them.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals, and its reflection yk:=xky_k := -x_k.

[L1]

Reflection on R\overline{\mathbb{R}}: aaa \mapsto -a satisfies (a)=a-(-a) = a and aba \le b if and only if ba-b \le -a (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined).

[L3]

For every real sequence the extended subsequential limit set is nonempty and has greatest element the limit superior (The limit superior is itself a subsequential limit in R\overline{\mathbb{R}} and is the greatest one).

[L5]

Scalar multiples of convergent sequences: zjzz_j \to z in R\mathbb{R} implies czjczc z_j \to c z (Algebra of limits: sums, scalar multiples, products and quotients).

[L6]

Divergence to ±\pm\infty, and order reversal: zj>Mz_j > M is equivalent to zj<M-z_j < -M, and MM runs over all reals exactly when M-M does (Divergence to ++\infty and to -\infty, Order is preserved by adding a constant and by adding inequalities).

Proof

technique · direct
1.1

Put yk:=xky_k := -x_k, a sequence of reals; then yk=xk-y_k = x_k for every kk, by the involution property of the reflection.

givenL1L4
1.2

Let LRL \in \overline{\mathbb{R}} and let n:NNn : \mathbb{N} \to \mathbb{N} be strictly increasing with (xnj)(x_{n_j}) converging to LL in R\overline{\mathbb{R}}.

givenL4
1.3

By [L3] applied to the sequence (yk)(y_k), the set SL(y)\overline{\operatorname{SL}}(y) is nonempty and has greatest element N0:=lim supkykN_0 := \limsup_k y_k, and N0=lim infkxkN_0 = -\liminf_k x_k by [L2].

givenL2L3L7
2.1

The reflected subsequence (ynj)=(xnj)(y_{n_j}) = (-x_{n_j}) converges to L-L in R\overline{\mathbb{R}}. If LL is real this is the scalar rule with c=1c = -1. If L=+L = +\infty then for every real MM there is JJ with xnj>Mx_{n_j} > M for all jJj \ge J, hence ynj<My_{n_j} < -M for all such jj; since M-M runs over all reals as MM does, ynj=Ly_{n_j} \to -\infty = -L. If L=L = -\infty the same argument with the inequalities exchanged gives ynj+=Ly_{n_j} \to +\infty = -L.

step 1.2L1L4L5L6
3.1

Hence LSL(x)L \in \overline{\operatorname{SL}}(x) implies LSL(y)-L \in \overline{\operatorname{SL}}(y), the same index map serving. Applying that implication to the sequence (yk)(y_k), whose reflection is (xk)(x_k), gives conversely that NSL(y)N \in \overline{\operatorname{SL}}(y) implies NSL(x)-N \in \overline{\operatorname{SL}}(x). So SL(x)={N:NSL(y)}\overline{\operatorname{SL}}(x) = \{\, -N : N \in \overline{\operatorname{SL}}(y) \,\}.

step 2.1step 1.1L1L4
4.1

Therefore N0SL(x)-N_0 \in \overline{\operatorname{SL}}(x), and N0=(lim infkxk)=lim infkxk-N_0 = -(-\liminf_k x_k) = \liminf_k x_k; and for any LSL(x)L \in \overline{\operatorname{SL}}(x) the element L-L lies in SL(y)\overline{\operatorname{SL}}(y), so LN0-L \le N_0 by maximality, whence lim infkxk=N0L\liminf_k x_k = -N_0 \le L by order reversal. Thus lim infkxk\liminf_k x_k is the least element of SL(x)\overline{\operatorname{SL}}(x).

step 3.1step 1.3L1L2

Remarks

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

If each yjy_j is a subsequential limit of (xk)(x_k) and yjyRy_j \to y \in \mathbb{R}, then yy is a subsequential limit of (xk)(x_k)

Statement

Let (xk)(x_k) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and let (yj)(y_j) be a sequence of reals with

Then ySL(x)y \in \operatorname{SL}(x).

In words: the subsequential limit set of a real sequence contains the limit of every convergent sequence of its own elements. When the topology of R\mathbb{R} arrives, that property is what it calls sequential closedness; that sequential closedness is in turn equivalent to closedness for subsets of R\mathbb{R} is a theorem there and not a matter of naming, and the half of that equivalence running from sequential closedness to closedness spends the axiom of countable choice. Here the property is stated and proved purely in terms of sequences, with no choice principle and no topological notion used or needed.

Facts & Assumptions

Given: A sequence (xk)(x_k) of reals; a sequence (yj)(y_j) of reals with yjSL(x)y_j \in \operatorname{SL}(x) for every jj; and a real yy with yjyy_j \to y.

[L1]

Subsequential limits and convergence: yjSL(x)y_j \in \operatorname{SL}(x) means that some strictly increasing m:NNm : \mathbb{N} \to \mathbb{N} has xmiyjx_{m_i} \to y_j; convergence of a sequence of reals is the rational-ε\varepsilon condition of Limits and Cauchy sequences of reals, and to establish convergence it suffices to produce a threshold for every real ε>0\varepsilon > 0, by the remark of Sequences of reals: bounded, eventually, frequently, tails, subsequences (Subsequential limit of a real sequence, and the subsequential limit set, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L2]

Index maps: a strictly increasing mm satisfies miim_i \ge i, and an index map with nj<nj+1n_j < n_{j+1} for every jj is strictly increasing (A strictly increasing index map satisfies nkkn_k \ge k).

[L3]

Well-ordering principle: every nonempty subset of N\mathbb{N} has a least element (The well-ordering principle).

[L4]

Recursion theorem: for a set AA, an element aAa \in A and f:AAf : A \to A there is a unique g:NAg : \mathbb{N} \to A with g0=ag_0 = a and gj+1=f(gj)g_{j+1} = f(g_j) (The recursion theorem).

[L5]

Absolute value and the triangle inequality: a+ba+b|a + b| \le |a| + |b|, and a<c|a| < c if and only if c<a<c-c < a < c for c>0c > 0 (The triangle inequality, Basic properties of the absolute value).

[L6]

Canonical naturals and reciprocals: for a natural q1q \ge 1 the element q1Rq \cdot 1_{\mathbb{R}} is positive and invertible, (2(n+1))1R=2((n+1)1R)\big(2(n+1)\big) \cdot 1_{\mathbb{R}} = 2 \big((n+1) \cdot 1_{\mathbb{R}}\big), and 0<ab0 < a \le b gives 0<1/b1/a0 < 1/b \le 1/a; moreover for every real η>0\eta > 0 there is a natural m1m \ge 1 with 1/m<η1/m < \eta (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean).

[L7]

The order on N\mathbb{N} is total, so any two indices have a common upper bound (Order on the natural numbers, \le is a linear order on N\mathbb{N}).

[L8]

Below every positive real lies a positive rational, which is how a convergence hypothesis stated for rational ε\varepsilon is instantiated at a real threshold (The rationals embed densely in the reals).

Proof

technique · constructive
1.1

For nNn \in \mathbb{N} put qn:=2(n+1)q_n := 2(n+1), a natural number 1\ge 1. Then qn1R=2((n+1)1R)>0q_n \cdot 1_{\mathbb{R}} = 2\big((n+1) \cdot 1_{\mathbb{R}}\big) > 0 is invertible, 1/qn>01/q_n > 0, and 1/qn+1/qn=2/qn=1/(n+1)1/q_n + 1/q_n = 2/q_n = 1/(n+1).

givenL6algebra
1.2

By hypothesis (yj)(y_j) converges to yy and every yjy_j lies in SL(x)\operatorname{SL}(x), so for each jj there is a strictly increasing mm with xmiyjx_{m_i} \to y_j.

givenL1
2.1

For every nNn \in \mathbb{N} there is k>nk > n with xky<1/(n+1)|x_k - y| < 1/(n+1). Indeed, take a rational ε1\varepsilon_1 with 0<ε1<1/qn0 < \varepsilon_1 < 1/q_n and instantiate the convergence yjyy_j \to y at ε1\varepsilon_1 to obtain an index JJ with yJy<ε1<1/qn|y_J - y| < \varepsilon_1 < 1/q_n. Since yJSL(x)y_J \in \operatorname{SL}(x), fix a strictly increasing mm with xmiyJx_{m_i} \to y_J, take a rational ε2\varepsilon_2 with 0<ε2<1/qn0 < \varepsilon_2 < 1/q_n and an index II with xmiyJ<ε2|x_{m_i} - y_J| < \varepsilon_2 for all iIi \ge I, and let ii be an index at least as large as both II and n+1n+1. Then k:=mik := m_i satisfies k=miin+1>nk = m_i \ge i \ge n + 1 > n and, by the triangle inequality applied to xky=(xkyJ)+(yJy)x_k - y = (x_k - y_J) + (y_J - y), xkyxkyJ+yJy<1/qn+1/qn=1/(n+1)|x_k - y| \le |x_k - y_J| + |y_J - y| < 1/q_n + 1/q_n = 1/(n+1).

step 1.1step 1.2L1L2L5L7L8
3.1

Define f:NNf : \mathbb{N} \to \mathbb{N} by letting f(n)f(n) be the least element of the set Gn:={kN:k>n and xky<1/(n+1)}G_n := \{\, k \in \mathbb{N} : k > n \text{ and } |x_k - y| < 1/(n+1) \,\}, which is nonempty by step 2.1. Then f(n)>nf(n) > n and xf(n)y<1/(n+1)|x_{f(n)} - y| < 1/(n+1) for every nn.

step 2.1L3construct
4.1

The recursion theorem applied to N\mathbb{N}, the element f(0)f(0) and the function ff gives n:NNn : \mathbb{N} \to \mathbb{N} with n0=f(0)n_0 = f(0) and nj+1=f(nj)n_{j+1} = f(n_j). Then nj<nj+1n_j < n_{j+1} for every jj, so nn is strictly increasing and njjn_j \ge j; moreover xnj+1y<1/(nj+1)1/(j+1)|x_{n_{j+1}} - y| < 1/(n_j + 1) \le 1/(j+1) for every jj, using that nj+1j+1n_j + 1 \ge j + 1.

step 3.1L2L4L6
5.1

The subsequence (xnj)(x_{n_j}) converges to yy: given a real ε>0\varepsilon > 0, take a natural m1m \ge 1 with 1/m<ε1/m < \varepsilon; every jmj \ge m satisfies j1j \ge 1, so step 4.1 applied at j1j - 1 gives xnjy<1/j1/m<ε|x_{n_j} - y| < 1/j \le 1/m < \varepsilon. Producing such a threshold for every real ε>0\varepsilon > 0 establishes convergence, and nn is strictly increasing, so ySL(x)y \in \operatorname{SL}(x).

step 4.1L1L2L6discharge-construct

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

If xkykx_k \le y_k eventually then lim supxklim supyk\limsup x_k \le \limsup y_k and lim infxklim infyk\liminf x_k \le \liminf y_k

Statement

Let (xk)(x_k) and (yk)(y_k) be sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with xkykx_k \le y_k eventually, that is for all kk from some index on. Then

lim supkxk    lim supkykandlim infkxk    lim infkyk\limsup_{k} x_k \;\le\; \limsup_{k} y_k \qquad \text{and} \qquad \liminf_{k} x_k \;\le\; \liminf_{k} y_k

in R\overline{\mathbb{R}} (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}}, The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined). No boundedness or convergence hypothesis is placed on either sequence.

Facts & Assumptions

Given: Sequences (xk)(x_k) and (yk)(y_k) of reals and an index KNK \in \mathbb{N} with xkykx_k \le y_k for every kKk \ge K; the tail ranges Tn(x)={xk:kn}T_n(x) = \{x_k : k \ge n\} and Tn(y)T_n(y), and the extended tail bounds sn(x)=supTn(x)s_n(x) = \sup T_n(x), in(x)=infTn(x)i_n(x) = \inf T_n(x) and likewise for yy (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}}).

[L1]

All tail bounds and both of lim sup\limsup, lim inf\liminf exist in R\overline{\mathbb{R}}; sns_n is the least upper bound of the tail range and ini_n its greatest lower bound; lim supkyk\limsup_k y_k is the greatest lower bound of {sn(y)}\{s_n(y)\} and lim infkyk\liminf_k y_k the least upper bound of {in(y)}\{i_n(y)\}; and smsns_m \le s_n, inimi_n \le i_m whenever nmn \le m (The tail suprema of any real sequence are nonincreasing in R\overline{\mathbb{R}}, so the limit superior exists for every sequence, 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}, Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L3]

A property holds eventually when it holds for all indices from some index on (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L4]

The order on N\mathbb{N} is total, so every nn satisfies nKn \ge K or n<Kn < K, and in the latter case nKn \le K (Order on the natural numbers, \le is a linear order on N\mathbb{N}).

Proof

technique · direct
1.1

By hypothesis fix KNK \in \mathbb{N} with xkykx_k \le y_k for every kKk \ge K.

givenL3
2.1

Let nKn \ge K. Every knk \ge n satisfies kKk \ge K, so xkyksn(y)x_k \le y_k \le s_n(y), and therefore sn(y)s_n(y) is an upper bound of Tn(x)T_n(x), whence sn(x)sn(y)s_n(x) \le s_n(y) by leastness. Dually in(x)xkyki_n(x) \le x_k \le y_k for every knk \ge n, so in(x)i_n(x) is a lower bound of Tn(y)T_n(y) and in(x)in(y)i_n(x) \le i_n(y) by greatest-lower-boundedness.

step 1.1L1L2L4
3.1

For every nNn \in \mathbb{N} one has lim supkxksn(y)\limsup_k x_k \le s_n(y). If nKn \ge K this is lim supkxksn(x)sn(y)\limsup_k x_k \le s_n(x) \le s_n(y), the first inequality because lim supkxk\limsup_k x_k is a lower bound of {sm(x)}\{s_m(x)\}. If n<Kn < K then nKn \le K, so sK(y)sn(y)s_K(y) \le s_n(y), and lim supkxksK(x)sK(y)sn(y)\limsup_k x_k \le s_K(x) \le s_K(y) \le s_n(y).

step 2.1L1L2L4
3.2

For every nNn \in \mathbb{N} one has in(x)lim infkyki_n(x) \le \liminf_k y_k. If nKn \ge K this is in(x)in(y)lim infkyki_n(x) \le i_n(y) \le \liminf_k y_k, the second inequality because lim infkyk\liminf_k y_k is an upper bound of {im(y)}\{i_m(y)\}. If n<Kn < K then nKn \le K, so in(x)iK(x)iK(y)lim infkyki_n(x) \le i_K(x) \le i_K(y) \le \liminf_k y_k.

step 2.1L1L2L4
4.1

By step 3.1 the element lim supkxk\limsup_k x_k is a lower bound of {sn(y):nN}\{s_n(y) : n \in \mathbb{N}\}, whose greatest lower bound is lim supkyk\limsup_k y_k, so lim supkxklim supkyk\limsup_k x_k \le \limsup_k y_k. By step 3.2 the element lim infkyk\liminf_k y_k is an upper bound of {in(x):nN}\{i_n(x) : n \in \mathbb{N}\}, whose least upper bound is lim infkxk\liminf_k x_k, so lim infkxklim infkyk\liminf_k x_k \le \liminf_k y_k.

step 3.1step 3.2L1

Remarks

  • "Eventually" is enough, and the proof shows why. Only tails with nKn \ge K are compared directly; the finitely many earlier tail bounds are absorbed by monotonicity of the tail bounds (The tail suprema of any real sequence are nonincreasing in R\overline{\mathbb{R}}, so the limit superior exists for every sequence), which lets sK(y)s_K(y) stand in for every earlier sn(y)s_n(y). No appeal to Convergence depends only on the tail is needed, since neither quantity is defined as a limit.

  • The comparison does not become strict. From xk<ykx_k < y_k for every kk one gets only lim supkxklim supkyk\limsup_k x_k \le \limsup_k y_k; the sequences xk=0x_k = 0 and yk=1/(k+1)y_k = 1/(k+1) have equal limits and hence equal limit superiors. This is the same phenomenon as for limits (Limits preserve non-strict inequalities).

  • Both conclusions have the same direction. It is the inner operation that differs between lim sup\limsup and lim inf\liminf, and both a supremum and an infimum are monotone in the set, so a pointwise inequality pushes both quantities the same way. What fails to be monotone is the gap between them: nothing here compares lim supkxk\limsup_k x_k with lim infkyk\liminf_k y_k.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

lim sup(xk+yk)lim supxk+lim supyk\limsup(x_k + y_k) \le \limsup x_k + \limsup y_k whenever the right-hand side is defined in R\overline{\mathbb{R}}, and dually for lim inf\liminf

Statement

Let (xk)(x_k) and (yk)(y_k) be sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and write Λ:=lim supkxk\Lambda := \limsup_{k} x_k, M:=lim supkykM := \limsup_{k} y_k (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}}).

  1. If the sum Λ+M\Lambda + M is defined in 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), that is if {Λ,M}{+,}\{\Lambda, M\} \ne \{+\infty, -\infty\}, then lim supk(xk+yk)    Λ+M.\limsup_{k}(x_k + y_k) \;\le\; \Lambda + M .
  2. Dually, writing λ:=lim infkxk\lambda := \liminf_k x_k and μ:=lim infkyk\mu := \liminf_k y_k, if λ+μ\lambda + \mu is defined in R\overline{\mathbb{R}} then lim infk(xk+yk)    λ+μ.\liminf_{k}(x_k + y_k) \;\ge\; \lambda + \mu .

The hypothesis is exactly the one The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined forces, and it cannot be dropped. When one of Λ\Lambda, MM is ++\infty and the other -\infty the right-hand side is not an element of R\overline{\mathbb{R}} at all, so there is nothing to compare. The inequality is genuinely an inequality: equality can fail, and does, for an alternating pair of sequences; the failure of additivity is recorded as a false statement among this page's examples, and the witness is a named counterexample on the companion page.

Facts & Assumptions

Given: Sequences (xk)(x_k) and (yk)(y_k) of reals, their termwise sum (xk+yk)(x_k + y_k), and Λ:=lim supkxk\Lambda := \limsup_k x_k, M:=lim supkykM := \limsup_k y_k, assumed to have a sum defined in R\overline{\mathbb{R}}.

[L2]

The order on R\overline{\mathbb{R}} is total and transitive, ++\infty is its greatest element and -\infty its least, and it restricts on R\mathbb{R} to the order of R\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, Partial order and partially ordered set).

[L3]

Partial addition on R\overline{\mathbb{R}}: a sum is undefined only for the pairs (+,)(+\infty, -\infty) and (,+)(-\infty, +\infty); a sum with one summand ++\infty and the other \ne -\infty is ++\infty; a sum with one summand -\infty and the other +\ne +\infty is -\infty; and (a+b)=(a)+(b)-(a+b) = (-a) + (-b), each side defined exactly when the other is (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined).

[L4]

Epsilon characterisation for a real limit superior: Λ=lim supkxk\Lambda = \limsup_k x_k real implies that for every real ε>0\varepsilon > 0 one has xk<Λ+εx_k < \Lambda + \varepsilon eventually (For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently).

[L6]

Reflection: lim supk(zk)=lim infkzk\limsup_k(-z_k) = -\liminf_k z_k and lim infk(zk)=lim supkzk\liminf_k(-z_k) = -\limsup_k z_k (lim sup(xk)=lim inf(xk)\limsup(-x_k) = -\liminf(x_k), with the reflection of R\overline{\mathbb{R}} exchanging ±\pm\infty).

[L7]

Order arithmetic in R\mathbb{R}: Order is preserved by adding a constant and by adding inequalities states the strict forms, that inequalities may be translated and added, so a<aa < a' and b<bb < b' give a+b<a+ba + b < a' + b'; adjoining the case of equality, in which both sides move by the same amount, gives the nonstrict forms used below. In particular aba \le b if and only if ba-b \le -a: translation by ab-a-b turns a<ba < b into b<a-b < -a and back, while a=ba = b holds exactly when a=b-a = -b.

[L8]

Reciprocal Archimedean property and canonical naturals: for every real δ>0\delta > 0 there is a natural m1m \ge 1 with 1/m<δ1/m < \delta; for a natural m1m \ge 1 the element 2m2m is a natural 1\ge 1 with (2m)1R=2(m1R)>0(2m) \cdot 1_{\mathbb{R}} = 2\big(m \cdot 1_{\mathbb{R}}\big) > 0, so 1/(2m)>01/(2m) > 0 and 1/(2m)+1/(2m)=1/m1/(2m) + 1/(2m) = 1/m (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order, Canonical naturals are positive and strictly increasing).

[L9]

Two properties each holding eventually hold together from the larger of the two thresholds on (Sequences of reals: bounded, eventually, frequently, tails, subsequences, \le is a linear order on N\mathbb{N}, Order on the natural numbers).

Proof

technique · direct
1.1

Since Λ+M\Lambda + M is defined, exactly one of the following three situations holds: at least one of Λ\Lambda, MM equals ++\infty, and then the other is \ne -\infty; both are real; or neither equals ++\infty and at least one equals -\infty. Both the hypothesis and the conclusion of claim 1 are unchanged by exchanging the two sequences, so in the third situation it may be assumed that Λ=\Lambda = -\infty.

givenL2L3
2.1

In the first situation Λ+M=+\Lambda + M = +\infty by the addition table, and every element of R\overline{\mathbb{R}} is +\le +\infty, so lim supk(xk+yk)Λ+M\limsup_k(x_k + y_k) \le \Lambda + M.

step 1.1L2L3
2.2

In the second situation let δ>0\delta > 0 be an arbitrary real, take a natural m1m \ge 1 with 1/m<δ1/m < \delta and put ε:=1/(2m)>0\varepsilon := 1/(2m) > 0, so that ε+ε=1/m<δ\varepsilon + \varepsilon = 1/m < \delta. By [L4] there are thresholds beyond which xk<Λ+εx_k < \Lambda + \varepsilon and beyond which yk<M+εy_k < M + \varepsilon; beyond the larger of them both hold, so adding the two inequalities gives xk+yk<Λ+M+ε+εx_k + y_k < \Lambda + M + \varepsilon + \varepsilon for all kNk \ge N, where NN is that larger threshold. Hence Λ+M+ε+ε\Lambda + M + \varepsilon + \varepsilon is an upper bound of the NN-th tail range of (xk+yk)(x_k + y_k), so the NN-th tail supremum is Λ+M+ε+ε\le \Lambda + M + \varepsilon + \varepsilon, and therefore lim supk(xk+yk)Λ+M+ε+ε<Λ+M+δ\limsup_k(x_k + y_k) \le \Lambda + M + \varepsilon + \varepsilon < \Lambda + M + \delta.

step 1.1L1L2L4L7L8L9
2.3

In the third situation, with Λ=\Lambda = -\infty, first note that there is a real BB with yk<By_k < B eventually: if MM is real, [L4] with ε=1\varepsilon = 1 gives yk<M+1y_k < M + 1 eventually, so B:=M+1B := M + 1 serves; and if M=M = -\infty then yky_k \to -\infty by [L5], so yk<0y_k < 0 eventually and B:=0B := 0 serves. Also Λ=\Lambda = -\infty gives xkx_k \to -\infty by [L5]. Now let cc be an arbitrary real: since cBc - B is real, xk<cBx_k < c - B eventually, and beyond the larger threshold both that and yk<By_k < B hold, so xk+yk<(cB)+B=cx_k + y_k < (c - B) + B = c there. As cc was arbitrary, xk+ykx_k + y_k \to -\infty, hence lim supk(xk+yk)==Λ+M\limsup_k(x_k + y_k) = -\infty = \Lambda + M by [L5] and the addition table.

step 1.1L3L4L5L7L9
3.1

In the second situation the conclusion follows from step 2.2: taking δ=1\delta = 1 shows lim supk(xk+yk)Λ+M+1\limsup_k(x_k + y_k) \le \Lambda + M + 1, a real number, so the left-hand side is not ++\infty; if it is -\infty then it is Λ+M\le \Lambda + M because -\infty is least; and if it is a real SS with S>Λ+MS > \Lambda + M, then δ0:=S(Λ+M)>0\delta_0 := S - (\Lambda + M) > 0 and step 2.2 applied with δ=δ0\delta = \delta_0 gives S<Λ+M+δ0=SS < \Lambda + M + \delta_0 = S, which is impossible. So lim supk(xk+yk)Λ+M\limsup_k(x_k + y_k) \le \Lambda + M by totality.

step 2.2L2L7
4.1

Claim 1 now holds in all three situations, by steps 2.1, 3.1 and 2.3.

step 2.1step 3.1step 2.3step 1.1
5.1

For claim 2, suppose λ+μ\lambda + \mu is defined. By [L6] the reflected sequences have lim supk(xk)=λ\limsup_k(-x_k) = -\lambda and lim supk(yk)=μ\limsup_k(-y_k) = -\mu, and (λ)+(μ)=(λ+μ)(-\lambda) + (-\mu) = -(\lambda + \mu) is defined exactly when λ+μ\lambda + \mu is, by [L3]. Claim 1 applied to (xk)(-x_k) and (yk)(-y_k), whose termwise sum is ((xk+yk))(-(x_k + y_k)), therefore gives lim infk(xk+yk)=lim supk((xk+yk))(λ)+(μ)=(λ+μ)-\liminf_k(x_k + y_k) = \limsup_k\big(-(x_k+y_k)\big) \le (-\lambda) + (-\mu) = -(\lambda + \mu); reflecting this inequality reverses it into lim infk(xk+yk)λ+μ\liminf_k(x_k + y_k) \ge \lambda + \mu.

step 4.1L3L6L7

Remarks

  • The three situations are not decoration. The middle one is the analytic content and the outer two are genuinely different arguments: the first is vacuous because ++\infty bounds everything, and the third is a statement about divergence to -\infty that has to be proved, since a sum of two sequences each running off to -\infty, or one running off with the other merely bounded above, is not covered by any algebra of limits (Divergence to ++\infty and to -\infty forbids that).

  • Why the real supremum of a sumset is not used. The natural one-line route, sn(x+y)sn(x)+sn(y)s_n(x+y) \le s_n(x) + s_n(y) followed by a passage to the infimum, needs the first inequality in R\overline{\mathbb{R}} and then still needs an ε\varepsilon argument to compare infn(sn(x)+sn(y))\inf_n\big(s_n(x) + s_n(y)\big) with Λ+M\Lambda + M. The identity sup(S+T)=supS+supT\sup(S+T) = \sup S + \sup T of Supremum of a sumset: sup(S+T)=supS+supT\sup(S + T) = \sup S + \sup T does not apply, since it requires both sets to be nonempty subsets of R\mathbb{R} bounded above, and a tail range of an unbounded sequence is not. The ε\varepsilon argument is therefore made directly, once.

  • Both halves of the ε\varepsilon split are reciprocals of natural numbers, not halvings in R\mathbb{R}. Choosing mm with 1/m<δ1/m < \delta and then working with 1/(2m)1/(2m) keeps every quantity a reciprocal of a canonical natural, so the only field facts used are that positives are invertible and that inequalities add.

  • Equality is the exception. Without a hypothesis on one of the two sequences the gap can be as large as the whole oscillation, as xk=(1)kx_k = (-1)^k, yk=(1)k+1y_k = (-1)^{k+1} give lim sup(xk+yk)=0<2=lim supxk+lim supyk\limsup(x_k + y_k) = 0 < 2 = \limsup x_k + \limsup y_k shows. It is standard, and neither needed nor proved on this page, that the inequality becomes an equality as soon as one of the two sequences converges to a real limit.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For bounded nonnegative sequences, lim sup(xkyk)(lim supxk)(lim supyk)\limsup(x_k y_k) \le (\limsup x_k)(\limsup y_k)

Statement

Let (xk)(x_k) and (yk)(y_k) be bounded sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with xk0x_k \ge 0 and yk0y_k \ge 0 for every kNk \in \mathbb{N}. Then lim supkxk\limsup_k x_k, lim supkyk\limsup_k y_k and lim supk(xkyk)\limsup_k (x_k y_k) are real numbers, all 0\ge 0, and

lim supk(xkyk)    (lim supkxk)(lim supkyk).\limsup_{k} (x_k y_k) \;\le\; \Big(\limsup_{k} x_k\Big)\Big(\limsup_{k} y_k\Big).

Both hypotheses are doing work. Boundedness makes all three quantities real, so that the product on the right is a product in the field R\mathbb{R} and no extended multiplication is involved; without it the right-hand side could be an undefined product 0(+)0 \cdot (+\infty) (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined). Nonnegativity is what lets two upper estimates be multiplied: for sequences of mixed sign the inequality is false in the stated form, since a product of two negative numbers is positive and the estimate would point the wrong way. Strictness is possible, and a witness is recorded on the companion page.

Facts & Assumptions

Given: Bounded sequences (xk)(x_k), (yk)(y_k) of reals with xk0x_k \ge 0 and yk0y_k \ge 0 for every kk; their termwise product (xkyk)(x_k y_k); and Λ:=lim supkxk\Lambda := \limsup_k x_k, M:=lim supkykM := \limsup_k y_k, P:=lim supk(xkyk)P := \limsup_k(x_k y_k) (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}}).

[L2]

The order on R\overline{\mathbb{R}} is total and transitive, restricts on R\mathbb{R} to the order of R\mathbb{R}, and has ++\infty greatest and -\infty least; a member of R\overline{\mathbb{R}} lying between two reals is itself real (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined, Partial order and partially ordered set).

[L3]

Epsilon characterisation for a real limit superior: for every real ε>0\varepsilon > 0 one has zk<lim supkzk+εz_k < \limsup_k z_k + \varepsilon eventually (For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently).

[L4]

Boundedness of a sequence of reals: there is a real BB with zkB|z_k| \le B for every kk; and zzz \le |z| always (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Lower bound, bounded below, bounded set, Basic properties of the absolute value).

[L5]

Products of inequalities: 0ab0 \le a \le b and 0cd0 \le c \le d give acbdac \le bd, which Multiplying inequalities of positives states in exactly this nonstrict form; and multiplication by a positive element preserves the order, Sign rules for products and monotonicity of multiplication stating the strict form a<b    ac<bca < b \iff ac < bc and the nonstrict form following by adjoining the case a=ba = b, where the two products are equal.

[L6]

Order arithmetic in R\mathbb{R}: inequalities may be added and translated, and the order is total, so exactly one of a<ba < b, a=ba = b, b<ab < a holds (Order is preserved by adding a constant and by adding inequalities).

[L7]

Reciprocal Archimedean property: for every real η>0\eta > 0 there is a natural m1m \ge 1 with 1/m<η1/m < \eta; and 0<ab0 < a \le b gives 0<1/b1/a0 < 1/b \le 1/a (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L8]

Two properties each holding eventually hold together from the larger of the two thresholds on, the order on N\mathbb{N} being total (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Order on the natural numbers, \le is a linear order on N\mathbb{N}).

Proof

technique · direct
1.1

Both sequences are bounded, so there are reals bounding xk|x_k| and yk|y_k|; let BB be the larger of the two, so that xkB|x_k| \le B and ykB|y_k| \le B for every kk, and Bx00B \ge |x_0| \ge 0. With xk0x_k \ge 0 and yk0y_k \ge 0 this gives 0xkB0 \le x_k \le B and 0ykB0 \le y_k \le B for every kk, hence 0xkykBB0 \le x_k y_k \le B \cdot B by [L5].

givenL4L5L6
2.1

Each of Λ\Lambda, MM, PP is a real number 0\ge 0. Indeed, for every nn the real BB is an upper bound of the nn-th tail range of (xk)(x_k), so snBs_n \le B and hence Λs0B\Lambda \le s_0 \le B; and snxn0s_n \ge x_n \ge 0 for every nn, so 00 is a lower bound of {sn}\{s_n\} and 0Λ0 \le \Lambda. Being between the reals 00 and BB, the element Λ\Lambda is real. The same argument gives 0MB0 \le M \le B, and, using the bound BBB \cdot B from step 1.1, 0PBB0 \le P \le B \cdot B.

step 1.1L1L2
3.1

Let δ>0\delta > 0 be an arbitrary real and put C:=Λ+M+1C := \Lambda + M + 1, a real with C1>0C \ge 1 > 0. Take a natural m11m_1 \ge 1 with 1/m1<11/m_1 < 1 and a natural m21m_2 \ge 1 with 1/m2<δ/C1/m_2 < \delta/C, let mm be the larger of m1m_1 and m2m_2, and set ε:=1/m\varepsilon := 1/m, so that 0<ε<10 < \varepsilon < 1 and εC<δ\varepsilon C < \delta. By [L3] there are thresholds beyond which xk<Λ+εx_k < \Lambda + \varepsilon and beyond which yk<M+εy_k < M + \varepsilon; let NN be the larger. For kNk \ge N we have 0xkΛ+ε0 \le x_k \le \Lambda + \varepsilon and 0ykM+ε0 \le y_k \le M + \varepsilon, so xkyk(Λ+ε)(M+ε)=ΛM+ε(Λ+M+ε)ΛM+εC<ΛM+δx_k y_k \le (\Lambda + \varepsilon)(M + \varepsilon) = \Lambda M + \varepsilon(\Lambda + M + \varepsilon) \le \Lambda M + \varepsilon C < \Lambda M + \delta, the middle step because Λ+M+εC\Lambda + M + \varepsilon \le C and ε>0\varepsilon > 0. Hence ΛM+εC\Lambda M + \varepsilon C is an upper bound of the NN-th tail range of (xkyk)(x_k y_k), so PΛM+εC<ΛM+δP \le \Lambda M + \varepsilon C < \Lambda M + \delta.

step 2.1L1L3L5L6L7L8algebra
4.1

Suppose P>ΛMP > \Lambda M. Both are real by step 2.1, so δ0:=PΛM>0\delta_0 := P - \Lambda M > 0, and step 3.1 applied with δ=δ0\delta = \delta_0 gives P<ΛM+δ0=PP < \Lambda M + \delta_0 = P, which is impossible. By totality PΛMP \le \Lambda M, which is the asserted inequality.

step 3.1step 2.1L2L6

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

n1/n1n^{1/n} \to 1

Statement

For a natural number n1n \ge 1 write ι(n):=n1R\iota(n) := n \cdot 1_{\mathbb{R}} for the canonical natural of R\mathbb{R} (Canonical naturals are positive and strictly increasing) and n1/n:=ι(n)1/nn^{1/n} := \iota(n)^{1/n}, n1/2:=ι(n)1/2n^{1/2} := \iota(n)^{1/2} for its roots (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base). Then:

  1. 1    n1/n    1+2n1/2\displaystyle 1 \;\le\; n^{1/n} \;\le\; 1 + \frac{2}{n^{1/2}} for every natural n1n \ge 1;
  2. the sequence rk:=(k+1)1/(k+1)r_k := (k+1)^{1/(k+1)}, kNk \in \mathbb{N}, converges to 11 (Limits and Cauchy sequences of reals).

The index range is not cosmetic. The expression n1/nn^{1/n} is defined only for n1n \ge 1, since 1/n1/n is not a rational number when n=0n = 0 (Rational powers ara^r of a positive base). Sequences in this library are functions on N\mathbb{N} and N\mathbb{N} contains 00 (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the statement of convergence is made about the shifted family rk=(k+1)1/(k+1)r_k = (k+1)^{1/(k+1)}, which is the classical family n1/nn^{1/n}, n1n \ge 1, reindexed by n=k+1n = k+1. Claim 1 is stated over the natural range n1n \ge 1 where the expression means something.

Facts & Assumptions

Given: For a natural m1m \ge 1 the canonical natural ι(m):=m1R\iota(m) := m \cdot 1_{\mathbb{R}}, extended by ι(0):=0\iota(0) := 0; this extension keeps the additivity ι(m+m)=ι(m)+ι(m)\iota(m + m') = \iota(m) + \iota(m') of Canonical naturals are positive and strictly increasing, which for mm or mm' equal to 00 reads ι(m)=ι(m)+0\iota(m) = \iota(m) + 0.

[L1]

Roots: for real a0a \ge 0 and natural n1n \ge 1 there is a unique real s0s \ge 0 with sn=as^n = a, written a1/na^{1/n}; it is >0> 0 when a>0a > 0, and a1/1=aa^{1/1} = a (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Integer powers ama^m).

[L2]

Rational powers and monotonicity: a1/na^{1/n} is the rational power ara^r at r=1/nr = 1/n, and for rational t>0t > 0 one has at>1a^t > 1 whenever a>1a > 1; also (1/a)1/2=1/a1/2\big(1/a\big)^{1/2} = 1/a^{1/2} for a>0a > 0 (Rational powers ara^r of a positive base, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}, Laws of rational exponents).

[L3]

AM-GM: for a natural n1n \ge 1 and reals a0,,an10a_0, \dots, a_{n-1} \ge 0, the geometric mean (j<naj)1/n\big(\prod_{j<n} a_j\big)^{1/n} is \le the arithmetic mean 1ι(n)j<naj\frac{1}{\iota(n)}\sum_{j<n} a_j (The arithmetic mean, geometric mean inequality).

[L4]

Finite sums and products: the empty sum is 00 and the empty product 11; sums and products split at any intermediate index; and j<mλ=ι(m)λ\sum_{j<m} \lambda = \iota(m)\lambda for a constant λ\lambda (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L5]
[L6]

Canonical naturals: ι(m)>0\iota(m) > 0 and ι(m)\iota(m) is invertible for m1m \ge 1, ι\iota is strictly increasing, and ι(2)=2>1\iota(2) = 2 > 1; the Archimedean property gives, for every real xx, a natural p1p \ge 1 with x<ι(p)x < \iota(p) (Canonical naturals are positive and strictly increasing, Every complete ordered field is Archimedean).

[L7]

Order and reciprocals: 0<a<b0 < a < b gives 0<1/b<1/a0 < 1/b < 1/a; multiplying an inequality by a positive element preserves it; and inequalities may be added and translated (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Order is preserved by adding a constant and by adding inequalities).

[L8]

Squares: for a,b0a, b \ge 0 one has a<ba < b if and only if aa<bba \cdot a < b \cdot b (Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n, Integer powers ama^m).

[L9]

Squeeze theorem, and the fact that a constant sequence converges to its value; to establish convergence it suffices to produce a threshold for every real ε>0\varepsilon > 0 (The squeeze theorem, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L10]

The order on N\mathbb{N} is total and ι\iota respects it (Order on the natural numbers, \le is a linear order on N\mathbb{N}).

Proof

technique · direct
1.1

For a natural n1n \ge 1 the element ι(n)\iota(n) is positive and invertible, so ι(n)1/n\iota(n)^{1/n} and ι(n)1/2\iota(n)^{1/2} exist and are positive.

givenL1L6
1.2

For every natural mm one has j<m1=1\prod_{j<m} 1 = 1: the empty product is 11, and if j<m1=1\prod_{j<m} 1 = 1 then j<m+11=(j<m1)1=1\prod_{j<m+1} 1 = \big(\prod_{j<m} 1\big) \cdot 1 = 1, so this follows by induction on mm.

givenL4L5
2.1

For n=1n = 1 one has ι(1)=1\iota(1) = 1 and 11/1=11^{1/1} = 1; for n2n \ge 2 one has ι(n)ι(2)=2>1\iota(n) \ge \iota(2) = 2 > 1 and 1/n1/n is a positive rational, so ι(n)1/n>1\iota(n)^{1/n} > 1. In either case n1/n1n^{1/n} \ge 1.

step 1.1L1L2L6L10
2.2

Let n2n \ge 2 and put u:=ι(n)1/2u := \iota(n)^{1/2}, so that u>0u > 0 and uu=ι(n)u \cdot u = \iota(n). Apply [L3] to the list of nn nonnegative reals given by a0=a1=ua_0 = a_1 = u and aj=1a_j = 1 for 2j<n2 \le j < n, the latter range being empty when n=2n = 2. Splitting at index 22 gives j<naj=(j<2aj)(j<n2a2+j)=(uu)1=ι(n)\prod_{j<n} a_j = \big(\prod_{j<2} a_j\big)\big(\prod_{j<n-2} a_{2+j}\big) = (u \cdot u) \cdot 1 = \iota(n) by step 1.2, so the geometric mean is ι(n)1/n\iota(n)^{1/n}; and j<naj=(j<2aj)+(j<n21)=(u+u)+ι(n2)=(u+u)+ι(n)2\sum_{j<n} a_j = \big(\sum_{j<2} a_j\big) + \big(\sum_{j<n-2} 1\big) = (u + u) + \iota(n-2) = (u+u) + \iota(n) - 2, using additivity of ι\iota and ι(2)=2\iota(2) = 2, so the arithmetic mean is A=((u+u)+ι(n)2)/ι(n)=1+((u+u)2)/ι(n)A = \big((u+u) + \iota(n) - 2\big)/\iota(n) = 1 + \big((u+u) - 2\big)/\iota(n). Since (u+u)2<u+u(u+u) - 2 < u + u and ι(n)>0\iota(n) > 0, and (u+u)/ι(n)=(u+u)/(uu)=2/u(u+u)/\iota(n) = (u+u)/(u \cdot u) = 2/u, this gives ι(n)1/nA1+2/u=1+2/n1/2\iota(n)^{1/n} \le A \le 1 + 2/u = 1 + 2/n^{1/2}.

step 1.1step 1.2L1L3L4L6L7algebra
2.3

For n=1n = 1 the same bound holds trivially: 11/1=11+2=1+2/11/21^{1/1} = 1 \le 1 + 2 = 1 + 2/1^{1/2}.

step 1.1L1L6L7
2.4

The sequence bk:=1+2/(k+1)1/2b_k := 1 + 2/(k+1)^{1/2} converges to 11. Given a real ε>0\varepsilon > 0, put t:=2/ε>0t := 2/\varepsilon > 0 and take a natural p1p \ge 1 with tt<ι(p)t \cdot t < \iota(p). For kpk \ge p we have k+1>pk + 1 > p, hence ι(k+1)>ι(p)>tt\iota(k+1) > \iota(p) > t \cdot t, and since (ι(k+1)1/2)(ι(k+1)1/2)=ι(k+1)\big(\iota(k+1)^{1/2}\big)\big(\iota(k+1)^{1/2}\big) = \iota(k+1) with both factors 0\ge 0, this forces t<ι(k+1)1/2t < \iota(k+1)^{1/2}. Therefore 0<2/ι(k+1)1/2<2/t=ε0 < 2/\iota(k+1)^{1/2} < 2/t = \varepsilon, that is bk1<ε|b_k - 1| < \varepsilon.

step 1.1L1L6L7L8L9L10algebra
3.1

Claim 1 is the combination of steps 2.1, 2.2 and 2.3, the two upper bounds covering n2n \ge 2 and n=1n = 1 respectively.

step 2.1step 2.2step 2.3
4.1

For every kNk \in \mathbb{N} the natural k+1k+1 is 1\ge 1, so claim 1 gives 1rkbk1 \le r_k \le b_k. The constant sequence 11 converges to 11 and (bk)(b_k) converges to 11 by step 2.4, so the squeeze theorem gives rk1r_k \to 1, which is claim 2.

step 3.1step 2.4L9

Remarks

  • Where the n\sqrt{n} comes from. AM-GM is applied to a list whose product is nn but whose entries are as close to 11 as possible: two copies of n1/2n^{1/2} and n2n-2 copies of 11. The arithmetic mean is then 1+(2n1/22)/n1 + (2n^{1/2} - 2)/n, which tends to 11 at the rate 2/n1/22/n^{1/2}. Splitting nn as n1/2n1/2n^{1/2} \cdot n^{1/2} rather than as n1n \cdot 1 is the whole trick: the list n,1,,1n, 1, \dots, 1 gives only n1/n21/nn^{1/n} \le 2 - 1/n, which does not converge to 11.

  • The lower bound is not decoration. Without n1/n1n^{1/n} \ge 1 the squeeze has nothing below it, and the upper bound alone would leave open a limit smaller than 11. It comes from monotonicity of rational powers in the base (Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}) and holds with equality only at n=1n = 1.

  • No logarithm and no exponential is used. The usual quick proof writes n1/n=e(logn)/nn^{1/n} = e^{(\log n)/n} and appeals to (logn)/n0(\log n)/n \to 0; neither function exists in this library yet, and the AM-GM route needs nothing beyond roots and finite sums.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For every a>0a > 0, a1/n1a^{1/n} \to 1

Statement

Let aRa \in \mathbb{R} with a>0a > 0, write ι(n):=n1R\iota(n) := n \cdot 1_{\mathbb{R}} for the canonical natural (Canonical naturals are positive and strictly increasing) and a1/na^{1/n} for the nn-th root (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base), defined for naturals n1n \ge 1. Then:

  1. for every real b1b \ge 1 and every natural n1n \ge 1, 1    b1/n    1+b1ι(n);1 \;\le\; b^{1/n} \;\le\; 1 + \frac{b-1}{\iota(n)};
  2. the sequence ck:=a1/(k+1)c_k := a^{1/(k+1)}, kNk \in \mathbb{N}, converges to 11 (Limits and Cauchy sequences of reals).

Index range. As for the previous lemma on this page, a1/na^{1/n} requires n1n \ge 1, so the sequence indexed by N\mathbb{N} (Sequences of reals: bounded, eventually, frequently, tails, subsequences) is the shifted family a1/(k+1)a^{1/(k+1)}; it is the classical family a1/na^{1/n}, n1n \ge 1, reindexed by n=k+1n = k+1.

Facts & Assumptions

Given: A real a>0a > 0; the canonical naturals ι(n)=n1R\iota(n) = n \cdot 1_{\mathbb{R}} for n1n \ge 1; and the sequence ck:=a1/(k+1)c_k := a^{1/(k+1)}.

[L1]

Roots: for real x0x \ge 0 and natural n1n \ge 1 there is a unique real s0s \ge 0 with sn=xs^n = x, written x1/nx^{1/n}; it is >0> 0 when x>0x > 0, and 11/n=11^{1/n} = 1 by uniqueness (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Integer powers ama^m).

[L2]

Rational powers: x1/nx^{1/n} is the rational power at exponent 1/n1/n; for rational t>0t > 0, x>1x > 1 implies xt>1x^t > 1; and (xy)1/n=x1/ny1/n(xy)^{1/n} = x^{1/n} y^{1/n} for x,y>0x, y > 0 (Rational powers ara^r of a positive base, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}, Laws of rational exponents).

[L3]

Bernoulli's inequality: (1+x)n1+ι(n)x(1+x)^n \ge 1 + \iota(n) x for x1x \ge -1 and nNn \in \mathbb{N} (Bernoulli's inequality (1+x)n1+nx(1+x)^n \ge 1 + nx).

[L4]

Canonical naturals: ι(n)>0\iota(n) > 0 and invertible for n1n \ge 1, and ι\iota is strictly increasing (Canonical naturals are positive and strictly increasing, Order on the natural numbers, \le is a linear order on N\mathbb{N}).

[L5]

Reciprocal Archimedean property: for every real η>0\eta > 0 there is a natural p1p \ge 1 with 1/p<η1/p < \eta; and 0<x<y0 < x < y gives 0<1/y<1/x0 < 1/y < 1/x (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L6]

Order arithmetic: inequalities may be added and translated, and multiplying an inequality by a positive element preserves it; the order is total, so exactly one of a<1a < 1, a=1a = 1, a>1a > 1 holds (Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)).

[L7]

Squeeze theorem; a constant sequence converges to its value; to establish convergence it suffices to produce a threshold for every real ε>0\varepsilon > 0 (The squeeze theorem, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L8]

Algebra of limits, reciprocal rule: if zjzz_j \to z with z0z \ne 0 and zj0z_j \ne 0 for every jj, then 1/zj1/z1/z_j \to 1/z (Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · cases
1.1

Let bb be any real with b1b \ge 1 and let n1n \ge 1 be a natural. If b=1b = 1 then b1/n=1b^{1/n} = 1 and both inequalities hold. If b>1b > 1 then 1/n1/n is a positive rational, so t:=b1/n1>0t := b^{1/n} - 1 > 0; Bernoulli's inequality applied to t1t \ge -1 gives b=(b1/n)n=(1+t)n1+ι(n)tb = \big(b^{1/n}\big)^n = (1+t)^n \ge 1 + \iota(n)t, hence ι(n)tb1\iota(n) t \le b - 1 and t(b1)/ι(n)t \le (b-1)/\iota(n) since ι(n)>0\iota(n) > 0. In both cases 1b1/n1+(b1)/ι(n)1 \le b^{1/n} \le 1 + (b-1)/\iota(n), which is claim 1.

givenL1L2L3L4L6
1.2

Case one: a=1a = 1.

givenassume-case one
1.3

Case big: a>1a > 1.

givenassume-case big
1.4

Case small: 0<a<10 < a < 1.

givenassume-case small
2.1

For every real b>1b > 1 the sequence b1/(k+1)b^{1/(k+1)} converges to 11. Put dk:=1+(b1)/ι(k+1)d_k := 1 + (b-1)/\iota(k+1). Given a real ε>0\varepsilon > 0, the quotient ε/(b1)\varepsilon/(b-1) is positive, so there is a natural p1p \ge 1 with 1/p<ε/(b1)1/p < \varepsilon/(b-1); for kpk \ge p we have k+1>pk+1 > p, hence ι(k+1)>ι(p)>0\iota(k+1) > \iota(p) > 0 and 0<(b1)/ι(k+1)<(b1)(1/p)<ε0 < (b-1)/\iota(k+1) < (b-1)(1/p) < \varepsilon, so dk1<ε|d_k - 1| < \varepsilon and dk1d_k \to 1. By step 1.1 applied at n=k+1n = k+1 we have 1b1/(k+1)dk1 \le b^{1/(k+1)} \le d_k for every kk, and the constant sequence 11 converges to 11, so the squeeze theorem gives b1/(k+1)1b^{1/(k+1)} \to 1.

step 1.1L4L5L6L7
2.2

In case one, ck=11/(k+1)=1c_k = 1^{1/(k+1)} = 1 for every kk, so (ck)(c_k) is the constant sequence 11 and converges to 11.

step 1.2L1L7
3.1

In case big, a>1a > 1, so step 2.1 applied with b=ab = a gives ck=a1/(k+1)1c_k = a^{1/(k+1)} \to 1.

step 2.1step 1.3
3.2

In case small, put a:=1/aa' := 1/a, which satisfies a>1a' > 1 because 0<a<10 < a < 1. For each natural n1n \ge 1 the product rule for roots gives a1/n(a)1/n=(aa)1/n=11/n=1a^{1/n} (a')^{1/n} = (a a')^{1/n} = 1^{1/n} = 1, so a1/n=1/(a)1/na^{1/n} = 1/(a')^{1/n}, and (a)1/n>0(a')^{1/n} > 0. By step 2.1 the sequence (a)1/(k+1)(a')^{1/(k+1)} converges to 101 \ne 0 with all terms nonzero, so the reciprocal rule gives ck=1/(a)1/(k+1)1/1=1c_k = 1/(a')^{1/(k+1)} \to 1/1 = 1.

step 2.1step 1.4L1L2L5L8
4.1

The three cases are exhaustive by trichotomy applied to aa and 11, the hypothesis a>0a > 0 excluding nothing else, and in each of them (ck)(c_k) converges to 11; together with step 1.1 this proves both claims.

step 2.2step 3.1step 3.2step 1.1L6cases: trichotomy of the ordercases-exhaustive

Remarks

  • Bernoulli is doing the whole job in the case a>1a > 1. The inequality (1+t)n1+nt(1+t)^n \ge 1 + nt converts the exact identity (a1/n)n=a\big(a^{1/n}\big)^n = a into the linear bound t(a1)/nt \le (a-1)/n on the excess t=a1/n1t = a^{1/n} - 1, and that bound is what tends to 00. No estimate on a1/na^{1/n} itself is needed beyond a1/n>1a^{1/n} > 1.

  • The case 0<a<10 < a < 1 is not symmetric to the case a>1a > 1 and is not proved again. It is transported by the reciprocal, using a1/n(1/a)1/n=1a^{1/n} (1/a)^{1/n} = 1 (Laws of rational exponents) and the reciprocal rule of Algebra of limits: sums, scalar multiples, products and quotients. The hypothesis of that rule, that the limit be nonzero and every term nonzero, is met because roots of positive reals are positive.

  • The rate is different from the one in n1/n1n^{1/n} \to 1. Here the excess is O(1/n)O(1/n) with a constant depending on aa; there the base itself grows with nn and the excess is only O(1/n1/2)O(1/n^{1/2}). The two lemmas are therefore not instances of one another in either direction.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For ak>0a_k > 0: lim infak+1/aklim infak1/klim supak1/klim supak+1/ak\liminf a_{k+1}/a_k \le \liminf a_k^{1/k} \le \limsup a_k^{1/k} \le \limsup a_{k+1}/a_k

Statement

Let (ak)kN(a_k)_{k \in \mathbb{N}} be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with ak>0a_k > 0 for every kk. Put

qk:=ak+1ak,rk:=ak+11/(k+1)(kN),q_k := \frac{a_{k+1}}{a_k}, \qquad r_k := a_{k+1}^{1/(k+1)} \qquad (k \in \mathbb{N}),

with roots as in Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a and Rational powers ara^r of a positive base. Then, in R\overline{\mathbb{R}} (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}}, The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined),

lim infkqk    lim infkrk    lim supkrk    lim supkqk.\liminf_{k} q_k \;\le\; \liminf_{k} r_k \;\le\; \limsup_{k} r_k \;\le\; \limsup_{k} q_k .

The root sequence must start at index 11, and (rk)(r_k) is the shift that makes it a sequence on N\mathbb{N}. The classical statement writes an1/na_n^{1/n}, which is meaningful only for n1n \ge 1, since 1/01/0 is not a rational number; sequences here are functions on N\mathbb{N} and N\mathbb{N} contains 00 (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the root family is written rk=ak+11/(k+1)r_k = a_{k+1}^{1/(k+1)}, which is an1/na_n^{1/n} reindexed by n=k+1n = k+1. The ratio family qkq_k needs no shift, and the four quantities in the display are those of the two sequences (qk)(q_k) and (rk)(r_k) exactly as written here.

This is why the root test dominates the ratio test. If the ratios converge, the outer two quantities coincide and the chain forces the roots to converge to the same value; but the roots can converge when the ratios do not, and then the chain is strict at both ends. Both phenomena are exhibited by named examples on the companion page.

Facts & Assumptions

Given: A sequence (ak)(a_k) of reals with ak>0a_k > 0 for every kk; the ratio sequence qk=ak+1/akq_k = a_{k+1}/a_k; the root sequence rk=ak+11/(k+1)r_k = a_{k+1}^{1/(k+1)}; and ι(n)=n1R\iota(n) = n \cdot 1_{\mathbb{R}} for the canonical naturals.

[L2]

The order on R\overline{\mathbb{R}} is total and transitive, ++\infty is greatest and -\infty least, it restricts on R\mathbb{R} to the order of R\mathbb{R}, and an element between two reals is real (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined, Partial order and partially ordered set).

[L3]

Epsilon characterisation, for a real LL: L=lim supkzkL = \limsup_k z_k gives zk<L+εz_k < L + \varepsilon eventually for every real ε>0\varepsilon > 0; L=lim infkzkL = \liminf_k z_k gives zk>Lεz_k > L - \varepsilon eventually for every real ε>0\varepsilon > 0 (For finite LL: L=lim supxkL = \limsup x_k iff for every ε>0\varepsilon > 0 one has xk<L+εx_k < L + \varepsilon eventually and xk>Lεx_k > L - \varepsilon frequently).

[L4]

lim infkzklim supkzk\liminf_k z_k \le \limsup_k z_k (lim infxklim supxk\liminf x_k \le \limsup x_k for every real sequence).

[L5]

Comparison: zkwkz_k \le w_k eventually implies lim supkzklim supkwk\limsup_k z_k \le \limsup_k w_k and lim infkzklim infkwk\liminf_k z_k \le \liminf_k w_k (If xkykx_k \le y_k eventually then lim supxklim supyk\limsup x_k \le \limsup y_k and lim infxklim infyk\liminf x_k \le \liminf y_k).

[L6]

A sequence converging to a real cc has lim sup=lim inf=c\limsup = \liminf = c; and lim infkzk=+\liminf_k z_k = +\infty implies zk+z_k \to +\infty, hence zk>Mz_k > M eventually for every real MM (A real sequence converges to LRL \in \mathbb{R} iff lim infxk=lim supxk=L\liminf x_k = \limsup x_k = L, and diverges to ±\pm\infty iff both equal ±\pm\infty, Divergence to ++\infty and to -\infty).

[L7]

For every real C>0C > 0 the sequence C1/(k+1)C^{1/(k+1)} converges to 11 (For every a>0a > 0, a1/n1a^{1/n} \to 1).

[L8]

Algebra of limits: a scalar multiple of a convergent sequence converges to the scalar multiple of the limit (Algebra of limits: sums, scalar multiples, products and quotients).

[L9]

Roots and powers of positive reals: x1/nx^{1/n} exists, is unique and is >0> 0 for x>0x > 0 and n1n \ge 1; (xy)1/n=x1/ny1/n(xy)^{1/n} = x^{1/n} y^{1/n}; the integer power xnx^n is the rational power at exponent nn, so (xn)1/n=xn(1/n)=x(x^n)^{1/n} = x^{n \cdot (1/n)} = x; xm=1/xmx^{-m} = 1/x^m and xmxm=xm+mx^{m} x^{m'} = x^{m+m'} for integer exponents and x0x \ne 0; xn>0x^n > 0 for x>0x > 0; and 0xy0 \le x \le y implies x1/ny1/nx^{1/n} \le y^{1/n} (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base, Laws of rational exponents, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}, Integer powers ama^m, Laws of integer exponents, Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n).

[L10]
[L11]

Archimedean facts: for every real η>0\eta > 0 there is a natural m1m \ge 1 with 1/m<η1/m < \eta; and 0<x<y0 < x < y gives 0<1/y<1/x0 < 1/y < 1/x (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L12]

Order arithmetic: Order is preserved by adding a constant and by adding inequalities and claim 4 of Sign rules for products and monotonicity of multiplication state the strict forms, that inequalities may be translated and added and that multiplication by a positive element preserves <<; adjoining the case of equality, where both sides move or scale alike, gives the nonstrict forms used below. Products of nonnegative inequalities multiply in the nonstrict form stated by Multiplying inequalities of positives, and the order on R\mathbb{R} is total.

[L13]

Strictly between any two reals lies a rational (The rationals embed densely in the reals).

Proof

technique · direct
1.1

Every qkq_k is positive, being a quotient of positive reals, and every rkr_k is positive, being a root of the positive real ak+1a_{k+1}. Hence 00 is a lower bound of every tail range of (qk)(q_k) and of (rk)(r_k), so every tail infimum is 0\ge 0 and therefore lim infkqk0\liminf_k q_k \ge 0 and lim infkrk0\liminf_k r_k \ge 0; with [L4] this also gives lim supkqk0\limsup_k q_k \ge 0.

givenL1L2L4L9L11
1.2

Let c>0c > 0 be real, let NNN \in \mathbb{N} and put C:=aNcNC := a_N c^{-N}, a positive real. If ak+1caka_{k+1} \le c\,a_k for every kNk \ge N then anCcna_n \le C c^n for every nNn \ge N; if ak+1caka_{k+1} \ge c\,a_k for every kNk \ge N then anCcna_n \ge C c^n for every nNn \ge N. Both are inductions on jj for n=N+jn = N + j: at j=0j = 0 one has CcN=aNcNcN=aNc0=aNC c^N = a_N c^{-N} c^N = a_N c^0 = a_N, and the inductive step multiplies the bound at nn by the positive cc and uses the hypothesis at k=nk = n.

givenL9L10L12
1.3

Let C>0C > 0 and c>0c > 0 be real and n1n \ge 1 a natural. Then (Ccn)1/n=C1/n(cn)1/n=C1/nc(C c^n)^{1/n} = C^{1/n} (c^n)^{1/n} = C^{1/n} c. Consequently 0<anCcn0 < a_n \le C c^n gives an1/nC1/nca_n^{1/n} \le C^{1/n} c, and anCcn>0a_n \ge C c^n > 0 gives an1/nC1/nca_n^{1/n} \ge C^{1/n} c, since xx1/nx \mapsto x^{1/n} is nondecreasing on the nonnegative reals.

givenL9
1.4

For real C>0C > 0 and c>0c > 0 the sequence uk:=C1/(k+1)cu_k := C^{1/(k+1)} c converges to cc, by [L7] and the scalar rule; hence lim supkuk=lim infkuk=c\limsup_k u_k = \liminf_k u_k = c.

givenL6L7L8
1.5

If lim supkqk=+\limsup_k q_k = +\infty then lim supkrklim supkqk\limsup_k r_k \le \limsup_k q_k, since ++\infty is the greatest element of R\overline{\mathbb{R}}.

givenL2
2.1

Suppose β:=lim supkqk\beta := \limsup_k q_k is real, and let ε>0\varepsilon > 0 be an arbitrary real. Put c:=β+εc := \beta + \varepsilon, which is positive since β0\beta \ge 0. By [L3] there is NN with qk<cq_k < c for all kNk \ge N, that is ak+1<caka_{k+1} < c\,a_k after multiplying by ak>0a_k > 0; so ak+1caka_{k+1} \le c\,a_k for kNk \ge N, and step 1.2 gives anCcna_n \le C c^n for all nNn \ge N with C:=aNcN>0C := a_N c^{-N} > 0. For kNk \ge N the index n:=k+1n := k+1 satisfies nNn \ge N and n1n \ge 1, so step 1.3 gives rkC1/(k+1)c=ukr_k \le C^{1/(k+1)} c = u_k. By step 1.4 and [L5], lim supkrklim supkuk=c=β+ε\limsup_k r_k \le \limsup_k u_k = c = \beta + \varepsilon.

step 1.1step 1.2step 1.3step 1.4L3L5L12L14
2.2

If α:=lim infkqk=0\alpha := \liminf_k q_k = 0 then lim infkrk0=α\liminf_k r_k \ge 0 = \alpha by step 1.1.

step 1.1
2.3

Suppose α:=lim infkqk>0\alpha := \liminf_k q_k > 0 and let cc be a real with 0<c<α0 < c < \alpha. Then qk>cq_k > c eventually: if α\alpha is real this is [L3] applied with ε:=αc>0\varepsilon := \alpha - c > 0, and if α=+\alpha = +\infty then qk+q_k \to +\infty by [L6], so qk>cq_k > c eventually. Fix NN with qk>cq_k > c for all kNk \ge N; then ak+1caka_{k+1} \ge c\,a_k for kNk \ge N, so step 1.2 gives anCcna_n \ge C c^n for all nNn \ge N with C:=aNcN>0C := a_N c^{-N} > 0, and step 1.3 gives rkC1/(k+1)c=ukr_k \ge C^{1/(k+1)} c = u_k for every kNk \ge N. By step 1.4 and [L5], lim infkrklim infkuk=c\liminf_k r_k \ge \liminf_k u_k = c.

step 1.1step 1.2step 1.3step 1.4L3L5L6L12L14
3.1

Hence lim supkrklim supkqk\limsup_k r_k \le \limsup_k q_k. By step 1.1 the element β=lim supkqk\beta = \limsup_k q_k is 0\ge 0, so it is either ++\infty, which is step 1.5, or real. In the real case step 2.1 with ε=1\varepsilon = 1 gives lim supkrkβ+1\limsup_k r_k \le \beta + 1, a real, so lim supkrk+\limsup_k r_k \ne +\infty; if lim supkrk=\limsup_k r_k = -\infty it is β\le \beta; and otherwise it is a real SS, and S>βS > \beta would give, on choosing a natural m1m \ge 1 with 1/m<Sβ1/m < S - \beta and applying step 2.1 with ε=1/m\varepsilon = 1/m, the impossibility Sβ+1/m<SS \le \beta + 1/m < S. By totality lim supkrkβ\limsup_k r_k \le \beta.

step 2.1step 1.5step 1.1L2L11L12
3.2

Hence lim infkqklim infkrk\liminf_k q_k \le \liminf_k r_k. By step 1.1 the element α=lim infkqk\alpha = \liminf_k q_k is 0\ge 0, so it is 00, or a positive real, or ++\infty. The first case is step 2.2. If α\alpha is a positive real and lim infkrk<α\liminf_k r_k < \alpha, then lim infkrk\liminf_k r_k lies between the reals 00 and α\alpha by step 1.1 and is therefore real, so [L13] supplies a real cc with lim infkrk<c<α\liminf_k r_k < c < \alpha, necessarily c>0c > 0; step 2.3 then gives lim infkrkc\liminf_k r_k \ge c, contradicting c>lim infkrkc > \liminf_k r_k, so lim infkrkα\liminf_k r_k \ge \alpha by totality. If α=+\alpha = +\infty, step 2.3 gives lim infkrkc\liminf_k r_k \ge c for every real cc with c>0c > 0, so lim infkrk\liminf_k r_k is not -\infty, and it is not a real tt either, since t0t \ge 0 by step 1.1 and then c:=t+1>0c := t+1 > 0 would give tt+1t \ge t+1; hence lim infkrk=+=α\liminf_k r_k = +\infty = \alpha.

step 2.2step 2.3step 1.1L2L12L13
4.1

Combining the three links, lim infkqklim infkrk\liminf_k q_k \le \liminf_k r_k by step 3.2, lim infkrklim supkrk\liminf_k r_k \le \limsup_k r_k by [L4], and lim supkrklim supkqk\limsup_k r_k \le \limsup_k q_k by step 3.1.

step 3.1step 3.2L4

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For every p>0p > 0 and every positive rational α\alpha, nα/(1+p)n0n^{\alpha}/(1+p)^n \to 0

Statement

Let pRp \in \mathbb{R} with p>0p > 0 and let αQ\alpha \in \mathbb{Q} with α>0\alpha > 0. Write ι(n):=n1R\iota(n) := n \cdot 1_{\mathbb{R}} for the canonical natural, with ι(0):=0\iota(0) := 0, and let

wk  :=  ι(k)α(1+p)k(kN),w_k \;:=\; \frac{\iota(k)^{\alpha}}{(1+p)^{k}} \qquad (k \in \mathbb{N}),

the numerator being a rational power (Rational powers ara^r of a positive base) and the denominator an integer power (Integer powers ama^m). Then wk0w_k \to 0 (Limits and Cauchy sequences of reals).

Every term is defined, including the one at k=0k = 0. The supplementary clause of Rational powers ara^r of a positive base gives 0α=00^{\alpha} = 0 for rational α>0\alpha > 0, and (1+p)0=1(1+p)^0 = 1, so w0=0w_0 = 0. No index shift is therefore needed here, in contrast with the two root lemmas earlier on this page, where the exponent is the index.

In words: a fixed power of nn is beaten by any geometric sequence of ratio >1> 1, however small the excess pp and however large the exponent α\alpha.

Facts & Assumptions

Given: A real p>0p > 0 and a rational α>0\alpha > 0; the base β:=1+p>1\beta := 1 + p > 1; the canonical naturals ι(n)=n1R\iota(n) = n \cdot 1_{\mathbb{R}} with ι(0)=0\iota(0) = 0; and wk=ι(k)α/βkw_k = \iota(k)^{\alpha}/\beta^{k}.

[L1]

Rational powers: xrx^r is defined and positive for real x>0x > 0 and rational rr, and 0r=00^{r} = 0 for rational r>0r > 0; the integer power xmx^{m} is the rational power at exponent mm; (xy)r=xryr(xy)^{r} = x^{r} y^{r}, which persists for x,y0x, y \ge 0 when r>0r > 0; xr=1/xrx^{-r} = 1/x^{r}; and (xr)s=xrs(x^{r})^{s} = x^{rs} (Rational powers ara^r of a positive base, Laws of rational exponents, Integer powers ama^m, Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a).

[L2]

Monotonicity of rational powers: for rational t>0t > 0, x>1x > 1 implies xt>1x^{t} > 1; and for rational t>0t > 0, 0<x<y0 < x < y implies xt<ytx^{t} < y^{t} (Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}).

[L3]

Integer powers: x>0x > 0 implies xm>0x^{m} > 0, and xmxm=xm+mx^{m} x^{m'} = x^{m+m'}, (xm)m=xmm(x^{m})^{m'} = x^{m m'} for integer exponents with x0x \ne 0 (Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n, Laws of integer exponents).

[L4]

Bernoulli's inequality: (1+x)n1+ι(n)x(1+x)^{n} \ge 1 + \iota(n) x for real x1x \ge -1 and natural nn (Bernoulli's inequality (1+x)n1+nx(1+x)^n \ge 1 + nx).

[L5]

Canonical naturals: ι(n)>0\iota(n) > 0 and invertible for n1n \ge 1, and ι\iota is strictly increasing (Canonical naturals are positive and strictly increasing, Order on the natural numbers, \le is a linear order on N\mathbb{N}).

[L6]

Reciprocal Archimedean property: for every real η>0\eta > 0 there is a natural m1m \ge 1 with 1/m<η1/m < \eta; and 0<x<y0 < x < y gives 0<1/y<1/x0 < 1/y < 1/x (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L7]

Order arithmetic: Order is preserved by adding a constant and by adding inequalities and claim 4 of Sign rules for products and monotonicity of multiplication state the strict forms, that inequalities may be translated and added and that multiplication by a positive element preserves <<; adjoining the case of equality gives the nonstrict forms used below. Products of nonnegative inequalities multiply in the nonstrict form stated by Multiplying inequalities of positives, and the order is total (Ordered field).

[L8]

Convergence to 00: it suffices to produce, for every real ε>0\varepsilon > 0, a threshold beyond which zk<ε|z_k| < \varepsilon; and z=z|z| = z for z0z \ge 0 (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Basic properties of the absolute value).

Proof

technique · direct
1.1

Since α>0\alpha > 0 is rational, so is 1/α1/\alpha; put δ:=β1/α\delta := \beta^{1/\alpha} and θ:=δ1/2\theta := \delta^{1/2}. From β>1\beta > 1 and 1/α>01/\alpha > 0 we get δ>1\delta > 1, and from δ>1\delta > 1 and 1/2>01/2 > 0 we get θ>1\theta > 1; hence θ1>0\theta - 1 > 0 and δ>0\delta > 0, θ>0\theta > 0.

givenL1L2L7
1.2

For every natural nn one has δn=θnθn\delta^{n} = \theta^{n} \theta^{n}, because θ2=(δ1/2)2=δ\theta^{2} = (\delta^{1/2})^{2} = \delta and therefore δn=(θ2)n=θ2n=θnθn\delta^{n} = (\theta^{2})^{n} = \theta^{2n} = \theta^{n} \theta^{n}.

givenL1L3
1.3

For every natural kk one has wk=ukαw_k = u_k^{\alpha}, where uk:=ι(k)/δku_k := \iota(k)/\delta^{k}. Indeed uk=ι(k)(1/δk)u_k = \iota(k) \cdot (1/\delta^{k}) with both factors 0\ge 0, so ukα=ι(k)α(1/δk)α=ι(k)α/(δk)αu_k^{\alpha} = \iota(k)^{\alpha} \big(1/\delta^{k}\big)^{\alpha} = \iota(k)^{\alpha}/\big(\delta^{k}\big)^{\alpha}, and (δk)α=δkα=(β1/α)kα=β(1/α)(kα)=βk\big(\delta^{k}\big)^{\alpha} = \delta^{k\alpha} = \big(\beta^{1/\alpha}\big)^{k\alpha} = \beta^{(1/\alpha)(k\alpha)} = \beta^{k}.

givenL1L3
2.1

For every natural n1n \ge 1 one has 0un<1/(ι(n)(θ1)(θ1))0 \le u_n < 1/\big(\iota(n)(\theta-1)(\theta-1)\big). Bernoulli's inequality applied to θ1>0\theta - 1 > 0 gives θn1+ι(n)(θ1)>ι(n)(θ1)>0\theta^{n} \ge 1 + \iota(n)(\theta-1) > \iota(n)(\theta-1) > 0, so multiplying this inequality by itself gives δn=θnθn>ι(n)(θ1)ι(n)(θ1)>0\delta^{n} = \theta^{n}\theta^{n} > \iota(n)(\theta-1)\iota(n)(\theta-1) > 0; dividing the positive ι(n)\iota(n) by the two positive quantities reverses the inequality and yields un=ι(n)/δn<ι(n)/(ι(n)ι(n)(θ1)(θ1))=1/(ι(n)(θ1)(θ1))u_n = \iota(n)/\delta^{n} < \iota(n)/\big(\iota(n)\iota(n)(\theta-1)(\theta-1)\big) = 1/\big(\iota(n)(\theta-1)(\theta-1)\big), while un0u_n \ge 0 because ι(n)>0\iota(n) > 0 and δn>0\delta^{n} > 0.

step 1.1step 1.2L3L4L5L6L7
3.1

The sequence (uk)(u_k) converges to 00. Note first u0=ι(0)/δ0=0/1=0u_0 = \iota(0)/\delta^{0} = 0/1 = 0. Given a real ε>0\varepsilon > 0, put η:=ε(θ1)(θ1)>0\eta := \varepsilon(\theta-1)(\theta-1) > 0 and take a natural m1m \ge 1 with 1/m<η1/m < \eta. For kmk \ge m we have ι(k)ι(m)>0\iota(k) \ge \iota(m) > 0, hence 1/ι(k)1/ι(m)<η1/\iota(k) \le 1/\iota(m) < \eta, and therefore 0uk<1/(ι(k)(θ1)(θ1))<η/((θ1)(θ1))=ε0 \le u_k < 1/\big(\iota(k)(\theta-1)(\theta-1)\big) < \eta/\big((\theta-1)(\theta-1)\big) = \varepsilon, so uk<ε|u_k| < \varepsilon.

step 2.1L5L6L7L8
4.1

The sequence (wk)(w_k) converges to 00. Given a real ε>0\varepsilon > 0, the element ε1/α\varepsilon^{1/\alpha} is a positive real, so by step 3.1 there is a threshold beyond which 0uk<ε1/α0 \le u_k < \varepsilon^{1/\alpha}. For such kk: if uk=0u_k = 0 then wk=0α=0<εw_k = 0^{\alpha} = 0 < \varepsilon, and if uk>0u_k > 0 then monotonicity of the rational power α\alpha in the base gives wk=ukα<(ε1/α)α=ε(1/α)α=εw_k = u_k^{\alpha} < \big(\varepsilon^{1/\alpha}\big)^{\alpha} = \varepsilon^{(1/\alpha)\alpha} = \varepsilon. In both cases wk=wk<ε|w_k| = w_k < \varepsilon, so wk0w_k \to 0.

step 3.1step 1.3L1L2L8

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For every real xx, xk/k!0x^k/k! \to 0

Statement

Write ι(n):=n1R\iota(n) := n \cdot 1_{\mathbb{R}} for the canonical natural (Canonical naturals are positive and strictly increasing) and define the factorial as the finite product (Finite sums and finite products, by recursion)

k!  :=  j<kι(j+1)(kN),k! \;:=\; \prod_{j < k} \iota(j+1) \qquad (k \in \mathbb{N}),

so that 0!=10! = 1, the empty product, and (k+1)!=k!ι(k+1)(k+1)! = k! \cdot \iota(k+1). Every k!k! is a positive real. Then, for every xRx \in \mathbb{R},

xkk!0,\frac{x^{k}}{k!} \longrightarrow 0 ,

the numerator being the integer power of Integer powers ama^m and the convergence that of Limits and Cauchy sequences of reals.

The index range needs no adjustment: k!k! is defined at k=0k = 0 with value 11, and x0=1x^0 = 1, so the sequence begins with x0/0!=1x^0/0! = 1.

Facts & Assumptions

Given: A real xx; the modulus M:=x0M := |x| \ge 0; the factorials k!=j<kι(j+1)k! = \prod_{j<k}\iota(j+1); and the canonical naturals ι(n)=n1R\iota(n) = n \cdot 1_{\mathbb{R}}.

[A1]

P(j)P(j) denotes the statement MN+j/(N+j)!AλjM^{N+j}/(N+j)! \le A \lambda^{j}, where NN, λ\lambda and AA are fixed in step 1.3.

[L1]

Finite products: the empty product is 11, j<m+1aj=(j<maj)am\prod_{j<m+1} a_j = \big(\prod_{j<m} a_j\big) a_m, and a product of positive factors is positive (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L2]

Integer powers: z0=1z^{0} = 1, zm+1=zmzz^{m+1} = z^{m} z, and z0z \ge 0 implies zm0z^{m} \ge 0 (Integer powers ama^m, Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n, Laws of integer exponents).

[L3]

Absolute value: zw=zw|zw| = |z||w|, z0|z| \ge 0, and z=z|z| = z for z0z \ge 0 (Basic properties of the absolute value).

[L4]
[L5]

Canonical naturals: ι(n)>0\iota(n) > 0 and invertible for n1n \ge 1, ι\iota is strictly increasing, and for every real yy there is a natural N1N \ge 1 with y<ι(N)y < \iota(N) (Canonical naturals are positive and strictly increasing, Every complete ordered field is Archimedean, Order on the natural numbers, \le is a linear order on N\mathbb{N}).

[L6]

Order arithmetic: Inverses of positives are positive, and reciprocation reverses order, claim 4 of Sign rules for products and monotonicity of multiplication and Order is preserved by adding a constant and by adding inequalities state the strict forms, that 0<u<v0 < u < v gives 0<1/v<1/u0 < 1/v < 1/u, that multiplication by a positive element preserves <<, and that inequalities may be translated and added; adjoining the case of equality gives the nonstrict forms used below, and multiplication by 00 sends both sides to 00, so a nonnegative multiplier preserves \le. Products of nonnegative inequalities multiply in the nonstrict form stated by Multiplying inequalities of positives.

[L7]

Geometric sequences: r<1|r| < 1 implies rj0r^{j} \to 0 (For r<1|r| < 1 the sequence rkr^k is null, and for r>1|r| > 1 the sequence rk|r|^k diverges to ++\infty); a scalar multiple of a convergent sequence converges to the scalar multiple of the limit (Algebra of limits: sums, scalar multiples, products and quotients).

[L8]

Squeeze theorem, and the fact that a constant sequence converges to its value (The squeeze theorem, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L9]

A sequence converges to zz if and only if some tail of it does; the KK-th tail of (zk)(z_k) is jzj+Kj \mapsto z_{j+K} (Convergence depends only on the tail, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Proof

technique · induction
1.1

Each k!k! is a product of the positive reals ι(j+1)\iota(j+1), j<kj < k, hence positive, and (k+1)!=k!ι(k+1)(k+1)! = k! \cdot \iota(k+1); also M=x0M = |x| \ge 0.

givenL1L3L5
1.2

For every kNk \in \mathbb{N} one has xk=Mk|x^{k}| = M^{k}: at k=0k = 0 both sides are 1=1=M0|1| = 1 = M^{0}, and if xk=Mk|x^{k}| = M^{k} then xk+1=xkx=xkx=MkM=Mk+1|x^{k+1}| = |x^{k} x| = |x^{k}||x| = M^{k} M = M^{k+1}, so this follows by induction on kk.

givenL2L3L4
1.3

Take a natural N1N \ge 1 with M<ι(N)M < \iota(N) and put λ:=M/ι(N)\lambda := M/\iota(N) and A:=MN/N!A := M^{N}/N!. Then 0λ<10 \le \lambda < 1, since 0M<ι(N)0 \le M < \iota(N) and ι(N)>0\iota(N) > 0, and A0A \ge 0.

givenL1L2L5L6choose
1.4

The statement P(0)P(0) holds, with equality: MN+0/(N+0)!=MN/N!=A=A1=Aλ0M^{N+0}/(N+0)! = M^{N}/N! = A = A \cdot 1 = A\lambda^{0}.

givenA1L2base
1.5

Fix jNj \in \mathbb{N} and assume P(j)P(j), that is MN+j/(N+j)!AλjM^{N+j}/(N+j)! \le A\lambda^{j}.

A1ih
2.1

Then P(j+1)P(j+1) holds. Indeed MN+j+1/(N+j+1)!=(MN+j/(N+j)!)(M/ι(N+j+1))M^{N+j+1}/(N+j+1)! = \big(M^{N+j}/(N+j)!\big)\big(M/\iota(N+j+1)\big), and N+j+1>NN + j + 1 > N gives ι(N+j+1)>ι(N)>0\iota(N+j+1) > \iota(N) > 0, hence 0M/ι(N+j+1)M/ι(N)=λ0 \le M/\iota(N+j+1) \le M/\iota(N) = \lambda; since also 0MN+j/(N+j)!Aλj0 \le M^{N+j}/(N+j)! \le A\lambda^{j} by step 1.5 and Aλj0A\lambda^{j} \ge 0, multiplying the two nonnegative inequalities gives MN+j+1/(N+j+1)!Aλjλ=Aλj+1M^{N+j+1}/(N+j+1)! \le A\lambda^{j}\lambda = A\lambda^{j+1}.

step 1.5A1L1L2L5L6
3.1

By the induction principle P(j)P(j) holds for every jNj \in \mathbb{N}, and MN+j/(N+j)!0M^{N+j}/(N+j)! \ge 0 always, so 0MN+j/(N+j)!Aλj0 \le M^{N+j}/(N+j)! \le A\lambda^{j} for every jj.

step 1.4step 2.1A1L1L2L4
4.1

Since λ=λ<1|\lambda| = \lambda < 1, the sequence (λj)j(\lambda^{j})_j converges to 00, hence so does (Aλj)j(A\lambda^{j})_j; the constant sequence 00 also converges to 00, so the squeeze theorem applied to step 3.1 shows that the NN-th tail jMN+j/(N+j)!j \mapsto M^{N+j}/(N+j)! converges to 00, and therefore (Mk/k!)k(M^{k}/k!)_k converges to 00. Finally xk/k!0=xk/k!=Mk/k!|x^{k}/k! - 0| = |x^{k}|/k! = M^{k}/k! by steps 1.1 and 1.2, so xk/k!0x^{k}/k! \to 0.

step 3.1step 1.1step 1.2L3L7L8L9discharge-induction

Remarks

RemarkRemark: AI-generatedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

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

Conventions: sup\sup \emptyset, unbounded sets, and the extended reals refused, inside R\mathbb{R}, the conventions supS=+\sup S = +\infty and inf=+\inf \emptyset = +\infty, and promised that a later page needing R\overline{\mathbb{R}} would introduce it explicitly as a new object with its own order and its own partial arithmetic. The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined is that introduction, and this page is the one that needed it. Nothing about the real supremum has changed: supS\sup S and infS\inf S for SRS \subseteq \mathbb{R} are still real numbers, still defined only under the nonempty and bounded hypotheses, and the extended bounds 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} are a different operation in a different ordered set, agreeing with the real one exactly where the real one is defined.

What is defined. On R\overline{\mathbb{R}} this library defines exactly three things: the total order, the reflection aaa \mapsto -a, and the two partial operations a+ba + b and abab. The order and the reflection are total. The two operations are not, and the gaps are these.

expressionstatus
a+ba + b with a,bRa, b \in \mathbb{R}the field sum
(+)+b(+\infty) + b with bb \ne -\infty++\infty
()+b(-\infty) + b with b+b \ne +\infty-\infty
(+)+()(+\infty) + (-\infty) and ()+(+)(-\infty) + (+\infty)undefined
abab with a,bRa, b \in \mathbb{R}the field product
(±)b(\pm\infty) \cdot b with b0b \ne 0±\pm\infty, by the sign rule
0(±)0 \cdot (\pm\infty) and (±)0(\pm\infty) \cdot 0undefined

What is not defined at all. There is no subtraction on R\overline{\mathbb{R}}, no division, no absolute value and no exponentiation. Where a proof on this page wants aba - b it writes a+(b)a + (-b), which inherits the gap at {+,}\{+\infty, -\infty\}; where it wants a quotient it does not write one. In particular the expressions (+)(+)(+\infty) - (+\infty), (+)/(+)(+\infty)/(+\infty) and 0/00/0 do not occur here, not because they are hard but because neither operation exists.

Why the two gaps are gaps. They are the two places where the value is not determined by the sequences involved, so no assignment could be compatible with limits. For the product this is proved: Null times divergent has no rule: xk=1/kx_k = 1/k with yk=cky_k = ck gives product limit cc, and with yk=k2y_k = k^2 gives divergence exhibits a null sequence and sequences diverging to ++\infty whose products behave differently, so 0(+)0 \cdot (+\infty) has no value that would make a product rule true. For the sum the same is visible with ak=ka_k = k and bk=kb_k = -k, whose sum is constantly 00, against ak=ka_k = k and bk=2kb_k = -2k, whose sum diverges to -\infty; both pairs have lim supak=+\limsup a_k = +\infty and lim supbk=\limsup b_k = -\infty.

Where each statement on this page carries the hypothesis. Reading the page in order, the pattern is that everything purely order-theoretic is unconditional and everything arithmetic is not.

What this costs a reader coming from a measure-theory text. Such a text typically declares 0:=00 \cdot \infty := 0, which is genuinely convenient there, because in an integral the factor 00 is a measure-zero set and the convention makes countable additivity work without cases. That convention is not in force here, and it is not compatible with limits: it is a decision about a particular formula, not a fact about R\overline{\mathbb{R}}. A statement quoted from such a source therefore needs its degenerate cases restored before it can be used with the results on this page.

One thing that is not a convention. The equations lim supkxk=+\limsup_k x_k = +\infty and lim infkxk=\liminf_k x_k = -\infty occurring throughout this page are ordinary equations between elements of R\overline{\mathbb{R}}, not abbreviations. That is precisely the difference from Divergence to ++\infty and to -\infty, where "xk+x_k \to +\infty" is a single abbreviation for a condition and no object named ++\infty is involved. Both readings coexist without conflict, and A real sequence converges to LRL \in \mathbb{R} iff lim infxk=lim supxk=L\liminf x_k = \limsup x_k = L, and diverges to ±\pm\infty iff both equal ±\pm\infty is the statement that relates them.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

FALSE: lim sup(xk+yk)=lim supxk+lim supyk\limsup(x_k + y_k) = \limsup x_k + \limsup y_k

Statement

False claim: for all sequences (xk)(x_k), (yk)(y_k) of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) whose limit superiors have a defined sum in 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),

lim supk(xk+yk)  =  lim supkxk+lim supkyk.\limsup_{k}(x_k + y_k) \;=\; \limsup_{k} x_k + \limsup_{k} y_k .

The corresponding statement with == replaced by \le is true and is lim sup(xk+yk)lim supxk+lim supyk\limsup(x_k + y_k) \le \limsup x_k + \limsup y_k whenever the right-hand side is defined in R\overline{\mathbb{R}}, and dually for lim inf\liminf. The claim above is what one gets by strengthening that inequality to an equality, and it fails: the two sides can differ by as much as the whole oscillation of the sequences, because the two limit superiors may be attained along different sets of indices while the sum of the sequences never sees either of them.

The witness is xk=(1)kx_k = (-1)^k and yk=(1)ky_k = -(-1)^k, refuted below; it is recorded separately as a named counterexample on the companion page.

Facts & Assumptions

[L2]

A strictly increasing index map satisfies njjn_j \ge j (A strictly increasing index map satisfies nkkn_k \ge k).

[L4]

The order on R\overline{\mathbb{R}} is total and restricts on R\mathbb{R} to the order of R\mathbb{R}; ±\pm\infty are not real (The extended real line R=R{,+}\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}, its order, and the arithmetic that is left undefined).

[L5]

Absolute value: t=1|t| = 1 forces t=1t = 1 or t=1t = -1 (Basic properties of the absolute value, Absolute value in an ordered field).

[L6]

Order arithmetic: 0<10 < 1, so 1<1-1 < 1 and 0<1+1=20 < 1 + 1 = 2; in particular 020 \ne 2 (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Ordered field, Complete ordered field (least-upper-bound property)).

[L7]

Subadditivity: lim supk(zk+wk)lim supkzk+lim supkwk\limsup_k(z_k + w_k) \le \limsup_k z_k + \limsup_k w_k whenever the right-hand side is defined (lim sup(xk+yk)lim supxk+lim supyk\limsup(x_k + y_k) \le \limsup x_k + \limsup y_k whenever the right-hand side is defined in R\overline{\mathbb{R}}, and dually for lim inf\liminf).

[L8]

The refuted claim: for all sequences whose limit superiors have a defined sum, lim supk(zk+wk)=lim supkzk+lim supkwk\limsup_k(z_k + w_k) = \limsup_k z_k + \limsup_k w_k.

Refutation

technique · direct
1.1

The sequences xk=skx_k = s_k and yk=sky_k = -s_k are sequences of reals, and xk+yk=sk+(sk)=0x_k + y_k = s_k + (-s_k) = 0 for every kk.

givenL1
1.2

Every value sks_k is 11 or 1-1, since sk=1|s_k| = 1; and for every nn both values occur at an index n\ge n, since sen=1s_{e_n} = 1 with enne_n \ge n and son=1s_{o_n} = -1 with onno_n \ge n.

givenL1L2L5
2.1

Hence Tn(x)={1,1}T_n(x) = \{1, -1\} for every nn. Its least upper bound in R\overline{\mathbb{R}} is 11: the element 11 bounds both 11 and 1-1 from above because 1<1-1 < 1, and any upper bound uu satisfies 1u1 \le u because 1Tn(x)1 \in T_n(x). So supTn(x)=1\sup T_n(x) = 1 for every nn, and lim supkxk\limsup_k x_k is the greatest lower bound of the one-element family {1}\{1\}, namely 11.

step 1.2L3L4L6
2.2

The sequence yk=sky_k = -s_k takes the value 11 at every ono_n and the value 1-1 at every ene_n, and takes no other value, so Tn(y)={1,1}T_n(y) = \{1, -1\} for every nn as well, and the same computation gives lim supkyk=1\limsup_k y_k = 1.

step 1.2L1L2L3L4L5L6
2.3

The sum sequence is constantly 00, so Tn(x+y)={0}T_n(x+y) = \{0\}, whose least upper bound is 00, and lim supk(xk+yk)=0\limsup_k(x_k + y_k) = 0.

step 1.1L3L4
3.1

Both limit superiors are the real number 11, so their sum is defined and equals 1+1=21 + 1 = 2, and the claim asserts 0=20 = 2 for this pair. But 0<20 < 2, so 020 \ne 2 and the claim fails.

step 2.1step 2.2step 2.3L6L8
4.1

The claim is therefore false. What survives is the inequality of [L7], which for this pair reads 020 \le 2 and is strict.

step 3.1L7L8

Remarks

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

FALSE: lim supak1/k=lim supak+1/ak\limsup a_k^{1/k} = \limsup a_{k+1}/a_k for every positive sequence

Statement

False claim: for every sequence (ak)(a_k) of reals with ak>0a_k > 0 for all kk,

lim supkak+11/(k+1)  =  lim supkak+1ak,\limsup_{k} a_{k+1}^{1/(k+1)} \;=\; \limsup_{k} \frac{a_{k+1}}{a_k},

that is, the limit superior of the root sequence equals the limit superior of the ratio sequence. (The root family is written with the shift of For ak>0a_k > 0: lim infak+1/aklim infak1/klim supak1/klim supak+1/ak\liminf a_{k+1}/a_k \le \liminf a_k^{1/k} \le \limsup a_k^{1/k} \le \limsup a_{k+1}/a_k, since ak1/ka_k^{1/k} is undefined at k=0k = 0; classically the claim reads lim supnan1/n=lim supnan+1/an\limsup_n a_n^{1/n} = \limsup_n a_{n+1}/a_n.)

What is true is the chain lim infkak+1ak    lim infkak+11/(k+1)    lim supkak+11/(k+1)    lim supkak+1ak\liminf_{k} \frac{a_{k+1}}{a_k} \;\le\; \liminf_{k} a_{k+1}^{1/(k+1)} \;\le\; \limsup_{k} a_{k+1}^{1/(k+1)} \;\le\; \limsup_{k} \frac{a_{k+1}}{a_k} of For ak>0a_k > 0: lim infak+1/aklim infak1/klim supak1/klim supak+1/ak\liminf a_{k+1}/a_k \le \liminf a_k^{1/k} \le \limsup a_k^{1/k} \le \limsup a_{k+1}/a_k. The claim above collapses its right-hand inequality to an equality, and that fails: the roots can converge while the ratios oscillate. This is exactly why a root criterion decides cases that a ratio criterion cannot.

The witness is ak=2k+(1)ka_k = 2^{-k + (-1)^k}. The computation below establishes all four quantities for it, namely lim infkak+1ak=18,lim supkak+1ak=2,limkak+11/(k+1)=12,\liminf_{k} \frac{a_{k+1}}{a_k} = \frac{1}{8}, \qquad \limsup_{k} \frac{a_{k+1}}{a_k} = 2, \qquad \lim_{k} a_{k+1}^{1/(k+1)} = \frac{1}{2}, and it is recorded as a named example on the companion page.

Facts & Assumptions

Given: The alternating sequence (sk)(s_k) and the index maps e,oe, o of The even and odd index maps and the alternating sequence: strictly increasing e,oe, o with N\mathbb{N} their disjoint union, and the unique (sk)(s_k) with s0=1s_0 = 1, sσ(k)=sks_{\sigma(k)} = -s_k, which satisfies sk=1|s_k| = 1, se1s \circ e \equiv 1 and so1s \circ o \equiv -1; the sequence tkt_k defined to be 22 when sk=1s_k = 1 and 1/21/2 when sk=1s_k = -1; the sequence ak:=2ktka_k := 2^{-k} t_k; the ratios qk:=ak+1/akq_k := a_{k+1}/a_k and the roots rk:=ak+11/(k+1)r_k := a_{k+1}^{1/(k+1)}.

[L1]

The alternating sequence: s0=1s_0 = 1, sk+1=sks_{k+1} = -s_k, sk=1|s_k| = 1 for every kk, sej=1s_{e_j} = 1 and soj=1s_{o_j} = -1, and ee, oo are strictly increasing (The even and odd index maps and the alternating sequence: strictly increasing e,oe, o with N\mathbb{N} their disjoint union, and the unique (sk)(s_k) with s0=1s_0 = 1, sσ(k)=sks_{\sigma(k)} = -s_k, which satisfies sk=1|s_k| = 1, se1s \circ e \equiv 1 and so1s \circ o \equiv -1); a strictly increasing index map satisfies njjn_j \ge j (A strictly increasing index map satisfies nkkn_k \ge k).

[L4]

Powers and roots of positive reals: integer powers with 2m2m=2m+m2^{m} 2^{m'} = 2^{m+m'} and 2m=1/2m2^{-m} = 1/2^{m}; (xy)1/n=x1/ny1/n(xy)^{1/n} = x^{1/n} y^{1/n}; the integer power is the rational power at an integer exponent, so (2n)1/n=2n/n=21\big(2^{-n}\big)^{1/n} = 2^{-n/n} = 2^{-1}; roots of positive reals are positive; and 0<xy0 < x \le y implies x1/ny1/nx^{1/n} \le y^{1/n} (Integer powers ama^m, Laws of integer exponents, Rational powers ara^r of a positive base, Laws of rational exponents, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}, Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a).

[L5]

For every real b>0b > 0 the sequence b1/(k+1)b^{1/(k+1)} converges to 11 (For every a>0a > 0, a1/n1a^{1/n} \to 1).

[L7]

Absolute value and order: t=1|t| = 1 forces t=1t = 1 or t=1t = -1; 0<10 < 1, so 1/2<1<21/2 < 1 < 2 and 1/8<21/8 < 2, and 1/221/2 \ne 2; reciprocals reverse the order; multiplying by a positive preserves it (Basic properties of the absolute value, Absolute value in an ordered field, The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)).

[L9]

The refuted claim: for every sequence of positive reals, lim supkak+11/(k+1)=lim supkak+1/ak\limsup_k a_{k+1}^{1/(k+1)} = \limsup_k a_{k+1}/a_k.

Refutation

technique · direct
1.1

Each sks_k is 11 or 1-1 because sk=1|s_k| = 1, so tkt_k is well defined, with tk{2,1/2}t_k \in \{2, 1/2\} and tk>0t_k > 0; hence ak=2ktk>0a_k = 2^{-k} t_k > 0 for every kk, and (ak)(a_k) is a sequence of positive reals to which the claim applies. This is the sequence usually written ak=2k+(1)ka_k = 2^{-k + (-1)^k}.

givenL1L4L7L9
1.2

Since sk+1=sks_{k+1} = -s_k and 111 \ne -1, exactly one of the two situations "sk=1s_k = 1 and sk+1=1s_{k+1} = -1" and "sk=1s_k = -1 and sk+1=1s_{k+1} = 1" occurs at each index kk. In the first, tk=2t_k = 2 and tk+1=1/2t_{k+1} = 1/2; in the second, tk=1/2t_k = 1/2 and tk+1=2t_{k+1} = 2.

givenL1L7
1.3

For every nn both values of ss occur at an index n\ge n: sen=1s_{e_n} = 1 with enne_n \ge n and son=1s_{o_n} = -1 with onno_n \ge n.

givenL1
2.1

The ratios are qk=ak+1/ak=(2(k+1)tk+1)/(2ktk)=21tk+1/tkq_k = a_{k+1}/a_k = \big(2^{-(k+1)} t_{k+1}\big)/\big(2^{-k} t_k\big) = 2^{-1} t_{k+1}/t_k, which by step 1.2 equals 21(1/2)/2=1/82^{-1}(1/2)/2 = 1/8 when sk=1s_k = 1 and 212/(1/2)=22^{-1} \cdot 2/(1/2) = 2 when sk=1s_k = -1.

step 1.1step 1.2L4L7algebra
2.2

The roots are rk=(2(k+1)tk+1)1/(k+1)=(2(k+1))1/(k+1)tk+11/(k+1)=21tk+11/(k+1)r_k = \big(2^{-(k+1)} t_{k+1}\big)^{1/(k+1)} = \big(2^{-(k+1)}\big)^{1/(k+1)} t_{k+1}^{1/(k+1)} = 2^{-1} t_{k+1}^{1/(k+1)}.

step 1.1L4
2.3

Since 1/2tk+121/2 \le t_{k+1} \le 2 for every kk and xx1/(k+1)x \mapsto x^{1/(k+1)} is nondecreasing on the positive reals, (1/2)1/(k+1)tk+11/(k+1)21/(k+1)(1/2)^{1/(k+1)} \le t_{k+1}^{1/(k+1)} \le 2^{1/(k+1)}; both bounding sequences converge to 11 by [L5], so the squeeze theorem gives tk+11/(k+1)1t_{k+1}^{1/(k+1)} \to 1.

step 1.1L4L5L6L7
3.1

By steps 1.2 and 1.3 the tail range of (qk)(q_k) at every index nn is exactly {1/8,2}\{1/8, 2\}: those are the only values, and each occurs at some index n\ge n. Its least upper bound in R\overline{\mathbb{R}} is 22 and its greatest lower bound is 1/81/8, since 1/8<21/8 < 2 and both belong to the set; hence lim supkqk\limsup_k q_k is the greatest lower bound of {2}\{2\}, namely 22, and lim infkqk\liminf_k q_k is the least upper bound of {1/8}\{1/8\}, namely 1/81/8.

step 2.1step 1.3L2L7
3.2

By steps 2.2 and 2.3 and the scalar rule, rk=21tk+11/(k+1)211=1/2r_k = 2^{-1} t_{k+1}^{1/(k+1)} \to 2^{-1} \cdot 1 = 1/2, so lim supkrk=lim infkrk=1/2\limsup_k r_k = \liminf_k r_k = 1/2.

step 2.2step 2.3L3L6
4.1

For this sequence the claim asserts lim supkrk=lim supkqk\limsup_k r_k = \limsup_k q_k, that is 1/2=21/2 = 2; but 1/2<1<21/2 < 1 < 2, so the two are different and the claim fails.

step 3.1step 3.2L7L9
5.1

The claim is therefore false. The true chain [L8] reads here 1/81/21/221/8 \le 1/2 \le 1/2 \le 2, so both outer inequalities are strict for this witness while the middle one is an equality.

step 4.1step 3.1step 3.2L7L8L9

Remarks

Sources

Standard references

Recommended treatments; not extraction sources.