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.

翻译：我们描述了 Ionescu-Tulcea 定理的形式化过程，该定理证明了马尔可夫链轨迹空间上概率测度的存在性，这一工作是在 Lean 证明助手中利用集成库 Mathlib 完成的。我们首先给出一个数学证明，然后揭示在尝试形式化该定理时出现的困难及其克服方法。最后，我们以此为基础，进一步形式化了任意概率测度族乘积的构造。