Zulip Chat Archive

Stream: new members

Topic: Eigenvalue of matrix products AB and BA

MohanadAhmed (Mar 26 2023 at 22:21):

Hello everyone,

I have been trying to prove the following:

Let wo matrices A(m×n) A (m \times n) and B(n×m) B (n \times m) such that the two products AB AB and BA BA can be formed and if zz is an eigenvalue of AB AB and z0 z \neq 0 is not zero then it must be an eigenvalue of BA. The math proof seemed straight forward but it took a lot a head banging to get the code shown below.

The math proof goes something like the following:

z is a non zero eigenvalue ofAB    vCm and v0ABv=zv    BABv=B(zv)    BA(Bv)=z(Bv)\begin{aligned} &z \text{ is a non zero eigenvalue } of AB \\ &\implies \exists v \in \mathbb{C}^m \text{ and } v \neq 0 | ABv = zv \\ &\implies BABv = B(zv) \implies BA (Bv) = z(Bv) \\ \end{aligned}

The last equation implies zz is an eigenvalue if we can show that BvBv (the proposed eigenvector of BABA) is not zero. Assume by way of contradiction Bv=0Bv = 0. Then:

ABv=A(Bv)=A0=0But v0    zv0But ABv=zv    0=zv0 a contradiction \begin{aligned} &ABv = A(Bv) = A0 = 0 \\ \text{But }\quad &v \neq 0 \implies zv \neq 0 \\ \text{But }\quad &ABv = zv \implies 0 = zv \neq 0 \rightarrow \text{ a contradiction } \end{aligned}

Below is my attempt. I have a few questions:

  1. I was not able to use the theorem protected theorem mul_assoc in the data.matrix.basic file. Is this because it is protected? How do I make use of it? Is there any other convenient way to go from ABv=zvABv = zv to BABv=zBVBABv = zBV? Any other suggestions to replace the sorry in ABveqzv_BABveqzBV ?

  2. The update of the status in vscode takes a long time after every modification I have to wait like 20 sec. (I am using lean3.50 with mathlib, rev=57e09a1296bfb4330ddf6624f1028ba186117d82). I ran the profile option on the lean executable and got this summary (I can post the whole log if necessary). I this expected? Is there any way I can cut down the item labelled tactic execution, since it seems to be the bulk of the time?

cumulative profiling times:
        compilation 0.0024ms
        decl post-processing 0.0083ms
        elaboration 23.2s
        elaboration: tactic compilation 38.6ms
        elaboration: tactic execution 22.1s
        parsing 199ms
        type checking 15.6ms
  1. Any thoughts on the proof. It was very ad-hoc so I guess it can use a lot of improvement?

Thanks a lot in advance for your time and help.

Here is my attempt:

import data.complex.basic
import data.matrix.basic
import linear_algebra.matrix.to_lin
import linear_algebra.eigenspace
import analysis.matrix
import analysis.inner_product_space.pi_L2

open_locale matrix big_operators complex_conjugate
open matrix
open module
open module.End
open linear_map
open orthonormal_basis

variables {m n l p : Type*}
variables [fintype m] [fintype n] [fintype l] [fintype p]
variables [decidable_eq m] [decidable_eq n] [decidable_eq l] [decidable_eq p]

theorem ABveqzv_BABveqzBV {A: matrix m n } {B: matrix n m } {z: } {v: m  }
(hinj: (AB).mul_vec v = zv)
(B(AB)).mul_vec v = z(B.mul_vec v) :=

lemma eig_AB_is_eig_BA
  {A: matrix m n } {B: matrix n m }
  (z: )
  (hEigz: has_eigenvalue (matrix.to_lin' (AB)) z)
  (hEigzNz: z  0)
  (has_eigenvalue (matrix.to_lin' (BA)) z) :=
  have hVecExists := hEigz.exists_has_eigenvector,
  cases hVecExists with v hv,
  have hsMul := hv.apply_eq_smul,
  cases hv with _ hvNz,
  have BvNz : B.mul_vec v  0, {
    rw to_lin' at hsMul,
    simp at hsMul,
    rw  mul_vec_mul_vec at hsMul,
    rw h at hsMul, simp at hsMul,
    have hxra: zv = 0, by {rw hsMul,},
    clear hsMul,
    rw smul_eq_zero at hxra,
    cases hxra with hzz hvz,
    exact hEigzNz hzz,
    exact hvNz hvz,

  have BvEig : has_eigenvector (matrix.to_lin' (BA)) z (B.mul_vec v), {
    unfold has_eigenvector,
    rw to_lin' at hsMul,
    simp at hsMul,
    rw mem_eigenspace_iff,
    split, rw [to_lin'], simp,
    exact ABveqzv_BABveqzBV hsMul,
    exact BvNz,
  exact has_eigenvalue_of_has_eigenvector BvEig,

Alex J. Best (Mar 26 2023 at 22:27):

Protected lemmas need to be used via their full name (in this case matrix.mul_assoc) this is normally done when the name is too common so it would overlap too much with other lemmas otherwise.

Alex J. Best (Mar 26 2023 at 22:29):

20s indeed does seem a bit long, I'd recommend commenting out different parts of your proof (using sorry { stuff } to disable bits of it) and seeing where the slow parts are, if there is one line that is taking most of the time or something we can definitely look at how to improve that

Alex J. Best (Mar 26 2023 at 22:29):

In general though, breaking larger proofs down into lots of smaller lemmas is always helpful for speed

MohanadAhmed (Mar 26 2023 at 22:51):

Thanks @Alex J. Best .
I tried what you suggested, commenting out and reprofiling. I made a guess that the simp tactic is the one taking a good bulk of the time. After replacing all the simps with simp only. It seems the time got better. The lean --profile command shows a reduction to 2sec.

cumulative profiling times:
        compilation 0.0025ms
        decl post-processing 0.007ms
        elaboration 2.34s
        elaboration: tactic compilation 29ms
        elaboration: tactic execution 2.09s
        parsing 207ms
        type checking 15.7ms

In VSCode however the time feels a bit more than that. But hey I will take that over the 20 secs :sweat_smile:

Any thoughts on the sorry in the theorem ABveqzv_BABveqzBV ?
Thanks again for your help.

Eric Wieser (Mar 26 2023 at 23:00):

You might be interested to know about set_option profiler true which lets you turn on profiling for a single block of code

Eric Wieser (Mar 26 2023 at 23:02):

Here's a proof of your missing lemma:

import data.matrix.basic
import data.complex.basic

open_locale matrix

variables {m n l p : Type*}
variables [fintype m] [fintype n] [fintype l] [fintype p]
variables [decidable_eq m] [decidable_eq n] [decidable_eq l] [decidable_eq p]

theorem ABveqzv_BABveqzBV {A : matrix m n } {B : matrix n m } {z : } {v : m  }
  (hinj : (AB).mul_vec v = zv) :
  (B(AB)).mul_vec v = z(B.mul_vec v) :=
  rw [matrix.mul_vec_smul, hinj, matrix.mul_vec_mul_vec],

Note that it goes faster the less you import

MohanadAhmed (Mar 26 2023 at 23:13):

Nice! Thanks a lot @Eric Wieser
A question poses it self to me,
In the second rewrite using hinj, you replaced the left side in the goal.
But is there a way to do it more "naturally", i.e. what is the lean equivalent of "multiply both sides of hinj by matrix BB from the left"?

Alex J. Best (Mar 26 2023 at 23:20):

You can use tactic#apply_fun for that something like apply_fun ((⬝) B) at hinj

Eric Wieser (Mar 26 2023 at 23:37):

replace hinj := congr_arg B.mul_vec hinj, does what you need

Eric Wieser (Mar 26 2023 at 23:38):

It's a matrix/vector multiply not a matrix/matrix, so you can't use like Alex suggests

MohanadAhmed (Mar 26 2023 at 23:42):

Using Alex's suggestion I tried apply_fun (B.mul_vec) at hinj. It seems to work

apply_fun (B.mul_vec) at hinj, -- Alex J Best'ts Suggestion.
  rw [matrix.mul_vec_mul_vec, mul_vec_smul] at hinj,

  -- rw [←matrix.mul_vec_smul, ←hinj, ←matrix.mul_vec_mul_vec], -- Eric Wiesers Proof

Eric Wieser (Mar 26 2023 at 23:55):

What's the goal state at the point you did tauto?

Eric Wieser (Mar 26 2023 at 23:55):

If it's what I think it is and hinj is exactly the goal, that's a massively overkill tactic that will make everything slower

Eric Wieser (Mar 26 2023 at 23:55):

You want either assumption or exact hinj

Michael Stoll (Mar 27 2023 at 01:07):

or rwa [...] at hinj?

MohanadAhmed (Mar 27 2023 at 07:50):

@Eric Wieser
Yes it is exactly hinj.
Thanks that is very useful to know.
Any references or thoughts on which tactics on which tactics to avoid? or which are slower than others?

Kevin Buzzard (Mar 27 2023 at 08:16):

Non terminal simps, finish, tidy and omega can sometimes be slow

Last updated: Dec 20 2023 at 11:08 UTC