Documentation

Mathlib.Algebra.Order.Chebyshev

Chebyshev's sum inequality #

This file proves the Chebyshev sum inequality.

Chebyshev's inequality states (∑ i in s, f i) * (∑ i in s, g i) ≤ s.card * ∑ i in 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} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {s : Finset ι} {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) :
((Finset.sum s fun (i : ι) => f i) Finset.sum s fun (i : ι) => g i) s.card Finset.sum s fun (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 AntivaryOn.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {s : Finset ι} {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) :
(s.card Finset.sum s fun (i : ι) => f i g i) (Finset.sum s fun (i : ι) => f i) Finset.sum s fun (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.

theorem Monovary.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ια} {g : ιβ} [Fintype ι] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun (i : ι) => f i) Finset.sum Finset.univ fun (i : ι) => g i) Fintype.card ι Finset.sum Finset.univ fun (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} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ια} {g : ιβ} [Fintype ι] (hfg : Antivary f g) :
(Fintype.card ι Finset.sum Finset.univ fun (i : ι) => f i g i) (Finset.sum Finset.univ fun (i : ι) => f i) Finset.sum Finset.univ fun (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} [LinearOrderedRing α] {s : Finset ι} {f : ια} {g : ια} (hfg : MonovaryOn f g s) :
((Finset.sum s fun (i : ι) => f i) * Finset.sum s fun (i : ι) => g i) s.card * Finset.sum s fun (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 AntivaryOn.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {s : Finset ι} {f : ια} {g : ια} (hfg : AntivaryOn f g s) :
(s.card * Finset.sum s fun (i : ι) => f i * g i) (Finset.sum s fun (i : ι) => f i) * Finset.sum s fun (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 greater than the size of the set times their scalar product.

theorem sq_sum_le_card_mul_sum_sq {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {s : Finset ι} {f : ια} :
(Finset.sum s fun (i : ι) => f i) ^ 2 s.card * Finset.sum s fun (i : ι) => 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} [LinearOrderedRing α] {f : ια} {g : ια} [Fintype ι] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun (i : ι) => f i) * Finset.sum Finset.univ fun (i : ι) => g i) (Fintype.card ι) * Finset.sum Finset.univ fun (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} [LinearOrderedRing α] {f : ια} {g : ια} [Fintype ι] (hfg : Antivary f g) :
((Fintype.card ι) * Finset.sum Finset.univ fun (i : ι) => f i * g i) (Finset.sum Finset.univ fun (i : ι) => f i) * Finset.sum Finset.univ fun (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 sum_div_card_sq_le_sum_sq_div_card {ι : Type u_1} {α : Type u_2} [LinearOrderedField α] {s : Finset ι} {f : ια} :
((Finset.sum s fun (i : ι) => f i) / s.card) ^ 2 (Finset.sum s fun (i : ι) => f i ^ 2) / s.card