Ergodicity

Start with six equally likely states

Let the space of possible states be

Give every state probability \(1/6\). Thus an event \(S\subseteq\Omega\) has probability

where \(|S|\) is the number of states in \(S\). Every subset is measurable in this finite example.

Put the following real-valued observable on the states:

An observable is a quantity read from the current state. Here it is the function \(f:\Omega\to\mathbb R\).

We will keep the same states, probabilities, and observable while changing only the time-one map.

System A: one orbit visits all six states

Define

This permutation preserves the uniform probability: the preimage of an event has exactly as many points as the event itself. Starting at any state, six steps visit every state exactly once. The six-step sum is

so the six-step average is

Now ask which events are unchanged by one step. An event \(S\) is strictly invariant when

The symbol \(T^{-1}(S)\) means preimage, not an inverse function:

If a strictly invariant event contains one state, moving forward around the cycle shows that it contains all six. Therefore the complete invariant-event list is

with probabilities \(0\) and \(1\). There is no invariant region holding a proper positive fraction of the probability. The system is ergodic.

System B: two sealed three-state orbits

Define instead

This map is also a permutation, so it preserves exactly the same uniform probability. But the event

is now strictly invariant:

Its complement \(R=\{3,4,5\}\) is also invariant and has probability \(1/2\). The complete invariant-event list is

with probabilities \(0,1/2,1/2,1\). The invariant events \(L\) and \(R\), each of probability \(1/2\), violate the null-or-conull criterion. Therefore this system is not ergodic.

The observable also exposes the split. Its average around the left orbit is

while its average around the right orbit is

Starting anywhere in \(L\), every complete three-step block averages to \(5\). Starting anywhere in \(R\), every complete three-step block averages to \(15\). The dynamics retain one bit of durable information: which component did the orbit start in?

What the example teaches

Ergodicity is a statement about invariant information, not about whether an orbit moves.

• Both examples move every state and preserve probability.
• The one-cycle system eventually carries every start through the same six states.
• The split system never carries a point from \(L\) to \(R\) or from \(R\) to \(L\).
• The component label is therefore an invariant distinction with probability \(1/2\) on each side.

This page’s six-state calculation complements Ergodic probability base . That entry separates probability normalization, measure preservation, and ergodic rigidity. Here the focus is the exact information that survives, its function-valued form, its effect on time averages, and its sharp separation from mixing.

The general definition

Let \((\Omega,\mathcal B)\) be a measurable space and let \(\mu\) be a measure on it:

• \(\Omega\) is the state space;
• \(\mathcal B\) is the collection of measurable events;
• \(\mu\) is a measure assigning sizes to those events; and
• \(T:\Omega\to\Omega\) is the time-one map.

The map is measure preserving when it is measurable and

for every measurable event \(S\).

The system is ergodic when it is measure preserving and every measurable strictly invariant event is null or conull:

Here \(S^{\mathsf c}=\Omega\setminus S\) is the complement of \(S\). A null set has measure zero. A conull event has a null complement, so it contains almost all measured states. On a probability space , where \(\mu(\Omega)=1\), the conclusion becomes

The number \(1\) comes from probability normalization, not from ergodicity alone. If the total mass were \(6\), a conull event would have mass \(6\).

Event form and function form

There are two closely related ways to detect invariant information.

Invariant events

An invariant event asks a yes-or-no question whose answer never changes along an orbit:

The indicator \(\mathbf 1_S\) equals \(1\) on \(S\) and \(0\) outside it. In the split example, \(\mathbf 1_L\) records which of the two orbit components contains \(x\).

Invariant functions

A measurable function \(g:\Omega\to\mathbb R\) is invariant when

for every \(x\). Such a function assigns one fixed value along each orbit.

For the one six-cycle, invariance forces the chain

For the split map, the function

is invariant and nonconstant. It stores the same component information as the event \(L\).

In a general ergodic system, a suitably measurable invariant function is constant almost everywhere . “Almost everywhere” means that the equality may fail on a null set. It does not mean pointwise equality at every state.

Strict invariance versus invariance modulo null sets

Three set statements must be kept separate:

1. Strict invariance: \(T^{-1}S=S\) as literal sets.
2. Almost invariance: \(T^{-1}S\) and \(S\) differ only on a null set.
3. Trivial modulo null sets: \(S\) differs from \(\varnothing\) or \(\Omega\) only on a null set.

The symmetric difference

contains the points on which membership in \(A\) and \(B\) disagrees. Almost invariance can therefore be written

Equivalently, Mathlib writes equality of the sets almost everywhere:

In the finite uniform six-state model, every nonempty event has positive probability. The only null event is \(\varnothing\), so equality modulo null sets is exactly ordinary equality. That is why the finite list of invariant events can be computed without qualifications.

General spaces can have nonempty null sets. Suppose \(N\) is null and \(T\) preserves \(\mu\). Then \(T^{-1}N\) is also null, and

is null. Thus \(N\) is almost invariant even if \(T^{-1}N\ne N\) pointwise. This is not a violation of ergodicity: \(N\) already represents the same measured event as \(\varnothing\).

Mathlib exposes this distinction deliberately:

• PreErgodic is defined using strict invariance of a measurable set;
• QuasiErgodic.ae_empty_or_univ₀ accepts a null-measurable, almost invariant set; and
• every Ergodic map yields the needed QuasiErgodic interface through hT.quasiErgodic.

The subscript zero in these Mathlib theorem names is part of the library identifier; it is not the probability value zero.

Ergodic does not mean mixing

Ergodicity rules out invariant distinctions. Strong mixing asks for a different, stronger property: widely separated observations should lose their correlation. On a probability space, one standard form is

for every pair of measurable events \(E,F\).

Return to the ergodic six-cycle and take

Because the orbit returns to \(0\) exactly at multiples of six,

Here \(6\mid n\) means that \(6\) divides \(n\). The proposed mixing target is

The overlap keeps cycling between \(1/6\) and \(0\), so it does not converge to \(1/36\). The map is ergodic but not mixing.

There is no paradox:

• ergodicity asks whether any event is unchanged forever;
• mixing asks whether long-lag overlaps approach a product; and
• a periodic orbit can have no proper invariant event while retaining perfect timing information.

The same system is a counterexample to the claim that ergodicity passes to every power. Since \(T_{\mathrm{one}}^6=\operatorname{id}\), every event is invariant under the sixth power, so \(T_{\mathrm{one}}^6\) is not ergodic.

Why time averages enter the story

For an observable \(f:\Omega\to\mathbb R\), the \(n\)-step Birkhoff average is

The notation \(T^k\) means apply \(T\) \(k\) times, as developed under orbit and iterate . In the one six-cycle, every block of six consecutive observations contains the same six values, so

for every start \(x\) and every positive integer \(m\).

In the split system,

The nonergodic limit is an invariant function: it is constant on each orbit component but not globally constant. Ergodicity is exactly the rigidity that collapses such invariant measurable targets to one almost-everywhere constant.

The project’s RMT-28 theorem applies this to the conditional expectation onto the invariant sigma algebra . Under an ergodic probability measure and integrability of \(f\), it identifies the almost-everywhere Birkhoff limit with the ordinary integral

Ergodicity by itself is not a convergence theorem. The Birkhoff theorem, measurability, integrability, and measure preservation still do real work.

In Lean: the same ideas in exact syntax

1. Say that an event is strictly invariant

T ⁻¹' S = S

#check T ⁻¹' S = S

2. Separate pre-ergodic rigidity from full ergodicity

hpre.ae_empty_or_univ hS hInv

structure PreErgodic (T : Ω → Ω) (μ : Measure Ω) : Prop where
  aeconst_set ⦃S : Set Ω⦄ :
    MeasurableSet S →
    T ⁻¹' S = S →
    EventuallyConst S (ae μ)

structure Ergodic (T : Ω → Ω) (μ : Measure Ω) : Prop extends
  MeasurePreserving T μ μ, PreErgodic T μ

#check PreErgodic T μ
#check Ergodic T μ
#check hT.toPreErgodic
#check hT.toMeasurePreserving
#check hpre.ae_empty_or_univ hS hInv
#check hpre.measure_self_or_compl_eq_zero hS hInv

3. Read the probability zero-one law

hpre.prob_eq_zero_or_one hS hInv

#check hpre.prob_eq_zero_or_one hS hInv

4. Move from strict to almost invariance

hT.quasiErgodic.ae_empty_or_univ₀ hNullMeas hAeInv

#check hT.quasiErgodic
#check hT.quasiErgodic.ae_empty_or_univ₀ hNullMeas hAeInv

5. Collapse an invariant function

hT.ae_eq_const_of_ae_eq_comp_ae hg hGInv

#check hT.ae_eq_const_of_ae_eq_comp_ae hg hGInv

6. Identify the ergodic Birkhoff limit

ae_tendsto_birkhoffAverage_integral_of_ergodic hT hf

theorem ae_tendsto_birkhoffAverage_integral_of_ergodic
    [IsProbabilityMeasure μ]
    (hT : Ergodic T μ) (hf : Integrable f μ) :
    ∀ᵐ ω ∂μ,
      Tendsto (fun n ↦ birkhoffAverage ℝ T f n ω) atTop
        (nhds (∫ x, f x ∂μ))

#check ae_tendsto_birkhoffAverage_integral_of_ergodic hT hf

Exact source excerpts

Resource label: pinned Mathlib. The repository’s pinned Mathlib/Dynamics/Ergodic/Ergodic.lean contains:

structure PreErgodic (f : α → α) (μ : Measure α := by volume_tac) : Prop where
  aeconst_set ⦃s : Set α⦄ :
    MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)

structure Ergodic (f : α → α) (μ : Measure α := by volume_tac) : Prop extends
  MeasurePreserving f μ μ, PreErgodic f μ

theorem PreErgodic.prob_eq_zero_or_one
    [IsProbabilityMeasure μ]
    (hf : PreErgodic f μ) (hs : MeasurableSet s)
    (hs' : f ⁻¹' s = s) :
    μ s = 0 ∨ μ s = 1

The same file’s almost-invariant interface is:

theorem QuasiErgodic.ae_empty_or_univ₀
    (hf : QuasiErgodic f μ)
    (hsm : NullMeasurableSet s μ)
    (hs : f ⁻¹' s =ᵐ[μ] s) :
    s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] Set.univ

Resource label: pinned Mathlib. Mathlib/Dynamics/Ergodic/Function.lean contains:

theorem Ergodic.ae_eq_const_of_ae_eq_comp_ae
    {g : α → X} (h : Ergodic f μ)
    (hgm : AEStronglyMeasurable g μ)
    (hg_eq : g ∘ f =ᵐ[μ] g) :
    ∃ c, g =ᵐ[μ] Function.const α c

Resource label: checked project source. ErgodicBirkhoffLimit.lean uses the two projections separately:

filter_upwards
    [ae_tendsto_birkhoffAverage_condExp hT.toMeasurePreserving hf,
      condExp_invariants_ae_eq_integral_of_preErgodic
        (T := T) (f := f) hT.toPreErgodic hf]
    with ω hconv htarget
simpa only [htarget] using hconv

The first line supplies orbit-average convergence to an invariant conditional expectation. The second collapses that invariant target to the integral. The proof therefore records which half of ergodicity does which job.

Standalone tutorial

Standalone tutorial. This worksheet imports only Std. It enumerates all \(64\) events, computes the invariant-event lists for the two six-state maps, checks the component-label function, prints six-step orbit sums, and prints the singleton-overlap pattern. It does not formalize measure theory or prove the general ergodic theorem.

Save the following as ErgodicityFiniteScratch.lean:

import Std

def states : List Nat :=
  List.range 6

def oneCycle (x : Nat) : Nat :=
  (x + 1) % 6

def splitCycles (x : Nat) : Nat :=
  if x < 3 then
    (x + 1) % 3
  else
    3 + (x - 3 + 1) % 3

def subsets : List (List Nat) :=
  states.foldr
    (fun x acc => acc ++ acc.map (fun event => x :: event))
    [[]]

def preimage (T : Nat → Nat) (event : List Nat) : List Nat :=
  states.filter fun x => event.contains (T x)

def invariant (T : Nat → Nat) (event : List Nat) : Bool :=
  preimage T event == event

def invariantEvents (T : Nat → Nat) : List (List Nat) :=
  subsets.filter fun event => invariant T event

def observable : Nat → Int
  | 0 => 2
  | 1 => 5
  | 2 => 8
  | 3 => 11
  | 4 => 14
  | 5 => 20
  | _ => 0

def componentMean (x : Nat) : Int :=
  if x < 3 then 5 else 15

def invariantFunction (T : Nat → Nat) (g : Nat → Int) : Bool :=
  states.all fun x => decide (g (T x) = g x)

def iterate (T : Nat → Nat) : Nat → Nat → Nat
  | 0, x => x
  | n + 1, x => T (iterate T n x)

def orbitValues
    (T : Nat → Nat) (start steps : Nat) : List Int :=
  (List.range steps).map fun n => observable (iterate T n start)

def orbitSum
    (T : Nat → Nat) (start steps : Nat) : Int :=
  (orbitValues T start steps).foldl (fun total x => total + x) 0

def overlapCount
    (T : Nat → Nat) (event : List Nat) (n : Nat) : Nat :=
  ((preimage (fun x => iterate T n x) event).filter
    (fun x => event.contains x)).length

#eval invariantEvents oneCycle
#eval invariantEvents splitCycles
#eval invariantFunction oneCycle componentMean
#eval invariantFunction splitCycles componentMean
#eval states.map fun x =>
  (x, orbitValues oneCycle x 6, orbitSum oneCycle x 6)
#eval states.map fun x =>
  (x, orbitValues splitCycles x 6, orbitSum splitCycles x 6)
#eval (List.range 13).map fun n =>
  (n, overlapCount oneCycle [0] n)

Run it on an ordinary Mac or Linux machine with the pinned small toolchain:

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

This exact worksheet was executed successfully with the pinned Lean 4.32.0 compiler and printed:

[[], [0, 1, 2, 3, 4, 5]]
[[], [3, 4, 5], [0, 1, 2], [0, 1, 2, 3, 4, 5]]
false
true
[(0, [2, 5, 8, 11, 14, 20], 60),
 (1, [5, 8, 11, 14, 20, 2], 60),
 (2, [8, 11, 14, 20, 2, 5], 60),
 (3, [11, 14, 20, 2, 5, 8], 60),
 (4, [14, 20, 2, 5, 8, 11], 60),
 (5, [20, 2, 5, 8, 11, 14], 60)]
[(0, [2, 5, 8, 2, 5, 8], 30),
 (1, [5, 8, 2, 5, 8, 2], 30),
 (2, [8, 2, 5, 8, 2, 5], 30),
 (3, [11, 14, 20, 11, 14, 20], 90),
 (4, [14, 20, 11, 14, 20, 11], 90),
 (5, [20, 11, 14, 20, 11, 14], 90)]
[(0, 1), (1, 0), (2, 0), (3, 0), (4, 0), (5, 0), (6, 1), (7, 0), (8, 0), (9, 0), (10, 0), (11, 0), (12, 1)]

The first function check printed false; the second printed true. Every one-cycle six-step sum is \(60\). Split starts \(0,1,2\) have sum \(30\), and starts \(3,4,5\) have sum \(90\). The overlap count for \(\{0\}\) is \(1\) at \(n=0,6,12\) and \(0\) at the other displayed times.

Dividing those counts by six gives the overlap probabilities in the figure. The worksheet is an executable audit of the finite arithmetic, not a proof that an abstract measure-preserving system is ergodic. It imports only Std and does not load the project or Mathlib.

Try it in the repository

import NonlinearDynamics.Random.RandomCocycles.ErgodicBirkhoffLimit

open MeasureTheory Set Filter Function ProbabilityTheory
open NonlinearDynamics.Random.RandomCocycles
open scoped ENNReal Topology BigOperators

universe uΩ

variable {Ω : Type uΩ} [MeasurableSpace Ω]
variable {T : Ω → Ω} {μ : Measure Ω}
variable {S : Set Ω} {f g : Ω → ℝ}
variable [IsProbabilityMeasure μ]

variable (hpre : PreErgodic T μ)
variable (hT : Ergodic T μ)
variable (hS : MeasurableSet S)
variable (hInv : T ⁻¹' S = S)
variable (hNullMeas : NullMeasurableSet S μ)
variable (hAeInv : T ⁻¹' S =ᵐ[μ] S)
variable (hg : AEStronglyMeasurable g μ)
variable (hGInv : g ∘ T =ᵐ[μ] g)
variable (hf : Integrable f μ)

#check PreErgodic
#check Ergodic
#check QuasiErgodic
#check hT.toPreErgodic
#check hT.toMeasurePreserving
#check hT.quasiErgodic
#check hpre.ae_empty_or_univ hS hInv
#check hpre.measure_self_or_compl_eq_zero hS hInv
#check hpre.prob_eq_zero_or_one hS hInv
#check hT.quasiErgodic.ae_empty_or_univ₀ hNullMeas hAeInv
#check hT.ae_eq_const_of_ae_eq_comp_ae hg hGInv
#check condExp_invariants_comp
#check condExp_invariants_ae_eq_integral_of_preErgodic
#check ae_tendsto_birkhoffAverage_integral_of_ergodic hT hf

cd formalization
lake env lean NonlinearDynamics/Random/RandomCocycles/ErgodicBirkhoffLimit.lean

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

Boundary cases and common traps

Identity dynamics

If \(T=\operatorname{id}\), every event is strictly invariant. On two atoms with positive mass, either singleton is a positive-mass invariant event with a positive-mass complement. The system is not pre-ergodic and therefore not ergodic. A function that assigns different values to the atoms is invariant and nonconstant.

A Dirac measure

A Dirac measure places all mass at one point. Every event is then null or conull, so PreErgodic T μ can hold even when \(T\) does not preserve \(\mu\). The project contains a checked instance of this boundary model. That model is a counterexample to any implication from pre-ergodicity alone to measure preservation.

The zero measure

Under Mathlib’s definition, a measurable map is ergodic with respect to the zero measure. Every event is both null and conull, and every almost-everywhere statement is vacuous. Consequently,

The project’s finite-mass normalization theorem keeps a separate \(\mu\ne0\) premise before it divides by total mass.

Noninvertible maps

The notation \(T^{-1}S\) is defined for every function. Ergodicity does not require \(T\) to have an inverse. The project includes an ergodic Dirac example whose map is neither injective nor surjective.

Exact invariant sigma algebra

Ergodicity says that invariant measurable information is trivial modulo null sets. It does not generally prove that Mathlib’s exact invariant sigma algebra is literally the smallest measurable space as a structure.

What ergodicity does not establish

Ergodicity alone does not prove:

• mixing, weak mixing, decay of correlations, or statistical independence;
• ergodicity of every powered map \(T^n\);
• injectivity, surjectivity, or invertibility of \(T\);
• that null sets are empty or impossible;
• pointwise constancy rather than almost-everywhere constancy;
• literal equality of the exact invariant sigma algebra with the bottom sigma algebra;
• measurability or integrability of an arbitrary observable;
• a Birkhoff convergence theorem without its additional hypotheses;
• a convergence rate for Birkhoff averages;
• thermalization, chaos in every sense, positive entropy, or sensitive dependence;
• a Lyapunov exponent, an Oseledets splitting, or a Kingman limit.

The exact promise is narrower: after measurable null distinctions are discarded, the dynamics retain no nontrivial invariant event and no nonconstant suitably measurable invariant observable.

Related concepts

• Event introduces measurable yes-or-no questions.
• Measurable space specifies which sets may be assigned measure.
• Measurable function is the analytic interface required of invariant observables.
• Null set explains why measure zero is not the same as logical impossibility.
• Almost everywhere formalizes equality after null exceptions are ignored.
• Measure-preserving transformation supplies the dynamical half of full ergodicity.
• Ergodic probability base separates mass-one normalization, preservation, and rigidity.
• Invariant sigma algebra gathers exact invariant measurable events.
• Conditional expectation is the general Birkhoff target before ergodic rigidity collapses it.
• Birkhoff Limits, Invariant Sigma Algebras, and Conditional Expectation develops the nonergodic predecessor.
• Ergodic Birkhoff Limits and Normalized Space Averages proves the probability and finite-mass endpoints used by the project.

References

Mathlib contributors. Ergodic structures and invariant-function theorems, Mathlib 4.32.0 at pinned commit 81a5d257. These are authoritative for the exact PreErgodic, QuasiErgodic, and Ergodic interfaces used here.

Mark Pollicott and Michiko Yuri. Ergodic measures, chapter 9 of Dynamical Systems and Ergodic Theory, Cambridge University Press, 1998. Textbook source for invariant sets, invariant functions, and the distinction between ergodicity and mixing.

Nonlinear Dynamics in Lean contributors. ErgodicBirkhoffLimit.lean, the checked project source for the minimized rigidity and convergence interfaces and their boundary probes.