论文标题
Doob的Mathlib中Doob的Martingale Convergence定理的形式化
A Formalization of Doob's Martingale Convergence Theorems in mathlib
论文作者
论文摘要
我们介绍了Doob的Mathlib图书馆中Doob的Martingale Convergence定理的形式化，用于精益定理供体。这些定理提供的条件（子）martingales几乎在任何地方或$ l^1 $中汇合。为了使这些结果形式化，我们建立了Banach空间中有条件期望的定义，并发展了随机过程，停止时间和Martingales的理论。作为收敛定理的应用，我们还介绍了莱维广泛的Borel-Cantelli引理的形式化。这项关于Martingale理论的工作是Mathlib中概率理论的最初发展之一，它基于该库的各个部分，例如拓扑，分析和最重要的是衡量理论。
We present the formalization of Doob's martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingales converge, almost everywhere or in $L^1$. In order to formalize those results, we build a definition of the conditional expectation in Banach spaces and develop the theory of stochastic processes, stopping times and martingales. As an application of the convergence theorems, we also present the formalization of Lévy's generalized Borel-Cantelli lemma. This work on martingale theory is one of the first developments of probability theory in mathlib, and it builds upon diverse parts of that library such as topology, analysis and most importantly measure theory.
