Brownian Motion
Abstract
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.
Notation
\(T\) denotes an index set (for a stochastic process).
\(\Omega \) is a measurable space. \(\mathbb {P}\) is the probability measure on \(\Omega \) and \(\mathbb {E}\) is the expectation operator with respect to \(\mathbb {P}\).
\(E, F\) are normed vector spaces. Most often \(F\) is a Banach space and \(E\) is a Hilbert space.