Markov Inequality (Generalized)

Stream: mathlib4

[Alvan Arulandu]

While Markov's is already formalized, I was wondering if it would be of interest to formalize some corollaries such as P(X >= a) <= E[X^n]/a^n or generally P(X >= a) <= E[f(X)] / f(a) for one-to-one f?

[Yaël Dillies]

Hey! I think those are a bit too easy to derive from the existing Markov inequality to have (P(X ≥ a) = P(f(X) ≥ f(a)) ≤ E[f(X)] / f(a)). However, we certainly want consequences of said corollaries, such as Chernoff's bound!

[Yaël Dillies]

It would be a great contribution to mathlib. But please coordinate with the people in #mathlib4 > Hoeffding's lemma to avoid duplicating work

[Rémy Degenne]

Chernoff's bound is here: ProbabilityTheory.measure_ge_le_exp_cgf

[Alvan Arulandu]

I agree that the derivation is simple, but I've seen it used in this form a lot in a probability class so was curious. No worries, and thank you so much for the Chernoff bound link!