Papers With

← All papers
First page of A Formalization of the Ionescu-Tulcea Theorem in Mathlib

A Formalization of the Ionescu-Tulcea Theorem in Mathlib

Etienne Marion

math.PR Jun 23, 2025 · v1
formalization mathlib probability
Read PDF arXiv abstract
TL;DR
Formalizes the Ionescu-Tulcea theorem in Lean using Mathlib and builds the product of an arbitrary family of probability measures.
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, which establishes the existence of a probability measure on the space of trajectories of a Markov chain, had not been formalized in a proof assistant. Formalizing it presents challenges in handling measure-theoretic constructions over infinite product spaces.

Approach

The theorem is formalized in Lean using Mathlib. The authors present the mathematical proof and describe the difficulties encountered during formalization and how they were overcome. The formalization is then extended to construct the product of an arbitrary family of probability measures.

Results

The Ionescu-Tulcea theorem is fully formalized in Lean/Mathlib, along with the construction of the product of an arbitrary family of probability measures built on top of it.