How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Limit superior and limit inferior of a real sequence as and in
Definition
Let be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences). For let
be the -th tail range of , a nonempty subset of since . Regard as a subset of (The extended real line , its order, and the arithmetic that is left undefined) and put
the supremum and infimum taken in , which exist for every and for every sequence by Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in . The limit superior and limit inferior of are then
again taken in and again existing by Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in , since and are subsets of on which no hypothesis is needed. Both are elements of , and either may be or . The notations , and all denote the first of them elsewhere; this library writes .
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 has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in to a subset of 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): needs bounded above, and needs nonempty, bounded below, and made of real numbers (Greatest lower bound (infimum)). None of those is automatic, and the discipline recorded in Conventions: , 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 is bounded, say for every , then each is a nonempty subset of bounded above by and below by , so by the agreement clause of Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in each and each is the real supremum or infimum of , and lies in . The family is then a nonempty set of reals bounded below by , so is likewise the real infimum of and lies in ; dually for . 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 occur.
Definition references
Sequences of reals: bounded, eventually, frequently, tails, subsequences
The extended real line , its order, and the arithmetic that is left undefined
Complete ordered field (least-upper-bound property)
Every nonempty set bounded below has an infimum
Lower bound, bounded below, bounded set
Remarks
-
The order of the two operations is not symmetric and must be kept straight. is an infimum of suprema and a supremum of infima. Taking them in the other order gives and , which are the extreme values of the whole sequence and carry no information about its behaviour at large indices. The point of the definition is that the inner operation looks at a tail and the outer one lets the tail recede.
-
Why tails at all. Each is a bound on the whole tail from index on, so it forgets the first terms; letting grow forgets any fixed finite number of them. That is what makes and tail quantities in the sense of Convergence depends only on the tail, and it is the reason they can characterise convergence, which is itself a tail property.
-
Neither quantity is a limit, and neither is claimed to be one. The symbols and are single pieces of notation for the two displayed expressions, exactly as "" is a single abbreviation in Divergence to and to . That the family does decrease to in a precise sense is a theorem, not part of this definition; the monotonicity half is The tail suprema of any real sequence are nonincreasing in , so the limit superior exists for every sequence.
-
The tail ranges are sets, not sequences. is the range of the -th tail, so repetitions and order are forgotten (Sequences of reals: bounded, eventually, frequently, tails, subsequences). That is harmless here, since a supremum depends only on the set of values, and it is what lets the whole definition be phrased with the order-theoretic operations of Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in and nothing else.
Depends on
The extended real line , its order, and the arithmetic that is left undefined
Sequences of reals: bounded, eventually, frequently, tails, subsequences
Complete ordered field (least-upper-bound property)
Every nonempty set bounded below has an infimum
Lower bound, bounded below, bounded set
Greatest lower bound (infimum)
Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in