Skip to content

Kantorovich, Bhatia–Davis and Popoviciu inequalities

14 fully proved

Scalar

TheoremWeighted variance as weighted squared deviation from the mean#✓fully proved

The weighted variance equals the weighted squared deviation from the weighted mean.

theorem weighted_variance_eq (hw_sum : ∑ i, w i = 1) :
    (∑ i, w i * lam i ^ 2) - (∑ i, w i * lam i) ^ 2
      = ∑ i, w i * (lam i - ∑ j, w j * lam j) ^ 2
Used by 1
Used byOperator variance as weighted squared deviation of eigenvalues

TheoremBhatia–Davis inequality#✓fully proved

Bhatia–Davis inequality, scalar weighted form: if the weights are nonnegative, sum to 1, and every λ i lies in [m, M], then the weighted variance is at most (M - μ) * (μ - m), where μ is the weighted mean.

theorem weighted_bhatia_davis (hw_nonneg : ∀ i, 0 ≤ w i) (hw_sum : ∑ i, w i = 1)
    (hlam : ∀ i, m ≤ lam i ∧ lam i ≤ M) :
    (∑ i, w i * lam i ^ 2) - (∑ i, w i * lam i) ^ 2
      ≤ (M - ∑ i, w i * lam i) * (∑ i, w i * lam i - m)
Used by 2
Used byBhatia–Davis inequality · Popoviciu's inequality

TheoremPopoviciu's inequality#✓fully proved

Popoviciu's inequality, scalar weighted form: the weighted variance is at most ((M - m) / 2)².

theorem weighted_popoviciu (hw_nonneg : ∀ i, 0 ≤ w i) (hw_sum : ∑ i, w i = 1)
    (hlam : ∀ i, m ≤ lam i ∧ lam i ≤ M) :
    (∑ i, w i * lam i ^ 2) - (∑ i, w i * lam i) ^ 2 ≤ ((M - m) / 2) ^ 2
Uses 1 · Used by 1
Proof usesBhatia–Davis inequality
Used byPopoviciu's inequality

TheoremKantorovich's inequality#✓fully proved

Kantorovich's inequality, scalar weighted form: if the weights are nonnegative, sum to 1, every λ i lies in [m, M], and 0 < m, then (∑ w i * λ i) * (∑ w i / λ i) ≤ (M + m)² / (4 * m * M).

theorem weighted_kantorovich (hw_nonneg : ∀ i, 0 ≤ w i) (hw_sum : ∑ i, w i = 1)
    (hm : 0 < m) (hlam : ∀ i, m ≤ lam i ∧ lam i ≤ M) :
    (∑ i, w i * lam i) * (∑ i, w i / lam i) ≤ (M + m) ^ 2 / (4 * m * M)
Used by 1
Used byKantorovich's inequality

Operator

TheoremEigenvector basis equation with real eigenvalues#✓fully proved

Real-valued form of LinearMap.IsSymmetric.apply_eigenvectorBasis: the eigenvalue is a plain real scalar, with no ℝ → 𝕜 coercion.

theorem apply_eigenvectorBasis_real (hT : T.IsSymmetric)
    (hn : Module.finrank ℝ E = n) (i : Fin n) :
    T ((hT.eigenvectorBasis hn) i) = (hT.eigenvalues hn i) • (hT.eigenvectorBasis hn) i
Used by 4
Used byEigenvalues lie within the Rayleigh quotient bounds · Inverse quadratic form as a weighted average of reciprocal eigenvalues · Rayleigh quotient as a weighted average of eigenvalues · Second moment as a weighted average of squared eigenvalues

TheoremEigenvalues lie within the Rayleigh quotient bounds#✓fully proved

The eigenvalues of a symmetric operator lie in [m, M] whenever its Rayleigh quotients do.

theorem eigenvalue_mem_Icc_of_rayleigh_bounds (hT : T.IsSymmetric)
    (hn : Module.finrank ℝ E = n)
    (hray : ∀ x, m * ‖x‖ ^ 2 ≤ ⟪x, T x⟫_ℝ ∧ ⟪x, T x⟫_ℝ ≤ M * ‖x‖ ^ 2)
    (i : Fin n) :
    m ≤ hT.eigenvalues hn i ∧ hT.eigenvalues hn i ≤ M
Uses 1 · Used by 4
Proof usesEigenvector basis equation with real eigenvalues
Used byBhatia–Davis inequality · Inverse quadratic form as a weighted average of reciprocal eigenvalues · Kantorovich's inequality · Popoviciu's inequality

TheoremEigenbasis weights sum to the squared norm#✓fully proved

The eigenbasis weights sum to ‖x‖².

theorem sum_weights_eq_norm_sq (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n)
    (x : E) :
    ∑ i, ((hT.eigenvectorBasis hn).repr x i) ^ 2 = ‖x‖ ^ 2
Used by 4
Used byBhatia–Davis inequality · Kantorovich's inequality · Popoviciu's inequality · Operator variance as weighted squared deviation of eigenvalues

TheoremRayleigh quotient as a weighted average of eigenvalues#✓fully proved

The Rayleigh quotient is the weighted average of the eigenvalues, with weights ((eigenvectorBasis).repr x i)².

theorem rayleigh_eq_weighted_sum (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n)
    (x : E) :
    ⟪x, T x⟫_ℝ
      = ∑ i, ((hT.eigenvectorBasis hn).repr x i) ^ 2 * hT.eigenvalues hn i
Uses 1 · Used by 4
Proof usesEigenvector basis equation with real eigenvalues
Used byBhatia–Davis inequality · Kantorovich's inequality · Popoviciu's inequality · Operator variance as weighted squared deviation of eigenvalues

TheoremSecond moment as a weighted average of squared eigenvalues#✓fully proved

The second-moment quadratic form is the weighted average of the squared eigenvalues.

theorem second_moment_eq_weighted_sum (hT : T.IsSymmetric)
    (hn : Module.finrank ℝ E = n) (x : E) :
    ⟪x, T (T x)⟫_ℝ
      = ∑ i, ((hT.eigenvectorBasis hn).repr x i) ^ 2 * (hT.eigenvalues hn i) ^ 2
Uses 1 · Used by 3
Proof usesEigenvector basis equation with real eigenvalues
Used byBhatia–Davis inequality · Popoviciu's inequality · Operator variance as weighted squared deviation of eigenvalues

TheoremInverse quadratic form as a weighted average of reciprocal eigenvalues#✓fully proved

The quadratic form of a two-sided inverse is the weighted average of the reciprocal eigenvalues.

theorem inv_rayleigh_eq_weighted_sum_div (hT : T.IsSymmetric)
    (hn : Module.finrank ℝ E = n) (hm : 0 < m)
    (hray : ∀ x, m * ‖x‖ ^ 2 ≤ ⟪x, T x⟫_ℝ ∧ ⟪x, T x⟫_ℝ ≤ M * ‖x‖ ^ 2)
    (hTS : ∀ x, T (S x) = x) (hST : ∀ x, S (T x) = x) (x : E) :
    ⟪x, S x⟫_ℝ
      = ∑ i, ((hT.eigenvectorBasis hn).repr x i) ^ 2 / hT.eigenvalues hn i
Uses 2 · Used by 1
Proof usesEigenvector basis equation with real eigenvalues · Eigenvalues lie within the Rayleigh quotient bounds
Used byKantorovich's inequality

TheoremOperator variance as weighted squared deviation of eigenvalues#✓fully proved

The variance of T at a unit vector is the weighted squared deviation of the eigenvalues from the Rayleigh quotient.

theorem variance_eq_weighted_sum_sq (hT : T.IsSymmetric)
    (hn : Module.finrank ℝ E = n) (x : E) (hx : ‖x‖ = 1) :
    ⟪x, T (T x)⟫_ℝ - ⟪x, T x⟫_ℝ ^ 2
      = ∑ i, ((hT.eigenvectorBasis hn).repr x i) ^ 2
        * (hT.eigenvalues hn i - ⟪x, T x⟫_ℝ) ^ 2
Uses 4
Proof usesRayleigh quotient as a weighted average of eigenvalues · Second moment as a weighted average of squared eigenvalues · Eigenbasis weights sum to the squared norm · Weighted variance as weighted squared deviation from the mean

TheoremBhatia–Davis inequality#✓fully proved

Bhatia–Davis inequality for a symmetric operator: the variance of T at a unit vector is at most (M - μ) * (μ - m), where μ is the Rayleigh quotient.

theorem bhatia_davis_inequality (hT : T.IsSymmetric)
    (x : E) (hx : ‖x‖ = 1)
    (hray : ∀ x, m * ‖x‖ ^ 2 ≤ ⟪x, T x⟫_ℝ ∧ ⟪x, T x⟫_ℝ ≤ M * ‖x‖ ^ 2) :
    ⟪x, T (T x)⟫_ℝ - ⟪x, T x⟫_ℝ ^ 2
      ≤ (M - ⟪x, T x⟫_ℝ) * (⟪x, T x⟫_ℝ - m)
Uses 5
Proof usesEigenvalues lie within the Rayleigh quotient bounds · Rayleigh quotient as a weighted average of eigenvalues · Second moment as a weighted average of squared eigenvalues · Eigenbasis weights sum to the squared norm · Bhatia–Davis inequality

TheoremPopoviciu's inequality#✓fully proved

Popoviciu's inequality for a symmetric operator: the variance of T at a unit vector is at most ((M - m) / 2)².

theorem popoviciu_inequality (hT : T.IsSymmetric)
    (x : E) (hx : ‖x‖ = 1)
    (hray : ∀ x, m * ‖x‖ ^ 2 ≤ ⟪x, T x⟫_ℝ ∧ ⟪x, T x⟫_ℝ ≤ M * ‖x‖ ^ 2) :
    ⟪x, T (T x)⟫_ℝ - ⟪x, T x⟫_ℝ ^ 2 ≤ ((M - m) / 2) ^ 2
Uses 5
Proof usesEigenvalues lie within the Rayleigh quotient bounds · Rayleigh quotient as a weighted average of eigenvalues · Second moment as a weighted average of squared eigenvalues · Eigenbasis weights sum to the squared norm · Popoviciu's inequality

TheoremKantorovich's inequality#✓fully proved

Kantorovich's inequality for a symmetric operator: for a unit vector x, the product of the Rayleigh quotient of T and the Rayleigh quotient of its two-sided inverse S is at most (M + m)² / (4 * m * M).

theorem kantorovich_inequality (hT : T.IsSymmetric)
    (x : E) (hx : ‖x‖ = 1)
    (hray : ∀ x, m * ‖x‖ ^ 2 ≤ ⟪x, T x⟫_ℝ ∧ ⟪x, T x⟫_ℝ ≤ M * ‖x‖ ^ 2)
    (hm : 0 < m) (hTS : ∀ x, T (S x) = x) (hST : ∀ x, S (T x) = x) :
    ⟪x, T x⟫_ℝ * ⟪x, S x⟫_ℝ ≤ (M + m) ^ 2 / (4 * m * M)
Uses 5
Proof usesEigenvalues lie within the Rayleigh quotient bounds · Inverse quadratic form as a weighted average of reciprocal eigenvalues · Rayleigh quotient as a weighted average of eigenvalues · Eigenbasis weights sum to the squared norm · Kantorovich's inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.