From 7847b494a1921e6f137076c92a0452f57e29863b Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Sun, 25 Aug 2024 00:13:19 +0300 Subject: [PATCH 01/19] Added Woodbury Identity --- .../Matrix/NonsingularInverse.lean | 30 +++++++++++++++++++ lake-manifest.json | 2 +- 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index e91010d1bc343..7bffd1a2335b9 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -483,6 +483,36 @@ theorem inv_eq_left_inv (h : B * A = 1) : A⁻¹ = B := theorem inv_eq_right_inv (h : A * B = 1) : A⁻¹ = B := inv_eq_left_inv (mul_eq_one_comm.2 h) +section Woodbury + +variable [Fintype m] [DecidableEq m] +variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) +variable [Invertible A] [Invertible C][Invertible (C⁻¹ + V * A⁻¹* U)] + +lemma add_mul_mul_inv_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, Matrix.add_mul, Matrix.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 [Matrix.mul_inv_of_invertible, 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_inv_cancel_right_of_invertible, ←Matrix.mul_assoc] + _ = 1 := by simp + +noncomputable def add_mul_mul_inv: Invertible (A+U*C*V) := by + apply Matrix.invertibleOfRightInverse _ _ (add_mul_mul_inv_mul_eq_one A U C V) + +/-- **Woodbury Identity** -/ +theorem add_mul_mul_inv_eq_sub: (A+U*C*V)⁻¹=A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U)⁻¹*V*A⁻¹:= + Matrix.inv_eq_right_inv (add_mul_mul_inv_mul_eq_one _ _ _ _) + +end Woodbury + section InvEqInv variable {C : Matrix n n α} diff --git a/lake-manifest.json b/lake-manifest.json index 16451a762d3d1..ea901904743d6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9339d48cc3b7431b6353af47f303691e9d4da229", + "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", From 21b4dc79e87963eaefb18f8aa8923bca54cc52d1 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Sun, 25 Aug 2024 00:27:53 +0300 Subject: [PATCH 02/19] Fixed style error --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 7bffd1a2335b9..32cbcc59263e1 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -501,7 +501,7 @@ lemma add_mul_mul_inv_mul_eq_one: (A+U*C*V)*(A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U) 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_inv_cancel_right_of_invertible, ←Matrix.mul_assoc] + simp only [Matrix.mul_add, Matrix.mul_inv_cancel_right_of_invertible, ← Matrix.mul_assoc] _ = 1 := by simp noncomputable def add_mul_mul_inv: Invertible (A+U*C*V) := by From fd0e4ba19eee604fd78f75abf8df8d7041649cf8 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Fri, 30 Aug 2024 19:34:40 +0300 Subject: [PATCH 03/19] Added docstring --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 32cbcc59263e1..6e0e94707da2e 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -504,6 +504,7 @@ lemma add_mul_mul_inv_mul_eq_one: (A+U*C*V)*(A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U) simp only [Matrix.mul_add, Matrix.mul_inv_cancel_right_of_invertible, ← Matrix.mul_assoc] _ = 1 := by simp +/-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A+U*C*V`-/ noncomputable def add_mul_mul_inv: Invertible (A+U*C*V) := by apply Matrix.invertibleOfRightInverse _ _ (add_mul_mul_inv_mul_eq_one A U C V) From 6d19472fac70cef9e79b8c9c9b564e1110b84e78 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Fri, 30 Aug 2024 21:52:04 +0300 Subject: [PATCH 04/19] update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index ea901904743d6..16451a762d3d1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", + "rev": "9339d48cc3b7431b6353af47f303691e9d4da229", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", From af90057308a9200445c9ed02aa1fb3daf4174f8c Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Wed, 4 Sep 2024 23:27:30 +0300 Subject: [PATCH 05/19] Fixed Spacing --- .../Matrix/NonsingularInverse.lean | 30 +++++++++++-------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 6e0e94707da2e..5e54505c081ba 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -487,29 +487,33 @@ section Woodbury variable [Fintype m] [DecidableEq m] variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) -variable [Invertible A] [Invertible C][Invertible (C⁻¹ + V * A⁻¹* U)] +variable [Invertible A] [Invertible C] [Invertible (C⁻¹ + V * A⁻¹ * U)] -lemma add_mul_mul_inv_mul_eq_one: (A+U*C*V)*(A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U)⁻¹*V*A⁻¹) = 1 := by +lemma add_mul_mul_inv_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 + (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, Matrix.add_mul, Matrix.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 + _ = (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 [Matrix.mul_inv_of_invertible, 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 + _ = 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_inv_cancel_right_of_invertible, ← Matrix.mul_assoc] _ = 1 := by simp -/-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A+U*C*V`-/ -noncomputable def add_mul_mul_inv: Invertible (A+U*C*V) := by +/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A+ U * C * V`-/ +noncomputable def add_mul_mul_inv: Invertible (A + U * C * V) := by apply Matrix.invertibleOfRightInverse _ _ (add_mul_mul_inv_mul_eq_one A U C V) /-- **Woodbury Identity** -/ -theorem add_mul_mul_inv_eq_sub: (A+U*C*V)⁻¹=A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U)⁻¹*V*A⁻¹:= +theorem add_mul_mul_inv_eq_sub: + (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := Matrix.inv_eq_right_inv (add_mul_mul_inv_mul_eq_one _ _ _ _) end Woodbury @@ -652,14 +656,14 @@ theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.r rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, mul_inv_rev, list_prod_inv_reverse Xs] -/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ +/-- One form of ** Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹ *ᵥ b = cramer A b := by rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul, h.mul_val_inv, one_smul] -/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ +/-- One form of ** Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • b ᵥ* A⁻¹ = cramer Aᵀ b := by From 36f5d09b404df21cb15d024979e3dcb71fd4075c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 7 Sep 2024 19:48:03 +0100 Subject: [PATCH 06/19] Add missing spaces MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 6e0e94707da2e..3c9c7e9a0f561 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -487,7 +487,7 @@ section Woodbury variable [Fintype m] [DecidableEq m] variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) -variable [Invertible A] [Invertible C][Invertible (C⁻¹ + V * A⁻¹* U)] +variable [Invertible A] [Invertible C] [Invertible (C⁻¹ + V * A⁻¹* U)] lemma add_mul_mul_inv_mul_eq_one: (A+U*C*V)*(A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U)⁻¹*V*A⁻¹) = 1 := by calc @@ -498,7 +498,7 @@ lemma add_mul_mul_inv_mul_eq_one: (A+U*C*V)*(A⁻¹-A⁻¹*U*(C⁻¹+V*A⁻¹*U) rw [Matrix.mul_inv_of_invertible, 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] + 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_inv_cancel_right_of_invertible, ← Matrix.mul_assoc] From 2ca03d41fed69b113f398fc3a54da6e43747338a Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Mon, 9 Sep 2024 10:42:06 +0300 Subject: [PATCH 07/19] removed noncomputable --- .../Matrix/NonsingularInverse.lean | 40 ++++++++++--------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 5e54505c081ba..a24608d1aa786 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -487,34 +487,36 @@ section Woodbury variable [Fintype m] [DecidableEq m] variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) -variable [Invertible A] [Invertible C] [Invertible (C⁻¹ + V * A⁻¹ * U)] +variable [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] -lemma add_mul_mul_inv_mul_eq_one: - (A + U * C * V) * (A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹) = 1 := by +lemma 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 + (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, Matrix.add_mul, Matrix.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 [Matrix.mul_inv_of_invertible, Matrix.one_mul] + _ = (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 + _ = 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 + _ = 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_inv_cancel_right_of_invertible, ← Matrix.mul_assoc] - _ = 1 := by simp + simp only [Matrix.mul_add, Matrix.mul_mul_invOf_self_cancel, ← Matrix.mul_assoc] + _ = 1 := by + rw [Matrix.mul_mul_invOf_self_cancel] + abel -/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A+ U * C * V`-/ -noncomputable def add_mul_mul_inv: Invertible (A + U * C * V) := by - apply Matrix.invertibleOfRightInverse _ _ (add_mul_mul_inv_mul_eq_one A U C V) +/-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A + U * C * V`-/ +def add_mul_mul_inv: Invertible (A + U*C*V) := by + apply Matrix.invertibleOfRightInverse _ _ (add_mul_mul_invOf_mul_eq_one A U C V) /-- **Woodbury Identity** -/ -theorem add_mul_mul_inv_eq_sub: - (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := - Matrix.inv_eq_right_inv (add_mul_mul_inv_mul_eq_one _ _ _ _) +theorem add_mul_mul_inv_eq_sub[Invertible (A + U*C*V)]: + ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by + rw [@invOf_eq_nonsing_inv] + apply inv_eq_right_inv + apply add_mul_mul_invOf_mul_eq_one + end Woodbury From ce41b09aa9b8e08d3a21d1d306c62b2521c0f904 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Mon, 9 Sep 2024 10:45:13 +0300 Subject: [PATCH 08/19] added spaces --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index a24608d1aa786..25634999c5c2c 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -489,17 +489,17 @@ variable [Fintype m] [DecidableEq m] variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) variable [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] -lemma add_mul_mul_invOf_mul_eq_one : (A + U*C*V)*(⅟A-⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by +lemma 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 + (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, Matrix.add_mul, Matrix.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 + _ = (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 + _ = 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 + _ = 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_mul_invOf_self_cancel, ← Matrix.mul_assoc] _ = 1 := by From 711cd00652ee365ee5f3a2ea2569b081e07b0d45 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Mon, 9 Sep 2024 10:50:08 +0300 Subject: [PATCH 09/19] indentation --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 25634999c5c2c..d2b33b122a99d 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -512,10 +512,10 @@ def add_mul_mul_inv: Invertible (A + U*C*V) := by /-- **Woodbury Identity** -/ theorem add_mul_mul_inv_eq_sub[Invertible (A + U*C*V)]: - ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by - rw [@invOf_eq_nonsing_inv] - apply inv_eq_right_inv - apply add_mul_mul_invOf_mul_eq_one + ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by + rw [@invOf_eq_nonsing_inv] + apply inv_eq_right_inv + apply add_mul_mul_invOf_mul_eq_one end Woodbury From 36cfd673cbecd36d3773e34470429e2f6f230c2f Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Wed, 11 Sep 2024 12:54:39 +0300 Subject: [PATCH 10/19] Moved lemma --- Mathlib/Data/Matrix/Invertible.lean | 27 ++++++++++++++++++ .../Matrix/NonsingularInverse.lean | 28 ++++--------------- 2 files changed, 32 insertions(+), 23 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index c0923041fcdb8..f0031522d4fb1 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ import Mathlib.Data.Matrix.Basic +import Mathlib.Tactic.Abel /-! # Extra lemmas about invertible matrices @@ -101,4 +102,30 @@ def transposeInvertibleEquivInvertible : Invertible Aᵀ ≃ Invertible A where end CommSemiring +section Ring + +variable [Ring α] (A : Matrix n n α) + +lemma add_mul_mul_invOf_mul_eq_one [Fintype m] [DecidableEq m] + (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) + [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)]: + (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, Matrix.add_mul, Matrix.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_mul_invOf_self_cancel, ← Matrix.mul_assoc] + _ = 1 := by + rw [Matrix.mul_mul_invOf_self_cancel] + abel + +end Ring + end Matrix diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index d2b33b122a99d..23af8d9d6954c 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -489,34 +489,16 @@ variable [Fintype m] [DecidableEq m] variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) variable [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] -lemma 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, Matrix.add_mul, Matrix.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_mul_invOf_self_cancel, ← Matrix.mul_assoc] - _ = 1 := by - rw [Matrix.mul_mul_invOf_self_cancel] - abel - /-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A + U * C * V`-/ def add_mul_mul_inv: Invertible (A + U*C*V) := by - apply Matrix.invertibleOfRightInverse _ _ (add_mul_mul_invOf_mul_eq_one A U C V) + apply Matrix.invertibleOfRightInverse _ _ (Matrix.add_mul_mul_invOf_mul_eq_one A U C V) /-- **Woodbury Identity** -/ -theorem add_mul_mul_inv_eq_sub[Invertible (A + U*C*V)]: +theorem add_mul_mul_inv_eq_sub [Invertible (A + U*C*V)]: ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by rw [@invOf_eq_nonsing_inv] apply inv_eq_right_inv - apply add_mul_mul_invOf_mul_eq_one - + apply Matrix.add_mul_mul_invOf_mul_eq_one end Woodbury @@ -658,14 +640,14 @@ theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.r rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, mul_inv_rev, list_prod_inv_reverse Xs] -/-- One form of ** Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ +/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹ *ᵥ b = cramer A b := by rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul, h.mul_val_inv, one_smul] -/-- One form of ** Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ +/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • b ᵥ* A⁻¹ = cramer Aᵀ b := by From 09de57d66d9c806a6b826b61ed16f2f4f5c2f4d0 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Wed, 11 Sep 2024 13:02:20 +0300 Subject: [PATCH 11/19] Added version for nonsingular inverse --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 23af8d9d6954c..e6d43a620ff77 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -494,12 +494,17 @@ def add_mul_mul_inv: Invertible (A + U*C*V) := by apply Matrix.invertibleOfRightInverse _ _ (Matrix.add_mul_mul_invOf_mul_eq_one A U C V) /-- **Woodbury Identity** -/ -theorem add_mul_mul_inv_eq_sub [Invertible (A + U*C*V)]: +theorem add_mul_mul_invOf_eq_sub [Invertible (A + U*C*V)]: ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by rw [@invOf_eq_nonsing_inv] apply inv_eq_right_inv apply Matrix.add_mul_mul_invOf_mul_eq_one +theorem add_mul_mul_inv_eq_sub [Invertible (A + U*C*V)]: + (A + U*C*V)⁻¹ = A⁻¹ - A⁻¹*U*(C⁻¹ + V*A⁻¹*U)⁻¹*V*A⁻¹ := by + simp only [← invOf_eq_nonsing_inv] + apply add_mul_mul_invOf_eq_sub + end Woodbury section InvEqInv From 27555877fb8cf9e32ff2378d94a1afcd230e99a2 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Wed, 18 Sep 2024 11:38:05 +0300 Subject: [PATCH 12/19] Fixed indentation --- Mathlib/Data/Matrix/Invertible.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index f0031522d4fb1..479eed4321a0f 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -107,9 +107,9 @@ section Ring variable [Ring α] (A : Matrix n n α) lemma add_mul_mul_invOf_mul_eq_one [Fintype m] [DecidableEq m] - (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) - [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)]: - (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by + (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) + [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)]: + (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 From 613c997d23605ca109f4f4e47b0fbbe990db097c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 22 Sep 2024 21:54:34 +0000 Subject: [PATCH 13/19] generalize the results to non-commutative rings --- Mathlib/Data/Matrix/Invertible.lean | 73 ++++++++++++++----- .../Matrix/NonsingularInverse.lean | 38 ++++------ 2 files changed, 69 insertions(+), 42 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index 479eed4321a0f..dbe91363346f2 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -104,27 +104,64 @@ end CommSemiring section Ring -variable [Ring α] (A : Matrix n n α) +section Woodbury -lemma add_mul_mul_invOf_mul_eq_one [Fintype m] [DecidableEq m] - (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) - [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)]: +variable [Fintype m] [DecidableEq m] [Ring α] + (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) + [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] + +lemma 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, Matrix.add_mul, Matrix.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_mul_invOf_self_cancel, ← Matrix.mul_assoc] - _ = 1 := by - rw [Matrix.mul_mul_invOf_self_cancel] - abel + (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_mul_invOf_self_cancel, ← Matrix.mul_assoc] + _ = 1 := by + rw [Matrix.mul_mul_invOf_self_cancel] + abel + +-- as above, but with multiplication reversed +lemma add_mul_mul_invOf_mul_eq_one' : + (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) = 1 := by + calc + (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) + _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by + simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc] + _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by + rw [invOf_mul_self, Matrix.mul_invOf_mul_self_cancel] + abel + _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by + rw [sub_right_inj, Matrix.mul_add] + simp_rw [Matrix.mul_assoc] + _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by + congr 1 + simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc, + Matrix.mul_invOf_mul_self_cancel] + _ = 1 := by + rw [Matrix.mul_invOf_mul_self_cancel] + abel + +/-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A + U * C * V`-/ +def invertibleAddMulMul : Invertible (A + U*C*V) where + invOf := ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _ + mul_invOf_self := add_mul_mul_invOf_mul_eq_one _ _ _ _ + +/-- The **Woodbury Identity** (`⅟` version). -/ +theorem invOf_add_mul_mul [Invertible (A + U*C*V)] : + ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by + letI := invertibleAddMulMul A U C V + convert (rfl : ⅟(A + U*C*V) = _) + +end Woodbury end Ring diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index e6d43a620ff77..501313a80bad7 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -483,30 +483,6 @@ theorem inv_eq_left_inv (h : B * A = 1) : A⁻¹ = B := theorem inv_eq_right_inv (h : A * B = 1) : A⁻¹ = B := inv_eq_left_inv (mul_eq_one_comm.2 h) -section Woodbury - -variable [Fintype m] [DecidableEq m] -variable (A: Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) -variable [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] - -/-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A + U * C * V`-/ -def add_mul_mul_inv: Invertible (A + U*C*V) := by - apply Matrix.invertibleOfRightInverse _ _ (Matrix.add_mul_mul_invOf_mul_eq_one A U C V) - -/-- **Woodbury Identity** -/ -theorem add_mul_mul_invOf_eq_sub [Invertible (A + U*C*V)]: - ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by - rw [@invOf_eq_nonsing_inv] - apply inv_eq_right_inv - apply Matrix.add_mul_mul_invOf_mul_eq_one - -theorem add_mul_mul_inv_eq_sub [Invertible (A + U*C*V)]: - (A + U*C*V)⁻¹ = A⁻¹ - A⁻¹*U*(C⁻¹ + V*A⁻¹*U)⁻¹*V*A⁻¹ := by - simp only [← invOf_eq_nonsing_inv] - apply add_mul_mul_invOf_eq_sub - -end Woodbury - section InvEqInv variable {C : Matrix n n α} @@ -617,6 +593,20 @@ theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse end Diagonal +section Woodbury + +variable [Fintype m] [DecidableEq m] +variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) +variable [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] + +/-- The **Woodbury Identity** (`⁻¹` version). -/ +theorem add_mul_mul_inv_eq_sub [Invertible (A + U*C*V)]: + (A + U*C*V)⁻¹ = A⁻¹ - A⁻¹*U*(C⁻¹ + V*A⁻¹*U)⁻¹*V*A⁻¹ := by + simp only [← invOf_eq_nonsing_inv] + apply invOf_add_mul_mul + +end Woodbury + @[simp] theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := by by_cases h : IsUnit A.det From 94b7d54aff17831b8360939cd8fe0efff2140382 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 22 Sep 2024 21:59:54 +0000 Subject: [PATCH 14/19] swap Invertible for IsUnit --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 501313a80bad7..393fa09a438e2 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -597,11 +597,15 @@ section Woodbury variable [Fintype m] [DecidableEq m] variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) -variable [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] /-- The **Woodbury Identity** (`⁻¹` version). -/ -theorem add_mul_mul_inv_eq_sub [Invertible (A + U*C*V)]: +theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V*A⁻¹*U)) : (A + U*C*V)⁻¹ = A⁻¹ - A⁻¹*U*(C⁻¹ + V*A⁻¹*U)⁻¹*V*A⁻¹ := by + obtain ⟨_⟩ := hA.nonempty_invertible + obtain ⟨_⟩ := hC.nonempty_invertible + obtain ⟨iAC⟩ := hAC.nonempty_invertible + simp only [← invOf_eq_nonsing_inv] at iAC + letI := invertibleAddMulMul A U C V simp only [← invOf_eq_nonsing_inv] apply invOf_add_mul_mul From 2f17c57ba5c2a9f2301ee6e3f1798d5f11eb9e01 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Mon, 23 Sep 2024 12:10:55 +0300 Subject: [PATCH 15/19] Added Author --- Mathlib/Data/Matrix/Invertible.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index dbe91363346f2..10d47043d7efc 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2023 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Eric Wieser +Authors: Eric Wieser, Ahmad Alkhalawi -/ import Mathlib.Data.Matrix.Basic import Mathlib.Tactic.Abel From 99b62dbcf824f06f6b4b6005f61624ac87ce2f49 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Tue, 24 Sep 2024 22:56:30 +0300 Subject: [PATCH 16/19] Added comment and some spaces --- Mathlib/Data/Matrix/Invertible.lean | 1 + Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index 10d47043d7efc..b57fcb81f51e9 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -110,6 +110,7 @@ variable [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] +-- Removed spaces around multiplication signs for better clarity lemma add_mul_mul_invOf_mul_eq_one : (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by calc diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 393fa09a438e2..083144c40eaa5 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -599,8 +599,8 @@ variable [Fintype m] [DecidableEq m] variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) /-- The **Woodbury Identity** (`⁻¹` version). -/ -theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V*A⁻¹*U)) : - (A + U*C*V)⁻¹ = A⁻¹ - A⁻¹*U*(C⁻¹ + V*A⁻¹*U)⁻¹*V*A⁻¹ := by +theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) : + (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := by obtain ⟨_⟩ := hA.nonempty_invertible obtain ⟨_⟩ := hC.nonempty_invertible obtain ⟨iAC⟩ := hAC.nonempty_invertible From e6cac703b3816c3eed494971b874f47e08353cf7 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Tue, 24 Sep 2024 22:59:25 +0300 Subject: [PATCH 17/19] Added space --- Mathlib/Data/Matrix/Invertible.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index b57fcb81f51e9..91e25c5d4faf2 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -150,7 +150,7 @@ lemma add_mul_mul_invOf_mul_eq_one' : rw [Matrix.mul_invOf_mul_self_cancel] abel -/-- If matrices `A`, `C`, and `C⁻¹ + V*A⁻¹*U` are invertible, then so is `A + U * C * V`-/ +/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`-/ def invertibleAddMulMul : Invertible (A + U*C*V) where invOf := ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _ From 6b1acd14b377b532ed32c3e533ea5945d846153b Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Tue, 24 Sep 2024 23:02:55 +0300 Subject: [PATCH 18/19] Another missing space --- Mathlib/Data/Matrix/Invertible.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index 91e25c5d4faf2..e4c52fe6d5034 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -108,7 +108,7 @@ section Woodbury variable [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) - [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A* U)] + [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] -- Removed spaces around multiplication signs for better clarity lemma add_mul_mul_invOf_mul_eq_one : From d51e3a90ee43c1ef6b0d9cda69e0d75395f1ebd8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 26 Sep 2024 00:59:31 +0000 Subject: [PATCH 19/19] fix the deprecations --- Mathlib/Data/Matrix/Invertible.lean | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index a27602e0a4327..b68c2fb925d3d 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -48,10 +48,12 @@ protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α) protected theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A * B * ⅟ B = A := by rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one] -@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := invOf_mul_cancel_left -@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := mul_invOf_cancel_left -@[deprecated (since := "2024-09-07")] alias mul_invOf_mul_self_cancel := invOf_mul_cancel_right -@[deprecated (since := "2024-09-07")] alias mul_mul_invOf_self_cancel := mul_invOf_cancel_right +@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := Matrix.invOf_mul_cancel_left +@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := Matrix.mul_invOf_cancel_left +@[deprecated (since := "2024-09-07")] +alias mul_invOf_mul_self_cancel := Matrix.invOf_mul_cancel_right +@[deprecated (since := "2024-09-07")] +alias mul_mul_invOf_self_cancel := Matrix.mul_invOf_cancel_right section ConjTranspose variable [StarRing α] (A : Matrix n n α) @@ -115,7 +117,7 @@ variable [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] --- Removed spaces around multiplication signs for better clarity +-- No spaces around multiplication signs for better clarity lemma add_mul_mul_invOf_mul_eq_one : (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by calc @@ -129,12 +131,12 @@ lemma add_mul_mul_invOf_mul_eq_one : 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_mul_invOf_self_cancel, ← Matrix.mul_assoc] + simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc] _ = 1 := by - rw [Matrix.mul_mul_invOf_self_cancel] + rw [Matrix.mul_invOf_cancel_right] abel --- as above, but with multiplication reversed +/-- Like `add_mul_mul_invOf_mul_eq_one`, but with multiplication reversed. -/ lemma add_mul_mul_invOf_mul_eq_one' : (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) = 1 := by calc @@ -142,7 +144,7 @@ lemma add_mul_mul_invOf_mul_eq_one' : _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc] _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by - rw [invOf_mul_self, Matrix.mul_invOf_mul_self_cancel] + rw [invOf_mul_self, Matrix.invOf_mul_cancel_right] abel _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by rw [sub_right_inj, Matrix.mul_add] @@ -150,9 +152,9 @@ lemma add_mul_mul_invOf_mul_eq_one' : _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by congr 1 simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc, - Matrix.mul_invOf_mul_self_cancel] + Matrix.invOf_mul_cancel_right] _ = 1 := by - rw [Matrix.mul_invOf_mul_self_cancel] + rw [Matrix.invOf_mul_cancel_right] abel /-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`-/