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.

Fair-coin frequency strong law

Statement

Assume the Axiom of Countable Choice. On one-sided binary sequence space with fair-coin probability,

$\frac{1}{n} \sum_{k = 0}^{n - 1} x_{k} ⟶ \frac{1}{2}$

almost surely.

Facts & Assumptions

Given: Countable choice, binary sequence space $Ω = {0, 1}^{N}$ , its fair-coin probability $p$ , and the left shift $σ$ .

[F1]

The fair-coin measure gives every one-coordinate cylinder mass $1 / 2$ (Fair-coin measure on binary sequences).

[F2]

The shift preserves $p$ , is strongly mixing, and hence is ergodic (The fair-coin one-sided shift preserves measure and is mixing, Mixing implies weak mixing, which implies ergodicity).

[F3]

Birkhoff supplies an invariant almost-everywhere limit (Birkhoff pointwise ergodic theorem), and ergodicity makes every finite invariant measurable function constant almost everywhere (Equivalent invariant-set and invariant-function criteria for ergodicity).

[F4]

Dominated convergence and invariance of integrals identify bounded ergodic limits (Dominated convergence, Integral invariance under measure-preserving maps).

Proof

technique · apply Birkhoff to the first coordinate

1.1

Define $f (x) = x_{0}$ . Then $f$ is the indicator of the one-coordinate cylinder ${x : x_{0} = 1}$ , so $0 \leq f \leq 1$ and $\int f d p = 1 / 2$ .

F1construct

1.2

Since $f (σ^{k} x) = x_{k}$ , $A_{n} f (x) = \frac{1}{n} \sum_{k = 0}^{n - 1} x_{k} .$

givenalgebra

2.1

By [F2] and [F3], $A_{n} f$ converges almost everywhere to a constant $c$ . The bound $0 \leq A_{n} f \leq 1$ , dominated convergence, and integral invariance give $c = \int c d p = \lim_{n} \int A_{n} f d p = \int f d p = \frac{1}{2} .$

F2F3F4step 1.1

3.1

Combining steps 1.2 and 2.1 proves the asserted almost-sure frequency limit. Countable choice is inherited from the fair-coin measure and shift suppliers [F1]–[F2]; no further simultaneous selections occur here.

F1F2step 1.2step 2.1∎

Depends on

Used by

The fair-coin strong law as a shift average Example

Dependency tree · two levels

43 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)