Exchangeability and de Finetti’s theorem

5 Common Ending

All three proofs converge to the same final step: extending from indicators to general sets via a monotone class argument.

Lemma 47 \(\pi \)-system uniqueness
✓
#

Lean declarations

Measures on product spaces are determined by their finite-dimensional marginals.

Theorem 48 Monotone class theorem
✓
#

Uses

Lean declarations

The monotone class theorem allows extending from indicators to measurable functions.

Theorem 49 Conditional independence extension
✓
#

Uses

Lean declarations

Conditional independence on indicators extends to the full product \(\sigma \)-algebra.