English
If A is invertible, and the Schur complement (D − C A^{-1} B) is invertible, then the block matrix fromBlocks A B C D is invertible. More explicitly, fromBlocks A B C D = fromBlocks(1 0 C A^{-1}) etc., giving an LDU-like decomposition.
Русский
Пусть A обратима, и знак Шура: D − C A^{-1} B обратим. Тогда блок-матрица fromBlocks A B C D обратима; существует разложение по блокам аналогичное LDU.
LaTeX
$$$[\text{Invertible}(A) \land \text{Invertible}(D - C A^{-1} B)] \Rightarrow \text{Invertible}(\text{fromBlocks } A B C D)$$$
Lean4
/-- LDU decomposition of a block matrix with an invertible top-left corner, using the
Schur complement. -/
theorem fromBlocks_eq_of_invertible₁₁ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α) (D : Matrix l n α)
[Invertible A] :
fromBlocks A B C D = fromBlocks 1 0 (C * ⅟A) 1 * fromBlocks A 0 0 (D - C * ⅟A * B) * fromBlocks 1 (⅟A * B) 0 1 := by
simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add, Matrix.one_mul, Matrix.mul_one,
invOf_mul_self, Matrix.mul_invOf_cancel_left, Matrix.mul_assoc, add_sub_cancel]
