Exchangeability and de Finetti’s theorem

6 Main Theorem

We package the three-way equivalence as three separate top-level theorems, one per proof of the main implication. The default project export is the martingale version.

Theorem 50 de Finetti–Ryll-Nardzewski equivalence (martingale route)
✓
#

Uses

Lean declarations

For an infinite sequence \((X_n)_{n \in \mathbb {N}}\) of random variables taking values in a standard Borel space \(\alpha \) (with \(\alpha \) nonempty), the following are equivalent:

  1. \((X_n)\) is contractable

  2. \((X_n)\) is exchangeable

  3. \((X_n)\) is conditionally i.i.d. (i.e., there exists a directing kernel \(\nu \))

This is the default project export. The proof constructs \(\nu \) from the tail \(\sigma \)-algebra \(\mathcal{T}\) via \(\nu (\omega )(B) = \mathbb {E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}](\omega )\).

Theorem 51 de Finetti–Ryll-Nardzewski equivalence (L\(^2\) route)
✓
#

Uses

Lean declarations

Same three-way equivalence, proved via the elementary L\(^2\) approach. This route is currently stated for real-valued sequences (see the L\(^2\) section caveat).

Theorem 52 de Finetti–Ryll-Nardzewski equivalence (Koopman route)
✓
#

Uses

Lean declarations

Same three-way equivalence, proved via the Mean Ergodic Theorem through the Koopman operator. This route is currently stated for real-valued sequences (see the Koopman section caveat).