Statistics library for Lean

Stream: general

[Sev]

Hi, I'm fairly new to Lean and was just curious if there are any libraries that exist for doing proofs relating to statistics. So, random variables, independence, etc?

[Mario Carneiro]

not too much. We have a decent amount of measure theory but not very much is specialized to the probability setting

[Mario Carneiro]

that said, the best way to grow the library support is to have someone motivated to write it by some application

[Sev]

I see, thanks!