Eigenvalue of matrix products AB and BA

Stream: new members

[MohanadAhmed]

Hello everyone,

I have been trying to prove the following:

Let wo matrices $A (m \times n)$ and $B (n \times m)$ such that the two products $AB$ and $BA$ can be formed and if $z$ is an eigenvalue of $AB$ and $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:

$$\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 $z$ is an eigenvalue if we can show that $Bv$ (the proposed eigenvector of $BA$) is not zero. Assume by way of contradiction $Bv = 0$. Then:

$$\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 = zv$ to $BABv = 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

3. 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: (A⬝B).mul_vec v = z•v)
:
(B⬝(A⬝B)).mul_vec v = z•(B.mul_vec v) :=
begin
  sorry,
end

lemma eig_AB_is_eig_BA
  {A: matrix m n ℂ} {B: matrix n m ℂ}
  (z: ℂ)
  (hEigz: has_eigenvalue (matrix.to_lin' (A⬝B)) z)
  (hEigzNz: z ≠ 0)
  :
  (has_eigenvalue (matrix.to_lin' (B⬝A)) z) :=
begin
  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, {
    by_contra,
    rw to_lin' at hsMul,
    simp at hsMul,
    rw ← mul_vec_mul_vec at hsMul,
    rw h at hsMul, simp at hsMul,
    have hxra: z•v = 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' (B⬝A)) 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,
end

[Alex J. Best]

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]

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]

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

[MohanadAhmed]

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]

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]

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 : (A⬝B).mul_vec v = z•v) :
  (B⬝(A⬝B)).mul_vec v = z•(B.mul_vec v) :=
begin
  rw [←matrix.mul_vec_smul, ←hinj, ←matrix.mul_vec_mul_vec],
end

Note that it goes faster the less you import

[MohanadAhmed]

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 $B$ from the left"?

[Alex J. Best]

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

[Eric Wieser]

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

[Eric Wieser]

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

[MohanadAhmed]

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,
  tauto,

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

[Eric Wieser]

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

[Eric Wieser]

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]

You want either assumption or exact hinj

[Michael Stoll]

or rwa [...] at hinj?

[MohanadAhmed]

@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]

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