Papers With

← All papers
First page of A Formalization of Doob's Martingale Convergence Theorems in mathlib

A Formalization of Doob's Martingale Convergence Theorems in mathlib

Kexing Ying, Rémy Degenne

cs.LO Dec 11, 2022 · v1
formalization probability analysis mathlib
Read PDF arXiv abstract
TL;DR
Formalizes Doob's martingale convergence and conditional expectation in Lean's mathlib.
Abstract
We present our formalization of Doob's martingale convergence theorems within the mathlib library for the Lean theorem prover. These theorems provide conditions under which (sub)martingales converge, almost everywhere or in L^1. To achieve this formalization, we construct a definition of conditional expectation in Banach spaces and develop theory around stochastic processes, stopping times, and martingales. As an application, we also formalize Lévy's generalized Borel-Cantelli lemma. This work represents one of the earliest developments of probability theory in mathlib, building on diverse parts of that library such as topology, analysis and most importantly measure theory.
Problem

Probability theory, specifically martingale convergence theory, was largely absent from Lean's mathematical library, despite being foundational to stochastic analysis and applications like the Borel-Cantelli lemma.

Approach

The authors formalize Doob's martingale convergence theorems in mathlib for the Lean theorem prover, providing conditions under which submartingales converge almost everywhere or in L^1. They construct a definition of conditional expectation in Banach spaces and develop theory around stochastic processes, stopping times, and martingales. As an application, they formalize Levy's generalized Borel-Cantelli lemma.

Results

The work represents one of the earliest developments of probability theory in mathlib, building on topology, analysis, and measure theory components of the library.