Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-02 08:56 aebd3428

View on Github →

feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187) Prove Chebyshev's sum inequality as a corollary to the rearrangement inequality.

Estimated changes

Created src/algebra/order/chebyshev.lean

added theorem antivary.card_mul_sum_le_sum_mul_sum

added theorem antivary.card_smul_sum_le_sum_smul_sum

added theorem antivary_on.card_mul_sum_le_sum_mul_sum

added theorem antivary_on.card_smul_sum_le_sum_smul_sum

added theorem monovary.sum_mul_sum_le_card_mul_sum

added theorem monovary.sum_smul_sum_le_card_smul_sum

added theorem monovary_on.sum_mul_sum_le_card_mul_sum

added theorem monovary_on.sum_smul_sum_le_card_smul_sum

added theorem sq_sum_le_card_mul_sum_sq