From 50ae8e1141ee46aa24f6d4ed61def8d34b1ebcd6 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 8 Sep 2020 03:46:31 +0200 Subject: stability by commutation --- CHANGELOG_UNRELEASED.md | 11 ++++++--- mathcomp/algebra/mxalgebra.v | 24 +++++++++++++++++++ mathcomp/algebra/mxpoly.v | 56 +++++++++++++++++++++++++++----------------- 3 files changed, 67 insertions(+), 24 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4cd65e8..251beb6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -217,9 +217,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`, `comm_mx_refl`, `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`, `comm_mxN`, `comm_mxN1`, `comm_mxD`, `comm_mxB`, `comm_mx_sum`, `comm_mxP`, `all_comm_mxP`, - `all_comm_mx1`, `all_comm_mx2P`, `all_comm_mx_cons`, `comm_mxC`, - `commCmx`, `comm_mx_horner`, and `horner_mxC`. The common arguments - of these lemmas `R` and `n` are maximal implicits. + `all_comm_mx1`, `all_comm_mx2P`, `all_comm_mx_cons`, `comm_mxC`, and + `commCmx`. The common arguments of these lemmas `R` and `n` are + maximal implicits. - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. - in `fintype.v`, added `mask_enum_ord`. @@ -231,6 +231,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `stable0mx`, `stableCmx`, `stablemx_sums`, and `stablemx_unit`. - in `mxpoly.v`, new lemma `horner_mx_stable`. +- in `mxalgebra.v`, added `comm_mx_stable`, `comm_mx_stable_ker`, and + `comm_mx_stable_eigenspace`. +- in `mxpoly.v`, added `comm_mx_horner`, `comm_horner_mx`, + `comm_horner_mx2`, `horner_mx_stable`, `comm_mx_stable_kermxpoly`, + and `comm_mx_stable_geigenspace`. ### Changed diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index adad2fc..7e213b8 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2272,6 +2272,30 @@ Qed. Lemma stablemx_unit (n : nat) (V f : 'M[F]_n) : V \in unitmx -> stablemx V f. Proof. by move=> Vunit; rewrite submx_full ?row_full_unit. Qed. +Section Commutation. + +Variable (n : nat). +Implicit Types (f g : 'M[F]_n). + +Lemma comm_mx_stable (f g : 'M[F]_n) : comm_mx f g -> stablemx f g. +Proof. by move=> comm_fg; rewrite [_ *m _]comm_fg mulmx_sub. Qed. + +Lemma comm_mx_stable_ker (f g : 'M[F]_n) : + comm_mx f g -> stablemx (kermx f) g. +Proof. +move=> comm_fg; apply/sub_kermxP. +by rewrite -mulmxA -[g *m _]comm_fg mulmxA mulmx_ker mul0mx. +Qed. + +Lemma comm_mx_stable_eigenspace (f g : 'M[F]_n) a : + comm_mx f g -> stablemx (eigenspace f a) g. +Proof. +move=> cfg; rewrite comm_mx_stable_ker//. +by apply/comm_mx_sym/comm_mxB => //; apply:comm_mxC. +Qed. + +End Commutation. + End Stability. Section DirectSums. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 9ffbe77..74d524e 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -268,8 +268,11 @@ Section HornerMx. Variables (R : comRingType) (n' : nat). Local Notation n := n'.+1. +Implicit Types (A B : 'M[R]_n) (p q : {poly R}). + +Section OneMatrix. + Variable A : 'M[R]_n. -Implicit Types p q : {poly R}. Definition horner_mx := horner_morph (comm_mxC^~ A). Canonical horner_mx_additive := [additive of horner_mx]. @@ -299,10 +302,9 @@ apply: eq_bigr => i _. by rewrite valK !linearZ rmorphX /= horner_mx_X rowK /= mxvecK. Qed. -End HornerMx. +End OneMatrix. -Lemma horner_mx_diag (R : comRingType) (n' : nat) - (d : 'rV[R]_n'.+1) (p : {poly R}) : +Lemma horner_mx_diag (d : 'rV[R]_n) (p : {poly R}) : horner_mx (diag_mx d) p = diag_mx (map_mx (horner p) d). Proof. apply/matrixP => i j; rewrite !mxE. @@ -313,6 +315,19 @@ rewrite (bigD1 j)//= ihp mxE ?eqxx mulr1n -mulrnAl big1 ?addr0//. by move=> k /negPf nkF; rewrite mxE nkF mulr0. Qed. +Lemma comm_mx_horner A B p : comm_mx A B -> comm_mx A (horner_mx B p). +Proof. +by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx. +Qed. + +Lemma comm_horner_mx A B p : comm_mx A B -> comm_mx (horner_mx A p) B. +Proof. by move=> ?; apply/comm_mx_sym/comm_mx_horner/comm_mx_sym. Qed. + +Lemma comm_horner_mx2 A p q : GRing.comm (horner_mx A p) (horner_mx A q). +Proof. exact/comm_mx_horner/comm_horner_mx. Qed. + +End HornerMx. + Lemma horner_mx_stable (K : fieldType) m n p (V : 'M[K]_(n.+1, m.+1)) (f : 'M_m.+1) : stablemx V f -> stablemx V (horner_mx f p). @@ -827,6 +842,14 @@ Lemma kermxpoly_min n (g : 'M_n.+1) p : mxminpoly g %| p -> (kermxpoly g p :=: 1)%MS. Proof. by rewrite /kermxpoly => /mxminpoly_minP ->; apply: kermx0. Qed. +Lemma comm_mx_stable_kermxpoly n (f g : 'M_n) (p : {poly K}) : comm_mx f g -> + stablemx (kermxpoly f p) g. +Proof. +case: n => [|n] in f g *; first by rewrite !thinmx0. +move=> fg; rewrite /kermxpoly; apply: comm_mx_stable_ker. +by apply/comm_mx_sym/comm_mx_horner/comm_mx_sym. +Qed. + Lemma mxdirect_kermxpoly n (g : 'M_n) (p q : {poly K}) : coprimep p q -> (kermxpoly g p :&: kermxpoly g q = 0)%MS. Proof. @@ -925,10 +948,13 @@ Lemma eigenpolyP n (g : 'M_n) (p : {poly K}) : reflect (exists2 v : 'rV_n, (v <= kermxpoly g p)%MS & v != 0) (eigenpoly g p). Proof. exact: rowV0Pn. Qed. -Lemma eigenvalue_poly n a (f : 'M_n) : - eigenvalue f a = eigenpoly f ('X - a%:P). +Lemma eigenvalue_poly n a (f : 'M_n) : eigenvalue f a = eigenpoly f ('X - a%:P). Proof. by rewrite /eigenpoly /eigenvalue eigenspace_poly. Qed. +Lemma comm_mx_stable_geigenspace n (f g : 'M_n) a : comm_mx f g -> + stablemx (geigenspace f a) g. +Proof. exact: comm_mx_stable_kermxpoly. Qed. + End KernelLemmas. Section MapKermxPoly. @@ -936,7 +962,9 @@ Variables (aF rF : fieldType) (f : {rmorphism aF -> rF}). Lemma map_kermxpoly (n : nat) (g : 'M_n) (p : {poly aF}) : map_mx f (kermxpoly g p) = kermxpoly (map_mx f g) (map_poly f p). -Proof. by case: n => [|n] in g *; rewrite ?thinmx0// map_kermx map_horner_mx. Qed. +Proof. +by case: n => [|n] in g *; rewrite ?thinmx0// map_kermx map_horner_mx. +Qed. Lemma map_geigenspace (n : nat) (g : 'M_n) (a : aF) : map_mx f (geigenspace g a) = geigenspace (map_mx f g) (f a). @@ -948,20 +976,6 @@ Proof. by rewrite /eigenpoly -map_kermxpoly map_mx_eq0. Qed. End MapKermxPoly. -Section CommmxPoly. - -Lemma comm_mx_horner (R : comRingType) (n' : nat) (A B : 'M[R]_n'.+1) - (p : {poly R}) : comm_mx A B -> comm_mx A (horner_mx B p). -Proof. -by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx. -Qed. - -Lemma horner_mxC (R : comRingType) (n' : nat) (A : 'M_n'.+1) (p q : {poly R}) : - GRing.comm (horner_mx A p) (horner_mx A p). -Proof. exact/comm_mx_horner/comm_mx_sym/comm_mx_horner. Qed. - -End CommmxPoly. - Section IntegralOverRing. Definition integralOver (R K : ringType) (RtoK : R -> K) (z : K) := -- cgit v1.2.3