Kexing Ying, Rémy Degenne: A Formalization of Doob's Martingale Convergence Theorems in mathlib. CPP 2023: 334-347