Weighted Chebyshev sum inequality

Mathlib's Chebyshev sum inequality (MonovaryOn.sum_mul_sum_le_card_mul_sum) counts every index once. This file weights the indices: under nonnegative weights, two functions that monovary have a nonnegative weighted covariance, and two that antivary a nonpositive one. With the weights a probability distribution this is the covariance inequality E[f] E[g] ≤ E[f g] for similarly ordered f and g.

Main results

• two_mul_sum_mul_sum_mul_mul_sub — twice the covariance defect is the double sum of the weighted products of pairwise differences.
• MonovaryOn.sum_mul_mul_sum_mul_le_sum_mul_sum_mul_mul, AntivaryOn.sum_mul_sum_mul_mul_le_sum_mul_mul_sum_mul — the weighted Chebyshev sum inequality on a finset, and Monovary.sum_mul_mul_sum_mul_le_sum_mul_sum_mul_mul, Antivary.sum_mul_sum_mul_mul_le_sum_mul_mul_sum_mul over a finite type.

theorem two_mul_sum_mul_sum_mul_mul_sub {ι : Type u_1} {α : Type u_2} [CommRing α] (w f g : ι → α) (s : Finset ι) : 2 * ((∑ i ∈ s, w i) * ∑ i ∈ s, w i * (f i * g i) - (∑ i ∈ s, w i * f i) * ∑ i ∈ s, w i * g i) = ∑ i ∈ s, ∑ j ∈ s, w i * w j * ((f i - f j) * (g i - g j))

Twice the covariance defect of weighted sums is the weighted double sum of the products of pairwise differences.

theorem MonovaryOn.sum_mul_mul_sum_mul_le_sum_mul_sum_mul_mul {ι : Type u_1} {α : Type u_2} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] {w f g : ι → α} {s : Finset ι} (hfg : MonovaryOn f g ↑s) (hw : ∀ i ∈ s, 0 ≤ w i) : (∑ i ∈ s, w i * f i) * ∑ i ∈ s, w i * g i ≤ (∑ i ∈ s, w i) * ∑ i ∈ s, w i * (f i * g i)

Weighted Chebyshev sum inequality: functions that monovary have nonnegative covariance under nonnegative weights.

theorem AntivaryOn.sum_mul_sum_mul_mul_le_sum_mul_mul_sum_mul {ι : Type u_1} {α : Type u_2} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] {w f g : ι → α} {s : Finset ι} (hfg : AntivaryOn f g ↑s) (hw : ∀ i ∈ s, 0 ≤ w i) : (∑ i ∈ s, w i) * ∑ i ∈ s, w i * (f i * g i) ≤ (∑ i ∈ s, w i * f i) * ∑ i ∈ s, w i * g i

Weighted Chebyshev sum inequality: functions that antivary have nonpositive covariance under nonnegative weights.

theorem Monovary.sum_mul_mul_sum_mul_le_sum_mul_sum_mul_mul {ι : Type u_1} {α : Type u_2} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] {w f g : ι → α} [Fintype ι] (hfg : Monovary f g) (hw : ∀ (i : ι), 0 ≤ w i) : (∑ i : ι, w i * f i) * ∑ i : ι, w i * g i ≤ (∑ i : ι, w i) * ∑ i : ι, w i * (f i * g i)

theorem Antivary.sum_mul_sum_mul_mul_le_sum_mul_mul_sum_mul {ι : Type u_1} {α : Type u_2} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] {w f g : ι → α} [Fintype ι] (hfg : Antivary f g) (hw : ∀ (i : ι), 0 ≤ w i) : (∑ i : ι, w i) * ∑ i : ι, w i * (f i * g i) ≤ (∑ i : ι, w i * f i) * ∑ i : ι, w i * g i