stochastic process

Stream: new members

[Joshua Banks]

Hi I am looking to define some basic properties of Brownian motion in mathlib, I am new to lean and mathlib and was wondering if anyone had an idea of how to represent or define a stochastic process in lean across some measurable space. I have defined a probability space and a random variable in that space. Any help or guidance is appropriated.

[Yaël Dillies]

Hey! When you say you've defined a probability space, do you mean you defined a specific probability space using the existing docs#measure_theory.measure_space, or you defined what it meant to be a probability space?

[Yaël Dillies]

cc @Jason KY. who is one of the main forces behind the push for probability in mathlib.

[Joshua Banks]

yes sorry I should have clarified, I have just used existing documentation, I'm very new and just trying to understand how to represent and define certain concepts. Thanks for your quick response.

[Yaël Dillies]

In my project LeanCamCombi, we defined sequences of Bernoulli random variables here. This is more or less what you want for a stochastic process.

[Jason KY.]

We currently have a bit of martingale theory (optional stopping, martingale convergence, etc.. c.f. here) mostly for discrete time martingales. We don't have the Gaussian yet so you will need to define that if you want to define Brownian motions. We are lacking a lot of tools for continuous time stochastic processes (e.g. previsibility, cadlag...) so it would be a good exercise to define those also

[Kevin Buzzard]

Just to remark that it took me a long time to understand what people meant by "the Gaussian". David Loeffler just seems to have proved that e^{-x^2/2} is its own Fourier transform, and I would have said that this was "the Gaussian" but my understanding is that other people mean far more general things by this phrase.