Minkowski's determinant inequality

For positive semidefinite real n × n matrices A and B, with n ≥ 1,

det A ^ (1 / n) + det B ^ (1 / n) ≤ det (A + B) ^ (1 / n).

Since det (c • A) ^ (1 / n) = c * det A ^ (1 / n) for c ≥ 0, this says that A ↦ det A ^ (1 / n) is concave on the convex cone of positive semidefinite matrices. The same statements hold for positive operators on a finite-dimensional real inner product space of dimension n, by passing to the matrix in an orthonormal basis.

This concavity is the matrix inequality behind the displacement convexity of internal energies in optimal transport. Along the interpolation x ↦ (1 - t) • x + t • ∇u x of the gradient of a convex function u, the Jacobian matrix (1 - t) • 1 + t • ∇²u x moves along a segment of positive semidefinite matrices, so t ↦ det ((1 - t) • 1 + t • ∇²u x) ^ (1 / n) is concave on [0, 1]; McCann's condition on an internal energy is exactly what turns this into convexity of the energy.

The proof first treats A = 1: with μ i ≥ 0 the eigenvalues of B, the inequality reads 1 + (∏ i, μ i) ^ (1 / n) ≤ (∏ i, (1 + μ i)) ^ (1 / n), the superadditivity of the geometric mean (Real.prod_rpow_add_prod_rpow_le_prod_add_rpow). A positive definite A factors as C * Cᵀ with C invertible, and congruence by C⁻¹ reduces the general inequality to that case. If neither matrix is positive definite then both determinants vanish and there is nothing to prove.

Main statements

• Matrix.PosSemidef.det_rpow_add_det_rpow_le: Minkowski's determinant inequality.
• Matrix.concaveOn_det_rpow: A ↦ det A ^ (1 / n) is concave on the positive semidefinite matrices.
• LinearMap.IsPositive.det_rpow_add_det_rpow_le and LinearMap.concaveOn_det_rpow: the same for positive operators on a finite-dimensional real inner product space.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press 2013, Section 7.8 (the Minkowski determinant theorem).
• R. J. McCann, A convexity principle for interacting gases, Adv. Math. 128 (1997), 153--179.

theorem Matrix.PosSemidef.det_rpow_add_det_rpow_le {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) : A.det ^ (↑(Fintype.card n))⁻¹ + B.det ^ (↑(Fintype.card n))⁻¹ ≤ (A + B).det ^ (↑(Fintype.card n))⁻¹

Minkowski's determinant inequality. For positive semidefinite real n × n matrices A and B with n ≥ 1, det A ^ (1 / n) + det B ^ (1 / n) ≤ det (A + B) ^ (1 / n).

theorem Matrix.concaveOn_det_rpow {n : Type u_1} [Fintype n] [DecidableEq n] : ConcaveOn ℝ {A : Matrix n n ℝ | A.PosSemidef} fun (A : Matrix n n ℝ) => A.det ^ (↑(Fintype.card n))⁻¹

A ↦ det A ^ (1 / n) is concave on the positive semidefinite real n × n matrices.

theorem LinearMap.IsPositive.det_rpow_add_det_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {A B : E →ₗ[ℝ] E} (hA : A.IsPositive) (hB : B.IsPositive) : LinearMap.det A ^ (↑(Module.finrank ℝ E))⁻¹ + LinearMap.det B ^ (↑(Module.finrank ℝ E))⁻¹ ≤ LinearMap.det (A + B) ^ (↑(Module.finrank ℝ E))⁻¹

Minkowski's determinant inequality for positive operators: on a nonzero real inner product space of finite dimension n, det A ^ (1 / n) + det B ^ (1 / n) ≤ det (A + B) ^ (1 / n).

theorem LinearMap.concaveOn_det_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : ConcaveOn ℝ {A : E →ₗ[ℝ] E | A.IsPositive} fun (A : E →ₗ[ℝ] E) => LinearMap.det A ^ (↑(Module.finrank ℝ E))⁻¹

On a finite-dimensional real inner product space of dimension n, A ↦ det A ^ (1 / n) is concave on the positive operators.