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 preserve a probability measure , and let be integrable, real-valued and measurable. Put , and for . Then , and also for .
Facts & Assumptions
Measure-preserving transformations and systems: Let be a measure space. A measurable self-map is measure preserving if for every . The quadruple is a measure-preserving system; it is a probability system if . Here denotes an inverse image, whether or not 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.
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.
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.
The Lebesgue integral is linear on : The class is a complex vector space, and the Lebesgue integral is complex-linear on it:
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
Proof
Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.
The measurable self-map in F1 and F2 make all finite sums and maxima measurable. Also , whose integral is by F3. Thus M_N and its composition with T are integrable.
For , , with . On E_N take a maximizing k to get . On the complement M_N=0 and . Hence everywhere .
Integrate the inequality in step 1.2. Integrability is supplied by step 1.1; F4 and F3 give .
The sets E_N increase to E. Since and pointwise, F5 takes step 2.1 to .
Depends on
- Measure-preserving transformations and systems
- Integral invariance under measure-preserving maps
- Arithmetic and lattice operations preserve measurability whenever they are defined
- The Lebesgue integral is linear on $L^1(\mu)$
- The modulus of an integral is bounded by the integral of the modulus
- Dominated convergence
- Monotonicity and nonnegative homogeneity of the nonnegative integral
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
- Durrett, Probability: Theory and Examples, 5th ed., Lemma 6.2.2, printed p.335; complete proof read (standard reference, not scraped)