feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices #6042

MohanadAhmed · 2023-07-21T15:08:44Z

This file provides proves the SVD theorem which decomposes a real/complex matrix into left eigenvectors, singular values block diagonal matrix and right eigenvectors.

Any matrix A (M × N) with rank r = A.rank and with elements in ℝ or ℂ fields can be decompsed into the product of three matrices:
$$A = USV$$

The three matrices are defined as
- $U$: an M × M matrix containing the left eigenvectors of the matrix
- $S$: an M × N matrix with an r × r block in the upper left corner with nonzero singular values
- $V$: an N × N matrix containing the right eigenvectors of the matrix
  Note that
$S$ is a block matrix $S = [S₁₁, S₁₂; S₂₁, S₂₂]$ with
- $S₁₁$: a diagonal r × r matrix and
- $S₁₂$ : r × (N - r) zero matrix, S₂₁ : (M - r) × r zero matrix and
- $S₂₂$: (M - r) × (N - r) zero matrix
$U$ is a block column matrix U = [U₁ U₂] with
- $U₁$ : a M × r containing left eigenvectors with nonzero singular values.
- $U₂$ : a M × (M - r) containing left eigenvectors with zero singular values.
$V$ is a block column matrix V = [V₁ V₂] with
- $V₁$ : a N × r containing right eigenvectors with nonzero singular values.
- $V₂$ : a M × (M - r) containing right eigenvectors with zero singular values.

Since in mathlib the eigenvalues of hermitian matrices are defined in an "arbitrary" undetermined order, we begin by partition the singular values into zero and non-zero values. We partition the corresponding eigenvectors from AᴴA and AAᴴ using similar rearrangements. These are included in SVD.svdReindex. The basic API for Column and Row partitioned matrices is from ColumnRowPartitioned.

We then proceed to transfer some of the lemmas we need about eigenvector matrices (for example that they are unitary: i.e. inverse is conjugate transpose.). Note that since invertibility in mathlib is defined for square matrices while our matrices are partitioned i.e. N × (N₁ ⊕ N₂) and N ≃ (N ⊕ N₂), Lean cannot apply the Invertible definition. We workaround this were necessary.

Lemma reduced_spectral_theorem (reduced_spectral_theorem') shows that AᴴA and AAᴴ, can be reduced to products containing only the non-zero singular eigenvectors. This is later used in proving the main SVD theroem. A few lemmas are provided about the invertibility of the non-zero singular values matrix: svdσ_inv, σ_inv_μ_σ_inv_eq_one, IsUnit_det_svdσ, IsUnit_det_svdσ_mapK and svdσ_inv_mapK.

To make relating left eigenvectors to right eigenvectors easier we define U₁ = AV₁σ⁻¹ while U₂ is obtained from the eigenvectors of (AAᴴ). This avoid a lengthy reindexing operation with many proofs. The vectors in U₂ have no such issue since they are multiplied by zero singular values anyway.

Co-authored-by: Mohanad Ahmed m.a.m.elhassan@gmail.com

Mathlib/LinearAlgebra/Matrix/SVD/ColumnRowBlocks.lean

eric-wieser · 2023-07-21T16:43:15Z

Mathlib/LinearAlgebra/Matrix/SVD/RankMulIsUnit.lean

I think these results should go in the existing matrix rank file; and they might already exist there!

I presume you mean this one. according to my looking they are not there (I did this search earlier when the proof was in lean 3 and again when I moved my proof to lean 4)

What I mean is that you should add your results below the existing results in that file!

sgouezel · 2023-09-21T15:41:56Z

Mathlib/LinearAlgebra/Matrix/SVD/Defs.lean

+Any matrix A (M × N) with rank r = A.rank and with elements in the field ℝ or ℂ can be decomposed
+into the product of three matrices `A = UξVᴴ` where:
+
+  * U: an `M × M` matrix containing the left eigenvectors of the matrix
+  * ξ: an `M × N` matrix with an `r × r` block in the upper left corner with nonzero singular values
+  * V: an `N × N` matrix containing the right eigenvectors of the matrix


I am completely confused by this docstring. To me, singular values of a matrix A have to do with the successive maximum expansion rates of the matrix, so I don't see how left or right eigenvectors of the matrix A would appear in a singular value decomposition.

Also, you should probably recall the definition of the singular values, as there are various definitions (notably do you have r singular values, or min M N of them, or infinitely many of them but all zero after step r).

The singular values for me are square roots of eigenvalues of AHA and AAH. They are also what remains of the matrix transformation if we rotate the source and target vector spaces until the transformation is diagonal.

The Singular Value Decomposition is a generalization of the Eigendecompositon. We sometimes abuse terminology and call the left singular vectors left eigenvectors and similarly for the right singular vectors.

If we write left singular vector in place of left eigenvectors and right singular vector in place of right eigenvectors, does that work for you?

* U: an `M × M` matrix containing the left singular vector of the matrix * ξ: an `M × N` matrix with an `r × r` block in the upper left corner with nonzero singular values * V: an `N × N` matrix containing the right singular vectorof the matrix

I did not define a function for singular values. I only defined the matrix of singular values which has the same dimensions as the original matrix A. It is also partitioned such that it is upper left block of size $r \times r$ contains the $r$ non-zero singular values.

I have no Idea what the maximum expansion rate of a matrix is.

sgouezel · 2023-09-21T15:42:52Z

Mathlib/LinearAlgebra/Matrix/SVD/Defs.lean

+Singular Value decomposition, SVD
+-/
+
+variable {𝕂 : Type*} [IsROrC 𝕂] [DecidableEq 𝕂]


Why did you put a [DecidableEq 𝕂] assumption?

Probably IsROrC should extend DecidableEq, since we already have DecidableEq Real and DecidableEq Complex instances.

Throughout the PR you will find comparisons against zero for example:

lemma rank_eq_card_pos_eigs_conjTranspose_mul_self (A: Matrix (Fin M) (Fin N) 𝕂) : A.rank = Fintype.card {i // (isHermitian_transpose_mul_self A).eigenvalues i ≠ 0} := by rw [← rank_conjTranspose_mul_self, IsHermitian.rank_eq_card_non_zero_eigs]

My understanding is this requires decidable equality to work.

#7315 looks to be a good solution here, as it seems we had this pattern elsewhere too.

sgouezel · 2023-09-21T15:43:43Z

Mathlib/LinearAlgebra/Matrix/SVD/Defs.lean

+namespace Matrix
+
+/-- The right eigenvectors of a matrix A corresponding to its non-zero eigenvalues -/
+noncomputable def svdV₁ (A : Matrix (Fin M) (Fin N) 𝕂) : Matrix (Fin N) (Fin (A.rank)) 𝕂 :=


the names in mathlib have to convey a meaning. In general, they are longer and more expressive than the names we would use in papers (which are just notations), because they have to be compatible with the whole library.

… nonneg

…ces (#7249) Lemmas `toBlocks₁₁_diagonal`, `toBlocks₂₂_diagonal`, `toBlocks₁₂_diagonal`, `toBlocks₂₁_diagonal` to make dealing with sub blocks of diagonal matrices a bit easier Useful for PR #6042

@Vierkantor

…7266) Given two matrices $A$ and $B$ whose product is 1 $AB = 1$, then left multiplication/right multiplication with these matrices from the appropriate side is an injection. Suggested by @Vierkantor in PR #6042

Mathlib/LinearAlgebra/Matrix/SVD/Reindex.lean

@Vierkantor

The PR provides two lemmas showing that the eigenvalues of $A\^HA$ and $AA^H$ are non-negative: - `eigenvalues_conjTranspose_mul_self_nonneg`: $$\text{eig}(A\^H A) \geq 0 $$ - `eigenvalues_self_mul_conjTranspose_nonneg`: $$\text{eig}(A A\^H) \geq 0 $$ This was suggested by @Vierkantor in PR #6042

Vierkantor · 2023-09-26T13:13:59Z

Sorry for the weeks of barely any contact. I finally have some real time to invest in reviewing. I hope I addressed all the open questions you still had.

We've been discussing this PR with the mathlib reviewer team, and I'm afraid that we concluded that this result still needs quite some work. Namely, we find it important to get the decomposition also for homomorphisms (specifically, elements of Module.End), and it seems better to first prove SVD for homomorphisms, and then derive the matrix result from that. Basically, the same approach as we already have for eigenvalues in mathlib.

MohanadAhmed · 2023-09-26T13:53:22Z

Sorry for the weeks of barely any contact. I finally have some real time to invest in reviewing. I hope I addressed all the open questions you still had.

We've been discussing this PR with the mathlib reviewer team, and I'm afraid that we concluded that this result still needs quite some work. Namely, we find it important to get the decomposition also for homomorphisms (specifically, elements of Module.End), and it seems better to first prove SVD for homomorphisms, and then derive the matrix result from that. Basically, the same approach as we already have for eigenvalues in mathlib.

@Vierkantor
Can you spell out what this means for this PR?

j-loreaux · 2024-02-13T18:58:16Z

@MohanadAhmed if you're interested in reviving this PR, let's discuss the plan on the Zulip thread.

In the meantime I'm marking this as WIP since we'll plan to refactor a bit.

MohanadAhmed added 19 commits July 19, 2023 10:19

Some starter work on Columns and Row Matrices for SVD

1565c01

Merge remote-tracking branch 'origin/master' into MohanadAhmed/svd

3fb06d3

Fit the 100 char line limit

d032a14

Complete comment descriptions of lemmas in ColumnRowBlocks.lean file

512ae3a

Import ColumnRowBlocks file into mathlib

c4fed53

IsROrC StarOrderedRing and Kernels of Mat mul conjTranspose

fe5bcbf

Multiplication by an invertible matrix

2be5943

Lots of stuff that might get lost

8c0514a

Some sleepless mess

a3baa4c

shorten the proof

f79af75

Delete a lot of hard but unncessary work!!!

08f6478

Finally the SVD Theorem is working

7c14e7e

Some documentation

3e02177

Some more clarification

8d32a2a

Include the "main" file in Mathlib.lean

4d35b5b

100 Line Limit

d5ecd84

Fix ERR_LIN and ERR_COP linter errors

bd63ad3

Clean ERR_IBY errors

f61ebe6

Clear unused variable warning

35173a4

eric-wieser reviewed Jul 21, 2023

View reviewed changes

Mathlib/LinearAlgebra/Matrix/SVD/ColumnRowBlocks.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 21, 2023

View reviewed changes

MohanadAhmed added 9 commits July 21, 2023 19:45

Clear "Check all files imported error"

f73fba8

Eric's suggested doc string should mention mul_eq_one_comm

3275f5e

Unused arguments build linter complaints

53569dd

replace equiv_sum_trans with Equiv.sumCongr

438fae5

Final removal equiv_sum_trans

5ed356b

Shutup all files imported linter

7681902

UnusedArgs linter complains about DecidableEq m

b05969a

Unusedarg linter

c8efec7

Trying not to interfere with simp

f5accd9

MohanadAhmed added 7 commits September 20, 2023 15:37

some cleanup

001b099

Merge remote-tracking branch 'origin/master' into MohanadAhmed/svd

7b694a0

remove inj lemmas

d2c2a76

use left inj

77da598

leftinj

8c2d63d

some stuff

b21f417

renames

34a136f

MohanadAhmed added awaiting-review The author would like community review of the PR awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 20, 2023

github-actions bot removed the awaiting-CI label Sep 20, 2023

sgouezel reviewed Sep 21, 2023

View reviewed changes

MohanadAhmed mentioned this pull request Sep 21, 2023

[Merged by Bors] - feat: eigenvalues of AᴴA and AAᴴ are non-negative #7312

Closed

MohanadAhmed added 2 commits September 22, 2023 00:21

Merge remote-tracking branch 'origin/master' into MohanadAhmed/svd

6312b8c

@Vierkantor suggestion get nezero form buried prop and prove AhA eigs…

52b9199

… nonneg

alexjbest reviewed Sep 22, 2023

View reviewed changes

Mathlib/LinearAlgebra/Matrix/SVD/Reindex.lean Outdated Show resolved Hide resolved

MohanadAhmed added 3 commits September 22, 2023 21:11

spacing in Reindex file after Matrix A

2b4109f

Reduced Spectral Theorem for the U1 (without prime matrix)

07b5beb

Merge remote-tracking branch 'origin/master' into MohanadAhmed/svd

b125ddc

Vierkantor removed their assignment Feb 13, 2024

j-loreaux self-assigned this Feb 13, 2024

j-loreaux added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Feb 13, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices #6042

feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices #6042

MohanadAhmed commented Jul 21, 2023 •

edited by jcommelin

eric-wieser Jul 21, 2023

MohanadAhmed Jul 21, 2023

eric-wieser Jul 21, 2023

sgouezel Sep 21, 2023 •

edited

MohanadAhmed Sep 21, 2023 •

edited

sgouezel Sep 21, 2023

eric-wieser Sep 21, 2023

MohanadAhmed Sep 21, 2023

eric-wieser Sep 21, 2023

sgouezel Sep 21, 2023

Vierkantor commented Sep 26, 2023

MohanadAhmed commented Sep 26, 2023 •

edited

j-loreaux commented Feb 13, 2024 •

edited

feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices #6042

Are you sure you want to change the base?

feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices #6042

Conversation

MohanadAhmed commented Jul 21, 2023 • edited by jcommelin

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgouezel Sep 21, 2023 • edited

Choose a reason for hiding this comment

MohanadAhmed Sep 21, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vierkantor commented Sep 26, 2023

MohanadAhmed commented Sep 26, 2023 • edited

j-loreaux commented Feb 13, 2024 • edited

MohanadAhmed commented Jul 21, 2023 •

edited by jcommelin

sgouezel Sep 21, 2023 •

edited

MohanadAhmed Sep 21, 2023 •

edited

MohanadAhmed commented Sep 26, 2023 •

edited

j-loreaux commented Feb 13, 2024 •

edited