Limit superior

Start with one real sequence. It has a large value once, then alternates forever:

Its first values are

The value \(5\) is the maximum of the whole sequence, but it occurs only at time zero. If we discard that first term, every remaining tail contains only \(-1\) and \(1\), and it contains \(1\) infinitely many times. The eventual upper edge is therefore \(1\), not \(5\):

The sequence does not converge. Its positive even terms are always \(1\), while its odd terms are always \(-1\). This one example already separates three different questions:

• the maximum asks for the largest value attained anywhere, which is \(5\);
• the limit superior asks for the highest level that survives arbitrarily far into the sequence, which is \(1\); and
• an ordinary limit would require all sufficiently late terms to gather around one value, which does not happen.

Compute the tail ceilings by hand

For each starting index \(N\in\mathbb N\), define the tail

and its tail ceiling

Here \(\sup\) means the least upper bound. It is the smallest number that is at least as large as every value in that tail.

For the worked sequence:

Deleting more terms can never raise a supremum, so

In this example the ceiling sequence is

and its infimum is \(1\). That is the limit superior calculation:

The general definition

For a sequence \((u_n)\) valued in the extended real line \(\mathbb R\cup\{-\infty,+\infty\}\), define

The extended real line supplies genuine top and bottom values. For example, the sequence \(u_n=-n\) has extended-real limsup \(-\infty\), while \(u_n=n\) has extended-real limsup \(+\infty\).

For bounded real sequences, three views say the same thing:

1. Tail-ceiling view: take the supremum of every tail, then take the infimum of those ceilings.
2. Eventual-upper-bound view: a real number \(b\) is an eventual upper bound when some cutoff \(N\) satisfies \(u_n\le b\) for every \(n\ge N\). The limsup is the smallest such eventual ceiling.
3. Repeated-return view: every level strictly below the limsup is exceeded arbitrarily late, while every level strictly above it eventually stays above all terms.

Here eventually means “after some finite cutoff, always.” The phrase arbitrarily late means “after every proposed cutoff, there is a later witness.” Neither word assigns a probability to the set of times.

Why neither a maximum nor one upper bound is a limit

A maximum is sensitive to the finite prefix. Changing only \(a_0\) from \(5\) to \(5000\) would change the maximum but leave every tail beginning at \(N\ge1\) unchanged. The limsup would remain \(1\).

A limsup need not be attained. For example, \(u_n=1-1/(n+1)\) never equals \(1\), but its tail ceilings decrease toward \(1\), so its limsup is \(1\). The worked alternating sequence does attain its limsup repeatedly, but that is a feature of the example, not part of the definition.

An upper-limsup estimate

says that for every real \(y\gt L\), the terms eventually satisfy \(u_n\lt y\). It does not say that \(u_n\to L\). The missing lower half is usually written

where the limit inferior records the eventual lower edge. In the worked sequence,

so the gap between the two edges exposes the failure of convergence.

Real-valued Lean needs explicit boundedness hypotheses

Mathlib’s Filter.limsup works in a conditionally complete order such as \(\mathbb R\). The real numbers do not contain actual elements \(-\infty\) and \(+\infty\), but a Lean definition must still return a real number for every real sequence.

At the pinned Mathlib revision, Filter.limsup_eq unfolds the real-valued operator as

For \(u_n=-n\), every real \(b\) is eventually an upper bound. The set inside the infimum is all of \(\mathbb R\), and Mathlib’s total real infimum satisfies \(\inf\mathbb R=0\). Thus real Filter.limsup returns \(0\) for this unbounded-below sequence, even though its extended-real limsup is \(-\infty\). The returned zero is a totalization default, not the sequence’s eventual upper level.

In Lean: name the eventual upper edge

Filter.limsup u Filter.atTop

The same expression with a convergent bounded sequence agrees with its ordinary limit. For the alternating worked example it records the upper edge \(1\), not a nonexistent ordinary limit.

In Lean: turn an upper-edge claim into eventual inequalities

Filter.limsup_le_iff hLower hUpper

A Mathlib-backed proof can use the exact pattern

example {u : ℕ → ℝ} {L : ℝ}
    (hLower : Filter.IsCoboundedUnder (· ≤ ·) Filter.atTop u)
    (hUpper : Filter.IsBoundedUnder (· ≤ ·) Filter.atTop u)
    (hEventually : ∀ y > L, ∀ᶠ n in Filter.atTop, u n < y) :
    Filter.limsup u Filter.atTop ≤ L := by
  exact (Filter.limsup_le_iff hLower hUpper).2 hEventually

The comparison symbols are literal Lean syntax inside this code block. The mathematical display above uses TeX commands so Hugo passes it safely to KaTeX.

Standalone tutorial

Standalone tutorial. The following complete file computes the worked sequence and several finite windows. It imports Std, not Mathlib or this project.

Save it as LimsupScratch.lean:

import Std

namespace LimsupScratch

def a : Nat → Int
  | 0 => 5
  | n + 1 => if n % 2 = 0 then -1 else 1

def firstTen : List Int :=
  (List.range 10).map a

def maxFromTo (start stop : Nat) : Int :=
  ((List.range (stop - start + 1)).map fun k => a (start + k)).foldl max (-100)

#eval firstTen
#eval [maxFromTo 0 9, maxFromTo 1 9, maxFromTo 4 9]

example : firstTen = [5, -1, 1, -1, 1, -1, 1, -1, 1, -1] := by
  decide

example : maxFromTo 0 9 = 5 := by decide
example : maxFromTo 1 9 = 1 := by decide
example : maxFromTo 4 9 = 1 := by decide
example : a 8 = 1 ∧ a 9 = -1 := by decide

end LimsupScratch

Run it on macOS or Linux with the pinned compiler:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean LimsupScratch.lean

The first output should be [5, -1, 1, -1, 1, -1, 1, -1, 1, -1]. The second should be [5, 1, 1]. These finite calculations display the stable tail ceiling, while the paper argument proves the infinite statement: after index zero every term is at most \(1\), and every tail contains a positive even index where the value is exactly \(1\).

This worksheet deliberately does not import Filter.limsup. That interface lives in Mathlib and belongs to the separate project check below. This exact worksheet was executed successfully with the pinned Lean 4.32.0 compiler on macOS; the same standalone command works on Linux.

In Lean: the project’s upper-limsup theorem

The project applies limsup to normalized subadditive processes. A subadditive process is a time-indexed family whose cost over two consecutive blocks is no larger than the sum of the two block costs, with the second block evaluated after moving the base point.

hX.ae_limsup_normalized_le_blockIntegral_of_ae_isBoundedUnder_ge hT hXlower b hb

The proof combines finite phase averaging with ordinary Birkhoff-sum limits under the original base map. It does not infer that every powered map is ergodic.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomCocycles.SubadditiveUpperLimsup

open Filter MeasureTheory

#check Filter.limsup
#check Filter.limsup_eq
#check Filter.limsup_nat_add
#check Filter.limsup_le_iff
#check Filter.le_limsup_iff
#check Filter.Tendsto.limsup_eq
#check NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.ae_limsup_normalized_le_blockIntegral_of_ae_isBoundedUnder_ge
#check NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.ae_limsup_normalized_le_blockIntegral
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_limsup_normalized_le_integratedLogPlusGrowthRate

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/SubadditiveUpperLimsup.lean

Boundary cases and near-misses

• Delete a finite prefix: the limsup is unchanged. This is why the isolated \(5\) disappears from the worked sequence.
• Constant sequence: if \(u_n=c\), every tail ceiling is \(c\), so the limsup and ordinary limit are both \(c\).
• Convergent but never attaining the limit: for \(u_n=1-1/(n+1)\), the limsup is \(1\) even though no term equals \(1\).
• Unbounded above: \(u_n=n\) has extended-real limsup \(+\infty\). A real-valued API cannot represent that conclusion as an ordinary real.
• Unbounded below: \(u_n=-n\) exposes the totalized-real warning above.
• Upper bound without convergence: the worked alternating tail satisfies \(\limsup a_n\le1\), but its lower edge is \(-1\).
• Almost-everywhere theorem: the project’s result may exclude a null set of sample points. It is not a pointwise statement about every sample.

What a limsup statement does not establish

An upper limsup or upper-limsup bound alone proves none of the following:

• existence of an ordinary limit;
• equality with the limit inferior;
• attainment of the limsup at a finite index;
• monotonicity of the original sequence;
• measurability, integrability, or an almost-everywhere claim;
• interchange of a limit and an integral;
• a signed logarithmic growth rate, Lyapunov exponent, invariant splitting, or Oseledets theorem.

Each conclusion needs its own hypotheses and proof. In the project’s subadditive program, the upper limsup is deliberately one half of a later squeeze argument.

Check your understanding

1. Change only \(a_0\) from \(5\) to \(5000\). Which of the maximum, limsup, and liminf change?
2. Why is the ceiling of every tail beginning at \(N\ge1\) exactly \(1\), not merely at most \(1\)?
3. What are the limsup and liminf of the sequence \(0,2,0,2,0,2,\ldots\)? Does it converge?
4. Give a convergent sequence whose limsup is not attained by any term.
5. In the eventual-bound characterization, why do we test every \(y\gt L\) instead of requiring every late term to satisfy \(u_n\le L\)?
6. Why does the real-valued sequence \(-n\) require care when interpreting Mathlib’s total Filter.limsup?
7. Which additional lower-edge inequality turns an upper-limsup estimate into a convergence squeeze?

Where to continue

The companion limit inferior chapter develops the lower edge and its own real-valued boundedness gate. Subadditive Upper Limsup Bounds Before Kingman Convergence builds the full phase-averaging proof around the exact project theorem. The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence then supplies the complementary lower mechanism used in the later convergence argument.

Sources

Resource label: pinned Mathlib. The repository pins Mathlib commit 81a5d257. Its official liminf and limsup source defines Filter.limsup, unfolds it with Filter.limsup_eq, proves finite-prefix invariance with Filter.limsup_nat_add, and states the bounded Filter.limsup_le_iff characterization used above. The official real-order source contains Real.sInf_univ, which explains the totalized value in the unbounded-below example.

Resource label: checked project source. The repository’s SubadditiveUpperLimsup module is authoritative for the almost-everywhere fixed-block theorem, its nonnegative compatibility wrapper, and the log-positive cocycle specialization described on this page.