PreprintCC BY-NC 4.0HAL
A Formalization of the Ionescu-Tulcea Theorem in 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.
Related
- Sharp bounds in Ionescu--Wainger multiplier theorem for canonical fractions
- Formalization of Sullivan's No Wandering Domains Theorem in Lean
- Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
- Formalization of Landau damping in the Vlasov--Poisson equations in Lean
- A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
BibTeX
@misc{marion2026formalization,
title = {{A Formalization of the Ionescu-Tulcea Theorem in Mathlib}},
author = {Etienne Marion},
howpublished = {HAL},
year = {2026},
month = sep,
eprint = {2506.18616},
archivePrefix = {arXiv},
url = {https://hal.science/hal-05123438v7},
note = {CC BY-NC 4.0},
}
RIS
TY - UNPB
TI - A Formalization of the Ionescu-Tulcea Theorem in Mathlib
AU - Etienne Marion
PY - 2026
DA - 2026/09/21
PB - HAL
UR - https://hal.science/hal-05123438v7
AB - 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.
ER -