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 requires integrability
Statement
Assume the Axiom of Countable Choice. False claim: Birkhoff's finite almost-everywhere convergence conclusion holds for every finite-valued measurable observable, without integrability.
Facts & Assumptions
Given: Countable choice, Lebesgue probability on , its doubling map , and
It suffices to test strict superlevel sets for extended-real measurability (Extended-real-valued measurable functions), and Borel sets are Lebesgue measurable under countable choice (Assuming countable choice, every Borel subset of is Lebesgue measurable).
Nonnegative integrals are monotone and agree with simple-function integrals (Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions); interval measure is interval length (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included).
The harmonic series diverges (For rational , converges iff ), and monotone convergence applies to increasing nonnegative measurable functions (Monotone convergence for the integral).
The doubling map is ergodic (Doubling is ergodic for Lebesgue measure); Birkhoff gives invariant finite limits for integrable truncations (Birkhoff pointwise ergodic theorem), and ergodicity makes those limits constant (Equivalent invariant-set and invariant-function criteria for ergodicity).
Dominated convergence and invariance of integrals identify the constant limits (Dominated convergence, Integral invariance under measure-preserving maps).
A countable union of null sets is null (Finite and countable subadditivity of measures).
Refutation
For , ; for , it is ; and for it is , with the right endpoint omitted if it equals . These are Borel. Hence [F1] makes the everywhere-finite function Lebesgue measurable.
On one has . For every , the simple function therefore satisfies , and
By [F2]–[F3], the right side is unbounded, so . Thus is not integrable under the integrability convention of Integrable real and complex functions, and their integrals.
For each integer , let . It is measurable, bounded, and hence integrable on this probability space; moreover . Monotone convergence and step 2.1 give
By [F4], converges almost everywhere to an invariant function and that function equals a constant almost everywhere. Since , [F5] identifies this constant as
Remove the countable union of the null exceptional sets in step 4.1; it is null by [F6]. At every remaining , for every and , , whence Because , this says .
Thus a finite-valued measurable observable can have divergent-to-infinity ergodic averages almost everywhere. This refutes the finite-limit claim and shows exactly why the hypothesis cannot be omitted. Countable choice is inherited from the Lebesgue and doubling-map suppliers; all truncations are explicit.
Depends on
- Birkhoff pointwise ergodic theorem
- Doubling is ergodic for Lebesgue measure
- Equivalent invariant-set and invariant-function criteria for ergodicity
- Integral invariance under measure-preserving maps
- Monotone convergence for the integral
- Dominated convergence
- Extended-real-valued measurable functions
- Assuming countable choice, every Borel subset of $\mathbb{R}^n$ is Lebesgue measurable
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- The nonnegative integral agrees with the simple integral on simple functions
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- For rational $p > 0$, $\sum 1/k^p$ converges iff $p > 1$
- Integrable real and complex functions, and their integrals
- Finite and countable subadditivity of measures
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
85 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
- Charles Walkden, Ergodic Theory lecture notes (standard reference, not scraped)