[Merged by Bors] - feat(LinearAlgebra/Matrix): Woodbury Identity by 4hma4d · Pull Request #16325 · leanprover-community/mathlib4

4hma4d · 2024-08-30T19:17:14Z

This adds the Woodbury Identity.

Zulip discussion

Also corrects some bad deprecations introduced in #16590, which affected development of this PR.

Co-authored-by: Mohanad Ahmad

github-actions · 2024-08-30T19:17:54Z

PR summary d51e3a90ee

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Matrix.Invertible	803	805	+2 (+0.25%)

Import changes for all files

Files	Import difference
`Mathlib.Data.Matrix.Invertible`	2

Declarations diff

+ add_mul_mul_invOf_mul_eq_one
+ add_mul_mul_invOf_mul_eq_one'
+ add_mul_mul_inv_eq_sub
+ invOf_add_mul_mul
+ invertibleAddMulMul

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

vihdzp · 2024-09-01T20:21:39Z

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

+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


Suggested change

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

Can you also properly space out the rest of the proof?

I think it might be worth deviating from the "spaces aroung *" style here, and only adding them around the additive operators.

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

…nto woodbury

eric-wieser · 2024-09-09T09:55:35Z

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

+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


Can you move this to Matrix/Invertible.lean, and generalize it from CommRing to Ring?

Should i move all of it or just this lemma?

Yes, all the lemmas currently in this PR. The lemma I suggest below about inv would remain in this file.

@4hma4d, do you want me to do the move for you? Happy to do so to get this PR over the line, but don't want to tread on your toes.

Sorry for the delay. I didn't move add_mul_mul_inv since it relies on Matrix.invertibleOfRightInverse which is proved in NonsingularInverse

I didn't move add_mul_mul_inv since it relies on Matrix.invertibleOfRightInverse which is proved in NonsingularInverse

Indeed, to prove add_mul_mul_inv for the non-commutative case you have to repeat the whole proof, but with multiplication on the left instead! I've pushed a commit that does that.

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Mathlib/Data/Matrix/Invertible.lean

eric-wieser · 2024-09-22T22:03:00Z

Mathlib/Data/Matrix/Invertible.lean

+-- 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


I copy-pasted this from your proof above, and tweaked it to reverse all the multiplications. Thanks for writing the original which made this relatively easy!

4hma4d · 2024-09-24T20:07:59Z

Is this fine? I added the spaces in Nonsingularinverse since I don't think it affects clarity there, and I added a comment in Invertible

eric-wieser · 2024-09-25T13:44:13Z

maintainer merge

Let's let another maintainer take the final look.
Thanks for your work here @4hma4d!

github-actions · 2024-09-25T13:44:39Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

riccardobrasca · 2024-09-25T13:52:38Z

Thanks!

bors merge

This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284) Co-authored-by: Mohanad Ahmad Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2024-09-25T13:54:43Z

Build failed:

Build

riccardobrasca · 2024-09-25T13:58:05Z

Can you please merge master and fix the problem? I think it is just something that is now deprecated.

bors d+

mathlib-bors · 2024-09-25T13:58:09Z

✌️ 4hma4d can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

4hma4d · 2024-09-26T03:23:56Z

bors r+

This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284) Also corrects some bad deprecations introduced in #16590, which affected development of this PR. Co-authored-by: Mohanad Ahmad Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2024-09-26T03:43:39Z

Pull request successfully merged into master.

Build succeeded:

This was added to mathlib in leanprover-community/mathlib4#16325

This main result is `Matrix.add_mul_mul_inv_eq_sub` which was added to mathlib in leanprover-community/mathlib4#16325. Some of these other corollaries could probably be upstreamed.

This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284) Also corrects some bad deprecations introduced in #16590, which affected development of this PR. Co-authored-by: Mohanad Ahmad Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

4hma4d added 4 commits August 25, 2024 00:13

Added Woodbury Identity

7847b49

Fixed style error

21b4dc7

Added docstring

fd0e4ba

update

6d19472

4hma4d added easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc) labels Aug 30, 2024

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 30, 2024

vihdzp removed the easy < 20s of review time. See the lifecycle page for guidelines. label Sep 1, 2024

vihdzp reviewed Sep 1, 2024

View reviewed changes

4hma4d and others added 2 commits September 4, 2024 23:27

Fixed Spacing

af90057

Add missing spaces

36f5d09

Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

eric-wieser reviewed Sep 7, 2024

View reviewed changes

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean Outdated Show resolved Hide resolved

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 7, 2024

4hma4d added 4 commits September 9, 2024 10:42

removed noncomputable

2ca03d4

added spaces

ce41b09

indentation

711cd00

Merge branch 'woodbury' of github.com:leanprover-community/mathlib4 i…

42803d5

…nto woodbury

eric-wieser reviewed Sep 9, 2024

View reviewed changes

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean Outdated Show resolved Hide resolved

eric-wieser self-assigned this Sep 10, 2024

eric-wieser reviewed Sep 10, 2024

View reviewed changes

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean Outdated Show resolved Hide resolved

4hma4d added 3 commits September 11, 2024 12:54

Moved lemma

36cfd67

Added version for nonsingular inverse

09de57d

Fixed indentation

2755587

MohanadAhmed removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2024

eric-wieser added 2 commits September 22, 2024 21:54

generalize the results to non-commutative rings

613c997

swap Invertible for IsUnit

94b7d54

eric-wieser reviewed Sep 22, 2024

View reviewed changes

Mathlib/Data/Matrix/Invertible.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Sep 22, 2024

View reviewed changes

4hma4d added 3 commits September 24, 2024 22:56

Added comment and some spaces

99b62db

Added space

e6cac70

Another missing space

6b1acd1

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 25, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 25, 2024

eric-wieser changed the title ~~feat (LinearAlgebra/Matrix): Woodbury Identity~~ feat(LinearAlgebra/Matrix): Woodbury Identity Sep 25, 2024

github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 25, 2024

eric-wieser added 2 commits September 26, 2024 00:51

Merge remote-tracking branch 'origin/master' into woodbury

8a34af5

fix the deprecations

d51e3a9

mathlib-bors bot changed the title ~~feat(LinearAlgebra/Matrix): Woodbury Identity~~ [Merged by Bors] - feat(LinearAlgebra/Matrix): Woodbury Identity Sep 26, 2024

mathlib-bors bot closed this Sep 26, 2024

mathlib-bors bot deleted the woodbury branch September 26, 2024 03:43

eric-wieser added a commit to eric-wieser/lean-matrix-cookbook that referenced this pull request Sep 28, 2024

The woodbury identity and related results

2ab24e0

This was added to mathlib in leanprover-community/mathlib4#16325

eric-wieser added a commit to eric-wieser/lean-matrix-cookbook that referenced this pull request Sep 29, 2024

The woodbury identity and related results

7713e27

This was added to mathlib in leanprover-community/mathlib4#16325

eric-wieser added a commit to eric-wieser/lean-matrix-cookbook that referenced this pull request Sep 29, 2024

The woodbury identity and related results

58d3bdf

This was added to mathlib in leanprover-community/mathlib4#16325

eric-wieser added a commit to eric-wieser/lean-matrix-cookbook that referenced this pull request Sep 29, 2024

The woodbury identity and related results

7015e20

This was added to mathlib in leanprover-community/mathlib4#16325

eric-wieser added a commit to eric-wieser/lean-matrix-cookbook that referenced this pull request Sep 29, 2024

The woodbury identity and related results

af8c50e

This was added to mathlib in leanprover-community/mathlib4#16325

	lemma add_mul_mul_inv_mul_eq_one: (A+UCV)(A⁻¹-A⁻¹U(C⁻¹+VA⁻¹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

Conversation

4hma4d commented Aug 30, 2024 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary d51e3a90ee

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Sep 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

4hma4d commented Sep 24, 2024

Uh oh!

eric-wieser commented Sep 25, 2024

Uh oh!

github-actions bot commented Sep 25, 2024

Uh oh!

riccardobrasca commented Sep 25, 2024

Uh oh!

mathlib-bors bot commented Sep 25, 2024

Uh oh!

riccardobrasca commented Sep 25, 2024

Uh oh!

mathlib-bors bot commented Sep 25, 2024

Uh oh!

4hma4d commented Sep 26, 2024

Uh oh!

mathlib-bors bot commented Sep 26, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

4hma4d commented Aug 30, 2024 •

edited by eric-wieser

Loading

github-actions bot commented Aug 30, 2024 •

edited

Loading

eric-wieser Sep 10, 2024 •

edited

Loading