mathlib documentation

linear_algebra.matrix.schur_complement

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 #

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