A Formalization of the Ionescu-Tulcea Theorem in Mathlib
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914400823148544 |
|---|---|
| author | Marion, Etienne |
| author_facet | Marion, Etienne |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_18616 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formalization of the Ionescu-Tulcea Theorem in Mathlib Marion, Etienne Probability Digital Libraries 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. |
| title | A Formalization of the Ionescu-Tulcea Theorem in Mathlib |
| topic | Probability Digital Libraries |
| url | https://arxiv.org/abs/2506.18616 |