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

1. Any thoughts on the proof. It was very ad-hoc so I guess it can use a lot of improvement?

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 (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 ?

#### 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 : (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 (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 $B$ 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,
tauto,

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