card_smul_sum_le_sum_smul_sum — Mathlib

English

Chebyshev’s inequality for antivariation: if f and g antivary on s, then card s times the sum of products is ≤ sums product.

Русский

Неравенство Чебышева для антивариации: если f и g antivary на s, то card s умноженное на сумму произведений ≤ произведение сумм.

LaTeX

$$$\\#s \\sum_{i\\in s} f_i g_i \\le (\\sum_{i\\in s} f_i)(\\sum_{i\\in s} g_i)$$$

Lean4

/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. 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 card_smul_sum_le_sum_smul_sum (hfg : AntivaryOn f g s) :
    #s • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, g i :=
  hfg.dual_right.sum_smul_sum_le_card_smul_sum

Похожие утверждения