Stream: math-comp users

Topic: Relating eigenvalue definition from mathcomp and Jordan form


view this post on Zulip Mohit Tekriwal (May 04 2022 at 13:13):

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

view this post on Zulip Yves Bertot (May 04 2022 at 14:30):

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.

view this post on Zulip Mohit Tekriwal (May 04 2022 at 14:36):

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

view this post on Zulip Yves Bertot (May 04 2022 at 14:51):

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.

view this post on Zulip Yves Bertot (May 04 2022 at 15:06):

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.

view this post on Zulip Mohit Tekriwal (May 04 2022 at 15:07):

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?

view this post on Zulip Yves Bertot (May 04 2022 at 15:07):

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

view this post on Zulip Yves Bertot (May 04 2022 at 15:08):

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.

view this post on Zulip Mohit Tekriwal (May 04 2022 at 15:09):

Cool, thanks !! This sounds good :)

view this post on Zulip Yves Bertot (May 05 2022 at 05:59):

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.

view this post on Zulip Yves Bertot (May 05 2022 at 05:59):

ping @Mohit Tekriwal

view this post on Zulip Mohit Tekriwal (May 05 2022 at 12:30):

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

view this post on Zulip Yves Bertot (May 07 2022 at 09:57):

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!

view this post on Zulip Mohit Tekriwal (May 08 2022 at 13:46):

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.

view this post on Zulip Mohit Tekriwal (May 08 2022 at 23:30):

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

view this post on Zulip Mohit Tekriwal (May 08 2022 at 23:33):

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.

view this post on Zulip Yves Bertot (May 09 2022 at 05:53):

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.

view this post on Zulip Mohit Tekriwal (May 09 2022 at 12:50):

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?

view this post on Zulip Yves Bertot (May 09 2022 at 12:53):

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.

view this post on Zulip Mohit Tekriwal (May 09 2022 at 12:55):

Thanks @Yves Bertot :)


Last updated: Jan 29 2023 at 19:02 UTC