Positive definite matrices and matrix inequalities

Positive definite and semidefinite matrices, criteria for definiteness, and inequalities for their determinants, traces and eigenvalues.

• Hadamard's inequality and determinant bounds for positive semidefinite matrices
• Lidskii's eigenvalue inequality
• Minkowski's determinant inequality
• Fischer's determinant inequality
• Sylvester's criterion
• Von Neumann's trace inequality

TheoremHoffman–Wielandt inequality for Hermitian matrices#✓fully proved

Let \(A\) and \(B\) be Hermitian \(n \times n\) complex matrices with eigenvalues \(\lambda_1 \ge \dots \ge \lambda_n\) and \(\mu_1 \ge \dots \ge \mu_n\) respectively, counted with multiplicity. Then \(\sum_{i=1}^n (\lambda_i - \mu_i)^2 \le \sum_{i=1}^n \sum_{j=1}^n |A_{ij} - B_{ij}|^2\), that is, the left side is at most the squared Frobenius norm of \(A - B\).

theorem hoffman_wielandt_hermitian
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ)
    (hA : A.IsHermitian) (hB : B.IsHermitian) :
    let hA_sym := (Matrix.isSymmetric_toEuclideanLin_iff.mpr hA)
    let hB_sym := (Matrix.isSymmetric_toEuclideanLin_iff.mpr hB)
    ∑ i : Fin n, (hA_sym.eigenvalues finrank_euclideanSpace_fin i -
        hB_sym.eigenvalues finrank_euclideanSpace_fin i) ^ 2 ≤
      ∑ i : Fin n, ∑ j : Fin n, Complex.normSq (A i j - B i j)

Sources

• A. J. Hoffman and H. W. Wielandt, Duke Math. J. 20 (1953), DOI 10.1215/S0012-7094-53-02004-3.

TheoremLog-determinant trace inequality#✓fully proved

Let \(A\) and \(B\) be positive definite real square matrices indexed by a finite set with \(n\) elements. Then \(\log(\det A \cdot \det B) \le \operatorname{tr}(AB) - n\).

The eigenvalues \(\lambda\) of the positive definite matrix \(B^{1/2} A B^{1/2}\), where \(B^{1/2}\) is the positive semidefinite square root of \(B\), satisfy \(\log \lambda \le \lambda - 1\); this matrix has determinant \(\det A \det B\) and trace \(\operatorname{tr}(AB)\).

theorem log_det_mul_le_trace {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) :
    log (A.det * B.det) ≤ (A * B).trace - Fintype.card ι

Used by 2

Used byDempster's covariance-selection MLE · The weighted Gaussian MLE when the sample covariance is positive definite

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.