English
If A is invertible and the corresponding Schur complement D - C A^{-1} B is invertible, then the block matrix fromBlocks A B C D is invertible.
Русский
Если A обратима и соответствующий Шур-комплемент D − C A^{-1} B обратим, тогда fromBlocks A B C D обращима.
LaTeX
$$$[\text{Invertible}(A) \land \text{Invertible}(D - C A^{-1} B)] \Rightarrow \text{Invertible}(\mathrm{fromBlocks}(A,B,C,D))$$$
Lean4
/-- A block matrix is invertible if the top left corner and the corresponding Schur complement
is. -/
def fromBlocks₁₁Invertible (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A]
[Invertible (D - C * ⅟A * B)] : Invertible (fromBlocks A B C D) := by
-- we argue by symmetry
letI := fromBlocks₂₂Invertible D C B A
letI iDCBA := submatrixEquivInvertible (fromBlocks D C B A) (Equiv.sumComm _ _) (Equiv.sumComm _ _)
exact
iDCBA.copy' _
(fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
(-(⅟(D - C * ⅟A * B) * C * ⅟A)) (⅟(D - C * ⅟A * B)))
(fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm
