Chebyshev's sum inequality

Remarks

Proof idea: expand to get the identity $$n \sum_{i=1}^{n} a_i b_i - \sum_{i=1}^{n} a_i \sum_{j=1}^{n} b_j = \frac{1}{2} \sum_{i=1}^{n} \sum_{j=1}^{n} (a_i - a_j)(b_i - b_j).$$ Each term on the right is $\ge 0$, because $a_i - a_j$ and $b_i - b_j$ have the same sign for monotone sequences ordered the same way.

If one sequence decreases and the other increases, the inequality is reversed. The common ordering is needed: for $a = (1, 0)$ and $b = (0, 1)$, the left side is $0$ and the right side is $1/4$.

Example: taking $b = a$ gives $n \sum a_i^2 \ge (\sum a_i)^2$, which holds for every real sequence after sorting.

Mathlib states a form as Monovary.sum_mul_sum_le_card_mul_sum.

Going deeper

For a student

The inequality follows from the rearrangement inequality by summing over the $n$ cyclic shifts of the second sequence. It has an integral form: if $f$ and $g$ are both increasing on $[0, 1]$, then $\int_0^1 f g \ge \int_0^1 f \int_0^1 g$. In probability it says that two increasing functions of the same random variable have nonnegative covariance.