Abstract

Our goal is to formalize Brownian motions (or \(\mathbb R^d\)-valued Gaussian processes) in some generality using Mathlib.

Outline

There are three main parts to this formalization:

• develop the theory of Gaussian distributions,

• 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.