Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Formalization of the Ionescu-Tulcea Theorem in Mathlib

Etienne Marion

TL;DR

The paper formalizes the Ionescu-Tulcea theorem in Lean/Mathlib, proving the existence of a kernel that describes infinite trajectories of a Markov process from a sequence of finite-step kernels. It navigates deep formalization challenges posed by dependent types and multi-kernel composition, introducing generalized constructions (η_{a,b}, traj) and marginals to build a projective-limit kernel ξ_a via Carathéodory extension. The work also demonstrates how the resulting framework yields a robust construction of the product of an arbitrary family of probability measures through countable and infinite product measures. Together, these results provide a natural and usable formal toolkit for modeling infinite stochastic processes in a proof assistant. The effort advances formal probability by aligning mathematical concepts with Lean/Mathlib’s API, facilitating future formalizations of complex stochastic constructions like Brownian motion.

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.

A Formalization of the Ionescu-Tulcea Theorem in Mathlib

TL;DR

The paper formalizes the Ionescu-Tulcea theorem in Lean/Mathlib, proving the existence of a kernel that describes infinite trajectories of a Markov process from a sequence of finite-step kernels. It navigates deep formalization challenges posed by dependent types and multi-kernel composition, introducing generalized constructions (η_{a,b}, traj) and marginals to build a projective-limit kernel ξ_a via Carathéodory extension. The work also demonstrates how the resulting framework yields a robust construction of the product of an arbitrary family of probability measures through countable and infinite product measures. Together, these results provide a natural and usable formal toolkit for modeling infinite stochastic processes in a proof assistant. The effort advances formal probability by aligning mathematical concepts with Lean/Mathlib’s API, facilitating future formalizations of complex stochastic constructions like Brownian motion.

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.

Paper Structure

This paper contains 11 sections, 12 theorems, 31 equations.

Table of Contents

  1. Introduction
  2. Mathematical aspects
  3. Preliminaries on probability theory
  4. Statement and proof of the theorem
  5. Formalization of the theorem
  6. Composition of kernels
  7. Projective family of measure
  8. Integrating against $\eta$
  9. The resulting kernel
  10. Infinite product of probability measures
  11. Conclusion

Key Result

Lemma 2.4

Let $\mu$ an additive content over $S$. To prove that $\mu$ is $\sigma$-sub-additive, it is enough to show that it is continuous at the empty set, namely that if $(A_n)_{n\in\mathbb{N}}$ is a non-increasing (for the inclusion of sets) family of elements of $S$ with empty intersection, then $\mu(A_n)

Theorems & Definitions (27)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Lemma 2.4
  • Theorem 2.5: Carathéodory's extension theorem
  • Definition 2.7
  • Definition 2.8
  • Definition 2.9
  • Definition 2.10
  • Theorem 2.11: Ionescu-Tulcea
  • ...and 17 more