2×2 block matrices and the Schur complement

This file proves properties of 2×2 block matrices [A B; C D] that relate to the Schur complement D - C*A⁻¹*B.

Some of the results here generalize to 2×2 matrices in a category, rather than just a ring. A few results in this direction can be found in the file CateogryTheory.Preadditive.Biproducts, especially the declarations CategoryTheory.Biprod.gaussian and CategoryTheory.Biprod.isoElim. Compare with Matrix.invertibleOfFromBlocks₁₁Invertible.

Main results

• Matrix.det_fromBlocks₁₁, Matrix.det_fromBlocks₂₂: determinant of a block matrix in terms of the Schur complement.
• Matrix.invOf_fromBlocks_zero₂₁_eq, Matrix.invOf_fromBlocks_zero₁₂_eq: the inverse of a block triangular matrix.
• Matrix.isUnit_fromBlocks_zero₂₁, Matrix.isUnit_fromBlocks_zero₁₂: invertibility of a block triangular matrix.
• Matrix.det_one_add_mul_comm: the Weinstein–Aronszajn identity.
• Matrix.PosSemidef.fromBlocks₁₁ and Matrix.PosSemidef.fromBlocks₂₂: If a matrix A is positive definite, then [A B; Bᴴ D] is postive semidefinite if and only if D - Bᴴ A⁻¹ B is postive semidefinite.

theorem Matrix.fromBlocks_eq_of_invertible₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α) (D : Matrix l n α) [Invertible A] : Matrix.fromBlocks A B C D = Matrix.fromBlocks 1 0 (C * ⅟A) 1 * Matrix.fromBlocks A 0 0 (D - C * ⅟A * B) * Matrix.fromBlocks 1 (⅟A * B) 0 1

LDU decomposition of a block matrix with an invertible top-left corner, using the Schur complement.

theorem Matrix.fromBlocks_eq_of_invertible₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] : Matrix.fromBlocks A B C D = Matrix.fromBlocks 1 (B * ⅟D) 0 1 * Matrix.fromBlocks (A - B * ⅟D * C) 0 0 D * Matrix.fromBlocks 1 0 (⅟D * C) 1

LDU decomposition of a block matrix with an invertible bottom-right corner, using the Schur complement.

Block triangular matrices

def Matrix.fromBlocksZero₂₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] : Invertible (Matrix.fromBlocks A B 0 D)

An upper-block-triangular matrix is invertible if its diagonal is.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.fromBlocksZero₁₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] : Invertible (Matrix.fromBlocks A 0 C D)

A lower-block-triangular matrix is invertible if its diagonal is.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.invOf_fromBlocks_zero₂₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] [Invertible (Matrix.fromBlocks A B 0 D)] : ⅟(Matrix.fromBlocks A B 0 D) = Matrix.fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D

theorem Matrix.invOf_fromBlocks_zero₁₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] [Invertible (Matrix.fromBlocks A 0 C D)] : ⅟(Matrix.fromBlocks A 0 C D) = Matrix.fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D

def Matrix.invertibleOfFromBlocksZero₂₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible (Matrix.fromBlocks A B 0 D)] : Invertible A × Invertible D

Both diagonal entries of an invertible upper-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).

Equations

• One or more equations did not get rendered due to their size.

def Matrix.invertibleOfFromBlocksZero₁₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible (Matrix.fromBlocks A 0 C D)] : Invertible A × Invertible D

Both diagonal entries of an invertible lower-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).

Equations

• One or more equations did not get rendered due to their size.

def Matrix.fromBlocksZero₂₁InvertibleEquiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) : Invertible (Matrix.fromBlocks A B 0 D) ≃ Invertible A × Invertible D

invertibleOfFromBlocksZero₂₁Invertible and Matrix.fromBlocksZero₂₁Invertible form an equivalence.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.fromBlocksZero₁₂InvertibleEquiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) : Invertible (Matrix.fromBlocks A 0 C D) ≃ Invertible A × Invertible D

invertibleOfFromBlocksZero₁₂Invertible and Matrix.fromBlocksZero₁₂Invertible form an equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.isUnit_fromBlocks_zero₂₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α} : IsUnit (Matrix.fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D

An upper block-triangular matrix is invertible iff both elements of its diagonal are.

This is a propositional form of Matrix.fromBlocksZero₂₁InvertibleEquiv.

@[simp]

theorem Matrix.isUnit_fromBlocks_zero₁₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α} : IsUnit (Matrix.fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D

A lower block-triangular matrix is invertible iff both elements of its diagonal are.

This is a propositional form of Matrix.fromBlocksZero₁₂InvertibleEquiv forms an iff.

theorem Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) (hAD : IsUnit A ↔ IsUnit D) : (Matrix.fromBlocks A B 0 D)⁻¹ = Matrix.fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

An expression for the inverse of an upper block-triangular matrix, when either both elements of diagonal are invertible, or both are not.

theorem Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) (hAD : IsUnit A ↔ IsUnit D) : (Matrix.fromBlocks A 0 C D)⁻¹ = Matrix.fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

An expression for the inverse of a lower block-triangular matrix, when either both elements of diagonal are invertible, or both are not.

2×2 block matrices

General 2×2 block matrices

def Matrix.fromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (A - B * ⅟D * C)] : Invertible (Matrix.fromBlocks A B C D)

A block matrix is invertible if the bottom right corner and the corresponding schur complement is.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.fromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (D - C * ⅟A * B)] : Invertible (Matrix.fromBlocks A B C D)

A block matrix is invertible if the top left corner and the corresponding schur complement is.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.invOf_fromBlocks₂₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (A - B * ⅟D * C)] [Invertible (Matrix.fromBlocks A B C D)] : ⅟(Matrix.fromBlocks A B C D) = Matrix.fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C))) (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

theorem Matrix.invOf_fromBlocks₁₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (D - C * ⅟A * B)] [Invertible (Matrix.fromBlocks A B C D)] : ⅟(Matrix.fromBlocks A B C D) = Matrix.fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B))) (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)

def Matrix.invertibleOfFromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (Matrix.fromBlocks A B C D)] : Invertible (A - B * ⅟D * C)

If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.invertibleOfFromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (Matrix.fromBlocks A B C D)] : Invertible (D - C * ⅟A * B)

If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.

Equations

• Matrix.invertibleOfFromBlocks₁₁Invertible A B C D = Matrix.invertibleOfFromBlocks₂₂Invertible D C B A

def Matrix.invertibleEquivFromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] : Invertible (Matrix.fromBlocks A B C D) ≃ Invertible (A - B * ⅟D * C)

Matrix.invertibleOfFromBlocks₂₂Invertible and Matrix.fromBlocks₂₂Invertible as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.invertibleEquivFromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] : Invertible (Matrix.fromBlocks A B C D) ≃ Invertible (D - C * ⅟A * B)

Matrix.invertibleOfFromBlocks₁₁Invertible and Matrix.fromBlocks₁₁Invertible as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.isUnit_fromBlocks_iff_of_invertible₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} [Invertible D] : IsUnit (Matrix.fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)

If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.

theorem Matrix.isUnit_fromBlocks_iff_of_invertible₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} [Invertible A] : IsUnit (Matrix.fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)

If the top-right element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.

Lemmas about Matrix.det

theorem Matrix.det_fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] : Matrix.det (Matrix.fromBlocks A B C D) = Matrix.det A * Matrix.det (D - C * ⅟A * B)

Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of the Schur complement.

@[simp]

theorem Matrix.det_fromBlocks_one₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) : Matrix.det (Matrix.fromBlocks 1 B C D) = Matrix.det (D - C * B)

theorem Matrix.det_fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] : Matrix.det (Matrix.fromBlocks A B C D) = Matrix.det D * Matrix.det (A - B * ⅟D * C)

Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms of the Schur complement.

@[simp]

theorem Matrix.det_fromBlocks_one₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) : Matrix.det (Matrix.fromBlocks A B C 1) = Matrix.det (A - B * C)

theorem Matrix.det_one_add_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) : Matrix.det (1 + A * B) = Matrix.det (1 + B * A)

The Weinstein–Aronszajn identity. Note the 1 on the LHS is of shape m×m, while the 1 on the RHS is of shape n×n.

theorem Matrix.det_mul_add_one_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) : Matrix.det (A * B + 1) = Matrix.det (B * A + 1)

Alternate statement of the Weinstein–Aronszajn identity

theorem Matrix.det_one_sub_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) : Matrix.det (1 - A * B) = Matrix.det (1 - B * A)

theorem Matrix.det_one_add_col_mul_row {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] (u : m → α) (v : m → α) : Matrix.det (1 + Matrix.col u * Matrix.row v) = 1 + Matrix.dotProduct v u

A special case of the Matrix determinant lemma for when A = I.

theorem Matrix.det_add_col_mul_row {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {A : Matrix m m α} (hA : IsUnit (Matrix.det A)) (u : m → α) (v : m → α) : Matrix.det (A + Matrix.col u * Matrix.row v) = Matrix.det A * Matrix.det (1 + Matrix.row v * A⁻¹ * Matrix.col u)

The Matrix determinant lemma

TODO: show the more general version without hA : IsUnit A.det as (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A) *ᵥ u.

theorem Matrix.det_add_mul {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α) (hA : IsUnit (Matrix.det A)) : Matrix.det (A + U * V) = Matrix.det A * Matrix.det (1 + V * A⁻¹ * U)

A generalization of the Matrix determinant lemma

Lemmas about ℝ and ℂ and other StarOrderedRings

def Matrix.«term_⊕ᵥ_» : Lean.TrailingParserDescr

Equations

• Matrix.«term_⊕ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.term_⊕ᵥ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ᵥ ") (Lean.ParserDescr.cat `term 66))

theorem Matrix.schur_complement_eq₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜] [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (x : m → 𝕜) (y : n → 𝕜) [Invertible A] (hA : Matrix.IsHermitian A) : Matrix.dotProduct (Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B (Matrix.conjTranspose B) D)) (Sum.elim x y) = Matrix.dotProduct (Matrix.vecMul (star (x + Matrix.mulVec (A⁻¹ * B) y)) A) (x + Matrix.mulVec (A⁻¹ * B) y) + Matrix.dotProduct (Matrix.vecMul (star y) (D - Matrix.conjTranspose B * A⁻¹ * B)) y

theorem Matrix.schur_complement_eq₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (x : m → 𝕜) (y : n → 𝕜) [Invertible D] (hD : Matrix.IsHermitian D) : Matrix.dotProduct (Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B (Matrix.conjTranspose B) D)) (Sum.elim x y) = Matrix.dotProduct (Matrix.vecMul (star (Matrix.mulVec (D⁻¹ * Matrix.conjTranspose B) x + y)) D) (Matrix.mulVec (D⁻¹ * Matrix.conjTranspose B) x + y) + Matrix.dotProduct (Matrix.vecMul (star x) (A - B * D⁻¹ * Matrix.conjTranspose B)) x

theorem Matrix.IsHermitian.fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜] [Fintype m] [DecidableEq m] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : Matrix.IsHermitian A) : Matrix.IsHermitian (Matrix.fromBlocks A B (Matrix.conjTranspose B) D) ↔ Matrix.IsHermitian (D - Matrix.conjTranspose B * A⁻¹ * B)

theorem Matrix.IsHermitian.fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : Matrix.IsHermitian D) : Matrix.IsHermitian (Matrix.fromBlocks A B (Matrix.conjTranspose B) D) ↔ Matrix.IsHermitian (A - B * D⁻¹ * Matrix.conjTranspose B)

theorem Matrix.PosSemidef.fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜] [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : Matrix.PosDef A) [Invertible A] : Matrix.PosSemidef (Matrix.fromBlocks A B (Matrix.conjTranspose B) D) ↔ Matrix.PosSemidef (D - Matrix.conjTranspose B * A⁻¹ * B)

theorem Matrix.PosSemidef.fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : Matrix.PosDef D) [Invertible D] : Matrix.PosSemidef (Matrix.fromBlocks A B (Matrix.conjTranspose B) D) ↔ Matrix.PosSemidef (A - B * D⁻¹ * Matrix.conjTranspose B)