Documentation

Mathlib.LinearAlgebra.Matrix.SchurComplement

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 Mathlib/CategoryTheory/Preadditive/Biproducts.lean, 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 positive semidefinite if and only if D - Bᴴ A⁻¹ B is positive 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] :

fromBlocks A B C D = fromBlocks 1 0 (C * ⅟ A) 1 * fromBlocks A 0 0 (D - C * ⅟ A * B) * 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] :

fromBlocks A B C D = fromBlocks 1 (B * ⅟ D) 0 1 * fromBlocks (A - B * ⅟ D * C) 0 0 D * 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 (fromBlocks A B 0 D)

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

Equations

A.fromBlocksZero₂₁Invertible B D = (Matrix.fromBlocks A B 0 D).invertibleOfLeftInverse (Matrix.fromBlocks (⅟ A) (-(⅟ A * B * ⅟ D)) 0 ⅟ D) ⋯

Instances For

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 (fromBlocks A 0 C D)

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

Equations

A.fromBlocksZero₁₂Invertible C D = (Matrix.fromBlocks A 0 C D).invertibleOfLeftInverse (Matrix.fromBlocks (⅟ A) 0 (-(⅟ D * C * ⅟ A)) ⅟ D) ⋯

Instances For

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 (fromBlocks A B 0 D)] :

⅟ (fromBlocks A B 0 D) = 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 (fromBlocks A 0 C D)] :

⅟ (fromBlocks A 0 C D) = 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 (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

A.invertibleOfFromBlocksZero₂₁Invertible B D = (A.invertibleOfLeftInverse (⅟ (Matrix.fromBlocks A B 0 D)).toBlocks₁₁ ⋯, D.invertibleOfRightInverse (⅟ (Matrix.fromBlocks A B 0 D)).toBlocks₂₂ ⋯)

Instances For

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 (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

A.invertibleOfFromBlocksZero₁₂Invertible C D = (A.invertibleOfRightInverse (⅟ (Matrix.fromBlocks A 0 C D)).toBlocks₁₁ ⋯, D.invertibleOfLeftInverse (⅟ (Matrix.fromBlocks A 0 C D)).toBlocks₂₂ ⋯)

Instances For

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 (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.

Instances For

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 (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.

Instances For

@[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 (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 (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) :

(fromBlocks A B 0 D)⁻¹ = 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) :

(fromBlocks A 0 C D)⁻¹ = 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 (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.

Instances For

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 (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.

Instances For

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 (fromBlocks A B C D)] :

⅟ (fromBlocks A B C D) = 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 (fromBlocks A B C D)] :

⅟ (fromBlocks A B C D) = 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 (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

A.invertibleOfFromBlocks₂₂Invertible B C D = ((A - B * ⅟ D * C).invertibleOfFromBlocksZero₁₂Invertible 0 D).1

Instances For

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 (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

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

Instances For

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 (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.

Instances For

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 (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.

Instances For

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 (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 (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] :

(fromBlocks A B C D).det = A.det * (D - C * ⅟ A * B).det

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 α) :

(fromBlocks 1 B C D).det = (D - C * B).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 D] :

(fromBlocks A B C D).det = D.det * (A - B * ⅟ D * C).det

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 α) :

(fromBlocks A B C 1).det = (A - B * C).det

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 α) :

(1 + A * B).det = (1 + B * A).det

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 α) :

(A * B + 1).det = (B * A + 1).det

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 α) :

(1 - A * B).det = (1 - B * A).det

theorem Matrix.det_one_add_replicateCol_mul_replicateRow {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] (u v : m → α) :

(1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u

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

@[deprecated Matrix.det_one_add_replicateCol_mul_replicateRow (since := "2025-03-20")]

theorem Matrix.det_one_add_col_mul_row {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] (u v : m → α) :

(1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u

Alias of Matrix.det_one_add_replicateCol_mul_replicateRow.

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

theorem Matrix.det_add_replicateCol_mul_replicateRow {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] {A : Matrix m m α} (hA : IsUnit A.det) (u v : m → α) :

(A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

The Matrix determinant lemma

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

@[deprecated Matrix.det_add_replicateCol_mul_replicateRow (since := "2025-03-20")]

theorem Matrix.det_add_col_mul_row {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] {A : Matrix m m α} (hA : IsUnit A.det) (u v : m → α) :

(A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Alias of Matrix.det_add_replicateCol_mul_replicateRow.

The Matrix determinant lemma

TODO: show the more general version without hA : IsUnit A.det as (A + replicateCol u * replicateRow 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 A.det) :

(A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

A generalization of the Matrix determinant lemma

Lemmas about `ℝ` and `ℂ` and other `StarOrderedRing`s #

def Matrix.«term_⊕ᵥ_» :

Lean.TrailingParserDescr

Notation for Sum.elim, scoped within the Matrix namespace.

Equations

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

Instances For

theorem Matrix.schur_complement_eq₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [StarRing 𝕜] [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 : A.IsHermitian) :

vecMul (star (Sum.elim x y)) (fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y = vecMul (star (x + (A⁻¹ * B).mulVec y)) A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) + vecMul (star y) (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ y

theorem Matrix.schur_complement_eq₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [StarRing 𝕜] [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 : D.IsHermitian) :

vecMul (star (Sum.elim x y)) (fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y = vecMul (star ((D⁻¹ * B.conjTranspose).mulVec x + y)) D ⬝ᵥ ((D⁻¹ * B.conjTranspose).mulVec x + y) + vecMul (star x) (A - B * D⁻¹ * B.conjTranspose) ⬝ᵥ x

theorem Matrix.IsHermitian.fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [StarRing 𝕜] [Fintype m] [DecidableEq m] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : A.IsHermitian) :

(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian

theorem Matrix.IsHermitian.fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [StarRing 𝕜] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : D.IsHermitian) :

(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian

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

(fromBlocks A B B.conjTranspose D).PosSemidef ↔ (D - B.conjTranspose * A⁻¹ * B).PosSemidef

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

(fromBlocks A B B.conjTranspose D).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef