# Chebyshev's sum inequality #

This file proves the Chebyshev sum inequality.

Chebyshev's inequality states (∑ i in s, f i) * (∑ i in s, g i) ≤ s.card * ∑ i in s, f i * g i when f g : ι → α monovary, and the reverse inequality when f and g antivary.

## Main declarations #

• MonovaryOn.sum_mul_sum_le_card_mul_sum: Chebyshev's inequality.
• AntivaryOn.card_mul_sum_le_sum_mul_sum: Chebyshev's inequality, dual version.
• sq_sum_le_card_mul_sum_sq: Special case of Chebyshev's inequality when f = g.

## Implementation notes #

In fact, we don't need much compatibility between the addition and multiplication of α, so we can actually decouple them by replacing multiplication with scalar multiplication and making f and g land in different types. As a bonus, this makes the dual statement trivial. The multiplication versions are provided for convenience.

The case for Monotone/Antitone pairs of functions over a LinearOrder is not deduced in this file because it is easily deducible from the Monovary API.

### Scalar multiplication versions #

theorem MonovaryOn.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) :
((s.sum fun (i : ι) => f i) s.sum fun (i : ι) => g i) s.card s.sum fun (i : ι) => f i g i

Chebyshev's Sum Inequality: When f and g monovary together (eg they are both monotone/antitone), the scalar product of their sum is less than the size of the set times their scalar product.

theorem AntivaryOn.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) :
(s.card s.sum fun (i : ι) => f i g i) (s.sum fun (i : ι) => f i) s.sum fun (i : ι) => g i

Chebyshev's Sum Inequality: When f and g antivary together (eg one is monotone, the other is antitone), the scalar product of their sum is less than the size of the set times their scalar product.

theorem Monovary.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
((Finset.univ.sum fun (i : ι) => f i) Finset.univ.sum fun (i : ι) => g i) Finset.univ.sum fun (i : ι) => f i g i

Chebyshev's Sum Inequality: When f and g monovary together (eg they are both monotone/antitone), the scalar product of their sum is less than the size of the set times their scalar product.

theorem Antivary.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
( Finset.univ.sum fun (i : ι) => f i g i) (Finset.univ.sum fun (i : ι) => f i) Finset.univ.sum fun (i : ι) => g i

Chebyshev's Sum Inequality: When f and g antivary together (eg one is monotone, the other is antitone), the scalar product of their sum is less than the size of the set times their scalar product.

### Multiplication versions #

Special cases of the above when scalar multiplication is actually multiplication.

theorem MonovaryOn.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} {s : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) :
((s.sum fun (i : ι) => f i) * s.sum fun (i : ι) => g i) s.card * s.sum fun (i : ι) => f i * g i

Chebyshev's Sum Inequality: When f and g monovary together (eg they are both monotone/antitone), the product of their sum is less than the size of the set times their scalar product.

theorem AntivaryOn.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} {s : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) :
(s.card * s.sum fun (i : ι) => f i * g i) (s.sum fun (i : ι) => f i) * s.sum fun (i : ι) => g i

Chebyshev's Sum Inequality: When f and g antivary together (eg one is monotone, the other is antitone), the product of their sum is greater than the size of the set times their scalar product.

theorem sq_sum_le_card_mul_sum_sq {ι : Type u_1} {α : Type u_2} {s : } {f : ια} :
(s.sum fun (i : ι) => f i) ^ 2 s.card * s.sum fun (i : ι) => f i ^ 2

Special case of Chebyshev's Sum Inequality or the Cauchy-Schwarz Inequality: The square of the sum is less than the size of the set times the sum of the squares.

theorem Monovary.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} [] (hfg : Monovary f g) :
((Finset.univ.sum fun (i : ι) => f i) * Finset.univ.sum fun (i : ι) => g i) () * Finset.univ.sum fun (i : ι) => f i * g i

Chebyshev's Sum Inequality: When f and g monovary together (eg they are both monotone/antitone), the product of their sum is less than the size of the set times their scalar product.

theorem Antivary.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} [] (hfg : Antivary f g) :
(() * Finset.univ.sum fun (i : ι) => f i * g i) (Finset.univ.sum fun (i : ι) => f i) * Finset.univ.sum fun (i : ι) => g i

Chebyshev's Sum Inequality: When f and g antivary together (eg one is monotone, the other is antitone), the product of their sum is less than the size of the set times their scalar product.

theorem sum_div_card_sq_le_sum_sq_div_card {ι : Type u_1} {α : Type u_2} {s : } {f : ια} :
((s.sum fun (i : ι) => f i) / s.card) ^ 2 (s.sum fun (i : ι) => f i ^ 2) / s.card