Zulip Chat Archive
Stream: new members
Topic: Equivalence between subtypes given a certain property
MohanadAhmed (May 31 2023 at 20:23):
Let $f_m$ be function mapping fin m
into real numbers and $f_n$ be a function mapping fin n
into a real numbers. The functions have the same nonzero values, but one might have many more zeros than the other. As such the "Number" of nonzero elements is the same in the range of the functions. I want to say there is an equivalence between the elements of fin m
and elements of fin n
that lead to the nonzero values in the results of functions $f_m$ and $f_n$ respectively.
The lemma definition at the bottom of the page does not even type check and lean has the short but uninformative error message `invalid expression starting at 36:2. So my questions are:

How do I express equivalence between two subtypes?
In this case the subtypes offin m
andfin n
that give nonzero values infm
andfn
respectively? 
Given the two lemmas
zero_or_fn_in_fm
andzero_or_fm_in_fn
how do I go about provingnon_zero_parts_equiv
?
import data.complex.basic
import linear_algebra.matrix.hermitian
import linear_algebra.matrix.pos_def
import linear_algebra.matrix.determinant
import linear_algebra.matrix.spectrum
open matrix
open_locale matrix complex_conjugate big_operators
def m: ℕ := 10
def n: ℕ := 14
/ Nonzero in fm is in fn /
lemma zero_or_fm_in_fn (fm : fin m → ℝ)(fn : fin n → ℝ):
∀(i: fin m), fm i = 0 ∨ (∃ (j: fin n), fn j = fm i) := sorry
/ Flipped Around /
lemma zero_or_fn_in_fm (fm : fin m → ℝ)(fn : fin n → ℝ):
∀(j: fin n), fn j = 0 ∨ (∃ (i: fin m), fn j = fm i) := sorry
def pm (fm : fin m → ℝ): fin m → Prop := (λ i, (fm i = 0))
def pn (fn : fin n → ℝ): fin n → Prop := (λ j, (fn j = 0))
noncomputable def pm_dec (fm : fin m → ℝ): decidable_pred (pm fm) := begin
unfold decidable_pred,
intro a,
rw pm, dsimp,
exact eq.decidable (fm a) 0,
end
/ I want to say there is an equivalence relation between
elements of fin m giving nonzero values for fm and the
elements of fin n giving nonzero values for fn.
/
lemma non_zero_parts_equiv (fm : fin m → ℝ)(fn : fin n → ℝ):
∃ e: ({i : fin m // pm fm} ≃ {j : fin n // pn fn}) := sorry
Eric Wieser (May 31 2023 at 21:29):
It doesn't typecheck because the syntax is ∃ x : X, p x
, not ∃ x : X
Eric Wieser (May 31 2023 at 21:29):
You can fix that with ∃ x : X, true
, but that's just a silly way of writing nonempty X
Eric Wieser (May 31 2023 at 21:30):
Are you sure you're not looking for X
by itself though? Here, that would be an algorithm for constructing the equiv
Eric Wieser (May 31 2023 at 21:33):
Your statement is sort of true by definition: #A = #B
(ie, the size of each type, docs#cardinal.mk, being the same) means nonempty (A ≃ B)
)
Eric Wieser (May 31 2023 at 21:35):
If you did want to prove this I think you could use docs#fin_enum to enumerate the elements in order...
Eric Wieser (May 31 2023 at 21:35):
... but this sounds like an #xy problem to me
MohanadAhmed (May 31 2023 at 22:12):
If I understand Wikipedia's description of XY problem. It means I should describe my original problem and leave the 'toy' version above which might obscure things. Well then! Here is a description of the original problem:
AB to BA Eigenvalue Problems
Let $A \in \mathbb{C} (m \times n)$ and $B \in \mathbb{C} (n \times m)$ matrices that are not necessarily square. I want to express the following fact from linear algebra:
Let $r$ be an integer representing the rank of the matrix $AB$. It is also the rank of the matrix $BA$. i.e. $r = \text{rank}{(AB)}= \text{rank}{(BA)}$ with $r \leq \text{min}{(m,n)}$. This is the number of nonzero eigenvalues. We can show in lean that the eigenvalues that are non zero are common between both. The first half of the proof is here > Eigenvalue of matrix products AB and BA. But that statement even if made in both directions is still lacking. What I want to say is
" The multiset (accounting for multiplicities) of nonzero eigenvalues in matrices $AB$ and $BA$ are the same and I want an equivalence that allows me to move between them"
The $A^HA$ to $AA^H$ Eigenvalues Problem
Starting from mathlib in its current form without more work the above looked a bit far. So I started with what I though to be a "simpler problem" (famous last words of many dead!)
Consider the matrices $A^HA$ and $AA^H$. These are nice matrices, very nice! Hermitian, Real Eigenvalues and in mathlib there is docs#matrix.is_hermitian.eigenvalues that reuses the matrix index. Hence we now have two function from indices fin m
to the eigenvalues of $A^HA$ and fin n
$AA^H$ to the eigenvalues. These sets of eigenvalues are the same if you discount the zero eigenvalues.
The SVD Relation
A useful side effect of proving this equivalence (between the subsets from fin m
and fin n
)is that having an SVD proof becomes much closer. You can reorder the results of docs#matrix.is_hermitian.spectral_theorem using your equivalence relation for both matrix decompositions and voila! you have an SVD decomposition.
Back to the question
How do I permute the eigenvalues sets of the two above matrices such that I have a bijection/equivalence between subtypes representing the nonzero elements of the eigenvalue functions of each matrix?
MohanadAhmed (May 31 2023 at 22:19):
So using your suggestion for the lemma statement:
import data.complex.basic
import linear_algebra.matrix.hermitian
import linear_algebra.matrix.pos_def
import linear_algebra.matrix.determinant
import linear_algebra.matrix.spectrum
open matrix
open_locale matrix complex_conjugate big_operators
def m: ℕ := 10
def n: ℕ := 14
/ Nonzero in fm is in fn /
lemma zero_or_fm_in_fn (fm : fin m → ℝ)(fn : fin n → ℝ):
∀(i: fin m), fm i = 0 ∨ (∃ (j: fin n), fn j = fm i) := sorry
/ Flipped Around /
lemma zero_or_fn_in_fm (fm : fin m → ℝ)(fn : fin n → ℝ):
∀(j: fin n), fn j = 0 ∨ (∃ (i: fin m), fn j = fm i) := sorry
def pm (fm : fin m → ℝ): fin m → Prop := (λ i, (fm i = 0))
def pn (fn : fin n → ℝ): fin n → Prop := (λ j, (fn j = 0))
#check pm
/ I want to say there is an equivalence relation between
elements of fin m giving nonzero values for fm and the
elements of fin n giving nonzero values for fn.
/
lemma non_zero_parts_equiv (fm : fin m → ℝ)(fn : fin n → ℝ):
nonempty({i : fin m // pm fm i} ≃ {j : fin n // pn fn j}):=
begin
end
MohanadAhmed (May 31 2023 at 22:20):
What do mean by " Here, that would be an algorithm for constructing the equiv"?
Kevin Buzzard (May 31 2023 at 22:26):
This idea that "real eigenvalues" are helping is I think false. The original question makes sense over any field, and any attempt to use special properties of R or C will end up with you proving a special case of the lemma which would not be suitable for mathlib.
Kevin Buzzard (May 31 2023 at 22:30):
Wait, this isn't even true is it? Let A=(0 1;0 0) and B=(1 0;0 0)
Kevin Buzzard (May 31 2023 at 22:33):
Or A=(1,1), B=(1;1)
MohanadAhmed (May 31 2023 at 22:38):
Kevin Buzzard said:
Wait, this isn't even true is it? Let A=(0 1;0 0) and B=(1 0;0 0)
You mean the statement an eigenvalue of $AB$ that is nonzero is an eigenvalue of $BA$?
MohanadAhmed (May 31 2023 at 22:39):
Lets begin with the second case example A = [1, 1] and B = [1; 1] I assume this is MATLAB notation i.e. A is a row and B is a column
MohanadAhmed (May 31 2023 at 22:40):
AB = 0
BA = [1 1; 1 1]
MohanadAhmed (May 31 2023 at 22:42):
AB is the zero matrix of size 1 x 1
MohanadAhmed (May 31 2023 at 22:42):
Nothing much to say here
MohanadAhmed (May 31 2023 at 22:43):
BA is the matrix [1 1; 1 1] ==> Charactersitic polynomial is the x^2 polynomial.
The only roots are zero and zero
MohanadAhmed (May 31 2023 at 22:44):
But these are already discounted in the statement. i.e. we are only concerned with nonzero eigenvalues
Kevin Buzzard (May 31 2023 at 22:44):
No, the claim that the ranks are equal
Kevin Buzzard (May 31 2023 at 22:44):
Or maybe you're using a nonstandard definition of the rank of a matrix?
MohanadAhmed (May 31 2023 at 22:45):
For square matrices in my head rank is the number of nonzero eigenvalues
Kevin Buzzard (May 31 2023 at 22:45):
Well in the textbooks rank is something else :/
MohanadAhmed (May 31 2023 at 22:45):
But that is not the correct definition
MohanadAhmed (May 31 2023 at 22:46):
You are right. rank(AB) \neq rank(BA)
MohanadAhmed (May 31 2023 at 22:46):
But No of NonZeroEigs(AB) = NonZeroEigs(BA)?
Kevin Buzzard (May 31 2023 at 22:46):
But I agree that the char power series are the same  yes
Kevin Buzzard (May 31 2023 at 22:47):
The char power series of a square matrix M is det(1tM), probably there is a better name for it
Kevin Buzzard (May 31 2023 at 22:47):
and CPS(AB)=CPS(BA).
Kevin Buzzard (May 31 2023 at 22:48):
This is a poly with constant term 1 whose roots are the multiset of reciprocals of nonzero eigenvalues of the matrix
Kevin Buzzard (May 31 2023 at 22:50):
If P(X) is the char poly of degree d then the char power series is X^d*P(1/X)
Kevin Buzzard (May 31 2023 at 22:52):
So one could even say that the multiset of nonzero eigenvalues was the same for AB and BA, but my claim is a cleaner way of expressing it
MohanadAhmed (May 31 2023 at 22:57):
Let me see if I get this:
 There is something called the characteristic power series given by: $CPS(X) = x^d P(x^{1})$ where $P(x)$ is the characteristic polynomial
 Its roots are $\frac{1}{\lambda_i}$ for $i\in[1,n]$ with $n$ dimension of tha matrix So basically that premultiplication with $x^d$ clears out the zero eigenvalues from the root set.
 You think expressing it in terms of Char Power Series is a better way
MohanadAhmed (May 31 2023 at 22:59):
So here are a few questions?
Is the "Char Power Series" currently in mathlib? Or do we need to define it?
MohanadAhmed (May 31 2023 at 22:59):
In what sense is it cleaner?
Kevin Buzzard (May 31 2023 at 23:04):
Instead of talking about equality of multisets of nonzero eigenvalues, my claim (det(1tAB)=det(1tBA)) is a clean equality of polynomials, from which the equality of multisets easily follows.
Kevin Buzzard (May 31 2023 at 23:06):
Furthermore my claim is true for matrices taking values in an arbitrary commutative ring like Z or Z/8Z so it's more general; over general rings polynomials of degree d can have more than d roots so the concept of eigenvalue is not well behaved, whereas as the concept of a polynomial is
MohanadAhmed (May 31 2023 at 23:09):
OK! I see. Yes, proving $det(I  tAB) = det(I  tBA)$ would be easier.
But still equality of the root sets does not mean they are indexed in the same way. So an equivalence between them is needed right?
MohanadAhmed (May 31 2023 at 23:11):
Sorry I guess you meant CPS (BA) = CPS(BA) which is not the same as $det(I  tAB) = det(I  tBA)$
MohanadAhmed (May 31 2023 at 23:11):
The CPS have the same roots but det(I  tAB) will have the extra zero roots right?
Kevin Buzzard (May 31 2023 at 23:12):
CPS(M):=det(ItM)
MohanadAhmed (May 31 2023 at 23:13):
But don't we need to mulitply by $x^d$ to clear the zeros?
MohanadAhmed (May 31 2023 at 23:13):
And invert the argument?
Kevin Buzzard (May 31 2023 at 23:13):
There is no d in my equation or any multiplication by any x^d
MohanadAhmed (May 31 2023 at 23:13):
Kevin Buzzard said:
If P(X) is the char poly of degree d then the char power series is X^d*P(1/X)
This one?
Kevin Buzzard (May 31 2023 at 23:14):
That's a theorem. I don't really know what you're saying.
Kevin Buzzard (May 31 2023 at 23:15):
I'm saying CPS(AB)=CPS(BA) and that if the base ring is an algebraically closed field like the complexes then the roots of CPS(M) are the reciprocals of the nonzero eigenvalues of M, with multiplicities
MohanadAhmed (May 31 2023 at 23:15):
What I understood was you are naming the characteristic polynomial P(X). Then defining the Characteristic Power Series in terms of it by:
CPS(X) := X^d P(1/X)
Kevin Buzzard (May 31 2023 at 23:16):
That's a more ugly definition, I would rather think of that as a theorem
Kevin Buzzard (May 31 2023 at 23:17):
But that's a concrete link between the CPS and the eigenvalues
Kevin Buzzard (May 31 2023 at 23:18):
CPS(M)=X^dP(1/X) is more accurate
MohanadAhmed (May 31 2023 at 23:20):
MohanadAhmed said:
OK! I see. Yes, proving $det(I  tAB) = det(I  tBA)$ would be easier.
But still equality of the root sets does not mean they are indexed in the same way. So an equivalence between them is needed right?
How about the equivalence between the two sets so that I can use the indices from one set in the other. That would be a useful step in an SVD proof?
Kevin Buzzard (May 31 2023 at 23:26):
What sets are you talking about? Here the correct concept is a multiset
MohanadAhmed (May 31 2023 at 23:40):
It is probably a misunderstanding from my side but in mathlib there are two things that can be seen as the same thing:

There is the multiset of roots of a polynomial. If the polynomial is selected to be the characteristic polynomial then the roots are the eigenvalues.
docs#polynomial.roots
docs#matrix.charpoly 
There is the eigenvalues of a hermitian matrix which map from the index set (say fintype n) to an eigenvalue. docs#matrix.is_hermitian.eigenvalues
The second one is ordered. So if I want to compare the eigenvalues between two matrices, I need to take care of this order by reindexing.
The second one also comes with eigenvectors associated with the eigenvalues. So using these eigenvectors with another matrix requires a mapping of the indices
MohanadAhmed (May 31 2023 at 23:42):
The first one is the multiset of roots (eigenvalues) you are talking about. But it comes alone without associated eigenvectors
Edit (10:55AM) : It seems my terminology is way off here. What I mean by ordered is that the index n docs#matrix.is_hermitian.eigenvalues ties the eigenvalues to the eigenvectors in docs#matrix.is_hermitian.eigenvector_matrix. When using those two theorems the eigenvalue are associated to some index (i : n)
Eric Wieser (May 31 2023 at 23:49):
MohanadAhmed said:
OK! I see. Yes, proving $det(I  tAB) = det(I  tBA)$ would be easier.
Note that this is "the matrix determinant lemma" and there is another recent thread about proving it here.
MohanadAhmed (May 31 2023 at 23:52):
I see where the confusion might be coming from:
The first question for the AB and BA matrices makes sense in general.
The second question for the A^HA and AA^H matrices is a special case of the first. But in the second case we have have a different proof because of this disconnect in mathlib between eigenvalues in general and eigenvalues of hermitian matrices
MohanadAhmed (May 31 2023 at 23:54):
So mathematically 2nd question is a special case of the first.
In mathlib the 2nd is not direct special case which can you just apply.
MohanadAhmed (Jun 01 2023 at 00:04):
MohanadAhmed said:
So using your suggestion for the lemma statement:
import data.complex.basic import linear_algebra.matrix.hermitian import linear_algebra.matrix.pos_def import linear_algebra.matrix.determinant import linear_algebra.matrix.spectrum open matrix open_locale matrix complex_conjugate big_operators def m: ℕ := 10 def n: ℕ := 14 / Nonzero in fm is in fn / lemma zero_or_fm_in_fn (fm : fin m → ℝ)(fn : fin n → ℝ): ∀(i: fin m), fm i = 0 ∨ (∃ (j: fin n), fn j = fm i) := sorry / Flipped Around / lemma zero_or_fn_in_fm (fm : fin m → ℝ)(fn : fin n → ℝ): ∀(j: fin n), fn j = 0 ∨ (∃ (i: fin m), fn j = fm i) := sorry def pm (fm : fin m → ℝ): fin m → Prop := (λ i, (fm i = 0)) def pn (fn : fin n → ℝ): fin n → Prop := (λ j, (fn j = 0)) #check pm / I want to say there is an equivalence relation between elements of fin m giving nonzero values for fm and the elements of fin n giving nonzero values for fn. / lemma non_zero_parts_equiv (fm : fin m → ℝ)(fn : fin n → ℝ): nonempty({i : fin m // pm fm i} ≃ {j : fin n // pn fn j}):= begin end
Any thoughts on how to prove this equivalence? @Eric Wieser
Eric Wieser (Jun 01 2023 at 00:07):
Your sorries are false, so I can use them to prove whatever I like!
Eric Wieser (Jun 01 2023 at 00:07):
(I think those two lemmas need to be assumptions instead, they certainly aren't universally true!)
MohanadAhmed (Jun 01 2023 at 08:30):
MohanadAhmed said:
Sorry I guess you meant CPS (BA) = CPS(BA) which is not the same as $det(I  tAB) = det(I  tBA)$
Some sleep helps!!
Characteristic Polynomial = $det(tI  M)$
Characteristic Power Seires = $det(I  tM)$
@Kevin Buzzard Would the first step in your suggested idea be to show that the roots of nonzero roots of $det(I  tM)$ and the roots of $det(I  tM)$ are related by being the inverses of each other?
Kevin Buzzard (Jun 01 2023 at 08:31):
The first step to proving what?
MohanadAhmed (Jun 01 2023 at 08:34):
The multiset of the nonzero eigenvalues of AB is the same as the multiset of the nonzero eigenvalues of BA?
MohanadAhmed (Jun 01 2023 at 08:38):
If I understood you correctly:
Let $P_M(t) = \text{det}(tI  M)$
Let $\text{CPS}_M(t) = \text{det}(I  tM)$
$CPS_M(t) = t^n P_M(1/t)$
MohanadAhmed (Jun 01 2023 at 08:38):
Where $n$ is the dimension of the matrix $M$
MohanadAhmed (Jun 01 2023 at 08:39):
Then nonzero roots of $CPS_M(t)$ are the same as the reciprocals of the nonzero roots of $P_M(t)$
Kevin Buzzard (Jun 01 2023 at 08:43):
Yes all those statements are true.
Kevin Buzzard (Jun 01 2023 at 08:44):
CPS_M(t) has constant term 1 so 0 is never a root.
MohanadAhmed (Jun 01 2023 at 12:38):
Eric Wieser said:
(I think those two lemmas need to be assumptions instead, they certainly aren't universally true!)
You are right. Does the following look more reasonable. If yes, any suggestions on how to proceed?
I guess an equivalent question is given a set of real numbers I want a permutation that orders them in increasing or decreasing order. There must be something like that already in mathlib, right?
import data.complex.basic
import linear_algebra.matrix.hermitian
import linear_algebra.matrix.pos_def
import linear_algebra.matrix.determinant
import linear_algebra.matrix.spectrum
open matrix
open_locale matrix complex_conjugate big_operators
variables m n : ℕ
/
I want to say there is an equivalence relation between
elements of fin m giving nonzero values for fm and the
elements of fin n giving nonzero values for fn.
/
def pm (fm : fin m → ℝ): fin m → Prop := (λ i, (fm i = 0))
def pn (fn : fin n → ℝ): fin n → Prop := (λ j, (fn j = 0))
lemma non_zero_parts_equiv (fm : fin m → ℝ)(fn : fin n → ℝ)
(h1: ∀(j: fin n), fn j = 0 ∨ (∃ (i: fin m), fn j = fm i))
(h2: ∀(i: fin m), fm i = 0 ∨ (∃ (j: fin n), fn j = fm i)):
nonempty({i : fin m // pm m fm i} ≃ {j : fin n // pn n fn j}):=
begin
end
Eric Wieser (Jun 01 2023 at 12:47):
That looks true, but h1 and h2 look super awkward
Eric Wieser (Jun 01 2023 at 12:49):
I would suggest the condition being (finset.univ.filter (pm fm)).card = (finset.univ.filter (pn fn)).card
Eric Wieser (Jun 01 2023 at 12:49):
Also, your pn
and pm
are alphaequivalent!
Eric Wieser (Jun 01 2023 at 13:08):
Wait, this is still false, consider fm = ![0, 0]
and fn = ![0]
. Both hypotheses are clearly true, but the conclusion would imply 2 = 1
Eric Wieser (Jun 01 2023 at 13:11):
Eric Wieser said:
Your statement is sort of true by definition:
#A = #B
(ie, the size of each type, docs#cardinal.mk, being the same) meansnonempty (A ≃ B)
)
Here's what I meant by that:
import set_theory.cardinal.basic
import data.real.basic
open_locale cardinal
lemma non_zero_parts_equiv {m n : ℕ} (fm : fin m → ℝ) (fn : fin n → ℝ)
 the number of nonzero entries is equal
(h : #{i // fm i ≠ 0} = #{i // fn i ≠ 0}) :
 the indices of nonzero entries are equivalent
nonempty ({i // fm i ≠ 0} ≃ {i // fn i ≠ 0}) :=
cardinal.eq.mp h
MohanadAhmed (Jun 01 2023 at 21:55):
MohanadAhmed said:
If I understood you correctly:
Let $P_M(t) = \text{det}(tI  M)$
Let $\text{CPS}_M(t) = \text{det}(I  tM)$
$CPS_M(t) = t^n P_M(1/t)$
The code below shows my initial attempt. It seems I can show that $\text{det}(I_m  tAB) = \text{det}(I_n  tBA)$. I am however not even able to state the connection between the characteristic polynomial and characteristic power series : $CPS_M(X) = X^n * P_M(1/X)$. How do I tell lean to give me the reciprocal of the polynomial indeterminate polynomial.X
?
import data.matrix.basic
import data.complex.basic
import linear_algebra.matrix.determinant
import linear_algebra.matrix.schur_complement
import data.polynomial.basic
open polynomial matrix function
open_locale big_operators polynomial matrix
variables {m n q R: Type*}
variables [fintype m][fintype n][decidable_eq m][decidable_eq n]
variables [fintype q][decidable_eq q]
variables [field R]
noncomputable def charpow_mat (M : matrix q q R) : (matrix q q R[X]) :=
(1: matrix q q R[X])  (matrix.scalar q (polynomial.X)) ⬝ ((C : R →+* R[X]).map_matrix M)
noncomputable def charpow (M: matrix q q R): polynomial R :=
(charpow_mat M).det
lemma charpow_comm (A: matrix m n R)(B: matrix n m R):
charpow (A⬝B) = charpow (B ⬝ A) :=
begin
unfold charpow, unfold charpow_mat,
simp only [coe_scalar, ring_hom.map_matrix_apply, matrix.map_mul, smul_mul, matrix.one_mul],
rw ← matrix.smul_mul,
rw det_one_sub_mul_comm,
rw matrix.mul_smul,
end
/ Does not type check /
lemma charpow_eq_X_pow_n_mul_charpoly_inv (M : matrix q q R):
charpow M = ((polynomial.X) ^ (fintype.card q)) * (M.charpoly.aeval X) := begin
end
Eric Wieser (Jun 01 2023 at 22:08):
I think for that you might need docs#laurent_polynomial
Eric Wieser (Jun 01 2023 at 22:12):
Eric Wieser said:
Note that this is "the matrix determinant lemma" and there is another recent thread about proving it here.
Whoops, I was obviously wrong; indeed, docs#matrix.det_one_sub_mul_comm (which I wrote!) is the statement.
MohanadAhmed (Jun 01 2023 at 22:24):
Perhaps it is easier to forget that connection and just show that
A is_root charpoly \imp 1/A is_root charpow?
Last updated: Dec 20 2023 at 11:08 UTC