# mathlib3documentation

algebra.order.chebyshev

# Chebyshev's sum inequality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• monovary_on.sum_mul_sum_le_card_mul_sum: Chebyshev's inequality.
• antivary_on.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 linear_order is not deduced in this file because it is easily deducible from the monovary API.

### Scalar multiplication versions #

theorem monovary_on.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {f : ι α} {g : ι β} (hfg : g s) :
s.sum (λ (i : ι), f i) s.sum (λ (i : ι), g i) s.card s.sum (λ (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_on.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {f : ι α} {g : ι β} (hfg : g s) :
s.card s.sum (λ (i : ι), f i g i) s.sum (λ (i : ι), f i) s.sum (λ (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} [ β] [ β] {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i) finset.univ.sum (λ (i : ι), g i) finset.univ.sum (λ (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} [ β] [ β] {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g i) finset.univ.sum (λ (i : ι), f i) finset.univ.sum (λ (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 monovary_on.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} {s : finset ι} {f g : ι α} (hfg : g s) :
s.sum (λ (i : ι), f i) * s.sum (λ (i : ι), g i) (s.card) * s.sum (λ (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_on.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} {s : finset ι} {f g : ι α} (hfg : g s) :
(s.card) * s.sum (λ (i : ι), f i * g i) s.sum (λ (i : ι), f i) * s.sum (λ (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 : finset ι} {f : ι α} :
s.sum (λ (i : ι), f i) ^ 2 (s.card) * s.sum (λ (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 : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i) * finset.univ.sum (λ (i : ι), g i) (fintype.card ι) * finset.univ.sum (λ (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 : ι α} [fintype ι] (hfg : g) :
(fintype.card ι) * finset.univ.sum (λ (i : ι), f i * g i) finset.univ.sum (λ (i : ι), f i) * finset.univ.sum (λ (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 : finset ι} {f : ι α} :
(s.sum (λ (i : ι), f i) / (s.card)) ^ 2 s.sum (λ (i : ι), f i ^ 2) / (s.card)