Alphabeta Math
LemmaStatement: 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.

The maximal ergodic inequality on a probability space

Statement

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}.

Facts & Assumptions

[F1]

Measure-preserving transformations and systems: Let (X,A,μ) be a measure space. A measurable self-map T:XX is measure preserving if μ(T1E)=μ(E) for every EA. The quadruple (X,A,μ,T) is a measure-preserving system; it is a probability system if μ(X)=1. Here T1E={x:T(x)E} denotes an inverse image, whether or not T is invertible. Neither completeness nor finiteness is implicit. The measure-space and measurable-map conventions are def-measure-space and def-measurable-function-between-measurable-spaces.

[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]

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.

[F4]

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(μ)).

[F5]

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μ.

Proof

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

1.1

The measurable self-map in F1 and F2 make all finite sums and maxima measurable. Also 0MNj<NfTj, whose integral is NfdP< by F3. Thus M_N and its composition with T are integrable.

F1F2F3
1.2

For 1kN, Skf=f+(Sk1f)Tf+MNT, with S0f=0. On E_N take a maximizing k to get fMNMNT. On the complement M_N=0 and MNT0. Hence everywhere f1ENMNMNT.

givenalgebra
2.1

Integrate the inequality in step 1.2. Integrability is supplied by step 1.1; F4 and F3 give ENfdPMNdPMNTdP=0.

F3F4step 1.2step 1.1
3.1

The sets E_N increase to E. Since f1ENf and f1ENf1E pointwise, F5 takes step 2.1 to EfdP0.

F5step 2.1

Depends on

Used by

Dependency tree · two levels

23 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