sum_smul_sum_le_card_smul_sum — Mathlib

English

Chebyshev’s inequality on sums for monovary f and g: the sum-product bound is controlled by card and sums.

Русский

Неравенство Чебышёва для монотов f и g на суммах.

LaTeX

$$$\\sum f \\sum g \\le |ι| \\sum f g$$$

Lean4

/-- **Chebyshev's Sum Inequality**: When `f` and `g` monovary together (e.g. they are both
monotone/antitone), the scalar product of their sum is less than the size of the set times their
scalar product. -/
theorem sum_smul_sum_le_card_smul_sum (hfg : Monovary f g) : (∑ i, f i) • ∑ i, g i ≤ Fintype.card ι • ∑ i, f i • g i :=
  (hfg.monovaryOn _).sum_smul_sum_le_card_smul_sum

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