English
If A is Hermitian, then FromBlocks(A,B,B^H,D) is Hermitian iff the Schur complement D - B^H A^{-1} B is Hermitian.
Русский
Если A Гермитова, то FromBlocks(A,B,B^H,D) Гермитова тогда и только тогда, когда Schur-комплемент D - B^H A^{-1} B Гермитова.
LaTeX
$$FromBlocks(A,B,B^{\\mathrm{H}},D)^{\\mathrm{H}} \\iff (D - B^{\\mathrm{H}} A^{-1} B)^{\\mathrm{H}}$$
Lean4
theorem fromBlocks₁₁ [Fintype m] [DecidableEq m] {A : Matrix m m α} (B : Matrix m n α) (D : Matrix n n α)
(hA : A.IsHermitian) : (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian :=
by
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := isHermitian_conjTranspose_mul_mul _ hA.inv
rw [isHermitian_fromBlocks_iff]
exact ⟨fun h ↦ h.2.2.2.sub hBAB, fun h ↦ ⟨hA, rfl, conjTranspose_conjTranspose B, sub_add_cancel D _ ▸ h.add hBAB⟩⟩
