A formalization of de Finetti’s theorem for infinite sequences on standard Borel spaces.

Main Result

Theorem (Kallenberg 1.1): For an infinite sequence of random variables on a standard Borel space, the following are equivalent:

1. (Contractable) All strictly increasing subsequences of equal length have the same distribution
2. (Exchangeable) Distribution invariant under finite permutations
3. (Conditionally i.i.d.) Admits a directing kernel (mixture-of-products representation)

Three Proofs

We formalize all three proofs from Kallenberg (2005):

Approach	Method
Martingale	Reverse martingale convergence (Aldous)
L²	Elementary contractability bounds (ℝ-valued, L² integrable)
Koopman	Mean Ergodic Theorem

Visualizations

Import Graphs

Modules colored by proof: 🔵 Martingale   🟢 L²   🟠 Koopman

Graph	Description
Modules (SVG)	104 files, clickable links to docs
Modules (interactive)	Draggable, zoomable
All declarations	Searchable
Blueprint only	Documented items

Links

• Blueprint - Proof structure with Lean links
• Blueprint (PDF) - Printable version
• Documentation - Generated Lean documentation
• GitHub Repository

References

• Kallenberg, O. (2005). Probabilistic Symmetries and Invariance Principles. Springer. Chapter 1, Theorem 1.1.