Schur complement #
This file proves properties of the Schur complement D - C A⁻¹ B of a block matrix [A B; C D].
The determinant of a block matrix in terms of the Schur complement is expressed in the lemmas
matrix.det_from_blocks₁₁ and matrix.det_from_blocks₂₂ in the file
linear_algebra.matrix.nonsingular_inverse.
Main result #
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.schur_complement_eq₁₁
{n : Type u_1}
{m : Type u_2}
{𝕜 : Type u_3}
[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₂₂
{n : Type u_1}
{m : Type u_2}
{𝕜 : Type u_3}
[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₁₁
{n : Type u_1}
{m : Type u_2}
{𝕜 : Type u_3}
[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₂₂
{n : Type u_1}
{m : Type u_2}
{𝕜 : Type u_3}
[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₁₁
{n : Type u_1}
{m : Type u_2}
{𝕜 : Type u_3}
[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₂₂
{n : Type u_1}
{m : Type u_2}
{𝕜 : Type u_3}
[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