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

How statement and proof provenance work

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

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

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

For finite $L$ : $L = lim sup x_{k}$ iff for every $ε > 0$ one has $x_{k} < L + ε$ eventually and $x_{k} > L - ε$ frequently

Statement

Let $(x_{k})$ be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and let $L \in R$ , with eventually and frequently as in Sequences of reals: bounded, eventually, frequently, tails, subsequences and $lim sup$ , $lim inf$ as in Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ .

$L = {lim sup}_{k} x_{k}$ if and only if for every real $ε > 0$ $x_{k} < L + ε eventually and x_{k} > L - ε frequently .$
Dually, $L = {lim inf}_{k} x_{k}$ if and only if for every real $ε > 0$ $x_{k} > L - ε eventually and x_{k} < L + ε frequently .$

The hypothesis $L \in R$ is not a restriction that can be lifted. Both conditions are stated with real $ε$ and real $L \pm ε$ , so neither has a reading at $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 sup}_{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 $(x_{k})$ of reals, a real number $L$ , the tail ranges $T_{n} = {x_{k} : k \geq n}$ , the extended tail suprema $s_{n} = \sup T_{n}$ , and $Λ : = {lim sup}_{k} x_{k} = \inf {s_{n} : n \in N}$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ).

[L1]

$Λ$ and every $s_{n}$ exist in $\overline{R}$ for every sequence, and $Λ$ is the greatest lower bound of ${s_{n}}$ while $s_{n}$ is the least upper bound of $T_{n}$ (Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ , The tail suprema of any real sequence are nonincreasing in $\overline{R}$ , so the limit superior exists for every sequence, Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L2]

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

[L3]

A property $P$ of indices holds eventually when it holds for all $k \geq K$ for some $K$ , and frequently when for every $K$ it holds for some $k \geq K$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L4]

Reciprocal Archimedean property: for every real $η > 0$ there is a natural $m \geq 1$ with $1 / m < η$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L5]

Order arithmetic in $R$ : for $ε > 0$ one has $L - ε < L < L + ε$ , and $a < b$ if and only if $- b < - a$ , both by translation invariance; the order is total, so exactly one of $a < b$ , $a = b$ , $b < a$ holds and $a < 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 sup}_{k} (- x_{k}) = - {lim inf}_{k} x_{k}$ and ${lim inf}_{k} (- x_{k}) = - {lim sup}_{k} x_{k}$ ( $lim sup (- x_{k}) = - lim inf (x_{k})$ , with the reflection of $\overline{R}$ exchanging $\pm \infty$ ).

Proof

technique · direct

1.1

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

assume-hypL1

1.2

For the converse implication of claim 1, assume that for every real $ε > 0$ the sequence satisfies $x_{k} < L + ε$ eventually and $x_{k} > L - ε$ frequently.

assume-hypL3

2.1

Under the assumption of step 1.1, $L + ε > L = Λ$ , so $L + ε$ is not a lower bound of ${s_{n}}$ , since $Λ$ is the greatest lower bound; by totality there is $n$ with $s_{n} < L + ε$ . For every $k \geq n$ we have $x_{k} \leq s_{n}$ , hence $x_{k} < L + ε$ ; so $x_{k} < L + ε$ eventually.

step 1.1L1L2L3L5

2.2

Under the assumption of step 1.1, fix $n \in N$ . Then $Λ \leq s_{n}$ because $Λ$ is a lower bound of ${s_{n}}$ , and $L - ε < L = Λ$ , so $L - ε < s_{n}$ . Hence $L - ε$ is not an upper bound of $T_{n}$ , for an upper bound $u$ of $T_{n}$ satisfies $s_{n} \leq u$ ; by totality of the order on $R$ there is therefore $k \geq n$ with $x_{k} > L - ε$ . As $n$ was arbitrary, $x_{k} > L - ε$ frequently.

step 1.1L1L2L3L5

2.3

Under the assumption of step 1.2, let $ε > 0$ be a real and take $N$ with $x_{k} < L + ε$ for all $k \geq N$ . Then $L + ε$ is an upper bound of $T_{N}$ , so $s_{N} \leq L + ε$ by leastness, and $Λ \leq s_{N}$ because $Λ$ is a lower bound of ${s_{n}}$ ; hence $Λ \leq L + ε$ .

step 1.2L1L2L3

2.4

Under the assumption of step 1.2, let $ε > 0$ be a real and fix $n$ . There is $k \geq n$ with $x_{k} > L - ε$ , and $x_{k} \leq s_{n}$ , so $L - ε < s_{n}$ and in particular $L - ε \leq s_{n}$ . As $n$ was arbitrary, $L - ε$ is a lower bound of ${s_{n}}$ , so $L - ε \leq Λ$ by greatest-lower-boundedness.

step 1.2L1L2L3

3.1

Taking $ε = 1$ in steps 2.3 and 2.4 gives $L - 1 \leq Λ \leq L + 1$ with $L \pm 1$ real, so $Λ$ is neither $+ \infty$ nor $- \infty$ and is therefore a real number. Suppose $Λ > L$ and put $δ : = Λ - L > 0$ ; choosing a natural $m \geq 1$ with $1 / m < δ$ and applying step 2.3 with $ε = 1 / m$ gives $Λ \leq L + 1 / m < L + δ = Λ$ , which is impossible. Suppose instead $Λ < L$ and put $δ : = L - Λ > 0$ ; choosing $m \geq 1$ with $1 / m < δ$ and applying step 2.4 with $ε = 1 / m$ gives $L - 1 / m \leq Λ$ , that is $δ = L - Λ \leq 1 / m < δ$ , again impossible. By trichotomy $Λ = 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 inf}_{k} x_{k}$ holds exactly when $- L = - {lim inf}_{k} x_{k} = {lim sup}_{k} (- x_{k})$ , since negation is injective on $\overline{R}$ . Applying claim 1 to the sequence $(- x_{k})$ and the real number $- L$ , that holds exactly when for every real $ε > 0$ one has $- x_{k} < - L + ε$ eventually and $- x_{k} > - L - ε$ frequently. Negating each of the two inequalities reverses it, turning them into $x_{k} > L - ε$ eventually and $x_{k} < L + ε$ frequently, which is claim 2.

step 4.1L5L6∎

Remarks

The two halves are not interchangeable. "Eventually below $L + ε$ " says $L$ is not exceeded in the long run; "frequently above $L - ε$ " says $L$ is approached again and again. Weakening the first to frequently would make the condition hold for $L = lim inf$ as well, and strengthening the second to eventually would force convergence, which is exactly the extra content of A real sequence converges to $L \in R$ iff $lim inf x_{k} = lim sup x_{k} = L$ , and diverges to $\pm \infty$ iff both equal $\pm \infty$ .
Real $ε$ is used throughout, and no rational test is involved. Neither condition is a convergence statement, so Limits and Cauchy sequences of reals and its quantification over rational $ε$ do not enter. Where a convergence hypothesis has to be fed into this lemma, as in A real sequence converges to $L \in R$ iff $lim inf x_{k} = lim sup x_{k} = L$ , and diverges to $\pm \infty$ iff both equal $\pm \infty$ , the passage between rational and real $ε$ is made there, by the sanctioned remark of Sequences of reals: bounded, eventually, frequently, tails, subsequences.
Why the epsilon lemmas for the real supremum are not cited. Epsilon characterisation of the supremum and Epsilon characterisation of the infimum characterise the real supremum and infimum of a nonempty set bounded on the relevant side. Here $s_{n}$ may be $+ \infty$ and the family ${s_{n}}$ may be unbounded below in $R$ , so neither lemma applies to the sets actually in play; the corresponding steps above are made directly from the least-upper-bound and greatest-lower-bound properties in $\overline{R}$ (Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ ), which need no hypothesis.
The Archimedean property is what closes the converse. Steps 2.3 and 2.4 give $L - ε \leq Λ \leq L + ε$ for every positive real $ε$ , and passing from that to $Λ = L$ needs a positive real strictly below any prescribed positive gap; For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ supplies $1 / m$ .

Depends on

Used by

Dependency tree · two levels

29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Limit superior and limit inferior (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (3.17) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.4 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.3 (standard reference, not scraped)

For finite LL: L=lim sup⁡xkL=limsupxk​ iff for every ε>0ε>0 one has xk<L+εxk​<L+ε eventually and xk>L−εxk​>L−ε frequently