Invariant sigma algebra

Start with six states and two sealed cycles

Let the state space be

An event is a subset of \(\Omega\), a yes-or-no question about the current state. Declare every subset measurable, and give each state probability \(1/6\). That uniform probability measure will matter when we compare null sets; enumerating invariant events needs only the map and the measurable subsets. There are

such events: each of the six states can independently be included or excluded. Those \(64\) events form the full ambient sigma algebra \(\mathcal B\). A sigma algebra is a collection of events containing the empty event and closed under complements and countable unions. The measurable-space entry develops those closure rules from the beginning.

Now split the dynamics into two three-state cycles:

Call the two components

The preimage of an event \(S\) is

This notation does not ask for an inverse function. It asks which starting states land in \(S\) after one step.

For the left component,

The same calculation gives \(T^{-1}(R)=R\). The empty event and the whole space are also unchanged by preimage. Therefore these four events survive:

They are the complete invariant sigma algebra for this map. To see why the list is complete, suppose an invariant event contains state \(0\). Exact invariance says membership at \(x\) agrees with membership at \(T(x)\), so the event must also contain \(1\), then \(2\), then the whole left cycle. The same argument independently includes either all or none of the right cycle. There are two choices for each cycle, hence \(2^2=4\) invariant events.

Compare those four events with the smallest possible sigma algebra,

Lean calls this the bottom measurable space; probability texts often call it the trivial sigma algebra. In this example the three levels are strict:

with \(2\), \(4\), and \(64\) events respectively. Here \(\mathcal P(\Omega)\) is the power set, meaning the collection of every subset of \(\Omega\).

The two-point event \(Q=\{0,3\}\) is a quick non-example:

Having the same number of points is irrelevant. The actual membership question must remain unchanged.

The general definition

Let \((\Omega,\mathcal B)\) be a measurable space and let \(T:\Omega\to\Omega\) be any self-map. The invariant sigma algebra is

Read the two gates separately:

1. \(S\in\mathcal B\) says that \(S\) is an ambient measurable event.
2. \(T^{-1}(S)=S\) is literal equality of ordinary sets.

The collection is itself a sigma algebra. Preimage fixes the empty set and the whole space, commutes with complement, and commutes with countable union:

Ambient measurability is also preserved by the sigma-algebra closure rules. These facts prove closure of \(\mathcal I_T\).

No measure is needed to form this collection, and Mathlib’s definition does not require \(T\) to be measurable. Those hypotheses enter later when one transports integrals or proves an ergodic theorem. The raw definition is set-theoretic.

Full, invariant, and bottom information are different

The invariant sigma algebra can sit anywhere between the bottom and ambient measurable spaces:

For measurable spaces, \(\mathcal A\le\mathcal B\) means every \(\mathcal A\)-measurable event is also \(\mathcal B\)-measurable. It is an information ordering: the larger sigma algebra can answer at least as many measurable yes-or-no questions.

The same six-state space gives three exact cases:

For the identity map, no membership answer ever changes. For one six-cycle, one included state forces inclusion of all six. For the split map, only the component label survives. This is the information that a conditional expectation onto \(\mathcal I_T\) is allowed to retain.

In Lean: membership means two exact tests

MeasurableSet[MeasurableSpace.invariants T] S ↔ MeasurableSet S ∧ T ⁻¹' S = S

The pinned Mathlib definition packages the same conjunction directly:

def MeasurableSpace.invariants
    [m : MeasurableSpace Ω] (T : Ω → Ω) : MeasurableSpace Ω :=
  { m ⊓ ⟨fun S ↦ T ⁻¹' S = S, by simp, by simp,
      fun F hF ↦ by simp [hF]⟩ with
    MeasurableSet' := fun S ↦ MeasurableSet[m] S ∧ T ⁻¹' S = S }

The operational theorem is definitionally exact:

theorem MeasurableSpace.measurableSet_invariants :
    MeasurableSet[MeasurableSpace.invariants T] S ↔
      MeasurableSet S ∧ T ⁻¹' S = S

The expression m ⊓ … intersects the ambient measurable space with the preimage-fixed collection. A reader normally uses measurableSet_invariants rather than unfolding this constructor.

Mathlib also records the ambient inclusion:

MeasurableSpace.invariants_le T :
  MeasurableSpace.invariants T ≤ inferInstance

It does not assert equality with the ambient space or with bottom. The map determines where the invariant sigma algebra lies between those extremes.

In Lean: invariant-measurable functions

A real-valued measurable function \(g:\Omega\to\mathbb R\) is measurable from \(\mathcal I_T\) when the inverse image of every Borel-measurable set of real numbers is an invariant event. The Borel sets are the standard measurable subsets of the real line generated by its open intervals. Mathlib’s exact interface is

Measurable[MeasurableSpace.invariants T] g ↔
  Measurable g ∧
    ∀ U, MeasurableSet U → (g ∘ T) ⁻¹' U = g ⁻¹' U

For a target whose singleton sets are measurable, including \(\mathbb R\), this forces pointwise function invariance.

MeasurableSpace.comp_eq_of_measurable_invariants hg

In the split example, such a function may use one value on \(L\) and another on \(R\). Invariance means constant along each orbit component, not globally constant. Global almost-everywhere constancy needs the additional ergodicity hypothesis.

One-step invariance also implies invariance under every iterate:

MeasurableSpace.le_invariants_iterate T n

The reverse inclusion can fail. For the one six-cycle, \(T^2\) has two three-cycles, so it retains more events than \(T\). Equality would erase that periodic information.

Strict invariance is not invariance modulo null sets

Once a measure \(\mu\) is present, a second convention calls \(S\) invariant when its one-step preimage differs from it only on a null set :

The symmetric difference \(A\mathbin{\triangle}B\) contains the points that belong to exactly one of \(A\) and \(B\). This is invariance modulo null sets. It depends on \(\mu\); Mathlib’s MeasurableSpace.invariants T does not.

The six-state uniform example hides the distinction because every state has positive probability \(1/6\). Its only null event is empty, so equality modulo null sets reduces to literal equality there.

A two-state example exposes the gap. Let \(\Omega=\{p,q\}\), put all probability mass at \(p\), and let \(T\) send both states to \(p\). This map preserves that Dirac probability measure. For \(S=\{q\}\),

Thus \(S\) is invariant modulo null sets but is absent from Mathlib’s exact invariant sigma algebra. Exact invariance always implies modulo-null invariance. This two-state system is a counterexample to the converse, even among measure-preserving probability systems.

This distinction also separates two statements that sound similar:

• \(\mathcal I_T=\bot\) says that the only literal invariant measurable events are empty and full.
• Ergodicity says invariant measurable events are empty or full after null sets are ignored.

The first is stronger when nonempty null sets exist. An ergodic system need not have its exact invariant sigma algebra definitionally equal to bottom. For a concrete boundary, keep the same two-state Dirac probability but use the identity map. Every event is then exactly invariant, so the exact invariant sigma algebra is the full four-event ambient space. Nevertheless each event is null or conull because only \(p\) carries mass. The identity system is ergodic for this concentrated measure even though its exact invariant sigma algebra is not bottom.

Why the project uses the exact field

Random-matrix-theory milestone 27 (RMT-27) identifies finite-measure Birkhoff limits with conditional expectation onto MeasurableSpace.invariants T. Conditional expectations are unique only almost everywhere , but the sigma algebra supplied to that construction is still Mathlib’s exact field.

The project first defines one total real-valued representative birkhoffLimit T f. Where finite Birkhoff averages converge, it selects their limit; elsewhere it uses a fixed fallback. The theorem birkhoffLimit_apply_base proves the ordinary pointwise identity

on both branches. Ambient measurability plus that literal invariance lets measurable_birkhoffLimit_invariants place the chosen representative in the exact invariant sigma algebra.

Under finite total measure, a measure-preserving map , and integrability of the observable, the final theorem proves almost-everywhere convergence to

μ[f | MeasurableSpace.invariants T]

It does not identify the exact field with a completed modulo-null field. It does not need to: the proof constructs the exact representative and applies conditional-expectation uniqueness for that exact sub-sigma algebra.

A tiny standalone Lean worksheet a human can type

Standalone tutorial. This file enumerates all \(64\) finite events and filters the four that pass the split map’s exact preimage test. It recreates finite Boolean set membership; it does not define Mathlib measurable spaces, measures, null sets, or conditional expectation.

Save it as InvariantSigmaFiniteScratch.lean:

import Std

def states : List Nat :=
  List.range 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

#eval subsets.length
#eval invariantEvents splitCycles
#eval preimage splitCycles [0, 3]

example : subsets.length = 64 := by decide

example : invariantEvents splitCycles =
    [[], [3, 4, 5], [0, 1, 2], [0, 1, 2, 3, 4, 5]] := by
  decide

example : preimage splitCycles [0, 3] = [2, 5] := by decide

From the directory containing the file, type:

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

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

64
[[], [3, 4, 5], [0, 1, 2], [0, 1, 2, 3, 4, 5]]
[2, 5]

This command is suitable for an ordinary Mac or Linux machine because the worksheet imports only Std. The worksheet is a finite audit of the running example, not a proof of Mathlib’s general measure-theoretic interface, and it does not load the project or Mathlib.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomCocycles.PointwiseBirkhoffLimit

open MeasureTheory Set Filter Function
open NonlinearDynamics.Random.RandomCocycles

universe uΩ

variable {Ω : Type uΩ} [MeasurableSpace Ω]
variable {T : Ω → Ω} {S : Set Ω} {g : Ω → ℝ}
variable (hg : Measurable[MeasurableSpace.invariants T] g)

#check MeasurableSpace.invariants T
#check MeasurableSpace.measurableSet_invariants (f := T) (s := S)
#check MeasurableSpace.invariants_id (α := Ω)
#check MeasurableSpace.invariants_le T
#check MeasurableSpace.measurable_invariants_dom (f := T) (g := g)
#check MeasurableSpace.comp_eq_of_measurable_invariants hg
#check MeasurableSpace.le_invariants_iterate T 2
#check birkhoffLimit_apply_base
#check measurable_birkhoffLimit_invariants
#check setIntegral_orbit_iterate_eq
#check setIntegral_birkhoffLimit_eq
#check ae_tendsto_birkhoffAverage_condExp

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

Boundaries and nonclaims

• No measure is built into the definition. A measure enters only when a theorem asks about null sets, integrals, probability, or preservation.
• No inverse map is required. Set preimages exist for every function, including noninjective and nonsurjective maps.
• Invariant does not mean globally constant. A function may use different values on different invariant components, as the split example shows.
• Ergodicity is additional. It trivializes invariant information modulo null sets; it does not generally make the exact sigma algebra literally bottom.
• One-step and iterate invariance differ. A powered map can retain periodic phase information that one step does not.
• The sigma algebra proves no convergence by itself. Birkhoff convergence also needs analytic and measure-preserving hypotheses.
• No completion is implicit. The exact Mathlib field and a completed modulo-null invariant field must not be silently identified.

This entry does not construct an ergodic-component quotient, prove mixing, prove independence, or establish a Lyapunov exponent or an Oseledets splitting.

Where to continue

Identifying the Finite-Measure Birkhoff Limit in Lean maps RMT-27’s exact representative, invariant-set integral identities, and conditional-expectation endpoint to checked source.

Birkhoff Limits, Invariant Sigma Algebras, and Conditional Expectation builds the full proof architecture. The ergodicity entry compares the one-cycle and split-cycle systems under the same uniform probability. The Koopman operator entry develops the function-level pullback \(g\mapsto g\circ T\).

References

Mathlib contributors. Exact invariant measurable spaces, Mathlib 4.32.0 at pinned commit 81a5d257.