Grüss’s finite covariance bound

Paper

Über das Maximum des absoluten Betrages von [integral covariance expression], 1935. Mathematische Zeitschrift 39, pp. 215–226; title formula abbreviated here. Read a later treatment of discrete Grüss inequalities.

The result

If one list stays in [m,M] and another in [p,P], the absolute weighted covariance is at most one quarter of the product of the two range widths.

|E[fg] − E[f]E[g]| ≤ (M − m)(P − p)/4

Scope & assumptions

6 checked theorems. Centered covariance/variance identities, nonnegative variance, the range variance bound, weighted Cauchy–Schwarz, and the final inequality. No integration or claim that the variance-bound ingredients are new.

Finite real lists indexed by a finite set; nonnegative weights summing to one; m ≤ fᵢ ≤ M and p ≤ gᵢ ≤ P. Constant ranges and zero weights are allowed. E means the weighted finite sum.

Prior work

No matching named Grüss formalization was located in the bounded search; first-formalization status is unconfirmed. Mathlib already supplies finite Cauchy–Schwarz and related probability variance bounds, including Popoviciu’s inequality. This artifact combines established ingredients in a finite weighted statement.

Lean proof

Lean + Mathlib 4.33.1 · 6 checked theorems

import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity

/-! Grüss (1935): a finite weighted analogue of the integral covariance bound.
Nonnegative weights sum to one. This file does not formalize integration.
Finite Cauchy--Schwarz is reused from Mathlib, not claimed as a new result. -/
namespace PaperToLean.Gruss
noncomputable section
open scoped BigOperators
variable {ι : Type*}
def avg (I : Finset ι) (w f : ι → ℝ) : ℝ := ∑ i ∈ I, w i * f i
def variance (I : Finset ι) (w f : ι → ℝ) : ℝ := avg I w (fun i => f i ^ 2) - (avg I w f) ^ 2
def covariance (I : Finset ι) (w f g : ι → ℝ) : ℝ := avg I w (fun i => f i * g i) - avg I w f * avg I w g

theorem centered_covariance (I : Finset ι) (w f g : ι → ℝ) (hw : ∑ i ∈ I, w i = 1) :
    avg I w (fun i => (f i - avg I w f) * (g i - avg I w g)) = covariance I w f g := by
  have hexp (u v : ℝ) : (∑ i ∈ I, w i * ((f i - u) * (g i - v))) =
      avg I w (fun i => f i * g i) - v * avg I w f -
      u * avg I w g + u * v * ∑ i ∈ I, w i := by
    simp only [avg, Finset.mul_sum, ← Finset.sum_sub_distrib,
      ← Finset.sum_add_distrib]
    apply Finset.sum_congr rfl
    intro i _
    ring
  change (∑ i ∈ I, w i * ((f i - avg I w f) * (g i - avg I w g))) = _
  rw [hexp, hw]
  unfold covariance
  ring

theorem centered_variance (I : Finset ι) (w f : ι → ℝ) (hw : ∑ i ∈ I, w i = 1) :
    avg I w (fun i => (f i - avg I w f) ^ 2) = variance I w f := by
  simpa only [variance, covariance, pow_two] using centered_covariance I w f f hw

theorem variance_nonneg (I : Finset ι) (w f : ι → ℝ)
    (hw : ∑ i ∈ I, w i = 1) (hw0 : ∀ i ∈ I, 0 ≤ w i) : 0 ≤ variance I w f := by
  rw [← centered_variance I w f hw]
  exact Finset.sum_nonneg (fun i hi => mul_nonneg (hw0 i hi) (sq_nonneg _))

theorem range_variance_bound (I : Finset ι) (w f : ι → ℝ) (m M : ℝ)
    (hw : ∑ i ∈ I, w i = 1) (hw0 : ∀ i ∈ I, 0 ≤ w i)
    (hlo : ∀ i ∈ I, m ≤ f i) (hhi : ∀ i ∈ I, f i ≤ M) :
    variance I w f ≤ (M - m) ^ 2 / 4 := by
  have hpoint : ∀ i ∈ I, w i * f i ^ 2 ≤ w i * ((m + M) * f i - m * M) := by
    intro i hi
    apply mul_le_mul_of_nonneg_left _ (hw0 i hi)
    nlinarith [mul_nonneg (sub_nonneg.mpr (hlo i hi)) (sub_nonneg.mpr (hhi i hi))]
  have hs := Finset.sum_le_sum hpoint
  have heq : (∑ i ∈ I, w i * ((m + M) * f i - m * M)) =
      (m + M) * avg I w f - m * M := by
    calc
      _ = (m + M) * avg I w f - m * M * (∑ i ∈ I, w i) := by
        simp only [avg, Finset.mul_sum, ← Finset.sum_sub_distrib]
        apply Finset.sum_congr rfl
        intro i _
        ring
      _ = _ := by rw [hw, mul_one]
  rw [heq] at hs
  change avg I w (fun i => f i ^ 2) ≤ _ at hs
  unfold variance
  nlinarith [sq_nonneg (avg I w f - (m + M) / 2)]

theorem covariance_cauchy (I : Finset ι) (w f g : ι → ℝ)
    (hw : ∑ i ∈ I, w i = 1) (hw0 : ∀ i ∈ I, 0 ≤ w i) :
    (covariance I w f g) ^ 2 ≤ variance I w f * variance I w g := by
  rw [← centered_covariance I w f g hw, ← centered_variance I w f hw,
    ← centered_variance I w g hw]
  apply Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul I
  · intro i hi
    exact mul_nonneg (hw0 i hi) (sq_nonneg _)
  · intro i hi
    exact mul_nonneg (hw0 i hi) (sq_nonneg _)
  · intro i _
    exact le_of_eq (by ring)

theorem inequality (I : Finset ι) (w f g : ι → ℝ) (m M p P : ℝ)
    (hw : ∑ i ∈ I, w i = 1) (hw0 : ∀ i ∈ I, 0 ≤ w i)
    (hmM : m ≤ M) (hpP : p ≤ P)
    (hf : ∀ i ∈ I, m ≤ f i ∧ f i ≤ M) (hg : ∀ i ∈ I, p ≤ g i ∧ g i ≤ P) :
    |covariance I w f g| ≤ (M - m) * (P - p) / 4 := by
  have hc := covariance_cauchy I w f g hw hw0
  have hfv := range_variance_bound I w f m M hw hw0 (fun i hi => (hf i hi).1) (fun i hi => (hf i hi).2)
  have hgv := range_variance_bound I w g p P hw hw0 (fun i hi => (hg i hi).1) (fun i hi => (hg i hi).2)
  have hprod := mul_le_mul hfv hgv (variance_nonneg I w g hw hw0) (by positivity : 0 ≤ (M - m) ^ 2 / 4)
  have hb : 0 ≤ (M - m) * (P - p) / 4 := by positivity
  have heq : ((M - m) * (P - p) / 4) ^ 2 = ((M - m) ^ 2 / 4) * ((P - p) ^ 2 / 4) := by ring
  have habs := sq_abs (covariance I w f g)
  nlinarith [abs_nonneg (covariance I w f g)]

#print axioms centered_covariance
#print axioms centered_variance
#print axioms variance_nonneg
#print axioms range_variance_bound
#print axioms covariance_cauchy
#print axioms inequality
end
end PaperToLean.Gruss

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Gruss.lean
SHA-256: 36adf642bd5ae96a43a2f77bf1dc7309ece7291fa3b67b05c337b5334cf6dbc3
Result: passed

'PaperToLean.Gruss.centered_covariance' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.centered_variance' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.variance_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.range_variance_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.covariance_cauchy' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.inequality' depends on axioms: [propext, Classical.choice, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Gruss.lean

A successful check prints the axiom dependencies and exits without errors.