## Stream: new members

#### Patrick Massot (Oct 11 2019 at 12:53):

Hi @Vincent Beffara, welcome! You'll eligible for the Giry test: do you know what is the Giry monad?

#### Patrick Massot (Oct 11 2019 at 13:21):

Oh crap: he left. I hope it's not because of the Giry joke. @Vincent Beffara this was a joke about computer scientists who like to pretend they think probability theory is the study of the Giry monad, an arcane part of category theory. But you're very welcome to formalize actual probability theory!

#### Kevin Buzzard (Oct 11 2019 at 17:19):

I was emailed by a computer scientist from Harvard earlier this week, who sent me a preprint in statistical learning theory where they have formalised some basic results from this area in Lean. I took a look through the paper and the first thing I noticed was that @Koundinya Vajjha was a co-author (which probably explained the Lean) but also that they talk extensively about the Giry monad. So there really are people out there who know what it is (but I think none of the authors were mathematicians...)

#### Koundinya Vajjha (Oct 11 2019 at 17:29):

Yeah that preprint was an outgrowth of my internship at Oracle Labs. The computer scientist who emailed you was probably Jean-Baptiste Tristan?

#### Kevin Buzzard (Oct 11 2019 at 17:31):

Indeed! Is it posted online anywhere? I was pleasantly surprised to see Giry monads in there, for me and Patrick they are becoming a running joke, I have asked several mathematicians about them (including a Fields Medallist and another highly prestigious person) and none of them have ever heard of them!

#### Koundinya Vajjha (Oct 11 2019 at 17:32):

No it's not posted online yet! And the Giry monad is really quite pleasant. It's a pity they haven't heard of it.

#### Kevin Buzzard (Oct 11 2019 at 17:33):

I guess many mathematicians haven't even heard of filters ;-)

#### Kevin Buzzard (Oct 11 2019 at 17:33):

but a lot more of them haven't heard of monads.

#### Patrick Massot (Oct 11 2019 at 17:33):

At least we hear the word

#### Koundinya Vajjha (Oct 11 2019 at 17:35):

Yeah I consider myself a mathematician (who formalizes) and it's really when you see the Giry monad in action to construct product measures, say, you realize how cool it is. :-)

#### Kevin Buzzard (Oct 11 2019 at 17:35):

Maybe I'm saying it wrong. How do you pronounce "Giry"?

#### Sebastien Gouezel (Oct 11 2019 at 17:52):

I don't think the Giry monad is relevant to mainstream mathematicians in probability theory, as we most often work with infinite sequences of random variables. For instance, the first theorem in a probability course is the law of large numbers, saying that if X_n is a sequence of integrable independent identically distributed random variables, then (X_0+...+X_{n-1})/n converges almost surely to the average of X_0. I was under the impression that this can not be conveniently expressed with the Giry monad, but I would be happy to be corrected if I am wrong!

#### Johan Commelin (Oct 11 2019 at 17:54):

Note that the law of large numbers is one of the 5 remaining theorems on Freek100.

#### Koundinya Vajjha (Oct 11 2019 at 17:55):

Johannes used to talk about the Ionescu-Tulcea theorem which allows one to construct Markov processes using the Giry monad for probability measures.

#### Sebastien Gouezel (Oct 11 2019 at 18:59):

Note that the law of large numbers is one of the 5 remaining theorems on Freek100.

Well, I have proved in Isabelle the Birkhoff theorem, which is a far reaching generalization of the law of large numbers...

#### Sebastien Gouezel (Oct 11 2019 at 19:01):

Johannes used to talk about the Ionescu-Tulcea theorem which allows one to construct Markov processes using the Giry monad for probability measures.

If you want to look at a Markov process in finite time, the Giry monad is perfect (and essentially designed for this, I would say). But if you want a theorem talking about the process over all times, I don't think it is the right tool.

#### Floris van Doorn (Oct 11 2019 at 19:04):

How much work would it be to specialize the Birkhoff theorem to the law of large numbers?

#### Sebastien Gouezel (Oct 11 2019 at 19:42):

Not that much. But given all the theory that Johannes and Jeremy have already developed to prove the (much harder) central limit theorem, it would probably be even quicker to formalize one of the classical proofs of the law of large numbers -- and this would just be an exercise, really.

#### Vincent Beffara (Oct 11 2019 at 20:44):

I had never heard of the Giri monad. And now that I had a quick look at the page, I am not really less perplexed than before

#### Vincent Beffara (Oct 11 2019 at 20:45):

To me randomness feels more like the IO monad from Haskell, an unknowable process that ends up producing a real number at the end ...

#### Patrick Massot (Oct 11 2019 at 20:50):

If you know monads from Haskell you're half way through understanding that Giry stuff.

#### Patrick Massot (Oct 11 2019 at 20:50):

And soon you'll be able to do probability theory the right way :lol:

#### Mario Carneiro (Oct 12 2019 at 04:56):

I think that the Giry monad is essentially the formalization of your intuition, @Vincent Beffara

#### Mario Carneiro (Oct 12 2019 at 04:58):

I'm not sure the definition itself provides much knowledge, but the idea that you can view random variables as a monad makes it really clear how to use them in diverse ways

#### Floris van Doorn (Oct 14 2019 at 19:23):

Not that much. But given all the theory that Johannes and Jeremy have already developed to prove the (much harder) central limit theorem, it would probably be even quicker to formalize one of the classical proofs of the law of large numbers -- and this would just be an exercise, really.

Is it really that easy? If we're talking about the strong law of large numbers, I believe the proof is quite tricky. According to Terry Tao:

The weak law is easy to prove, but the strong law (which of course implies the weak law, by Egoroff’s theorem) is more subtle, and in fact the proof of this law (assuming just finiteness of the first moment) usually only appears in advanced graduate texts.

https://terrytao.wordpress.com/2008/06/18/the-strong-law-of-large-numbers/

#### Sebastien Gouezel (Oct 14 2019 at 19:36):

No, the strong law of large numbers is not easy, but it is not hard either. The proof takes less than two pages in standard textbooks (for instance Billingsley, probability and measure), and all the supporting material is already formalized, so I am pretty sure I could do it in a few hours, say.

Last updated: May 14 2021 at 06:16 UTC