Symmetric matrix eigen-decomposition

Stream: Is there code for X?

[Gabriel Moise]

Is there code for the following :

If Q is symmetric, then Q = R D R^T for some orthonormal matrix R and diagonal matrix D, where the columns of R constitute an orthonormal basis of eigenvectors of Q, and the diagonal matrix D is comprised of the corresponding eigenvalues of Q.

This proposition involves other helping lemmas, like showing that

If Q is a symmetric matrix, then Q has n (distinct) eigenvectors that form an orthonormal basis for ℜ^n.

and that

If Q is symmetric positive semi-definite, the eigenvalues of Q are nonnegative.

so, if there is code close to any of those, it would help as well. Thank you! :smile:

[Johan Commelin]

I'm not aware of anything in that direction. But @Anne Baanen is the local linalg expert (-;

[Anne Baanen]

I wish we had any matrix decompositions! I think this one is not too hard compared to say the LU-decomposition, though. We have docs#module.End.eigenspace, and if we have a basis on that, then we can probably get quite close with docs#is_basis_to_matrix_mul_linear_map_to_matrix

[Anne Baanen]

Looks like the eigen-stuff is less developed than I remembered. So this is still quite far away I'm afraid :(

[Oliver Nash]

On the other hand, I'm about to start using the eigen stuff and I might end up filling in some holes. I even just made a small PR: https://github.com/leanprover-community/mathlib/pull/7059

[Oliver Nash]

I was pretty happy to see there's a decent start already in place.

[Gabriel Moise]

Oh, I see! I was trying to follow the proofs from http://s3.amazonaws.com/mitsloan-php/wp-faculty/sites/30/2016/12/15032137/Symmetric-Matrices-and-Eigendecomposition.pdf so I though maybe some partial work has been done towards any small lemma there. I was thinking of writing the eigenstuff from the beginning, but I am not sure it can lead anywhere. So far, I have:

def has_eigen (M : matrix V V R) (μ : R) (x : V → R) : Prop :=
  x ≠ 0 ∧ (mul_vec M x = μ • x)

def has_eigenvector (M : matrix V V R) (x : V → R) : Prop :=
  ∃ μ : R, has_eigen M μ x

def has_eigenvalue (M : matrix V V R) (μ : R) : Prop :=
  ∃ x : V → R, has_eigen M μ x

def symmetric_matrix (M : matrix V V R) : Prop := M = Mᵀ

For the following lemmas, I supposed that M is symmetric.
Lemma 1 : The eigenvectors that correspond to different eigenvalues are orthogonal (DONE)

lemma different_eigenvalues_orthogonal_eigenvectors (M : matrix V V R) (H_symm : symmetric_matrix M) (v w : V → R) (μ μ' : R)
(H_ne : μ ≠ μ') (H₁ : has_eigen M μ v) (H₂ : has_eigen M μ' w) : dot_product v w = 0

Lemma 2: If there are two eigenvectors that have the same correspoding eigenvalue, then any linear combination of them (not 0) is also an eigenvector. (DONE)

lemma same_eigenvalue_linear_combination {M : matrix V V R} {a b : R} (H_symm : symmetric_matrix M) (v w : V → R) (μ : R)
(H_ne : a • v + b • w ≠ 0) (H₁ : has_eigen M μ v) (H₂ : has_eigen M μ w) : has_eigenvector M (a • v + b • w)

Lemma 3 : M has a full orthonormal basis of eigenvectors v1, . . . , vn. All eigenvalues and eigenvectors are real.
( I don't even have a formulation for this part, which is quite a crucial lemma :sad: )

Lemma 4 : M is diagonalizable. (main focus)

def orthogonal_matrix (M : matrix V V ℝ) : Prop := M ⬝ Mᵀ = (1 : matrix V V ℝ)
def diagonal_matrix (M : matrix V V ℝ) : Prop := ∀ i j : V, i ≠ j → M i j = 0

-- A real square matrix M is orthogonally diagonalizable if there exist an orthogonal matrix U and a
-- diagonal matrix D such that M = U ⬝ D ⬝ Uᵀ.
def diagonalizable_matrix (M : matrix V V ℝ) : Prop :=
  ∃ U D : matrix V V ℝ, orthogonal_matrix U ∧ diagonal_matrix D ∧ M = U ⬝ D ⬝ Uᵀ
lemma matrix_diagonalization (H_symm : symmetric_matrix M) : diagonalizable_matrix M

I am not quit sure I can get anywhere with what I started, I was following the material from :

• https://ocw.mit.edu/courses/mathematics/18-409-topics-in-theoretical-computer-science-an-algorithmists-toolkit-fall-2009/lecture-notes/MIT18_409F09_scribe1.pdf
• http://s3.amazonaws.com/mitsloan-php/wp-faculty/sites/30/2016/12/15032137/Symmetric-Matrices-and-Eigendecomposition.pdf
  and trying to implement what they prove. Any suggestion is more than welcomed, since I am not a very experienced Lean programmer, nor a very good mathematician :smile: