Exchangeability and de Finetti’s theorem

3 Easy Directions

3.1 Exchangeable implies Contractable

Lemma 10 Permutation extension
✓
#

Lean declarations

Any strictly increasing function \(k : \mathrm{Fin}(m) \to \mathbb {N}\) with range contained in \(\{ 0, \ldots , n-1\} \) extends to a permutation of \(\{ 0, \ldots , n-1\} \).

Theorem 11 Exchangeable implies Contractable
✓
#

Uses

Lean declarations

If \((X_n)\) is exchangeable, then it is contractable.

3.2 Conditionally i.i.d. implies Exchangeable

Theorem 12 Conditionally i.i.d. implies Exchangeable
✓
#

Uses

Lean declarations

If \((X_n)\) is conditionally i.i.d., then it is exchangeable.