Isabelle/HOL 中鞅的形式化

本论文给出了使用 Isabelle/HOL 在任意 Banach 空间中对鞅的形式化。我们首先考察了知名证明库中的形式化，并将条件期望算子的定义从实数推广到一般 Banach 空间。Isabelle 库当前对条件期望的形式化仅限于实值函数。为克服此局限，我们利用测度论论证，通过简单函数的适当极限在 Banach 空间中构造条件期望。随后，我们定义随机过程，并利用适当的 locale 定义引入适应过程、渐进可测过程与可预测过程的概念。我们展示了关系 $$\text{adapted} \supseteq \text{progressive} \supseteq \text{predictable}$$ 此外，我们证明当指标集离散时，渐进可测性与适应性等价。我们特别关注离散时间下的可预测过程，证明 $(X_n)_{n \in \mathbb{N}}$ 可预测当且仅当 $(X_{n + 1})_{n \in \mathbb{N}}$ 适应。我们严格定义了鞅、下鞅与上鞅，并给出其首批推论与系。离散时间鞅在形式化中受到特别关注。在形式化的每一步中，我们广泛使用了 Isabelle 强大的 locale 系统。该形式化进一步通过将 Bochner 积分中的概念从实数推广到配备第二可数拓扑的任意 Banach 空间而做出贡献。我们引入了 Banach 空间上可积简单函数的归纳格式。此外，我们形式化了一个称为“平均定理”的有力结果，其使我们能证明 Banach 空间中密度的唯一性。