Theorems · Theorem · real analysis

Monovary.sum_mul_sum_le_card_mul_sum

∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {f g : ι → α} [inst_4 : Fintype ι], Monovary f g → (∑ i, f i) * ∑ i, g i ≤ ↑(Fintype.card ι) * ∑ i, 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

0 results in Mathlib

Foundations

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

Assumes

SemiringLinearOrderIsStrictOrderedRingExistsAddOfLEFintype