Simple eigenvector problem

Stream: new members

[MohanadAhmed]

Hi everyone,

I am trying to prove that the vector [0,0,1] is a an eigenvector of the matrix [2,0,0; 0, 1, 0; 0, 0, 1]. I am stuck with the compositions of the vec_head and vec_tail functions as can be seen below. Lean seems to know how to evaluate them as you can see from the #eval below them. Any help appreciated

import data.complex.basic
import data.matrix.basic
import data.fintype.card
import linear_algebra.matrix.to_lin
import linear_algebra.eigenspace

def M  := !![(2:ℂ), 0, 0; 0, 1, 0; 0, 0, 1]
def v: (fin 3) → ℂ := ![0, 0, 1]

open module.End.eigenvalues
open module.End
open matrix

example : has_eigenvector (matrix.to_lin' M) (1:ℂ) v := begin
  rw M, rw v,
  rw module.End.has_eigenvector, split,
  {
    rw mem_eigenspace_iff, rw matrix.to_lin'_apply,
    -- rw matrix.mul_vec_cons, rw zero_smul, rw one_smul,
    -- rw zero_add, rw matrix.mul_vec_cons,
    simp only [
      matrix.mul_vec_cons, zero_smul, one_smul,
      matrix.mul_vec_empty, add_zero, zero_add
    ],
    sorry,      -- Here is where the vec_head vec_tail compositions appear
  },
  simp only [ne.def, cons_eq_zero_iff, one_ne_zero, false_and, and_false, not_false_iff],
end

#check vec_head ∘ vec_tail ∘ vec_tail ∘ ![![2, 0, 0], ![0, 1, 0], ![0, 0, 1]]
#eval vec_head ∘ vec_tail ∘ vec_tail ∘ ![![2, 0, 0], ![0, 1, 0], ![0, 0, 1]]

[Eric Wieser]

Note you should write M using !![2,0,0; ...] not ![![2,0,0], ...]; the latter has the wrong type.

[Eric Wieser]

What goal are you left with at the sorry?

[MohanadAhmed]

Eric Wieser said:

Note you should write M using !![2,0,0; ...] not ![![2,0,0], ...]; the latter has the wrong type.

The single exclamation mark "array of arrays" is the result of applying the simplifier i.e. after

simp only [
      matrix.mul_vec_cons, zero_smul, one_smul,
      matrix.mul_vec_empty, add_zero, zero_add
    ],

Eric Wieser said:

What goal are you left with at the sorry?

The goal at the sorry is
vec_head ∘ vec_tail ∘ vec_tail ∘ ![![2, 0, 0], ![0, 1, 0], ![0, 0, 1]]

After a lot of just trying stuff randomly and then using the simplifier, the code below seems to get it done.

The simplifier originally applied mul_vec_cons. I replaced that with repeated application of cons_mul_vec followed by vec3_dot_product then calling the simplifier.

But this small problem cannot (or should not be!) that hard. What am I missing? Is the API to matrices and vectors too brittle or is the simplifier missing some lemmas?
Is there a shorter way?

import data.complex.basic
import data.matrix.basic
import data.matrix.notation
import data.fin.vec_notation
import data.fintype.vector
import data.fintype.card
import linear_algebra.matrix.to_lin
import linear_algebra.eigenspace
import tactic

def M  := !![(2:ℂ), 0, 0; 0, 1, 0; 0, 0, 1]
def v: (fin 3) → ℂ := ![0, 0, 1]

open module.End.eigenvalues
open module.End
open matrix

open_locale matrix

example : has_eigenvector (matrix.to_lin' M) (1:ℂ) v := begin
  rw M, rw v,
  rw module.End.has_eigenvector, split,
  {
    rw mem_eigenspace_iff, rw matrix.to_lin'_apply,
    rw matrix.cons_mul_vec,
    rw matrix.cons_mul_vec,
    rw matrix.cons_mul_vec,
    rw vec3_dot_product,
    rw vec3_dot_product,
    rw vec3_dot_product,
     simp only [ one_smul],
     simp only [cons_val_zero, mul_zero, cons_val_one, head_cons, cons_vec_bit0_eq_alt0, cons_vec_append, empty_vec_append,
  cons_vec_alt0, mul_one, zero_add, mul_vec_cons, empty_add_empty],
  },
  simp only [ne.def, cons_eq_zero_iff, one_ne_zero, false_and, and_false, not_false_iff],
end

[Eric Wieser]

MohanadAhmed said:

Eric Wieser said:

What goal are you left with at the sorry?

The goal at the sorry is
vec_head ∘ vec_tail ∘ vec_tail ∘ ![![2, 0, 0], ![0, 1, 0], ![0, 0, 1]]

I don't believe you, that goal doesn't have an = in it!

[MohanadAhmed]

Sorry I forgot to copy the RHS
vec_head ∘ vec_tail ∘ vec_tail ∘ ![![2, 0, 0], ![0, 1, 0], ![0, 0, 1]] = ![0, 0, 1]

I did the eval below it ,just to check if lean can calculate the LHS to be the same as the RHS.

[MohanadAhmed]

So #eval vec_head ∘ vec_tail ∘ vec_tail ∘ ![![2, 0, 0], ![0, 1, 0], ![0, 0, 1]] evaluates to ![0, 0, 1]

[Eric Wieser]

The ones you used in #eval are 0, 1, 2 : Nat, not 0, 1, 2 : R; lean doesn't know what R is so can't evaluate it

[Eric Wieser]

At any rate, I think ext, simp should make progress

[Eric Wieser]

With #18805 (edit: ), you can prove it as

example : has_eigenvector (matrix.to_lin' M) (1:ℂ) v := begin
  rw [module.End.has_eigenvector],
  split,
  { rw [mem_eigenspace_iff, matrix.to_lin'_apply],
    have : M.mul_vec v = ![2*0 + 0*0 + 0*1, 0*0 + 1*0 + 0*1, 0*0 + 0*0 + 1*1] :=
      (mul_vecᵣ_eq _ _).symm,
    rw [this, v],
    simp },
  simp only [v, ne.def, cons_eq_zero_iff, one_ne_zero, false_and, and_false, not_false_iff],
end

matrix.mul_vecᵣ_eq does all the boring expansion into the form you expect; you just have to write out the target expression.

[Kevin Buzzard]

Could this be a job for norm_num?

[Eric Wieser]

Perhaps. Note that with #15738 it's just a job for rw