1 paper
Kexing Ying, Rémy Degenne
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)martingal…