Convergence Without Existence: Birkhoff Events and Ergodic Rigidity in Lean

This is the proof-to-prose companion for formalization/NonlinearDynamics/Random/RandomCocycles/BirkhoffConvergence.lean. It covers all thirty-seven public declarations in exact source order and all twelve anonymous compiled boundary probes.

Its immediate predecessor is Pack the Marked Starts: Ordered Disjoint Intervals for Subadditive Cocycles in Lean. RMT-21 supplies a finite covering inequality but no mechanism making its marked set large. The earlier interface audit Probability and Ergodic Base Interfaces for Matrix Cocycles separates integrability, probability normalization, preservation, and ergodicity. RMT-22 now gives those interfaces a concrete invariant event while leaving the missing convergence theorem visible.

Reusable definitions include the Birkhoff sum , the Birkhoff convergence event , and the ergodic probability base . The parallel textbook treatment is Birkhoff Convergence Events Before the Pointwise Ergodic Theorem.

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. distinguish a finite Birkhoff sum from a totalized Birkhoff average;
2. explain why the time-zero average is exactly zero;
3. state the hypotheses for finite-horizon measurability;
4. state the different hypotheses for finite-horizon integrability;
5. explain why neither finite theorem needs a probability measure;
6. define the finite-real convergence event without asserting membership;
7. explain why a sequence of measurable real functions has a measurable convergence event;
8. distinguish measurable, almost-everywhere measurable, almost-everywhere strongly measurable, and integrable observables in this module;
9. explain why quasi-measure preservation is needed to transport null exceptions through every iterate;
10. explain why fixed-horizon almost-everywhere equality must be intersected over countably many horizons;
11. derive the forward finite-prefix average identity;
12. derive its reverse identity;
13. identify the coefficient sequences tending to one;
14. identify the endpoint terms tending to zero;
15. prove that convergence moves from \(\omega\) to \(T\omega\);
16. prove that convergence moves back without inverting \(T\);
17. distinguish equality of limits from mere equivalence of existence;
18. read exact preimage invariance as a pointwise biconditional;
19. explain why exact event invariance needs no measurable structure;
20. distinguish the measurable/pre-ergodic route from the null-measurable/quasi-ergodic route;
21. distinguish almost-everywhere empty-or-universal from numerical probability zero-or-one;
22. explain why either dichotomy remains conditional on event membership;
23. explain why the zero-measure dichotomy is true but vacuous;
24. explain why identity dynamics can have universal convergence without being ergodic;
25. identify why \(X_0\) is absent from the one-step event;
26. state which candidate fields are and are not used by each wrapper;
27. state why the cocycle event is measurable without generator integrability or a nonempty matrix index;
28. distinguish Mathlib’s existing bounded shift-difference theorem from RMT-22’s boundedness-free convergence equivalence;
29. recognize a concrete divergent orbit in the final probes; and
30. list every major analytic theorem that remains unproved.

Time averages ask two different questions

Imagine following one state \(\omega\) under repeated application of \(T\):

An observable \(g\) assigns a real reading to each visited state. The average \(A_n g(\omega)\) asks for the mean of the first \(n\) readings. At least two questions immediately arise:

1. Does the sequence \(A_n g(\omega)\) converge for this point?
2. If the set of convergent points is invariant and the system is ergodic, how large can that set be?

The first is an existence question. The second is a rigidity question. Birkhoff’s 1931 paper is part of the historical origin of modern pointwise ergodic theory, but its original setting and language should not be silently identified with every modern abstract formulation (Birkhoff, 1931). RMT-22 does not formalize that historical theorem. It isolates the event needed to state the first question, then proves a strong conditional answer to the second.

This separation is not pedantry. A set may satisfy

and therefore be null or conull under an ergodic hypothesis, while nothing yet shows that it is conull. The alternative \(E=\varnothing\) almost everywhere remains open. A zero-one theorem does not decide whether the answer is zero or one.

Three layers, three jobs

The module is easiest to understand as three layers.

The finite analytic layer proves measurability and integrability separately at every natural horizon. It uses only finite sums, iterated measurability, measure preservation, and integrability under composition.

The event layer forms the set of points where the average sequence tends to some real limit. It proves ordinary measurability when the observable is ordinary measurable and null-measurability when only an almost-everywhere representative is available.

The rigidity layer uses finite-prefix algebra to prove exact event invariance. An ergodic interface can then say that the event is trivial modulo null sets. Probability normalization is added only when the conclusion is written numerically as measure zero or one.

No layer secretly performs the job of another. Integrability does not make the raw representative ordinarily measurable. Ergodicity does not prove convergence. Probability normalization does not imply ergodicity. Exact invariance does not imply that the event is inhabited.

A notation runway

Reuse Mathlib’s finite Birkhoff API

RMT-22 does not define a second notion of time average. It imports Mathlib’s birkhoffSum and birkhoffAverage. At horizon \(n\), the sum is

The average is scalar multiplication by the inverse of the natural number cast into the scalar field. Over the reals this is

These definitions and their basic recurrences are in the pinned Mathlib source (finite Birkhoff sums, totalized averages).

Time zero is totalized, not excluded

Because the inverse of zero in a field is zero and the empty finite sum is zero,

This makes the API total on natural horizons. It does not assert a separate process normalization such as \(X_0=0\), and it does not change a sequence’s limit. The first boundary probe checks the exact equality rather than leaving it to convention.

At horizon one, the average is \(g(\omega)\). For a constant observable \(c\), the sequence is therefore zero at horizon zero and \(c\) at every positive horizon. It still converges to \(c\). This simple example foreshadows the main idea: a finite prefix can differ without affecting convergence.

Finite measurability is closure under finite operations

The declaration measurable_birkhoffSum assumes Measurable T and Measurable g. For each index \(j\), iterated measurability gives measurability of \(T^j\), composition gives measurability of \(g\circ T^j\), and Finset.measurable_sum closes the finite sum.

The next declaration, measurable_birkhoffAverage, rewrites the average as a constant real scalar times the measurable sum. It includes \(n=0\) without a separate branch.

Neither theorem mentions a measure. They are statements about the measurable structure on \(\Omega\) and ordinary measurability of finite functions.

Finite integrability needs preservation, not probability

The declaration integrable_birkhoffSum changes hypotheses. It assumes MeasurePreserving T μ μ and Integrable g μ. Every iterate of a measure-preserving map is measure preserving, so each composition \(g\circ T^j\) remains integrable. A finite sum of integrable functions is integrable.

Then integrable_birkhoffAverage closes under multiplication by the constant \(n^{-1}\). Time zero again needs no exception.

These proofs need no finite total mass and no probability normalization. They do not need ergodicity. They also prove no uniform estimate in \(n\), no maximal inequality, and no convergence. They say only that each separately fixed finite average has a legitimate Lebesgue integral.

Turn pointwise convergence into an event

The definition birkhoffConvergenceSet T g is

The limit is required to be a finite real number because \(c\) has type ℝ. Divergence to positive or negative infinity does not count. The definition has no measure argument and needs no measurable-space instance in its substance. It is just a predicate on points.

The simp theorem mem_birkhoffConvergenceSet_iff exposes that definition. Although its proof is reflexivity, the named theorem gives later proofs and users a stable public rewrite rule.

Most importantly, the existential quantifier defines a set without producing a witness for any point. Writing \(E(T,g)\) does not assert \(\omega\in E(T,g)\), \(E(T,g)\ne\varnothing\), or that \(E(T,g)\) is conull.

Ordinary measurability of the event

If \(T\) and \(g\) are ordinarily measurable, every function \(\omega\mapsto A_n g(\omega)\) is measurable. The upstream theorem MeasureTheory.measurableSet_exists_tendsto packages the descriptive set-theoretic fact that, for a measurable sequence with a suitable Polish target, the set where some limit exists is measurable. The real numbers meet that target requirement (measurable convergence events).

The declaration measurableSet_birkhoffConvergenceSet applies that theorem to the measurable finite averages. This is an event-measurability theorem, not a convergence theorem. It proves the set can be measured, not that its measure is large.

Why integrability alone takes the null-measurable route

In Mathlib, Integrable g μ supplies an almost-everywhere strongly measurable function. It need not certify ordinary measurability of the exact raw function \(g\) at every point. A null-set modification may be required.

That distinction matters because orbit averages inspect

Changing \(g\) on a null set is harmless only if the preimages of that null set under all iterates remain null. This is why the representative path asks for Measure.QuasiMeasurePreserving T μ μ. Ordinary measurability of \(T\) alone does not control how null exceptions pull back.

Fixed horizon is not all horizons

Mathlib provides QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq: if \(g=h\) almost everywhere, then for each fixed \(n\), their horizon-\(n\) averages agree almost everywhere (a.e. finite-average transport).

The convergence event depends on every horizon simultaneously. RMT-22’s birkhoffConvergenceSet_ae_eq_of_ae_eq therefore cannot select one fixed \(n\). It uses ae_all_iff to obtain one conull set on which

This is a countable intersection, so the null exceptions remain controlled. On that common set, the two sequences are termwise equal and hence converge to exactly the same finite limits. The result is event equality almost everywhere:

Skipping the countable all-horizon step would be a quantifier error. An exceptional null set that depends on \(n\) does not by itself give a single point where every equality holds.

Three ergonomic corollaries, one proof idea

For nullMeasurableSet_birkhoffConvergenceSet_of_aemeasurable, Lean chooses the measurable representative hg.mk g. That representative is ordinarily measurable and equals \(g\) almost everywhere (measurable representatives). Its convergence event is measurable. The event of the raw \(g\) agrees with it almost everywhere, so the raw event is null-measurable.

The theorem nullMeasurableSet_birkhoffConvergenceSet_of_aestronglyMeasurable forwards through hg.aemeasurable. The theorem nullMeasurableSet_birkhoffConvergenceSet_of_integrable forwards through hg.aestronglyMeasurable.

The three names preserve useful interfaces. Their mathematical payload is not three different convergence arguments. It is one representative argument exposed at the levels users naturally possess.

Delete one prefix without changing the limit

The algebraic heart of RMT-22 is independent of all measure theory. Compare the orbit beginning at \(\omega\) with the orbit beginning one step later:

The second row deletes one finite prefix term. The associated averages use different denominators, so the proof is not literally “the tails are equal.” It records the exact reweighting and then passes to the limit.

How to read the plate. The clay block is the one deleted observation. The blue and green blocks are the common orbit tail, relabeled because the sample size changes. The forward and backward arrows are both proved. This is a conceptual diagram, not a claim that either sequence converges. The result needs no boundedness of the orbit, no inverse for \(T\), and no measurable structure.

The forward identity

For every natural \(n\), the declaration birkhoffAverage_succ_apply_base proves

Start from the exact sum relation

Divide by \(n+1\), then rewrite \(S_{n+2}\) as \((n+2)A_{n+2}\). The use of \(n+1\) and \(n+2\) keeps every denominator positive, so the identity is valid for every natural \(n\) without a side-condition.

Suppose \(A_n g(\omega)\to c\). Then the shifted subsequence \(A_{n+2}g(\omega)\) also tends to \(c\), while

Limit arithmetic yields \(A_{n+1}g(T\omega)\to c\), and deleting its finite time-zero prefix yields \(A_n g(T\omega)\to c\). This is tendsto_birkhoffAverage_apply_base.

Notice what did not happen. The proof never bounded \(g(T^j\omega)\) as \(j\) varies. The only endpoint term is the fixed real number \(g(\omega)\) divided by a denominator tending to infinity.

The reverse identity

The declaration birkhoffAverage_succ_succ_apply solves the same finite equation in the other direction:

If the averages at \(T\omega\) tend to \(c\), then

so the shifted averages at \(\omega\) tend to \(c\). Restoring two finite initial terms does not change the limit. The declaration tendsto_birkhoffAverage_of_apply_base carries out exactly that argument.

This reverse direction does not apply an inverse map. It reconstructs the longer prefix at \(\omega\) by adding the single known value \(g(\omega)\) to the orbit prefix based at \(T\omega\). Consequently \(T\) may be noninjective or nonsurjective.

Same limit, not merely simultaneous existence

The theorem tendsto_birkhoffAverage_apply_base_iff packages the two directions for a specified real \(c\):

This is stronger than saying that both sequences converge or both diverge. When they converge, Lean records that the limits are identical.

Mathlib already has exact finite shift formulas and results showing a shifted average difference tends to zero under bounded-orbit or global boundedness hypotheses (bounded shift results). RMT-22 must therefore not claim that it invented a shift API. Its narrower addition is the direct boundedness-free equivalence of convergence to the same finite limit after adding or deleting one orbit prefix.

Exact event invariance

Unfold membership in the preimage:

Set extensionality turns the pointwise biconditional into preimage_birkhoffConvergenceSet:

The theorem explicitly omits the measurable-space instance. It assumes nothing about \(T\) or \(g\). Exact invariance is finite-sequence algebra, not a consequence of measure preservation, ergodicity, or invertibility.

Climb from exact invariance to conditional rigidity

An invariant event becomes rigid only after its measurability status and an ergodic hypothesis are supplied. RMT-22 deliberately keeps those inputs in separate theorem arguments. That separation makes it possible to see exactly where each assumption enters.

Logical ladder. The first two rungs establish that the event can be used in measure theory. The third is a pointwise equality needing no measure theory. The fourth uses the matching ergodic interface. The fifth additionally uses mass one. The crossed-out branch is essential: none of these steps establishes that even one point lies in the convergence event.

The ordinarily measurable path

The theorem birkhoffConvergenceSet_ae_empty_or_univ_of_measurableSet accepts two explicit inputs:

1. hT : PreErgodic T μ;
2. a proof that birkhoffConvergenceSet T g is measurable.

It supplies the exact preimage equality proved earlier to Mathlib’s PreErgodic.ae_empty_or_univ. The conclusion is

The pre-ergodic, quasi-ergodic, and probability event interfaces are upstream Mathlib declarations (ergodic event APIs). RMT-22’s work at this rung is to construct an event with exactly the regularity and invariance those declarations require.

The theorem does not require that measurability arose from an ordinarily measurable \(g\). A caller may have established event measurability by another route. This keeps the result modular.

The null-measurable path

The theorem birkhoffConvergenceSet_ae_empty_or_univ_of_nullMeasurableSet accepts QuasiErgodic T μ and null-measurability of the event. It uses QuasiErgodic.ae_empty_or_univ₀. The exact set equality is converted into the almost-everywhere pointwise invariance proposition that this interface requires.

This route matters for raw integrable representatives. Their events have been proved null-measurable, not necessarily ordinarily measurable. Requiring an ordinary measurable event here would discard the null-set stability supplied by the representative construction.

The declarations birkhoffConvergenceSet_ae_empty_or_univ_of_aemeasurable, birkhoffConvergenceSet_ae_empty_or_univ_of_aestronglyMeasurable, and birkhoffConvergenceSet_ae_empty_or_univ_of_integrable expose the null-measurable theorem at three common observable interfaces. The latter two forward through the same implication chain used earlier.

Null-or-conull is not zero-or-one until mass is one

For a general measure, saying an event is conull means its complement is null. Its measure need not be the real number one. It may be any finite total mass or even infinity. A numerical zero-one law therefore requires [IsProbabilityMeasure μ].

The theorem measure_birkhoffConvergenceSet_eq_zero_or_one_of_measurableSet uses PreErgodic.prob_eq_zero_or_one directly for a measurable event with exact invariance.

The theorem measure_birkhoffConvergenceSet_eq_zero_or_one_of_nullMeasurableSet first obtains the almost-everywhere empty-or-universal dichotomy. In the empty branch, almost-everywhere equality with the empty set gives measure zero. In the universal branch, measure congruence and probability normalization give measure one.

Finally, measure_birkhoffConvergenceSet_eq_zero_or_one_of_aemeasurable, measure_birkhoffConvergenceSet_eq_zero_or_one_of_aestronglyMeasurable, and measure_birkhoffConvergenceSet_eq_zero_or_one_of_integrable forward through the same representative ladder.

The result is a dichotomy:

It is not a proof of the second branch. A pointwise ergodic theorem would add an existence conclusion showing that, under its own hypotheses, the event is conull. RMT-22 contains no such step.

Why the zero measure is a valid boundary case

Under the zero measure, every set is null and every two functions are almost everywhere equal. The empty-or-universal disjunction is therefore true but places no pointwise constraint on the event. The seventh boundary probe keeps this case compiled.

This is not a defect in the theorem. Almost-everywhere statements intentionally forget behavior on null sets, and for the zero measure the entire space is null. The right lesson is to avoid translating a valid measure-theoretic statement into a stronger pointwise story.

Specialize without importing a theorem

The last ten declarations adapt the generic event to two project interfaces. They are intentionally thin. Their purpose is to make future theorem statements readable; they add no convergence field to an existing structure.

The one-step observable of a candidate process

For a real process \(X:\mathbb N\to\Omega\to\mathbb R\), the definition oneStepBirkhoffConvergenceSet T X is

The definition does not require shifted subadditivity, integrability, or any law for \(X\). It does not inspect \(X_0\). This is a naming layer for the one-step observable whose orbit averages will matter in later additive and subadditive arguments.

Inside the namespace IsIntegrableSubadditiveProcessCandidate, the theorem nullMeasurableSet_oneStepBirkhoffConvergenceSet obtains integrability from hX.integrable 1 and combines it with quasi-measure preservation. The shifted-subadditivity field is not used.

The exact invariance theorem preimage_oneStepBirkhoffConvergenceSet uses no candidate witness at all. It is the generic prefix theorem applied to \(X_1\).

The theorem oneStepBirkhoffConvergenceSet_ae_empty_or_univ combines one-step integrability with QuasiErgodic. Under a probability instance, measure_oneStepBirkhoffConvergenceSet_eq_zero_or_one gives the numeric dichotomy.

None of these declarations asserts that averages of \(X_1\) converge. None identifies their limit with the normalized process \(X_n/n\). Shifted subadditivity is present in the receiver package because that is the project’s common process interface, but it is not the missing Kingman theorem.

The log-positive matrix-cocycle observable

For a discrete matrix cocycle \(C\), the definition generatorLogPlusBirkhoffConvergenceSet C is

The name “generator” refers to the one-step log-positive norm observable. It does not say that a Lyapunov exponent exists. Because the observable is already proved ordinarily measurable and the cocycle stores a measure-preserving base, measurableSet_generatorLogPlusBirkhoffConvergenceSet needs no generator-integrability hypothesis and no nonempty matrix-index hypothesis.

The exact theorem preimage_generatorLogPlusBirkhoffConvergenceSet again uses only the generic prefix result. The rigidity theorem generatorLogPlusBirkhoffConvergenceSet_ae_empty_or_univ uses ordinary event measurability and PreErgodic C.base μ. With a probability instance, measure_generatorLogPlusBirkhoffConvergenceSet_eq_zero_or_one gives the numerical alternative.

The observable is log-positive. It clips all contraction to zero. Even a future convergence theorem for its Birkhoff averages would not by itself produce a signed Lyapunov exponent, singular-value spectrum, or Oseledets splitting.

The complete source-order tour

The frozen 602-line module has thirty-seven public declarations. The following map preserves exact source order. The twelve anonymous examples that follow them are mapped in the next section.

Items 1-4: finite measurability and integrability

1. measurable_birkhoffSum proves measurability of each finite real Birkhoff sum from measurable dynamics and observable.
2. measurable_birkhoffAverage multiplies the sum by the totalized inverse horizon and includes time zero.
3. integrable_birkhoffSum transports one-step integrability through every preserved iterate and closes a finite sum.
4. integrable_birkhoffAverage closes the finite sum under constant scalar multiplication, again including time zero.

Items 5-11: the event and representative independence

5. birkhoffConvergenceSet defines the points where the real average sequence tends to some finite real limit.
6. mem_birkhoffConvergenceSet_iff is the public membership rewrite.
7. measurableSet_birkhoffConvergenceSet proves event measurability for ordinarily measurable dynamics and observable.
8. birkhoffConvergenceSet_ae_eq_of_ae_eq takes the countable all-horizon intersection and proves almost-everywhere event equality for almost-everywhere equal observables under quasi-measure preservation.
9. nullMeasurableSet_birkhoffConvergenceSet_of_aemeasurable replaces an a.e. measurable observable by its measurable representative.
10. nullMeasurableSet_birkhoffConvergenceSet_of_aestronglyMeasurable forwards from a.e. strong measurability.
11. nullMeasurableSet_birkhoffConvergenceSet_of_integrable forwards from integrability through a.e. strong measurability.

Items 12-17: finite-prefix shift equivalence

12. birkhoffAverage_succ_apply_base expresses the shifted-base average through the next original-base average and one vanishing endpoint term.
13. tendsto_birkhoffAverage_apply_base transports convergence and its exact finite limit from \(\omega\) to \(T\omega\).
14. birkhoffAverage_succ_succ_apply solves the finite identity in the reverse direction.
15. tendsto_birkhoffAverage_of_apply_base transports convergence and the same limit from \(T\omega\) back to \(\omega\).
16. tendsto_birkhoffAverage_apply_base_iff packages both directions for a specified limit.
17. preimage_birkhoffConvergenceSet proves exact preimage invariance with no structural assumption on \(T\) or \(g\).

Items 18-27: ergodic rigidity and probability zero-one laws

18. birkhoffConvergenceSet_ae_empty_or_univ_of_measurableSet uses a measurable event and PreErgodic to obtain the a.e. dichotomy.
19. birkhoffConvergenceSet_ae_empty_or_univ_of_nullMeasurableSet uses a null-measurable event and QuasiErgodic.
20. birkhoffConvergenceSet_ae_empty_or_univ_of_aemeasurable supplies null-measurability from an a.e. measurable observable.
21. birkhoffConvergenceSet_ae_empty_or_univ_of_aestronglyMeasurable exposes the same result for a.e. strongly measurable input.
22. birkhoffConvergenceSet_ae_empty_or_univ_of_integrable exposes it for an integrable observable.
23. measure_birkhoffConvergenceSet_eq_zero_or_one_of_measurableSet adds probability normalization to the measurable/pre-ergodic route.
24. measure_birkhoffConvergenceSet_eq_zero_or_one_of_nullMeasurableSet converts the null-measurable a.e. dichotomy to numeric measure alternatives.
25. measure_birkhoffConvergenceSet_eq_zero_or_one_of_aemeasurable specializes the probability result to an a.e. measurable observable.
26. measure_birkhoffConvergenceSet_eq_zero_or_one_of_aestronglyMeasurable specializes it to an a.e. strongly measurable observable.
27. measure_birkhoffConvergenceSet_eq_zero_or_one_of_integrable specializes it to an integrable observable.

Items 28-32: the one-step process event

28. oneStepBirkhoffConvergenceSet names \(E(T,X_1)\) and leaves \(X_0\) irrelevant.
29. IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_oneStepBirkhoffConvergenceSet uses the candidate’s integrability field only at horizon one.
30. IsIntegrableSubadditiveProcessCandidate.preimage_oneStepBirkhoffConvergenceSet is the unconditional exact preimage equality.
31. IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffConvergenceSet_ae_empty_or_univ combines one-step integrability with quasi-ergodicity.
32. IsIntegrableSubadditiveProcessCandidate.measure_oneStepBirkhoffConvergenceSet_eq_zero_or_one adds probability normalization.

Items 33-37: the discrete matrix-cocycle event

33. DiscreteMatrixCocycle.generatorLogPlusBirkhoffConvergenceSet names the event for the one-step log-positive norm observable.
34. DiscreteMatrixCocycle.measurableSet_generatorLogPlusBirkhoffConvergenceSet proves ordinary event measurability from the cocycle’s existing measurable interfaces.
35. DiscreteMatrixCocycle.preimage_generatorLogPlusBirkhoffConvergenceSet proves exact invariance without integrability or nonempty index assumptions.
36. DiscreteMatrixCocycle.generatorLogPlusBirkhoffConvergenceSet_ae_empty_or_univ combines ordinary measurability, exact invariance, and pre-ergodicity.
37. DiscreteMatrixCocycle.measure_generatorLogPlusBirkhoffConvergenceSet_eq_zero_or_one adds probability normalization, still without proving convergence.

Twelve probes audit the quantifiers

The source ends with twelve anonymous example blocks. They compile as theorem-sized tests while adding no public names.

Probe 1: totalization at time zero

For every \(T\), \(g\), and \(\omega\), the average at horizon zero is exactly zero. The probe calls Mathlib’s birkhoffAverage_zero. It does not refer to \(X_0\) of a separate process.

Probe 2: the zero observable converges everywhere

Every finite average of the zero observable is zero, so its convergence event is the universal set for every map \(T\). No measurable structure is used.

Probe 3: every constant observable converges everywhere

For a constant \(c\), the positive-horizon average is \(c\). The exceptional time-zero value is one finite prefix, so the sequence tends to \(c\). The probe uses Mathlib’s fixed-composition average theorem after horizon one.

Probe 4: identity dynamics converges for every observable

Under id, the orbit never leaves \(\omega\), so every positive-horizon average is \(g(\omega)\). Therefore the event is universal for an arbitrary function \(g\), even without measurability.

Identity dynamics is not generally ergodic. On a space with nontrivial measurable sets of intermediate measure, every measurable set is invariant. This probe separates convergence from ergodicity.

Probe 5: a noninjective map still has exact event invariance

The constant map from Bool to false is not injective. Nevertheless the generic preimage theorem applies to every observable. This directly tests that the reverse convergence implication did not use an inverse.

Probe 6: replace an a.e. measurable representative

For hg : AEMeasurable g μ, the raw event agrees almost everywhere with the event of hg.mk g under quasi-measure-preserving dynamics. This is the representative theorem in its most concrete form.

Probe 7: zero-measure rigidity is valid and vacuous

For the zero measure and a measurable \(T\), every observable is a.e. measurable. The convergence event is a.e. empty or a.e. universal. Since both descriptions can hold under the zero measure, the result carries no pointwise membership information.

Probe 8: \(X_0\) does not enter the one-step event

The probe defines \(X_n=1\) when \(n=0\) and \(X_n=0\) otherwise, over the zero measure and identity map. It packages this as an integrable subadditive-process candidate, records \(X_0(\omega_0)\ne0\), and still proves that the one-step event is universal because \(X_1\) is zero.

This prevents a common category mistake: Mathlib’s totalized \(A_0=0\) and the project’s process value \(X_0\) are unrelated definitions.

Probe 9: empty matrix dimension remains legal

For a cocycle indexed by Empty, the generator event is measurable and exactly invariant. No nonempty-index assumption was inserted merely to state or measure the event.

Probe 10: a supplied divergence proof gives nonmembership

If every finite \(c\) fails to be a limit of the average sequence at \(\omega\), then \(\omega\) is not in the convergence event. This is the definition read negatively, with no hidden compactness or extended-real limit.

Probe 11: compute an unbounded arithmetic orbit

Take \(\Omega=\mathbb N\), \(T(k)=k+1\), \(g(k)=k\), and start at zero. The accompanying formal proof establishes

The finite sum is \(0+1+\cdots+n=n(n+1)/2\), divided by \(n+1\).

Probe 12: the arithmetic orbit diverges

The final anonymous declaration establishes

It assumes a finite limit \(c\), shifts past time zero, rewrites the sequence as \(n/2\), and combines convergence to \(c\) with divergence to positive infinity to obtain a contradiction.

This probe is an explicit witness that the generic event need not be universal. It also explains why exact invariance cannot possibly be an existence theorem.

How Lean executes the proof

The mathematical spine is short, but several Lean moves carry important logical information. Seeing those moves makes the source easier to reuse.

Iterate measurability rather than expanding recursion

hT.iterate j gives measurability of \(T^j\) directly. The finite sum proof can then be written as a closure argument over Finset.range n instead of manually unfolding iteration at every horizon.

Transport integrability through preserved iterates

(hT.iterate j).integrable_comp_of_integrable hg is the finite analytic engine. It makes the direction of composition explicit: \(g\circ T^j\), with both source and target measure equal to \(\mu\). integrable_finsetSum then closes the finite family.

Use one conull set for the whole sequence

The representative proof first establishes a proposition of the form

∀ᵐ ω ∂μ, ∀ n : ℕ,
  birkhoffAverage ℝ T g n ω = birkhoffAverage ℝ T h n ω

The order of quantifiers matters. Lean’s ae_all_iff moves from an a.e. equality for each natural \(n\) to one a.e. statement containing every \(n\). Only then can Tendsto.congr’ compare the whole sequences.

Shift only after proving a positive-index identity

Both recurrence theorems use \(n+1\) and \(n+2\), so denominators are nonzero. The limit proofs then use tendsto_add_atTop_iff_nat to add or delete the finite prefix. This keeps division arithmetic separate from the topological fact that a finite sequence prefix does not affect a limit.

Let field arithmetic certify the exact equations

After rewriting with birkhoffSum_succ’, positivity discharges the denominator obligations. field_simp and ring normalization close the rational identity. The theorem is exact before any asymptotic reasoning enters.

Compose elementary limits

The forward theorem combines a ratio tending to one, a shifted average tending to \(c\), and a fixed numerator divided by a growing natural tending to zero. The reverse theorem uses the analogous ratio. Lean’s Tendsto.mul, Tendsto.add, and Tendsto.sub mirror the calculation.

Keep event equality pointwise until the last line

For exact preimage invariance, Set.ext reduces set equality to one point. The membership simp theorem exposes the existential limit, and the two transport theorems solve the directions. No measure-theory automation is needed because the statement is not measure theoretic.

Match regularity to the ergodic API

The measurable path calls PreErgodic.ae_empty_or_univ. The null-measurable path calls QuasiErgodic.ae_empty_or_univ₀. Keeping both theorem families avoids coercing a null-measurable raw event into a false ordinary-measurability claim.

Common wrong turns

Calling the event a convergence theorem

A set comprehension is not a proof of membership. The event can be defined, measured, and shown invariant even when it is empty.

Reading zero-one as one

The disjunction \(\mu(E)=0\lor\mu(E)=1\) does not select its right branch. An existence theorem is needed to rule out zero.

Claiming Mathlib lacked shift lemmas

Mathlib already supplies exact finite shift identities and bounded shift-difference convergence results. The contribution here is the precise boundedness-free convergence equivalence needed for event invariance.

Using only one fixed-horizon a.e. equality

Convergence is a property of the entire sequence. A proof for one \(n\), or a family of a.e. proofs with no countable intersection, is insufficient.

Treating integrability as ordinary measurability

Integrability supplies a.e. strong measurability. RMT-22 uses a measurable representative and concludes null-measurability of the raw event.

Forgetting quasi-measure preservation

An a.e. modification of \(g\) can be encountered after iterating \(T\). Null exceptions must stay null under the relevant preimages. Arbitrary measurable dynamics do not promise that.

Assuming the backward implication needs an inverse

It does not solve \(T\omega'=\omega\). It adds back the one known prefix value \(g(\omega)\). Noninjective maps are explicitly tested.

Assuming boundedness of the observable

The correction term uses one fixed value \(g(\omega)\), not a supremum over the orbit. The divergent arithmetic example has an unbounded observable and still fits the exact identities.

Confusing \(A_0\) with \(X_0\)

The average’s time-zero value is determined by Mathlib’s totalized scalar inverse. A separate process may have any \(X_0\) allowed by its own interface.

Treating identity convergence as ergodicity

Identity dynamics gives constant positive-horizon averages at each point, but it leaves every set invariant. Universal convergence and ergodicity are different properties.

Treating the zero measure as pointwise evidence

Every exceptional set is null under the zero measure. A valid a.e. theorem can be entirely vacuous pointwise.

Calling Mathlib’s martingale inequality Hopf’s theorem

Mathlib’s declaration named maximal_ineq in the optional-stopping development is Doob’s martingale inequality, not Hopf’s maximal ergodic inequality (Doob boundary). A matching name fragment is not a matching theorem.

Calling mean convergence pointwise convergence

Mathlib’s Hilbert-space mean ergodic development concerns convergence in the Hilbert-space sense, not almost-everywhere convergence of real orbit averages (mean-ergodic boundary). It cannot fill the pointwise gap by renaming the topology.

Calling the cocycle wrapper a Lyapunov theorem

The wrapper concerns averages of a log-positive one-step norm observable. It does not identify normalized product growth, retain negative logarithmic growth, or construct invariant subspaces.

What this event does not prove

RMT-22 proves a reusable conditional bridge. Its boundary is part of its result. It proves neither

nor

It proves no convergence-existence theorem, no Hopf maximal inequality, and no maximal estimate of any kind. It proves no pointwise Birkhoff theorem. It proves no statement identifying a limit with a conditional expectation or an invariant function. It proves no integral of a limit and no interchange between a limit and an integral.

It proves no Kingman subadditive ergodic theorem. Kingman’s 1968 paper develops ergodic theory for subadditive stochastic processes and presents it as a generalization of stationary laws of large numbers (Kingman, 1968). RMT-22 studies additive Birkhoff averages of a one-step observable only to isolate their convergence event. It does not connect that event to \(X_n/n\), the centered process, or the marked sets in RMT-20 and RMT-21.

It proves no frequency or density theorem for favorable orbit positions. It does not show that the interval-packing marked set has positive lower density. It proves no Lyapunov exponent, no signed log-growth limit, no singular-value rate, no exterior-power theorem, and no Oseledets splitting.

The event’s exact invariance is still useful. It completes a theorem-ready interface: once a future pointwise convergence theorem supplies membership, the present rigidity lemmas can immediately turn invariance into an ergodic conclusion without rebuilding finite-prefix algebra.

Exercises with solutions

Exercise 1: expand the first three horizons

Write \(A_0g(\omega)\), \(A_1g(\omega)\), and \(A_2g(\omega)\).

Solution. They are \(0\), \(g(\omega)\), and \(\bigl(g(\omega)+g(T\omega)\bigr)/2\). The zero value is totalization; the other two follow from Finset.range indexing.

Exercise 2: separate the finite hypotheses

Which hypotheses prove measurability of \(A_n\), and which prove integrability?

Solution. Measurability uses ordinary measurability of \(T\) and \(g\). Integrability uses measure preservation of \(T\) and integrability of \(g\). Neither uses probability or ergodicity.

Exercise 3: reject a hidden probability assumption

Why is finite-horizon integrability valid on an infinite measure space?

Solution. A finite sum of integrable functions remains integrable, and measure preservation carries integrability through each iterate. Total mass does not enter that closure argument.

Exercise 4: read the existential literally

What does \(\omega\in E(T,g)\) provide?

Solution. It provides a finite real \(c\) and a proof that \(A_n g(\omega)\to c\). The definition by itself provides neither a member \(\omega\) nor a limit for an unspecified point.

Exercise 5: distinguish finite and extended limits

Does divergence of \(A_n g(\omega)\) to positive infinity put \(\omega\) in the event?

Solution. No. The witness \(c\) has type ℝ, so only a finite real limit qualifies.

Exercise 6: find the countability step

Why is the upstream fixed-\(n\) a.e. equality insufficient?

Solution. Convergence uses every term. The exceptional set may depend on \(n\). Because the horizons are natural numbers, ae_all_iff intersects countably many conull sets and produces one set where all terms agree.

Exercise 7: identify the representative

What is the role of hg.mk g?

Solution. It is an ordinarily measurable function equal to \(g\) almost everywhere. Its convergence event is measurable; representative independence then proves the raw event is equal to that measurable set modulo null sets.

Exercise 8: explain quasi-measure preservation

Why does representative independence mention the dynamics?

Solution. Orbit averages evaluate \(g\) after iterates of \(T\). A null set where two representatives differ must have null preimages under those iterates. Quasi-measure preservation supplies that control.

Exercise 9: derive the forward identity

Starting from \(S_{n+1}g(T\omega)=S_{n+2}g(\omega)-g(\omega)\), derive the formula for \(A_{n+1}g(T\omega)\).

Solution. Divide by \(n+1\) and replace \(S_{n+2}=(n+2)A_{n+2}\). The result is \((n+2)A_{n+2}/(n+1)-g(\omega)/(n+1)\).

Exercise 10: derive the reverse identity

Solve the same equation for \(A_{n+2}g(\omega)\).

Solution. Add \(g(\omega)\), divide by \(n+2\), and replace \(S_{n+1}g(T\omega)=(n+1)A_{n+1}g(T\omega)\).

Exercise 11: locate boundedness

Where does the prefix-shift proof assume a bound on \(g(T^j\omega)\)?

Solution. Nowhere. The only deleted term is the fixed real number \(g(\omega)\), divided by a denominator tending to infinity.

Exercise 12: avoid an inverse

How does the reverse theorem recover convergence at \(\omega\) without inverting \(T\)?

Solution. It reconstructs each sufficiently long original prefix from the shifted prefix plus \(g(\omega)\). It never searches for a preimage point.

Exercise 13: preserve the exact limit

What does the iff theorem preserve beyond convergence existence?

Solution. It preserves the exact finite limit \(c\). The two sequences cannot converge to different real numbers.

Exercise 14: prove the event equality pointwise

What is the key equivalence for a fixed \(\omega\)?

Solution. \(T\omega\in E(T,g)\) iff \(\omega\in E(T,g)\), obtained by moving the existential limit witness through the two transport lemmas.

Exercise 15: distinguish the two ergodic routes

When should a caller use the measurable-set theorem rather than the null-measurable-set theorem?

Solution. Use the measurable route when ordinary event measurability is available and a PreErgodic witness matches it. Use the null-measurable route for an event known only modulo null sets, with a QuasiErgodic witness.

Exercise 16: interpret conull outside probability

If \(E\) is conull, must \(\mu(E)=1\)?

Solution. No. It has the same measure as the whole space when measurable enough, and that total mass need not be one. The numeric zero-one theorem adds IsProbabilityMeasure.

Exercise 17: refuse to choose a disjunct

Why does \(\mu(E)=0\lor\mu(E)=1\) not prove convergence almost everywhere?

Solution. Almost-everywhere convergence corresponds to the measure-one branch. The theorem leaves the measure-zero branch possible.

Exercise 18: test identity dynamics

Why does every observable converge along identity dynamics?

Solution. For positive horizons the orbit average is constantly \(g(\omega)\). This pointwise fact does not make identity dynamics ergodic.

Exercise 19: test the constant map

What does the Boolean constant-map probe rule out?

Solution. It rules out any hidden injectivity or invertibility premise in exact event invariance.

Exercise 20: separate \(A_0\) and \(X_0\)

Can the one-step event be universal when \(X_0(\omega_0)\ne0\)?

Solution. Yes. The event averages \(X_1\) along the orbit. The compiled probe sets \(X_1=0\) while retaining a nonzero time-zero process value.

Exercise 21: audit candidate fields

Which candidate fact makes the one-step event null-measurable?

Solution. hX.integrable 1, together with quasi-measure preservation. Shifted subadditivity is not used for that theorem.

Exercise 22: audit cocycle dimension

Why does the empty-index cocycle still have a measurable invariant event?

Solution. The existing log-positive observable is ordinarily measurable for every finite index type, including Empty. Event definition and prefix invariance require no nonempty dimension.

Exercise 23: compute the arithmetic example

Why is the average of \(0,1,\ldots,n\) equal to \(n/2\)?

Solution. The sum is \(n(n+1)/2\), and the prefix contains \(n+1\) terms. Division cancels the factor \(n+1\).

Exercise 24: place the missing theorem

What additional conclusion would a pointwise Birkhoff theorem contribute to this module’s ladder?

Solution. Under its own assumptions it would show that the convergence event is conull, selecting the universal branch of the conditional rigidity dichotomy. It would also normally identify the limit more precisely. RMT-22 does neither.

Reproducibility and audit ledger

From the repository root:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomCocycles/BirkhoffConvergence.lean
lake build NonlinearDynamics.Random.RandomCocycles.BirkhoffConvergence
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomCocycles.lean
lake env lean -DwarningAsError=true NonlinearDynamics/Random.lean
lake env lean -DwarningAsError=true NonlinearDynamics.lean
cd ..
python3 scripts/check_teaching_source_hygiene.py
make site-check

The public-surface audit should include:

import NonlinearDynamics

open MeasureTheory Set Filter
open NonlinearDynamics.Random.RandomCocycles

#check measurable_birkhoffAverage
#check birkhoffConvergenceSet
#check birkhoffConvergenceSet_ae_eq_of_ae_eq
#check nullMeasurableSet_birkhoffConvergenceSet_of_integrable
#check tendsto_birkhoffAverage_apply_base_iff
#check preimage_birkhoffConvergenceSet
#check birkhoffConvergenceSet_ae_empty_or_univ_of_integrable
#check measure_birkhoffConvergenceSet_eq_zero_or_one_of_integrable
#check IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffConvergenceSet_ae_empty_or_univ
#check DiscreteMatrixCocycle.generatorLogPlusBirkhoffConvergenceSet_ae_empty_or_univ

The integrated source is 602 lines with SHA-256 cec39333cd0751ca7b52283049cf11ec8a8a8870eff3dbeaf32bfda81d111fbd. That hash records the exact source audited for this chapter. The repository module remains the authority. The six source-level #print axioms commands audit representative-independence, measurable-representative, finite-prefix, generic rigidity, candidate rigidity, and cocycle rigidity theorems.

This article publishes as an open working note with draft: false and retains pro_reviewed: false. Automated checks do not replace human mathematical, source, accessibility, and editorial review.

The next ridge

RMT-22 has made the convergence event measurable enough to use and exactly invariant enough to be ergodically rigid. It also includes a formal arithmetic-orbit proof that a point can lie outside the event. The gap is now sharper than “we need ergodic theory.” We need a theorem that proves membership under explicit hypotheses.

A natural next analytic slice is a finite Hopf-style maximal inequality with all sign, truncation, measurability, integrability, and finite-measure assumptions explicit. Such an inequality is a standard route toward a pointwise Birkhoff development. It must be formalized rather than confused with Mathlib’s Doob martingale inequality or Hilbert-space mean ergodic convergence.

That finite slice is developed next in Peel the Positive Maximum: A Finite Hopf Lemma in Lean. It proves a strict finite maximal-event integral inequality and finite average-threshold consequences. It still does not prove an infinite-horizon maximal theorem or pointwise convergence.

Only after a pointwise Birkhoff theorem is available can this branch justify the frequency of measurable favorable sets along typical orbits. That density input is what the finite phase-averaging and interval-packing mechanisms from RMT-20 and RMT-21 still lack. A later Kingman proof must additionally connect one-step additive averages, centered subadditive processes, finite packing bounds, normalized sample limits, integrated Fekete rates, and any invariant limit identification.

For matrix cocycles, further observable work remains. The present log-positive scalar sees expansion but clips contraction. Signed logarithms, zero products, negative-tail integrability, singular values, exterior powers, and invariant splittings require separate definitions and theorems before Lyapunov or Oseledets language becomes warranted.

References

The links below were checked on 2026-07-21. The pinned Mathlib 4.32.0 checkout at commit 81a5d257c8e410db227a6665ed08f64fea08e997 is the exact authority for upstream theorem names used by the frozen proof.

Mathlib contributors. Finite Birkhoff sums and recurrences, Mathlib 4.32.0. These lines define birkhoffSum and provide the finite successor relations reused by RMT-22. The exact shifted-sum difference is existing upstream algebra.

Mathlib contributors. Totalized Birkhoff averages, Mathlib 4.32.0. These definitions and simp lemmas record the horizon-zero and horizon-one behavior. The exact finite shifted-average difference is also upstream.

Mathlib contributors. Birkhoff averages under quasi-measure-preserving maps, Mathlib 4.32.0. The relevant theorem transports almost-everywhere equality of observables to almost-everywhere equality of averages for one fixed horizon. RMT-22 adds the countable all-horizon step before comparing convergence events.

Mathlib contributors. Measurability of sequence convergence events, Mathlib 4.32.0. RMT-22 applies this general Polish-space infrastructure to the sequence of real finite Birkhoff averages.

Mathlib contributors. Measurable representatives of almost-everywhere measurable functions, Mathlib 4.32.0. These declarations provide AEMeasurable.mk, measurable_mk, and ae_eq_mk for the ordinary measurable representative used by the proof.

Mathlib contributors. Pre-ergodic and quasi-ergodic event rigidity, with the null-or-conull and probability interfaces, Mathlib 4.32.0. RMT-22 supplies these APIs with an exact invariant convergence event; it does not obtain convergence from them.

Mathlib contributors. Bounded-orbit and globally bounded shifted-average convergence, Mathlib 4.32.0. These existing declarations are the novelty boundary for RMT-22’s boundedness-free finite-prefix convergence equivalence.

Mathlib contributors. Doob maximal inequality in the optional-stopping development, Mathlib 4.32.0. This is a martingale theorem, not Hopf’s maximal ergodic inequality.

Mathlib contributors. Hilbert-space mean ergodic theorem scope, Mathlib 4.32.0. The file describes mean convergence in a Hilbert-space setting, not pointwise almost-everywhere convergence of real Birkhoff averages.

George D. Birkhoff. Proof of the Ergodic Theorem, Proceedings of the National Academy of Sciences 17(12), 656-660, 1931, with the open archival copy. The paper proves almost-everywhere existence of trajectory time fractions in its invariant-volume dynamical setting and contrasts trajectorywise convergence with convergence in mean. It is historical primary evidence, not the literal statement of a modern arbitrary-measure-space Lean theorem.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499-510, 1968. The paper develops ergodic theory for subadditive stochastic processes and presents it as a generalization of stationary laws of large numbers. It is the historical asymptotic destination, not a theorem proved or imported by RMT-22.

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