Almost sure frequency of heads

Variance and covariance identities for random variables: Let $X,Y$ be square-integrable real random variables on one probability space. Then $\mathrm{Var}(X)=\mathbb{E}[X^2]-\mathbb{E}[X{]}^2,$ $\mathrm{Cov}(X,Y)=\mathbb{E}[XY]-\mathbb{E}[X]\mathbb{E}[Y]\mathrm{.}$ Moreover, covariance is symmetric and bilinear on finite linear combinations. On finite full-power-set probability spaces these formulas reduce to the published finite identities.

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 F6, the coordinate maps $X_n(x)=x_n$ have laws ${\mu }_n$ and are independent.

Iid finite variance strong law: IID square-integrable real variables satisfy $S_n\mathrm{/}n\to \mathbb{E}{X}_1$ almost surely.