diff --git a/theory/jordan.v b/theory/jordan.v index b23b69b..f4ea6d4 100644 --- a/theory/jordan.v +++ b/theory/jordan.v @@ -188,24 +188,26 @@ Import PolyPriField. Local Open Scope ring_scope. -Definition Jordan_form m (A : 'M[R]_m.+1) := +(* This contains the main algorithmic description of the computation of + Jordan normal forms, but the dimension is too complex for practical use. *) +Definition pre_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. -Lemma upt_Jordan n (A : 'M[R]_n.+1) : - upper_triangular_mx (Jordan_form A). +Lemma upt_pre_Jordan n (A : 'M[R]_n.+1) : + upper_triangular_mx (pre_Jordan_form A). Proof. apply: upper_triangular_diag_block=> j. exact: upt_Jordan_block. Qed. -Lemma Jordan n (A : 'M[R]_n.+1) : similar A (Jordan_form A). +Lemma pre_Jordan n (A : 'M[R]_n.+1) : similar A (pre_Jordan_form A). Proof. apply:(similar_trans (Frobenius _)). apply:(similar_trans (similar_Frobenius _)). -rewrite /Frobenius_form_CF /Jordan_form /root_seq_poly /linear_factor_seq. +rewrite /Frobenius_form_CF /pre_Jordan_form /root_seq_poly /linear_factor_seq. set s1 := flatten _. set s2 := map _ _. have Hs: size s1 = size s2. @@ -225,17 +227,64 @@ apply: (@invariant_factor_neq0 _ _ A). by rewrite mem_nth. Qed. -Lemma Jordan_char_poly n (A : 'M_n.+1) : - char_poly A = \prod_i ('X - ((Jordan_form A) i i)%:P). +(* The concept of similarity contains the information that the size + is unchanged. We can now define a more practical function for + the Jordan form. *) +Definition Jordan_form m : 'M[R]_m -> 'M[R]_m := + if m is n.+1 return 'M_m -> 'M_m then + fun A => castmx (esym (proj1 (pre_Jordan A)), esym (proj1 (pre_Jordan A))) + (pre_Jordan_form A) + else + id. + +Lemma upt_Jordan (n : nat) (A : 'M[R]_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_pre_Jordan A=> /eqP/matrixP uj. +by rewrite [LHS]uj /upper_part_mx mxE. +Qed. + +Lemma Jordan (n : nat)(A : 'M[R]_n) : + (0 < n)%N -> similar A (Jordan_form A). Proof. -rewrite (similar_char_poly (Jordan A)). -exact: (char_poly_triangular_mx (upt_Jordan A)). +case: n A => [ | n] // A; split; first by []. +apply (similar_trans (pre_Jordan A)); apply/similar_cast/similar_refl. Qed. -Lemma eigen_diag n (A : 'M_n.+1) : +Lemma pre_Jordan_char_poly n (A : 'M_n.+1) : + char_poly A = \prod_i ('X - ((pre_Jordan_form A) i i)%:P). +Proof. +rewrite (similar_char_poly (pre_Jordan A)). +exact: (char_poly_triangular_mx (upt_pre_Jordan A)). +Qed. + +Lemma Jordan_char_poly (n : nat) (A : 'M[R]_n) : + (0 < n)%N -> + char_poly A = \prod_i ('X - (Jordan_form A i i)%:P). +Proof. +case: n A => [ | n]; first by []. +move=> A _; rewrite pre_Jordan_char_poly. +have tonat m (f : 'I_m.+1 -> {poly R}) : \prod_i (f i) = + \prod_(0 <= i < m.+1 | (i < m.+1)%N) (f (inord i)). + have pred_eq : forall i, ((i < m.+1)%N = (0 <= i < m.+1) && true)%N. + by move=> i; rewrite andbT. + rewrite (eq_bigl _ _ pred_eq) -big_nat_cond big_mkord. + by apply: eq_bigr=> i; rewrite inord_val. +set w := size_sum _; rewrite [LHS]tonat [RHS]tonat. +have weq : w = n by have [+ _] := pre_Jordan A; rewrite -/w => - [] ->. +rewrite {1 2}weq; apply: eq_bigr => i ilt; rewrite /Jordan_form castmxE. +set prf := esym _. +suff -> : cast_ord prf (inord i) = (inord i : 'I_w.+1); first by []. +by apply/val_inj=> /=; rewrite !inordK // -/w weq. +Qed. + +Lemma pre_Jordan_eigen_diag n (A : 'M_n.+1) : let sp := root_seq_poly (invariant_factors A) in let sizes := [seq (x.2).-1 | x <- sp] in - perm_eq [seq (Jordan_form A) i i | i <- enum 'I_(size_sum sizes).+1] + perm_eq [seq (pre_Jordan_form A) i i | i <- enum 'I_(size_sum sizes).+1] (root_seq (char_poly A)). Proof. have Hinj: injective (fun (c : R) => 'X - c%:P). @@ -254,18 +303,47 @@ apply: (@unicity_decomposition _ _ _ (char_poly A)). -move=> r /(nthP 0) []i; rewrite !size_map=> Hi. rewrite (nth_map 0) ?size_map // => <-. exact: monicXsubC. - +by rewrite !big_map; exact: Jordan_char_poly. + +by rewrite !big_map; exact: pre_Jordan_char_poly. -rewrite big_map {1}[char_poly A]root_seq_eq . by rewrite (monicP (char_poly_monic A)) scale1r. Qed. +Lemma eigen_diag (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 (pre_Jordan_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: (pre_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 (pre_Jordan A)). +have ilt' : (i < (size_sum + [seq x.2.-1 | x <- root_seq_poly (invariant_factors A)]).+1)%N. + by rewrite -(proj1 (pre_Jordan A)). +rewrite -[i in RHS]/(nat_of_ord (Ordinal ilt')). +rewrite nth_ord_enum /=. +suff -> : cast_ord (esym (esym (proj1 (pre_Jordan A)))) (Ordinal ilt) = + Ordinal ilt' by []. +by apply/val_inj. +Qed. + Lemma diagonalization n (A : 'M[R]_n.+1) : uniq (root_seq (mxminpoly A)) -> similar A (diag_mx_seq n.+1 n.+1 (root_seq (char_poly A))). Proof. move=> H. -have [Heq _]:= (Jordan A). +have [Heq _]:= (pre_Jordan A). pose s := [seq (x.2).-1 | x <- root_seq_poly (invariant_factors A)]. -have Hs: size ([seq (Jordan_form A) i i | i <- enum 'I_(size_sum s).+1]) = n.+1. +have Hs: size ([seq (pre_Jordan_form A) i i | + i <- enum 'I_(size_sum s).+1]) = n.+1. by rewrite size_map size_enum_ord. have Hn i: nth 0%N s i = 0%N. case: (ltnP i (size (root_seq_poly (invariant_factors A))))=> Hi. @@ -286,9 +364,10 @@ have Hn i: nth 0%N s i = 0%N. -by rewrite inE prednK. by rewrite -ltnS prednK. by rewrite nth_default // size_map. -apply: (similar_trans (Jordan A)). -apply: (similar_trans _ (similar_diag_mx_seq (erefl n.+1) Hs (eigen_diag A))). -rewrite /Jordan_form diag_block_mx_seq //. +apply: (similar_trans (pre_Jordan A)). +apply: (similar_trans _ + (similar_diag_mx_seq (erefl n.+1) Hs (pre_Jordan_eigen_diag A))). +rewrite /pre_Jordan_form diag_block_mx_seq //. rewrite size_map size_enum_ord in Hs. rewrite Hs. set s1 := mkseq _ _. @@ -323,3 +402,13 @@ exact: diagonalization. Qed. End jordan. + +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.