English
If the whole block matrix is invertible and the bottom-right block D is invertible, then the Schur complement A − B D^{-1} C is invertible.
Русский
Если вся блочная матрица обратима и D обратим, то Шур-комплемент A − B D^{-1} C обратим.
LaTeX
$$$\text{Invertible}(\mathrm{fromBlocks}(A,B,C,D)) \Rightarrow \text{Invertible}(A - B D^{-1} C)$$$
Lean4
/-- If a block matrix is invertible and so is its bottom left element, then so is the corresponding
Schur complement. -/
def invertibleOfFromBlocks₂₂Invertible (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α)
[Invertible D] [Invertible (fromBlocks A B C D)] : Invertible (A - B * ⅟D * C) :=
by
suffices Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D) by
exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1
letI : Invertible (1 : Matrix n n α) := invertibleOne
letI : Invertible (1 : Matrix m m α) := invertibleOne
letI iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1 : Matrix (m ⊕ n) (m ⊕ n) α) := fromBlocksZero₁₂Invertible _ _ _
letI iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1 : Matrix (m ⊕ n) (m ⊕ n) α) := fromBlocksZero₂₁Invertible _ _ _
letI iBDC := Invertible.copy ‹_› _ (fromBlocks_eq_of_invertible₂₂ A B C D).symm
refine (iBD.mulLeft _).symm ?_
exact (iDC.mulRight _).symm iBDC
