← All papers
A Formalization of the Ionescu-Tulcea Theorem in Mathlib
math.PR
Jun 23, 2025 · v7
cs.DL
TL;DR
Formalizes the Ionescu-Tulcea theorem and products of arbitrary families of probability measures in Lean 4 within Mathlib.
Abstract
We describe the formalization of the Ionescu-Tulcea theorem, showing the existence of a probability measure on the space of trajectories of a Markov chain, in the proof assistant Lean using the integrated library Mathlib. We first present a mathematical proof before exposing the difficulties which arise when trying to formalize it, and how they were overcome. We then build on this work to formalize the construction of the product of an arbitrary family of probability measures.
Problem
The Ionescu-Tulcea theorem guarantees the existence of a probability measure on the trajectory space of a Markov chain. It was not available in Mathlib.
Approach
A mathematical proof of the theorem is presented first. The formalization difficulties that arise in Lean with Mathlib are then described, along with how they were overcome. The result is then used to construct the product of an arbitrary family of probability measures.
Results
Lean/Mathlib formalizations of the Ionescu-Tulcea theorem and of the infinite product of probability measures.