mathlib3
3891ab62 - feat(measure_theory/integral/lebesgue): Add Markov inequalities for tsum and card using counting measure. (#17588)

Commit
3 years ago
feat(measure_theory/integral/lebesgue): Add Markov inequalities for tsum and card using counting measure. (#17588) Add Markov inequalities for `tsum` and `finset.card` using the counting measure to translate the Markov inequality from measure theory to these. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Author
Parents
Loading