English
If f and g antivary on a finite index set, then the product of their sums dominates the sum of their products by the size of the index set: |ι| ∑ i f(i)g(i) ≤ (∑ i f(i))(∑ i g(i)).
Русский
Если f и g антивариантны на конечном множестве индексов, то |ι| ∑ f(i)g(i) ≤ (∑ f(i))(∑ g(i)).
LaTeX
$$$|s| \sum_{i \in s} f(i) g(i) \le \left(\sum_{i \in s} f(i)\right) \left(\sum_{i \in s} g(i)\right)$$$
Lean4
/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. 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 card_mul_sum_le_sum_mul_sum (hfg : Antivary f g) : Fintype.card ι * ∑ i, f i * g i ≤ (∑ i, f i) * ∑ i, g i :=
(hfg.antivaryOn _).card_mul_sum_le_sum_mul_sum
