Lean formalization of a Brownian motion
Our goal is to formalize Brownian motions in Lean using Mathlib. There are two main parts to this formalization:
-
develop the theory of Gaussian distributions and build a projective family of Gaussian distributions and define its projective limit by the Kolmogorov extension theorem,
-
prove the Kolmogorov-Chentsov continuity theorem.
For more information, see the project home page, in particular the blueprint.
The project is ongoing.