Determinant inequalities for positive-semidefinite matrices

The determinant is monotone on the positive-semidefinite cone. Hadamard--Fischer bounds a block determinant by the product of its diagonal-block determinants. The overlapping-block version is the local Gram determinant inequality used when comparing the Euclidean volumes of an intersection and a sum of subspaces. The monotonicity and block statements include singular matrices and empty blocks, over either real or complex scalars.

For real positive-semidefinite n × n matrices, the inequality of arithmetic and geometric means for the eigenvalues gives det A ≤ (tr A / n) ^ n, and its mixed form det A * det B ≤ (tr (A * B) / n) ^ n is the pointwise step of the Aleksandrov–Bakelman–Pucci maximum principle. Read through the standard basis of ℝⁿ, it bounds det T det A by (∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ / n)ⁿ for a positive operator T (LinearMap.IsPositive.det_mul_det_le_sum_mul_apply_div_card_pow), where the principal part ∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ = tr (A M_T) (LinearMap.IsSymmetric.trace_mul_toMatrix) is nonnegative (LinearMap.IsPositive.sum_mul_apply_nonneg).

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, §7.8.
• J.-H. Evertse and R. G. Ferretti, A further improvement of the quantitative Subspace Theorem, §6.1, (6.12), for the subspace-height application.

theorem Matrix.PosSemidef.one_le_det_one_add {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] {B : Matrix n n 𝕜} (hB : B.PosSemidef) : 1 ≤ (1 + B).det

Adding a positive-semidefinite matrix to the identity cannot decrease its determinant.

theorem Matrix.PosSemidef.det_le_det_add {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) : A.det ≤ (A + B).det

Adding a positive-semidefinite matrix cannot decrease the determinant of a positive-semidefinite matrix, including when the first matrix is singular.

theorem Matrix.PosSemidef.det_le_det {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hAB : A ≤ B) : A.det ≤ B.det

The determinant is monotone for the Loewner order on positive-semidefinite matrices.

theorem Matrix.PosSemidef.det_fromBlocks_le {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {A : Matrix m m 𝕜} {B : Matrix m n 𝕜} {D : Matrix n n 𝕜} (h : (fromBlocks A B B.conjTranspose D).PosSemidef) : (fromBlocks A B B.conjTranspose D).det ≤ A.det * D.det

Hadamard--Fischer inequality. The determinant of a positive-semidefinite block matrix is at most the product of the diagonal-block determinants.

theorem Matrix.PosSemidef.det_mul_det_fromBlocks_le {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [Fintype p] [DecidableEq p] {A : Matrix m m 𝕜} {B : Matrix m n 𝕜} {C : Matrix m p 𝕜} {D : Matrix n n 𝕜} {E : Matrix n p 𝕜} {F : Matrix p p 𝕜} (h : (fromBlocks A (B.fromCols C) (B.fromCols C).conjTranspose (fromBlocks D E E.conjTranspose F)).PosSemidef) : A.det * (fromBlocks A (B.fromCols C) (B.fromCols C).conjTranspose (fromBlocks D E E.conjTranspose F)).det ≤ (fromBlocks A B B.conjTranspose D).det * (fromBlocks A C C.conjTranspose F).det

Koteljanskii's inequality for overlapping blocks. The product of the principal minors on the common block and on all three blocks is bounded by the product of the two intermediate principal minors. No block need be nonsingular.

theorem Matrix.PosSemidef.det_le_trace_div_card_pow {n : Type u_3} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) : A.det ≤ (A.trace / ↑(Fintype.card n)) ^ Fintype.card n

The determinant–trace inequality. The determinant of a real positive-semidefinite n × n matrix is at most the n-th power of the mean of its eigenvalues, det A ≤ (tr A / n) ^ n: the inequality of arithmetic and geometric means for the eigenvalues. For n = 0 both sides are 1.

theorem Matrix.PosSemidef.det_mul_det_le_trace_mul_div_card_pow {n : Type u_3} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) : A.det * B.det ≤ ((A * B).trace / ↑(Fintype.card n)) ^ Fintype.card n

The mixed determinant–trace inequality. For real positive-semidefinite n × n matrices A and B, det A * det B ≤ (tr (A * B) / n) ^ n.

theorem LinearMap.IsSymmetric.trace_mul_toMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] {T : EuclideanSpace ℝ ι →ₗ[ℝ] EuclideanSpace ℝ ι} (hT : T.IsSymmetric) (A : Matrix ι ι ℝ) : (A * (toMatrix (EuclideanSpace.basisFun ι ℝ).toBasis (EuclideanSpace.basisFun ι ℝ).toBasis) T).trace = ∑ i : ι, ∑ j : ι, A i j * (T (EuclideanSpace.single j 1)).ofLp i

For a symmetric operator T on ℝⁿ, the trace of A times the matrix of T is ∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ.

theorem LinearMap.IsPositive.sum_mul_apply_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {T : EuclideanSpace ℝ ι →ₗ[ℝ] EuclideanSpace ℝ ι} (hT : T.IsPositive) {A : Matrix ι ι ℝ} (hA : A.PosSemidef) : 0 ≤ ∑ i : ι, ∑ j : ι, A i j * (T (EuclideanSpace.single j 1)).ofLp i

The principal part of a positive operator. If T is a positive operator on ℝⁿ and A is positive semidefinite, then 0 ≤ ∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ.

theorem LinearMap.IsPositive.det_mul_det_le_sum_mul_apply_div_card_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {T : EuclideanSpace ℝ ι →ₗ[ℝ] EuclideanSpace ℝ ι} (hT : T.IsPositive) {A : Matrix ι ι ℝ} (hA : A.PosSemidef) : LinearMap.det T * A.det ≤ ((∑ i : ι, ∑ j : ι, A i j * (T (EuclideanSpace.single j 1)).ofLp i) / ↑(Fintype.card ι)) ^ Fintype.card ι

The determinant bound for a positive operator. If T is a positive operator on ℝⁿ and A is positive semidefinite, then det T det A ≤ (∑ᵢⱼ Aᵢⱼ (T eⱼ)ᵢ / n)ⁿ: the determinant–trace inequality Matrix.PosSemidef.det_mul_det_le_trace_mul_div_card_pow for A and the matrix of T. Applied to T = -D²u on the upper contact set, it bounds the Hessian determinant by the elliptic operator.