English
If f and g monovary on a finite index set, then the product of their sums is at most the size of the index set times the sum of their pointwise products: (∑ i∈ι f(i))(∑ i∈ι g(i)) ≤ |ι| ∑ i∈ι f(i)g(i).
Русский
Если функции f и g моновариантны вместе на конечном множестве индексов, то произведение их сумм не превосходит размера множества умноженного на сумму попарных произведений: (∑ f(i))(∑ g(i)) ≤ |ι| ∑ f(i)g(i).
LaTeX
$$$\left(\sum_{i \in s} f(i)\right) \left(\sum_{i \in s} g(i)\right) \le |s| \sum_{i \in s} f(i) g(i)$$$
Lean4
/-- **Chebyshev's Sum Inequality**: When `f` and `g` monovary together (e.g. they are both
monotone/antitone), the product of their sum is less than the size of the set times their scalar
product. -/
theorem sum_mul_sum_le_card_mul_sum (hfg : Monovary f g) : (∑ i, f i) * ∑ i, g i ≤ Fintype.card ι * ∑ i, f i * g i :=
(hfg.monovaryOn _).sum_mul_sum_le_card_mul_sum
