Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Birkhoff's theorem for an ergodic probability system

Statement

If T is an ergodic measure-preserving transformation of a probability space and f is an integrable real-valued measurable function, then, for n1, the averages Anf=n1j=0n1fTj satisfy Anfc=fdP almost surely and in L1. Invertibility is not required.

Facts & Assumptions

[F1]

The Lebesgue integral is linear on L1(μ): The class L1(μ) is a complex vector space, and the Lebesgue integral is complex-linear on it: (αf+βg)dμ=αfdμ+βgdμ(α,βC, f,gL1(μ)).

[F2]

Arithmetic and lattice operations preserve measurability whenever they are defined: Let (X,A) be a measurable space and let f,g:XR be measurable. Then:

  1. cf is measurable for every real scalar c;
  2. max(f,g), min(f,g), f, f+, and f are measurable;
  3. if f+g is pointwise defined, then f+g is measurable;
  4. with the convention of rem-zero-times-infinity-convention-for-pointwise-products, the pointwise product fg is measurable.
[F3]

Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable: Let (X,A) be a measurable space and let fn:XR be measurable for every nN. Then the functions

supnfn,infnfn,lim supnfn,lim infnfn

are measurable. The set

{x:limnfn(x) exists in R}

is measurable. In particular, if fnf pointwise, then f is measurable.

[F4]

The maximal ergodic inequality on a probability space: Let T preserve a probability measure P, and let f be integrable, real-valued and measurable. Put Skf=j=0k1fTj, MN=max(0,S1f,,SNf) and EN={MN>0} for N1. Then ENfdP0, and also EfdP0 for E={supk1Skf>0}.

[F5]

Ergodicity relative to an invariant measure: A measure-preserving system is ergodic for μ if each EI has μ(E)=0 or μ(XE)=0, with I as in def-strict-and-mod-null-invariant-σ-algebras. For a probability system this means μ(E){0,1}. The definition is relative to the invariant measure; no probability assumption is implicit in the general null/conull formulation.

[F6]

Finite and countable subadditivity of measures: Let μ be a measure and let (Ek)kN be measurable. Then

μ(kNEk)k=0μ(Ek).

For every mN one also has

μ(k<mEk)k<mμ(Ek),

including m=0, where both sides are 0.

[F7]

Dominated convergence: Let f and (fn) be measurable complex-valued functions such that fnf almost everywhere and fng almost everywhere for a single nonnegative measurable function g with gdμ<+. Then fL1(μ), fnfdμ0, and hence fndμfdμ.

[F8]

The modulus of an integral is bounded by the integral of the modulus: If fL1(μ), then fdμfdμ.

[F9]

Integral invariance under measure-preserving maps: If T preserves μ and f:X[0,] is measurable, then fTdμ=fdμ, allowing infinity. If f is integrable real or complex valued, fT is integrable and the same equality holds. Conversely, for a measurable self-map, equality for every measurable indicator implies measure preservation.

Proof

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1

Set h=fc so hdP=0 by F1. For n1, the finite averages are measurable by F2, and L=lim supnAnh is extended-real measurable by F3.

F1F2F3
1.2

At every x and every n1, Anh(Tx)=((n+1)/n)An+1h(x)h(x)/n. This implies L(Tx)=L(x) even if L is infinite: multiplying a real sequence by positive factors tending to one preserves finite limsup by eventual upper bounds and a subsequence tending to that limsup; if the limsup is positive infinity there is a subsequence tending to positive infinity, and if it is negative infinity all sufficiently late terms lie below every fixed negative bound. Subtraction of h(x)/n tends to zero because h is finite everywhere. Thus for every ε>0 the measurable set D={L>ε} is strictly invariant.

givenalgebra
2.1

Let g=(hε)1D, an integrable function. Strict invariance in step 1.2 gives Sng=1D(Snhnε) for n1. Outside D all these sums vanish; inside D the defining strict limsup gives some positive sum. Thus {supn1Sng>0}=D, and F4 gives D(hε)dP0.

F4step 1.2
3.1

By F5, P(D) is zero or one. If it were one, step 1.1 would give D(hε)=ε<0, contrary to step 2.1. Hence P(D)=0. Apply this conclusion to h and -h and to ε=1/m for every positive integer m. F6 makes the union of the exceptional events null, so lim supAnh0lim infAnh almost surely. This proves the almost-sure assertion.

F5F6step 1.1step 2.1
4.1

For each integer K1 put fK=f1{fK} and cK=fK. Step 3.1 applied to f_K gives AnfKcK almost surely, and AnfKcK2K. F7 yields AnfKcK10.

F7
5.1

By F8 and F9, An(ffK)1ffK1 and ccKffK1. Consequently Anfc12ffK1+AnfKcK1. Dominated convergence makes the first term tend to zero as K increases, uniformly in n; step 4.1 then handles the second term with K fixed. This proves L1 convergence.

F8F9step 4.1

Depends on

Used by

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources