A Formalization of Doob's Martingale Convergence Theorems in mathlib. - Kexing Ying; Rémy Degenne (CPP, 2023)