From 7520e81244705edc1d1093c3d131c436f8332136 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Oct 2024 09:15:20 +0100 Subject: [PATCH] Equation 158 (#16) Adapted from #3, using new results that have since been upstreamed to mathlib Co-authored-by: MohanadAhmed --- MatrixCookbook/3Inverses.lean | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/MatrixCookbook/3Inverses.lean b/MatrixCookbook/3Inverses.lean index e67453b..0b2ff9b 100644 --- a/MatrixCookbook/3Inverses.lean +++ b/MatrixCookbook/3Inverses.lean @@ -104,10 +104,26 @@ theorem eq_157 (A : Matrix n n ℂ) (B : Matrix m m ℂ) (U : Matrix n m ℂ) (V Matrix.add_mul_mul_inv_eq_sub _ _ _ _ hA hB h open scoped ComplexOrder in +/-- Note that this has been generalized from the `ℝ`/`ᵀ` in the source to `ℂ`/`ᴴ`. -/ theorem eq_158 (P : Matrix n n ℂ) (R : Matrix m m ℂ) (B : Matrix m n ℂ) (hP : P.PosDef) (hR : R.PosDef) : - (P + Bᵀ * R * B)⁻¹ * Bᵀ * R⁻¹ = P * Bᵀ * (B*P⁻¹*Bᵀ + R)⁻¹ := by - sorry + (P⁻¹ + Bᴴ * R⁻¹ * B)⁻¹ * Bᴴ * R⁻¹ = P * Bᴴ * (B * P * Bᴴ + R)⁻¹ := by + letI : Invertible P := hP.isUnit.invertible + letI : Invertible R := hR.isUnit.invertible + letI : Invertible (R + B*P*Bᴴ) := + (hR.add_posSemidef <| hP.posSemidef.mul_mul_conjTranspose_same B).isUnit.invertible + rw [Matrix.add_mul_mul_inv_eq_sub, add_comm _ R] + · simp_rw [Matrix.inv_inv_of_invertible, Matrix.sub_mul, Matrix.mul_assoc, ← Matrix.mul_sub] + congr 2 + simp_rw [← Matrix.mul_assoc] + refine hR.isUnit.isRegular.right ?_ + simp_rw [Matrix.sub_mul, sub_eq_iff_eq_add, Matrix.mul_assoc, ← Matrix.mul_add, + ← Matrix.mul_assoc, Matrix.inv_mul_cancel_right_of_invertible, + Matrix.inv_mul_of_invertible] + · simpa only [isUnit_nonsing_inv_iff] using hP.isUnit + · simpa only [isUnit_nonsing_inv_iff] using hR.isUnit + · simp_rw [Matrix.inv_inv_of_invertible] + exact isUnit_of_invertible _ /-! ### The Kailath Variant -/