invertibleOfFromBlocksZero₁₂Invertible

English

If the whole block matrix is invertible, then the Schur complement A − B D^{-1} C is invertible.

Русский

Если вся блочная матрица обратима, то Шур-комплемент A − B D^{-1} C обратим.

LaTeX

$$$\text{Invertible}(\mathrm{fromBlocks}(A,B,C,D)) \Rightarrow \text{Invertible}(A - B D^{-1} C)$$$

Lean4

/-- Both diagonal entries of an invertible lower-block-triangular matrix are invertible (by reading
off the diagonal entries of the inverse). -/
def invertibleOfFromBlocksZero₁₂Invertible (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α)
    [Invertible (fromBlocks A 0 C D)] : Invertible A × Invertible D
    where
  fst :=
    invertibleOfRightInverse _ (⅟(fromBlocks A 0 C D)).toBlocks₁₁ <|
      by
      have := mul_invOf_self (fromBlocks A 0 C D)
      rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this
      replace := congr_arg Matrix.toBlocks₁₁ this
      simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.zero_mul, add_zero, ← fromBlocks_one] using this
  snd :=
    invertibleOfLeftInverse _ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ <|
      by
      have := invOf_mul_self (fromBlocks A 0 C D)
      rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this
      replace := congr_arg Matrix.toBlocks₂₂ this
      simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.mul_zero, zero_add, ← fromBlocks_one] using this

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