English
If A is Hermitian and invertible, then the block matrix fromBlocks(A,B,B^H,D) is Hermitian iff the Schur complement D - B^H A^{-1} B is Hermitian.
Русский
Если A Герметова и обратима, то блочно-матрица изBlocks(A,B,B^H,D) Гермитова тогда и только тогда, когдаSchur-комплемент D - B^H A^{-1} B Гермитова.
LaTeX
$$$\\text{FromBlocks}(A,B,B^{\\mathrm{H}},D) \\text{ Hermitian } \\iff (D - B^{\\mathrm{H}} A^{-1} B) \\text{ Hermitian}$$$
Lean4
theorem schur_complement_eq₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m α} (B : Matrix m n α)
(D : Matrix n n α) (x : m → α) (y : n → α) [Invertible A] (hA : A.IsHermitian) :
(star (x ⊕ᵥ y)) ᵥ* (Matrix.fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
(star (x + (A⁻¹ * B) *ᵥ y)) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B) *ᵥ y) + (star y) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y :=
by
simp [Function.star_sumElim, vecMul_fromBlocks, add_vecMul, dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, hA.eq,
conjTranspose_nonsing_inv, star_mulVec]
abel
