A Machine-Checked It\^o Calculus for Brownian Motion (opens in new tab)

We present a machine-checked development of the $L^2$ It\^o calculus of Brownian motion on a bounded time interval $[0,T]$, formalized in Lean 4 on top of Mathlib and the BrownianMotion package. The development contains: the construction of the It\^o integral as an isometry of Hilbert spaces, from a predictable-rectangle $\pi$-system through the density of simple adapted processes; the It\^o integral as a process, proved to be an $L^2$-continuou...