Library jordan
Require Import ssreflect ssrfun ssrbool eqtype ssrnat ssralg matrix div zmodp.
Require Import seq path fintype poly mxpoly mxalgebra bigop binomial polydiv.
Require Import finfun mxstructure similar companion frobenius_form.
Require Import ssrcomplements dvdring polydvd smith_complements closed_poly.
Require Import seq path fintype poly mxpoly mxalgebra bigop binomial polydiv.
Require Import finfun mxstructure similar companion frobenius_form.
Require Import ssrcomplements dvdring polydvd smith_complements closed_poly.
The main result of this file is the theorem of Jordan decomposition.
A direct consequence of this theorem is the diagonalization theorem.
Jordan_block lam n == The Jordan block of dimension n with
the value lam on the diagonal.
Jordan_form M == The block diagonal matrix formed by the
Jordan blocks of roots of invariant
factors of M, and of dimension their
multiplicity.
Set Implicit Arguments.
Section def.
Variable R : ringType.
Import GRing.Theory.
Local Open Scope ring_scope.
Definition Jordan_block lam n : 'M[R]_n :=
\matrix_(i,j) (lam *+ (i == j :> nat) + (i.+1 == j)%:R).
Lemma Jordan_block0 : Jordan_block 0 1 = 0.
Lemma upt_Jordan_block lam n : upper_triangular_mx (Jordan_block lam n).
End def.
Section trigonal.
Variable R : comRingType.
Import GRing.Theory.
Local Open Scope ring_scope.
Lemma det_Jordan_block (lam : R) n : \det (Jordan_block lam n) = lam ^+ n.
Lemma Jordan_expn (lam : R) n k :
(Jordan_block lam n.+1)^+ k =
\matrix_(i,j) (('C(k,j - i)%:R * (lam^+ (k - (j - i)))) *+ (i <= j)).
Lemma char_poly_Jordan_block (lam : R) n :
char_poly (Jordan_block lam n) = ('X - lam%:P) ^+n.
End trigonal.
Section similar.
Variable R : fieldType.
Import GRing.Theory.
Import PolyPriField.
Local Open Scope ring_scope.
Lemma similar_cj n (lam : R) :
similar (companion_mx (('X - lam%:P)^+ n.+1)) (Jordan_block lam n.+1).
End similar.
Section jordan.
Variable R : closedFieldType.
Import GRing.Theory.
Import PolyPriField.
Local Open Scope ring_scope.
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.
Lemma upt_Jordan n (A : 'M[R]_n.+1) :
upper_triangular_mx (Jordan_form A).
Lemma Jordan n (A : 'M[R]_n.+1) : similar A (Jordan_form A).
Lemma Jordan_char_poly n (A : 'M_n.+1) :
char_poly A = \prod_i ('X - ((Jordan_form A) i i)%:P).
Lemma 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]
(root_seq (char_poly A)).
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))).
Lemma ex_diagonalization n (A : 'M[R]_n.+1) : uniq (root_seq (mxminpoly A)) ->
{s | similar A (diag_mx_seq n.+1 n.+1 s)}.
End jordan.
This page has been generated by coqdoc