Formalization of a Brownian motion and of stochastic integrals in Lean

Bibliography