A Formalization of the Ionescu-Tulcea Theorem in Mathlib

TL;DR

This paper details the formalization of the Ionescu-Tulcea theorem within the Lean proof assistant, demonstrating how to construct probability measures on Markov chain trajectories and product measures.

Contribution

It introduces a formal proof of the Ionescu-Tulcea theorem in Lean, including the construction of product measures, advancing formal probability theory.

Findings

Successful formalization of the Ionescu-Tulcea theorem in Lean

Development of methods to construct product probability measures

Overcoming formalization challenges in measure-theoretic proofs

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.