Skip to content

Tags: cameronfreer/exchangeability

Tags

v1.1

Toggle v1.1's commit message
Lean 4.27.0-rc1 upgrade complete - all proofs verified

v1.0.0

Toggle v1.0.0's commit message
Complete formalization of de Finetti's theorem

Three independent proofs of Kallenberg Theorem 1.1:
- Martingale approach (default)
- L² approach
- Koopman/Ergodic approach

All proofs complete with no sorries.