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]

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.