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