The Fundamental Theorem of Asset Pricing, Formalized in Lean 4
创建于 更新于
摘要
本文在 Lean 4 与 Mathlib 框架下，对“资产定价基本定理”给出三种设定的形式化证明：有限状态多期市场（Harrison–Pliska）、单期标量回报、以及单期多资产向量回报。核心结论是：若不存在套利，则存在一个与物理测度等价的等价鞅测度 Q，使贴现价格在 Q 下为鞅；反向方向则通过在各设定中给出明确构造来证明。有限状态通过几何的分离超平面实现无套利等价性，单期标量通过简单的密度变换构造 Q，d-资产情形通过对一个光滑凸势能的最小化获得 θ0，从而得到 Q 的密度 σ(⟨θ0, Y⟩) 的归一化形式。该方法避免了传统 Hahn–Banach、L0-闭性等非构造性依赖，且对冗余资产通过 gains kernel 自动吸收，不需要额外非冗余性假设。全文在 Mathlib 的经典公设下逐步证明，确保无 sorry 且可重复验证，标志着在证明性推导领域的一次重要进展 [page::0]。
