Topic: Chebyshev's inequality
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.
Mario Carneiro (May 30 2019 at 16:54):
Certainly. Let's get probability measures and probability theory
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
ennreal. What is the consensus on this now?
Mario Carneiro (May 30 2019 at 16:59):
what is your personal consensus on that? Sounds like you've already found an answer
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.
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