diff options
Diffstat (limited to 'mathcomp')
| -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 |
16 files changed, 980 insertions, 859 deletions
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. |