A Machine-Checked Itô Calculus for Brownian Motion
创建于 更新于
摘要
本文在 Lean 4 之上、基于 Mathlib 与 BrownianMotion 包，对 Brownian motion 的 Itô 积分及 Itô 公式进行了机器可检验化的正式化工作。在区间 [0, T] 上，Itô 积分被构造成一个希尔伯特空间同构，通过可预测矩形 π 系统与简单自适应过程的密度论联系起来，最终延展为自洽的 L2 积分映射。作为一个随机过程，Itô 积分构成一个连续的 L2 Martingale，其核心结构恒等式是：对任意 t，(φ • B)t 等于其终值在 Ft 上的条件期望投影；由此得到自适应性、马尔科夫性、收缩性界以及端点与随时间的 Itô 等距性等推论。对于有界导数的 C3 函数，本文给出离散到连续的推导路径，并证明时间相关形式 df = fx dB + ( ft + 12 fxx) dt 的 Itô 公式，且给出明确的 L2 误差界限。随后再从 L2 理论自然过渡到路径意义，得到 Itô 积分的几乎处处连续修改及其在空集外的全局局部鞘表示，最终将有界区间的结果拼接到半直线上的连续局部鞘对象，使之成为经典理论中的全局对象。文中称这是首个在任意证明助手中完成的 Itô 积分与 Itô 公式的机器可检验化工作，且首次达到路径连续的局部鞘形式，明确给出发展边界：区间 [0, T] 的 L2 积分与有界导数的 Itô 公式；对无界导数、Beyond Brownian 的积分对象以及 filtration 的右连续性等未覆盖。整部工作约 7,900 行 Lean 代码，26 个模块，所有定理无困惑性错误，且所有头部结果的公理均由工具链强制对齐至 Mathlib 的经典默认值，并可从固定工具链复现。[page::1]
