A Formalization of Doob's Martingale Convergence Theorems in mathlib

TL;DR

This paper formalizes Doob's martingale convergence theorems within the mathlib library for the Lean theorem prover, establishing foundational probability results through extensive measure-theoretic and stochastic process formalizations.

Contribution

It introduces a formalization of key martingale convergence theorems and related concepts like conditional expectation and stopping times in mathlib, advancing the mechanized probability theory.

Findings

Formalization of Doob's martingale convergence theorems in mathlib

Development of conditional expectation in Banach spaces

Formal proof of Lévy's generalized Borel-Cantelli lemma

Abstract

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.