4 papers
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…
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 bu…
A Formally Verified Library of Mathematical Finance in Lean 4
Raphael Coelho
We describe a library of mathematical finance built in the Lean~4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than three hundred sorry-free…
Three-Currency HJM for Brazilian Credit Markets
Raphael Coelho
This paper develops a three-currency Heath-Jarrow-Morton framework in which corporate credit is treated as a separate economy, connected to the nominal and real economies through s…