Examples of using probability theory in Lean

Stream: new members

[Ching-Tsun Chou]

Are there good examples of using probability theory in Lean? At present I am more interested in examples of using probability theory than developing probability theory. Elementary examples involving discrete probabilities will do. Thanks in advance!

[Zhang Qinchuan]

There is an official blog about probability : https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/

[Ching-Tsun Chou]

Yes, I am aware of that blog post. Thanks!

[Ching-Tsun Chou]

I want to see some examples of Lean's probability theory in action.

[Yaël Dillies]

If you know the Marcinkiewicz-Zygmund inequality, here is a proof of it for discrete uniform iid random variables using no probability theory: https://github.com/YaelDillies/LeanAPAP/blob/master/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

[Yaël Dillies]

Warning: it wasn't written for someone else to read