# 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 #

**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.

**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.

**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.

**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.

**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.

**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.

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.

**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.

**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.