card_mul_sum_le_sum_mul_sum — Mathlib

English

Chebyshev inequality for antivariation in monovary dual form; sum/product relations.

Русский

Неравенство Чебышёва для антивариации в двойной форме моновариации; связи сумм/произведений.

LaTeX

$$$\\text{AntivaryOn}(f,g,s) \\Rightarrow \\sum f \\cdot \\sum g \\ge |s| \\sum f g$$$

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 greater than the size of the set times their scalar
product. -/
theorem card_mul_sum_le_sum_mul_sum (hfg : AntivaryOn f g s) :
    (#s : α) * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i :=
  by
  rw [← nsmul_eq_mul]
  exact hfg.card_smul_sum_le_sum_smul_sum

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