Stream: new members

Topic: stochastic process

Joshua Banks (Feb 02 2023 at 21:51):

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 (Feb 02 2023 at 21:56):

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 (Feb 02 2023 at 21:57):

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

Joshua Banks (Feb 02 2023 at 23:11):

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 (Feb 02 2023 at 23:14):

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. (Feb 03 2023 at 16:03):

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 (Feb 03 2023 at 16:43):

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.

Last updated: Dec 20 2023 at 11:08 UTC