The Missing Step Closes: Pointwise Birkhoff by Maximal Control in Lean

Milestone status. RMT-26 is implementation-complete in the linked Lean module. This prose and its figures are published as an open working note. The theorem closes the maximal-to-pointwise convergence step, but limit identification remains a separate ridge.

For a slower textbook ascent, read Pointwise Birkhoff from Maximal Control and Dense Good Functions. The compact reusable definitions are the Birkhoff Cauchy exceptional set and the weak type (1,1) maximal bound . They build on the existing Birkhoff sum , Birkhoff convergence event , and infinite-horizon average-exceedance event entries.

The question RMT-25 could not answer

The previous milestone deliberately separated two statements.

1. Every real \(L^2\) observable has Koopman averages converging in \(L^2\) norm to the fixed-space projection.
2. A dense \(L^2\) class, consisting of fixed vectors plus simple coboundaries, has full-sequence almost-everywhere convergent pointwise averages.

Neither statement implies that the full average sequence converges pointwise for every \(L^2\) vector, much less every \(L^1\) observable. Norm convergence can supply an almost-everywhere convergent subsequence, but the omitted indices can still oscillate. Density alone also fails: two \(L^1\)-near functions can be pointwise far apart on a small set, and orbit averages can revisit that set.

The required bridge must answer a stability question:

If \(g\) has convergent averages and \(f-g\) is small in \(L^1\), how large can the set be on which the averages of \(f\) still fail the Cauchy test?

The RMT-24 maximal estimate answers exactly this question. The rest of RMT-26 is the architecture needed to ask it in a countable, representative-safe form.

Prior work, contribution, and non-claims

Prior work. Birkhoff’s 1931 paper established an individual ergodic theorem for invariant flows, using its own limsup and liminf argument. The transformation maximal theorem appeared explicitly in Yosida and Kakutani’s 1939 paper. Yosida’s 1940 paper then used a closure lemma traced to Banach’s 1926 almost-everywhere convergence principle. Hopf later generalized the maximal framework to positive contraction and Markov operators. RMT-26 follows this broad Banach-principle strategy, with the repository’s weak maximal bound providing quantitative continuity in measure. It is not a line-by-line formalization of any one historical proof.

This note’s contribution. The checked module:

• turns absolute Birkhoff-average exceedance into a named event with a weak maximal estimate;
• defines a representative-stable fixed-scale Cauchy exceptional event;
• proves a sharp-enough three-term containment using the error at each endpoint and the approximant’s own Cauchy tail;
• derives null exceptional sets from arbitrarily close pointwise-good approximants;
• packages finite-measure \(L^2\to L^1\) inclusion as a continuous linear map with its norm coefficient and dense range;
• transfers the RMT-25 core into \(L^1\); and
• concludes full-sequence almost-everywhere convergence for every real integrable observable.

Not claimed. RMT-26 does not prove:

• that the limit equals conditional expectation onto an invariant sigma algebra;
• that ergodicity makes the limit constant or equal to the space average;
• strong \(L^1\) boundedness of the maximal function;
• \(L^1\)-norm convergence of the averages;
• the infinite-measure version of the theorem;
• a canonical pointwise representative for an \(L^1\) equivalence class;
• Kingman’s subadditive theorem, Lyapunov exponents, or Oseledets splittings.

One orbit, three errors

Suppose \(g\) has a Cauchy tail at a point \(\omega\). For large \(m,n\), insert and subtract the two approximating averages:

There are three terms, which explains the threshold \(\varepsilon/3\). The middle term is eventually strictly below \(\varepsilon/3\) because \(g\)’s averages are Cauchy. If neither endpoint error exceeds \(\varepsilon/3\), then the two weak endpoint inequalities plus the strict middle inequality make the total strictly below \(\varepsilon\). That contradicts membership in the non-strict failure event.

Two small design choices matter.

First, maximal events use only positive horizons. The Cauchy failure supplies witnesses beyond every requested lower bound, so the proof takes witnesses past \(\max(N,1)\). Horizon zero never enters the maximal event. Second, the failure event uses \(\varepsilon\le |A_mf-A_nf|\), not a strict inequality. Its complement therefore gives the strict estimate demanded by Metric.cauchySeq_iff without a later boundary repair.

Absolute maximal control

The elementary inequality behind the absolute event is

The source declaration abs_birkhoffAverage_le_birkhoffAverage_abs proves it directly from the finite-sum triangle inequality. Lean’s natural-number inverse is totalized, so the horizon-zero case is also true: both sides are zero.

birkhoffAverageAbsoluteExceedanceSet names the event

mem_birkhoffAverageAbsoluteExceedanceSet_iff exposes the exact membership interface. birkhoffAverageAbsoluteExceedanceSet_subset sends \(M_a(h)\) into the existing one-sided exceedance event for \(|h|\). The RMT-24 theorem then immediately yields measureReal_birkhoffAverageAbsoluteExceedanceSet_le:

Here \(\mu_{\mathbb R}\) is Mathlib’s real-valued projection of an extended measure. Finite total mass is explicit because that projection sends infinity to zero. This is weak type \((1,1)\): it controls the measure of level sets. It does not state that the supremum function itself is integrable.

The Cauchy exceptional event

The module defines birkhoffCauchyExceptionalSet T f ε by

This is a tail event for one fixed numerical scale. It does not say that the sequence fails to converge in every possible way. It says that arbitrarily late pairs remain at least \(\varepsilon\) apart.

mem_birkhoffCauchyExceptionalSet_iff is intentionally a reflexive API theorem. It makes rewriting and source coverage explicit even though the proof is rfl.

measurableSet_birkhoffCauchyExceptionalSet expands the event as a countable intersection over tail cutoffs and countable unions over the two witness horizons. Each innermost set is measurable because finite Birkhoff averages of a measurable observable are measurable.

An \(L^1\) vector is an equivalence class, but this event is defined from a chosen ordinary function. birkhoffCauchyExceptionalSet_ae_eq_of_ae_eq proves that quasi-measure-preserving dynamics transport the event across almost-everywhere equal representatives. The proof first transports every finite average and then uses ae_all_iff to take the countable intersection over horizons. This representative theorem feeds nullMeasurableSet_birkhoffCauchyExceptionalSet_of_aemeasurable, which chooses a measurable representative, and nullMeasurableSet_birkhoffCauchyExceptionalSet_of_integrable, which obtains almost-everywhere measurability from integrability.

These null-measurability declarations are not ornamental. They prevent the formal proof from silently assuming that a chosen \(L^1\) representative is everywhere measurable.

The maximal-closure engine

birkhoffCauchyExceptionalSet_subset_exceedance_union_compl formalizes the three-error argument. For \(\varepsilon\gt0\), it proves

where \(\operatorname{Conv}(g)\) is the existing birkhoffConvergenceSet T g. The proof assumes no measurable space because it is pure pointwise metric algebra.

measureReal_birkhoffCauchyExceptionalSet_le adds finite measure, measure preservation, integrability of the error \(f-g\), and almost-everywhere convergence of \(g\). The complement of \(g\)’s good event has real measure zero. Subadditivity for the union and the absolute maximal estimate give

The abstract approximation hypothesis used by measure_birkhoffCauchyExceptionalSet_eq_zero_of_dense_good says that for every \(\delta\gt0\), there is an ordinary function \(g\) such that:

1. \(f-g\) is integrable;
2. \(\int|f-g|\,d\mu\lt\delta\); and
3. the Birkhoff averages of \(g\) converge almost everywhere.

To prove that \(D_\varepsilon(f)\) is null, the Lean proof does not take an informal limit. It fixes an arbitrary \(\eta\gt0\), chooses \(\delta=\eta(\varepsilon/3)\), derives \(\mu_{\mathbb R}(D_\varepsilon(f))\le\eta\), and invokes the ordered-real lemma that a nonnegative number below every positive tolerance is zero. Finite mass then converts real measure zero back to extended measure zero.

cauchySeq_birkhoffAverage_of_not_mem_exceptional is the pointwise countable bridge. Given a target tolerance \(r\gt0\), Mathlib’s exists_nat_one_div_lt supplies \(k\) with \(1/(k+1)\lt r\). Nonmembership in \(D_{1/(k+1)}(f)\) supplies one tail on which every pair is closer than that reciprocal threshold, hence closer than \(r\).

Finally, ae_mem_birkhoffConvergenceSet_of_dense_good intersects the conull complements of all reciprocal exceptional sets. At every surviving point the averages form a real Cauchy sequence. cauchySeq_tendsto_of_complete produces a real limit, and mem_birkhoffConvergenceSet_iff packages it as convergence event membership.

This abstract theorem does not require Integrable f. It consumes only arbitrarily close approximants whose errors are integrable. The final specialization adds integrability to manufacture precisely those approximants.

Why finite measure turns L² into an L¹ dense source

The dense good class from RMT-25 lives in \(L^2\), while the target theorem is about \(L^1\). On a finite measure space, Hölder’s inequality gives

RMT-26 packages this inclusion instead of hiding it inside the last proof.

l2ToL1Linear constructs the underlying linear map from Mathlib’s exponent monotonicity theorem. l2ToL1Linear_apply_ae records that the same almost-everywhere function is used on both sides.

norm_l2ToL1Linear_apply_le proves the quantitative norm inequality. The proof works first in extended nonnegative real seminorms, establishes that the right side is not infinity, and only then applies ENNReal.toReal_mono. Skipping that finiteness check would be unsound because toReal is totalized.

l2ToL1 bundles the linear map as a continuous linear map. l2ToL1_apply_ae exposes its representative identity, while norm_l2ToL1_le records the operator-norm bound. On a probability space the coefficient becomes one. On the zero measure space the operator norm becomes zero, which is why the module states a bound rather than unconditional norm equality.

l2ToL1_injective proves injectivity at the quotient level. It is not a pointwise statement. Two \(L^2\) classes with equal \(L^1\) images have almost-everywhere equal representatives and are therefore equal as \(L^2\) classes.

denseRange_l2ToL1 proves density using finite-range simple functions. Every simple \(L^1\) vector has a genuine finite-range representative; finite mass makes that representative square-integrable. Since simple functions are dense in \(L^1\), the inclusion has dense range.

dense_image_l2ToL1_of_dense is the reusable topological lemma: the image of a dense set under a continuous map with dense range is dense. It is applied to define fixedPlusSimpleCoboundarySetL1, the image of the RMT-25 core. dense_fixedPlusSimpleCoboundarySetL1 proves its density.

ae_mem_birkhoffConvergenceSet_of_mem_fixedPlusSimpleCoboundarySetL1 performs the representative bridge. A member of the \(L^1\) core comes from an \(L^2\) core vector. RMT-25 gives almost-everywhere convergence for the \(L^2\) representative, l2ToL1_apply_ae relates the two representatives, and the earlier convergence-event transport theorem carries membership across that almost-everywhere equality.

The final theorem

The public summit is ae_mem_birkhoffConvergenceSet_of_integrable:

theorem ae_mem_birkhoffConvergenceSet_of_integrable
    [IsFiniteMeasure μ]
    (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) :
    ∀ᵐ ω ∂μ, ω ∈ birkhoffConvergenceSet T f

The proof turns \(f\) into its \(L^1\) equivalence class, chooses a nearby member \(g_1\) of fixedPlusSimpleCoboundarySetL1, and uses the exact identity

The first equality is representative-safe: hf.coeFn_toL1 supplies the almost-everywhere equality between the raw function and its \(L^1\) class. The included core theorem supplies almost-everywhere convergence for \(g_1\). These data satisfy the abstract maximal-closure hypothesis, so the conclusion follows.

The limit remains existential and point-dependent:

Nothing in the signature says that \(c\) is measurable as a selected function, invariant, integrable, a conditional expectation, or constant. Those are later theorems, not prose consequences of this one.

Assumption ledger

Finite mass is sufficient here, not mathematically optimal for every version of Birkhoff’s theorem. The formalization makes the chosen route visible rather than advertising it as a sharp boundary.

Declaration map, in source order

The table is intentionally complete. Small event-membership and representative lemmas are part of the public proof contract, not disposable implementation trivia.

Boundary probes compiled with the theorem

Seven anonymous examples keep the edge behavior executable.

1. Zero threshold. birkhoffCauchyExceptionalSet T f 0 = Set.univ because choosing \(m=n=N\) always witnesses distance at least zero. This proves that positive scale is essential to the quantitative closure statements.
2. Zero measure. The l2ToL1 operator norm is zero, not one. Total mass zero collapses both quotient spaces.
3. Probability specialization. If \(\mu(\Omega)=1\), the general norm bound simplifies to \(\lVert l2ToL1\rVert\le1\). Probability is a corollary, not a premise of the main theorem.
4. Positive threshold. Threshold one exercises the strict positivity gate in the absolute maximal estimate and simplifies away the denominator.
5. Zero-measure theorem. The final pointwise theorem compiles directly at the zero measure with no nonzero-mass premise; its almost-everywhere conclusion is vacuous, as it should be.
6. Identity dynamics. Every integrable observable satisfies the final conclusion for MeasurePreserving.id μ without an ergodicity hypothesis.
7. Nonbijective Dirac dynamics. The constant map on Bool preserves the Dirac mass at false, is neither injective nor surjective, and still satisfies the final theorem for every integrable observable. It simultaneously blocks hidden injectivity, surjectivity, and invertibility requirements.

The module also prints the axiom footprints of the absolute maximal theorem, the abstract closure theorem, the dense inclusion, the included core, and the final pointwise theorem. The warning-fatal check reports only propext, Classical.choice, and Quot.sound. No project axiom, sorry, or unsafe declaration appears.

How to run the formalization

From the repository root on macOS or Linux:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomCocycles/PointwiseBirkhoff.lean
lake build
cd ..
make content-hygiene
make site-check

The direct Lean command checks the leaf module with warnings fatal. lake build checks the complete project import graph. The final two commands inspect the public teaching content and render the site.

To inspect only the theorem signature in a scratch file:

import NonlinearDynamics.Random.RandomCocycles.PointwiseBirkhoff

open MeasureTheory Filter
open NonlinearDynamics.Random.RandomCocycles

#check ae_mem_birkhoffConvergenceSet_of_integrable
#print axioms ae_mem_birkhoffConvergenceSet_of_integrable

Solved exercises

Exercise 1: prove the absolute average inequality

Expand the Birkhoff average as a nonnegative scalar times a finite sum. Apply the finite-sum triangle inequality, then multiply by the nonnegative inverse of the natural horizon. At horizon zero Lean’s totalized inverse and empty sum make both sides zero. This is exactly the proof strategy of abs_birkhoffAverage_le_birkhoffAverage_abs.

Exercise 2: why is there no factor two?

One could split \(h=h^+-h^-\) and control positive and negative crossings separately, which often introduces a factor two. Here \(|A_nh|\le A_n|h|\) pointwise, so a single application of the one-sided maximal estimate to \(|h|\) controls the absolute event with constant one.

Exercise 3: distinguish weak and strong type

The inequality \(\mu\{M h\gt a\}\le\lVert h\rVert_1/a\) controls level-set measure and is weak type \((1,1)\). A strong type statement would bound \(\int M h\,d\mu\) by a constant times \(\lVert h\rVert_1\). The latter is not proved and is generally false for the classical maximal ergodic operator at the endpoint.

Exercise 4: negate the exceptional event

Negating

gives

The strict inequality appears because the original relation was non-strict. This matches the metric Cauchy criterion directly.

Exercise 5: derive the three-error bound

Insert \(A_mg\) and \(A_ng\) between \(A_mf\) and \(A_nf\), then use the real triangle inequality twice. Linearity of Birkhoff averages turns each endpoint difference into an average of \(f-g\). Two endpoint bounds of \(\varepsilon/3\) plus one strict middle bound below \(\varepsilon/3\) give a strict total below \(\varepsilon\).

Exercise 6: why force the witnesses past one?

The maximal event quantifies only \(n\ge1\), while a Cauchy failure supplies witnesses beyond any chosen tail index. Ask the failure event for witnesses beyond \(\max(N,1)\). They remain beyond the approximant’s Cauchy cutoff and become legal positive-time maximal witnesses.

Exercise 7: kill one fixed scale

Fix \(\eta\gt0\) and choose a good \(g\) with \(\lVert f-g\rVert_1\lt\eta\varepsilon/3\). The quantitative closure bound gives

Because the real measure is nonnegative and this holds for every positive \(\eta\), it equals zero. The Lean proof then converts real-measure zero back to ordinary extended-measure zero.

Exercise 8: why not intersect every real epsilon?

An uncountable intersection of conull sets need not be conull. The reciprocal naturals \(1/(k+1)\) form a countable positive family approaching zero. Every positive tolerance dominates one of them, so they are sufficient for the Cauchy criterion.

Exercise 9: locate completeness

All maximal and density reasoning produces only a pointwise Cauchy sequence. The fact that every real Cauchy sequence converges enters exactly at cauchySeq_tendsto_of_complete. Replacing \(\mathbb R\) by an incomplete metric codomain would require completion or a stronger hypothesis.

Exercise 10: prove the finite-measure inclusion coefficient

Apply Hölder to \(h\cdot1\):

RMT-26 uses Mathlib’s exponent-comparison theorem at the extended seminorm level and then justifies the conversion to real norms.

Exercise 11: explain dense range

Finite-range simple functions are dense in \(L^1\). On a finite measure space, every measurable finite-range function is square-integrable because it is measurable, bounded, and the whole space has finite mass. Thus every simple \(L^1\) vector lies in the image of l2ToL1, and the image is dense.

Exercise 12: handle zero total mass

When \(\mu=0\), every two functions are almost everywhere equal. Both \(L^1\) and \(L^2\) are zero spaces, so the inclusion map has operator norm zero. The bound \(\lVert l2ToL1\rVert\le\mu(\Omega)^{1/2}\) specializes correctly to zero.

Exercise 13: separate injectivity from pointwise equality

l2ToL1_injective says equality of the \(L^1\) images forces equality of the \(L^2\) equivalence classes. It does not say their chosen representatives are equal at every point. The proof uses almost-everywhere equalities and Lp.ext.

Exercise 14: reconstruct the final approximation

Turn the raw integrable \(f\) into hf.toL1 f. Density gives \(g_1\) in the included core with dist f₁ g₁ < δ. The theorem L1.dist_eq_integral_dist and the representative equality hf.coeFn_toL1 identify that distance with \(\int|f-g_1|\,d\mu\). The core theorem supplies almost-everywhere convergence for \(g_1\), completing the abstract hypothesis.

Exercise 15: show why ergodicity is absent

The closure proof requires only almost-everywhere convergence of each approximant. It does not require invariant events to have measure zero or full measure. Ergodicity is relevant when identifying or rigidifying the limit, not when proving that a limit exists.

Exercise 16: audit the noninjective Dirac example

Let \(S:\mathrm{Bool}\to\mathrm{Bool}\) be constant at false. It is not injective because false and true have the same image. The pushforward of the Dirac mass at false is still that Dirac mass. Therefore S is measure-preserving and the final theorem applies even though no inverse exists.

Exercise 17: identify the finite-prefix principle

A sequence converges if and only if any sequence obtained by changing finitely many terms converges to the same limit. The proof does not need this as a separate lemma: every Cauchy statement is tail-based, and the maximal containment explicitly pushes witnesses beyond horizon one.

Exercise 18: state the exact summit without overclaiming

The correct conclusion is

It is not yet \(c=\mathbb E[f\mid\mathcal I]\), not yet \(c=\int f\,d\mu\), and not yet a named measurable function. Each stronger statement needs additional proof.

Discussion

Everything in this section is interpretation. The warning-fatal theorem and its explicit assumptions stand on their own; the conceptual connections below do not add checked conclusions.

The proof illustrates why pointwise ergodic theory is often organized around maximal inequalities. Density proves a theorem on a tractable algebraic core, but a pointwise conclusion is discontinuous in ordinary norm topology. A weak maximal inequality supplies the missing replacement for continuity: small norm error implies small measure of the set on which any time horizon exposes a large pointwise error. This is exactly the form of stability needed to pass from the core to the completed space.

The formal architecture also separates three completions that are easy to blend in prose. Completing simple functions in \(L^1\) creates equivalence classes. Completing the real numbers turns pointwise Cauchy sequences into limits. Taking a countable intersection of conull sets creates one set on which every reciprocal-scale condition holds simultaneously. Each completion has a different theorem and a different failure mode.

The next natural theorem is limit identification. That task is not a cosmetic corollary. It requires choosing a measurable limit representative, proving integrability and invariance, relating its integrals over invariant measurable sets to those of \(f\), and reconciling exact invariant sets with a mod-null invariant sigma algebra. Only after that layer can ergodicity collapse the limit to a constant, and only under probability normalization does the familiar space-average formula take its simplest form.

The next ridge

RMT-26 completes the existence half of the real finite-measure pointwise Birkhoff theorem. RMT-27 supplies the missing measurable representative, uniform-integrability and \(L^1\) bridge, invariant-set integral identities, and conditional-expectation uniqueness. With the additive theorem complete, the roadmap can add the carefully normalized ergodic corollary and then return to the orbit-majorant, phase-averaging, and interval-packing infrastructure for Kingman’s theorem.

References

Stefan Banach. Sur la convergence presque partout de fonctionnelles linéaires, Bulletin des Sciences Mathématiques 50, 27–32 and 36–43, 1926, reprinted in the linked collected-works scan. Theorems I and III develop continuity in measure and extension of almost-everywhere convergence from a dense subset. RMT-26 uses a Banach-principle strategy with a quantitative weak maximal estimate; it does not claim to invoke Banach’s historical theorem verbatim.

George D. Birkhoff. Proof of the Ergodic Theorem, Proceedings of the National Academy of Sciences 17(12), 656–660, 1931, DOI. The paper treats an invariant flow and proves its individual theorem with a limsup and liminf integral argument. It did not use the later transformation maximal theorem.

Kôsaku Yosida and Shizuo Kakutani. Birkhoff’s Ergodic Theorem and the Maximal Ergodic Theorem, Proceedings of the Imperial Academy 15(6), 165–168, 1939, DOI. Theorem 2 is presented as the new maximal ergodic theorem. Its map assumptions differ from RMT-26, so the chapter cites it for lineage rather than theorem identity.

Kôsaku Yosida. Ergodic theorems of Birkhoff-Khintchine’s type, Japanese Journal of Mathematics 17, 31–36, 1940, DOI. Pages 33–34 combine a closure lemma attributed to Banach with convergence on a bounded dense class. This is the closest primary historical precedent for the architecture used here.

Eberhard Hopf. The General Temporally Discrete Markoff Process, Journal of Rational Mechanics and Analysis 3, 13–45, 1954, DOI. Hopf generalized the maximal and ergodic framework to positive contractions and Markov operators. The repository uses the historically modest phrase “Hopf-style maximal control.”

Adriano Garsia. A Simple Proof of E. Hopf’s Maximal Ergodic Theorem, Journal of Mathematics and Mechanics 14(3), 381–382, 1965, DOI. This short proof is the closest classical source for the finite-maximum proof style upstream of RMT-24.

Michael Keane and Karl Petersen. Easy and Nearly Simultaneous Proofs of the Ergodic Theorem and Maximal Ergodic Theorem, IMS Lecture Notes–Monograph Series 48, 248–251, 2006, with open arXiv:math/0608251v1, submitted 2006-08-10. The peer-reviewed article treats a possibly noninvertible measure-preserving transformation on a probability space and separates the maximal inequality from the convergence corollary.

Mathlib contributors. Exponent comparison for finite-measure Lp spaces, simple-function density, and the L1 norm-integral bridge, Mathlib 4.32.0. These are the pinned upstream interfaces behind the finite measure inclusion, dense range, and final raw-representative approximation.

Nonlinear Dynamics in Lean contributors. PointwiseBirkhoff.lean, the checked source described declaration by declaration in this chapter.

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