Write Permission and Status of Probability Theory

Stream: mathlib4

[Matteo Vilucchio]

Hello to everyone, I am Matteo and I am interested in learning LEAN to add the basic concepts of Probability Theory to mathlib.
Following the guide, I am asking the write permission.

Also I am interested if there are other people interested in formalising the Probability Theory.

[Rémy Degenne]

Welcome! What kind of results do you want to PR to Mathlib?

[Geoffrey Irving]

I have some finitely supported probability theory formalized as part of https://github.com/girving/debate.

[Matteo Vilucchio]

@Rémy Degenne I was looking to arrive at the central limit theorem for iid variables as a start. I saw that it is still not done from here https://leanprover-community.github.io/undergrad_todo.html

[Rémy Degenne]

Great! What is your github username? That's needed to invite you to the repository.

[Matteo Vilucchio]

My username on Github is mvilucchio

[Rémy Degenne]

You should have received an invitation.