6 Brownian motion
6.1 Stochastic process with continuous paths
Let \(\Omega = \mathbb {R}^{\mathbb {R}_+}\) and consider the probability space \((\Omega , P_B)\) (where \(P_B\) is the measure defined in Definition 4.10). The identity on that space is a function \(\Omega \to \mathbb {R}_+ \to \mathbb {R}\). We reorder the arguments to define a stochastic process \(X : \mathbb {R}_+ \to \Omega \to \mathbb {R}\), which we call the pre-Brownian process.
For any \(t_1, \ldots , t_n \in \mathbb {R}_+\), the distribution of \((X_{t_1}, \ldots , X_{t_n})\) is given by a finite-dimensional distribution of \(P_B\), and therefore is Gaussian.
Let \(X\) be the pre-Brownian process of Definition 6.1. Then, for all \(s, t \in \mathbb {R}_+\), the random variable \(X_t - X_s\) is a Gaussian random variable with mean \(0\) and variance \(|t - s|\).
The map
is a continuous linear map, and \((X_s, X_t)\) is Gaussian by Lemma 6.2, therefore \(X_t - X_s\) is Gaussian by Lemma 3.7. By definition of \(P_B\), we have
and
Therefore \(X_t - X_s\) is Gaussian with mean \(0\) and variance \(|t - s|\).
The pre-Brownian process \(X\) of Definition 6.1 satisfies the Kolmogorov condition for exponents \((2n,n)\) with constant \((2n - 1)!!\) for all \(n \in \mathbb {N}\). That is, for all \(s, t \in \mathbb {R}_+\), we have
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 \(\gamma \in (0, 1/2)\). We call \(B\) the Brownian motion on \(\mathbb {R}_+\).
The Brownian motion is a Gaussian process.
The paths of the Brownian motion are locally Hölder continuous of all orders \(\gamma \in (0, 1/2)\).
Consider the cover of \(\mathbb {R}_+\) given by \(T_n := [0, n + 1)\). By Lemma 5.82, this cover has bounded covering numbers with exponent \(1\). Moreover, by Lemma 6.4, the pre-Brownian process satisfies the Kolmogorov condition with exponents \((2n + 4, n + 2)\) for all \(n \in \mathbb {N}\). In particular, for all \(n \in \mathbb {N}\), \(2n + 4 {\gt} 1\). Applying Theorem 5.84 we deduce that the modification used in Definition 6.5 has locally Hölder continuous paths for all orders \(\gamma \in (0, \sup _n (n + 1) / (2n + 4))\). Clearly for all \(n \in \mathbb {N}\) we have \((n + 1) / (2n + 4) \leqslant 2\), and this quantity tends to \(2\) as \(n\) goes to infinity. Therefore the Brownian motion has Hölder continuous paths of order \(\gamma \) for all \(\gamma \in (0, 1 / 2)\).
The paths of the Brownian motion are continuous.
The paths are \(1/4\)-Hölder continuous by Lemma 6.7 because \(0 {\lt} 1/4 {\lt} 1/2\), therefore they are continuous.
For \(t \in \mathbb {R}_+\), the law of \(B_t\) (the Brownian motion at time \(t\)) is the real Gaussian measure \(\mathcal{N}(0,t)\).
The Brownian motion \(B\) is a modification of the pre-Brownian process, and therefore has same finite dimensional distributions. By Definition 4.10, \(B_t\) has law \(\mathcal{N}(0,t)\).
For \(s, t \in \mathbb {R}_+\), the law of \(B_t - B_s\) is the real Gaussian measure \(\mathcal{N}(0,\vert t - s \vert )\).
The Brownian motion \(B\) is a modification of the pre-Brownian process, and therefore has same finite dimensional distributions. By Lemma 6.3, \(B_t - B_s\) has law \(\mathcal{N}(0,\vert t - s \vert )\).
We say that a stochastic process \(X : T \to \Omega \to E\) has independent increments if for all \(t_1, \ldots , t_n \in T\) with \(t_1 \le t_2 \le \cdots \le t_n\), the random variables \(X_{t_2} - X_{t_1}, X_{t_3} - X_{t_2}, \ldots , X_{t_n} - X_{t_{n-1}}\) are independent.
The Brownian motion has independent increments.
Let \(t_1 \le t_2 \le \ldots \le t_n\) be \(n\) times in \(\mathbb {R}_+\). Then \((B_{t_2} - B_{t_1}, B_{t_3} - B_{t_2}, \ldots , B_{t_n} - B_{t_{n-1}})\) is a linear transformation of \((B_{t_1}, \ldots , B_{t_n})\), hence it is Gaussian. We can compute its mean (which is \(0\)) and its covariance matrix. The covariance matrix is diagonal, which means the the random variables are uncorrelated. Because they are jointly Gaussian, this implies that they are independent.
6.2 Wiener measure on the continuous functions
We want to turn the Brownian motion into a measure on the continuous functions \(C(\mathbb {R}_+, \mathbb {R})\) with the Borel sigma-algebra generated by the compact-open topology.
The pushforward of the measure \(P_B\) of Definition 4.10 by the Brownian motion \(B\) is a measure on the continuous functions on \(\mathbb {R}^{\mathbb {R}_+}\), with the sigma-algebra induced by the product sigma-algebra on \(\mathbb {R}^{\mathbb {R}_+}\).
Lean remark: the auxiliary Wiener measure is a measure on the subtype {f // Continuous f}. This is not the same type as \(C(\mathbb {R}_+, \mathbb {R})\).
The Borel sigma-algebra on \(C(\mathbb {R}_+, \mathbb {R})\) coming from the compact-open topology is equal to the smallest sigma-algebra for which the evaluation maps \(f \mapsto f(t)\) are measurable for every \(t \in \mathbb {R}_+\).
We prove that this holds for \(C(X, Y)\) as long as \(X\) and \(Y\) are second-countable topological spaces endowed with their Borel sigma-algebra, \(X\) is locally compact (i.e. each point of \(X\) has a basis of compact neighbourhoods), and \(Y\) is regular (i.e. for any \(C \subseteq Y\) closed and \(y \notin C\), there exist disjoint open subsets \(U, V \subseteq Y\) such that \(C \subseteq U\) and \(y \in V\)). The proof is taken from this stackexchange question.
We denote by \(\mathcal{T}_1\) and \(\mathcal{T}_2\) the two sigma-algebras.
First of all, the evaluation maps are continuous for the compact-open topology, and therefore measurable for \(\mathcal{T}_1\). We deduce that \(\mathcal{T}_2 \subseteq \mathcal{T}_1\).
Let us turn to the converse direction. For any \(A \subseteq X\) and \(B \subseteq Y\), denote
The compact-open topology is generated by the sets of the form \(M(K, U)\), for \(K\) compact and \(U\) open. Because \(X\) and \(Y\) are second-countable and \(X\) is locally compact, \(C(X, Y)\) is second-countable. Therefore it is enough to show that for any \(K\) compact and \(U\) open, \(M(K, U) \in \mathcal{T}_2\). We now fix \(K\) and \(U\).
Consider \((V_n)_{n \in \mathbb {N}}\) a countable family of subsets of \(Y\) which generates the topology (it exists by second-countability assumption). Clearly we have that
Conversely, consider \(y \in U\). Because \(Y\) is regular, the set of \(\overline{V_n}\) such that \(y \in V_n\) is a basis of neighbourhoods of \(y\). Indeed, consider \(A\) an open neighbourhood of \(y\). Then \(A^c\) is a closed set which does not contain \(y\). Therefore there exist disjoint open sets \(B\) and \(C\) such that \(y \in B\) and \(A^c \subseteq C\). There exists \(n \in \mathbb {N}\) such that \(x \in V_n \subseteq B\). Therefore \(V_n \subseteq C^c\), so \(\overline{V_n} \subseteq C^c \subseteq A\), and we are done. This proves that we have in fact
Consider now \(f \in M(K, U)\). We then have
Because \(K\) is compact and \(f\) is continuous, \(f(K)\) is compact. But each \(V_n\) is open, so there exists a finite set \(\hat{f}\) of natural integers such that for any \(n \in \hat{f}\), \(\overline{V_n} \subseteq U\), and
Conversely, if there exists a finite set \(\hat{f}\) such that for any \(n \in \hat{f}\), \(\overline{V_n} \subseteq U\), and
then \(f(K) \subseteq U\). We can therefore write that
This is a countable union, so we just have to prove that each term is measurable.
We now fix a finite set \(I\) as in the union above. Because \(X\) is second countable, there exists \(Q\) a countable dense subset of \(K\). For any \(f\) continuous, because \(Q\) is dense and \(\bigcup _{i \in I} \overline{V_i}\) is closed, we have
In other words, \(M\left(K, \bigcup _{i \in I} \overline{V_i}\right) = M\left(Q, \bigcup _{i \in I} \overline{V_i}\right)\). We can write
and it is enough to show that each term in the intersection is measurable. Because \(\bigcup _{i \in I} \overline{V_i}\) is closed, it is measurable. It therefore remains to prove that \(f \mapsto f(q)\) is measurable for all \(q \in Q\), but this is obvious from the definition of \(\mathcal{T}_2\). This concludes the proof.
The identity is a measurable equivalence between the continuous functions of \(\mathbb {R}^{\mathbb {R}_+}\) with the subset sigma-algebra obtained from the product sigma-algebra, and \(C(\mathbb {R}_+, \mathbb {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.
The Wiener measure on \(C(\mathbb {R}_+, \mathbb {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.