Hadamard's inequality and determinant bounds for positive semidefinite matrices

TheoremHadamard's determinant inequality#✓fully proved

For every natural number \(n\) and every \(n \times n\) complex matrix \(A = (a_{ij})\),

\[|\det A| \le \prod_{i=1}^{n} \Big( \sum_{j=1}^{n} |a_{ij}|^2 \Big)^{1/2},\]

that is, the absolute value of the determinant of \(A\) is at most the product of the Euclidean lengths of its rows.

public theorem hadamard_determinant_inequality {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℂ) :
    ‖A.det‖ ≤ ∏ i : Fin n, Real.sqrt (∑ j : Fin n, Complex.normSq (A i j))

Sources

• J. Hadamard, Résolution d'une question relative aux déterminants, Bulletin des Sciences Mathématiques 17 (1893), 240–246.

Used by 1

Used byHadamard's inequality for positive semidefinite matrices

TheoremHadamard's inequality for positive semidefinite matrices#✓fully proved

Let \(A\) be a positive semidefinite complex \(n \times n\) matrix. Then the real part of the determinant of \(A\) is at most the product of the real parts of its diagonal entries: \(\operatorname{Re} \det A \le \prod_{i=1}^{n} \operatorname{Re} A_{ii}\).

theorem PosSemidef.det_re_le_prod_diag_re (hA : A.PosSemidef) :
    (A.det).re ≤ ∏ i, (A i i).re

Uses 1

Proof usesHadamard's determinant inequality

TheoremAM–GM inequality for the determinant of a positive semidefinite matrix#✓fully proved

Let \(n \ge 1\) and let \(A\) be a positive semidefinite complex \(n \times n\) matrix. Then \((\operatorname{Re} \det A)^{1/n} \le \operatorname{Re}(\operatorname{tr} A)/n\).

This is the arithmetic–geometric mean inequality for the eigenvalues of \(A\).

theorem PosSemidef.geomMean_det_le_trace_div (hA : A.PosSemidef) (hn : 0 < n) :
    (A.det).re ^ ((n : ℝ)⁻¹) ≤ (A.trace).re / (n : ℝ)

Used by 1

Used byAM–GM inequality for the determinant of a positive semidefinite matrix, power form

TheoremAM–GM inequality for the determinant of a positive semidefinite matrix, power form#✓fully proved

Let \(n \ge 1\) and let \(A\) be a positive semidefinite complex \(n \times n\) matrix. Then \(\operatorname{Re} \det A \le (\operatorname{Re}(\operatorname{tr} A)/n)^n\).

theorem PosSemidef.det_re_le_pow_trace_div (hA : A.PosSemidef) (hn : 0 < n) :
    (A.det).re ≤ ((A.trace).re / (n : ℝ)) ^ n

Uses 1

Proof usesAM–GM inequality for the determinant of a positive semidefinite matrix

TheoremEquality in the AM–GM bound for the determinant#✓fully proved

Let \(n \ge 1\) and let \(A\) be a positive semidefinite complex \(n \times n\) matrix. Then \((\operatorname{Re} \det A)^{1/n} = \operatorname{Re}(\operatorname{tr} A)/n\) if and only if \(A = cI\) for some real number \(c \ge 0\), where \(I\) is the \(n \times n\) identity matrix.

theorem PosSemidef.amgm_eq_iff (hA : A.PosSemidef) (hn : 0 < n) :
    (A.det).re ^ ((n : ℝ)⁻¹) = (A.trace).re / (n : ℝ) ↔
      ∃ c : ℝ, 0 ≤ c ∧ A = (c : ℂ) • (1 : Matrix (Fin n) (Fin n) ℂ)

TheoremThe trace of a product of positive semidefinite matrices has nonnegative real part#✓fully proved

Let \(A\) and \(B\) be positive semidefinite complex \(n \times n\) matrices. Then the real part of the trace of \(AB\) is nonnegative: \(\operatorname{Re} \operatorname{tr}(AB) \ge 0\).

theorem PosSemidef.trace_mul_nonneg_re (hA : A.PosSemidef) (hB : B.PosSemidef) :
    0 ≤ ((A * B).trace).re

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.