  We present the formalization of Doob's martingale convergence theorems in the
mathlib library for the Lean theorem prover. These theorems give conditions
under which (sub)martingales converge, almost everywhere or in $L^1$. In order
to formalize those results, we build a definition of the conditional
expectation in Banach spaces and develop the theory of stochastic processes,
stopping times and martingales. As an application of the convergence theorems,
we also present the formalization of L\'evy's generalized Borel-Cantelli lemma.
This work on martingale theory is one of the first developments of probability
theory in mathlib, and it builds upon diverse parts of that library such as
topology, analysis and most importantly measure theory.
