English
For a block matrix fromBlocks(A,B,Bᴴ,D) with A positive definite, the PSD property is equivalent to the Schur complement D − Bᴴ A⁻¹ B.
Русский
Для блочной матрицы fromBlocks(A,B,Bᴴ,D) с A положительно definite эквивалентно условие неотрицательного квадратичного дополнения Шура: D − Bᴴ A⁻¹ B.
LaTeX
$$$$ \\operatorname{PosSemidef}(\\mathrm{fromBlocks} A B B^{\\mathrm{H}} D) \\iff \\operatorname{PosSemidef}\\left( D - B^{\\mathrm{H}} A^{-1} B \\right). $$$$
Lean4
theorem fromBlocks₁₁ [DecidableEq m] {A : Matrix m m R'} (B : Matrix m n R') (D : Matrix n n R') (hA : A.PosDef)
[Invertible A] : (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef :=
by
rw [PosSemidef, IsHermitian.fromBlocks₁₁ _ _ hA.1]
constructor
· refine fun h => ⟨h.1, fun x => ?_⟩
have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
rwa [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_cancel, dotProduct_zero, zero_add, ←
dotProduct_mulVec] at this
· refine fun h => ⟨h.1, fun x => ?_⟩
rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]
apply le_add_of_nonneg_of_le
· rw [← dotProduct_mulVec]
apply hA.posSemidef.2
· rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]
apply h.2