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

I was not able to use the theorem
protected theorem mul_assoc
in thedata.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 thesorry
inABveqzv_BABveqzBV
? 
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
withmathlib, 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 labelledtactic execution
, since it seems to be the bulk of the time?
cumulative profiling times:
compilation 0.0024ms
decl postprocessing 0.0083ms
elaboration 23.2s
elaboration: tactic compilation 38.6ms
elaboration: tactic execution 22.1s
parsing 199ms
type checking 15.6ms
 Any thoughts on the proof. It was very adhoc 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 (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 postprocessing 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 : (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