2026/06/13 by Raphael Coelho · 1 voice
Economics, Econometrics and Finance · Mathematics · #q-fin.MF #math.PR
arxiv published 2026/06/13 · arxiv updated 2026/06/27
We develop the Itô calculus of Brownian motion, machine-checked in Lean~4 over Mathlib and the \leanBrownianMotion package. On a bounded interval [0,T] the Itô integral is built as a Hilbert-space isometry, from a predictable-rectangle π-system through the density of simple adapted processes. Realized as a process, it is a continuous L2 martingale. One structural identity drives this: the integral at time t is the conditional-expectation projection of its terminal value onto \Ft, and from it adaptedness, the martingale property, the contraction bound, and both the terminal and time-indexed Itô isometries follow as corollaries. On this integral we prove Itô's formula for C3 functions with bounded derivatives, including the time-dependent form df = fx dB + (ft + \tfrac12 fxx) dt, by a discrete-to-continuous argument through weighted quadratic variation with explicit L2 remainder bounds. We then pass from the L2 theory to the pathwise. The integral process has an almost-surely continuous modification, and its everywhere-continuous representative is a local martingale for the null-augmented Brownian filtration; gluing the bounded-horizon representatives along the half-line yields the Itô integral as a continuous local martingale on all of \R≥ 0, the form it takes in the classical theory. To our knowledge these are the first machine-checked constructions of the Itô integral and of Itô's formula in any proof assistant, and the first to reach a pathwise-continuous local martingale. The boundary is explicit. The L2 integral and Itô's formula are developed on [0,T] with bounded-derivative integrands; the unrestricted C2 formula, integrators beyond brownian motion, and right-continuity of the filtration lie outside the development.