Chebyshev's inequality

Stream: maths

[Koundinya Vajjha]

I'm working on some stuff and managed to prove the markov and chebyshev inequality. Is there any interest in adding these to mathlib? I ask this because I understand that the Bochner integral is on the way.

[Mario Carneiro]

Certainly. Let's get probability measures and probability theory

[Koundinya Vajjha]

I did have some elementary probability theory in a PR which was closed. I could try to chop it up a bit and resubmit. The main question there was if we wanted a probability measure which lands in nnreal or ennreal. What is the consensus on this now?

[Mario Carneiro]

what is your personal consensus on that? Sounds like you've already found an answer

[Koundinya Vajjha]

I did feel like almost everything goes through with ennreal and it's easier to work with those, but Johannes suggested a nnreal probability measure. He has more experience than I do so I'm not sure.

[Mario Carneiro]

I think there is probably a use for both, but if ennreal is easier to use then that's fine