English
If D is invertible and the Schur complement A - B D^{-1} C is invertible, then fromBlocks A B C D is invertible. Moreover, the inverse is given by a corresponding block expression.
Русский
Пусть D обратима и Schur-комплемент A − B D^{-1} C обратим, тогда fromBlocks A B C D обратима, и ее обратная матрица имеет соответствующую блочную форму.
LaTeX
$$$[\text{Invertible}(D) \land \text{Invertible}(A - B D^{-1} C)] \Rightarrow \text{Invertible}(\mathrm{fromBlocks}(A,B,C,D))$$$$
Lean4
/-- LDU decomposition of a block matrix with an invertible bottom-right corner, using the
Schur complement. -/
theorem fromBlocks_eq_of_invertible₂₂ (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α) (D : Matrix n n α)
[Invertible D] :
fromBlocks A B C D = fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1 :=
(Matrix.reindex (Equiv.sumComm _ _) (Equiv.sumComm _ _)).injective <| by
simpa [reindex_apply, Equiv.sumComm_symm, ← submatrix_mul_equiv _ _ _ (Equiv.sumComm n m),
← submatrix_mul_equiv _ _ _ (Equiv.sumComm n l), Equiv.sumComm_apply,
fromBlocks_submatrix_sum_swap_sum_swap] using fromBlocks_eq_of_invertible₁₁ D C B A
