6 Brownian motion
6.1 Stochastic process with continuous paths
Let
Let
The pre-Brownian process
By Theorem 5.84, there exists a modification
The Brownian motion is a Gaussian process.
The paths of the Brownian motion are locally Hölder continuous of all orders
The paths of the Brownian motion are continuous.
For
For
We say that a stochastic process
The Brownian motion has independent increments.
6.2 Wiener measure on the continuous functions
We want to turn the Brownian motion into a measure on the continuous functions
The pushforward of the measure
Lean remark: the auxiliary Wiener measure is a measure on the subtype {f // Continuous f}. This is not the same type as
The Borel sigma-algebra on
The identity is a measurable equivalence between the continuous functions of
Mathematically this says nothing more than the equality of sigma-algebras of Theorem 6.14 but in Lean we have two different types so we need an equivalence.
The Wiener measure on
TODO: add the main properties of the Brownian motion and the Wiener measure. We need to be able to tell that we have built the correct objects.