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.
Main results #
matrix.det_from_blocks₁₁,matrix.det_from_blocks₂₂: determinant of a block matrix in terms of the Schur complement.matrix.det_one_add_mul_comm: the Weinstein–Aronszajn identity.matrix.schur_complement_pos_semidef_iff: If a matrixAis positive definite, then[A B; Bᴴ D]is postive semidefinite if and only ifD - Bᴴ A⁻¹ Bis 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 : 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.
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] :
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 α) :
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] :
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 α) :
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 α) :
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_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 + matrix.dot_product v u
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) :
matrix.dot_product (matrix.vec_mul (has_star.star (sum.elim x y)) (matrix.from_blocks A B B.conj_transpose D)) (sum.elim x y) = matrix.dot_product (matrix.vec_mul (has_star.star (x + (A⁻¹.mul B).mul_vec y)) A) (x + (A⁻¹.mul B).mul_vec y) + matrix.dot_product (matrix.vec_mul (has_star.star y) (D - (B.conj_transpose.mul A⁻¹).mul B)) y
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 : matrix m m 𝕜)
(B : matrix m n 𝕜)
{D : matrix n n 𝕜}
(x : m → 𝕜)
(y : n → 𝕜)
[invertible D]
(hD : D.is_hermitian) :
matrix.dot_product (matrix.vec_mul (has_star.star (sum.elim x y)) (matrix.from_blocks A B B.conj_transpose D)) (sum.elim x y) = matrix.dot_product (matrix.vec_mul (has_star.star ((D⁻¹.mul B.conj_transpose).mul_vec x + y)) D) ((D⁻¹.mul B.conj_transpose).mul_vec x + y) + matrix.dot_product (matrix.vec_mul (has_star.star x) (A - (B.mul D⁻¹).mul B.conj_transpose)) x
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) :
(matrix.from_blocks A B B.conj_transpose D).is_hermitian ↔ (D - (B.conj_transpose.mul A⁻¹).mul B).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) :
(matrix.from_blocks A B B.conj_transpose D).is_hermitian ↔ (A - (B.mul D⁻¹).mul B.conj_transpose).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] :
(matrix.from_blocks A B B.conj_transpose D).pos_semidef ↔ (D - (B.conj_transpose.mul A⁻¹).mul B).pos_semidef
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] :
(matrix.from_blocks A B B.conj_transpose D).pos_semidef ↔ (A - (B.mul D⁻¹).mul B.conj_transpose).pos_semidef