fromBlocks₁₁ — Mathlib

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

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