Henstock--Kurzweil Path Integral in Financial Mathematics: A Machine-Verified Pricing of European and Barrier Options

Alexander S. Ushakov and Yury N. Berdinsky

Papers from arXiv.org

Abstract: 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.

Date: 2026-07
References: Add references at CitEc
Citations:

Downloads: (external link)
https://arxiv.org/pdf/2608.19223 Latest version (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:arx:papers:2608.19223

Access Statistics for this paper

More papers in Papers from arXiv.org
Bibliographic data for series maintained by arXiv administrators ().