fromBlocks₂₂ — Mathlib

English

If D is Hermitian, then 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

$$FromBlocks(A,B,B^{\\mathrm{H}},D)^{\\mathrm{H}} \\iff (A - B D^{-1} B^{\\mathrm{H}})^{\\mathrm{H}}$$

Lean4

theorem fromBlocks₂₂ [Fintype n] [DecidableEq n] (A : Matrix m m α) (B : Matrix m n α) {D : Matrix n n α}
    (hD : D.IsHermitian) : (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian :=
  by
  rw [← isHermitian_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply, fromBlocks_submatrix_sum_swap_sum_swap]
  convert IsHermitian.fromBlocks₁₁ _ _ hD <;> simp

Похожие утверждения