English
If A, C are invertible and (C^{-1} + V A^{-1} U) is invertible, then A + U C V is invertible and its inverse is given by the explicit block formula.
Русский
Если A и C обратимы, а C^{-1} + V A^{-1} U обратима, то A + U C V обратима, и её обратная матрица имеет явное блочное выражение.
LaTeX
$$$\text{Invertible}(A),\ \text{Invertible}(C),\ \text{Invertible}(C^{-1} + V A^{-1} U) \Rightarrow \text{Invertible}(A + U C V)\text{ with }(A + U C V)^{-1} = \tfrac{1}{A} - \tfrac{1}{A} U \tfrac{1}{( \tfrac{1}{C} + V \tfrac{1}{A} U)} V \tfrac{1}{A}$$$
Lean4
theorem add_mul_mul_invOf_mul_eq_one : (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) = 1 := by
calc
(A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)
_ =
A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A -
U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A :=
by simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]
_ = (1 + U * C * V * ⅟A) - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) :=
by
rw [mul_invOf_self, Matrix.one_mul]
abel
_ = 1 + U * C * V * ⅟A - (U + U * C * V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A := by
rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
_ = 1 + U * C * V * ⅟A - U * C * (⅟C + V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A :=
by
congr
simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]
_ = 1 := by
rw [Matrix.mul_invOf_cancel_right]
abel
-- No spaces around multiplication signs for better clarity
