English
For a block matrix fromBlocks(A,B,Bᴴ,D) with D positive definite and invertible, the PSD property is equivalent to the Schur complement A − B D⁻¹ Bᴴ.
Русский
Для блочной матрицы fromBlocks(A,B,Bᴴ,D) с D положительно определенной и обратимой, свойство PSD эквивалентно Schur комплементу A − B D⁻¹ Bᴴ.
LaTeX
$$$$ \\operatorname{PosSemidef}(\\mathrm{fromBlocks} A B B^{\\mathrm{H}} D) \\iff \\operatorname{PosSemidef}\\left(A - B D^{-1} B^{\\mathrm{H}}\\right). $$$$
Lean4
theorem fromBlocks₂₂ [DecidableEq n] (A : Matrix m m R') (B : Matrix m n R') {D : Matrix n n R'} (hD : D.PosDef)
[Invertible D] : (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef :=
by
rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply, fromBlocks_submatrix_sum_swap_sum_swap]
convert fromBlocks₁₁ Bᴴ A hD <;> simp
