(Disclaimer: I'm worried that this question will appear lazy, but I did spend some time on it and am about to give up.)
In Mathlib, under probability, there are processes, filtrations and martingales. However, I cannot find Brownian motion. And there appears to be an ongoing discussion about probability spaces. Can someone please share any pointers that will help with formalizing this:
Let $(\Omega,F,P)$ be a probability space. For each $\omega \in \Omega$, suppose there is a continuous function $W(t)$ with $t \ge 0$ that satisfies $W(0) = 0$ and that depends on $\omega$. Then $W(t)$ is a Brownian motion if, for all $0 = t_0 \lt t_1 \lt \cdots \lt t_m$, the increments $D(t_i) = W(t_{i+1})−W(t_i)$ for $0 \le i \lt m$ are independent, and each is normally distributed with $\mathsf{E}[D(t_i)] = 0$ and $\mathsf{Var}[D(t_i)] = t_{i+1}−t_i$.
code. You can use$...$to write the LaTeX math. $\endgroup$