Formalization of a Brownian motion and of stochastic integrals in Lean

1 Brownian motion

Overview

This part of the blueprint is a guide to the formalization of a standard Brownian motion in Lean using Mathlib. There are two main parts to this formalization:

  • a development of the theory of Gaussian distributions, the construction of a projective family of Gaussian distributions and its projective limit by the Kolmogorov extension theorem,

  • a proof of a Kolmogorov-Chentsov continuity theorem, following [ .

Putting the two sides together, we then build a stochastic process that fits the definition of a Brownian motion on the real line.

Status The formalization is complete.

Formalization authors Rémy Degenne, Markus Himmel, David Ledvinka, Etienne Marion, Peter Pfaffelhuber.

With additional contributions from Jonas Bayer, Lorenzo Loccioli, Pietro Monticone, Alessio Rondelli and Jérémy Scanvic.