Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14
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 pointwise ergodic theorem

Statement

Let μ be sigma-finite, let T preserve μ, and let f be a finite-valued real- or complex-valued measurable representative in L1(μ). Then Anf converges μ-almost everywhere to a finite-valued integrable function f∗ satisfying

f∗∘T=f∗μ-almost everywhere,∥f∗∥1≤∥f∥1.

The a.e. class of f∗ depends only on the a.e. class of f. No ergodicity, finite total measure, completeness, or invertibility is assumed.

Facts & Assumptions

Given: The sigma-finite measure-preserving system and integrable representative in the Statement.

[F1]

Every rational oscillation set is invariant and has finite measure (Sigma-finite ergodic oscillation sets have finite measure).

[F2]

The maximal ergodic theorem holds on arbitrary measure spaces (Maximal ergodic theorem).

[F3]

Fatou's lemma bounds the integral of a lower limit of nonnegative measurable functions (Fatou's lemma).

[F4]

Composition by T preserves integrals, and countable unions of measurable null sets are null (Integral invariance under measure-preserving maps, Finite and countable subadditivity of measures).

Proof

technique · direct rational-oscillation argument
1.1givenalgebra

Suppose first that f is real. Write u=lim sup⁡nAnf and ℓ=lim inf⁡nAnf. The exact identity Anf(Tx)=n+1nAn+1f(x)−1nf(x) shows that u∘T=u and ℓ∘T=ℓ, with extended values allowed. The divergence set {ℓ<u} is the union of the sets Eα,β over rational β<α.

1.2F4

If f=g a.e., let N={f≠g}. Outside ⋃k≥0T−kN, a null set by preservation and [F4], every summand in Snf equals the corresponding summand in Sng. Thus the limits agree a.e.; the construction descends to the L1 class.

2.1F1F2step 1.1

Fix such β<α and put E=Eα,β. By [F1], E is strictly invariant and μ(E)<∞. For g=(f−α)1E, strict invariance gives Sng=1E(Snf−nα). Every x∈E has Snf(x)>nα for some n, so E={sup⁡nSng>0}. Applying [F2] gives ∫Ef dμ≥αμ(E).

3.1F1F2step 2.1

Apply the same argument to −f and the thresholds −β>−α. Its oscillation set is again E, so ∫Ef dμ≤βμ(E). Because f is integrable and E has finite measure, both inequalities are finite. Thus (α−β)μ(E)≤0, and μ(E)=0.

4.1F3F4step 1.1step 3.1

There are only countably many rational pairs. Hence [F4] and steps 1.1–3.1 show that Anf has an extended-real limit off a null set. On that set, ∣f∗∣=lim inf⁡n∣Anf∣, and contractivity gives ∫∣Anf∣≤∫∣f∣. Fatou therefore yields ∫∣f∗∣≤∫∣f∣<∞, which both makes f∗ finite a.e. and proves integrability.

5.1F4step 1.1step 4.1

Define f∗=0 on the exceptional null set. The identity in step 1.1 shows that the convergence set and the limit are invariant wherever the averages converge; after adding the null exceptional orbit set if necessary, f∗∘T=f∗ a.e.

6.1F3F4step 4.1step 5.1step 1.2∎

For complex f, apply the real result to Re⁡f and Im⁡f and combine their two conull convergence sets. Their limits give the complex limit, its invariance, and its representative independence. Fatou applied directly to ∣Anf∣ gives the stated complex L1 bound. Only these two determined components are used, so no choice principle enters.

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