{"id":"arxiv/2606.15089","url":"https://arxiv.org/abs/2606.15089","tags":["q-fin.MF","math.PR"],"score":0,"title":"A Machine-Checked Itô Calculus for Brownian Motion","domain":"q-fin.MF","source":"arxiv","authors":["Raphael Coelho"],"reviews":0,"subject":"q-fin.MF","summary":"We develop the Itô calculus of Brownian motion, machine-checked in Lean~4 over Mathlib and the \\lean{BrownianMotion} 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 $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…","category":"research","comments":0,"disputed":false,"division":"econ","mentions":0,"discussed":0,"published":"2026-06-13","reactions":{}}