Birkhoff strong law for iid coordinate shifts

The Axiom of Choice: The Axiom of Choice (AC) is the following statement.

Every family of nonempty sets has a choice function (def-choice-function).

Written out: for every set $\mathcal{F}$ all of whose members are nonempty, there exists a function $g$ with domain $\mathcal{F}$ satisfying $g(S)\in S$ for all $S\in \mathcal{F}$.

An equivalent formulation is that a product of nonempty sets is nonempty: if $X_i\mathrm{\ne }\mathrm{\varnothing }$ for every $i\in I$, then ${\prod }_{i\in I}{X}_i\mathrm{\ne }\mathrm{\varnothing }$. Here ${\prod }_{i\in I}{X}_i$ is the set of functions $f$ with domain $I$ such that $f(i)\in X_i$ for every $i\in I$; when a family of nonempty sets is indexed by itself, such an $f$ is precisely a choice function for it.

The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$): The Axiom of Countable Choice, written ${\mathrm{A}\mathrm{C}}_{\omega }$, is the following statement.

For every family $(X_n{)}_{n\in \mathbb{N}}$ of nonempty sets indexed by $\mathbb{N}$ there is a function $f$ with domain $\mathbb{N}$ such that $f(n)\in X_n$ for every $n\in \mathbb{N}$.

Equivalently, in the vocabulary of def-choice-function: every at most countable family of nonempty sets (def-countable) has a choice function.

The recursion theorem: Let $(N,0,\sigma )$ be a Peano system (def-peano-system), in particular the natural numbers $\mathbb{N}$ (def-natural-numbers). For any set $A$, any element $a\in A$, and any function $f:A\to A$, there is a unique function $g:N\to A$ such that $g(0)=a$ and $g(\sigma (n))=f(g(n))$ for all $n\in N$.

The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain: Let $X$ be a set and let $R\subseteq X\times X$ be a binary relation on $X$. Call $R$ entire on $X$ when

$\text{for every }x\in X\text{ there is }y\in X\text{ with }xRy\mathrm{.}$

The Axiom of Dependent Choice, written $\mathrm{D}\mathrm{C}$, is the following statement.

For every nonempty set $X$, every relation $R$ entire on $X$, and every $a\in X$, there is a function $x:\mathbb{N}\to X$ (def-function, def-natural-numbers) with $x_0=a\text{and}{x}_{n}R{x}_{n+1}\text{ for every }n\in \mathbb{N}\mathrm{.}$

Here a sequence in $X$ means a function from $\mathbb{N}$ to $X$, not necessarily a real-valued sequence. As everywhere in this library $\mathbb{N}$ contains $0$, and the sequence is indexed from $0$; the term $x_0$ is the prescribed starting point $a$ and every later term is related to its predecessor.

What DC adds to what came before. def-choice-function and def-axiom-of-choice select one element from each member of a family that is fixed in advance, and def-countable-choice does the same for a family indexed by $\mathbb{N}$. In both, the family is given before any selection is made. DC is the principle needed when the $n$-th set to select from is not known until the first $n$ selections have been made: here the admissible values of $x_{n+1}$ are exactly the $R$-successors of $x_n$, so the family being chosen from is built along the choosing. That is precisely the situation ${\mathrm{A}\mathrm{C}}_{\omega }$ does not cover, and it is why a construction "pick $x_{n+1}$ depending on $x_n$, for every $n$ at once" is not licensed by countable choice.

The starting point may be dropped. The formally weaker statement obtained by deleting the clause $x_0=a$ — for every nonempty $X$ and every entire $R$ there is a sequence with $x_{n}R{x}_{n+1}$ for all $n$ — is an immediate consequence of the form above, since $X$ is nonempty and any of its elements may be taken as $a$. The reverse derivation is standard and is not needed anywhere in this library, so it is not carried out; every use below prescribes $x_0$.

$R$ need not be an order and the terms need not be distinct. What DC delivers is a sequence, that is a function $\mathbb{N}\to X$, not a chain in the order-theoretic sense (def-chain). The relation may be symmetric, and the sequence may repeat a value or be constant; all that is asserted is $x_{n}R{x}_{n+1}$ at every index.

Assuming countable and dependent choice, countable products of arbitrary probability spaces: Assume countable choice and dependent choice. For probability spaces $(E_n,{\mathcal{E}}_n,{\mu }_n{)}_{n\in \mathbb{N}}$ there is a unique probability measure on the canonical countable-product sigma-algebra having the prescribed finite product marginals.

Coordinate random elements of a countable product are independent: Under the measure of F5, the coordinate maps $X_n(x)=x_n$ have laws ${\mu }_n$ and are independent.

Measure preservation can be checked on a generating pi-system: Let $T:X\to X$ be measurable on $(X,\mathcal{A},\mu )$. Let $\mathcal{P}$ be a $\pi$-system generating $\mathcal{A}$, with an increasing sequence $P_n\in \mathcal{P}$ covering $X$ and satisfying $\mu (P_n)<\mathrm{\infty }$. If $\mu (T^{-1}P)=\mu (P)$ for every $P\in \mathcal{P}$, then $T$ preserves $\mu$. For finite $\mu$, a generating $\pi$-system can be enlarged by $X$ to meet the exhaustion condition.

Kolmogorov zero-one law: Let $(X_n{)}_{n\in \mathbb{N}}$ be an independent sequence of random elements, and let $\mathcal{T}(X_n:n\in \mathbb{N})$ be its tail $\sigma$-algebra. Then every event $A\in \mathcal{T}(X_n:n\in \mathbb{N})$ satisfies $\mathbb{P}(A)\in \{0,1\}\mathrm{.}$

Ergodicity relative to an invariant measure: A measure-preserving system is ergodic for $\mu$ if each $E\in \mathcal{I}$ has $\mu (E)=0$ or $\mu (X\setminus E)=0$, with $\mathcal{I}$ as in def-strict-and-mod-null-invariant-$\sigma$-algebras. For a probability system this means $\mu (E)\in \{0,1\}$. The definition is relative to the invariant measure; no probability assumption is implicit in the general null/conull formulation.

Birkhoff's theorem for an ergodic probability system: If $T$ is an ergodic measure-preserving transformation of a probability space and $f$ is an integrable real-valued measurable function, then $A_{n}f=n^{-1}{\sum }_{j=0}^{n-1}f\circ T^j\to c=\int fdP$ almost surely and in $L^1$. Invertibility is not required.