Theorems · Theorem · real analysis

MonovaryOn.sum_mul_sum_le_card_mul_sum

∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f g : ι → α}, MonovaryOn f g ↑s → (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑s.card * ∑ i ∈ s, f i * g i

Chebyshev's Sum Inequality: When f and g monovary together (e.g. they are both monotone/antitone), the product of their sum is less than the size of the set times their scalar product.

Defined in

Mathlib.Algebra.Order.Chebyshev

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringLinearOrderIsStrictOrderedRingExistsAddOfLE