# mathlib3documentation

linear_algebra.matrix.schur_complement

# 2×2 block matrices and the Schur complement #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 the file cateogry_theory.preadditive.biproducts, especially the declarations category_theory.biprod.gaussian and category_theory.biprod.iso_elim. Compare with matrix.invertible_of_from_blocks₁₁_invertible.

## Main results #

• matrix.det_from_blocks₁₁, matrix.det_from_blocks₂₂: determinant of a block matrix in terms of the Schur complement.
• matrix.inv_of_from_blocks_zero₂₁_eq, matrix.inv_of_from_blocks_zero₁₂_eq: the inverse of a block triangular matrix.
• matrix.is_unit_from_blocks_zero₂₁, matrix.is_unit_from_blocks_zero₁₂: invertibility of a block triangular matrix.
• matrix.det_one_add_mul_comm: the Weinstein–Aronszajn identity.
• matrix.schur_complement_pos_semidef_iff : 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.from_blocks_eq_of_invertible₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype l] [fintype m] [fintype n] [decidable_eq l] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible A] :
C D = 0 (C.mul ( A)) 1).mul 0 (D - (C.mul ( A)).mul B))).mul (( A).mul B) 0 1)

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

theorem matrix.from_blocks_eq_of_invertible₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype l] [fintype m] [fintype n] [decidable_eq l] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible D] :
C D = (B.mul ( D)) 0 1).mul (matrix.from_blocks (A - (B.mul ( D)).mul C) 0 0 D)).mul (( D).mul C) 1)

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

#### Block triangular matrices #

def matrix.from_blocks_zero₂₁_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (D : n α) [invertible A] [invertible D] :

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

Equations
def matrix.from_blocks_zero₁₂_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (C : m α) (D : n α) [invertible A] [invertible D] :

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

Equations
theorem matrix.inv_of_from_blocks_zero₂₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (D : n α) [invertible A] [invertible D] [invertible 0 D)] :
0 D) = (-(( A).mul B).mul ( D)) 0 ( D)
theorem matrix.inv_of_from_blocks_zero₁₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (C : m α) (D : n α) [invertible A] [invertible D] [invertible C D)] :
C D) = 0 (-(( D).mul C).mul ( A)) ( D)
def matrix.invertible_of_from_blocks_zero₂₁_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (D : n α) [invertible 0 D)] :

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

Equations
def matrix.invertible_of_from_blocks_zero₁₂_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (C : m α) (D : n α) [invertible C D)] :

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

Equations
def matrix.from_blocks_zero₂₁_invertible_equiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (D : n α) :

invertible_of_from_blocks_zero₂₁_invertible and from_blocks_zero₂₁_invertible form an equivalence.

Equations
def matrix.from_blocks_zero₁₂_invertible_equiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (C : m α) (D : n α) :

invertible_of_from_blocks_zero₁₂_invertible and from_blocks_zero₁₂_invertible form an equivalence.

Equations
@[simp]
theorem matrix.is_unit_from_blocks_zero₂₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] {A : m α} {B : n α} {D : n α} :

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

This is a propositional form of matrix.from_blocks_zero₂₁_invertible_equiv.

@[simp]
theorem matrix.is_unit_from_blocks_zero₁₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] {A : m α} {C : m α} {D : n α} :

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

This is a propositional form of matrix.from_blocks_zero₁₂_invertible_equiv forms an iff.

theorem matrix.inv_from_blocks_zero₂₁_of_is_unit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (D : n α) (hAD : ) :
0 D)⁻¹ = (-(A⁻¹.mul B).mul 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_from_blocks_zero₁₂_of_is_unit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (C : m α) (D : n α) (hAD : ) :
C D)⁻¹ = (-(D⁻¹.mul C).mul 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.from_blocks₂₂_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible D] [invertible (A - (B.mul ( D)).mul C)] :

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

Equations
def matrix.from_blocks₁₁_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible A] [invertible (D - (C.mul ( A)).mul B)] :

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

Equations
theorem matrix.inv_of_from_blocks₂₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible D] [invertible (A - (B.mul ( D)).mul C)] [invertible C D)] :
C D) = matrix.from_blocks ( (A - (B.mul ( D)).mul C)) (-(( (A - (B.mul ( D)).mul C)).mul B).mul ( D)) (-(( D).mul C).mul ( (A - (B.mul ( D)).mul C))) ( D + (((( D).mul C).mul ( (A - (B.mul ( D)).mul C))).mul B).mul ( D))
theorem matrix.inv_of_from_blocks₁₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible A] [invertible (D - (C.mul ( A)).mul B)] [invertible C D)] :
C D) = matrix.from_blocks ( A + (((( A).mul B).mul ( (D - (C.mul ( A)).mul B))).mul C).mul ( A)) (-(( A).mul B).mul ( (D - (C.mul ( A)).mul B))) (-(( (D - (C.mul ( A)).mul B)).mul C).mul ( A)) ( (D - (C.mul ( A)).mul B))
def matrix.invertible_of_from_blocks₂₂_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible D] [invertible C D)] :
invertible (A - (B.mul ( D)).mul C)

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

Equations
def matrix.invertible_of_from_blocks₁₁_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible A] [invertible C D)] :
invertible (D - (C.mul ( A)).mul B)

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

Equations
def matrix.invertible_equiv_from_blocks₂₂_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible D] :
invertible C D) invertible (A - (B.mul ( D)).mul C)

matrix.invertible_of_from_blocks₂₂_invertible and matrix.from_blocks₂₂_invertible as an equivalence.

Equations
def matrix.invertible_equiv_from_blocks₁₁_invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible A] :
invertible C D) invertible (D - (C.mul ( A)).mul B)

matrix.invertible_of_from_blocks₁₁_invertible and matrix.from_blocks₁₁_invertible as an equivalence.

Equations
theorem matrix.is_unit_from_blocks_iff_of_invertible₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] {A : m α} {B : n α} {C : m α} {D : n α} [invertible D] :
is_unit C D) is_unit (A - (B.mul ( D)).mul 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.is_unit_from_blocks_iff_of_invertible₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] {A : m α} {B : n α} {C : m α} {D : n α} [invertible A] :
is_unit C D) is_unit (D - (C.mul ( A)).mul 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_from_blocks₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible A] :
C D).det = A.det * (D - (C.mul ( A)).mul 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_from_blocks_one₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (B : n α) (C : m α) (D : n α) :
C D).det = (D - C.mul B).det
theorem matrix.det_from_blocks₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) (D : n α) [invertible D] :
C D).det = D.det * (A - (B.mul ( D)).mul 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_from_blocks_one₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : m α) (B : n α) (C : m α) :
C 1).det = (A - B.mul C).det
theorem matrix.det_one_add_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) :
(1 + A.mul B).det = (1 + B.mul 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] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) :
(A.mul B + 1).det = (B.mul 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] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) :
(1 - A.mul B).det = (1 - B.mul A).det
theorem matrix.det_one_add_col_mul_row {m : Type u_2} {α : Type u_4} [fintype m] [decidable_eq m] [comm_ring α] (u v : m α) :
(1 + (matrix.col u).mul (matrix.row v)).det = 1 +

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

TODO: show this more generally.

### Lemmas about ℝ and ℂ#

theorem matrix.schur_complement_eq₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [is_R_or_C 𝕜] [fintype m] [decidable_eq m] [fintype n] {A : m 𝕜} (B : n 𝕜) (D : n 𝕜) (x : m 𝕜) (y : n 𝕜) [invertible A] (hA : A.is_hermitian) :
theorem matrix.schur_complement_eq₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [is_R_or_C 𝕜] [fintype m] [fintype n] [decidable_eq n] (A : m 𝕜) (B : n 𝕜) {D : n 𝕜} (x : m 𝕜) (y : n 𝕜) [invertible D] (hD : D.is_hermitian) :
theorem matrix.is_hermitian.from_blocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [is_R_or_C 𝕜] [fintype m] [decidable_eq m] {A : m 𝕜} (B : n 𝕜) (D : n 𝕜) (hA : A.is_hermitian) :
theorem matrix.is_hermitian.from_blocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] (A : m 𝕜) (B : n 𝕜) {D : n 𝕜} (hD : D.is_hermitian) :
theorem matrix.pos_semidef.from_blocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [is_R_or_C 𝕜] [fintype m] [decidable_eq m] [fintype n] {A : m 𝕜} (B : n 𝕜) (D : n 𝕜) (hA : A.pos_def) [invertible A] :
theorem matrix.pos_semidef.from_blocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [is_R_or_C 𝕜] [fintype m] [fintype n] [decidable_eq n] (A : m 𝕜) (B : n 𝕜) {D : n 𝕜} (hD : D.pos_def) [invertible D] :