Documentation

Mathlib.Algebra.Order.Chebyshev

Chebyshev's sum inequality #

This file proves the Chebyshev sum inequality.

Chebyshev's inequality states (∑ i ∈ s, f i) * (∑ i ∈ s, g i) ≤ s.card * ∑ i ∈ s, f i * g i when f g : ι → α monovary, and the reverse inequality when f and g antivary.

Main declarations #

Implementation notes #

In fact, we don't need much compatibility between the addition and multiplication of α, so we can actually decouple them by replacing multiplication with scalar multiplication and making f and g land in different types. As a bonus, this makes the dual statement trivial. The multiplication versions are provided for convenience.

The case for Monotone/Antitone pairs of functions over a LinearOrder is not deduced in this file because it is easily deducible from the Monovary API.

Scalar multiplication versions #

theorem MonovaryOn.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [ExistsAddOfLE α] [LinearOrderedCancelAddCommMonoid β] [Module α β] [OrderedSMul α β] {s : Finset ι} {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) :
(∑ is, f i) is, g i s.card is, f i g i

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

theorem AntivaryOn.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [ExistsAddOfLE α] [LinearOrderedCancelAddCommMonoid β] [Module α β] [OrderedSMul α β] {s : Finset ι} {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) :
s.card is, f i g i (∑ is, f i) is, g i

Chebyshev's Sum Inequality: When f and g antivary together (eg 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.

theorem Monovary.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [ExistsAddOfLE α] [LinearOrderedCancelAddCommMonoid β] [Module α β] [OrderedSMul α β] {f : ια} {g : ιβ} [Fintype ι] (hfg : 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 (eg they are both monotone/antitone), the scalar product of their sum is less than the size of the set times their scalar product.

theorem Antivary.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [ExistsAddOfLE α] [LinearOrderedCancelAddCommMonoid β] [Module α β] [OrderedSMul α β] {f : ια} {g : ιβ} [Fintype ι] (hfg : Antivary f g) :
Fintype.card ι i : ι, f i g i (∑ i : ι, f i) i : ι, g i

Chebyshev's Sum Inequality: When f and g antivary together (eg 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.

Multiplication versions #

Special cases of the above when scalar multiplication is actually multiplication.

theorem MonovaryOn.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} [LinearOrderedSemiring α] [ExistsAddOfLE α] {s : Finset ι} {f : ια} {g : ια} (hfg : MonovaryOn f g s) :
(∑ is, f i) * is, g i s.card * is, f i * g i

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

theorem AntivaryOn.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} [LinearOrderedSemiring α] [ExistsAddOfLE α] {s : Finset ι} {f : ια} {g : ια} (hfg : AntivaryOn f g s) :
s.card * is, f i * g i (∑ is, f i) * is, g i

Chebyshev's Sum Inequality: When f and g antivary together (eg 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 pow_sum_le_card_mul_sum_pow {ι : Type u_1} {α : Type u_2} [LinearOrderedSemiring α] [ExistsAddOfLE α] {s : Finset ι} {f : ια} (hf : is, 0 f i) (n : ) :
(∑ is, f i) ^ (n + 1) s.card ^ n * is, f i ^ (n + 1)

Special case of Jensen's inequality for sums of powers.

theorem sq_sum_le_card_mul_sum_sq {ι : Type u_1} {α : Type u_2} [LinearOrderedSemiring α] [ExistsAddOfLE α] {s : Finset ι} {f : ια} :
(∑ is, f i) ^ 2 s.card * is, f i ^ 2

Special case of Chebyshev's Sum Inequality or the Cauchy-Schwarz Inequality: The square of the sum is less than the size of the set times the sum of the squares.

theorem Monovary.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} [LinearOrderedSemiring α] [ExistsAddOfLE α] {f : ια} {g : ια} [Fintype ι] (hfg : 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 (eg they are both monotone/antitone), the product of their sum is less than the size of the set times their scalar product.

theorem Antivary.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} [LinearOrderedSemiring α] [ExistsAddOfLE α] {f : ια} {g : ια} [Fintype ι] (hfg : Antivary f g) :
(Fintype.card ι) * i : ι, f i * g i (∑ i : ι, f i) * i : ι, g i

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

theorem pow_sum_div_card_le_sum_pow {ι : Type u_1} {α : Type u_2} [LinearOrderedSemifield α] [ExistsAddOfLE α] {s : Finset ι} {f : ια} (hf : is, 0 f i) (n : ) :
(∑ is, f i) ^ (n + 1) / s.card ^ n is, f i ^ (n + 1)

Special case of Jensen's inequality for sums of powers.

theorem sum_div_card_sq_le_sum_sq_div_card {ι : Type u_1} {α : Type u_2} [LinearOrderedSemifield α] [ExistsAddOfLE α] {s : Finset ι} {f : ια} :
((∑ is, f i) / s.card) ^ 2 (∑ is, f i ^ 2) / s.card