English
Chebyshev’s inequality for monovary: when f and g monovary on s, the sum/product inequality holds with card s.
Русский
Неравенство Чебышева для моно-вариаций: если f и g монотонны вместе на s, выполняется соответствующее неравенство.
LaTeX
$$$\\text{MonovaryOn}(f,g,s) \\Rightarrow (\\sum_{i\\in s} f_i) \\cdot (\\sum_{i\\in s} g_i) \\ge |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 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 : MonovaryOn f g s) :
(∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i := by
classical
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]
exact
sum_le_card_nsmul _ _ _ fun n _ ↦
hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _
