Chebyshev's sum inequality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

monovary_on.sum_mul_sum_le_card_mul_sum: Chebyshev's inequality.
antivary_on.card_mul_sum_le_sum_mul_sum: Chebyshev's inequality, dual version.
sq_sum_le_card_mul_sum_sq: Special case of Chebyshev's inequality when f = g.

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 linear_order is not deduced in this file because it is easily deducible from the monovary API.

Scalar multiplication versions #

source

theorem monovary_on.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f g ↑s) :

s.sum (λ (i : ι), f i) • s.sum (λ (i : ι), g i) ≤ s.card • s.sum (λ (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.

source

theorem antivary_on.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f g ↑s) :

s.card • s.sum (λ (i : ι), f i • g i) ≤ s.sum (λ (i : ι), f i) • s.sum (λ (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.

source

theorem monovary.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f g) :

finset.univ.sum (λ (i : ι), f i) • finset.univ.sum (λ (i : ι), g i) ≤ fintype.card ι • finset.univ.sum (λ (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.

source

theorem antivary.card_smul_sum_le_sum_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f g) :

fintype.card ι • finset.univ.sum (λ (i : ι), f i • g i) ≤ finset.univ.sum (λ (i : ι), f i) • finset.univ.sum (λ (i : ι), g i)

Multiplication versions #

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

source

theorem monovary_on.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {f g : ι → α} (hfg : monovary_on f g ↑s) :

s.sum (λ (i : ι), f i) * s.sum (λ (i : ι), g i) ≤ ↑(s.card) * s.sum (λ (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.

source

theorem antivary_on.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {f g : ι → α} (hfg : antivary_on f g ↑s) :

↑(s.card) * s.sum (λ (i : ι), f i * g i) ≤ s.sum (λ (i : ι), f i) * s.sum (λ (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.

source

theorem sq_sum_le_card_mul_sum_sq {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {f : ι → α} :

s.sum (λ (i : ι), f i) ^ 2 ≤ ↑(s.card) * s.sum (λ (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.

source

theorem monovary.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {f g : ι → α} [fintype ι] (hfg : monovary f g) :

finset.univ.sum (λ (i : ι), f i) * finset.univ.sum (λ (i : ι), g i) ≤ ↑(fintype.card ι) * finset.univ.sum (λ (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.

source

theorem antivary.card_mul_sum_le_sum_mul_sum {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {f g : ι → α} [fintype ι] (hfg : antivary f g) :

↑(fintype.card ι) * finset.univ.sum (λ (i : ι), f i * g i) ≤ finset.univ.sum (λ (i : ι), f i) * finset.univ.sum (λ (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.

source

theorem sum_div_card_sq_le_sum_sq_div_card {ι : Type u_1} {α : Type u_2} [linear_ordered_field α] {s : finset ι} {f : ι → α} :

(s.sum (λ (i : ι), f i) / ↑(s.card)) ^ 2 ≤ s.sum (λ (i : ι), f i ^ 2) / ↑(s.card)