diff options
| author | Cyril Cohen | 2016-08-25 01:38:44 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2016-08-25 01:39:43 +0200 |
| commit | 2d824f394e8c3148e95b3374fb9903f6032ba3e6 (patch) | |
| tree | 6640dead8c6ee6147eebdc0c9e12bfa621787ced | |
| parent | 933085b944ecef3d50de3c81444079c30c462ca9 (diff) | |
Enriched numClosedFieldType so that it factors a lot of theory from both complex and algC.
The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.
| -rw-r--r-- | etc/ChangeLog | 13 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 738 | ||||
| -rw-r--r-- | mathcomp/character/all_character.v | 14 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/algC.v | 672 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 8 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 2 | ||||
| -rw-r--r-- | mathcomp/odd_order/BGappendixC.v | 11 | ||||
| -rw-r--r-- | mathcomp/odd_order/PFsection11.v | 2 | ||||
| -rw-r--r-- | mathcomp/odd_order/PFsection3.v | 2 | ||||
| -rw-r--r-- | mathcomp/odd_order/PFsection5.v | 8 | ||||
| -rw-r--r-- | mathcomp/odd_order/PFsection6.v | 6 | ||||
| -rw-r--r-- | mathcomp/odd_order/PFsection7.v | 2 | ||||
| -rw-r--r-- | mathcomp/real_closed/complex.v | 320 | ||||
| -rw-r--r-- | mathcomp/real_closed/polyrcf.v | 42 |
17 files changed, 993 insertions, 859 deletions
diff --git a/etc/ChangeLog b/etc/ChangeLog index ee28d7d..e33edb4 100644 --- a/etc/ChangeLog +++ b/etc/ChangeLog @@ -1,3 +1,16 @@ +25/08/2016 - refactoring of algC and complex in ssrnum - development version + * ssrnum's interface numClosedFieldType factors some theory from + both complex and algC. Because of that Re, Im, 'i, conjC, n.-root + and sqrtC are not specialized to algC anymore. In case of + ambiguity, they should be instanciated with algC using typing + constraints. Moreoever some lemmas from the theory like conjCK + have an extra nonmaximal implicit argument (C : + numClosedFieldType) which could break some proofs. Additionally, + ad-hoc constructions from complex.v like -*+ or complex.Re are now + deprecated and one should rely solely on the ssrnum interface. The + next revision might definietly hide those constructions under a + module. + 24/11/2015 - major reorganization of the archive - version 1.6 * Files split into subdirectories: ssreflect, algebra, fingroup, solvable, field and character. In this way the user can decide diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 9012291..9a38f5b 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -11,8 +11,6 @@ Require Import bigop ssralg div ssrnum ssrint. (* structure of archimedean, real field, with int and nat declared as closed *) (* subrings. *) (* rat == the type of rational number, with single constructor Rat *) -(* Rat p h == the element of type rat build from p a pair of integers and*) -(* h a proof of (0 < p.2) && coprime `|p.1| `|p.2| *) (* n%:Q == explicit cast from int to rat, postfix notation for the *) (* ratz constant *) (* numq r == numerator of (r : rat) *) diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index a494f3f..887fa9b 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -5107,6 +5107,12 @@ Variable F : closedFieldType. Lemma solve_monicpoly : ClosedField.axiom F. Proof. by case: F => ? []. Qed. +Lemma imaginary_exists : {i : F | i ^+ 2 = -1}. +Proof. +have /sig_eqW[i Di2] := @solve_monicpoly 2 (nth 0 [:: -1]) isT. +by exists i; rewrite Di2 !big_ord_recl big_ord0 mul0r mulr1 !addr0. +Qed. + End ClosedFieldTheory. Module SubType. @@ -5741,6 +5747,7 @@ Definition rmorph_alg := rmorph_alg. Definition lrmorphismP := lrmorphismP. Definition can2_lrmorphism := can2_lrmorphism. Definition bij_lrmorphism := bij_lrmorphism. +Definition imaginary_exists := imaginary_exists. Notation null_fun V := (null_fun V) (only parsing). Notation in_alg A := (in_alg_loc A). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index b1c1746..47d73e6 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2,7 +2,7 @@ (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype. +Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype path. From mathcomp Require Import bigop ssralg finset fingroup zmodp poly. @@ -60,17 +60,24 @@ Require Import bigop ssralg finset fingroup zmodp poly. (* == clone of a canonical archiFieldType structure on T *) (* *) (* * RealClosedField (Real Field with the real closed axiom) *) -(* realClosedFieldType *) -(* == interface for a real closed field. *) -(* RealClosedFieldType T r *) -(* == packs the real closed axiom r into a *) -(* realClodedFieldType. The carrier T must have a real *) +(* rcfType == interface for a real closed field. *) +(* RcfType T r == packs the real closed axiom r into a *) +(* rcfType. The carrier T must have a real *) (* field type structure. *) -(* [realClosedFieldType of T for S ] *) -(* == T-clone of the realClosedFieldType structure S. *) -(* [realClosedFieldype of T] *) -(* == clone of a canonical realClosedFieldType structure on *) +(* [rcfType of T] == clone of a canonical realClosedFieldType structure on *) (* T. *) +(* [rcfType of T for S ] *) +(* == T-clone of the realClosedFieldType structure S. *) +(* *) +(* * NumClosedField (Partially ordered Closed Field with conjugation) *) +(* numClosedFieldType == interface for a closed field with conj. *) +(* NumClosedFieldType T r == packs the real closed axiom r into a *) +(* numClosedFieldType. The carrier T must have a closed *) +(* field type structure. *) +(* [numClosedFieldType of T] == clone of a canonical numClosedFieldType *) +(* structure on T *) +(* [numClosedFieldType of T for S ] *) +(* == T-clone of the realClosedFieldType structure S. *) (* *) (* Over these structures, we have the following operations *) (* `|x| == norm of x. *) @@ -89,6 +96,18 @@ Require Import bigop ssralg finset fingroup zmodp poly. (* and n such that `|x| < n%:R. *) (* Num.sqrt x == in a real-closed field, a positive square root of x if *) (* x >= 0, or 0 otherwise. *) +(* For numeric algebraically closed fields we provide the generic definitions *) +(* 'i == the imaginary number (:= sqrtC (-1)). *) +(* 'Re z == the real component of z. *) +(* 'Im z == the imaginary component of z. *) +(* z^* == the complex conjugate of z (:= conjC z). *) +(* sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. *) +(* n.-root z == more generally, for n > 0, an nth root of z, chosen with a *) +(* minimal non-negative argument for n > 1 (i.e., with a *) +(* maximal real part subject to a nonnegative imaginary part). *) +(* Note that n.-root (-1) is a primitive 2nth root of unity, *) +(* an thus not equal to -1 for n odd > 1 (this will be shown in *) +(* file cyclotomic.v). *) (* *) (* There are now three distinct uses of the symbols <, <=, > and >=: *) (* 0-ary, unary (prefix) and binary (infix). *) @@ -401,9 +420,17 @@ Module ClosedField. Section ClassDef. +Record imaginary_mixin_of (R : numDomainType) := ImaginaryMixin { + imaginary : R; + conj_op : {rmorphism R -> R}; + _ : imaginary ^+ 2 = - 1; + _ : forall x, x * conj_op x = `|x| ^+ 2; +}. + Record class_of R := Class { base : GRing.ClosedField.class_of R; - mixin : mixin_of (ring_for R base) + mixin : mixin_of (ring_for R base); + conj_mixin : imaginary_mixin_of (num_for R (NumDomain.Class mixin)) }. Definition base2 R (c : class_of R) := NumField.Class (mixin c). Local Coercion base : class_of >-> GRing.ClosedField.class_of. @@ -419,7 +446,8 @@ Definition pack := fun bT b & phant_id (GRing.ClosedField.class bT) (b : GRing.ClosedField.class_of T) => fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) => - Pack (@Class T b m) T. + fun mc => Pack (@Class T b m mc) T. +Definition clone := fun b & phant_id class (b : class_of T) => Pack b T. Definition eqType := @Equality.Pack cT xclass xT. Definition choiceType := @Choice.Pack cT xclass xT. @@ -431,6 +459,7 @@ Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. Definition numDomainType := @NumDomain.Pack cT xclass xT. Definition fieldType := @GRing.Field.Pack cT xclass xT. +Definition numFieldType := @NumField.Pack cT xclass xT. Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT. Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT. Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass xT. @@ -467,6 +496,8 @@ Coercion fieldType : type >-> GRing.Field.type. Canonical fieldType. Coercion decFieldType : type >-> GRing.DecidableField.type. Canonical decFieldType. +Coercion numFieldType : type >-> NumField.type. +Canonical numFieldType. Coercion closedFieldType : type >-> GRing.ClosedField.type. Canonical closedFieldType. Canonical join_dec_numDomainType. @@ -474,7 +505,11 @@ Canonical join_dec_numFieldType. Canonical join_numDomainType. Canonical join_numFieldType. Notation numClosedFieldType := type. -Notation "[ 'numClosedFieldType' 'of' T ]" := (@pack T _ _ id _ _ id) +Notation NumClosedFieldType T m := (@pack T _ _ id _ _ id m). +Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ id) + (at level 0, format "[ 'numClosedFieldType' 'of' T 'for' cT ]") : + form_scope. +Notation "[ 'numClosedFieldType' 'of' T ]" := (@clone T _ _ id) (at level 0, format "[ 'numClosedFieldType' 'of' T ]") : form_scope. End Exports. @@ -4085,6 +4120,682 @@ Qed. End RealClosedFieldTheory. +Definition conjC {C : numClosedFieldType} : {rmorphism C -> C} := + ClosedField.conj_op (ClosedField.conj_mixin (ClosedField.class C)). +Notation "z ^*" := (@conjC _ z) (at level 2, format "z ^*") : ring_scope. + +Definition imaginaryC {C : numClosedFieldType} : C := + ClosedField.imaginary (ClosedField.conj_mixin (ClosedField.class C)). +Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope. + +Section ClosedFieldTheory. + +Variable C : numClosedFieldType. +Implicit Types a x y z : C. + +Definition normCK x : `|x| ^+ 2 = x * x^*. +Proof. by case: C x => ? [? ? []]. Qed. + +Lemma sqrCi : 'i ^+ 2 = -1 :> C. +Proof. by case: C => ? [? ? []]. Qed. + +Lemma conjCK : involutive (@conjC C). +Proof. +have JE x : x^* = `|x|^+2 / x. + have [->|x_neq0] := eqVneq x 0; first by rewrite rmorph0 invr0 mulr0. + by apply: (canRL (mulfK _)) => //; rewrite mulrC -normCK. +move=> x; have [->|x_neq0] := eqVneq x 0; first by rewrite !rmorph0. +rewrite !JE normrM normfV exprMn normrX normr_id. +rewrite invfM exprVn mulrA -[X in X * _]mulrA -invfM -exprMn. +by rewrite divff ?mul1r ?invrK // !expf_eq0 normr_eq0 //. +Qed. + +Let Re2 z := z + z^*. +Definition nnegIm z := (0 <= imaginaryC * (z^* - z)). +Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z <= Re2 y). + +CoInductive rootC_spec n (x : C) : Type := + RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0 + & forall z, (n > 0)%N -> z ^+ n = x -> argCle y z. + +Fact rootC_subproof n x : rootC_spec n x. +Proof. +have realRe2 u : Re2 u \is Num.real. + rewrite realEsqr expr2 {2}/Re2 -{2}[u]conjCK addrC -rmorphD -normCK. + by rewrite exprn_ge0 ?normr_ge0. +have argCle_total : total argCle. + move=> u v; rewrite /total /argCle. + by do 2!case: (nnegIm _) => //; rewrite ?orbT //= real_leVge. +have argCle_trans : transitive argCle. + move=> u v w /implyP geZuv /implyP geZvw; apply/implyP. + by case/geZvw/andP=> /geZuv/andP[-> geRuv] /ler_trans->. +pose p := 'X^n - (x *+ (n > 0))%:P; have [r0 Dp] := closed_field_poly_normal p. +have sz_p: size p = n.+1. + rewrite size_addl ?size_polyXn // ltnS size_opp size_polyC mulrn_eq0. + by case: posnP => //; case: negP. +pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. +have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P). + rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. + rewrite subr0 eqxx scale1r; apply: eq_big_perm. + by rewrite perm_eq_sym perm_sort. +have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). + move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0. + by rewrite subr_eq0; apply: eqP. +exists r`_0 => [|z n_gt0 /(mem_rP z n_gt0) r_z]. + have sz_r: size r = n by apply: succn_inj; rewrite -sz_p Dp size_prod_XsubC. + case: posnP => [n0 | n_gt0]; first by rewrite nth_default // sz_r n0. + by apply/mem_rP=> //; rewrite mem_nth ?sz_r. +case: {Dp mem_rP}r r_z r_arg => // y r1; rewrite inE => /predU1P[-> _|r1z]. + by apply/implyP=> ->; rewrite lerr. +by move/(order_path_min argCle_trans)/allP->. +Qed. + +Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y. +Notation "n .-root" := (nthroot n) (at level 2, format "n .-root") : ring_core_scope. +Notation "n .-root" := (nthroot n) (only parsing) : ring_scope. +Notation sqrtC := 2.-root. + +Definition Re x := (x + x^*) / 2%:R. +Definition Im x := 'i * (x^* - x) / 2%:R. +Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope. +Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope. + +Let nz2 : 2%:R != 0 :> C. Proof. by rewrite pnatr_eq0. Qed. + +Lemma normCKC x : `|x| ^+ 2 = x^* * x. Proof. by rewrite normCK mulrC. Qed. + +Lemma mul_conjC_ge0 x : 0 <= x * x^*. +Proof. by rewrite -normCK exprn_ge0 ?normr_ge0. Qed. + +Lemma mul_conjC_gt0 x : (0 < x * x^*) = (x != 0). +Proof. +have [->|x_neq0] := altP eqP; first by rewrite rmorph0 mulr0. +by rewrite -normCK exprn_gt0 ?normr_gt0. +Qed. + +Lemma mul_conjC_eq0 x : (x * x^* == 0) = (x == 0). +Proof. by rewrite -normCK expf_eq0 normr_eq0. Qed. + +Lemma conjC_ge0 x : (0 <= x^*) = (0 <= x). +Proof. +wlog suffices: x / 0 <= x -> 0 <= x^*. + by move=> IH; apply/idP/idP=> /IH; rewrite ?conjCK. +rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite rmorph0. +by rewrite -(pmulr_rge0 _ x_gt0) mul_conjC_ge0. +Qed. + +Lemma conjC_nat n : (n%:R)^* = n%:R :> C. Proof. exact: rmorph_nat. Qed. +Lemma conjC0 : 0^* = 0 :> C. Proof. exact: rmorph0. Qed. +Lemma conjC1 : 1^* = 1 :> C. Proof. exact: rmorph1. Qed. +Lemma conjC_eq0 x : (x^* == 0) = (x == 0). Proof. exact: fmorph_eq0. Qed. + +Lemma invC_norm x : x^-1 = `|x| ^- 2 * x^*. +Proof. +have [-> | nx_x] := eqVneq x 0; first by rewrite conjC0 mulr0 invr0. +by rewrite normCK invfM divfK ?conjC_eq0. +Qed. + +(* Real number subset. *) + +Lemma CrealE x : (x \is real) = (x^* == x). +Proof. +rewrite realEsqr ger0_def normrX normCK. +by have [-> | /mulfI/inj_eq-> //] := eqVneq x 0; rewrite rmorph0 !eqxx. +Qed. + +Lemma CrealP {x} : reflect (x^* = x) (x \is real). +Proof. by rewrite CrealE; apply: eqP. Qed. + +Lemma conj_Creal x : x \is real -> x^* = x. +Proof. by move/CrealP. Qed. + +Lemma conj_normC z : `|z|^* = `|z|. +Proof. by rewrite conj_Creal ?normr_real. Qed. + +Lemma geC0_conj x : 0 <= x -> x^* = x. +Proof. by move=> /ger0_real/CrealP. Qed. + +Lemma geC0_unit_exp x n : 0 <= x -> (x ^+ n.+1 == 1) = (x == 1). +Proof. by move=> x_ge0; rewrite pexpr_eq1. Qed. + +(* Elementary properties of roots. *) + +Ltac case_rootC := rewrite /nthroot; case: (rootC_subproof _ _). + +Lemma root0C x : 0.-root x = 0. Proof. by case_rootC. Qed. + +Lemma rootCK n : (n > 0)%N -> cancel n.-root (fun x => x ^+ n). +Proof. by case: n => //= n _ x; case_rootC. Qed. + +Lemma root1C x : 1.-root x = x. Proof. exact: (@rootCK 1). Qed. + +Lemma rootC0 n : n.-root 0 = 0. +Proof. +have [-> | n_gt0] := posnP n; first by rewrite root0C. +by have /eqP := rootCK n_gt0 0; rewrite expf_eq0 n_gt0 /= => /eqP. +Qed. + +Lemma rootC_inj n : (n > 0)%N -> injective n.-root. +Proof. by move/rootCK/can_inj. Qed. + +Lemma eqr_rootC n : (n > 0)%N -> {mono n.-root : x y / x == y}. +Proof. by move/rootC_inj/inj_eq. Qed. + +Lemma rootC_eq0 n x : (n > 0)%N -> (n.-root x == 0) = (x == 0). +Proof. by move=> n_gt0; rewrite -{1}(rootC0 n) eqr_rootC. Qed. + +(* Rectangular coordinates. *) + +Lemma nonRealCi : ('i : C) \isn't real. +Proof. by rewrite realEsqr sqrCi oppr_ge0 ltr_geF ?ltr01. Qed. + +Lemma neq0Ci : 'i != 0 :> C. +Proof. by apply: contraNneq nonRealCi => ->; apply: real0. Qed. + +Lemma normCi : `|'i| = 1 :> C. +Proof. +apply/eqP; rewrite -(@pexpr_eq1 _ _ 2) ?normr_ge0 //. +by rewrite -normrX sqrCi normrN1. +Qed. + +Lemma invCi : 'i^-1 = - 'i :> C. +Proof. by rewrite -div1r -[1]opprK -sqrCi mulNr mulfK ?neq0Ci. Qed. + +Lemma conjCi : 'i^* = - 'i :> C. +Proof. by rewrite -invCi invC_norm normCi expr1n invr1 mul1r. Qed. + +Lemma Crect x : x = 'Re x + 'i * 'Im x. +Proof. +rewrite 2!mulrA -expr2 sqrCi mulN1r opprB -mulrDl addrACA subrr addr0. +by rewrite -mulr2n -mulr_natr mulfK. +Qed. + +Lemma Creal_Re x : 'Re x \is real. +Proof. by rewrite CrealE fmorph_div rmorph_nat rmorphD conjCK addrC. Qed. + +Lemma Creal_Im x : 'Im x \is real. +Proof. +rewrite CrealE fmorph_div rmorph_nat rmorphM rmorphB conjCK. +by rewrite conjCi -opprB mulrNN. +Qed. +Hint Resolve Creal_Re Creal_Im. + +Fact Re_is_additive : additive Re. +Proof. by move=> x y; rewrite /Re rmorphB addrACA -opprD mulrBl. Qed. +Canonical Re_additive := Additive Re_is_additive. + +Fact Im_is_additive : additive Im. +Proof. +by move=> x y; rewrite /Im rmorphB opprD addrACA -opprD mulrBr mulrBl. +Qed. +Canonical Im_additive := Additive Im_is_additive. + +Lemma Creal_ImP z : reflect ('Im z = 0) (z \is real). +Proof. +rewrite CrealE -subr_eq0 -(can_eq (mulKf neq0Ci)) mulr0. +by rewrite -(can_eq (divfK nz2)) mul0r; apply: eqP. +Qed. + +Lemma Creal_ReP z : reflect ('Re z = z) (z \in real). +Proof. +rewrite (sameP (Creal_ImP z) eqP) -(can_eq (mulKf neq0Ci)) mulr0. +by rewrite -(inj_eq (addrI ('Re z))) addr0 -Crect eq_sym; apply: eqP. +Qed. + +Lemma ReMl : {in real, forall x, {morph Re : z / x * z}}. +Proof. +by move=> x Rx z /=; rewrite /Re rmorphM (conj_Creal Rx) -mulrDr -mulrA. +Qed. + +Lemma ReMr : {in real, forall x, {morph Re : z / z * x}}. +Proof. by move=> x Rx z /=; rewrite mulrC ReMl // mulrC. Qed. + +Lemma ImMl : {in real, forall x, {morph Im : z / x * z}}. +Proof. +by move=> x Rx z; rewrite /Im rmorphM (conj_Creal Rx) -mulrBr mulrCA !mulrA. +Qed. + +Lemma ImMr : {in real, forall x, {morph Im : z / z * x}}. +Proof. by move=> x Rx z /=; rewrite mulrC ImMl // mulrC. Qed. + +Lemma Re_i : 'Re 'i = 0. Proof. by rewrite /Re conjCi subrr mul0r. Qed. + +Lemma Im_i : 'Im 'i = 1. +Proof. +rewrite /Im conjCi -opprD mulrN -mulr2n mulrnAr ['i * _]sqrCi. +by rewrite mulNrn opprK divff. +Qed. + +Lemma Re_conj z : 'Re z^* = 'Re z. +Proof. by rewrite /Re addrC conjCK. Qed. + +Lemma Im_conj z : 'Im z^* = - 'Im z. +Proof. by rewrite /Im -mulNr -mulrN opprB conjCK. Qed. + +Lemma Re_rect : {in real &, forall x y, 'Re (x + 'i * y) = x}. +Proof. +move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ReP x Rx). +by rewrite ReMr // Re_i mul0r addr0. +Qed. + +Lemma Im_rect : {in real &, forall x y, 'Im (x + 'i * y) = y}. +Proof. +move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ImP x Rx) add0r. +by rewrite ImMr // Im_i mul1r. +Qed. + +Lemma conjC_rect : {in real &, forall x y, (x + 'i * y)^* = x - 'i * y}. +Proof. +by move=> x y Rx Ry; rewrite /= rmorphD rmorphM conjCi mulNr !conj_Creal. +Qed. + +Lemma addC_rect x1 y1 x2 y2 : + (x1 + 'i * y1) + (x2 + 'i * y2) = x1 + x2 + 'i * (y1 + y2). +Proof. by rewrite addrACA -mulrDr. Qed. + +Lemma oppC_rect x y : - (x + 'i * y) = - x + 'i * (- y). +Proof. by rewrite mulrN -opprD. Qed. + +Lemma subC_rect x1 y1 x2 y2 : + (x1 + 'i * y1) - (x2 + 'i * y2) = x1 - x2 + 'i * (y1 - y2). +Proof. by rewrite oppC_rect addC_rect. Qed. + +Lemma mulC_rect x1 y1 x2 y2 : + (x1 + 'i * y1) * (x2 + 'i * y2) + = x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1). +Proof. +rewrite mulrDl !mulrDr mulrCA -!addrA mulrAC -mulrA; congr (_ + _). +by rewrite mulrACA -expr2 sqrCi mulN1r addrA addrC. +Qed. + +Lemma normC2_rect : + {in real &, forall x y, `|x + 'i * y| ^+ 2 = x ^+ 2 + y ^+ 2}. +Proof. +move=> x y Rx Ry; rewrite /= normCK rmorphD rmorphM conjCi !conj_Creal //. +by rewrite mulrC mulNr -subr_sqr exprMn sqrCi mulN1r opprK. +Qed. + +Lemma normC2_Re_Im z : `|z| ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2. +Proof. by rewrite -normC2_rect -?Crect. Qed. + +Lemma invC_rect : + {in real &, forall x y, (x + 'i * y)^-1 = (x - 'i * y) / (x ^+ 2 + y ^+ 2)}. +Proof. +by move=> x y Rx Ry; rewrite /= invC_norm conjC_rect // mulrC normC2_rect. +Qed. + +Lemma lerif_normC_Re_Creal z : `|'Re z| <= `|z| ?= iff (z \is real). +Proof. +rewrite -(mono_in_lerif ler_sqr); try by rewrite qualifE normr_ge0. +rewrite normCK conj_Creal // normC2_Re_Im -expr2. +rewrite addrC -lerif_subLR subrr (sameP (Creal_ImP _) eqP) -sqrf_eq0 eq_sym. +by apply: lerif_eq; rewrite -realEsqr. +Qed. + +Lemma lerif_Re_Creal z : 'Re z <= `|z| ?= iff (0 <= z). +Proof. +have ubRe: 'Re z <= `|'Re z| ?= iff (0 <= 'Re z). + by rewrite ger0_def eq_sym; apply/lerif_eq/real_ler_norm. +congr (_ <= _ ?= iff _): (lerif_trans ubRe (lerif_normC_Re_Creal z)). +apply/andP/idP=> [[zRge0 /Creal_ReP <- //] | z_ge0]. +by have Rz := ger0_real z_ge0; rewrite (Creal_ReP _ _). +Qed. + +(* Equality from polar coordinates, for the upper plane. *) +Lemma eqC_semipolar x y : + `|x| = `|y| -> 'Re x = 'Re y -> 0 <= 'Im x * 'Im y -> x = y. +Proof. +move=> eq_norm eq_Re sign_Im. +rewrite [x]Crect [y]Crect eq_Re; congr (_ + 'i * _). +have /eqP := congr1 (fun z => z ^+ 2) eq_norm. +rewrite !normC2_Re_Im eq_Re (can_eq (addKr _)) eqf_sqr => /pred2P[] // eq_Im. +rewrite eq_Im mulNr -expr2 oppr_ge0 real_exprn_even_le0 //= in sign_Im. +by rewrite eq_Im (eqP sign_Im) oppr0. +Qed. + +(* Nth roots. *) + +Let argCleP y z : + reflect (0 <= 'Im z -> 0 <= 'Im y /\ 'Re z <= 'Re y) (argCle y z). +Proof. +suffices dIm x: nnegIm x = (0 <= 'Im x). + rewrite /argCle !dIm ler_pmul2r ?invr_gt0 ?ltr0n //. + by apply: (iffP implyP) => geZyz /geZyz/andP. +by rewrite /('Im x) pmulr_lge0 ?invr_gt0 ?ltr0n //; congr (0 <= _ * _). +Qed. +(* case Du: sqrCi => [u u2N1] /=. *) +(* have/eqP := u2N1; rewrite -sqrCi eqf_sqr => /pred2P[] //. *) +(* have:= conjCi; rewrite /'i; case_rootC => /= v v2n1 min_v conj_v Duv. *) +(* have{min_v} /idPn[] := min_v u isT u2N1; rewrite negb_imply /nnegIm Du /= Duv. *) +(* rewrite rmorphN conj_v opprK -opprD mulrNN mulNr -mulr2n mulrnAr -expr2 v2n1. *) +(* by rewrite mulNrn opprK ler0n oppr_ge0 (ler_nat _ 2 0). *) + + +Lemma rootC_Re_max n x y : + (n > 0)%N -> y ^+ n = x -> 0 <= 'Im y -> 'Re y <= 'Re (n.-root x). +Proof. +by move=> n_gt0 yn_x leI0y; case_rootC=> z /= _ /(_ y n_gt0 yn_x)/argCleP[]. +Qed. + +Let neg_unity_root n : (n > 1)%N -> exists2 w : C, w ^+ n = 1 & 'Re w < 0. +Proof. +move=> n_gt1; have [|w /eqP pw_0] := closed_rootP (\poly_(i < n) (1 : C)) _. + by rewrite size_poly_eq ?oner_eq0 // -(subnKC n_gt1). +rewrite horner_poly (eq_bigr _ (fun _ _ => mul1r _)) in pw_0. +have wn1: w ^+ n = 1 by apply/eqP; rewrite -subr_eq0 subrX1 pw_0 mulr0. +suffices /existsP[i ltRwi0]: [exists i : 'I_n, 'Re (w ^+ i) < 0]. + by exists (w ^+ i) => //; rewrite exprAC wn1 expr1n. +apply: contra_eqT (congr1 Re pw_0); rewrite negb_exists => /forallP geRw0. +rewrite raddf_sum raddf0 /= (bigD1 (Ordinal (ltnW n_gt1))) //=. +rewrite (Creal_ReP _ _) ?rpred1 // gtr_eqF ?ltr_paddr ?ltr01 //=. +by apply: sumr_ge0 => i _; rewrite real_lerNgt ?rpred0. +Qed. + +Lemma Im_rootC_ge0 n x : (n > 1)%N -> 0 <= 'Im (n.-root x). +Proof. +set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1. +apply: wlog_neg; rewrite -real_ltrNge ?rpred0 // => ltIy0. +suffices [z zn_x leI0z]: exists2 z, z ^+ n = x & 'Im z >= 0. + by rewrite /y; case_rootC => /= y1 _ /(_ z n_gt0 zn_x)/argCleP[]. +have [w wn1 ltRw0] := neg_unity_root n_gt1. +wlog leRI0yw: w wn1 ltRw0 / 0 <= 'Re y * 'Im w. + move=> IHw; have: 'Re y * 'Im w \is real by rewrite rpredM. + case/real_ger0P=> [|/ltrW leRIyw0]; first exact: IHw. + apply: (IHw w^*); rewrite ?Re_conj ?Im_conj ?mulrN ?oppr_ge0 //. + by rewrite -rmorphX wn1 rmorph1. +exists (w * y); first by rewrite exprMn wn1 mul1r rootCK. +rewrite [w]Crect [y]Crect mulC_rect. +by rewrite Im_rect ?rpredD ?rpredN 1?rpredM // addr_ge0 // ltrW ?nmulr_rgt0. +Qed. + +Lemma rootC_lt0 n x : (1 < n)%N -> (n.-root x < 0) = false. +Proof. +set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1. +apply: negbTE; apply: wlog_neg => /negbNE lt0y; rewrite ler_gtF //. +have Rx: x \is real by rewrite -[x](rootCK n_gt0) rpredX // ltr0_real. +have Re_y: 'Re y = y by apply/Creal_ReP; rewrite ltr0_real. +have [z zn_x leR0z]: exists2 z, z ^+ n = x & 'Re z >= 0. + have [w wn1 ltRw0] := neg_unity_root n_gt1. + exists (w * y); first by rewrite exprMn wn1 mul1r rootCK. + by rewrite ReMr ?ltr0_real // ltrW // nmulr_lgt0. +without loss leI0z: z zn_x leR0z / 'Im z >= 0. + move=> IHz; have: 'Im z \is real by []. + case/real_ger0P=> [|/ltrW leIz0]; first exact: IHz. + apply: (IHz z^*); rewrite ?Re_conj ?Im_conj ?oppr_ge0 //. + by rewrite -rmorphX zn_x conj_Creal. +by apply: ler_trans leR0z _; rewrite -Re_y ?rootC_Re_max ?ltr0_real. +Qed. + +Lemma rootC_ge0 n x : (n > 0)%N -> (0 <= n.-root x) = (0 <= x). +Proof. +set y := n.-root x => n_gt0. +apply/idP/idP=> [/(exprn_ge0 n) | x_ge0]; first by rewrite rootCK. +rewrite -(ger_lerif (lerif_Re_Creal y)). +have Ray: `|y| \is real by apply: normr_real. +rewrite -(Creal_ReP _ Ray) rootC_Re_max ?(Creal_ImP _ Ray) //. +by rewrite -normrX rootCK // ger0_norm. +Qed. + +Lemma rootC_gt0 n x : (n > 0)%N -> (n.-root x > 0) = (x > 0). +Proof. by move=> n_gt0; rewrite !lt0r rootC_ge0 ?rootC_eq0. Qed. + +Lemma rootC_le0 n x : (1 < n)%N -> (n.-root x <= 0) = (x == 0). +Proof. +by move=> n_gt1; rewrite ler_eqVlt rootC_lt0 // orbF rootC_eq0 1?ltnW. +Qed. + +Lemma ler_rootCl n : (n > 0)%N -> {in Num.nneg, {mono n.-root : x y / x <= y}}. +Proof. +move=> n_gt0 x x_ge0 y; have [y_ge0 | not_y_ge0] := boolP (0 <= y). + by rewrite -(ler_pexpn2r n_gt0) ?qualifE ?rootC_ge0 ?rootCK. +rewrite (contraNF (@ler_trans _ _ 0 _ _)) ?rootC_ge0 //. +by rewrite (contraNF (ler_trans x_ge0)). +Qed. + +Lemma ler_rootC n : (n > 0)%N -> {in Num.nneg &, {mono n.-root : x y / x <= y}}. +Proof. by move=> n_gt0 x y x_ge0 _; apply: ler_rootCl. Qed. + +Lemma ltr_rootCl n : (n > 0)%N -> {in Num.nneg, {mono n.-root : x y / x < y}}. +Proof. by move=> n_gt0 x x_ge0 y; rewrite !ltr_def ler_rootCl ?eqr_rootC. Qed. + +Lemma ltr_rootC n : (n > 0)%N -> {in Num.nneg &, {mono n.-root : x y / x < y}}. +Proof. by move/ler_rootC/lerW_mono_in. Qed. + +Lemma exprCK n x : (0 < n)%N -> 0 <= x -> n.-root (x ^+ n) = x. +Proof. +move=> n_gt0 x_ge0; apply/eqP. +by rewrite -(eqr_expn2 n_gt0) ?rootC_ge0 ?exprn_ge0 ?rootCK. +Qed. + +Lemma norm_rootC n x : `|n.-root x| = n.-root `|x|. +Proof. +have [-> | n_gt0] := posnP n; first by rewrite !root0C normr0. +apply/eqP; rewrite -(eqr_expn2 n_gt0) ?rootC_ge0 ?normr_ge0 //. +by rewrite -normrX !rootCK. +Qed. + +Lemma rootCX n x k : (n > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k. +Proof. +move=> n_gt0 x_ge0; apply/eqP. +by rewrite -(eqr_expn2 n_gt0) ?(exprn_ge0, rootC_ge0) // 1?exprAC !rootCK. +Qed. + +Lemma rootC1 n : (n > 0)%N -> n.-root 1 = 1. +Proof. by move/(rootCX 0)/(_ ler01). Qed. + +Lemma rootCpX n x k : (k > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k. +Proof. +by case: n => [|n] k_gt0; [rewrite !root0C expr0n gtn_eqF | apply: rootCX]. +Qed. + +Lemma rootCV n x : (n > 0)%N -> 0 <= x -> n.-root x^-1 = (n.-root x)^-1. +Proof. +move=> n_gt0 x_ge0; apply/eqP. +by rewrite -(eqr_expn2 n_gt0) ?(invr_ge0, rootC_ge0) // !exprVn !rootCK. +Qed. + +Lemma rootC_eq1 n x : (n > 0)%N -> (n.-root x == 1) = (x == 1). +Proof. by move=> n_gt0; rewrite -{1}(rootC1 n_gt0) eqr_rootC. Qed. + +Lemma rootC_ge1 n x : (n > 0)%N -> (n.-root x >= 1) = (x >= 1). +Proof. +by move=> n_gt0; rewrite -{1}(rootC1 n_gt0) ler_rootCl // qualifE ler01. +Qed. + +Lemma rootC_gt1 n x : (n > 0)%N -> (n.-root x > 1) = (x > 1). +Proof. by move=> n_gt0; rewrite !ltr_def rootC_eq1 ?rootC_ge1. Qed. + +Lemma rootC_le1 n x : (n > 0)%N -> 0 <= x -> (n.-root x <= 1) = (x <= 1). +Proof. by move=> n_gt0 x_ge0; rewrite -{1}(rootC1 n_gt0) ler_rootCl. Qed. + +Lemma rootC_lt1 n x : (n > 0)%N -> 0 <= x -> (n.-root x < 1) = (x < 1). +Proof. by move=> n_gt0 x_ge0; rewrite !ltr_neqAle rootC_eq1 ?rootC_le1. Qed. + +Lemma rootCMl n x z : 0 <= x -> n.-root (x * z) = n.-root x * n.-root z. +Proof. +rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite !(mul0r, rootC0). +have [| n_gt1 | ->] := ltngtP n 1; last by rewrite !root1C. + by case: n => //; rewrite !root0C mul0r. +have [x_ge0 n_gt0] := (ltrW x_gt0, ltnW n_gt1). +have nx_gt0: 0 < n.-root x by rewrite rootC_gt0. +have Rnx: n.-root x \is real by rewrite ger0_real ?ltrW. +apply: eqC_semipolar; last 1 first; try apply/eqP. +- by rewrite ImMl // !(Im_rootC_ge0, mulr_ge0, rootC_ge0). +- by rewrite -(eqr_expn2 n_gt0) ?normr_ge0 // -!normrX exprMn !rootCK. +rewrite eqr_le; apply/andP; split; last first. + rewrite rootC_Re_max ?exprMn ?rootCK ?ImMl //. + by rewrite mulr_ge0 ?Im_rootC_ge0 ?ltrW. +rewrite -[n.-root _](mulVKf (negbT (gtr_eqF nx_gt0))) !(ReMl Rnx) //. +rewrite ler_pmul2l // rootC_Re_max ?exprMn ?exprVn ?rootCK ?mulKf ?gtr_eqF //. +by rewrite ImMl ?rpredV // mulr_ge0 ?invr_ge0 ?Im_rootC_ge0 ?ltrW. +Qed. + +Lemma rootCMr n x z : 0 <= x -> n.-root (z * x) = n.-root z * n.-root x. +Proof. by move=> x_ge0; rewrite mulrC rootCMl // mulrC. Qed. + +Lemma imaginaryCE : 'i = sqrtC (-1). +Proof. +have : sqrtC (-1) ^+ 2 - 'i ^+ 2 == 0 by rewrite sqrCi rootCK // subrr. +rewrite subr_sqr mulf_eq0 subr_eq0 addr_eq0; have [//|_/= /eqP sCN1E] := eqP. +by have := @Im_rootC_ge0 2 (-1) isT; rewrite sCN1E raddfN /= Im_i ler0N1. +Qed. + +(* More properties of n.-root will be established in cyclotomic.v. *) + +(* The proper form of the Arithmetic - Geometric Mean inequality. *) + +Lemma lerif_rootC_AGM (I : finType) (A : pred I) (n := #|A|) E : + {in A, forall i, 0 <= E i} -> + n.-root (\prod_(i in A) E i) <= (\sum_(i in A) E i) / n%:R + ?= iff [forall i in A, forall j in A, E i == E j]. +Proof. +move=> Ege0; have [n0 | n_gt0] := posnP n. + rewrite n0 root0C invr0 mulr0; apply/lerif_refl/forall_inP=> i. + by rewrite (card0_eq n0). +rewrite -(mono_in_lerif (ler_pexpn2r n_gt0)) ?rootCK //=; first 1 last. +- by rewrite qualifE rootC_ge0 // prodr_ge0. +- by rewrite rpred_div ?rpred_nat ?rpred_sum. +exact: lerif_AGM. +Qed. + +(* Square root. *) + +Lemma sqrtC0 : sqrtC 0 = 0. Proof. exact: rootC0. Qed. +Lemma sqrtC1 : sqrtC 1 = 1. Proof. exact: rootC1. Qed. +Lemma sqrtCK x : sqrtC x ^+ 2 = x. Proof. exact: rootCK. Qed. +Lemma sqrCK x : 0 <= x -> sqrtC (x ^+ 2) = x. Proof. exact: exprCK. Qed. + +Lemma sqrtC_ge0 x : (0 <= sqrtC x) = (0 <= x). Proof. exact: rootC_ge0. Qed. +Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0). Proof. exact: rootC_eq0. Qed. +Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0). Proof. exact: rootC_gt0. Qed. +Lemma sqrtC_lt0 x : (sqrtC x < 0) = false. Proof. exact: rootC_lt0. Qed. +Lemma sqrtC_le0 x : (sqrtC x <= 0) = (x == 0). Proof. exact: rootC_le0. Qed. + +Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x <= y}}. +Proof. exact: ler_rootC. Qed. +Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y}}. +Proof. exact: ltr_rootC. Qed. +Lemma eqr_sqrtC : {mono sqrtC : x y / x == y}. +Proof. exact: eqr_rootC. Qed. +Lemma sqrtC_inj : injective sqrtC. +Proof. exact: rootC_inj. Qed. +Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x * y}}. +Proof. by move=> x y _; apply: rootCMr. Qed. + +Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 <= 'Im x) && ~~ (x < 0)). +Proof. +apply: (iffP andP) => [[leI0x not_gt0x] | <-]; last first. + by rewrite sqrtC_lt0 Im_rootC_ge0. +have /eqP := sqrtCK (x ^+ 2); rewrite eqf_sqr => /pred2P[] // defNx. +apply: sqrCK; rewrite -real_lerNgt ?rpred0 // in not_gt0x; +apply/Creal_ImP/ler_anti; +by rewrite leI0x -oppr_ge0 -raddfN -defNx Im_rootC_ge0. +Qed. + +Lemma normC_def x : `|x| = sqrtC (x * x^*). +Proof. by rewrite -normCK sqrCK ?normr_ge0. Qed. + +Lemma norm_conjC x : `|x^*| = `|x|. +Proof. by rewrite !normC_def conjCK mulrC. Qed. + +Lemma normC_rect : + {in real &, forall x y, `|x + 'i * y| = sqrtC (x ^+ 2 + y ^+ 2)}. +Proof. by move=> x y Rx Ry; rewrite /= normC_def -normCK normC2_rect. Qed. + +Lemma normC_Re_Im z : `|z| = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2). +Proof. by rewrite normC_def -normCK normC2_Re_Im. Qed. + +(* Norm sum (in)equalities. *) + +Lemma normC_add_eq x y : + `|x + y| = `|x| + `|y| -> + {t : C | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}. +Proof. +move=> lin_xy; apply: sig2_eqW; pose u z := if z == 0 then 1 else z / `|z|. +have uE z: (`|u z| = 1) * (`|z| * u z = z). + rewrite /u; have [->|nz_z] := altP eqP; first by rewrite normr0 normr1 mul0r. + by rewrite normf_div normr_id mulrCA divff ?mulr1 ?normr_eq0. +have [->|nz_x] := eqVneq x 0; first by exists (u y); rewrite uE ?normr0 ?mul0r. +exists (u x); rewrite uE // /u (negPf nz_x); congr (_ , _). +have{lin_xy} def2xy: `|x| * `|y| *+ 2 = x * y ^* + y * x ^*. + apply/(addrI (x * x^*))/(addIr (y * y^*)); rewrite -2!{1}normCK -sqrrD. + by rewrite addrA -addrA -!mulrDr -mulrDl -rmorphD -normCK lin_xy. +have def_xy: x * y^* = y * x^*. + apply/eqP; rewrite -subr_eq0 -[_ == 0](@expf_eq0 _ _ 2). + rewrite (canRL (subrK _) (subr_sqrDB _ _)) opprK -def2xy exprMn_n exprMn. + by rewrite mulrN mulrAC mulrA -mulrA mulrACA -!normCK mulNrn addNr. +have{def_xy def2xy} def_yx: `|y * x| = y * x^*. + by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy. +rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM. +by rewrite mulrCA divfK ?normr_eq0 // mulrAC mulrA. +Qed. + +Lemma normC_sum_eq (I : finType) (P : pred I) (F : I -> C) : + `|\sum_(i | P i) F i| = \sum_(i | P i) `|F i| -> + {t : C | `|t| == 1 & forall i, P i -> F i = `|F i| * t}. +Proof. +have [i /andP[Pi nzFi] | F0] := pickP [pred i | P i & F i != 0]; last first. + exists 1 => [|i Pi]; first by rewrite normr1. + by case/nandP: (F0 i) => [/negP[]// | /negbNE/eqP->]; rewrite normr0 mul0r. +rewrite !(bigD1 i Pi) /= => norm_sumF; pose Q j := P j && (j != i). +rewrite -normr_eq0 in nzFi; set c := F i / `|F i|; exists c => [|j Pj]. + by rewrite normrM normfV normr_id divff. +have [Qj | /nandP[/negP[]// | /negbNE/eqP->]] := boolP (Q j); last first. + by rewrite mulrC divfK. +have: `|F i + F j| = `|F i| + `|F j|. + do [rewrite !(bigD1 j Qj) /=; set z := \sum_(k | _) `|_|] in norm_sumF. + apply/eqP; rewrite eqr_le ler_norm_add -(ler_add2r z) -addrA -norm_sumF addrA. + by rewrite (ler_trans (ler_norm_add _ _)) // ler_add2l ler_norm_sum. +by case/normC_add_eq=> k _ [/(canLR (mulKf nzFi)) <-]; rewrite -(mulrC (F i)). +Qed. + +Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I -> C) : + `|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) -> + (forall i, P i -> `|F i| = 1) -> + {t : C | `|t| == 1 & forall i, P i -> F i = t}. +Proof. +case/normC_sum_eq=> t t1 defF normF. +by exists t => // i Pi; rewrite defF // normF // mul1r. +Qed. + +Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I -> C) : + (forall i, P i -> `|F i| <= G i) -> + \sum_(i | P i) F i = \sum_(i | P i) G i -> + forall i, P i -> F i = G i. +Proof. +set sumF := \sum_(i | _) _; set sumG := \sum_(i | _) _ => leFG eq_sumFG. +have posG i: P i -> 0 <= G i by move/leFG; apply: ler_trans; apply: normr_ge0. +have norm_sumG: `|sumG| = sumG by rewrite ger0_norm ?sumr_ge0. +have norm_sumF: `|sumF| = \sum_(i | P i) `|F i|. + apply/eqP; rewrite eqr_le ler_norm_sum eq_sumFG norm_sumG -subr_ge0 -sumrB. + by rewrite sumr_ge0 // => i Pi; rewrite subr_ge0 ?leFG. +have [t _ defF] := normC_sum_eq norm_sumF. +have [/(psumr_eq0P posG) G0 i Pi | nz_sumG] := eqVneq sumG 0. + by apply/eqP; rewrite G0 // -normr_eq0 eqr_le normr_ge0 -(G0 i Pi) leFG. +have t1: t = 1. + apply: (mulfI nz_sumG); rewrite mulr1 -{1}norm_sumG -eq_sumFG norm_sumF. + by rewrite mulr_suml -(eq_bigr _ defF). +have /psumr_eq0P eqFG i: P i -> 0 <= G i - F i. + by move=> Pi; rewrite subr_ge0 defF // t1 mulr1 leFG. +move=> i /eqFG/(canRL (subrK _))->; rewrite ?add0r //. +by rewrite sumrB -/sumF eq_sumFG subrr. +Qed. + +Lemma normC_sub_eq x y : + `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}. +Proof. +rewrite -{-1}(subrK y x) => /(canLR (subrK _))/esym-Dx; rewrite Dx. +by have [t ? [Dxy Dy]] := normC_add_eq Dx; exists t; rewrite // mulrDl -Dxy -Dy. +Qed. + +End ClosedFieldTheory. + +Notation "n .-root" := (@nthroot _ n) (at level 2, format "n .-root") : ring_scope. +Notation sqrtC := 2.-root. +Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope. +Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope. +Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope. + End Theory. Module RealMixin. @@ -4225,3 +4936,4 @@ Export Num.Syntax Num.PredInstances. Notation RealLeMixin := Num.RealMixin.Le. Notation RealLtMixin := Num.RealMixin.Lt. Notation RealLeAxiom R := (Num.RealMixin.Real (Phant R) (erefl _)). +Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin. diff --git a/mathcomp/character/all_character.v b/mathcomp/character/all_character.v index 936fa6c..03f1b57 100644 --- a/mathcomp/character/all_character.v +++ b/mathcomp/character/all_character.v @@ -1,7 +1,7 @@ -Require Export character. -Require Export classfun. -Require Export inertia. -Require Export integral_char. -Require Export mxabelem. -Require Export mxrepresentation. -Require Export vcharacter. +From mathcomp Require Export character. +From mathcomp Require Export classfun. +From mathcomp Require Export inertia. +From mathcomp Require Export integral_char. +From mathcomp Require Export mxabelem. +From mathcomp Require Export mxrepresentation. +From mathcomp Require Export vcharacter. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 4c27bd7..7473338 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -969,7 +969,8 @@ Lemma cfCauchySchwarz_sqrt phi psi : `|'[phi, psi]| <= sqrtC '[phi] * sqrtC '[psi] ?= iff ~~ free (phi :: psi). Proof. rewrite -(sqrCK (normr_ge0 _)) -sqrtCM ?qualifE ?cfnorm_ge0 //. -rewrite (mono_in_lerif ler_sqrtC) 1?rpredM ?qualifE ?normr_ge0 ?cfnorm_ge0 //. +rewrite (mono_in_lerif (@ler_sqrtC _)) 1?rpredM ?qualifE; +rewrite ?normr_ge0 ?cfnorm_ge0 //. exact: cfCauchySchwarz. Qed. diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index b465542..6c53127 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -17,6 +17,14 @@ Require Import algebraics_fundamentals. (* algebraic contents of the Fundamenta Theorem of Algebra. *) (* algC == the closed, countable field of algebraic numbers. *) (* algCeq, algCring, ..., algCnumField == structures for algC. *) +(* The ssrnum interfaces are implemented for algC as follows: *) +(* x <= y <=> (y - x) is a nonnegative real *) +(* x < y <=> (y - x) is a (strictly) positive real *) +(* `|z| == the complex norm of z, i.e., sqrtC (z * z^* ). *) +(* Creal == the subset of real numbers (:= Num.real for algC). *) +(* 'i == the imaginary number (:= sqrtC (-1)). *) +(* 'Re z == the real component of z. *) +(* 'Im z == the imaginary component of z. *) (* z^* == the complex conjugate of z (:= conjC z). *) (* sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. *) (* n.-root z == more generally, for n > 0, an nth root of z, chosen with a *) @@ -25,15 +33,7 @@ Require Import algebraics_fundamentals. (* Note that n.-root (-1) is a primitive 2nth root of unity, *) (* an thus not equal to -1 for n odd > 1 (this will be shown in *) (* file cyclotomic.v). *) -(* The ssrnum interfaces are implemented for algC as follows: *) -(* x <= y <=> (y - x) is a nonnegative real *) -(* x < y <=> (y - x) is a (strictly) positive real *) -(* `|z| == the complex norm of z, i.e., sqrtC (z * z^* ). *) -(* Creal == the subset of real numbers (:= Num.real for algC). *) (* In addition, we provide: *) -(* 'i == the imaginary number (:= sqrtC (-1)). *) -(* 'Re z == the real component of z. *) -(* 'Im z == the imaginary component of z. *) (* Crat == the subset of rational numbers. *) (* Cint == the subset of integers. *) (* Cnat == the subset of natural integers. *) @@ -237,9 +237,8 @@ Parameter numMixin : Num.mixin_of ringType. Canonical numDomainType := NumDomainType type numMixin. Canonical numFieldType := [numFieldType of type]. -Parameter conj : {rmorphism type -> type}. -Axiom conjK : involutive conj. -Axiom normK : forall x, `|x| ^+ 2 = x * conj x. +Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType. +Canonical numClosedFieldType := NumClosedFieldType type conjMixin. Axiom algebraic : integralRange (@ratr unitRingType). @@ -446,6 +445,11 @@ rewrite -(fmorph_root CtoL_rmorphism) -map_poly_comp; congr (root _ _): pu0. by apply/esym/eq_map_poly; apply: fmorph_eq_rat. Qed. +Program Definition conjMixin := + ImaginaryMixin (svalP (imaginary_exists closedFieldType)) + (fun x => esym (normK x)). +Canonical numClosedFieldType := NumClosedFieldType type conjMixin. + End Implementation. Definition divisor := Implementation.type. @@ -464,47 +468,7 @@ Local Notation ZtoC := (intr : int -> algC). Local Notation Creal := (Num.real : qualifier 0 algC). Fact algCi_subproof : {i : algC | i ^+ 2 = -1}. -Proof. exact: imaginary_exists. Qed. - -Let Re2 z := z + z^*. -Definition nnegIm z := 0 <= sval algCi_subproof * (z^* - z). -Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z <= Re2 y). - -CoInductive rootC_spec n (x : algC) : Type := - RootCspec (y : algC) of if (n > 0)%N then y ^+ n = x else y = 0 - & forall z, (n > 0)%N -> z ^+ n = x -> argCle y z. - -Fact rootC_subproof n x : rootC_spec n x. -Proof. -have realRe2 u : Re2 u \is Creal. - rewrite realEsqr expr2 {2}/Re2 -{2}[u]conjK addrC -rmorphD -normK. - by rewrite exprn_ge0 ?normr_ge0. -have argCtotal : total argCle. - move=> u v; rewrite /total /argCle. - by do 2!case: (nnegIm _) => //; rewrite ?orbT //= real_leVge. -have argCtrans : transitive argCle. - move=> u v w /implyP geZuv /implyP geZvw; apply/implyP. - by case/geZvw/andP=> /geZuv/andP[-> geRuv] /ler_trans->. -pose p := 'X^n - (x *+ (n > 0))%:P; have [r0 Dp] := closed_field_poly_normal p. -have sz_p: size p = n.+1. - rewrite size_addl ?size_polyXn // ltnS size_opp size_polyC mulrn_eq0. - by case: posnP => //; case: negP. -pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. -have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P). - rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. - rewrite subr0 eqxx scale1r; apply: eq_big_perm. - by rewrite perm_eq_sym perm_sort. -have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). - move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0. - by rewrite subr_eq0; apply: eqP. -exists r`_0 => [|z n_gt0 /(mem_rP z n_gt0) r_z]. - have sz_r: size r = n by apply: succn_inj; rewrite -sz_p Dp size_prod_XsubC. - case: posnP => [n0 | n_gt0]; first by rewrite nth_default // sz_r n0. - by apply/mem_rP=> //; rewrite mem_nth ?sz_r. -case: {Dp mem_rP}r r_z r_arg => // y r1; rewrite inE => /predU1P[-> _|r1z]. - by apply/implyP=> ->; rewrite lerr. -by move/(order_path_min argCtrans)/allP->. -Qed. +Proof. exact: GRing.imaginary_exists. Qed. CoInductive getCrat_spec : Type := GetCrat_spec CtoQ of cancel QtoC CtoQ. @@ -559,13 +523,10 @@ Module Import Exports. Import Implementation Internals. Notation algC := type. -Notation conjC := conj. Delimit Scope C_scope with C. Delimit Scope C_core_scope with Cc. Delimit Scope C_expanded_scope with Cx. Open Scope C_core_scope. -Notation "x ^*" := (conjC x) (at level 2, format "x ^*") : C_core_scope. -Notation "x ^*" := x^* (only parsing) : C_scope. Canonical eqType. Canonical choiceType. @@ -583,6 +544,7 @@ Canonical fieldType. Canonical numFieldType. Canonical decFieldType. Canonical closedFieldType. +Canonical numClosedFieldType. Notation algCeq := eqType. Notation algCzmod := zmodType. @@ -591,22 +553,7 @@ Notation algCuring := unitRingType. Notation algCnum := numDomainType. Notation algCfield := fieldType. Notation algCnumField := numFieldType. - -Definition rootC n x := let: RootCspec y _ _ := rootC_subproof n x in y. -Notation "n .-root" := (rootC n) (at level 2, format "n .-root") : C_core_scope. -Notation "n .-root" := (rootC n) (only parsing) : C_scope. -Notation sqrtC := 2.-root. - -Definition algCi := sqrtC (-1). -Notation "'i" := algCi (at level 0) : C_core_scope. -Notation "'i" := 'i (only parsing) : C_scope. - -Definition algRe x := (x + x^*) / 2%:R. -Definition algIm x := 'i * (x^* - x) / 2%:R. -Notation "'Re z" := (algRe z) (at level 10, z at level 8) : C_core_scope. -Notation "'Im z" := (algIm z) (at level 10, z at level 8) : C_core_scope. -Notation "'Re z" := ('Re z) (only parsing) : C_scope. -Notation "'Im z" := ('Im z) (only parsing) : C_scope. +Notation algCnumClosedField := numClosedFieldType. Notation Creal := (@Num.Def.Rreal numDomainType). @@ -692,596 +639,27 @@ Let nz2 : 2%:R != 0 :> algC. Proof. by rewrite -!CintrE. Qed. (* Conjugation and norm. *) -Definition conjCK : involutive conjC := Algebraics.Implementation.conjK. -Definition normCK x : `|x| ^+ 2 = x * x^* := Algebraics.Implementation.normK x. Definition algC_algebraic x := Algebraics.Implementation.algebraic x. -Lemma normCKC x : `|x| ^+ 2 = x^* * x. Proof. by rewrite normCK mulrC. Qed. - -Lemma mul_conjC_ge0 x : 0 <= x * x^*. -Proof. by rewrite -normCK exprn_ge0 ?normr_ge0. Qed. - -Lemma mul_conjC_gt0 x : (0 < x * x^*) = (x != 0). -Proof. -have [->|x_neq0] := altP eqP; first by rewrite rmorph0 mulr0. -by rewrite -normCK exprn_gt0 ?normr_gt0. -Qed. - -Lemma mul_conjC_eq0 x : (x * x^* == 0) = (x == 0). -Proof. by rewrite -normCK expf_eq0 normr_eq0. Qed. - -Lemma conjC_ge0 x : (0 <= x^*) = (0 <= x). -Proof. -wlog suffices: x / 0 <= x -> 0 <= x^*. - by move=> IH; apply/idP/idP=> /IH; rewrite ?conjCK. -rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite rmorph0. -by rewrite -(pmulr_rge0 _ x_gt0) mul_conjC_ge0. -Qed. - -Lemma conjC_nat n : (n%:R)^* = n%:R. Proof. exact: rmorph_nat. Qed. -Lemma conjC0 : 0^* = 0. Proof. exact: rmorph0. Qed. -Lemma conjC1 : 1^* = 1. Proof. exact: rmorph1. Qed. -Lemma conjC_eq0 x : (x^* == 0) = (x == 0). Proof. exact: fmorph_eq0. Qed. - -Lemma invC_norm x : x^-1 = `|x| ^- 2 * x^*. -Proof. -have [-> | nx_x] := eqVneq x 0; first by rewrite conjC0 mulr0 invr0. -by rewrite normCK invfM divfK ?conjC_eq0. -Qed. - (* Real number subset. *) Lemma Creal0 : 0 \is Creal. Proof. exact: rpred0. Qed. Lemma Creal1 : 1 \is Creal. Proof. exact: rpred1. Qed. Hint Resolve Creal0 Creal1. (* Trivial cannot resolve a general real0 hint. *) -Lemma CrealE x : (x \is Creal) = (x^* == x). -Proof. -rewrite realEsqr ger0_def normrX normCK. -by have [-> | /mulfI/inj_eq-> //] := eqVneq x 0; rewrite rmorph0 !eqxx. -Qed. - -Lemma CrealP {x} : reflect (x^* = x) (x \is Creal). -Proof. by rewrite CrealE; apply: eqP. Qed. - -Lemma conj_Creal x : x \is Creal -> x^* = x. -Proof. by move/CrealP. Qed. - -Lemma conj_normC z : `|z|^* = `|z|. -Proof. by rewrite conj_Creal ?normr_real. Qed. - -Lemma geC0_conj x : 0 <= x -> x^* = x. -Proof. by move=> /ger0_real/CrealP. Qed. - -Lemma geC0_unit_exp x n : 0 <= x -> (x ^+ n.+1 == 1) = (x == 1). -Proof. by move=> x_ge0; rewrite pexpr_eq1. Qed. - -(* Elementary properties of roots. *) - -Ltac case_rootC := rewrite /rootC; case: (rootC_subproof _ _). - -Lemma root0C x : 0.-root x = 0. Proof. by case_rootC. Qed. - -Lemma rootCK n : (n > 0)%N -> cancel n.-root (fun x => x ^+ n). -Proof. by case: n => //= n _ x; case_rootC. Qed. - -Lemma root1C x : 1.-root x = x. Proof. exact: (@rootCK 1). Qed. - -Lemma rootC0 n : n.-root 0 = 0. -Proof. -have [-> | n_gt0] := posnP n; first by rewrite root0C. -by have /eqP := rootCK n_gt0 0; rewrite expf_eq0 n_gt0 /= => /eqP. -Qed. - -Lemma rootC_inj n : (n > 0)%N -> injective n.-root. -Proof. by move/rootCK/can_inj. Qed. - -Lemma eqr_rootC n : (n > 0)%N -> {mono n.-root : x y / x == y}. -Proof. by move/rootC_inj/inj_eq. Qed. - -Lemma rootC_eq0 n x : (n > 0)%N -> (n.-root x == 0) = (x == 0). -Proof. by move=> n_gt0; rewrite -{1}(rootC0 n) eqr_rootC. Qed. - -(* Rectangular coordinates. *) - -Lemma sqrCi : 'i ^+ 2 = -1. Proof. exact: rootCK. Qed. - -Lemma nonRealCi : 'i \isn't Creal. -Proof. by rewrite realEsqr sqrCi oppr_ge0 ltr_geF ?ltr01. Qed. - -Lemma neq0Ci : 'i != 0. -Proof. by apply: contraNneq nonRealCi => ->; apply: real0. Qed. - -Lemma normCi : `|'i| = 1. -Proof. -apply/eqP; rewrite -(@pexpr_eq1 _ _ 2) ?normr_ge0 //. -by rewrite -normrX sqrCi normrN1. -Qed. - -Lemma invCi : 'i^-1 = - 'i. -Proof. by rewrite -div1r -[1]opprK -sqrCi mulNr mulfK ?neq0Ci. Qed. - -Lemma conjCi : 'i^* = - 'i. -Proof. by rewrite -invCi invC_norm normCi expr1n invr1 mul1r. Qed. - Lemma algCrect x : x = 'Re x + 'i * 'Im x. -Proof. -rewrite 2!mulrA -expr2 sqrCi mulN1r opprB -mulrDl addrACA subrr addr0. -by rewrite -mulr2n -mulr_natr mulfK. -Qed. - -Lemma Creal_Re x : 'Re x \is Creal. -Proof. by rewrite CrealE fmorph_div rmorph_nat rmorphD conjCK addrC. Qed. - -Lemma Creal_Im x : 'Im x \is Creal. -Proof. -rewrite CrealE fmorph_div rmorph_nat rmorphM rmorphB conjCK. -by rewrite conjCi -opprB mulrNN. -Qed. -Hint Resolve Creal_Re Creal_Im. - -Fact algRe_is_additive : additive algRe. -Proof. by move=> x y; rewrite /algRe rmorphB addrACA -opprD mulrBl. Qed. -Canonical algRe_additive := Additive algRe_is_additive. - -Fact algIm_is_additive : additive algIm. -Proof. -by move=> x y; rewrite /algIm rmorphB opprD addrACA -opprD mulrBr mulrBl. -Qed. -Canonical algIm_additive := Additive algIm_is_additive. - -Lemma Creal_ImP z : reflect ('Im z = 0) (z \is Creal). -Proof. -rewrite CrealE -subr_eq0 -(can_eq (mulKf neq0Ci)) mulr0. -by rewrite -(can_eq (divfK nz2)) mul0r; apply: eqP. -Qed. - -Lemma Creal_ReP z : reflect ('Re z = z) (z \in Creal). -Proof. -rewrite (sameP (Creal_ImP z) eqP) -(can_eq (mulKf neq0Ci)) mulr0. -by rewrite -(inj_eq (addrI ('Re z))) addr0 -algCrect eq_sym; apply: eqP. -Qed. - -Lemma algReMl : {in Creal, forall x, {morph algRe : z / x * z}}. -Proof. -by move=> x Rx z /=; rewrite /algRe rmorphM (conj_Creal Rx) -mulrDr -mulrA. -Qed. - -Lemma algReMr : {in Creal, forall x, {morph algRe : z / z * x}}. -Proof. by move=> x Rx z /=; rewrite mulrC algReMl // mulrC. Qed. - -Lemma algImMl : {in Creal, forall x, {morph algIm : z / x * z}}. -Proof. -by move=> x Rx z; rewrite /algIm rmorphM (conj_Creal Rx) -mulrBr mulrCA !mulrA. -Qed. - -Lemma algImMr : {in Creal, forall x, {morph algIm : z / z * x}}. -Proof. by move=> x Rx z /=; rewrite mulrC algImMl // mulrC. Qed. - -Lemma algRe_i : 'Re 'i = 0. Proof. by rewrite /algRe conjCi subrr mul0r. Qed. - -Lemma algIm_i : 'Im 'i = 1. -Proof. -rewrite /algIm conjCi -opprD mulrN -mulr2n mulrnAr ['i * _]sqrCi. -by rewrite mulNrn opprK divff. -Qed. - -Lemma algRe_conj z : 'Re z^* = 'Re z. -Proof. by rewrite /algRe addrC conjCK. Qed. - -Lemma algIm_conj z : 'Im z^* = - 'Im z. -Proof. by rewrite /algIm -mulNr -mulrN opprB conjCK. Qed. - -Lemma algRe_rect : {in Creal &, forall x y, 'Re (x + 'i * y) = x}. -Proof. -move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ReP x Rx). -by rewrite algReMr // algRe_i mul0r addr0. -Qed. - -Lemma algIm_rect : {in Creal &, forall x y, 'Im (x + 'i * y) = y}. -Proof. -move=> x y Rx Ry; rewrite /= raddfD /= (Creal_ImP x Rx) add0r. -by rewrite algImMr // algIm_i mul1r. -Qed. - -Lemma conjC_rect : {in Creal &, forall x y, (x + 'i * y)^* = x - 'i * y}. -Proof. -by move=> x y Rx Ry; rewrite /= rmorphD rmorphM conjCi mulNr !conj_Creal. -Qed. +Proof. by rewrite [LHS]Crect. Qed. -Lemma addC_rect x1 y1 x2 y2 : - (x1 + 'i * y1) + (x2 + 'i * y2) = x1 + x2 + 'i * (y1 + y2). -Proof. by rewrite addrACA -mulrDr. Qed. +Lemma algCreal_Re x : 'Re x \is Creal. +Proof. by rewrite Creal_Re. Qed. -Lemma oppC_rect x y : - (x + 'i * y) = - x + 'i * (- y). -Proof. by rewrite mulrN -opprD. Qed. - -Lemma subC_rect x1 y1 x2 y2 : - (x1 + 'i * y1) - (x2 + 'i * y2) = x1 - x2 + 'i * (y1 - y2). -Proof. by rewrite oppC_rect addC_rect. Qed. - -Lemma mulC_rect x1 y1 x2 y2 : - (x1 + 'i * y1) * (x2 + 'i * y2) - = x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1). -Proof. -rewrite mulrDl !mulrDr mulrCA -!addrA mulrAC -mulrA; congr (_ + _). -by rewrite mulrACA -expr2 sqrCi mulN1r addrA addrC. -Qed. - -Lemma normC2_rect : - {in Creal &, forall x y, `|x + 'i * y| ^+ 2 = x ^+ 2 + y ^+ 2}. -Proof. -move=> x y Rx Ry; rewrite /= normCK rmorphD rmorphM conjCi !conj_Creal //. -by rewrite mulrC mulNr -subr_sqr exprMn sqrCi mulN1r opprK. -Qed. - -Lemma normC2_Re_Im z : `|z| ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2. -Proof. by rewrite -normC2_rect -?algCrect. Qed. - -Lemma invC_rect : - {in Creal &, forall x y, (x + 'i * y)^-1 = (x - 'i * y) / (x ^+ 2 + y ^+ 2)}. -Proof. -by move=> x y Rx Ry; rewrite /= invC_norm conjC_rect // mulrC normC2_rect. -Qed. - -Lemma lerif_normC_Re_Creal z : `|'Re z| <= `|z| ?= iff (z \is Creal). -Proof. -rewrite -(mono_in_lerif ler_sqr); try by rewrite qualifE normr_ge0. -rewrite normCK conj_Creal // normC2_Re_Im -expr2. -rewrite addrC -lerif_subLR subrr (sameP (Creal_ImP _) eqP) -sqrf_eq0 eq_sym. -by apply: lerif_eq; rewrite -realEsqr. -Qed. - -Lemma lerif_Re_Creal z : 'Re z <= `|z| ?= iff (0 <= z). -Proof. -have ubRe: 'Re z <= `|'Re z| ?= iff (0 <= 'Re z). - by rewrite ger0_def eq_sym; apply/lerif_eq/real_ler_norm. -congr (_ <= _ ?= iff _): (lerif_trans ubRe (lerif_normC_Re_Creal z)). -apply/andP/idP=> [[zRge0 /Creal_ReP <- //] | z_ge0]. -by have Rz := ger0_real z_ge0; rewrite (Creal_ReP _ _). -Qed. - -(* Equality from polar coordinates, for the upper plane. *) -Lemma eqC_semipolar x y : - `|x| = `|y| -> 'Re x = 'Re y -> 0 <= 'Im x * 'Im y -> x = y. -Proof. -move=> eq_norm eq_Re sign_Im. -rewrite [x]algCrect [y]algCrect eq_Re; congr (_ + 'i * _). -have /eqP := congr1 (fun z => z ^+ 2) eq_norm. -rewrite !normC2_Re_Im eq_Re (can_eq (addKr _)) eqf_sqr => /pred2P[] // eq_Im. -rewrite eq_Im mulNr -expr2 oppr_ge0 real_exprn_even_le0 //= in sign_Im. -by rewrite eq_Im (eqP sign_Im) oppr0. -Qed. - -(* Nth roots. *) - -Let argCleP y z : - reflect (0 <= 'Im z -> 0 <= 'Im y /\ 'Re z <= 'Re y) (argCle y z). -Proof. -suffices dIm x: nnegIm x = (0 <= 'Im x). - rewrite /argCle !dIm ler_pmul2r ?invr_gt0 ?ltr0n //. - by apply: (iffP implyP) => geZyz /geZyz/andP. -rewrite /('Im x) pmulr_lge0 ?invr_gt0 ?ltr0n //; congr (0 <= _ * _). -case Du: algCi_subproof => [u u2N1] /=. -have/eqP := u2N1; rewrite -sqrCi eqf_sqr => /pred2P[] //. -have:= conjCi; rewrite /'i; case_rootC => /= v v2n1 min_v conj_v Duv. -have{min_v} /idPn[] := min_v u isT u2N1; rewrite negb_imply /nnegIm Du /= Duv. -rewrite rmorphN conj_v opprK -opprD mulrNN mulNr -mulr2n mulrnAr -expr2 v2n1. -by rewrite mulNrn opprK ler0n oppr_ge0 (leC_nat 2 0). -Qed. - -Lemma rootC_Re_max n x y : - (n > 0)%N -> y ^+ n = x -> 0 <= 'Im y -> 'Re y <= 'Re (n.-root%C x). -Proof. -by move=> n_gt0 yn_x leI0y; case_rootC=> z /= _ /(_ y n_gt0 yn_x)/argCleP[]. -Qed. - -Let neg_unity_root n : (n > 1)%N -> exists2 w : algC, w ^+ n = 1 & 'Re w < 0. -Proof. -move=> n_gt1; have [|w /eqP pw_0] := closed_rootP (\poly_(i < n) (1 : algC)) _. - by rewrite size_poly_eq ?oner_eq0 // -(subnKC n_gt1). -rewrite horner_poly (eq_bigr _ (fun _ _ => mul1r _)) in pw_0. -have wn1: w ^+ n = 1 by apply/eqP; rewrite -subr_eq0 subrX1 pw_0 mulr0. -suffices /existsP[i ltRwi0]: [exists i : 'I_n, 'Re (w ^+ i) < 0]. - by exists (w ^+ i) => //; rewrite exprAC wn1 expr1n. -apply: contra_eqT (congr1 algRe pw_0); rewrite negb_exists => /forallP geRw0. -rewrite raddf_sum raddf0 /= (bigD1 (Ordinal (ltnW n_gt1))) //=. -rewrite (Creal_ReP _ _) ?rpred1 // gtr_eqF ?ltr_paddr ?ltr01 //=. -by apply: sumr_ge0 => i _; rewrite real_lerNgt. -Qed. - -Lemma Im_rootC_ge0 n x : (n > 1)%N -> 0 <= 'Im (n.-root x). -Proof. -set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1. -apply: wlog_neg; rewrite -real_ltrNge // => ltIy0. -suffices [z zn_x leI0z]: exists2 z, z ^+ n = x & 'Im z >= 0. - by rewrite /y; case_rootC => /= y1 _ /(_ z n_gt0 zn_x)/argCleP[]. -have [w wn1 ltRw0] := neg_unity_root n_gt1. -wlog leRI0yw: w wn1 ltRw0 / 0 <= 'Re y * 'Im w. - move=> IHw; have: 'Re y * 'Im w \is Creal by rewrite rpredM. - case/real_ger0P=> [|/ltrW leRIyw0]; first exact: IHw. - apply: (IHw w^*); rewrite ?algRe_conj ?algIm_conj ?mulrN ?oppr_ge0 //. - by rewrite -rmorphX wn1 rmorph1. -exists (w * y); first by rewrite exprMn wn1 mul1r rootCK. -rewrite [w]algCrect [y]algCrect mulC_rect. -by rewrite algIm_rect ?rpredD ?rpredN 1?rpredM // addr_ge0 // ltrW ?nmulr_rgt0. -Qed. - -Lemma rootC_lt0 n x : (1 < n)%N -> (n.-root x < 0) = false. -Proof. -set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1. -apply: negbTE; apply: wlog_neg => /negbNE lt0y; rewrite ler_gtF //. -have Rx: x \is Creal by rewrite -[x](rootCK n_gt0) rpredX // ltr0_real. -have Re_y: 'Re y = y by apply/Creal_ReP; rewrite ltr0_real. -have [z zn_x leR0z]: exists2 z, z ^+ n = x & 'Re z >= 0. - have [w wn1 ltRw0] := neg_unity_root n_gt1. - exists (w * y); first by rewrite exprMn wn1 mul1r rootCK. - by rewrite algReMr ?ltr0_real // ltrW // nmulr_lgt0. -without loss leI0z: z zn_x leR0z / 'Im z >= 0. - move=> IHz; have: 'Im z \is Creal by []. - case/real_ger0P=> [|/ltrW leIz0]; first exact: IHz. - apply: (IHz z^*); rewrite ?algRe_conj ?algIm_conj ?oppr_ge0 //. - by rewrite -rmorphX zn_x conj_Creal. -by apply: ler_trans leR0z _; rewrite -Re_y ?rootC_Re_max ?ltr0_real. -Qed. - -Lemma rootC_ge0 n x : (n > 0)%N -> (0 <= n.-root x) = (0 <= x). -Proof. -set y := n.-root x => n_gt0. -apply/idP/idP=> [/(exprn_ge0 n) | x_ge0]; first by rewrite rootCK. -rewrite -(ger_lerif (lerif_Re_Creal y)). -have Ray: `|y| \is Creal by apply: normr_real. -rewrite -(Creal_ReP _ Ray) rootC_Re_max ?(Creal_ImP _ Ray) //. -by rewrite -normrX rootCK // ger0_norm. -Qed. - -Lemma rootC_gt0 n x : (n > 0)%N -> (n.-root x > 0) = (x > 0). -Proof. by move=> n_gt0; rewrite !lt0r rootC_ge0 ?rootC_eq0. Qed. - -Lemma rootC_le0 n x : (1 < n)%N -> (n.-root x <= 0) = (x == 0). -Proof. -by move=> n_gt1; rewrite ler_eqVlt rootC_lt0 // orbF rootC_eq0 1?ltnW. -Qed. - -Lemma ler_rootCl n : (n > 0)%N -> {in Num.nneg, {mono n.-root : x y / x <= y}}. -Proof. -move=> n_gt0 x x_ge0 y; have [y_ge0 | not_y_ge0] := boolP (0 <= y). - by rewrite -(ler_pexpn2r n_gt0) ?qualifE ?rootC_ge0 ?rootCK. -rewrite (contraNF (@ler_trans _ _ 0 _ _)) ?rootC_ge0 //. -by rewrite (contraNF (ler_trans x_ge0)). -Qed. - -Lemma ler_rootC n : (n > 0)%N -> {in Num.nneg &, {mono n.-root : x y / x <= y}}. -Proof. by move=> n_gt0 x y x_ge0 _; apply: ler_rootCl. Qed. - -Lemma ltr_rootCl n : (n > 0)%N -> {in Num.nneg, {mono n.-root : x y / x < y}}. -Proof. by move=> n_gt0 x x_ge0 y; rewrite !ltr_def ler_rootCl ?eqr_rootC. Qed. - -Lemma ltr_rootC n : (n > 0)%N -> {in Num.nneg &, {mono n.-root : x y / x < y}}. -Proof. by move/ler_rootC/lerW_mono_in. Qed. - -Lemma exprCK n x : (0 < n)%N -> 0 <= x -> n.-root (x ^+ n) = x. -Proof. -move=> n_gt0 x_ge0; apply/eqP. -by rewrite -(eqr_expn2 n_gt0) ?rootC_ge0 ?exprn_ge0 ?rootCK. -Qed. - -Lemma norm_rootC n x : `|n.-root x| = n.-root `|x|. -Proof. -have [-> | n_gt0] := posnP n; first by rewrite !root0C normr0. -apply/eqP; rewrite -(eqr_expn2 n_gt0) ?rootC_ge0 ?normr_ge0 //. -by rewrite -normrX !rootCK. -Qed. - -Lemma rootCX n x k : (n > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k. -Proof. -move=> n_gt0 x_ge0; apply/eqP. -by rewrite -(eqr_expn2 n_gt0) ?(exprn_ge0, rootC_ge0) // 1?exprAC !rootCK. -Qed. - -Lemma rootC1 n : (n > 0)%N -> n.-root 1 = 1. -Proof. by move/(rootCX 0)/(_ ler01). Qed. - -Lemma rootCpX n x k : (k > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k. -Proof. -by case: n => [|n] k_gt0; [rewrite !root0C expr0n gtn_eqF | apply: rootCX]. -Qed. - -Lemma rootCV n x : (n > 0)%N -> 0 <= x -> n.-root x^-1 = (n.-root x)^-1. -Proof. -move=> n_gt0 x_ge0; apply/eqP. -by rewrite -(eqr_expn2 n_gt0) ?(invr_ge0, rootC_ge0) // !exprVn !rootCK. -Qed. - -Lemma rootC_eq1 n x : (n > 0)%N -> (n.-root x == 1) = (x == 1). -Proof. by move=> n_gt0; rewrite -{1}(rootC1 n_gt0) eqr_rootC. Qed. - -Lemma rootC_ge1 n x : (n > 0)%N -> (n.-root x >= 1) = (x >= 1). -Proof. -by move=> n_gt0; rewrite -{1}(rootC1 n_gt0) ler_rootCl // qualifE ler01. -Qed. - -Lemma rootC_gt1 n x : (n > 0)%N -> (n.-root x > 1) = (x > 1). -Proof. by move=> n_gt0; rewrite !ltr_def rootC_eq1 ?rootC_ge1. Qed. - -Lemma rootC_le1 n x : (n > 0)%N -> 0 <= x -> (n.-root x <= 1) = (x <= 1). -Proof. by move=> n_gt0 x_ge0; rewrite -{1}(rootC1 n_gt0) ler_rootCl. Qed. - -Lemma rootC_lt1 n x : (n > 0)%N -> 0 <= x -> (n.-root x < 1) = (x < 1). -Proof. by move=> n_gt0 x_ge0; rewrite !ltr_neqAle rootC_eq1 ?rootC_le1. Qed. - -Lemma rootCMl n x z : 0 <= x -> n.-root (x * z) = n.-root x * n.-root z. -Proof. -rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite !(mul0r, rootC0). -have [| n_gt1 | ->] := ltngtP n 1; last by rewrite !root1C. - by case: n => //; rewrite !root0C mul0r. -have [x_ge0 n_gt0] := (ltrW x_gt0, ltnW n_gt1). -have nx_gt0: 0 < n.-root x by rewrite rootC_gt0. -have Rnx: n.-root x \is Creal by rewrite ger0_real ?ltrW. -apply: eqC_semipolar; last 1 first; try apply/eqP. -- by rewrite algImMl // !(Im_rootC_ge0, mulr_ge0, rootC_ge0). -- by rewrite -(eqr_expn2 n_gt0) ?normr_ge0 // -!normrX exprMn !rootCK. -rewrite eqr_le; apply/andP; split; last first. - rewrite rootC_Re_max ?exprMn ?rootCK ?algImMl //. - by rewrite mulr_ge0 ?Im_rootC_ge0 ?ltrW. -rewrite -[n.-root _](mulVKf (negbT (gtr_eqF nx_gt0))) !(algReMl Rnx) //. -rewrite ler_pmul2l // rootC_Re_max ?exprMn ?exprVn ?rootCK ?mulKf ?gtr_eqF //. -by rewrite algImMl ?rpredV // mulr_ge0 ?invr_ge0 ?Im_rootC_ge0 ?ltrW. -Qed. - -Lemma rootCMr n x z : 0 <= x -> n.-root (z * x) = n.-root z * n.-root x. -Proof. by move=> x_ge0; rewrite mulrC rootCMl // mulrC. Qed. - -(* More properties of n.-root will be established in cyclotomic.v. *) - -(* The proper form of the Arithmetic - Geometric Mean inequality. *) - -Lemma lerif_rootC_AGM (I : finType) (A : pred I) (n := #|A|) E : - {in A, forall i, 0 <= E i} -> - n.-root (\prod_(i in A) E i) <= (\sum_(i in A) E i) / n%:R - ?= iff [forall i in A, forall j in A, E i == E j]. -Proof. -move=> Ege0; have [n0 | n_gt0] := posnP n. - rewrite n0 root0C invr0 mulr0; apply/lerif_refl/forall_inP=> i. - by rewrite (card0_eq n0). -rewrite -(mono_in_lerif (ler_pexpn2r n_gt0)) ?rootCK //=; first 1 last. -- by rewrite qualifE rootC_ge0 // prodr_ge0. -- by rewrite rpred_div ?rpred_nat ?rpred_sum. -exact: lerif_AGM. -Qed. - -(* Square root. *) - -Lemma sqrtC0 : sqrtC 0 = 0. Proof. exact: rootC0. Qed. -Lemma sqrtC1 : sqrtC 1 = 1. Proof. exact: rootC1. Qed. -Lemma sqrtCK x : sqrtC x ^+ 2 = x. Proof. exact: rootCK. Qed. -Lemma sqrCK x : 0 <= x -> sqrtC (x ^+ 2) = x. Proof. exact: exprCK. Qed. - -Lemma sqrtC_ge0 x : (0 <= sqrtC x) = (0 <= x). Proof. exact: rootC_ge0. Qed. -Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0). Proof. exact: rootC_eq0. Qed. -Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0). Proof. exact: rootC_gt0. Qed. -Lemma sqrtC_lt0 x : (sqrtC x < 0) = false. Proof. exact: rootC_lt0. Qed. -Lemma sqrtC_le0 x : (sqrtC x <= 0) = (x == 0). Proof. exact: rootC_le0. Qed. - -Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x <= y}}. -Proof. exact: ler_rootC. Qed. -Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y}}. -Proof. exact: ltr_rootC. Qed. -Lemma eqr_sqrtC : {mono sqrtC : x y / x == y}. -Proof. exact: eqr_rootC. Qed. -Lemma sqrtC_inj : injective sqrtC. -Proof. exact: rootC_inj. Qed. -Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x * y}}. -Proof. by move=> x y _; apply: rootCMr. Qed. - -Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 <= 'Im x) && ~~ (x < 0)). -Proof. -apply: (iffP andP) => [[leI0x not_gt0x] | <-]; last first. - by rewrite sqrtC_lt0 Im_rootC_ge0. -have /eqP := sqrtCK (x ^+ 2); rewrite eqf_sqr => /pred2P[] // defNx. -apply: sqrCK; rewrite -real_lerNgt // in not_gt0x; apply/Creal_ImP/ler_anti; -by rewrite leI0x -oppr_ge0 -raddfN -defNx Im_rootC_ge0. -Qed. - -Lemma normC_def x : `|x| = sqrtC (x * x^*). -Proof. by rewrite -normCK sqrCK ?normr_ge0. Qed. - -Lemma norm_conjC x : `|x^*| = `|x|. -Proof. by rewrite !normC_def conjCK mulrC. Qed. - -Lemma normC_rect : - {in Creal &, forall x y, `|x + 'i * y| = sqrtC (x ^+ 2 + y ^+ 2)}. -Proof. by move=> x y Rx Ry; rewrite /= normC_def -normCK normC2_rect. Qed. - -Lemma normC_Re_Im z : `|z| = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2). -Proof. by rewrite normC_def -normCK normC2_Re_Im. Qed. - -(* Norm sum (in)equalities. *) - -Lemma normC_add_eq x y : - `|x + y| = `|x| + `|y| -> - {t : algC | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}. -Proof. -move=> lin_xy; apply: sig2_eqW; pose u z := if z == 0 then 1 else z / `|z|. -have uE z: (`|u z| = 1) * (`|z| * u z = z). - rewrite /u; have [->|nz_z] := altP eqP; first by rewrite normr0 normr1 mul0r. - by rewrite normf_div normr_id mulrCA divff ?mulr1 ?normr_eq0. -have [->|nz_x] := eqVneq x 0; first by exists (u y); rewrite uE ?normr0 ?mul0r. -exists (u x); rewrite uE // /u (negPf nz_x); congr (_ , _). -have{lin_xy} def2xy: `|x| * `|y| *+ 2 = x * y ^* + y * x ^*. - apply/(addrI (x * x^*))/(addIr (y * y^*)); rewrite -2!{1}normCK -sqrrD. - by rewrite addrA -addrA -!mulrDr -mulrDl -rmorphD -normCK lin_xy. -have def_xy: x * y^* = y * x^*. - apply/eqP; rewrite -subr_eq0 -[_ == 0](@expf_eq0 _ _ 2). - rewrite (canRL (subrK _) (subr_sqrDB _ _)) opprK -def2xy exprMn_n exprMn. - by rewrite mulrN mulrAC mulrA -mulrA mulrACA -!normCK mulNrn addNr. -have{def_xy def2xy} def_yx: `|y * x| = y * x^*. - by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy. -rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM. -by rewrite mulrCA divfK ?normr_eq0 // mulrAC mulrA. -Qed. - -Lemma normC_sum_eq (I : finType) (P : pred I) (F : I -> algC) : - `|\sum_(i | P i) F i| = \sum_(i | P i) `|F i| -> - {t : algC | `|t| == 1 & forall i, P i -> F i = `|F i| * t}. -Proof. -have [i /andP[Pi nzFi] | F0] := pickP [pred i | P i & F i != 0]; last first. - exists 1 => [|i Pi]; first by rewrite normr1. - by case/nandP: (F0 i) => [/negP[]// | /negbNE/eqP->]; rewrite normr0 mul0r. -rewrite !(bigD1 i Pi) /= => norm_sumF; pose Q j := P j && (j != i). -rewrite -normr_eq0 in nzFi; set c := F i / `|F i|; exists c => [|j Pj]. - by rewrite normrM normfV normr_id divff. -have [Qj | /nandP[/negP[]// | /negbNE/eqP->]] := boolP (Q j); last first. - by rewrite mulrC divfK. -have: `|F i + F j| = `|F i| + `|F j|. - do [rewrite !(bigD1 j Qj) /=; set z := \sum_(k | _) `|_|] in norm_sumF. - apply/eqP; rewrite eqr_le ler_norm_add -(ler_add2r z) -addrA -norm_sumF addrA. - by rewrite (ler_trans (ler_norm_add _ _)) // ler_add2l ler_norm_sum. -by case/normC_add_eq=> k _ [/(canLR (mulKf nzFi)) <-]; rewrite -(mulrC (F i)). -Qed. - -Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I -> algC) : - `|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) -> - (forall i, P i -> `|F i| = 1) -> - {t : algC | `|t| == 1 & forall i, P i -> F i = t}. -Proof. -case/normC_sum_eq=> t t1 defF normF. -by exists t => // i Pi; rewrite defF // normF // mul1r. -Qed. - -Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I -> algC) : - (forall i, P i -> `|F i| <= G i) -> - \sum_(i | P i) F i = \sum_(i | P i) G i -> - forall i, P i -> F i = G i. -Proof. -set sumF := \sum_(i | _) _; set sumG := \sum_(i | _) _ => leFG eq_sumFG. -have posG i: P i -> 0 <= G i by move/leFG; apply: ler_trans; apply: normr_ge0. -have norm_sumG: `|sumG| = sumG by rewrite ger0_norm ?sumr_ge0. -have norm_sumF: `|sumF| = \sum_(i | P i) `|F i|. - apply/eqP; rewrite eqr_le ler_norm_sum eq_sumFG norm_sumG -subr_ge0 -sumrB. - by rewrite sumr_ge0 // => i Pi; rewrite subr_ge0 ?leFG. -have [t _ defF] := normC_sum_eq norm_sumF. -have [/(psumr_eq0P posG) G0 i Pi | nz_sumG] := eqVneq sumG 0. - by apply/eqP; rewrite G0 // -normr_eq0 eqr_le normr_ge0 -(G0 i Pi) leFG. -have t1: t = 1. - apply: (mulfI nz_sumG); rewrite mulr1 -{1}norm_sumG -eq_sumFG norm_sumF. - by rewrite mulr_suml -(eq_bigr _ defF). -have /psumr_eq0P eqFG i: P i -> 0 <= G i - F i. - by move=> Pi; rewrite subr_ge0 defF // t1 mulr1 leFG. -move=> i /eqFG/(canRL (subrK _))->; rewrite ?add0r //. -by rewrite sumrB -/sumF eq_sumFG subrr. -Qed. - -Lemma normC_sub_eq x y : - `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}. -Proof. -rewrite -{-1}(subrK y x) => /(canLR (subrK _))/esym-Dx; rewrite Dx. -by have [t ? [Dxy Dy]] := normC_add_eq Dx; exists t; rewrite // mulrDl -Dxy -Dy. -Qed. +Lemma algCreal_Im x : 'Im x \is Creal. +Proof. by rewrite Creal_Im. Qed. +Hint Resolve algCreal_Re algCreal_Im. (* Integer subset. *) - (* Not relying on the undocumented interval library, for now. *) + Lemma floorC_itv x : x \is Creal -> (floorC x)%:~R <= x < (floorC x + 1)%:~R. Proof. by rewrite /floorC => Rx; case: (floorC_subproof x) => //= m; apply. Qed. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 5134a2f..4337327 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -259,12 +259,6 @@ by rewrite Dp map_monic; exists p; rewrite // -Dp root_minPoly. Qed. Prenex Implicits alg_integral. -Lemma imaginary_exists (C : closedFieldType) : {i : C | i ^+ 2 = -1}. -Proof. -have /sig_eqW[i Di2] := @solve_monicpoly C 2 (nth 0 [:: -1]) isT. -by exists i; rewrite Di2 big_ord_recl big_ord1 mul0r mulr1 !addr0. -Qed. - Import DefaultKeying GRing.DefaultPred. Implicit Arguments map_poly_inj [[F] [R] x1 x2]. @@ -275,7 +269,7 @@ Proof. have maxn3 n1 n2 n3: {m | [/\ n1 <= m, n2 <= m & n3 <= m]%N}. by exists (maxn n1 (maxn n2 n3)); apply/and3P; rewrite -!geq_max. have [C [/= QtoC algC]] := countable_algebraic_closure [countFieldType of rat]. -exists C; have [i Di2] := imaginary_exists C. +exists C; have [i Di2] := GRing.imaginary_exists C. pose Qfield := fieldExtType rat; pose Cmorph (L : Qfield) := {rmorphism L -> C}. have charQ (L : Qfield): [char L] =i pred0 := ftrans (char_lalg L) (char_num _). have sepQ (L : Qfield) (K E : {subfield L}): separable K E. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 01eea88..70553a0 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -232,7 +232,7 @@ Structure base_type : Type := PackBase { (* coercion of A * B to pred_sort in x \in A * B, or rho * tau to *) (* ffun and Funclass in (rho * tau) x, when rho tau : perm T. *) (* Therefore we define an alias of sort for argument types, and *) -(* make it the default coercion FinGroup.base_class >-> Sortclass *) +(* make it the default coercion FinGroup.base_type >-> Sortclass *) (* so that arguments of a functions whose parameters are of type, *) (* say, gT : finGroupType, can be coerced to the coercion class *) (* of arg_sort. Care should be taken, however, to declare the *) diff --git a/mathcomp/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v index a64c49a..16a0a3c 100644 --- a/mathcomp/odd_order/BGappendixC.v +++ b/mathcomp/odd_order/BGappendixC.v @@ -288,7 +288,7 @@ Proof. have [q_gt4 | q_le4] := ltnP 4 q. pose inK x := enum_rank_in (classes1 H) (x ^: H). have inK_E x: x \in H -> enum_val (inK x) = x ^: H. - by move=> Hx; rewrite enum_rankK_in ?mem_classes. + by move=> Hx; rewrite enum_rankK_in ?mem_classes. pose j := inK s; pose k := inK (s ^+ 2)%g; pose e := gring_classM_coef j j k. have cPP: abelian P by rewrite -(injm_abelian inj_sigma) ?zmod_abelian. have Hs: s \in H by rewrite -(sdprodW defH) -[s]mulg1 mem_mulg. @@ -355,18 +355,19 @@ have [q_gt4 | q_le4] := ltnP 4 q. by rewrite sub_cent1 groupX // (subsetP cPP). rewrite mulrnA -second_orthogonality_relation ?groupX // big_mkcond. by apply: ler_sum => i _; rewrite normCK; case: ifP; rewrite ?mul_conjC_ge0. - have sqrtP_gt0: 0 < sqrtC #|P|%:R by rewrite sqrtC_gt0 ?gt0CG. - have{De ub_linH'}: `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R. + have sqrtP_gt0: 0 < sqrtC #|P|%:R :> algC by rewrite sqrtC_gt0 ?gt0CG. + have{De ub_linH'}: + `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R :> algC. rewrite natrM De mulrCA mulrA divfK ?neq0CG // (bigID linH) /= sum_linH. rewrite mulrDr addrC addKr mulrC mulr_suml /chi_s2. rewrite (ler_trans (ler_norm_sum _ _ _)) // -ler_pdivr_mulr // mulr_suml. apply: ler_trans (ub_linH' 1%N isT); apply: ler_sum => i linH'i. rewrite ler_pdivr_mulr // degU ?divfK ?neq0CG //. rewrite normrM -normrX norm_conjC ler_wpmul2l ?normr_ge0 //. - rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK. + rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK. apply: ler_trans (ub_linH' 2 isT); rewrite (bigD1 i) ?ler_paddr //=. by apply: sumr_ge0 => i1 _; rewrite exprn_ge0 ?normr_ge0. - rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. + rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. rewrite -ltC_nat -(ltr_pmul2l (gt0CG P)) {lb_Pe}(ltr_le_trans _ lb_Pe) //. rewrite ltr_subr_addl (@ler_lt_trans _ ((p ^ q.-1)%:R ^+ 2)) //; last first. rewrite -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //. diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v index b966f25..3c4ec9f 100644 --- a/mathcomp/odd_order/PFsection11.v +++ b/mathcomp/odd_order/PFsection11.v @@ -232,7 +232,7 @@ Lemma bounded_proper_coherent H1 : (#|HU : H1| <= 2 * q * #|U : C| + 1)%N. Proof. move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU. -suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R. +suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC. rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM. congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)). rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC. diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index cb55ae4..9011122 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.v @@ -1360,7 +1360,7 @@ have{oxi_00} oxi_i0 i j i0: '[xi_ i j, xi_ i0 0] = ((i == i0) && (j == 0))%:R. by rewrite cfdotC Xi0_X0j // conjC0. have [-> | nzi2] := altP (i2 =P 0); first exact: oxi_0j. have [-> | nzj2] := altP (j2 =P 0); first exact: oxi_i0. -rewrite cfdotC eq_sym; apply: canLR conjCK _; rewrite rmorph_nat. +rewrite cfdotC eq_sym; apply: canLR (@conjCK _) _; rewrite rmorph_nat. have [-> | nzi1] := altP (i1 =P 0); first exact: oxi_0j. have [-> | nzj1] := altP (j1 =P 0); first exact: oxi_i0. have ->: xi_ i1 j1 = beta i1 j1 + xi_ i1 0 + xi_ 0 j1 by rewrite /xi_ !ifN. diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index d318f5f..3f90da7 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.v @@ -492,7 +492,7 @@ Definition subcoherent S tau R := (*c*) pairwise_orthogonal S, (*d*) {in S, forall xi : 'CF(L : {set gT}), [/\ {subset R xi <= 'Z[irr G]}, orthonormal (R xi) - & tau (xi - xi^*)%CF = \sum_(alpha <- R xi) alpha]} + & tau (xi - xi^*%CF) = \sum_(alpha <- R xi) alpha]} & (*e*) {in S &, forall xi phi : 'CF(L), orthogonal phi (xi :: xi^*%CF) -> orthogonal (R phi) (R xi)}]. @@ -621,7 +621,7 @@ have isoS1: {in S1, isometry [eta tau with eta1 |-> zeta1], to 'Z[irr G]}. split=> [xi eta | eta]; rewrite !in_cons /=; last first. by case: eqP => [-> | _ /isoS[/Ztau/zcharW]]. do 2!case: eqP => [-> _|_ /isoS[? ?]] //; last exact: Itau. - by apply/(can_inj conjCK); rewrite -!cfdotC. + by apply/(can_inj (@conjCK _)); rewrite -!cfdotC. have [nu Dnu IZnu] := Zisometry_of_iso freeS1 isoS1. exists nu; split=> // phi; rewrite zcharD1E => /andP[]. case/(zchar_expansion (free_uniq freeS1)) => b Zb {phi}-> phi1_0. @@ -646,7 +646,7 @@ have N_S: {subset S <= character} by move=> _ /irrS/irrP[i ->]; apply: irr_char. have Z_S: {subset S <= 'Z[irr L]} by move=> chi /N_S/char_vchar. have o1S: orthonormal S by apply: sub_orthonormal (irr_orthonormal L). have [[_ dotSS] oS] := (orthonormalP o1S, orthonormal_orthogonal o1S). -pose beta chi := tau (chi - chi^*)%CF; pose eqBP := _ =P beta _. +pose beta chi := tau (chi - chi^*%CF); pose eqBP := _ =P beta _. have Zbeta: {in S, forall chi, chi - (chi^*)%CF \in 'Z[S, L^#]}. move=> chi Schi; rewrite /= zcharD1E rpredB ?mem_zchar ?ccS //= !cfunE. by rewrite subr_eq0 conj_Cnat // Cnat_char1 ?N_S. @@ -885,7 +885,7 @@ Lemma subcoherent_norm chi psi (tau1 : {additive 'CF(L) -> 'CF(G)}) X Y : [/\ chi \in S, psi \in 'Z[irr L] & orthogonal (chi :: chi^*)%CF psi] -> let S0 := chi - psi :: chi - chi^*%CF in {in 'Z[S0], isometry tau1, to 'Z[irr G]} -> - tau1 (chi - chi^*)%CF = tau (chi - chi^*)%CF -> + tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) -> [/\ tau1 (chi - psi) = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)] -> [/\ (*a*) '[chi] <= '[X] & (*b*) '[psi] <= '[Y] -> diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v index 6d9ecfc..cbde798 100644 --- a/mathcomp/odd_order/PFsection6.v +++ b/mathcomp/odd_order/PFsection6.v @@ -83,13 +83,13 @@ Lemma coherent_seqIndD_bound (A B C D : {group gT}) : (*a*) [/\ A \proper K, B \subset D, D \subset C, C \subset K & D / B \subset 'Z(C / B)]%g -> (*b*) coherent (S A) L^# tau -> \unless coherent (S B) L^# tau, - #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R. + #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R :> algC. Proof. move=> [nsAL nsBL nsCL nsDL] [ltAK sBD sDC sCK sDbZC] cohA. have sBC := subset_trans sBD sDC; have sBK := subset_trans sBC sCK. have [sAK nsBK] := (proper_sub ltAK, normalS sBK sKL nsBL). have{sBC} [nsAK nsBC] := (normalS sAK sKL nsAL, normalS sBC sCK nsBK). -rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n //. +rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n ?ler01 //. apply/unless_contra; rewrite negbK -(Lagrange_index sKL sCK) natrM => lb_KA. pose S2 : seq 'CF(L) := [::]; pose S1 := S2 ++ S A; rewrite -[S A]/S1 in cohA. have ccsS1S: cfConjC_subset S1 calS by apply: seqInd_conjC_subset1. @@ -153,7 +153,7 @@ have sAbZH: (A / B \subset 'Z(H / B))%g. by apply: homg_quotientS; rewrite ?(subset_trans sHL) ?normal_norm. have ltAH: A \proper H. by rewrite properEneq sAH (contraTneq _ lbHA) // => ->; rewrite indexgg addn1. -set x := sqrtC #|H : A|%:R. +set x : algC := sqrtC #|H : A|%:R. have [nz_x x_gt0]: x != 0 /\ 0 < x by rewrite gtr_eqF sqrtC_gt0 gt0CiG. without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2%:R * #|L : H|%:R * x. have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK). diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v index cea9319..4610829 100644 --- a/mathcomp/odd_order/PFsection7.v +++ b/mathcomp/odd_order/PFsection7.v @@ -324,7 +324,7 @@ transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x). apply: eq_bigr => x Ax; rewrite part_a // sum_cfunE -mulrA mulr_suml. apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _). rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu). - rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -4!mulrA 2!(mulrCA _^-1). + rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -3!mulrA 2!(mulrCA _^-1). by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*). rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=. apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu. diff --git a/mathcomp/real_closed/complex.v b/mathcomp/real_closed/complex.v index 9c67f32..8ea1266 100644 --- a/mathcomp/real_closed/complex.v +++ b/mathcomp/real_closed/complex.v @@ -21,6 +21,7 @@ Import GRing.Theory Num.Theory. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Obligation Tactic := idtac. Local Open Scope ring_scope. @@ -36,18 +37,22 @@ Local Notation sqrtr := Num.sqrt. CoInductive complex (R : Type) : Type := Complex { Re : R; Im : R }. -Definition real_complex_def (F : ringType) (phF : phant F) (x : F) := +Delimit Scope complex_scope with C. +Local Open Scope complex_scope. + +Definition real_complex_def (F : ringType) (phF : phant F) (x : F) := Complex x 0. Notation real_complex F := (@real_complex_def _ (Phant F)). Notation "x %:C" := (real_complex _ x) - (at level 2, left associativity, format "x %:C") : ring_scope. -Notation "x +i* y" := (Complex x y) : ring_scope. -Notation "x -i* y" := (Complex x (- y)) : ring_scope. -Notation "x *i " := (Complex 0 x) (at level 8, format "x *i") : ring_scope. -Notation "''i'" := (Complex 0 1) : ring_scope. + (at level 2, left associativity, format "x %:C") : complex_scope. +Notation "x +i* y" := (Complex x y) : complex_scope. +Notation "x -i* y" := (Complex x (- y)) : complex_scope. +Notation "x *i " := (Complex 0 x) (at level 8, format "x *i") : complex_scope. +Notation "''i'" := (Complex 0 1) : complex_scope. Notation "R [i]" := (complex R) (at level 2, left associativity, format "R [i]"). +(* Module ComplexInternal. *) Module ComplexEqChoice. Section ComplexEqChoice. @@ -70,11 +75,11 @@ Definition complex_choiceMixin (R : choiceType) := Definition complex_countMixin (R : countType) := PcanCountMixin (@ComplexEqChoice.complex_of_sqRK R). -Canonical Structure complex_eqType (R : eqType) := +Canonical complex_eqType (R : eqType) := EqType R[i] (complex_eqMixin R). -Canonical Structure complex_choiceType (R : choiceType) := +Canonical complex_choiceType (R : choiceType) := ChoiceType R[i] (complex_choiceMixin R). -Canonical Structure complex_countType (R : countType) := +Canonical complex_countType (R : countType) := CountType R[i] (complex_countMixin R). Lemma eq_complex : forall (R : eqType) (x y : complex R), @@ -99,19 +104,22 @@ Definition addc (x y : R[i]) := let: a +i* b := x in let: c +i* d := y in (a + c) +i* (b + d). Definition oppc (x : R[i]) := let: a +i* b := x in (- a) +i* (- b). -Lemma addcC : commutative addc. -Proof. by move=> [a b] [c d] /=; congr (_ +i* _); rewrite addrC. Qed. -Lemma addcA : associative addc. -Proof. by move=> [a b] [c d] [e f] /=; rewrite !addrA. Qed. - -Lemma add0c : left_id C0 addc. -Proof. by move=> [a b] /=; rewrite !add0r. Qed. +Program Definition complex_zmodMixin := @ZmodMixin _ C0 oppc addc _ _ _ _. +Next Obligation. by move=> [a b] [c d] [e f] /=; rewrite !addrA. Qed. +Next Obligation. by move=> [a b] [c d] /=; congr (_ +i* _); rewrite addrC. Qed. +Next Obligation. by move=> [a b] /=; rewrite !add0r. Qed. +Next Obligation. by move=> [a b] /=; rewrite !addNr. Qed. +Canonical complex_zmodType := ZmodType R[i] complex_zmodMixin. -Lemma addNc : left_inverse C0 oppc addc. -Proof. by move=> [a b] /=; rewrite !addNr. Qed. +Definition scalec (a : R) (x : R[i]) := + let: b +i* c := x in (a * b) +i* (a * c). -Definition complex_ZmodMixin := ZmodMixin addcA addcC add0c addNc. -Canonical Structure complex_ZmodType := ZmodType R[i] complex_ZmodMixin. +Program Definition complex_lmodMixin := @LmodMixin _ _ scalec _ _ _ _. +Next Obligation. by move=> a b [c d] /=; rewrite !mulrA. Qed. +Next Obligation. by move=> [a b] /=; rewrite !mul1r. Qed. +Next Obligation. by move=> a [b c] [d e] /=; rewrite !mulrDr. Qed. +Next Obligation. by move=> [a b] c d /=; rewrite !mulrDl. Qed. +Canonical complex_lmodType := LmodType R R[i] complex_lmodMixin. Definition mulc (x y : R[i]) := let: a +i* b := x in let: c +i* d := y in ((a * c) - (b * d)) +i* ((a * d) + (b * c)). @@ -146,9 +154,8 @@ Lemma nonzero1c : C1 != C0. Proof. by rewrite eq_complex /= oner_eq0. Qed. Definition complex_comRingMixin := ComRingMixin mulcA mulcC mul1c mulc_addl nonzero1c. -Canonical Structure complex_Ring := - Eval hnf in RingType R[i] complex_comRingMixin. -Canonical Structure complex_comRing := Eval hnf in ComRingType R[i] mulcC. +Canonical complex_ringType :=RingType R[i] complex_comRingMixin. +Canonical complex_comRingType := ComRingType R[i] mulcC. Lemma mulVc : forall x, x != C0 -> mulc (invc x) x = C1. Proof. @@ -159,19 +166,16 @@ Qed. Lemma invc0 : invc C0 = C0. Proof. by rewrite /= !mul0r oppr0. Qed. -Definition ComplexFieldUnitMixin := FieldUnitMixin mulVc invc0. -Canonical Structure complex_unitRing := - Eval hnf in UnitRingType C ComplexFieldUnitMixin. -Canonical Structure complex_comUnitRing := - Eval hnf in [comUnitRingType of R[i]]. +Definition complex_fieldUnitMixin := FieldUnitMixin mulVc invc0. +Canonical complex_unitRingType := UnitRingType C complex_fieldUnitMixin. +Canonical complex_comUnitRingType := Eval hnf in [comUnitRingType of R[i]]. -Lemma field_axiom : GRing.Field.mixin_of complex_unitRing. +Lemma field_axiom : GRing.Field.mixin_of complex_unitRingType. Proof. by []. Qed. Definition ComplexFieldIdomainMixin := (FieldIdomainMixin field_axiom). -Canonical Structure complex_iDomain := - Eval hnf in IdomainType R[i] (FieldIdomainMixin field_axiom). -Canonical Structure complex_fieldMixin := FieldType R[i] field_axiom. +Canonical complex_idomainType := IdomainType R[i] (FieldIdomainMixin field_axiom). +Canonical complex_fieldType := FieldType R[i] field_axiom. Ltac simpc := do ? [ rewrite -[(_ +i* _) - (_ +i* _)]/(_ +i* _) @@ -184,20 +188,22 @@ split; [|split=> //] => a b /=; simpc; first by rewrite subrr. by rewrite !mulr0 !mul0r addr0 subr0. Qed. -Canonical Structure real_complex_rmorphism := +Canonical real_complex_rmorphism := RMorphism real_complex_is_rmorphism. -Canonical Structure real_complex_additive := +Canonical real_complex_additive := Additive real_complex_is_rmorphism. -Lemma Re_is_additive : additive (@Re R). -Proof. by case=> a1 b1; case=> a2 b2. Qed. +Lemma Re_is_scalar : scalar (@Re R). +Proof. by move=> a [b c] [d e]. Qed. -Canonical Structure Re_additive := Additive Re_is_additive. +Canonical Re_additive := Additive Re_is_scalar. +Canonical Re_linear := Linear Re_is_scalar. -Lemma Im_is_additive : additive (@Im R). -Proof. by case=> a1 b1; case=> a2 b2. Qed. +Lemma Im_is_scalar : scalar (@Im R). +Proof. by move=> a [b c] [d e]. Qed. -Canonical Structure Im_additive := Additive Im_is_additive. +Canonical Im_additive := Additive Im_is_scalar. +Canonical Im_linear := Linear Im_is_scalar. Definition lec (x y : R[i]) := let: a +i* b := x in let: c +i* d := y in @@ -207,7 +213,7 @@ Definition ltc (x y : R[i]) := let: a +i* b := x in let: c +i* d := y in (d == b) && (a < c). -Definition normc (x : R[i]) : R := +Definition normc (x : R[i]) : R := let: a +i* b := x in sqrtr (a ^+ 2 + b ^+ 2). Notation normC x := (normc x)%:C. @@ -233,14 +239,10 @@ move: x y => [a b] [c d] /= /andP[/eqP -> a_ge0] /andP[/eqP -> c_ge0]. by rewrite eqxx ler_total. Qed. -(* :TODO: put in ssralg ? *) -Lemma exprM (a b : R) : (a * b) ^+ 2 = a ^+ 2 * b ^+ 2. -Proof. by rewrite mulrACA. Qed. - Lemma normcM x y : normc (x * y) = normc x * normc y. Proof. move: x y => [a b] [c d] /=; rewrite -sqrtrM ?addr_ge0 ?sqr_ge0 //. -rewrite sqrrB sqrrD mulrDl !mulrDr -!exprM. +rewrite sqrrB sqrrD mulrDl !mulrDr -!exprMn. rewrite mulrAC [b * d]mulrC !mulrA. suff -> : forall (u v w z t : R), (u - v + w) + (z + v + t) = u + w + (z + t). by rewrite addrAC !addrA. @@ -282,56 +284,51 @@ have [huv|] := ger0P (u + v); last first. by move=> /ltrW /ler_trans -> //; rewrite pmulrn_lge0 // mulr_ge0 ?sqrtr_ge0. rewrite -(@ler_pexpn2r _ 2) -?topredE //=; last first. by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //. -rewrite -mulr_natl !exprM !sqr_sqrtr ?(ler_paddr, sqr_ge0) //. -rewrite -mulrnDl -mulr_natl !exprM ler_pmul2l ?exprn_gt0 ?ltr0n //. -rewrite sqrrD mulrDl !mulrDr -!exprM addrAC. -rewrite [_ + (b * d) ^+ 2]addrC [X in _ <= X]addrAC -!addrA !ler_add2l. -rewrite mulrAC mulrA -mulrA mulrACA mulrC. -by rewrite -subr_ge0 addrAC -sqrrB sqr_ge0. +rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_paddr, sqr_ge0) //. +rewrite -mulrnDl -mulr_natl !exprMn ler_pmul2l ?exprn_gt0 ?ltr0n //. +rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA ler_add2l !addrA. +rewrite [_ + (b * d) ^+ 2]addrC -addrA ler_add2l. +have: 0 <= (a * d - b * c) ^+ 2 by rewrite sqr_ge0. +by rewrite sqrrB addrAC subr_ge0 [_ * c]mulrC mulrACA [d * _]mulrC. Qed. -Definition complex_POrderedMixin := NumMixin lec_normD ltc0_add eq0_normC +Definition complex_numMixin := NumMixin lec_normD ltc0_add eq0_normC ge0_lec_total normCM lec_def ltc_def. -Canonical Structure complex_numDomainType := - NumDomainType R[i] complex_POrderedMixin. +Canonical complex_numDomainType := NumDomainType R[i] complex_numMixin. End ComplexField. End ComplexField. -Canonical complex_ZmodType (R : rcfType) := - ZmodType R[i] (ComplexField.complex_ZmodMixin R). -Canonical complex_Ring (R : rcfType) := - Eval hnf in RingType R[i] (ComplexField.complex_comRingMixin R). -Canonical complex_comRing (R : rcfType) := - Eval hnf in ComRingType R[i] (@ComplexField.mulcC R). -Canonical complex_unitRing (R : rcfType) := - Eval hnf in UnitRingType R[i] (ComplexField.ComplexFieldUnitMixin R). -Canonical complex_comUnitRing (R : rcfType) := - Eval hnf in [comUnitRingType of R[i]]. -Canonical complex_iDomain (R : rcfType) := - Eval hnf in IdomainType R[i] (FieldIdomainMixin (@ComplexField.field_axiom R)). -Canonical complex_fieldType (R : rcfType) := - FieldType R[i] (@ComplexField.field_axiom R). -Canonical complex_numDomainType (R : rcfType) := - NumDomainType R[i] (ComplexField.complex_POrderedMixin R). -Canonical complex_numFieldType (R : rcfType) := - [numFieldType of complex R]. - +Canonical ComplexField.complex_zmodType. +Canonical ComplexField.complex_lmodType. +Canonical ComplexField.complex_ringType. +Canonical ComplexField.complex_comRingType. +Canonical ComplexField.complex_unitRingType. +Canonical ComplexField.complex_comUnitRingType. +Canonical ComplexField.complex_idomainType. +Canonical ComplexField.complex_fieldType. +Canonical ComplexField.complex_numDomainType. +Canonical complex_numFieldType (R : rcfType) := [numFieldType of complex R]. Canonical ComplexField.real_complex_rmorphism. Canonical ComplexField.real_complex_additive. Canonical ComplexField.Re_additive. Canonical ComplexField.Im_additive. Definition conjc {R : ringType} (x : R[i]) := let: a +i* b := x in a -i* b. -Notation "x ^*" := (conjc x) (at level 2, format "x ^*"). +Notation "x ^*" := (conjc x) (at level 2, format "x ^*") : complex_scope. +Local Open Scope complex_scope. +Delimit Scope complex_scope with C. Ltac simpc := do ? - [ rewrite -[(_ +i* _) - (_ +i* _)]/(_ +i* _) - | rewrite -[(_ +i* _) + (_ +i* _)]/(_ +i* _) - | rewrite -[(_ +i* _) * (_ +i* _)]/(_ +i* _) - | rewrite -[(_ +i* _) <= (_ +i* _)]/((_ == _) && (_ <= _)) - | rewrite -[(_ +i* _) < (_ +i* _)]/((_ == _) && (_ < _)) - | rewrite -[`|_ +i* _|]/(sqrtr (_ + _))%:C + [ rewrite -[- (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C - (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C + (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C * (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C ^*]/(_ +i* _)%C + | rewrite -[_ *: (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C <= (_ +i* _)%C]/((_ == _) && (_ <= _)) + | rewrite -[(_ +i* _)%C < (_ +i* _)%C]/((_ == _) && (_ < _)) + | rewrite -[`|(_ +i* _)%C|]/(sqrtr (_ + _))%:C%C | rewrite (mulrNN, mulrN, mulNr, opprB, opprD, mulr0, mul0r, subr0, sub0r, addr0, add0r, mulr1, mul1r, subrr, opprK, oppr0, eqxx) ]. @@ -341,18 +338,18 @@ Section ComplexTheory. Variable R : rcfType. -Lemma ReiNIm : forall x : R[i], Re (x * 'i) = - Im x. +Lemma ReiNIm : forall x : R[i], Re (x * 'i%C) = - Im x. Proof. by case=> a b; simpc. Qed. -Lemma ImiRe : forall x : R[i], Im (x * 'i) = Re x. +Lemma ImiRe : forall x : R[i], Im (x * 'i%C) = Re x. Proof. by case=> a b; simpc. Qed. -Lemma complexE x : x = (Re x)%:C + 'i * (Im x)%:C :> R[i]. +Lemma complexE x : x = (Re x)%:C + 'i%C * (Im x)%:C :> R[i]. Proof. by case: x => *; simpc. Qed. Lemma real_complexE x : x%:C = x +i* 0 :> R[i]. Proof. done. Qed. -Lemma sqr_i : 'i ^+ 2 = -1 :> R[i]. +Lemma sqr_i : 'i%C ^+ 2 = -1 :> R[i]. Proof. by rewrite exprS; simpc; rewrite -real_complexE rmorphN. Qed. Lemma complexI : injective (real_complex R). Proof. by move=> x y []. Qed. @@ -377,13 +374,17 @@ split=> [[a b] [c d]|] /=; first by simpc; rewrite [d - _]addrC. by split=> [[a b] [c d]|] /=; simpc. Qed. +Lemma conjc_is_scalable : scalable (@conjc R). +Proof. by move=> a [b c]; simpc. Qed. + Canonical conjc_rmorphism := RMorphism conjc_is_rmorphism. Canonical conjc_additive := Additive conjc_is_rmorphism. +Canonical conjc_linear := AddLinear conjc_is_scalable. Lemma conjcK : involutive (@conjc R). Proof. by move=> [a b] /=; rewrite opprK. Qed. -Lemma mulcJ_ge0 (x : R[i]) : 0 <= x * x ^*. +Lemma mulcJ_ge0 (x : R[i]) : 0 <= x * x^*%C. Proof. by move: x=> [a b]; simpc; rewrite mulrC addNr eqxx addr_ge0 ?sqr_ge0. Qed. @@ -391,14 +392,14 @@ Qed. Lemma conjc_real (x : R) : x%:C^* = x%:C. Proof. by rewrite /= oppr0. Qed. -Lemma ReJ_add (x : R[i]) : (Re x)%:C = (x + x^*) / 2%:R. +Lemma ReJ_add (x : R[i]) : (Re x)%:C = (x + x^*%C) / 2%:R. Proof. case: x => a b; simpc; rewrite [0 ^+ 2]mul0r addr0 /=. rewrite -!mulr2n -mulr_natr -mulrA [_ * (_ / _)]mulrA. by rewrite divff ?mulr1 // -natrM pnatr_eq0. Qed. -Lemma ImJ_sub (x : R[i]) : (Im x)%:C = (x^* - x) / 2%:R * 'i. +Lemma ImJ_sub (x : R[i]) : (Im x)%:C = (x^*%C - x) / 2%:R * 'i%C. Proof. case: x => a b; simpc; rewrite [0 ^+ 2]mul0r addr0 /=. rewrite -!mulr2n -mulr_natr -mulrA [_ * (_ / _)]mulrA. @@ -426,7 +427,7 @@ Proof. exact: (conjc_nat 1). Qed. Lemma conjc_eq0 : forall x : R[i], (x ^* == 0) = (x == 0). Proof. by move=> [a b]; rewrite !eq_complex /= eqr_oppLR oppr0. Qed. -Lemma conjc_inv: forall x : R[i], (x^-1)^* = (x^* )^-1. +Lemma conjc_inv: forall x : R[i], (x^-1)^* = (x^*%C )^-1. Proof. exact: fmorphV. Qed. Lemma complex_root_conj (p : {poly R[i]}) (x : R[i]) : @@ -448,18 +449,36 @@ Qed. Lemma normc_def (z : R[i]) : `|z| = (sqrtr ((Re z)^+2 + (Im z)^+2))%:C. Proof. by case: z. Qed. -Lemma add_Re2_Im2 (z : R[i]) : ((Re z)^+2 + (Im z)^+2)%:C = `|z|^+2. +Lemma add_Re2_Im2 (z : R[i]) : ((Re z)^+2 + (Im z)^+2)%:C = `|z|^+2. Proof. by rewrite normc_def -rmorphX sqr_sqrtr ?addr_ge0 ?sqr_ge0. Qed. -Lemma addcJ (z : R[i]) : z + z^* = 2%:R * (Re z)%:C. +Lemma addcJ (z : R[i]) : z + z^*%C = 2%:R * (Re z)%:C. Proof. by rewrite ReJ_add mulrC mulfVK ?pnatr_eq0. Qed. -Lemma subcJ (z : R[i]) : z - z^* = 2%:R * (Im z)%:C * 'i. +Lemma subcJ (z : R[i]) : z - z^*%C = 2%:R * (Im z)%:C * 'i%C. Proof. rewrite ImJ_sub mulrCA mulrA mulfVK ?pnatr_eq0 //. -by rewrite -mulrA ['i * _]sqr_i mulrN1 opprB. +by rewrite -mulrA ['i%C * _]sqr_i mulrN1 opprB. Qed. +Lemma complex_real (a b : R) : a +i* b \is Num.real = (b == 0). +Proof. +rewrite realE; simpc; rewrite [0 == _]eq_sym. +by have [] := ltrgtP 0 a; rewrite ?(andbF, andbT, orbF, orbb). +Qed. + +Lemma complex_realP (x : R[i]) : reflect (exists y, x = y%:C) (x \is Num.real). +Proof. +case: x=> [a b] /=; rewrite complex_real. +by apply: (iffP eqP) => [->|[c []//]]; exists a. +Qed. + +Lemma RRe_real (x : R[i]) : x \is Num.real -> (Re x)%:C = x. +Proof. by move=> /complex_realP [y ->]. Qed. + +Lemma RIm_real (x : R[i]) : x \is Num.real -> (Im x)%:C = 0. +Proof. by move=> /complex_realP [y ->]. Qed. + End ComplexTheory. (* Section RcfDef. *) @@ -593,13 +612,13 @@ apply/eqP/eqP=> [eqs|->]; last by rewrite sqrtc0. by rewrite -[x]sqr_sqrtc eqs exprS mul0r. Qed. -Lemma normcE x : `|x| = sqrtc (x * x^*). +Lemma normcE x : `|x| = sqrtc (x * x^*%C). Proof. case: x=> a b; simpc; rewrite [b * a]mulrC addNr sqrtc_sqrtr //. by simpc; rewrite /= addr_ge0 ?sqr_ge0. Qed. -Lemma sqr_normc (x : R[i]) : (`|x| ^+ 2) = x * x^*. +Lemma sqr_normc (x : R[i]) : (`|x| ^+ 2) = x * x^*%C. Proof. by rewrite normcE sqr_sqrtc. Qed. Lemma normc_ge_Re (x : R[i]) : `|Re x|%:C <= `|x|. @@ -607,17 +626,17 @@ Proof. by case: x => a b; simpc; rewrite -sqrtr_sqr ler_wsqrtr // ler_addl sqr_ge0. Qed. -Lemma normcJ (x : R[i]) : `|x^*| = `|x|. +Lemma normcJ (x : R[i]) : `|x^*%C| = `|x|. Proof. by case: x => a b; simpc; rewrite /= sqrrN. Qed. -Lemma invc_norm (x : R[i]) : x^-1 = `|x|^-2 * x^*. +Lemma invc_norm (x : R[i]) : x^-1 = `|x|^-2 * x^*%C. Proof. case: (altP (x =P 0)) => [->|dx]; first by rewrite rmorph0 mulr0 invr0. -apply: (mulIf dx); rewrite mulrC divff // -mulrA [_^* * _]mulrC -(sqr_normc x). +apply: (mulIf dx); rewrite mulrC divff // -mulrA [_^*%C * _]mulrC -(sqr_normc x). by rewrite mulVf // expf_neq0 ?normr_eq0. Qed. -Lemma canonical_form (a b c : R[i]) : +Lemma canonical_form (a b c : R[i]) : a != 0 -> let d := b ^+ 2 - 4%:R * a * c in let r1 := (- b - sqrtc d) / 2%:R / a in @@ -637,7 +656,7 @@ rewrite sqr_sqrtc sqrrN /d opprB addrC addrNK -2!mulrA. by rewrite mulrACA -natf_div // mul1r mulrAC divff ?mul1r. Qed. -Lemma monic_canonical_form (b c : R[i]) : +Lemma monic_canonical_form (b c : R[i]) : let d := b ^+ 2 - 4%:R * c in let r1 := (- b - sqrtc d) / 2%:R in let r2 := (- b + sqrtc d) / 2%:R in @@ -649,12 +668,12 @@ Qed. Section extramx. (* missing lemmas from matrix.v or mxalgebra.v *) -Lemma mul_mx_rowfree_eq0 (K : fieldType) (m n p: nat) - (W : 'M[K]_(m,n)) (V : 'M[K]_(n,p)) : +Lemma mul_mx_rowfree_eq0 (K : fieldType) (m n p: nat) + (W : 'M[K]_(m,n)) (V : 'M[K]_(n,p)) : row_free V -> (W *m V == 0) = (W == 0). Proof. by move=> free; rewrite -!mxrank_eq0 mxrankMfree ?mxrank_eq0. Qed. -Lemma sub_sums_genmxP (F : fieldType) (I : finType) (P : pred I) (m n : nat) +Lemma sub_sums_genmxP (F : fieldType) (I : finType) (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B_ : I -> 'M_(m, n)) : reflect (exists u_ : I -> 'M_m, A = \sum_(i | P i) u_ i *m B_ i) (A <= \sum_(i | P i) <<B_ i>>)%MS. @@ -706,7 +725,7 @@ rewrite eq_mviE xpair_eqE -!val_eqE /= eq_sym andbb. rewrite ltn_eqF // subr0 mulr1 summxE big1. rewrite [w as X in X *m _]mx11_scalar => ->. by rewrite mul_scalar_mx scale0r submx0. -move=> [i' j'] /= /andP[lt_j'i']. +move=> [i' j'] /= /andP[lt_j'i']. rewrite xpair_eqE /= => neq'_ij. rewrite /= !mxvec_delta !mxE big_ord1 !mxE !eqxx !eq_mviE. rewrite !xpair_eqE /= [_ == i']eq_sym [_ == j']eq_sym (negPf neq'_ij) /=. @@ -730,7 +749,7 @@ rewrite (eq_bigr (fun _ => 1%N)); last first. by move/eqP; rewrite oner_eq0. transitivity (\sum_(i < n) (\sum_(j < n | j < i) 1))%N. by rewrite pair_big_dep. -apply: eq_bigr => [] [[|i] Hi] _ /=; first by rewrite big1. +apply: eq_bigr => [] [[|i] Hi] _ /=; first by rewrite big1. rewrite (eq_bigl _ _ (fun _ => ltnS _ _)). have [n_eq0|n_gt0] := posnP n; first by move: Hi (Hi); rewrite {1}n_eq0. rewrite -[n]prednK // big_ord_narrow_leq /=. @@ -795,13 +814,13 @@ case: sp => [|sp] in Hsp *. move: Hsp => /eqP/size_poly1P/sig2_eqW [c c_neq0 ->]. by exists ((-c)%:M); rewrite monicE lead_coefC => /eqP ->; apply: det_mx00. have addn1n n : (n + 1 = 1 + n)%N by rewrite addn1. -exists (castmx (erefl _, addn1n _) +exists (castmx (erefl _, addn1n _) (block_mx (\row_(i < sp) - p`_(sp - i)) (-p`_0)%:M 1%:M 0)). elim/poly_ind: p sp Hsp (addn1n _) => [|p c IHp] sp; first by rewrite size_poly0. rewrite size_MXaddC. have [->|p_neq0] //= := altP eqP; first by rewrite size_poly0; case: ifP. -move=> [Hsp] eq_cast. +move=> [Hsp] eq_cast. rewrite monicE lead_coefDl ?size_polyC ?size_mul ?polyX_eq0 //; last first. by rewrite size_polyX addn2 Hsp ltnS (leq_trans (leq_b1 _)). rewrite lead_coefMX -monicE => p_monic. @@ -845,7 +864,7 @@ congr (_ * 'X + c%:P * _). apply/matrixP => k l; rewrite !simp. case: splitP => k' /=; rewrite ?ord1 /bump ltnNge leq_ord add0n. case: splitP => [k'' /= |k'' -> //]; rewrite ord1 !simp => k_eq0 _. - case: splitP => l' /=; rewrite ?ord1 /bump ltnNge leq_ord add0n !simp; + case: splitP => l' /=; rewrite ?ord1 /bump ltnNge leq_ord add0n !simp; last by move/eqP; rewrite ?addn0 ltn_eqF. move<-; case: splitP => l'' /=; rewrite ?ord1 ?addn0 !simp. by move<-; rewrite subSn ?leq_ord ?coefE. @@ -853,7 +872,7 @@ congr (_ * 'X + c%:P * _). by rewrite !rmorphN ?subnn addr0. case: splitP => k'' /=; rewrite ?ord1 => -> // []; rewrite !simp. case: splitP => l' /=; rewrite /bump ltnNge leq_ord add0n !simp -?val_eqE /=; - last by rewrite ord1 addn0 => /eqP; rewrite ltn_eqF. + last by rewrite ord1 addn0 => /eqP; rewrite ltn_eqF. by case: splitP => l'' /= -> <- <-; rewrite !simp // ?ord1 ?addn0 ?ltn_eqF. move=> {IHp Hsp p_neq0 p_monic}; rewrite add0n; set s := _ ^+ _; apply: (@mulfI _ s); first by rewrite signr_eq0. @@ -958,7 +977,7 @@ Definition CommonEigenVec_def K (phK : phant K) (d r : nat) := exists2 v : 'rV_m, (v != 0) & forall f, f \in sf -> exists a, (v <= eigenspace f a)%MS. Notation CommonEigenVec K d r := (@CommonEigenVec_def _ (Phant K) d r). - + Definition Eigen1Vec_def K (phK : phant K) (d : nat) := forall (m : nat) (V : 'M[K]_m), ~~ (d %| \rank V) -> forall (f : 'M_m), (V *m f <= V)%MS -> exists a, eigenvalue f a. @@ -1028,7 +1047,7 @@ have [eqWV|neqWV] := altP (@eqmxP _ _ _ _ W 1%:M). by exists a; rewrite -eigenspace_restrict // eqWV submx1. have lt_WV : (\rank W < \rank V)%N. rewrite -[X in (_ < X)%N](@mxrank1 K) rank_ltmx //. - by rewrite ltmxEneq neqWV // submx1. + by rewrite ltmxEneq neqWV // submx1. have ltZV : (\rank Z < \rank V)%N. rewrite -[X in (_ < X)%N]rWZ -subn_gt0 addnK lt0n mxrank_eq0 -lt0mx. move: a_eigen_f' => /eigenvalueP [v /eigenspaceP] sub_vW v_neq0. @@ -1067,16 +1086,16 @@ suff: exists a, eigenvalue (restrict V f) a. by move=> [a /eigenvalue_restrict Hf]; exists a; apply: Hf. move: (\rank V) (restrict V f) => {f f_stabV V m} n f in HrV *. pose u := map_mx (@Re R) f; pose v := map_mx (@Im R) f. -have fE : f = MtoC u + 'i *: MtoC v. +have fE : f = MtoC u + 'i%C *: MtoC v. rewrite /u /v [f]lock; apply/matrixP => i j; rewrite !mxE /=. by case: (locked f i j) => a b; simpc. move: u v => u v in fE *. pose L1fun : 'M[R]_n -> _ := - 2%:R^-1 \*: (mulmxr u \+ (mulmxr v \o trmx) + 2%:R^-1 \*: (mulmxr u \+ (mulmxr v \o trmx) \+ ((mulmx (u^T)) \- (mulmx (v^T) \o trmx))). pose L1 := lin_mx [linear of L1fun]. pose L2fun : 'M[R]_n -> _ := - 2%:R^-1 \*: (((@GRing.opp _) \o (mulmxr u \o trmx) \+ mulmxr v) + 2%:R^-1 \*: (((@GRing.opp _) \o (mulmxr u \o trmx) \+ mulmxr v) \+ ((mulmx (u^T) \o trmx) \+ (mulmx (v^T)))). pose L2 := lin_mx [linear of L2fun]. have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _). @@ -1111,7 +1130,7 @@ do [move=> /(congr1 vec_mx); rewrite mxvecK linearZ /=] in g_eigenL2. move=> {L1 L2 L1fun L2fun Hg HrV}. set vg := vec_mx g in g_eigenL1 g_eigenL2. exists (a +i* b); apply/eigenvalueP. -pose w := (MtoC vg - 'i *: MtoC vg^T). +pose w := (MtoC vg - 'i%C *: MtoC vg^T). exists (nz_row w); last first. rewrite nz_row_eq0 subr_eq0; apply: contraNneq g_neq0 => Hvg. rewrite -vec_mx_eq0; apply/eqP/matrixP => i j; rewrite !mxE /=. @@ -1124,11 +1143,11 @@ rewrite (submx_trans (nz_row_sub _)) //; apply/eigenspaceP. rewrite fE [a +i* b]complexE /=. rewrite !(mulmxDr, mulmxBl, =^~scalemxAr, =^~scalemxAl) -!map_mxM. rewrite !(scalerDl, scalerDr, scalerN, =^~scalemxAr, =^~scalemxAl). -rewrite !scalerA /= mulrAC ['i * _]sqr_i ?mulN1r scaleN1r scaleNr !opprK. -rewrite [_ * 'i]mulrC -!scalerA -!map_mxZ /=. -do 2!rewrite [X in (_ - _) + X]addrC [_ - 'i *: _ + _]addrACA. +rewrite !scalerA /= mulrAC ['i%C * _]sqr_i ?mulN1r scaleN1r scaleNr !opprK. +rewrite [_ * 'i%C]mulrC -!scalerA -!map_mxZ /=. +do 2!rewrite [X in (_ - _) + X]addrC [_ - 'i%C *: _ + _]addrACA. rewrite ![- _ + _]addrC -!scalerBr -!(rmorphB, rmorphD) /=. -congr (_ + 'i *: _); congr map_mx; rewrite -[_ *: _^T]linearZ /=; +congr (_ + 'i%C *: _); congr map_mx; rewrite -[_ *: _^T]linearZ /=; rewrite -g_eigenL1 -g_eigenL2 linearZ -(scalerDr, scalerBr); do ?rewrite ?trmxK ?trmx_mul ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=; rewrite -[in X in _ *: (_ + X)]addrC 1?opprD 1?opprB ?mulmxN ?mulNmx; @@ -1206,8 +1225,8 @@ move=> /(_ m.+1 1 _ f) []; last by move=> a; exists a. + by rewrite mxrank1 (contra (dvdn_leq _)) // -ltnNge ltn_expl. + by rewrite submx1. Qed. - -Lemma C_acf_axiom : GRing.ClosedField.axiom [ringType of R[i]]. + +Lemma complex_acf_axiom : GRing.ClosedField.axiom [ringType of R[i]]. Proof. move=> n c n_gt0; pose p := 'X^n - \poly_(i < n) c i. suff [x rpx] : exists x, root p x. @@ -1223,14 +1242,67 @@ have [] := Theorem7' (companion p); first by rewrite -(subnK sp_gt1) addn2. by move=> x; rewrite eigenvalue_root_char companionK //; exists x. Qed. -Definition C_decFieldMixin := closed_fields_QEMixin C_acf_axiom. -Canonical C_decField := DecFieldType R[i] C_decFieldMixin. -Canonical C_closedField := ClosedFieldType R[i] C_acf_axiom. +Definition complex_decFieldMixin := closed_fields_QEMixin complex_acf_axiom. +Canonical complex_decField := DecFieldType R[i] complex_decFieldMixin. +Canonical complex_closedField := ClosedFieldType R[i] complex_acf_axiom. + +Definition complex_numClosedFieldMixin := + ImaginaryMixin (sqr_i R) (fun x=> esym (sqr_normc x)). + +Canonical complex_numClosedFieldType := + NumClosedFieldType R[i] complex_numClosedFieldMixin. End Paper_HarmDerksen. End ComplexClosed. +(* End ComplexInternal. *) + +(* Canonical ComplexInternal.complex_eqType. *) +(* Canonical ComplexInternal.complex_choiceType. *) +(* Canonical ComplexInternal.complex_countType. *) +(* Canonical ComplexInternal.complex_ZmodType. *) +(* Canonical ComplexInternal.complex_Ring. *) +(* Canonical ComplexInternal.complex_comRing. *) +(* Canonical ComplexInternal.complex_unitRing. *) +(* Canonical ComplexInternal.complex_comUnitRing. *) +(* Canonical ComplexInternal.complex_iDomain. *) +(* Canonical ComplexInternal.complex_fieldType. *) +(* Canonical ComplexInternal.ComplexField.real_complex_rmorphism. *) +(* Canonical ComplexInternal.ComplexField.real_complex_additive. *) +(* Canonical ComplexInternal.ComplexField.Re_additive. *) +(* Canonical ComplexInternal.ComplexField.Im_additive. *) +(* Canonical ComplexInternal.complex_numDomainType. *) +(* Canonical ComplexInternal.complex_numFieldType. *) +(* Canonical ComplexInternal.conjc_rmorphism. *) +(* Canonical ComplexInternal.conjc_additive. *) +(* Canonical ComplexInternal.complex_decField. *) +(* Canonical ComplexInternal.complex_closedField. *) +(* Canonical ComplexInternal.complex_numClosedFieldType. *) + +(* Definition complex_algebraic_trans := ComplexInternal.complex_algebraic_trans. *) + +Section ComplexClosedTheory. + +Variable R : rcfType. + +Lemma complexiE : 'i%C = 'i%R :> R[i]. +Proof. by []. Qed. + +Lemma complexRe (x : R[i]) : (Re x)%:C = 'Re x. +Proof. +rewrite {1}[x]Crect raddfD /= mulrC ReiNIm rmorphB /=. +by rewrite ?RRe_real ?RIm_real ?Creal_Im ?Creal_Re // subr0. +Qed. + +Lemma complexIm (x : R[i]) : (Im x)%:C = 'Im x. +Proof. +rewrite {1}[x]Crect raddfD /= mulrC ImiRe rmorphD /=. +by rewrite ?RRe_real ?RIm_real ?Creal_Im ?Creal_Re // add0r. +Qed. + +End ComplexClosedTheory. + Definition complexalg := realalg[i]. Canonical complexalg_eqType := [eqType of complexalg]. diff --git a/mathcomp/real_closed/polyrcf.v b/mathcomp/real_closed/polyrcf.v index 949dec0..c29cb96 100644 --- a/mathcomp/real_closed/polyrcf.v +++ b/mathcomp/real_closed/polyrcf.v @@ -360,48 +360,6 @@ rewrite !mul1r mulrC -ltr_subl_addr. by rewrite (ler_lt_trans _ (He' y _)) // ler_sub_dist. Qed. -(* Todo : orderedpoly !! *) -(* Lemma deriv_expz_nat (n : nat) p : (p ^ n)^`() = (p^`() * p ^ (n.-1)) *~ n. *) -(* Proof. *) -(* elim: n => [|n ihn] /= in p *; first by rewrite expr0z derivC mul0zr. *) -(* rewrite exprSz_nat derivM ihn mulzrAr mulrCA -exprSz_nat. *) -(* by case: n {ihn}=> [|n] //; rewrite mul0zr addr0 mul1zr. *) -(* Qed. *) - -(* Definition derivCE := (derivE, deriv_expz_nat). *) - -(* Lemma size_poly_ind : forall K : {poly R} -> Prop, *) -(* K 0 -> *) -(* (forall p sp, size p = sp.+1 -> *) -(* forall q, (size q <= sp)%N -> K q -> K p) *) -(* -> forall p, K p. *) -(* Proof. *) -(* move=> K K0 ihK p. *) -(* move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn. *) -(* by move: spn; rewrite leqn0 size_poly_eq0; move/eqP->. *) -(* case spSn: (size p == n.+1). *) -(* move/eqP:spSn; move/ihK=> ihKp; apply: (ihKp 0)=>//. *) -(* by rewrite size_poly0. *) -(* by move:spn; rewrite leq_eqVlt spSn /= ltnS; by move/ihn. *) -(* Qed. *) - -(* Lemma size_poly_indW : forall K : {poly R} -> Prop, *) -(* K 0 -> *) -(* (forall p sp, size p = sp.+1 -> *) -(* forall q, size q = sp -> K q -> K p) *) -(* -> forall p, K p. *) -(* Proof. *) -(* move=> K K0 ihK p. *) -(* move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn. *) -(* by move: spn; rewrite leqn0 size_poly_eq0; move/eqP->. *) -(* case spSn: (size p == n.+1). *) -(* move/eqP:spSn; move/ihK=> ihKp; case: n ihn spn ihKp=> [|n] ihn spn ihKp. *) -(* by apply: (ihKp 0)=>//; rewrite size_poly0. *) -(* apply: (ihKp 'X^n)=>//; first by rewrite size_polyXn. *) -(* by apply: ihn; rewrite size_polyXn. *) -(* by move:spn; rewrite leq_eqVlt spSn /= ltnS; by move/ihn. *) -(* Qed. *) - Lemma poly_ltsp_roots p (rs : seq R) : (size rs >= size p)%N -> uniq rs -> all (root p) rs -> p = 0. Proof. |