Zulip Chat Archive

Stream: maths

Topic: Chebyshev's inequality


view this post on Zulip Koundinya Vajjha (May 30 2019 at 16:51):

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.

view this post on Zulip Mario Carneiro (May 30 2019 at 16:54):

Certainly. Let's get probability measures and probability theory

view this post on Zulip Koundinya Vajjha (May 30 2019 at 16:56):

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?

view this post on Zulip Mario Carneiro (May 30 2019 at 16:59):

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

view this post on Zulip Koundinya Vajjha (May 30 2019 at 17:00):

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.

view this post on Zulip Mario Carneiro (May 30 2019 at 17:05):

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


Last updated: May 06 2021 at 18:20 UTC