Ergodic probability base

Consider four states with equal probability:

Every subset of this finite space is an event . The total mass is

so \(\mu\) is a probability measure . We will put two different time evolutions on exactly this same probability space.

Two systems, one decisive difference

The first evolution is one four-state cycle:

The second evolution has two disconnected two-state cycles:

Both maps are permutations. For any event \(S\subseteq\Omega\), a permutation does not change the number of points in its preimage:

Every map from this finite discrete measurable space is measurable. Thus both the counting calculation and the required measurability gate hold.

Thus both maps are measure-preserving transformations . Probability normalization and measure preservation do not distinguish the two systems.

The four-cycle is ergodic

An event \(S\) is strictly invariant when

The notation means preimage: a point \(x\) belongs to \(T_{\mathrm{cycle}}^{-1}(S)\) exactly when \(T_{\mathrm{cycle}}(x)\in S\). It does not require an inverse function.

Test the tempting half-space \(A=\{0,2\}\):

So \(A\) is not invariant. In fact, suppose an invariant event \(S\) contains one point \(x\). Invariance gives

Following the four-cycle from \(x\) visits every state, so \(S=\Omega\). If \(S\) contains no point, then \(S=\varnothing\). The only invariant events are therefore

with probabilities \(0\) and \(1\). This system is ergodic.

The split system is not ergodic

Now take

The split map never moves a point between \(B\) and its complement:

But

This measurable invariant event is neither null nor full. The split map is probability preserving, but it is not ergodic.

Unpack the three layers

An ergodic probability base combines three statements about a state space \(\Omega\), a measure \(\mu\), and a time-one map \(T:\Omega\to\Omega\).

1. Probability normalization

The measure has total mass one:

This fixes the unit of measure. It lets an integrable raw integral be called an expectation . It does not make \(T\) measurable, measure preserving, or ergodic.

If we keep the same four-cycle but assign mass \(1/2\) to every point, then the total mass is \(2\). The invariant sets are still only empty and full, but their measures are \(0\) and \(2\), not \(0\) and \(1\). The numerical zero-or-one conclusion uses probability normalization. This rescaled cycle is measure preserving and ergodic, but it is not a probability base.

2. Measure preservation

The map is measurable and transporting the measure through one time step returns the same measure:

Equivalently, for every measurable event \(S\),

This says the statistical weight of events is unchanged by the dynamics. It does not say that invariant events are null or conull. The split example preserves the uniform measure and still has the half-mass invariant event \(B\).

3. Ergodic rigidity

Among measurable events satisfying \(T^{-1}S=S\), only null or conull events are allowed:

Here \(S^{\mathsf c}\) is the complement of \(S\). On a probability space, the second alternative is equivalent to \(\mu(S)=1\). A null set may contain points, so this is an almost-everywhere statement in a general space. In the finite uniform example, every point has positive mass, and the only null event is empty.

Invariant functions carry the same idea

A real-valued observable is a function \(g:\Omega\to\mathbb R\). It is invariant when advancing the base does not change its value:

On the four-cycle, this equation forces

On the split system, define

Then \(h\circ T_{\mathrm{split}}=h\), but \(h\) is not constant. This is the function version of the invariant half-event: \(B=h^{-1}(\{0\})\).

In a general measure space, the checked theorem uses two weaker phrases:

• \(g\) is almost-everywhere strongly measurable, a standard measurable representative condition; and
• \(g\circ T=g\) holds almost everywhere, so failure on a null set is allowed.

Ergodicity then gives a constant \(c\) such that \(g=c\) almost everywhere. The almost-everywhere entry explains the quantifier, and the measurable function entry explains why measurability is a separate gate.

Ergodic does not mean mixing or independent

Mixing would require long-lag overlaps to approach the product of their probabilities. The four-cycle fails this stronger condition. Let \(D=\{0\}\). Then

This periodic sequence does not converge to

So the running example is ergodic and not mixing. It also does not make the events \(D\) and \(T_{\mathrm{cycle}}^{-1}D\) independent: their intersection has probability \(0\), while the product of their probabilities is \(1/16\). The independence page develops that separate probabilistic relation.

Ergodicity also need not pass to a power of the map. The square \(T_{\mathrm{cycle}}^2\) splits the states into the two cycles \(\{0,2\}\) and \(\{1,3\}\). Thus \(\{0,2\}\) is invariant under the square and has probability \(1/2\), even though the original four-cycle is ergodic.

How the project keeps the assumptions separate

The project does not define a new structure called ErgodicProbabilityBase. The phrase is a coordination label for separate hypotheses:

[IsProbabilityMeasure μ]
hErg : Ergodic C.base μ

The cocycle \(C\) already stores a measure-preserving base. Mathlib’s Ergodic structure also contains measure preservation, plus the invariant-event rigidity field. The probability typeclass adds total mass one.

The same module has a third, independent analytic hypothesis, C.HasIntegrableGeneratorLogPlus. It propagates integrability from a one-step log-positive matrix observable to every finite horizon. It is not part of probability or ergodicity.

This separation supports three precise conclusions:

None of these rows alone states that a time average or normalized matrix product converges.

In Lean

The probability layer is a typeclass whose single field is total mass one.

[IsProbabilityMeasure μ]

The exact pinned Mathlib class is:

class IsProbabilityMeasure (μ : Measure α) : Prop where
  measure_univ : μ univ = 1

Ergodicity combines preservation with invariant-event rigidity.

hErg : Ergodic T μ

These are the exact pinned Mathlib structures:

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 μ

The project exposes the probability zero-or-one statement directly.

C.ergodicBase_invariantEvent_prob_eq_zero_or_one hErg hs hinv

The exact checked project theorem is:

theorem ergodicBase_invariantEvent_prob_eq_zero_or_one
    [IsProbabilityMeasure μ]
    (C : DiscreteMatrixCocycle (ι := ι) μ)
    (hErg : Ergodic C.base μ) {s : Set Ω}
    (hs : MeasurableSet s) (hinv : C.base ⁻¹' s = s) :
    μ s = 0 ∨ μ s = 1 :=
  hErg.toPreErgodic.prob_eq_zero_or_one hs hinv

The invariant-function statement replaces strict pointwise equality with an almost-everywhere equality.

C.ergodicBase_ae_eq_const_of_ae_invariant hErg hg hinv

The exact project theorem is:

theorem ergodicBase_ae_eq_const_of_ae_invariant
    (C : DiscreteMatrixCocycle (ι := ι) μ)
    (hErg : Ergodic C.base μ) {g : Ω → ℝ}
    (hg : AEStronglyMeasurable g μ)
    (hinv : g ∘ C.base =ᵐ[μ] g) :
    ∃ c : ℝ, g =ᵐ[μ] Function.const Ω c :=
  hErg.ae_eq_const_of_ae_eq_comp_ae hg hinv

Standalone tutorial

Standalone tutorial. This worksheet imports only Lean’s Std library. It does not import Mathlib or this project. It enumerates all sixteen events on four points and checks invariance by finite computation.

Save the following as ErgodicBaseWorksheet.lean in a temporary directory outside the repository:

import Std

namespace ErgodicBaseWorksheet

inductive Point where
  | p0
  | p1
  | p2
  | p3
deriving Repr, DecidableEq

def points : List Point := [.p0, .p1, .p2, .p3]

def cycle : Point → Point
  | .p0 => .p1
  | .p1 => .p2
  | .p2 => .p3
  | .p3 => .p0

def split : Point → Point
  | .p0 => .p1
  | .p1 => .p0
  | .p2 => .p3
  | .p3 => .p2

def invariant (T : Point → Point) (A : List Point) : Bool :=
  points.all fun x => decide (T x ∈ A) == decide (x ∈ A)

def allEvents : List (List Point) :=
  points.foldr
    (fun x events => events ++ events.map (fun event => x :: event))
    [[]]

def alternating : List Point := [.p0, .p2]
def firstSplitCycle : List Point := [.p0, .p1]

def splitLabel : Point → Nat
  | .p0 => 0
  | .p1 => 0
  | .p2 => 1
  | .p3 => 1

def functionInvariant (T : Point → Point) (g : Point → Nat) : Bool :=
  points.all fun x => g (T x) == g x

#eval invariant cycle alternating
#eval invariant split firstSplitCycle
#eval (allEvents.filter (invariant cycle)).map fun A => A.length
#eval (allEvents.filter (invariant split)).map fun A => A.length
#eval functionInvariant split splitLabel

example : invariant cycle alternating = false := by decide
example : invariant split firstSplitCycle = true := by decide
example : (allEvents.filter (invariant cycle)).length = 2 := by decide
example : (allEvents.filter (invariant split)).length = 4 := by decide
example : functionInvariant split splitLabel = true := by decide
example : splitLabel .p0 ≠ splitLabel .p2 := by decide

end ErgodicBaseWorksheet

From that temporary directory, a human with the pinned Lean toolchain already installed can type:

elan run leanprover/lean4:v4.32.0 lean ErgodicBaseWorksheet.lean

The first two evaluations print false and true. The next two print invariant-event cardinalities \(0,4\) for the single cycle and \(0,2,2,4\) for the split system. Dividing by four gives probabilities \(0,1\) versus \(0,1/2,1/2,1\). The last evaluation prints true for the nonconstant split-system label. This finite program models strict invariance exactly; it does not implement Mathlib measures or almost-everywhere equivalence.

Try it in the repository

import NonlinearDynamics.Random.RandomCocycles.ProbabilityErgodicBase

#check MeasureTheory.IsProbabilityMeasure
#check MeasureTheory.measure_univ
#check MeasurePreserving
#check PreErgodic
#check Ergodic
#check PreErgodic.prob_eq_zero_or_one
#check Ergodic.ae_eq_const_of_ae_eq_comp_ae

#check NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.finiteHorizonLogPlusExpectation
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.finiteHorizonLogPlusExpectation_eq_integratedLogPlusNorm
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.ergodicBase_invariantEvent_prob_eq_zero_or_one
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.ergodicBase_ae_eq_const_of_ae_invariant

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

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

Boundaries and nonclaims

• An ergodic probability base is measure preserving, but a measure-preserving probability base need not be ergodic.
• The probability zero-or-one conclusion concerns invariant measurable events, not arbitrary events.
• Invariant functions are almost everywhere constant in the general theorem, not necessarily pointwise constant on every input.
• Ergodicity does not imply mixing, independence, or decay of correlations.
• Ergodicity of \(T\) does not imply ergodicity of every power \(T^n\).
• Ergodicity and probability normalization do not imply integrability of an arbitrary observable.
• Probability, ergodicity, and finite-horizon integrability still do not by themselves prove a pointwise ergodic theorem, a subadditive limit, a Lyapunov exponent, or an Oseledets splitting.

Where to continue

The ergodicity entry isolates Mathlib’s PreErgodic rigidity from the measure-preserving field of full Ergodic. The Probability Normalization and Ergodic Rigidity Before Kingman derives the complete project interface and keeps the finite-time integrability and subadditive-rate declarations visible.

The Birkhoff Convergence Events Before the Pointwise Ergodic Theorem uses invariant-event rigidity but does not assert that rigidity chooses the full-probability branch. The later Ergodic Birkhoff Limits and Normalized Space Averages adds the convergence and limit-identification theorems.

References

Mathlib contributors. Probability-measure typeclasses, Mathlib 4 documentation. The pinned source defines IsProbabilityMeasure μ by the equation μ univ = 1.

Mathlib contributors. Measure-preserving maps, Mathlib 4 documentation. This official source packages measurability and pushforward preservation.

Mathlib contributors. Ergodic maps and measures, Mathlib 4 documentation. This official source defines PreErgodic and Ergodic and proves the probability zero-or-one bridge for measurable strictly invariant events.

Mathlib contributors. Functions invariant under an ergodic map, Mathlib 4 documentation. This official source proves almost-everywhere constancy of suitably measurable almost-everywhere invariant functions.

The exact upstream Lean source audited for this entry is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.