## Stream: Is there code for X?

### Topic: Symmetric matrix eigen-decomposition

#### 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:

#### 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 (-;

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

#### 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 :(

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

#### Oliver Nash (Apr 06 2021 at 11:45):

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

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