Chebyshev's sum inequality and Abel's inequality

This file proves the Chebyshev sum inequality, as well as Abel's 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.

Abel's inequality controls a weighted sum of a sequence f multiplied by an antitone nonnegative sequence g in terms of the partial sums of f.

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.
• Finset.sum_mul_le_sum_mul_of_sum_range_le, Finset.sum_mul_le_mul_of_sum_range_le, Finset.mul_le_sum_mul_of_le_sum_range, Finset.abs_sum_mul_le_mul_of_abs_sum_range_le: Abel's inequality and its one-sided and absolute-value forms.

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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {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 (e.g. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {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 (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.

theorem Monovary.sum_smul_sum_le_card_smul_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {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 (e.g. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {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 (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.

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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [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 (e.g. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [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 (e.g. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [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 Multiset.sq_sum_le_card_mul_sum_sq {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] (m : Multiset α) : m.sum ^ 2 ≤ ↑m.card * (map (fun (x : α) => x ^ 2) m).sum

Special case of Chebyshev's Sum Inequality or the Cauchy-Schwarz Inequality for a multiset: the square of the sum is at most the cardinality times the sum of the squares.

theorem Monovary.sum_mul_sum_le_card_mul_sum {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [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 (e.g. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [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 (e.g. 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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] [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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {f : ι → α} : ((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card

theorem Finset.sum_mul_le_sum_mul_of_sum_range_le {R : Type u_4} {f c g : ℕ → R} {n : ℕ} [Ring R] [PartialOrder R] [IsOrderedRing R] (hfc : ∀ k ≤ n, ∑ i ∈ range k, f i ≤ ∑ i ∈ range k, c i) (hg₀ : 0 ≤ g) (hg : AntitoneOn g (Set.Iio n)) : ∑ i ∈ range n, f i * g i ≤ ∑ i ∈ range n, c i * g i

Abel's inequality (comparison form): if the partial sums of f are dominated by those of c up to n, and g is nonnegative and antitone, then the g-weighted sum of f is dominated by that of c.

theorem Finset.sum_mul_le_mul_of_sum_range_le {R : Type u_4} {f g : ℕ → R} {M : R} {n : ℕ} [Ring R] [PartialOrder R] [IsOrderedRing R] (hf : ∀ k ≤ n, ∑ i ∈ range k, f i ≤ M) (hg₀ : 0 ≤ g) (hg : AntitoneOn g (Set.Iio n)) : ∑ i ∈ range n, f i * g i ≤ M * g 0

Abel's inequality (one-sided upper form): if every partial sum of f up to n is at most M, and g is nonnegative and antitone, then ∑ i ∈ range n, f i * g i ≤ M * g 0.

theorem Finset.mul_le_sum_mul_of_le_sum_range {R : Type u_4} {f g : ℕ → R} {m : R} {n : ℕ} [Ring R] [PartialOrder R] [IsOrderedRing R] (hf : ∀ k ≤ n, m ≤ ∑ i ∈ range k, f i) (hg₀ : 0 ≤ g) (hg : AntitoneOn g (Set.Iio n)) : m * g 0 ≤ ∑ i ∈ range n, f i * g i

Abel's inequality (one-sided lower form): if every partial sum of f up to n is at least m, and g is nonnegative and antitone, then m * g 0 ≤ ∑ i ∈ range n, f i * g i.

theorem Finset.abs_sum_mul_le_mul_of_abs_sum_range_le {R : Type u_4} {f g : ℕ → R} {M : R} {n : ℕ} [Ring R] [LinearOrder R] [IsOrderedRing R] (hf : ∀ k ≤ n, |∑ i ∈ range k, f i| ≤ M) (hg₀ : 0 ≤ g) (hg : AntitoneOn g (Set.Iio n)) : |∑ i ∈ range n, f i * g i| ≤ M * g 0

Abel's inequality: if every partial sum of f up to n has absolute value at most M, and g is nonnegative and antitone, then |∑ i ∈ range n, f i * g i| ≤ M * g 0.