Brownian Motion

6 Brownian motion

6.1 Stochastic process with continuous paths

Definition 6.1 pre-Brownian process
#

Let Ω=RR+ and consider the probability space (Ω,PB) (where PB is the measure defined in Definition 4.10). The identity on that space is a function ΩR+R. We reorder the arguments to define a stochastic process X:R+ΩR, which we call the pre-Brownian process.

The pre-Brownian process X of Definition 6.1 is a Gaussian process.

Proof
Lemma 6.3

Let X be the pre-Brownian process of Definition 6.1. Then, for all s,tR+, the random variable XtXs is a Gaussian random variable with mean 0 and variance |ts|.

Proof

The pre-Brownian process X of Definition 6.1 satisfies the Kolmogorov condition for exponents (2n,n) with constant (2n1)!! for all nN. That is, for all s,tR+, we have

E[|XtXs|2n](2n1)!!|ts|n.
Proof
Definition 6.5 Brownian motion

By Theorem 5.84, there exists a modification B of the pre-Brownian process such that all the paths of B are Hölder continuous of all orders γ(0,1/2). We call B the Brownian motion on R+.

The Brownian motion is a Gaussian process.

Proof

The paths of the Brownian motion are locally Hölder continuous of all orders γ(0,1/2).

Proof
Lemma 6.8

The paths of the Brownian motion are continuous.

Proof
Lemma 6.9

For tR+, the law of Bt (the Brownian motion at time t) is the real Gaussian measure N(0,t).

Proof
Lemma 6.10

For s,tR+, the law of BtBs is the real Gaussian measure N(0,|ts|).

Proof
Definition 6.11
#

We say that a stochastic process X:TΩE has independent increments if for all t1,,tnT with t1t2tn, the random variables Xt2Xt1,Xt3Xt2,,XtnXtn1 are independent.

Lemma 6.12

The Brownian motion has independent increments.

Proof

6.2 Wiener measure on the continuous functions

We want to turn the Brownian motion into a measure on the continuous functions C(R+,R) with the Borel sigma-algebra generated by the compact-open topology.

Definition 6.13 Auxiliary Wiener measure

The pushforward of the measure PB of Definition 4.10 by the Brownian motion B is a measure on the continuous functions on RR+, with the sigma-algebra induced by the product sigma-algebra on RR+.

Lean remark: the auxiliary Wiener measure is a measure on the subtype {f // Continuous f}. This is not the same type as C(R+,R).

Theorem 6.14

The Borel sigma-algebra on C(R+,R) coming from the compact-open topology is equal to the smallest sigma-algebra for which the evaluation maps ff(t) are measurable for every tR+.

Proof
Definition 6.15

The identity is a measurable equivalence between the continuous functions of RR+ with the subset sigma-algebra obtained from the product sigma-algebra, and C(R+,R) with the Borel sigma-algebra coming from the compact-open topology.

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.

Definition 6.16 Wiener measure

The Wiener measure on C(R+,R) with the Borel sigma-algebra is the map of the auxiliary Wiener measure by the measurable equivalence of definition 6.15.

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.