Equivalence between subtypes given a certain property

Stream: new members

[MohanadAhmed]

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:

1. How do I express equivalence between two subtypes?
   In this case the subtypes of fin m and fin n that give nonzero values in fm and fn respectively?

2. Given the two lemmas zero_or_fn_in_fm and zero_or_fm_in_fn how do I go about proving non_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]

It doesn't typecheck because the syntax is ∃ x : X, p x, not ∃ x : X

[Eric Wieser]

You can fix that with ∃ x : X, true, but that's just a silly way of writing nonempty X

[Eric Wieser]

Are you sure you're not looking for X by itself though? Here, that would be an algorithm for constructing the equiv

[Eric Wieser]

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]

If you did want to prove this I think you could use docs#fin_enum to enumerate the elements in order...

[Eric Wieser]

... but this sounds like an #xy problem to me

[MohanadAhmed]

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]

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]

What do mean by " Here, that would be an algorithm for constructing the equiv"?

[Kevin Buzzard]

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]

Wait, this isn't even true is it? Let A=(0 1;0 0) and B=(1 0;0 0)

[Kevin Buzzard]

Or A=(1,1), B=(1;-1)

[MohanadAhmed]

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 non-zero is an eigenvalue of $BA$?

[MohanadAhmed]

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]

AB = 0
BA = [1 1; -1 -1]

[MohanadAhmed]

AB is the zero matrix of size 1 x 1

[MohanadAhmed]

Nothing much to say here

[MohanadAhmed]

BA is the matrix [1 1; -1 -1] ==> Charactersitic polynomial is the x^2 polynomial.
The only roots are zero and zero

[MohanadAhmed]

But these are already discounted in the statement. i.e. we are only concerned with nonzero eigenvalues

[Kevin Buzzard]

No, the claim that the ranks are equal

[Kevin Buzzard]

Or maybe you're using a nonstandard definition of the rank of a matrix?

[MohanadAhmed]

For square matrices in my head rank is the number of nonzero eigenvalues

[Kevin Buzzard]

Well in the textbooks rank is something else :-/

[MohanadAhmed]

But that is not the correct definition

[MohanadAhmed]

You are right. rank(AB) \neq rank(BA)

[MohanadAhmed]

But No of NonZeroEigs(AB) = NonZeroEigs(BA)?

[Kevin Buzzard]

But I agree that the char power series are the same -- yes

[Kevin Buzzard]

The char power series of a square matrix M is det(1-tM), probably there is a better name for it

[Kevin Buzzard]

and CPS(AB)=CPS(BA).

[Kevin Buzzard]

This is a poly with constant term 1 whose roots are the multiset of reciprocals of nonzero eigenvalues of the matrix

[Kevin Buzzard]

If P(X) is the char poly of degree d then the char power series is X^d*P(1/X)

[Kevin Buzzard]

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]

Let me see if I get this:

1. There is something called the characteristic power series given by: $CPS(X) = x^d P(x^{-1})$ where $P(x)$ is the characteristic polynomial
2. 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.
3. You think expressing it in terms of Char Power Series is a better way

[MohanadAhmed]

So here are a few questions?
Is the "Char Power Series" currently in mathlib? Or do we need to define it?

[MohanadAhmed]

In what sense is it cleaner?

[Kevin Buzzard]

Instead of talking about equality of multisets of nonzero eigenvalues, my claim (det(1-tAB)=det(1-tBA)) is a clean equality of polynomials, from which the equality of multisets easily follows.

[Kevin Buzzard]

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]

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]

Sorry I guess you meant CPS (BA) = CPS(BA) which is not the same as $det(I - tAB) = det(I - tBA)$

[MohanadAhmed]

The CPS have the same roots but det(I - tAB) will have the extra zero roots right?

[Kevin Buzzard]

CPS(M):=det(I-tM)

[MohanadAhmed]

But don't we need to mulitply by $x^d$ to clear the zeros?

[MohanadAhmed]

And invert the argument?

[Kevin Buzzard]

There is no d in my equation or any multiplication by any x^d

[MohanadAhmed]

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]

That's a theorem. I don't really know what you're saying.

[Kevin Buzzard]

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]

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]

That's a more ugly definition, I would rather think of that as a theorem

[Kevin Buzzard]

But that's a concrete link between the CPS and the eigenvalues

[Kevin Buzzard]

CPS(M)=X^dP(1/X) is more accurate

[MohanadAhmed]

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]

What sets are you talking about? Here the correct concept is a multiset

[MohanadAhmed]

It is probably a misunderstanding from my side but in mathlib there are two things that can be seen as the same thing:

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

2. 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]

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]

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]

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]

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]

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]

Your sorries are false, so I can use them to prove whatever I like!

[Eric Wieser]

(I think those two lemmas need to be assumptions instead, they certainly aren't universally true!)

[MohanadAhmed]

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 non-zero roots of $det(I - tM)$ and the roots of $det(I - tM)$ are related by being the inverses of each other?

[Kevin Buzzard]

The first step to proving what?

[MohanadAhmed]

The multiset of the nonzero eigenvalues of AB is the same as the multiset of the nonzero eigenvalues of BA?

[MohanadAhmed]

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]

Where $n$ is the dimension of the matrix $M$

[MohanadAhmed]

Then non-zero roots of $CPS_M(t)$ are the same as the reciprocals of the non-zero roots of $P_M(t)$

[Kevin Buzzard]

Yes all those statements are true.

[Kevin Buzzard]

CPS_M(t) has constant term 1 so 0 is never a root.

[MohanadAhmed]

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]

That looks true, but h1 and h2 look super awkward

[Eric Wieser]

I would suggest the condition being (finset.univ.filter (pm fm)).card = (finset.univ.filter (pn fn)).card

[Eric Wieser]

Also, your pn and pm are alpha-equivalent!

[Eric Wieser]

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]

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) means nonempty (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 non-zero entries is equal
  (h : #{i // fm i ≠ 0} = #{i // fn i ≠ 0}) :
  -- the indices of non-zero entries are equivalent
  nonempty ({i // fm i ≠ 0} ≃ {i // fn i ≠ 0}) :=
cardinal.eq.mp h

[MohanadAhmed]

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]

I think for that you might need docs#laurent_polynomial

[Eric Wieser]

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]

Perhaps it is easier to forget that connection and just show that
A is_root charpoly \imp 1/A is_root charpow?