card_smul_sum_le_sum_smul_sum — Mathlib

English

Chebyshev inequality for antivariation on a finite set, in dual form.

Русский

Неравенство Чебышёва для антивариации на конечном множестве, в двойной форме.

LaTeX

$$$\\text{AntivaryOn}(f,g,s) \\Rightarrow \\#s \\sum f_i g_i \\le (\\sum f_i)(\\sum 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 : Antivary f g) : Fintype.card ι • ∑ i, f i • g i ≤ (∑ i, f i) • ∑ i, g i :=
  (hfg.dual_right.monovaryOn _).sum_smul_sum_le_card_smul_sum

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