Minkowski's determinant inequality

TheoremMinkowski's determinant inequality#✓fully proved

For positive semidefinite A and B, (det (A + B)) ^ (1 / n) ≥ (det A) ^ (1 / n) + (det B) ^ (1 / n).

theorem PosSemidef.minkowski_det (hA : A.PosSemidef) (hB : B.PosSemidef)
    (hn : 0 < n) :
    (A.det).re ^ ((n : ℝ)⁻¹) + (B.det).re ^ ((n : ℝ)⁻¹) ≤
      ((A + B).det).re ^ ((n : ℝ)⁻¹)

Used by 1

Used byMonotonicity of the determinant on the positive semidefinite cone

TheoremMonotonicity of the determinant on the positive semidefinite cone#✓fully proved

det B ≤ det (A + B) for A and B positive semidefinite.

theorem PosSemidef.det_le_det_add (hA : A.PosSemidef) (hB : B.PosSemidef) :
    (B.det).re ≤ ((A + B).det).re

Uses 1 · Used by 1

Proof usesMinkowski's determinant inequality

Used byMonotonicity of the determinant on the positive semidefinite cone

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.