Fischer's determinant inequality

TheoremDeterminant at least one when W minus identity is positive semidefinite#✓fully proved

If W - 1 is positive semidefinite, then 1 ≤ det W, since every eigenvalue of W is at least 1.

theorem one_le_det_of_posSemidef_sub_one {n : Type*} [Fintype n] [DecidableEq n]
    {W : Matrix n n ℝ} (hW : W.IsHermitian) (h : (W - 1).PosSemidef) :
    1 ≤ W.det

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

Monotonicity of the determinant on the positive semidefinite cone: if S and D - S are positive semidefinite, then det S ≤ det D.

theorem det_le_det_of_posSemidef_le {n : Type*} [Fintype n] [DecidableEq n]
    {S D : Matrix n n ℝ} (hS : S.PosSemidef) (hSD : (D - S).PosSemidef) :
    S.det ≤ D.det

Uses 1 · Used by 1

Proof usesMonotonicity of the determinant on the positive semidefinite cone

Used byFischer's determinant inequality

TheoremFischer's determinant inequality#✓fully proved

For a positive semidefinite block matrix [[A, B], [Bᴴ, D]] with real entries, det [[A, B], [Bᴴ, D]] ≤ det A * det D.

theorem fischer_det_fromBlocks_le {m n : Type*} [Fintype m] [Fintype n]
    [DecidableEq m] [DecidableEq n] {A : Matrix m m ℝ} {B : Matrix m n ℝ}
    {D : Matrix n n ℝ} (hM : (Matrix.fromBlocks A B Bᴴ D).PosSemidef) :
    (Matrix.fromBlocks A B Bᴴ D).det ≤ A.det * D.det

Uses 1

Proof usesMonotonicity of the determinant on the positive semidefinite cone

TheoremEquality case of Fischer's inequality#✓fully proved

For A and D positive definite and [[A, B], [Bᴴ, D]] positive semidefinite, det [[A, B], [Bᴴ, D]] = det A * det D iff B = 0.

theorem fischer_det_fromBlocks_eq_iff {m n : Type*} [Fintype m] [Fintype n]
    [DecidableEq m] [DecidableEq n] {A : Matrix m m ℝ} {B : Matrix m n ℝ}
    {D : Matrix n n ℝ} (hA : A.PosDef) (hD : D.PosDef)
    (hM : (Matrix.fromBlocks A B Bᴴ D).PosSemidef) :
    (Matrix.fromBlocks A B Bᴴ D).det = A.det * D.det ↔ B = 0

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.