Measure-preserving transformation

A measure-preserving transformation moves outcomes without changing their overall statistical mass. If \(T:\Omega\to\Omega\) preserves a measure \(\mu\), then every measurable event \(A\) satisfies

The preimage \(T^{-1}(A)\) is the set of starting states that land in \(A\) after one step. Preservation compares the mass of that set of starters with the mass already assigned to the target event. The equation must hold for every measurable event, not merely for one convenient example.

Start with four equally weighted states

Let

Every subset is measurable. Define the cyclic transformation

Equivalently, \(T(i)=i+1\pmod 4\). Take the event

To find its preimage, ask which starting states land in \(0\) or \(1\). State \(3\) lands in \(0\), and state \(0\) lands in \(1\), so

The sets are different, but their masses agree:

For the singleton event \(B=\{2\}\), the preimage is \(T^{-1}(B)=\{1\}\), and both masses are \(1/4\).

These checks are instances of a general finite argument. The cycle is a permutation, so the preimage of every subset contains exactly as many states as the subset itself. Uniform mass depends only on that count. Therefore

for every \(S\subseteq\Omega\), and \(T\) preserves \(\mathbb P\).

The definition uses preimages, not images

Let \((\Omega,\mathcal F,\mu)\) be a measure space. A self-map \(T:\Omega\to\Omega\) is measure preserving when:

1. \(T\) is measurable; and

2. the pushforward of \(\mu\) through \(T\) equals \(\mu\):

   \[ T_*\mu=\mu. \]

By the definition of pushforward, the second condition says that every measurable \(A\in\mathcal F\) obeys

Preimages are essential. The direct image \(T(A)\) asks where points in \(A\) go. The preimage asks which starting points will be observed inside the target event \(A\), which is exactly what pushforward measure evaluates.

The definition also works between different measured spaces, with a source measure \(\mu_a\) and target measure \(\mu_b\). In that setting preservation means \(T_*\mu_a=\mu_b\). Dynamical systems usually use the self-map case \(\mu_a=\mu_b=\mu\).

A measurable collapse that fails preservation

On the same four-state probability space, define

Because every subset of this finite space is measurable, every function from \(\Omega\) to itself is measurable. In particular, \(C\) is measurable.

Now test the singleton event

Two states collapse into \(0\), so

Consequently,

The event \(F\) witnesses failure of the equality required for every measurable event, so \(C\) is not measure preserving. The pushforward law has mass \(1/2\) at \(0\), mass \(1/2\) at \(2\), and no mass at \(1\) or \(3\). It is not the original uniform law.

The example isolates the difference:

• measurability guarantees that preimages of measurable events are still measurable;
• measure preservation additionally requires those preimages to have the correct masses.

Measurability makes the comparison legal. It does not make the equality true.

One event cannot certify the whole measure

The same collapsing map passes a nontrivial test. Let

Since \(C\) only takes the values \(0\) and \(2\),

and hence

The whole-space event also always passes for any self-map:

Neither equality proves preservation. Equality of measures means agreement on every measurable event. A single witness can disprove preservation, as \(F=\{0\}\) did, but a single successful event cannot prove it.

There is another distinction hiding here. An event is invariant when \(T^{-1}(A)=A\) as sets. Under the four-cycle, the earlier event \(A=\{0,1\}\) is not invariant because its preimage is \(\{3,0\}\), yet its mass is preserved. A measure-preserving map need not fix individual events; it must preserve the mass of all of them.

Preservation is not ergodicity

Ergodicity is a rigidity property added on top of measure preservation. A measure-preserving system is ergodic when every measurable invariant event is null or conull.

The four-cycle is ergodic under the uniform probability measure. If a set is unchanged by taking its one-step preimage, membership of one state forces membership of the next state around the entire cycle. The only invariant sets are therefore \(\varnothing\) and \(\Omega\).

But preservation alone does not imply ergodicity. The identity map

preserves every measure, because \(I^{-1}(A)=A\) for every event. On the four-state uniform space, each singleton is an invariant event of mass \(1/4\). Those intermediate-mass invariant events show that the identity system is not ergodic.

Thus the logical relationship is:

while the converse fails.

Why orbit averages need preservation

A Birkhoff sum samples an observable \(g\) along an orbit:

If \(T\) preserves \(\mu\), then every iterate \(T^j\) also preserves \(\mu\). Pulling \(g\) back along \(T^j\) therefore leaves its distributional mass controlled. In particular, if \(g\) is integrable, then \(g\circ T^j\) is integrable. The project’s finite Birkhoff-sum theorem adds these integrable orbit terms.

This use of preservation does not assume ergodicity. Integrability of finite orbit sums needs stable mass under the dynamics. Identifying a long-time limit with a constant requires additional rigidity.

In Lean: the event equation

μ (T ⁻¹' A) = μ A

Mathlib packages the global property as one proof object:

hT : MeasurePreserving T μ μ

Exact project usage

The project’s discrete matrix cocycle stores preservation of its base map as a field, separately from measurability of its matrix generator:

structure DiscreteMatrixCocycle (μ : Measure Ω) where
  base : Ω → Ω
  generator : RandomMatrix Ω ι ι ℂ
  base_preserving : MeasurePreserving base μ μ
  measurable_generator : Measurable generator

The same module proves that every natural-number iterate preserves the measure:

theorem base_iterate_preserving (C : DiscreteMatrixCocycle (ι := ι) μ)
    (k : ℕ) : MeasurePreserving C.base^[k] μ μ :=
  C.base_preserving.iterate k

The Birkhoff module uses exactly that kind of hypothesis when it proves finite orbit sums integrable:

theorem integrable_birkhoffSum (hT : MeasurePreserving T μ μ)
    (hg : Integrable g μ) (n : ℕ) : Integrable (birkhoffSum T g n) μ := by
  change Integrable (fun ω ↦ ∑ j ∈ Finset.range n, g (T^[j] ω)) μ
  apply integrable_finsetSum
  intro j _hj
  change Integrable (g ∘ T^[j]) μ
  exact (hT.iterate j).integrable_comp_of_integrable hg

The last line says: preservation passes to the \(j\)-th iterate, and that iterate preserves integrability under composition. No ergodicity hypothesis appears in this finite theorem.

Enumerate the four-state test locally

On the uniform four-state space, mass in quarters equals the number of states in an event. This bounded Std worksheet enumerates all sixteen events. It checks that the cycle preserves every event and identifies the singleton that witnesses failure for the collapse. Save it as /tmp/MeasurePreservingScratch.lean on a normal Mac or Linux computer:

import Std

namespace MeasurePreservingScratch

def states : List Nat := [0, 1, 2, 3]

def cycle (state : Nat) : Nat :=
  (state + 1) % 4

def collapse (state : Nat) : Nat :=
  if state < 2 then 0 else 2

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

def massQuarters (event : List Nat) : Nat :=
  event.length

def allEvents : List (List Nat) :=
  [[], [0], [1], [2], [3],
   [0, 1], [0, 2], [0, 3], [1, 2], [1, 3], [2, 3],
   [0, 1, 2], [0, 1, 3], [0, 2, 3], [1, 2, 3], states]

def preservesEveryEvent (T : Nat → Nat) : Bool :=
  allEvents.all (fun event =>
    massQuarters (preimage T event) == massQuarters event)

def halfEvent : List Nat := [0, 1]
def singletonZero : List Nat := [0]

#eval preimage cycle halfEvent
#eval [massQuarters (preimage cycle halfEvent), massQuarters halfEvent]
#eval preimage collapse singletonZero
#eval [massQuarters (preimage collapse singletonZero),
       massQuarters singletonZero]
#eval [preservesEveryEvent cycle, preservesEveryEvent collapse]

example : preimage cycle halfEvent = [0, 3] := by decide
example : massQuarters (preimage cycle halfEvent) = 2 := by decide
example : preimage collapse singletonZero = [0, 1] := by decide
example : preservesEveryEvent cycle = true := by decide
example : preservesEveryEvent collapse = false := by decide

end MeasurePreservingScratch

Type these commands exactly:

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

This exact standalone worksheet was executed successfully with Lean 4.32.0. It printed:

[0, 3]
[2, 2]
[0, 1]
[2, 1]
[true, false]

The list [0, 3] is the same set as the page’s \(\{3,0\}\); lists retain the ascending enumeration order. The next line compares equal masses \(2/4\) and \(2/4\). For the collapse, the singleton preimage has mass \(2/4\) instead of \(1/4\). This exhaustive finite test is possible because there are only sixteen events. It is not a general proof of MeasurePreserving.

Full project check

The next worksheet is a full project check. It uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory:

import NonlinearDynamics.Random.RandomCocycles.BirkhoffConvergence

open MeasureTheory Set

#check MeasurePreserving
#check MeasurePreserving.measure_preimage
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.base_preserving
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.base_iterate_preserving
#check NonlinearDynamics.Random.RandomCocycles.integrable_birkhoffSum

variable {Ω : Type*} [MeasurableSpace Ω]
variable (μ : Measure Ω) (T : Ω → Ω) (A : Set Ω)

example (hT : MeasurePreserving T μ μ) (hA : MeasurableSet A) :
    μ (T ⁻¹' A) = μ A := by
  exact hT.measure_preimage hA.nullMeasurableSet

The first two commands inspect Mathlib’s global certificate and its preimage theorem. The next three inspect the exact project fields and consumers shown above. The final example turns the mathematical sentence into a checked Lean statement: hA proves that \(A\) is measurable, its nullMeasurableSet consequence supplies the slightly more general hypothesis accepted by Mathlib, and hT.measure_preimage returns the equality.

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

Distinctions and failure modes

Where to continue

Read measure for the mass assignment being preserved and event for the measurable sets on which the preimage equation is tested. Read measurable space for the gate that makes those preimages admissible. Then read ergodicity for the additional condition that collapses invariant events to null or conull ones.

The chapter Birkhoff Limits, Invariant Sigma Algebras, and Conditional Expectation shows how preservation supports the orbit-average analysis before any ergodic specialization.

References

Mathlib contributors. Measure-preserving maps, Mathlib 4 documentation. This official implementation reference defines MeasurePreserving and states MeasurePreserving.measure_preimage.

Karl Petersen. Ergodic Theory, Cambridge University Press, 1983. This is a standard reference for measure-preserving transformations, invariant events, ergodicity, and orbit averages.

Nonlinear Dynamics in Lean contributors. Discrete.lean and BirkhoffConvergence.lean, the checked project sources for the bundled measure-preserving cocycle base, its iterates, and finite Birkhoff integrability.