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 is an ergodic measure-preserving transformation of a probability space and is an integrable real-valued measurable function, then, for , the averages satisfy almost surely and in . Invertibility is not required.
Facts & Assumptions
The Lebesgue integral is linear on : The class is a complex vector space, and the Lebesgue integral is complex-linear on it:
Arithmetic and lattice operations preserve measurability whenever they are defined: Let be a measurable space and let be measurable. Then:
- is measurable for every real scalar ;
- , , , , and are measurable;
- if is pointwise defined, then is measurable;
- with the convention of rem-zero-times-infinity-convention-for-pointwise-products, the pointwise product is measurable.
Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable: Let be a measurable space and let be measurable for every . Then the functions
are measurable. The set
is measurable. In particular, if pointwise, then is measurable.
The maximal ergodic inequality on a probability space: Let preserve a probability measure , and let be integrable, real-valued and measurable. Put , and for . Then , and also for .
Ergodicity relative to an invariant measure: A measure-preserving system is ergodic for if each has or , with as in def-strict-and-mod-null-invariant--algebras. For a probability system this means . The definition is relative to the invariant measure; no probability assumption is implicit in the general null/conull formulation.
Finite and countable subadditivity of measures: Let be a measure and let be measurable. Then
For every one also has
including , where both sides are .
Dominated convergence: Let and be measurable complex-valued functions such that almost everywhere and almost everywhere for a single nonnegative measurable function with . Then , and hence
Integral invariance under measure-preserving maps: If preserves and is measurable, then , allowing infinity. If is integrable real or complex valued, 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.
Set so by F1. For , the finite averages are measurable by F2, and is extended-real measurable by F3.
At every and every , . This implies even if 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 tends to zero because is finite everywhere. Thus for every the measurable set is strictly invariant.
Let , an integrable function. Strict invariance in step 1.2 gives for . Outside all these sums vanish; inside the defining strict limsup gives some positive sum. Thus , and F4 gives .
By F5, P(D) is zero or one. If it were one, step 1.1 would give , 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 almost surely. This proves the almost-sure assertion.
For each integer put and . Step 3.1 applied to f_K gives almost surely, and . F7 yields .
By F8 and F9, and . Consequently . 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 convergence.
Depends on
- The maximal ergodic inequality on a probability space
- Ergodicity relative to an invariant measure
- Integral invariance under measure-preserving maps
- Arithmetic and lattice operations preserve measurability whenever they are defined
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
- The Lebesgue integral is linear on $L^1(\mu)$
- The modulus of an integral is bounded by the integral of the modulus
- Dominated convergence
- Finite and countable subadditivity of measures
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.