English
If A is invertible and the Schur complement D - C A^{-1} B is invertible, then the inverse of fromBlocks A B C D is the block matrix with A^{-1} in the top-left and D^{-1} in the bottom-right, and the off-diagonal blocks given by −D^{-1} C A^{-1} and −A^{-1} B D^{-1}.
Русский
Если A обратима и Schur-комплемент D − C A^{-1} B обратим, то ⅟(fromBlocks A B C D) имеет блочное представление с A^{-1} в верхнем левом углу и D^{-1} внизу справа.
LaTeX
$$$\text{Invertible}(A) \land \text{Invertible}(D - C A^{-1} B) \Rightarrow ⅟(\mathrm{fromBlocks}(A,B,C,D)) = \mathrm{fromBlocks}(A^{-1} + A^{-1} B (D - C A^{-1} B)^{-1} C A^{-1}, -(A^{-1} B (D - C A^{-1} B)^{-1}), -(D - C A^{-1} B)^{-1} C A^{-1}, (D - C A^{-1} B)^{-1})$$$
Lean4
theorem invOf_fromBlocks₁₁_eq (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)] :
⅟(fromBlocks A B C D) =
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)) :=
by
letI := fromBlocks₁₁Invertible A B C D
convert (rfl : ⅟(fromBlocks A B C D) = _)
