{"id":"palomar/PALOMAR-2026-09-30-000029","url":"https://github.com/savarin/lean-stochastic-calculus/tree/bde839683ba3cf1bf149355a40e9de9522babe92","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000029-v1.json","repo":"https://github.com/savarin/lean-stochastic-calculus","tags":["math.PR","q-fin.MF","msc:91G20","msc:60H10","msc:60H05","mathematical-finance","stochastic-calculus","lean-formalization"],"score":0,"title":"Black-Scholes pricing via Girsanov change of measure","trust":"high","domain":"math.PR","source":"palomar","authors":["Ezzeri Esa"],"reviews":0,"subject":"math.PR","summary":"Formal proof of the time-zero Black-Scholes formula for a European call on any strong solution of the geometric Brownian motion SDE, with positive initial price, strike, volatility and maturity, and constant drift and interest rate. The change of measure uses the constant-drift case of the general predictable (dynamic) Girsanov theorem. The discounted stopped asset is a martingale under one fixed terminal measure, and the call-payoff expectation equals the closed-form Black-Scholes expression.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true}