Limit inferior

Start with one sequence you can calculate

Consider the real sequence with two interlaced rails:

Here \(\mathbb N=\{0,1,2,\ldots\}\). The first eight terms are exact rational numbers:

A tail beginning at cutoff \(N\) is the infinite list \(a_N,a_{N+1},a_{N+2},\ldots\). Its infimum is the greatest real number that is no larger than every value in that tail. For this sequence the first tail floors are

This pattern has an exact proof. From cutoff \(2K\) or \(2K+1\), the term

is still present. Every later odd term is at least this large, because its positive fraction is smaller, while every even term is larger than \(3\). Therefore the tail floor is not merely approximated by that odd term; it is attained there:

The floors rise through

and approach \(-1\). That eventual lower edge is the limit inferior, or liminf:

Why this sequence still does not converge

The even-indexed subsequence tends to \(3\):

The odd-indexed subsequence tends to \(-1\):

A convergent sequence cannot have two subsequences with different limits. Thus \((a_n)\) does not converge. Its liminf is \(-1\), while its companion limit superior , or limsup, is \(3\). The gap between the two edges records the persistent oscillation.

This is the first misconception to retire:

The definition after seeing it happen

For a sequence valued in the extended real line \(\mathbb R\cup\{-\infty,+\infty\}\), define one floor for each tail:

Advancing from \(N\) to \(N+1\) removes one candidate from the infimum. It cannot lower the floor, so \(m_N\le m_{N+1}\). The liminf is the supremum, meaning the least upper bound, of all those rising floors:

The extended real endpoints make this formula valid for every sequence. A sequence escaping downward may have liminf \(-\infty\); a sequence escaping upward may have liminf \(+\infty\). No arbitrary finite number is needed.

Three readings of the same definition are useful:

1. Tail-floor reading: take the infimum of every suffix and watch those infima rise.
2. Eventual-lower-bound reading: collect levels \(b\) for which \(b\le a_n\) from some time onward; the liminf is the highest such eventual floor when the real order-boundedness hypotheses hold.
3. Repeated-return reading: if \(y\) lies strictly above the liminf, the sequence must return below \(y\) arbitrarily late, again under the side conditions required by a conditionally complete real codomain.

Deleting finitely many initial terms changes none of these eventual statements. That is why the prefix is irrelevant and why Mathlib provides the tail-invariance theorem Filter.liminf_nat_add.

Eventually and frequently are logical, not probabilistic

For natural-number time, a property \(P(n)\) holds eventually when some cutoff works forever afterward:

It holds frequently when every cutoff has a later witness:

Lean writes the second statement as ∃ᶠ n in Filter.atTop, P n. Filter.atTop is the filter that formalizes moving toward arbitrarily large natural numbers. These words make no claim about probability, positive density, or how often the witnesses occur relative to all times.

For the worked sequence, every \(y\gt-1\) has values below it frequently, because sufficiently late odd terms remain below \(y\). Every \(b\lt-1\) is eventually a lower bound because both rails eventually lie above \(b\).

Mathlib’s real liminf is deliberately total

The real numbers are conditionally complete: every nonempty set that is bounded above has a real supremum. They do not contain actual elements \(+\infty\) and \(-\infty\). Mathlib nevertheless defines Filter.liminf so that it returns a real number for every real sequence.

At the pinned Mathlib revision, Filter.liminf_eq unfolds the operator as

Now take the near-miss \(u_n=-n\). Given any proposed real floor \(b\), choose a natural number \(n\gt-b\). Then \(-n\lt b\), and later values only decrease. No real number is an eventual lower bound. The set inside the supremum is empty.

Mathlib’s real order uses

Consequently,

The real value \(0\) is a totalization default. It is not a hidden lower edge of the sequence.

Two similarly named order hypotheses play different roles in the pinned API:

Because the relation is written (· ≥ ·), the names can be misread. Follow the displayed inequality rather than guessing from the identifier.

The repository’s quadratic boundary model

Random-matrix-theory milestone 33 (RMT-33) checks a stronger near-miss inside the exact subadditive-process interface. On a one-point probability space, take the identity base map and

It is shifted subadditive because

The one-step value is \(X_1=-1\). Subtracting its one-step orbit sum gives

Lean’s total normalization sets the time-zero value to \(0\). At every positive time,

This sequence crosses the rational target \(-2\) at every \(n\ge4\), so it belongs to the project’s strict rational lower-deviation event at target \(-1\). Yet it is unbounded below. Its extended-real liminf is \(-\infty\), while its Mathlib real liminf is the totalized value \(0\).

Therefore the unguarded implication

is false. The checked project theorem makes the eventual lower-bound argument an explicit input instead of hiding it.

A second near-miss: strict margins matter

For positive \(n\), let \(v_n=-1/n\), and set the totalized time-zero value to \(0\). Then \(v_n\to0\) and \(v_n\lt0\) frequently. But for every fixed rational \(q\lt0\), the inequality \(v_n\lt q\) eventually stops holding.

Approaching a target from below is not the same as crossing one strictly lower target arbitrarily late. RMT-33 therefore uses two rational gaps. Starting from \(\liminf u_n\lt\delta\), it chooses an outer rational target \(c\lt\delta\) that remains above the liminf. Membership in the event at \(c\) then exposes an inner rational witness \(q\lt c\) crossed frequently. The impossible substitution \(\delta\lt\delta\) would lose this room.

In Lean

Filter.liminf a Filter.atTop = (-1 : ℝ)

Filter.IsBoundedUnder (· ≥ ·) Filter.atTop u

liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet hlower hω

A tiny standalone worksheet

Standalone tutorial. Save the following as LimitInferiorTutorial.lean. It calculates the first eight exact rational values and their finite-window minima. It does not import Mathlib, define Filter.liminf, or prove the infinite limiting statement.

import Std

def upperRail (k : Nat) : Rat :=
  3 + 1 / ((k : Rat) + 1)

def lowerRail (k : Nat) : Rat :=
  -1 - 1 / ((k : Rat) + 1)

def sample (n : Nat) : Rat :=
  let k := n / 2
  if n % 2 = 0 then upperRail k else lowerRail k

def minRat (x y : Rat) : Rat :=
  if x ≤ y then x else y

def minimum? : List Rat → Option Rat
  | [] => none
  | x :: xs => some (xs.foldl minRat x)

def finiteTailMin (start stop : Nat) : Option Rat :=
  minimum? ((List.range (stop - start)).map
    (fun offset => sample (start + offset)))

#eval (List.range 8).map sample
#eval (List.range 8).map (fun start => finiteTailMin start 8)

example : sample 0 = 4 := by native_decide
example : sample 1 = -2 := by native_decide
example : sample 6 = (13 : Rat) / 4 := by native_decide
example : finiteTailMin 2 8 = some ((-3 : Rat) / 2) := by native_decide

From the directory containing the file, type:

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

The first evaluation should reproduce \(4,-2,7/2,-3/2,10/3,-4/3,13/4,-5/4\). The second should report the finite-window minima \(-2,-2,-3/2,-3/2,-4/3,-4/3,-5/4,-5/4\). These finite minima agree with the first four infinite tail floors because each listed lower-rail value is the smallest value that appears after its cutoff in the full sequence. The paper argument above, not this finite computation, proves the claim about all tails. This exact worksheet was executed successfully with the pinned Lean 4.32.0 compiler; it imports only Std and does not load the project or Mathlib.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomCocycles.SubadditiveKingman

open Filter
open NonlinearDynamics.Random.RandomCocycles

#check Filter.liminf
#check Filter.liminf_eq
#check Filter.liminf_nat_add
#check Filter.liminf_le_of_frequently_le
#check Filter.frequently_lt_of_liminf_lt
#check Filter.le_liminf_iff
#check Filter.Tendsto.liminf_eq
#check liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet
#check IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_of_liminf_normalizedCenteredProcess_lt
#check IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_iff_liminf_normalizedCenteredProcess_lt
#check IsIntegrableSubadditiveProcessCandidate.ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess

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

Liminf supplies only the lower half of convergence

In the bounded regime required by Filter.le_liminf_iff, the inequality

says that every real level strictly below \(L\) is eventually below every term. It does not control the upper excursions. If one also proves

with the required upper and lower bounds, the two edges squeeze the sequence to \(L\). Mathlib packages that last step as tendsto_of_le_liminf_of_limsup_le.

RMT-33 also adds a convergent Birkhoff average back to a centered process. The pinned theorem le_liminf_add provides

under explicit boundedness hypotheses. This is an inequality with side conditions, not unconditional distributivity of liminf over addition.

What this page does not claim

A lower-liminf identity or inequality alone proves none of the following:

• convergence of the original sequence;
• equality with the limsup;
• attainment of the lower edge at a finite time;
• integrability or an almost-everywhere statement;
• convergence in \(L^1\), probability, or distribution;
• interchange of a limit and an integral;
• a signed logarithmic growth rate, Lyapunov exponent, or Oseledets splitting.

Each conclusion needs its own upper bound, measurability, integrability, measure-theoretic, or multiplicative hypotheses.

Where to continue

The limit superior entry develops the upper edge. Birkhoff sums explains the orbit averages that enter the repository’s centered-process identity, while orbit-majorant centering separates that construction from expectation centering.

Continue with the textbook The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence or its declaration-by-declaration Development Notebook companion.

Official sources

• The pinned Mathlib order source for liminf, tail invariance, frequent crossings, and order characterizations defines the exact filter API used by the formalization.
• The pinned topological liminf and limsup source contains convergence identification and the final squeeze theorem.
• The pinned ordered-addition source states le_liminf_add with its exact hypotheses.
• The pinned real conditional-completeness source defines Real.sSup_empty = 0; the pinned extended-real source defines EReal by adjoining both endpoints to the reals.