Chebyshev's sum inequality

This file proves the Chebyshev sum inequality.

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

Main declarations

• MonovaryOn.sum_mul_sum_le_card_mul_sum: Chebyshev's inequality.
• AntivaryOn.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 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) : (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ s.card • ∑ i ∈ s, 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 • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, 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) : (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑s.card * ∑ i ∈ s, 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 * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, 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 : ∀ i ∈ s, 0 ≤ f i) (n : ℕ) : (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑s.card ^ n * ∑ i ∈ s, 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 : ι → α} : (∑ i ∈ s, f i) ^ 2 ≤ ↑s.card * ∑ i ∈ s, 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 : ∀ i ∈ s, 0 ≤ f i) (n : ℕ) : (∑ i ∈ s, f i) ^ (n + 1) / ↑s.card ^ n ≤ ∑ i ∈ s, 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 : ι → α} : ((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card