AI 中文总结
该研究将Henstock–Kurzweil gauge积分应用于Black–Scholes期权定价模型，在Lean 4 / Mathlib中机器验证了欧式期权等定价公式，证明其与经典Ito微积分兼容。
AI 中文摘要
我们将Henstock–Kurzweil（HK） gauge积分应用于期权定价的Black–Scholes模型，无需随机微积分，直接从高斯柱核得到欧式看涨期权价格。在风险中性测度下，对数价格是漂移项ν = r - σ²/2的布朗运动，其转移密度为高斯核G_t(x,y) = (2πσ²t)^{-1/2}exp(-(y - x - νt)²/(2σ²t))。我们在Lean 4 / Mathlib中对以下内容进行了机器检查的形式化：Chapman–Kolmogorov（半群）性质、G_t是概率密度的事实、定价算子的强连续性、带标准正态CDF N的闭式价格C = S₀N(d₁) - Ke^{-rT}N(d₂)，以及漂移-扩散Chernoff分解在每一层的精确性。整个证明无“sorry”，仅依赖propext、https://、https://。数字期权和障碍期权被作为进一步示例处理，说明了该方法的普适性，且我们证明了该构造在连续极限下与经典Ito微积分兼容。
英文摘要
We apply the Henstock--Kurzweil (HK) gauge integral to the Black--Scholes model of option pricing and obtain the European call price directly from a Gaussian cylindrical kernel, without stochastic calculus. Under the risk- neutral measure, the log-price is a Brownian motion with drift nu = r - sigma^2/2. Its transition density is the Gaussian kernel G_t(x,y) = (2 pi sigma^2 t)^{-1/2} exp( - (y - x - nu t)^2 / (2 sigma^2 t) ). We give a machine-checked formalization in Lean 4 / Mathlib of the following: the Chapman--Kolmogorov (semigroup) property, the fact that G_t is a probability density, strong continuity of the pricing operator, the closed-form price C = S_0 N(d_1) - K e^{-rT} N(d_2) with the standard normal CDF N, and the exactness of the drift--diffusion Chernoff splitting at every level. The entire proof is "sorry"-free and depends only on propext, Classical.choice, and Quot.sound. Digital and barrier options are treated as further examples, illustrating the universality of the method, and we show that the construction is compatible with the classical Ito calculus in the continuum limit.
