So I have been working with the canonical forms library and the mathcomp library. I need the definition of eigenvalue defined in the canonical forms library (as the diagonal entry of the Jordan matrix):

```
Definition Jordan_form m (A : 'M[R]_m.+1) :=
let sp := root_seq_poly (invariant_factors A) in
let sizes := [seq (x.2).-1 | x <- sp] in
let blocks n i := Jordan_block (nth (0,0%N) sp i).1 n.+1 in
diag_block_mx sizes blocks.
```

In mathcomp, eigenvalue is defined as :

```
Definition eigenvalue : pred F := fun a ⇒ eigenspace a != 0.
```

And there is a lemma in mathcomp relating the above definition of eigenvalue to the roots of the characteristic polynomial:

```
Lemma eigenvalue_root_char (F : fieldType) n (A : 'M[F]_n) a :
eigenvalue A a = root (char_poly A) a.
```

My question is: Does there already exist a lemma somewhere relating the mathcomp definition of eigenvalue and the one defined using the Jordan matrix ?

I have a proof relating them for a complex matrix as follows:

```
Definition lambda_seq (n: nat) (A: 'M[complex R]_n.+1):=
let sizes:= size_sum
[seq x.2.-1
| x <- root_seq_poly (invariant_factors A)] in
[seq (Jordan_form A) i i | i <- enum 'I_(sizes).+1].
Lemma Jordan_ii_is_eigen_aux:
forall (n: nat) (A: 'M[complex R]_n.+1),
let sizes:= size_sum
[seq x.2.-1
| x <- root_seq_poly (invariant_factors A)] in
forall (i: 'I_sizes.+1),
@eigenvalue (complex_fieldType _) n.+1 A (@nth _ 0%C (lambda_seq A) i).
Proof.
intros.
rewrite eigenvalue_root_char.
rewrite -root_root_seq.
+ assert (perm_eq [seq (Jordan_form A) i i | i <- enum 'I_(sizes).+1]
(root_seq (char_poly A))).
{ apply eigen_diag. }
apply perm_mem in H. unfold eq_mem in H.
specialize (H (@nth _ 0%C (lambda_seq A) i)).
rewrite -H. rewrite /lambda_seq. apply mem_nth.
by rewrite size_map size_enum_ord.
+ apply monic_neq0. apply char_poly_monic.
Qed.
```

Does this look okay? Is there an easy way to use both the definitions of eigenvalues together?

Thanks !!

I think it is a mistake of the Jordan form development that `A`

and `Jordan_form A`

do not have the same dimension. Following your question, I am working on modifying the interface of file `jordan.v`

in `coqeal`

so that the type of `Jordan_form A`

is :

```
forall (F : closedFieldType)(n : nat), 'M[F]_n -> 'M[F]_n
```

There are only 4 theorems mentioning `Jordan_form`

in the development so far: `Jordan`

, `upt_Jordan`

, `eigen_diag`

, they should be reformulated for the nicer type of `Jordan_form`

. For now, I only dealt with the first 3:

```
Definition Jordan_form' (F : closedFieldType) (n : nat)
(A : 'M[F]_n) : 'M[F]_n.
case: n A.
exact id.
move=> n A; apply: (castmx _ (Jordan_form A)).
by split; apply/esym/(proj1 (Jordan A)).
Defined.
Lemma Jordan' (F : closedFieldType)(n : nat)(A : 'M[F]_n) :
(0 < n)%N -> similar A (Jordan_form' A).
Proof.
case: n A => [ | n] // A; split; first by [].
apply (similar_trans (Jordan A)); apply/similar_cast/similar_refl.
Qed.
Lemma upt_Jordan' (F : closedFieldType) (n : nat) (A : 'M[F]_n) :
upper_triangular_mx (Jordan_form' A).
Proof.
case: n A => [ | n] A; first by apply/eqP/matrixP=> -[].
apply/eqP/matrixP=> i j; rewrite /Jordan_form' castmxE /upper_part_mx.
rewrite mxE castmxE.
have := upt_Jordan A=> /eqP/matrixP uj.
by rewrite [LHS]uj /upper_part_mx mxE.
Qed.
Lemma eigen_diag' (R : closedFieldType) (n : nat) (A : 'M[R]_n) :
(0 < n)%N ->
perm_eq [seq Jordan_form' A i i | i : 'I_n] (root_seq (char_poly A)).
Proof.
case: n A => [ | n ] A; first by [].
move=> _.
apply: perm_trans (eigen_diag A).
set x := (X in perm_eq X _).
set y := (X in perm_eq _ X).
suff : x = y by move=> ->; rewrite perm_refl.
rewrite {}/x {}/y /Jordan_form'.
apply: (@eq_from_nth _ 0).
by rewrite !size_map -!enumT !size_enum_ord; case: (Jordan A).
move=> i; rewrite size_map size_enum_ord => ilt.
rewrite (nth_map 0); last by rewrite size_enum_ord.
rewrite castmxE.
rewrite -[i in LHS]/(nat_of_ord (Ordinal ilt)) nth_ord_enum.
rewrite (nth_map 0); last by rewrite size_enum_ord -(proj1 (Jordan A)).
have ilt' : (i < (size_sum
[seq x.2.-1 | x <- root_seq_poly (invariant_factors A)]).+1)%N.
by rewrite -(proj1 (Jordan A)).
rewrite -[i in RHS]/(nat_of_ord (Ordinal ilt')).
rewrite nth_ord_enum /=.
suff -> : cast_ord (esym (esym (proj1 (Jordan A)))) (Ordinal ilt) =
Ordinal ilt' by [].
by apply/val_inj.
Qed.
```

Thanks @Yves Bertot !! I will follow your development closely.

In this new context, here is my description of the sequence of eigenvalues, as extracted from the Jordan form.

```
Definition eigenvalue_seq (R : closedFieldType) (n : nat):
'M[R]_n -> seq R :=
match n return 'M[R]_n -> seq R with
| 0 => fun _ => [::]
| S n => fun A => [seq Jordan_form' A i i | i : 'I_n.+1]
end.
```

Now, for the theorem you named `Jordan_ii_is_eigen_aux`

, I find the following formulation more pleasing to the eye. I hope it will also be more pleasant to use.

```
Definition eigenvalue_Jordan (R : closedFieldType) (n : nat) (A : 'M[R]_n) :
(0 < n)%N ->
{in [seq Jordan_form' A i i | i : 'I_n], forall x, eigenvalue A x}.
Proof.
case: n A => [ | n]; first by [].
move=> A _ x; rewrite eigenvalue_root_char -root_root_seq; last first.
by apply/monic_neq0/char_poly_monic.
by rewrite (perm_mem (eigen_diag' A isT)).
Qed.
```

Thanks @Yves Bertot the description of the sequence of eigenvalues looks good and I will try to use these definitions and lemmas. One question: How should I use your developments in my proof? Would you be pushing them somewhere?

I still have to complete the proof of lemma `Jordan_char_poly'`

.

For now you can copy-paste this to your code as a temporary measure. I will make a pull-request to coqeal as soon as I am finished. At review time it will probably be modified slightly, but there should be no loss in functionality.

Cool, thanks !! This sounds good :)

Okay, I finished a rephrasing the Jordan form function in a branch of coqeal. The result is visible here: https://github.com/ybertot/coqeal/blob/b18ee537d6472d5233c4c44fc45eef3f65daf5fe/theory/jordan.v#L233

However, I am not completely convinced this is the right solution, because more packaging is required to explain that the final matrix is composed of Jordan blocks, a property that is more obvious with the previous presentation.

ping @Mohit Tekriwal

Thanks a lot @Yves Bertot . I will take a look at your results. Thanks for your help :)

I gave it a few more thoughts, maybe we should avoid redesigning the function `Jordan_form`

, but to make it practical to describe the relation between eigenvalues and elements of the diagonal, you have to avoid writing lemmas where you have to mention explicitely the size of `Jordan_form A`

. The attempts I made about changing the type of this function made it possible to learn a few things about the development of Jordan forms. In particular, you should remember that the theorem `Jordan`

is actually a conjunction, where the first component is a proof that the size of `Jordan_form A`

is provably equal to the size of A. Once you know this, you can use natural number as indices, as long as you are able to provide a proof that these natural numbers are smaller than `n.+1`

. Here is another way to describe the property that you requested, compatible with the original design of `Jordan_form`

, as visible on the master branch of coq-community/coqeal:

```
Lemma Jordan_form_diag_eigenvalues (F : closedFieldType) (n : nat)
(A : 'M[F]_n.+1) :
perm_eq [seq Jordan_form A (inord i) (inord i) | i <- iota 0 n.+1]
(root_seq (char_poly A)).
Proof.
have := eigen_diag A; lazy zeta.
set w := size_sum _.
have -> : [seq Jordan_form A i i | i <- enum 'I_w.+1] =
[seq Jordan_form A (inord k) (inord k) |
k <- [seq val i | i <- enum 'I_w.+1]].
rewrite -[RHS]map_comp.
have ext : {in enum 'I_w.+1, forall i, Jordan_form A i i =
Jordan_form A (inord (val i)) (inord (val i))}.
by move=> i iin; rewrite inord_val.
by rewrite eq_in_map in ext; rewrite ext.
rewrite val_enum_ord=> tmp.
by rewrite [X in iota 0 X] (proj1 (Jordan A)).
Qed.
```

You can see that the elements of the matrix `Jordan_form A`

are accessed from natural numbers taken from the list `(iota 0 n.+1)`

. These natural numbers are transformed into numbers of the correct finite type thanks to the function `inord`

. This function maps a natural number `i `

to the same number as an element of an `'I_k.+1`

as long as we have a proof that `(n < k.+1`

. The nice feature here is that we never need to write `k`

. Here we take the elements to be smaller than `n.+1`

and we use the first part of `Jordan A`

to show that this the right number (the size of both `A`

and `Jordan_form A`

).

The final statement of the theorem is stronger that what you describe, because we not only show that all elements of the diagonal are eigenvalues, but that also that all eigenvalues are on the diagonal, respecting multiplicity!

Thanks @Yves Bertot for the pointers !! This makes a lot of sense. Your insight on the theorem `Jordan`

is really helpful. I was looking for a proof that the size of the `Jordan_form A`

is equal to the size of `A`

.

@Yves Bertot I have been trying to prove the following lemma:

```
Lemma total_eigen_val: forall (n:nat) (A: 'M[complex R]_n.+1),
(size_sum
[seq x.2.-1 | x <- root_seq_poly (invariant_factors A)]).+1 = n.+1.
```

I was looking at the proof of `Jordan`

but they do not prove this directly. My developments rely on this lemma. Assuming this, I was able to work around the dimension issues. I need this because in order to use the Jordan decomposition lemmas, I have to consider the `size_sum ....`

fact. Informally, this makes sense to me, since the LHS defines the number of eigenvalues and they have to equal to the size of the original matrix.

The direction I took is as follows:

```
Lemma total_eigen_val: forall (n:nat) (A: 'M[complex R]_n.+1),
(size_sum
[seq x.2.-1 | x <- root_seq_poly (invariant_factors A)]).+1 = n.+1.
Proof.
intros.
rewrite map_comp.
assert ((size_sum [seq (size p).-2 | p : {poly complex_fieldType R_realFieldType} <- (invariant_factors A)]).+1 =
(size_sum
[seq i.-1
| i <- [seq i.2
| i <- root_seq_poly
(invariant_factors A)]]).+1).
{ admit. }
rewrite -H.
rewrite -cast_inv.
by rewrite size_Frobenius_seq.
Admitted.
```

I fear to repeat myself, but the theorem `Jordan`

contains the fact your need. As illustrated by the following proof:

```
Variable R : closedFieldType.
Lemma total_eigen_val: forall (n:nat) (A: 'M[R]_n.+1),
(size_sum
[seq x.2.-1 | x <- root_seq_poly (invariant_factors A)]).+1 = n.+1.
Proof.
by move=> n A; rewrite -(proj1 (Jordan A)).
Qed.
```

The difference between your statement and mine is that in my statement the matrix has coefficients in type `closedFieldType`

, while in your statement the patrix coefficient are in `complex R`

. For lack of time, I have not yet been ablt to type in your statement, because in my context, `R[i]`

(a.k.a. complex R) is not recognized a a fieldType. I don't know what is missing.

Ah okay. Thanks @Yves Bertot !! This really helps. Sorry for my misunderstanding. I see now what you meant. I was able to apply this for `complex R`

. I guess, you might need to import the complex theory from `realclosed`

. I was able to close my proofs. I will be writing in the next few days. Can I share my draft and my proof script with you for review when I have a decent draft?

I figured it out, to be able to use `complex R`

as a closed field, I need `R`

to be a real closed field. With

```
Variable R : rcfType.
```

the example above works fine.

Note that you cannot rewrite in the other direction, because `n`

occurs in too many places where it is *locked* by the type of another object depending on it.

Thanks @Yves Bertot :)

Last updated: Jan 29 2023 at 19:02 UTC