Theorems · Theorem · real analysis

AntivaryOn.card_smul_sum_le_sum_smul_sum

∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {s : Finset ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → s.card • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, g i

Chebyshev's Sum Inequality: When f and g antivary together (e.g. one is monotone, the other is antitone), the scalar product of their sum is less than the size of the set times their scalar product.

Defined in

Mathlib.Algebra.Order.Chebyshev

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringLinearOrderIsStrictOrderedRingExistsAddOfLEAddCommMonoidLinearOrderIsOrderedCancelAddMonoidModulePosSMulMono