Brownian Motion

Abstract
Outline
Notation
1 Auxiliary results
2 Characteristic functions
3 Gaussian distributions ▶
- 3.1 Gaussian measures ▶
- 3.2 Gaussian processes
4 Projective family of the Brownian motion ▶
- 4.1 Kolmogorov extension theorem
- 4.2 Projective family of Gaussian measures ▶
5 Kolmogorov-Chentsov Theorem ▶
Dependency graph

1 Auxiliary results

Mathlib contains a definition of a product measure indexed by a finite set, but does not have lemmas about integrals against such a measure.