de Finetti's theorem: an infinite exchangeable $0$–$1$ sequence is a unique mixture of Bernoulli trials

This is de Finetti's theorem for exchangeable sequences of $0$–$1$ random variables: every such sequence is a mixture of i.i.d. Bernoulli sequences.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and let $X_1, X_2, X_3, \dots$ be random variables on it that take only the values $0$ and $1$. The finite family $X_1,\dots,X_n$ is called exchangeable if for every permutation $(k_1,\dots,k_n)$ of $(1,\dots,n)$ the random vector $(X_{k_1},\dots,X_{k_n})$ has the same $n$-dimensional distribution as $(X_1,\dots,X_n)$; the infinite sequence $(X_k)$ is exchangeable if $X_1,\dots,X_n$ are exchangeable for every $n$. Write $S_n = X_1 + \dots + X_n$.

Theorem (de Finetti). If the infinite sequence $(X_k)$ is exchangeable, then there is a probability distribution $F$ concentrated on the interval $[0,1]$ such that for all integers $0 \le k \le n$:

1. the probability that the first $k$ variables equal $1$ and the next $n-k$ equal $0$ is

2. the number of successes among the first $n$ trials has the mixed binomial law

Moreover $F$ is unique: if $G$ is any probability distribution concentrated on $[0,1]$ such that identity 1 holds with $G$ in place of $F$ for all $0 \le k \le n$, then $G = F$. (Taking $k = n$ shows that $G$ and $F$ have the same moments $\int_0^1 \theta^n$, and a distribution on the compact interval $[0,1]$ is determined by its moments — the uniqueness half of the Hausdorff moment problem.)

In words: an infinite exchangeable $0$–$1$ sequence behaves as if a success probability $\theta$ were first drawn at random from $F$ and the trials were then independent Bernoulli$(\theta)$ trials. This representation is the foundation of the subjectivist (Bayesian) interpretation of probability, where $F$ plays the role of a prior distribution, and it is the prototype of the representation theorems for symmetric measures (Hewitt–Savage) and for exchangeable sequences in general Borel spaces (Ryll-Nardzewski). The hypothesis that the sequence is infinite cannot be dropped: finite exchangeable families need not be mixtures of i.i.d. sequences.

Formalization Note The sequence is indexed from $0$: X i stands for $X_{i+1}$, so the event in (1) is $\{X_i = 1 \text{ for } i<k,\ X_i = 0 \text{ for } k \le i < n\}$ and $S_n$ is ∑ i ∈ Finset.range n, X i. The variables are real-valued, measurable, and take the value $0$ or $1$ at every point. Exchangeability is stated directly: for every $n$ and every σ : Equiv.Perm (Fin n), the push-forward of $\mathbb P$ under $\omega \mapsto (X_{\sigma(i)}(\omega))_{i<n}$ equals the push-forward under $\omega \mapsto (X_i(\omega))_{i<n}$. The mixing distribution $F$ is a probability measure on $\mathbb R$ with $F(\mathbb R \setminus [0,1]) = 0$, so the integrands are bounded $F$-almost everywhere and the Bochner integrals are genuine. Probabilities are converted to real numbers with ENNReal.toReal. The case $n = 0$ is included and reduces to $1 = F([0,1])$. Uniqueness is stated among probability measures $G$ on $\mathbb R$ with $G(\mathbb R \setminus [0,1]) = 0$, assuming of $G$ only identity 1 for all $k \le n$, and concludes the equality of measures G = F; this is equivalent to uniqueness among Borel probability measures on $[0,1]$.