2 papers
q-fin.MF2026
The Fundamental Theorem of Asset Pricing, Formalized in Lean 4
Raphael Coelho
The Fundamental Theorem of Asset Pricing states that a market is free of arbitrage exactly when it admits an equivalent martingale measure. We formalize it in Lean 4 over Mathlib i…
q-fin.MF2026
A Machine-Checked Itô Calculus for Brownian Motion
Raphael Coelho
We develop the Itô calculus of Brownian motion, machine-checked in Lean~4 over Mathlib and the \lean{BrownianMotion} package. On a bounded interval the Itô integral is buil…