Birkhoff Convergence Events Before the Pointwise Ergodic Theorem

Base camp: a two-state average you can finish by hand

Let the state space be \(\Omega=\{a,b\}\). One deterministic update swaps the states:

An observable is a function that assigns a reading to each state. Take

Starting at \(a\), the readings are \(0,2,0,2,\ldots\). Starting at \(b\), they are \(2,0,2,0,\ldots\). Write \(S_n^g(x)\) for the sum of the first \(n\) readings from \(x\), and \(A_n^g(x)=S_n^g(x)/n\) for \(n\gt0\). Lean’s totalized convention also sets \(A_0^g(x)=0\).

The first values are completely explicit:

The table suggests a limit, but a finite table cannot prove one. The formulas for every \(k\ge1\) do:

Both possible starts therefore have convergent averages with limit \(1\). The convergence event is the set of starting states whose full average sequence tends to some finite real number. For this model, it is the whole state space:

That is a direct every-point calculation. It does not use ergodicity to choose a branch of a dichotomy.

A finite-horizon measurability and integrability ledger

Give \(\Omega\) its full power-set measurable space and the uniform probability measure \(\mu(\{a\})=\mu(\{b\})=1/2\). Every subset is measurable, so every function from this two-point space to \(\mathbb R\) is a measurable function . Every such function with finite values is also integrable .

Here is the complete finite ledger through horizon four:

| \(n\) | \((S_n(a),S_n(b))\) | \((A_n(a),A_n(b))\) | \(\int |S_n|\,d\mu\) | \(\int |A_n|\,d\mu\) | measurable? | integrable? | |—:|—:|—:|—:|—:|—:|—:| | \(0\) | \((0,0)\) | \((0,0)\) | \(0\) | \(0\) | yes | yes | | \(1\) | \((0,2)\) | \((0,2)\) | \(1\) | \(1\) | yes | yes | | \(2\) | \((2,2)\) | \((1,1)\) | \(2\) | \(1\) | yes | yes | | \(3\) | \((2,4)\) | \((2/3,4/3)\) | \(3\) | \(1\) | yes | yes | | \(4\) | \((4,4)\) | \((1,1)\) | \(4\) | \(1\) | yes | yes |

The general Lean theorems mirror this elementary ledger. Measurability of \(T\) and \(g\) makes every finite sum and average measurable. Measure preservation plus integrability of \(g\) makes every finite sum and average integrable. Those are finite-horizon statements; they do not yet discuss a limit.

Delete one reading, then restore it

The basic prefix identity is

For \(n=4\) and \(\omega=a\), every number is visible:

Normalize and solve in either direction:

The first line deletes the initial reading; the second restores it. For a general fixed value \(g(\omega)\), its normalized contribution is divided by a growing horizon and tends to zero. That is the mechanism behind the same-limit theorem later in the chapter.

A deterministic near miss: bounded readings need not settle

Now use a separate state space \(\Omega=\mathbb N\), the shift \(T(k)=k+1\), and a bounded zero-one observable. Set \(g(0)=0\). For \(m\ge0\), put

Thus the values are \(1\) on \(1,\ldots,9\), \(0\) on \(10,\ldots,99\), \(1\) on \(100,\ldots,999\), and so on. At the first four decimal endpoints:

For \(r\ge0\), the number of ones below both \(10^{2r+1}\) and \(10^{2r+2}\) is

Dividing by the two different horizons gives

One sequence cannot converge to two distinct real limits. Hence \(0\notin E(T,g)\). The readings are bounded; the failure comes from successively longer blocks pulling the running mean into two different camps. No measure has been introduced, so this example does not contradict a pointwise ergodic theorem. It only proves that the event definition alone cannot supply membership.

Why formalize the event before proving a pointwise theorem?

There is a seductive but invalid shortcut in ergodic formalization. Define the set where the averages converge, prove that the set is invariant, invoke ergodicity, and then speak as if convergence had been established almost everywhere. Ergodicity does not justify that last step. It says an invariant measurable event is trivial up to null sets. The trivial event may be the empty one.

Random-matrix-theory milestone 22 (RMT-22) formalizes everything in that sentence except the shortcut. It starts with Mathlib’s finite birkhoffSum and birkhoffAverage, supplies their missing real measurability and finite integrability lemmas, defines the convergence event, transports that event across almost-everywhere representatives, proves a boundedness-free finite-prefix equivalence, and derives conditional ergodic dichotomies. It also compiles a divergent example, making it impossible to mistake the event definition for an existence theorem.

The compact term page is Birkhoff convergence event . The declaration-complete implementation narrative is Birkhoff Convergence Events and Ergodic Rigidity in Lean. The finite combinatorial predecessor is Finite Ordered Interval Packing for Nonpositive Subadditive Processes.

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. define a finite Birkhoff sum and average with the correct zero-based range;
2. explain why Mathlib’s time-zero average is totalized to zero;
3. prove finite measurability from measurable iterates and finite sums;
4. prove finite integrability from preservation and one-step integrability;
5. define the convergence event without asserting membership;
6. state why a real convergence event is measurable for a measurable sequence;
7. distinguish ordinary measurability, almost-everywhere measurability, and null measurability;
8. explain why integrability does not upgrade the supplied representative to ordinary measurability;
9. construct an ordinarily measurable representative with AEMeasurable.mk;
10. state where quasi-measure preservation enters representative transport;
11. explain the countable all-horizon intersection behind event congruence;
12. derive both positive-index finite-prefix identities;
13. prove convergence at \(\omega\) implies convergence at \(T\omega\) to the same limit;
14. prove the converse without assuming that \(T\) is invertible;
15. deduce exact preimage invariance of the event;
16. distinguish preimage invariance from image invariance;
17. explain why ordinary measurable rigidity needs only PreErgodic;
18. explain why the representative-safe path uses QuasiErgodic;
19. derive a probability zero-one corollary from an almost-everywhere dichotomy;
20. explain why zero-measure rigidity is formally valid and informationally vacuous;
21. interpret the candidate one-step event without assuming anything about \(X_0\);
22. interpret the matrix-cocycle wrapper without generator integrability;
23. explain why the empty matrix index needs no special exclusion;
24. reproduce the divergent successor-orbit example;
25. classify each of the thirty-seven public declarations by proof layer;
26. state the common axiom footprint of the high-level theorems;
27. distinguish event rigidity from convergence existence;
28. state what a pointwise ergodic theorem would add;
29. explain why this milestone does not complete Kingman’s theorem;
30. identify the next analytic dependencies without overclaiming them;
31. derive the even and odd average formulas for the two-state swap;
32. prove decimal-block nonconvergence from the limits \(10/11\) and \(1/11\);
33. run the byte-identical standalone Std worksheet on a normal macOS or Linux machine; and
34. distinguish all thirty-seven public declarations from the imported helper APIs and twelve anonymous source probes.

The common setup and notation ledger

Let:

• \(\Omega\) be a type equipped with a measurable space;
• \(\mu\) be a measure on \(\Omega\);
• \(T:\Omega\to\Omega\) be a discrete-time map;
• \(T^j\) be its \(j\)-fold iterate;
• \(g,h:\Omega\to\mathbb R\) be real observables;
• \(n\in\mathbb N\) be a finite horizon;
• \(\omega\in\Omega\) be a starting point; and
• \(A_n^g(\omega)\) denote the real Birkhoff average of \(g\) along the first \(n\) orbit positions of \(\omega\).

The almost-everywhere equality

means that the set of points where the two functions differ has \(\mu\)-measure zero. The notation \(E=F\) almost everywhere for sets means their membership predicates agree outside a μ-null set. The almost everywhere glossary entry gives the foundational distinction from pointwise equality.

The object below every asymptotic theorem

Mathlib defines the finite Birkhoff sum by

The finite set Finset.range n contains \(0,1,\ldots,n-1\). Thus \(S_0^g=0\), \(S_1^g(\omega)=g(\omega)\), and

The alternative successor law peels from the other end:

The finite average is

Lean works in a division semiring where inversion is total. Consequently \(0^{-1}=0\) and \(A_0^g=0\). This is a useful API convention: formulas have a value at every natural horizon. It is not evidence about the value of a different process \(X_0\), and it cannot turn a positive-time argument into a time-zero theorem.

Finite measurability

Assume \(T\) and \(g\) are measurable. The proof of measurable_birkhoffSum follows the displayed sum literally:

1. hT.iterate j makes every finite iterate measurable;
2. hg.comp makes \(g\circ T^j\) measurable; and
3. Finset.measurable_sum closes the finite sum.

The average is a constant multiple of the sum, so measurable_birkhoffAverage needs no new dynamics. These theorems use neither \(\mu\) nor preservation.

Finite integrability

Assume instead that \(T\) preserves \(\mu\) and \(g\) is integrable. Every iterate \(T^j\) also preserves \(\mu\). Mathlib’s MeasurePreserving.integrable_comp_of_integrable therefore makes \(g\circ T^j\) integrable. A finite sum of integrable functions is integrable, and scalar multiplication gives the average theorem.

No finite-measure or probability typeclass is needed. Preservation, not probability, is what moves integrability along the orbit.

Convergence becomes a subset

Define

This definition packages a property of a whole sequence into a set. It has three deliberate features.

First, the limit is existential. The event asks whether there is some finite real limit, not whether the limit equals a chosen constant. Second, the target is the real line. A sequence tending to positive infinity is outside the event. Third, membership is pointwise. Measure theory enters only when one asks whether the set is measurable or how large it is.

The simp theorem mem_birkhoffConvergenceSet_iff is definitionally true, but its public name matters. It gives rewriting tools a stable boundary and makes boundary probes readable.

The logical direction must remain visible:

A set-builder expression can define the set of solutions to an impossible equation. Naming the set does not solve the equation.

Ordinary measurability gives a measurable event

Suppose each map \(\omega\mapsto A_n^g(\omega)\) is measurable. The real line is a completely metrizable second-countable space whose open sets are measurable. Mathlib’s MeasureTheory.measurableSet_exists_tendsto states that the set of points where a measurable sequence converges to some target point is measurable.

Applying it yields

This theorem consumes only ordinary measurability of \(T\) and \(g\). It does not consume a measure, so it cannot depend on probability, preservation, integrability, or ergodicity.

The proof is topological as well as measurable. Convergence to some real can be expressed through countably many accuracy and tail conditions. The second-countability and complete-metrizability hypotheses are the library’s general route to making that description measurable. RMT-22 reuses the general theorem instead of reconstructing a real-specific countable formula.

An integrable observable is only measurable almost everywhere

The raw function stored in an Integrable g μ proof need not be ordinarily measurable at every point. It is almost-everywhere strongly measurable. Since the target is real, that gives almost-everywhere measurability, but exceptional values remain possible.

The safe route begins one layer lower with

hg : AEMeasurable g μ

Mathlib’s representative API constructs hg.mk g, an ordinarily measurable function equal to \(g\) almost everywhere. Call it \(\widetilde g\). The event \(E(T,\widetilde g)\) is measurable by the preceding section. To transfer that fact back to \(E(T,g)\), one must prove the two events agree almost everywhere.

Why quasi-measure preservation appears

From \(g=\widetilde g\) almost everywhere, it does not follow for an arbitrary map \(T\) that

almost everywhere. The exceptional set is pulled back by \(T^j\). A quasi-measure-preserving self-map sends null sets to null preimages, which is exactly the property needed.

Mathlib already proves fixed-horizon transport:

for each \(n\). Event convergence depends on every \(n\), so RMT-22 takes the countable intersection of these almost-everywhere facts with ae_all_iff. Outside one null set, the two entire sequences agree term by term. They therefore converge to exactly the same finite limits.

This gives

The event for \(g\) is consequently null measurable. It agrees almost everywhere with an ordinarily measurable event, but RMT-22 never claims the raw representative’s event is itself ordinarily measurable.

Three public interfaces, one proof core

RMT-22 exposes:

• nullMeasurableSet_birkhoffConvergenceSet_of_aemeasurable;
• nullMeasurableSet_birkhoffConvergenceSet_of_aestronglyMeasurable; and
• nullMeasurableSet_birkhoffConvergenceSet_of_integrable.

These are top-level theorem names, not declarations placed inside the Integrable namespace as though they were upstream methods. The suffix records the premise through which each corollary enters. The primary mathematics lives in the almost-everywhere-measurable theorem.

Delete one finite prefix without boundedness

The event is invariant because passing from \(\omega\) to \(T\omega\) deletes the first orbit value. A finite prefix cannot affect convergence of normalized averages, but formalizing that sentence requires exact coefficient control.

For every \(n\in\mathbb N\), RMT-22 proves

If \(A_n^g(\omega)\to c\), then the shifted subsequence \(A_{n+2}^g(\omega)\to c\). The first coefficient tends to one and the final correction tends to zero. Hence \(A_n^g(T\omega)\to c\).

The converse identity is

If the shifted averages converge to \(c\), the correction again vanishes and the coefficient again tends to one. Thus the original averages converge to the same \(c\).

Why the formulas start at positive indices

The denominators are \(n+1\) and \(n+2\), so they are nonzero. Writing the identities directly at index \(n\) would force a separate positive-horizon premise or invite a vacuous time-zero division. The successor form keeps the useful theorem total in \(n\) while every displayed denominator remains positive.

Why no boundedness premise is needed

Mathlib already contains exact shifted-difference identities and boundedness-based convergence results under bounded-orbit or global boundedness hypotheses. RMT-22 does not claim that no shift API existed upstream. Its contribution is the boundedness-free same-limit equivalence obtained by solving the exact finite identities in both directions and taking limits.

The proof uses only real algebra and elementary sequence limits. It needs no measurability, measure, preservation, integrability, boundedness, or invertibility.

Exact preimage invariance, not image invariance

Combining both limit directions gives

Existentially quantify \(c\). Pointwise membership then satisfies

This is exactly the set equality

The theorem is stronger than almost-everywhere invariance and weaker than an image statement. If \(T\) is constant on a two-point space, it is not injective, yet the preimage equation remains valid. No inverse is constructed.

One must not rewrite the result as \(T(E)=E\). Image equality can fail for a nonsurjective map because points outside the image have no predecessor. The formal module makes no image-invariance declaration.

Two ergodic routes, two precise receivers

Mathlib separates pre-ergodicity, quasi-ergodicity, and ergodicity.

• PreErgodic T μ says ordinarily measurable strictly invariant sets are almost everywhere empty or full.
• QuasiErgodic T μ adds quasi-measure preservation and supports null-measurable, almost-invariant sets.
• Ergodic T μ adds full measure preservation to the same pre-ergodic core.

The ordinarily measurable event and its exact preimage equation need only the first receiver:

provided the event’s measurability is supplied.

The representative-safe event may be only null measurable. Its generic rigidity theorem therefore takes QuasiErgodic T μ. Exact invariance is converted to almost-everywhere invariance, and Mathlib’s QuasiErgodic.ae_empty_or_univ₀ closes the dichotomy.

An ordinary ergodic map can enter through hT.quasiErgodic. Keeping the generic receiver weak makes the dependency visible instead of baking a stronger project-specific assumption into the theorem.

Probability converts conull to the number one

Under [IsProbabilityMeasure μ], the full space has measure one. An almost-everywhere-empty event has measure zero, while an almost-everywhere-full event has measure one. RMT-22 therefore derives

Probability does not create the dichotomy. Ergodic rigidity creates it; probability converts the full branch into the numeral one.

The zero-measure boundary

Every measurable map is quasi-ergodic for the zero measure. Every two sets are equal almost everywhere for that measure. The null-or-conull result therefore compiles for every observable, but it carries no information about pointwise membership. RMT-22 includes this probe because it exposes the difference between a valid almost-everywhere proposition and a substantive probability statement.

In Lean: seven bridges from the ledger to conditional rigidity

Each bridge presents one idea in spoken mathematics, paper notation, and exact project syntax. The first two concern one finite horizon. The next three build and shift the convergence event. The final two state exact invariance and its conditional measure-theoretic consequences.

Bridge 1: name one finite orbit average

birkhoffAverage ℝ T g n ω

Bridge 2: state the finite measure ledger

measurable_birkhoffAverage hT hg n

Bridge 3: turn convergence into point membership

mem_birkhoffConvergenceSet_iff

Bridge 4: transport the event across representatives

birkhoffConvergenceSet_ae_eq_of_ae_eq hT hgh

Bridge 5: delete or restore one prefix without changing the limit

tendsto_birkhoffAverage_apply_base_iff

Bridge 6: express pointwise equivalence as exact set invariance

preimage_birkhoffConvergenceSet T g

Bridge 7: keep rigidity and existence separate

birkhoffConvergenceSet_ae_empty_or_univ_of_integrable hg hT

Try the exact declarations in the repository

import NonlinearDynamics.Random.RandomCocycles.BirkhoffConvergence

open MeasureTheory Set Filter
open NonlinearDynamics.Random.RandomCocycles

#check measurable_birkhoffSum
#check measurable_birkhoffAverage
#check integrable_birkhoffSum
#check integrable_birkhoffAverage
#check birkhoffConvergenceSet
#check mem_birkhoffConvergenceSet_iff
#check measurableSet_birkhoffConvergenceSet
#check birkhoffConvergenceSet_ae_eq_of_ae_eq
#check nullMeasurableSet_birkhoffConvergenceSet_of_aemeasurable
#check nullMeasurableSet_birkhoffConvergenceSet_of_aestronglyMeasurable
#check nullMeasurableSet_birkhoffConvergenceSet_of_integrable
#check birkhoffAverage_succ_apply_base
#check tendsto_birkhoffAverage_apply_base
#check birkhoffAverage_succ_succ_apply
#check tendsto_birkhoffAverage_of_apply_base
#check tendsto_birkhoffAverage_apply_base_iff
#check preimage_birkhoffConvergenceSet
#check birkhoffConvergenceSet_ae_empty_or_univ_of_measurableSet
#check birkhoffConvergenceSet_ae_empty_or_univ_of_nullMeasurableSet
#check birkhoffConvergenceSet_ae_empty_or_univ_of_aemeasurable
#check birkhoffConvergenceSet_ae_empty_or_univ_of_aestronglyMeasurable
#check birkhoffConvergenceSet_ae_empty_or_univ_of_integrable
#check measure_birkhoffConvergenceSet_eq_zero_or_one_of_measurableSet
#check measure_birkhoffConvergenceSet_eq_zero_or_one_of_nullMeasurableSet
#check measure_birkhoffConvergenceSet_eq_zero_or_one_of_aemeasurable
#check measure_birkhoffConvergenceSet_eq_zero_or_one_of_aestronglyMeasurable
#check measure_birkhoffConvergenceSet_eq_zero_or_one_of_integrable
#check oneStepBirkhoffConvergenceSet
#check IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_oneStepBirkhoffConvergenceSet
#check IsIntegrableSubadditiveProcessCandidate.preimage_oneStepBirkhoffConvergenceSet
#check IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffConvergenceSet_ae_empty_or_univ
#check IsIntegrableSubadditiveProcessCandidate.measure_oneStepBirkhoffConvergenceSet_eq_zero_or_one
#check DiscreteMatrixCocycle.generatorLogPlusBirkhoffConvergenceSet
#check DiscreteMatrixCocycle.measurableSet_generatorLogPlusBirkhoffConvergenceSet
#check DiscreteMatrixCocycle.preimage_generatorLogPlusBirkhoffConvergenceSet
#check DiscreteMatrixCocycle.generatorLogPlusBirkhoffConvergenceSet_ae_empty_or_univ
#check DiscreteMatrixCocycle.measure_generatorLogPlusBirkhoffConvergenceSet_eq_zero_or_one

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

Type both ledgers yourself with Lean and Std

The next worksheet imports only Lean’s small Std library. It computes both starts of the two-state swap, checks the finite prefix identity, and computes the first four decimal-block endpoints with exact rational numbers. It does not import Mathlib, create a measure, or prove an infinite limit.

Save this exact text as /tmp/BirkhoffConvergenceTutorial.lean:

import Std

namespace BirkhoffConvergenceTutorial

inductive Point where
  | a
  | b
  deriving Repr, DecidableEq

def step : Point → Point
  | .a => .b
  | .b => .a

def observe : Point → Nat
  | .a => 0
  | .b => 2

def iterate : Nat → Point → Point
  | 0, p => p
  | n + 1, p => iterate n (step p)

def orbitValues (n : Nat) (p : Point) : List Nat :=
  (List.range n).map fun j => observe (iterate j p)

def orbitSum (n : Nat) (p : Point) : Nat :=
  (orbitValues n p).sum

def orbitAverage (n : Nat) (p : Point) : Rat :=
  if n = 0 then 0 else (orbitSum n p : Rat) / (n : Rat)

def decadeValueAux : Nat → Nat → Bool → Nat
  | 0, _, _ => 0
  | fuel + 1, n, oneBlock =>
      if n < 10 then
        if oneBlock then 1 else 0
      else
        decadeValueAux fuel (n / 10) (!oneBlock)

def decadeValue (n : Nat) : Nat :=
  if n = 0 then 0 else decadeValueAux (n + 1) n true

def decadeOnes (n : Nat) : Nat :=
  ((List.range n).map decadeValue).sum

def decadeAverage (n : Nat) : Rat :=
  if n = 0 then 0 else (decadeOnes n : Rat) / (n : Rat)

#eval orbitValues 8 .a
#eval orbitValues 8 .b
#eval (List.range 9).map fun n => (n, orbitSum n .a, orbitAverage n .a)
#eval (List.range 9).map fun n => (n, orbitSum n .b, orbitAverage n .b)
#eval (orbitSum 5 .a, observe .a + orbitSum 4 (step .a))
#eval (orbitAverage 4 (step .a),
  (5 : Rat) / 4 * orbitAverage 5 .a - (observe .a : Rat) / 4)
#eval [10, 100, 1000, 10000].map fun n =>
  (n, decadeOnes n, decadeAverage n)

example : orbitValues 8 .a = [0, 2, 0, 2, 0, 2, 0, 2] := by
  native_decide

example : orbitValues 8 .b = [2, 0, 2, 0, 2, 0, 2, 0] := by
  native_decide

example :
    (List.range 12).all (fun n =>
      orbitSum (n + 1) .a = observe .a + orbitSum n (step .a)) = true := by
  native_decide

example :
    [10, 100, 1000, 10000].map (fun n => decadeAverage n) =
      [9 / 10, 9 / 100, 909 / 1000, 909 / 10000] := by
  native_decide

end BirkhoffConvergenceTutorial

From the repository root or any other directory, type:

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

The byte-for-byte standard output is:

[0, 2, 0, 2, 0, 2, 0, 2]
[2, 0, 2, 0, 2, 0, 2, 0]
[(0, 0, 0),
 (1, 0, 0),
 (2, 2, 1),
 (3, 2, (2 : Rat)/3),
 (4, 4, 1),
 (5, 4, (4 : Rat)/5),
 (6, 6, 1),
 (7, 6, (6 : Rat)/7),
 (8, 8, 1)]
[(0, 0, 0),
 (1, 2, 2),
 (2, 2, 1),
 (3, 4, (4 : Rat)/3),
 (4, 4, 1),
 (5, 6, (6 : Rat)/5),
 (6, 6, 1),
 (7, 8, (8 : Rat)/7),
 (8, 8, 1)]
(4, 4)
(1, 1)
[(10, 9, (9 : Rat)/10), (100, 9, (9 : Rat)/100), (1000, 909, (909 : Rat)/1000), (10000, 909, (909 : Rat)/10000)]

The first two lists are the orbit readings. The next two ledgers contain \((n,S_n,A_n)\). The pair (4, 4) checks \(S_5(a)=g(a)+S_4(Ta)\), and (1, 1) checks the normalized delete-one-prefix identity. The final line reproduces every endpoint count and fraction in the nonconvergence table.

Standalone tutorial, suitable for a normal macOS or Linux machine. It imports only Std and never opens this project’s Mathlib dependency graph. This exact file and output were checked with the pinned Lean 4.32.0 toolchain. The full project declarations use the command in the preceding repository box.

Thin wrappers should keep thin premises

Integrable subadditive-process candidates

Let \(X:\mathbb N\to\Omega\to\mathbb R\) satisfy the RMT-17 candidate interface: every \(X_n\) is integrable and the family is shifted subadditive. RMT-22 defines

The subadditive inequality is not used in the event definition, exact invariance, or one-step integrability extraction. The wrapper remains useful because it connects the project process to a standard event; the candidate package itself does not imply convergence.

The null-measurability wrapper takes the candidate and a quasi-measure-preserving map. The rigidity and zero-one wrappers take QuasiErgodic. They do not take a stronger Ergodic receiver merely because matrix-cocycle applications often have one.

The value \(X_0\) remains irrelevant. A compiled model sets \(X_0=1\) and \(X_n=0\) for positive \(n\) over the zero measure. It satisfies the candidate laws, and its one-step event is the whole space.

Discrete matrix cocycles

For a discrete matrix cocycle \(C\), define

The cocycle already stores measurability of its generator and preservation of its base. Earlier modules prove ordinary measurability of the one-step log-positive norm. Therefore \(E_C\) is ordinarily measurable, and exact preimage invariance is purely pointwise.

The rigidity wrapper takes only PreErgodic C.base μ. It does not require C.HasIntegrableGeneratorLogPlus, because no proof step uses integrability. It does not require Nonempty ι, because the empty-index matrix observable remains measurable and the event remains well-typed. An explicit ι := Empty probe calls both wrappers without an hC hypothesis.

This is premise auditing in action: a natural application may possess stronger structure, but a theorem should expose only what its proof consumes.

The complete thirty-seven-declaration ledger

The frozen RMT-22 source is 602 lines and has SHA-256 cec39333cd0751ca7b52283049cf11ec8a8a8870eff3dbeaf32bfda81d111fbd. It contains exactly thirty-seven public declarations and twelve anonymous compiled boundary probes. The named interface appears below in source order.

Finite measurability and integrability

The first pair has no measure argument. The second pair has no probability or ergodicity premise.

Event and representative layer

The ae_eq in declaration 8 refers to equality of event membership almost everywhere. It does not produce set equality pointwise.

Positive-index shift and exact invariance

All six are pointwise and measure free. Declaration 17 says nothing about the image \(T(E)\).

Generic rigidity and probability laws

The five numerical theorems require a probability measure. The five preceding dichotomies do not.

Candidate specialization

The wrapper never states that \(X_n/n\) converges. It studies only ordinary Birkhoff averages of the one-step observable \(X_1\).

Matrix-cocycle specialization

The source-level count treats every declaration once. Anonymous examples and the six #print axioms commands are verification surfaces, not public API names.

Complete proof-helper map

The module declares no private named helper theorem. Its proof bodies use imported Mathlib interfaces and local have statements. The table below accounts for those helper families and shows exactly which public declarations consume them.

This map distinguishes project declarations from upstream machinery. For example, birkhoffSum_succ’ is an imported finite-sum recurrence; birkhoffAverage_succ_apply_base is this module’s new solved average identity. The 37-name ledger, this helper map, the 12-probe narrative below, and the six axiom prints together cover every source-level proof surface in the 602-line file.

Proof architecture as a dependency graph

The declarations form three main routes.

Route A: ordinary measurable observable

Probability is added only if the final conclusion must be written \(\mu(E)=0\) or \(\mu(E)=1\).

Route B: almost-everywhere representative

The quasi-measure-preserving field of QuasiErgodic supports both representative transport and the null-measurable rigidity theorem.

Route C: pointwise shift

This route is independent of A and B. It needs no measurable space at all. The final rigidity theorems join the pointwise shift route to either event measurability route.

Models that test the API boundary

The source compiles twelve anonymous probes. Each tests a possible source of accidental strengthening.

Probe 1: time zero

For every \(T,g,\omega\), Mathlib gives \(A_0^g(\omega)=0\). This tests the totalized convention and prevents prose from calling it a positive-time average.

Probes 2 and 3: zero and constant observables

The zero observable has event \(\Omega\). A constant \(c\) also has event \(\Omega\) even though the time-zero value is zero: the sequence is \(0,c,c,c,\ldots\), which converges to \(c\).

Probe 4: identity dynamics

For the identity map and arbitrary \(g\), every positive average at \(\omega\) equals \(g(\omega)\). The event is \(\Omega\) without any measurability premise.

Probe 5: a constant noninjective base

On the two-element Boolean type, the constant map is not injective. The exact preimage theorem still applies. This refutes any hidden use of invertibility.

Probe 6: representative transport

For hg : AEMeasurable g μ, the event for \(g\) is almost everywhere equal to the event for hg.mk g under quasi-measure-preserving dynamics. This tests the direction of ae_eq_mk and the set-congruence proof.

Probe 7: zero measure

Every measurable map is quasi-ergodic for the zero measure, so the event dichotomy holds for arbitrary \(g\). The statement is intentionally described as vacuous.

Probe 8: a candidate with nonzero time zero

Set \(X_0=1\) and \(X_n=0\) for every positive \(n\), over the zero measure. This is an integrable shifted-subadditive-process candidate. The one-step event is \(\Omega\). Thus no theorem silently assumes \(X_0=0\).

Probe 9: empty matrix index without generator integrability

A cocycle indexed by the empty type calls event measurability and exact invariance without HasIntegrableGeneratorLogPlus and without a nonempty-index instance.

Probe 10: abstract nonmembership

If the average sequence is proved not to tend to any real \(c\), membership in the convergence event is definitionally impossible. The simp theorem closes that argument directly.

Probes 11 and 12: an explicit divergent orbit

Take \(\Omega\) to be the natural numbers, \(T(k)=k+1\), \(g(k)=k\), and \(\omega=0\). A finite calculation gives

In the first probe, the finite-sum identity establishes the exact formula. The second proves \(n/2\to+\infty\), contradicting convergence to any finite real. Therefore \(0\notin E(T,g)\).

Axiom and source-integrity audit

RMT-22 prints the axioms of six representative high-level theorems:

• almost-everywhere event congruence;
• null measurability from an almost-everywhere measurable representative;
• the same-limit shift equivalence;
• integrable-observable ergodic rigidity;
• the candidate rigidity wrapper; and
• the matrix-cocycle rigidity wrapper.

Each print contains only propext, Classical.choice, and Quot.sound. These are the standard logical axioms inherited from Mathlib’s classical and quotient infrastructure. There is no sorry, admit, custom axiom, or unsafe declaration.

The source imports Mathlib’s finite Birkhoff algebra, quasi-measure-preserving transport, and the general measurable convergence-set theorem. It does not redefine the upstream finite sum or average.

Solved exercises

These exercises are cumulative. Try each problem before opening its solution.

Exercise 1: expand the first three sums

Write \(S_0^g(\omega)\), \(S_1^g(\omega)\), and \(S_3^g(\omega)\).

Exercise 2: explain the time-zero average

Why does \(A_0^g=0\) not imply \(X_0=0\) for a process \(X\)?

Exercise 3: locate the preservation premise

Which finite theorem needs measure preservation: measurability of the sum or integrability of the sum?

Exercise 4: definition versus witness

Does defining \(E(T,g)\) give a term of type ∃ ω, ω ∈ birkhoffConvergenceSet T g?

Exercise 5: measurable event without a measure

Why can measurableSet_birkhoffConvergenceSet omit μ entirely?

Exercise 6: the representative trap

What invalid step would occur if one wrote “\(g\) is integrable, therefore \(g\) is measurable” in the ordinary pointwise sense?

Exercise 7: why quasi-measure preservation

Let \(N=\{\omega:g(\omega)\ne h(\omega)\}\) be null. Where can the orbitwise equality fail at horizon \(j\)?

Exercise 8: fixed horizon versus every horizon

Why is one application of birkhoffAverage_ae_eq_of_ae_eq insufficient for event congruence?

Exercise 9: derive the forward shift identity

Starting from \(S_{n+2}^g(\omega)=g(\omega)+S_{n+1}^g(T\omega)\), solve for \(A_{n+1}^g(T\omega)\).

Exercise 10: preserve the limit value

Suppose \(A_n^g(\omega)\to c\). Why does the forward identity give limit \(c\), not merely existence of some limit at \(T\omega\)?

Exercise 11: no inverse map

Why does the converse shift theorem not require a point \(\upsilon\) with \(T\upsilon=\omega\)?

Exercise 12: preimage versus image

Translate \(T^{-1}E=E\) into a pointwise biconditional. Does it imply \(T(E)=E\)?

Exercise 13: identify the weakest ordinary receiver

Given a measurable set \(E\) and exact equality \(T^{-1}E=E\), which Mathlib structure suffices for the null-or-conull conclusion?

Exercise 14: identify the representative-safe receiver

Why does a null-measurable event naturally pair with QuasiErgodic T μ?

Exercise 15: do not choose the branch

Suppose ergodicity yields \(E=\varnothing\) almost everywhere or \(E=\Omega\) almost everywhere. What extra fact would rule out the first branch?

Exercise 16: probability’s exact job

What does [IsProbabilityMeasure μ] add to an already proved null-or-conull dichotomy?

Exercise 17: zero measure

Why can a set be both almost everywhere empty and almost everywhere full for the zero measure?

Exercise 18: constant observable and time zero

For \(g\equiv c\ne0\), list the average sequence and its limit.

Exercise 19: successor orbit divergence

Verify that \(A_{n+1}^g(0)=n/2\) for \(T(k)=k+1\) and \(g(k)=k\).

Exercise 20: finite real versus infinity

Why is a sequence tending to positive infinity outside the convergence event?

Exercise 21: candidate time zero

Which candidate field could force \(X_0=0\)?

Exercise 22: candidate law usage

Does preimage_oneStepBirkhoffConvergenceSet use integrability or subadditivity?

Exercise 23: cocycle integrability

Why is HasIntegrableGeneratorLogPlus absent from the cocycle event measurability theorem?

Exercise 24: empty matrix index

What breaks in the event definition when the finite matrix index is empty?

Exercise 25: classify declaration 8

Is birkhoffConvergenceSet_ae_eq_of_ae_eq a measurability theorem, an existence theorem, or a congruence theorem?

Exercise 26: count the generic rigidity family

Why are declarations 18 through 27 ten theorems rather than one theorem with many typeclass searches?

Exercise 27: axiom footprint

What would be suspicious in the printed axiom list beyond the three standard axioms reported here?

Exercise 28: distinguish Birkhoff from Kingman

What sequence does RMT-22 study for a candidate \(X\), and what sequence would a subadditive ergodic theorem study?

Exercise 29: identify the missing theorem role

What logical statement would a pointwise Birkhoff theorem add to the present event layer?

Exercise 30: state the exact summit

Summarize RMT-22 in one sentence without using the words “proves Birkhoff’s theorem.”

Premise ledger

The distinction between proof dependency and ambient structure matters. A DiscreteMatrixCocycle stores a measure-preserving base even when a specific wrapper calls only its measurability or passes an external pre-ergodic proof. The theorem should not be described as assumption free; its receiver still carries structure. It should be described as requiring no additional generator-integrability or nonempty-index premise.

Nonclaim ledger

RMT-22 does not establish:

1. that \(E(T,g)\) is nonempty for arbitrary \(T,g\);
2. that any named point belongs to the event, except in boundary examples;
3. that the event has positive measure;
4. that the conull branch of ergodic rigidity holds;
5. a maximal ergodic inequality;
6. the pointwise Birkhoff ergodic theorem;
7. convergence to a conditional expectation;
8. convergence to the space average under ergodicity;
9. convergence in integrable norm, probability, or distribution;
10. interchange of limit and integral;
11. a density or frequency theorem for marked orbit starts;
12. Kingman’s subadditive ergodic theorem;
13. almost-everywhere convergence of \(X_n/n\);
14. equality of a samplewise limit with the deterministic Fekete rate;
15. ergodicity of \(T^b\) from ergodicity of \(T\);
16. mixing, independence, or correlation decay;
17. image invariance of the convergence event;
18. a signed cocycle growth limit;
19. a Lyapunov exponent; or
20. an Oseledets filtration or splitting.

The theorem that a convergence event is null or conull is genuinely useful. It becomes decisive once another argument gives positive measure or almost-everywhere membership. It is not a substitute for that argument.

The existence theorem that RMT-22 leaves open

The classical pointwise Birkhoff ergodic theorem starts with a measure-preserving transformation and an integrable observable. In a standard probability-space formulation, it proves that the finite averages converge almost everywhere to an invariant integrable function; under ergodicity that limit is almost everywhere constant and agrees with the space average.

RMT-22 stops before every part of that existence statement. The pinned Mathlib release contains finite Birkhoff algebra, quasi-measure-preserving representative transport, ergodic rigidity, and specialized mean-ergodic results in normed settings. The Mathlib API audited for RMT-22 did not itself contain the measure-theoretic pointwise Birkhoff theorem needed here.

The project later built that analytic route in separate modules. RMT-23 supplies a finite Hopf-style maximal ergodic inequality and a horizon-uniform weak estimate for strict finite average-threshold events. The finite maximal Deep Dive begins that climb. The later Pointwise Birkhoff from Maximal Control and Dense Good Functions chapter reaches the project theorem ae_mem_birkhoffConvergenceSet_of_integrable. Under a finite measure, measure-preserving dynamics, and an integrable real observable, that theorem proves almost-everywhere membership in the convergence event.

This later result does not change what RMT-22 proves. In the present module, the null-or-conull and zero-one theorems remain conditional dichotomies. A caller that wants the conull branch must import and apply the later pointwise theorem or provide another membership argument. The later theorem also stops at convergence-event membership: it does not identify the limit with a conditional expectation or, under ergodicity, with the space average.

For the subadditive program, even a pointwise theorem for the one-step observable is not the final summit. The RMT-20 phase estimate and RMT-21 interval packing still need a checked density or frequency input to control marked starts and connect finite bounds to \(X_n/n\). Only after that analytic bridge can the project proceed toward Kingman’s theorem without adding an unsupported convergence claim.

Where to continue

The Birkhoff convergence event entry is the compact definition, boundary, and premise reference.

The Birkhoff sum entry develops the finite sum and powered-map block interpretation. The ergodic probability base entry separates preservation, probability, ergodicity, and integrability.

Probability Normalization and Ergodic Rigidity Before Kingman is the RMT-17 foundation for the two rigidity receivers and candidate wrapper.

Finite Ordered Interval Packing for Nonpositive Subadditive Processes is the immediate finite predecessor. Its marked-start density gap remains open after RMT-22.

Birkhoff Convergence Events and Ergodic Rigidity in Lean maps all thirty-seven names to their checked proofs and build commands.

Finite Maximal Ergodic Inequalities: From Orbit Maxima to Threshold Events continues the analytic route with strict finite running maxima, measure-preserving cancellation, and a positive-threshold weak estimate. It still makes no pointwise convergence claim.

Pointwise Birkhoff from Maximal Control and Dense Good Functions completes the later finite-measure maximal-closure route to ae_mem_birkhoffConvergenceSet_of_integrable. Read it after this chapter to see exactly which new hypotheses and approximation machinery choose the conull branch.

References

All Mathlib links below use the v4.32.0 revision pinned by this project. The local source authority is commit 81a5d257c8e410db227a6665ed08f64fea08e997.

Mathlib contributors. Finite Birkhoff sums, with the pinned definition and recurrence laws. The same pinned source contains the exact shifted finite-sum difference used to audit the new finite-prefix formulas.

Mathlib contributors. Finite Birkhoff averages, with the pinned totalized definition and shifted-difference identity. RMT-22 reuses these finite objects and adds a boundedness-free same-limit equivalence.

Mathlib contributors. Quasi-measure-preserving Birkhoff transport, with the pinned fixed-horizon a.e. theorem. RMT-22 takes a countable all-horizon intersection before transporting convergence events.

Mathlib contributors. Measurable convergence sets, with the pinned theorem. This is the general topological-measure bridge used for the real event.

Mathlib contributors. Almost-everywhere measurable representatives, with the pinned AEMeasurable.mk, measurable_mk, and ae_eq_mk API. The project uses this AEMeasurable layer as its primary theorem and exposes strong-measurability and integrability corollaries.

Mathlib contributors. Ergodic maps and measures, with the pinned ordinary measurable rigidity and zero-one law and null-measurable quasi-ergodic rigidity.

Mathlib contributors. Normed-space Birkhoff sums, with the pinned boundedness-based shift convergence results. These theorems define the novelty boundary accurately: shift infrastructure already existed, while RMT-22 supplies the real boundedness-free two-way same-limit statement needed for exact event invariance.

George D. Birkhoff. Proof of the Ergodic Theorem, Proceedings of the National Academy of Sciences 17(12), 656-660, 1931, DOI 10.1073/pnas.17.2.656. This primary source is the historical pointwise theorem. The current module formalizes event infrastructure before that existence result.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499-510, 1968. This primary source is the later subadditive destination. RMT-22 proves none of its normalized-process convergence conclusions.

The exact upstream revision audited for this chapter is commit 81a5d257, the v4.32.0 revision pinned by formalization/lake-manifest.json.