Henstock-Kurzweil-Pfadintegral in der Finanzmathematik: Eine computerverifizierte Bewertung von europäischen Optionen und Barriere-Optionen

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

Yury Berdinsky and Alexander Ushakov ()
Additional contact information
Yury Berdinsky: SPBU - Saint Petersburg State University
Alexander Ushakov: SPBU - Saint Petersburg State University, NIF - V.A. Fock Institute of Physics - SPbU - St Petersburg State University

Working Papers from HAL

Abstract: Wir wenden den in früheren Teilen dieses Programms entwickelten Henstock-Kurzweil-(HK)-Pfadintegral-Apparat mit Gauß-Kern auf die erste große Anwendung außerhalb der Quantenmechanik an: die Black-Scholes-Formel zur Bewertung europäischer Optionen. Unter dem risikoneutralen Maß ist der Log-Preis x_t = log S_t eine Brownsche Bewegung mit Drift ν = r − σ²/2 und Volatilität σ > 0; seine Übergangsdichte ist der Gauß-Kern mit Drift: G_t(x,y) = (2πσ²t)^(−1/2) exp(−(y − x − νt)²/(2σ²t)), t > 0. Wir präsentieren eine vollständige, computerverifizierte Lean 4 / Mathlib-Formalisierung der Konstruktion: - das Chapman-Kolmogorow-(Halbgruppen)-Gesetz: ∫_ℝ G_s(x,z) G_t(z,y) dz = G_{s+t}(x,y); - die Tatsache, dass G_t eine Wahrscheinlichkeitsdichte ist; - die starke Stetigkeit des Evolutionsoperators (P_t ψ)(x) = ∫_ℝ G_t(x,y) ψ(y) dy; - und den geschlossenen Preis einer europäischen Kaufoption (Call), der direkt aus dem Kern gewonnen wird: C = e^(−rT) ∫_ℝ max(e^y − K, 0) G_T(log S_0, y) dy = S_0 N(d₁) − K e^(−rT) N(d₂), mit den Standardvariablen d₁, d₂ und N als Standardnormalverteilungsfunktion (CDF). Wir zeigen ferner, dass die Drift-Diffusions-Chernoff-Aufspaltung auf jeder Stufe exakt ist, was eine strenge pfadintegrale Ableitung liefert. Alle Aussagen in der begleitenden Datei HkBlackScholes.lean sind lückenlos ("sorry-free") und hängen nur von den Standardaxiomen propext, Classical.choice und Quot.sound ab.

Keywords: machine verification; barrier options; Lean 4; Mathlib; financial mathematics; risk-neutral valuation; Chapman–Kolmogorov equation; Girsanov theorem; Chernoff product; Wiener measure; real-time integration; stochastic differential equations; Cameron–Martin theorem; functional integration; Kuelbs–Steadman spaces; cylindrical measure; Itô calculus; digital option; European option pricing; Black–Scholes formula; path integral; gauge integral; Henstock–Kurzweil integral; noyau gaussien; formule de Black-Scholes; intégrale de chemin; intégrale de jauge de Henstock-Kurzweil; intégrale de jauge de Henstock-Kurzweil intégrale de chemin formule de Black-Scholes noyau gaussien (search for similar items in EconPapers)
Date: 2026-08-04
Note: View the original document on HAL open archive server: https://hal.science/hal-05711259v1
References: Add references at CitEc
Citations:

Downloads: (external link)
https://hal.science/hal-05711259v1/document (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:hal:wpaper:hal-05711259

DOI: 10.5281/zenodo.21600941

Access Statistics for this paper

More papers in Working Papers from HAL
Bibliographic data for series maintained by CCSD ().