1 paper · 1 filter
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…