A formalization of Doob's martingale convergence theorems in mathlib
summary
Formalization of Doob’s martingale convergence theorems in mathlib proves almost-sure and L1 convergence for martingales, builds a conditional expectation via orthogonal projection on L2 then extends to L1, and supports Banach-valued martingales (not just real-valued) while requiring only finite measures. The project formalizes stopping times, upcrossing estimates and uses the upcrossing inequality to bound expected upcrossings, produces Lévy’s generalized Borel–Cantelli lemma, and is merged into mathlib so the results can be reused by subsequent formal developments.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:36Intuition for Martingales
- 3:14Gambler's Ruin
- 4:47Motivation
- 5:51Formalization of probability theory
- 7:42Lean and mathlib
- 9:56Construction of the Conditional Expectation
- 11:41Conditional Expectation in Lean
- 14:22Martingale Convergence Theorems
- 15:43Proof Outline
- 18:08Formalized theorems
- 18:44Final Remarks
related talks
33mA Few Connections Between Optimization and Probability
01h 08mTools from Stochastic Calculus 2
34mMatrix Martingales in Randomized Numerical Linear Algebra
13mFormalizing a First-order Differentiable Logic with MathComp
58mTools from Stochastic Calculus 1
01h 00mLocalization Schemes
57mBlackwell’s Approachability Theorem
56mSome Probabilistic Uses of Dirichlet Eigenvectors