mathlib3 documentation

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 #

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 : matrix m m α) (B : matrix m n α) (C : matrix l m α) (D : matrix l n α) [invertible A] :
matrix.from_blocks A B C D = ((matrix.from_blocks 1 0 (C.mul ( A)) 1).mul (matrix.from_blocks A 0 0 (D - (C.mul ( A)).mul B))).mul (matrix.from_blocks 1 (( 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 : matrix l m α) (B : matrix l n α) (C : matrix n m α) (D : matrix n n α) [invertible D] :
matrix.from_blocks A B C D = ((matrix.from_blocks 1 (B.mul ( D)) 0 1).mul (matrix.from_blocks (A - (B.mul ( D)).mul C) 0 0 D)).mul (matrix.from_blocks 1 0 (( 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 : matrix m m α) (B : matrix m n α) (D : matrix n 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 : matrix m m α) (C : matrix n m α) (D : matrix n 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 : matrix m m α) (B : matrix m n α) (D : matrix n n α) [invertible A] [invertible D] [invertible (matrix.from_blocks A B 0 D)] :
(matrix.from_blocks A B 0 D) = matrix.from_blocks ( A) (-(( 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 : matrix m m α) (C : matrix n m α) (D : matrix n n α) [invertible A] [invertible D] [invertible (matrix.from_blocks A 0 C D)] :
(matrix.from_blocks A 0 C D) = matrix.from_blocks ( A) 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 : matrix m m α) (B : matrix m n α) (D : matrix n n α) [invertible (matrix.from_blocks A B 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 : matrix m m α) (C : matrix n m α) (D : matrix n n α) [invertible (matrix.from_blocks A 0 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 : matrix m m α) (B : matrix m n α) (D : matrix n 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 : matrix m m α) (C : matrix n m α) (D : matrix n 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 : matrix m m α} {B : matrix m n α} {D : matrix n 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 : matrix m m α} {C : matrix n m α} {D : matrix n 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 : matrix m m α) (B : matrix m n α) (D : matrix n n α) (hAD : is_unit A is_unit 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 : matrix m m α) (C : matrix n m α) (D : matrix n n α) (hAD : is_unit A is_unit 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible D] [invertible (A - (B.mul ( D)).mul C)] [invertible (matrix.from_blocks A B C D)] :
(matrix.from_blocks A B 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible A] [invertible (D - (C.mul ( A)).mul B)] [invertible (matrix.from_blocks A B C D)] :
(matrix.from_blocks A B 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible D] [invertible (matrix.from_blocks A B 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible A] [invertible (matrix.from_blocks A B 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
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 : matrix m m α} {B : matrix m n α} {C : matrix n m α} {D : matrix n n α} [invertible D] :
is_unit (matrix.from_blocks A B 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 : matrix m m α} {B : matrix m n α} {C : matrix n m α} {D : matrix n n α} [invertible A] :
is_unit (matrix.from_blocks A B 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible A] :
(matrix.from_blocks A B 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 : matrix m n α) (C : matrix n m α) (D : matrix n n α) :
(matrix.from_blocks 1 B 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible D] :
(matrix.from_blocks A B 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 : matrix m m α) (B : matrix m n α) (C : matrix n m α) :
(matrix.from_blocks A B 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 : matrix m n α) (B : matrix n 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 : matrix m n α) (B : matrix n 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 : matrix m n α) (B : matrix n 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 α) :

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 : matrix m m 𝕜} (B : matrix m n 𝕜) (D : matrix n n 𝕜) (x : m 𝕜) (y : n 𝕜) [invertible A] (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 m] [decidable_eq m] {A : matrix m m 𝕜} (B : matrix m n 𝕜) (D : matrix n 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 : matrix m m 𝕜) (B : matrix m n 𝕜) {D : matrix n 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 : matrix m m 𝕜} (B : matrix m n 𝕜) (D : matrix n 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 : matrix m m 𝕜) (B : matrix m n 𝕜) {D : matrix n n 𝕜} (hD : D.pos_def) [invertible D] :