A Machine-Checked Itô Calculus for Brownian Motion
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2606.15089
curl -X POST /api/v1/records/arxiv/2606.15089/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.15089/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'