Zulip Chat Archive

Stream: Is there code for X?

Topic: Symmetric matrix eigen-decomposition

view this post on Zulip Gabriel Moise (Apr 06 2021 at 11:24):

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:

view this post on Zulip Johan Commelin (Apr 06 2021 at 11:25):

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

view this post on Zulip Anne Baanen (Apr 06 2021 at 11:29):

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

view this post on Zulip Anne Baanen (Apr 06 2021 at 11:35):

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

view this post on Zulip Oliver Nash (Apr 06 2021 at 11:44):

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

view this post on Zulip Oliver Nash (Apr 06 2021 at 11:45):

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

view this post on Zulip Gabriel Moise (Apr 06 2021 at 11:58):

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 :

Last updated: May 07 2021 at 22:14 UTC