English
If D is invertible and the Schur complement A - B D^{-1} C is invertible, then the block matrix fromBlocks A B C D is invertible. The inverse is given by a detailed block expression.
Русский
Если D обратима и Шур-комплемент 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
/-- A block matrix is invertible if the bottom right 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 D]
[Invertible (A - B * ⅟D * C)] : Invertible (fromBlocks A B C D) := by
-- factor `fromBlocks` via `fromBlocks_eq_of_invertible₂₂`, and state the inverse we expect
convert
Invertible.copy' _ _
(fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
(⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D))
(fromBlocks_eq_of_invertible₂₂ _ _ _ _) _
· -- the product is invertible because all the factors are
letI : Invertible (1 : Matrix n n α) := invertibleOne
letI : Invertible (1 : Matrix m m α) := invertibleOne
refine Invertible.mul ?_ (fromBlocksZero₁₂Invertible _ _ _)
exact Invertible.mul (fromBlocksZero₂₁Invertible _ _ _) (fromBlocksZero₂₁Invertible _ _ _)
· -- unfold the `Invertible` instances to get the raw factors
change
_ =
fromBlocks 1 0 (-(1 * (⅟D * C) * 1)) 1 *
(fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * 0 * ⅟D)) 0 (⅟D) *
fromBlocks 1 (-(1 * (B * ⅟D) * 1)) 0 1)
-- combine into a single block matrix
simp only [fromBlocks_multiply, Matrix.one_mul, Matrix.mul_one, Matrix.zero_mul, Matrix.mul_zero, add_zero,
zero_add, neg_zero, Matrix.mul_neg, Matrix.neg_mul, neg_neg, ← Matrix.mul_assoc, add_comm (⅟D)]
