Zulip Chat Archive
Stream: Brownian motion
Topic: If it looks like a duck...
Rémy Degenne (Jun 29 2025 at 14:36):
We will soon have a completely formalized definition of an object that we call Brownian motion on , and we have some of its properties. How do we make sure that it is actually a Brownian motion?
So what characterization should we use, and what properties are we missing for that characterization?
Rémy Degenne (Jun 29 2025 at 15:12):
It would be nice to show that our Brownian has independent increments.
Peter Pfaffelhuber (Jun 29 2025 at 19:19):
We know that for has a multinomial normal distribution with expectation 0 and covariance matrix . Let us write . By some theorem which we have already shown this means that as a linear transformation of a multinomial distribution is again multinomial norman with expectation 0 and covariance . This shows that and are uncorrelated, hence independent.
Peter Pfaffelhuber (Jun 29 2025 at 19:20):
For more than two timepoints it may be more involved...
Peter Pfaffelhuber (Jun 29 2025 at 19:23):
From the result on two timepoints, it should be straight-forward to show that Brownian Motion is a martingale:
Peter Pfaffelhuber (Jun 29 2025 at 19:27):
Also, , showing that is a martingale.
Etienne Marion (Jul 11 2025 at 13:41):
Update on this: In #134 (quite messy right now), I defined an IsBrownian X P predicate. It means that under P, X has the right finite-dimensional distributions, and X is almost-surely continuous. I managed to prove that an almost-surely continuous process with independent increments such that for any t, X t has law gaussianReal 0 t is Brownian in the sense of this predicate.
Rémy Degenne (Jul 12 2025 at 08:15):
Nice! Of course at some point we will want to know that independent increments and continuous paths imply that the process has Gaussian laws, such that those conditions are enough to be Brownian, but proving that fact requires the CLT, which we don't have yet.
Last updated: Dec 20 2025 at 21:32 UTC