A Machine-Checked It\^o Calculus for Brownian Motion

Abstract

We develop the It\^o calculus of Brownian motion, machine-checked in Lean~4 over Mathlib and the \lean{BrownianMotion} package. On a bounded interval $[0,T]$ the It\^o integral is built as a Hilbert-space isometry, from a predictable-rectangle $\pi$-system through the density of simple adapted processes. Realized as a process, it is a continuous $L^2$ martingale. One structural identity drives this: the integral at time $t$ is the conditional-expectation projection of its terminal value onto $\F_t$, and from it adaptedness, the martingale property, the contraction bound, and both the terminal and time-indexed It\^o isometries follow as corollaries. On this integral we prove It\^o's formula for $C^3$ functions with bounded derivatives, including the time-dependent form $df = f_x\,dB + (f_t + \tfrac12 f_{xx})\,dt$, by a discrete-to-continuous argument through weighted quadratic variation with explicit $L^2$ remainder bounds. We then pass from the $L^2$ 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\^o integral as a continuous local martingale on all of $\R_{\ge 0}$, the form it takes in the classical theory. To our knowledge these are the first machine-checked constructions of the It\^o integral and of It\^o's formula in any proof assistant, and the first to reach a pathwise-continuous local martingale. The boundary is explicit. The $L^2$ integral and It\^o's formula are developed on $[0,T]$ with bounded-derivative integrands; the unrestricted $C^2$ formula, integrators beyond brownian motion, and right-continuity of the filtration lie outside the development.