Library mathcomp.algebra.num_theory.numfield
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import ssrAC div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly orderedzmod numdomain.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import ssrAC div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly orderedzmod numdomain.
Number structures (numfield.v)
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
NB: The header of ssrnum.v explains how to use the files in this directory.
This file defines the following number structures:
numFieldType == Field with an order and a norm
The HB class is called NumField.
numClosedFieldType == Partially ordered Closed Field with conjugation
The HB class is called ClosedField.
realFieldType == Num Field where all elements are positive or negative
The HB class is called RealField.
rcfType == A Real Field with the real closed axiom
The HB class is called RealClosedField.
Over these structures, we have the following operation:
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
'Re z == the real component of z
'Im z == the imaginary component of z
z^* == the complex conjugate of z
:= Num.conj 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).
- list of prefixes : p : positive n : negative sp : strictly positive sn : strictly negative i : interior = in [0, 1] or ]0, 1[ e : exterior = in [1, +oo[ or ]1; +oo[ w : non strict (weak) monotony
Reserved Notation "n .-root" (format "n .-root").
Reserved Notation "'i".
Reserved Notation "'Re z" (at level 10, z at level 8).
Reserved Notation "'Im z" (at level 10, z at level 8).
Set Implicit Arguments.
Local Open Scope order_scope.
Local Open Scope group_scope.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory.
Import orderedzmod.Num numdomain.Num.
Module Num.
#[short(type="numFieldType")]
HB.structure Definition NumField := { R of GRing.UnitRing_isField R &
GRing.IntegralDomain R &
POrderedZmodule R &
NormedZmodule (POrderedZmodule.clone R _) R &
isNumRing R }.
Module NumFieldExports.
Bind Scope ring_scope with NumField.sort.
End NumFieldExports.
#[short(type="numClosedFieldType")]
HB.structure Definition ClosedField :=
{ R of NumField_isImaginary R & GRing.ClosedField R & NumField R }.
Definition conj {C : numClosedFieldType} : C → C := @conj_subdef C.
#[export] HB.instance Definition _ C := GRing.RMorphism.on (@conj C).
#[deprecated(since="mathcomp 2.5.0",note="Use conj instead.")]
Notation conj_op := conj (only parsing).
Module ClosedFieldExports.
Bind Scope ring_scope with ClosedField.sort.
End ClosedFieldExports.
#[short(type="realFieldType")]
HB.structure Definition RealField :=
{ R of Order.Total ring_display R & NumField R }.
Module RealFieldExports.
Bind Scope ring_scope with RealField.sort.
End RealFieldExports.
#[short(type="rcfType")]
HB.structure Definition RealClosedField :=
{ R of RealField_isClosed R & RealField R }.
Module RealClosedFieldExports.
Bind Scope ring_scope with RealClosedField.sort.
End RealClosedFieldExports.
Section RealClosed.
Variable R : rcfType.
Lemma poly_ivt : real_closed_axiom R.
Fact sqrtr_subproof (x : R) :
exists2 y, 0 ≤ y & (if 0 ≤ x then y ^+ 2 == x else y == 0) : bool.
End RealClosed.
Module Import Def.
Notation conjC := conj.
Definition sqrtr {R} x := s2val (sig2W (@sqrtr_subproof R x)).
End Def.
Notation sqrt := sqrtr.
Module Import Syntax.
Notation "z ^*" := (conj z) : ring_scope.
Notation "'i" := imaginary : ring_scope.
End Syntax.
Module Export Theory.
Section NumFieldTheory.
Variable F : numFieldType.
Implicit Types x y z t : F.
Lemma unitf_gt0 x : 0 < x → x \is a GRing.unit.
Lemma unitf_lt0 x : x < 0 → x \is a GRing.unit.
Lemma lef_pV2 : {in pos &, {mono (@GRing.inv F) : x y /~ x ≤ y}}.
Lemma lef_nV2 : {in neg &, {mono (@GRing.inv F) : x y /~ x ≤ y}}.
Lemma ltf_pV2 : {in pos &, {mono (@GRing.inv F) : x y /~ x < y}}.
Lemma ltf_nV2 : {in neg &, {mono (@GRing.inv F) : x y /~ x < y}}.
Definition ltef_pV2 := (lef_pV2, ltf_pV2).
Definition ltef_nV2 := (lef_nV2, ltf_nV2).
Lemma invf_pgt : {in pos &, ∀ x y, (x < y^-1) = (y < x^-1)}.
Lemma invf_pge : {in pos &, ∀ x y, (x ≤ y^-1) = (y ≤ x^-1)}.
Lemma invf_ngt : {in neg &, ∀ x y, (x < y^-1) = (y < x^-1)}.
Lemma invf_nge : {in neg &, ∀ x y, (x ≤ y^-1) = (y ≤ x^-1)}.
Lemma invf_gt1 x : 0 < x → (1 < x^-1) = (x < 1).
Lemma invf_ge1 x : 0 < x → (1 ≤ x^-1) = (x ≤ 1).
Definition invf_gte1 := (invf_ge1, invf_gt1).
Lemma invf_plt : {in pos &, ∀ x y, (x^-1 < y) = (y^-1 < x)}.
Lemma invf_ple : {in pos &, ∀ x y, (x^-1 ≤ y) = (y^-1 ≤ x)}.
Lemma invf_nlt : {in neg &, ∀ x y, (x^-1 < y) = (y^-1 < x)}.
Lemma invf_nle : {in neg &, ∀ x y, (x^-1 ≤ y) = (y^-1 ≤ x)}.
Lemma invf_le1 x : 0 < x → (x^-1 ≤ 1) = (1 ≤ x).
Lemma invf_lt1 x : 0 < x → (x^-1 < 1) = (1 < x).
Definition invf_lte1 := (invf_le1, invf_lt1).
Definition invf_cp1 := (invf_gte1, invf_lte1).
These lemma are all combinations of mono(LR|RL) with ler_ [pn]mul2[rl].
Lemma ler_pdivlMr z x y : 0 < z → (x ≤ y / z) = (x × z ≤ y).
Lemma ltr_pdivlMr z x y : 0 < z → (x < y / z) = (x × z < y).
Definition lter_pdivlMr := (ler_pdivlMr, ltr_pdivlMr).
Lemma ler_pdivrMr z x y : 0 < z → (y / z ≤ x) = (y ≤ x × z).
Lemma ltr_pdivrMr z x y : 0 < z → (y / z < x) = (y < x × z).
Definition lter_pdivrMr := (ler_pdivrMr, ltr_pdivrMr).
Lemma ler_pdivlMl z x y : 0 < z → (x ≤ z^-1 × y) = (z × x ≤ y).
Lemma ltr_pdivlMl z x y : 0 < z → (x < z^-1 × y) = (z × x < y).
Definition lter_pdivlMl := (ler_pdivlMl, ltr_pdivlMl).
Lemma ler_pdivrMl z x y : 0 < z → (z^-1 × y ≤ x) = (y ≤ z × x).
Lemma ltr_pdivrMl z x y : 0 < z → (z^-1 × y < x) = (y < z × x).
Definition lter_pdivrMl := (ler_pdivrMl, ltr_pdivrMl).
Lemma ler_ndivlMr z x y : z < 0 → (x ≤ y / z) = (y ≤ x × z).
Lemma ltr_ndivlMr z x y : z < 0 → (x < y / z) = (y < x × z).
Definition lter_ndivlMr := (ler_ndivlMr, ltr_ndivlMr).
Lemma ler_ndivrMr z x y : z < 0 → (y / z ≤ x) = (x × z ≤ y).
Lemma ltr_ndivrMr z x y : z < 0 → (y / z < x) = (x × z < y).
Definition lter_ndivrMr := (ler_ndivrMr, ltr_ndivrMr).
Lemma ler_ndivlMl z x y : z < 0 → (x ≤ z^-1 × y) = (y ≤ z × x).
Lemma ltr_ndivlMl z x y : z < 0 → (x < z^-1 × y) = (y < z × x).
Definition lter_ndivlMl := (ler_ndivlMl, ltr_ndivlMl).
Lemma ler_ndivrMl z x y : z < 0 → (z^-1 × y ≤ x) = (z × x ≤ y).
Lemma ltr_ndivrMl z x y : z < 0 → (z^-1 × y < x) = (z × x < y).
Definition lter_ndivrMl := (ler_ndivrMl, ltr_ndivrMl).
Lemma natf_div m d : (d %| m)%N → (m %/ d)%:R = m%:R / d%:R :> F.
Lemma normfV : {morph (norm : F → F) : x / x ^-1}.
Lemma normf_div : {morph (norm : F → F) : x y / x / y}.
Lemma invr_sg x : (sg x)^-1 = sgr x.
Lemma sgrV x : sgr x^-1 = sgr x.
Lemma splitr x : x = x / 2%:R + x / 2%:R.
Lemma ltr_pdivlMr z x y : 0 < z → (x < y / z) = (x × z < y).
Definition lter_pdivlMr := (ler_pdivlMr, ltr_pdivlMr).
Lemma ler_pdivrMr z x y : 0 < z → (y / z ≤ x) = (y ≤ x × z).
Lemma ltr_pdivrMr z x y : 0 < z → (y / z < x) = (y < x × z).
Definition lter_pdivrMr := (ler_pdivrMr, ltr_pdivrMr).
Lemma ler_pdivlMl z x y : 0 < z → (x ≤ z^-1 × y) = (z × x ≤ y).
Lemma ltr_pdivlMl z x y : 0 < z → (x < z^-1 × y) = (z × x < y).
Definition lter_pdivlMl := (ler_pdivlMl, ltr_pdivlMl).
Lemma ler_pdivrMl z x y : 0 < z → (z^-1 × y ≤ x) = (y ≤ z × x).
Lemma ltr_pdivrMl z x y : 0 < z → (z^-1 × y < x) = (y < z × x).
Definition lter_pdivrMl := (ler_pdivrMl, ltr_pdivrMl).
Lemma ler_ndivlMr z x y : z < 0 → (x ≤ y / z) = (y ≤ x × z).
Lemma ltr_ndivlMr z x y : z < 0 → (x < y / z) = (y < x × z).
Definition lter_ndivlMr := (ler_ndivlMr, ltr_ndivlMr).
Lemma ler_ndivrMr z x y : z < 0 → (y / z ≤ x) = (x × z ≤ y).
Lemma ltr_ndivrMr z x y : z < 0 → (y / z < x) = (x × z < y).
Definition lter_ndivrMr := (ler_ndivrMr, ltr_ndivrMr).
Lemma ler_ndivlMl z x y : z < 0 → (x ≤ z^-1 × y) = (y ≤ z × x).
Lemma ltr_ndivlMl z x y : z < 0 → (x < z^-1 × y) = (y < z × x).
Definition lter_ndivlMl := (ler_ndivlMl, ltr_ndivlMl).
Lemma ler_ndivrMl z x y : z < 0 → (z^-1 × y ≤ x) = (z × x ≤ y).
Lemma ltr_ndivrMl z x y : z < 0 → (z^-1 × y < x) = (z × x < y).
Definition lter_ndivrMl := (ler_ndivrMl, ltr_ndivrMl).
Lemma natf_div m d : (d %| m)%N → (m %/ d)%:R = m%:R / d%:R :> F.
Lemma normfV : {morph (norm : F → F) : x / x ^-1}.
Lemma normf_div : {morph (norm : F → F) : x y / x / y}.
Lemma invr_sg x : (sg x)^-1 = sgr x.
Lemma sgrV x : sgr x^-1 = sgr x.
Lemma splitr x : x = x / 2%:R + x / 2%:R.
lteif
Lemma lteif_pdivlMr C z x y :
0 < z → x < y / z ?<= if C = (x × z < y ?<= if C).
Lemma lteif_pdivrMr C z x y :
0 < z → y / z < x ?<= if C = (y < x × z ?<= if C).
Lemma lteif_pdivlMl C z x y :
0 < z → x < z^-1 × y ?<= if C = (z × x < y ?<= if C).
Lemma lteif_pdivrMl C z x y :
0 < z → z^-1 × y < x ?<= if C = (y < z × x ?<= if C).
Lemma lteif_ndivlMr C z x y :
z < 0 → x < y / z ?<= if C = (y < x × z ?<= if C).
Lemma lteif_ndivrMr C z x y :
z < 0 → y / z < x ?<= if C = (x × z < y ?<= if C).
Lemma lteif_ndivlMl C z x y :
z < 0 → x < z^-1 × y ?<= if C = (y < z × x ?<= if C).
Lemma lteif_ndivrMl C z x y :
z < 0 → z^-1 × y < x ?<= if C = (z × x < y ?<= if C).
Interval midpoint.
Local Notation mid x y := ((x + y) / 2).
Lemma midf_le x y : x ≤ y → (x ≤ mid x y) × (mid x y ≤ y).
Lemma midf_lt x y : x < y → (x < mid x y) × (mid x y < y).
Definition midf_lte := (midf_le, midf_lt).
Lemma ler_addgt0Pr x y : reflect (∀ e, e > 0 → x ≤ y + e) (x ≤ y).
Lemma ler_addgt0Pl x y : reflect (∀ e, e > 0 → x ≤ e + y) (x ≤ y).
Lemma lt_le a b : (∀ x, x < a → x < b) → a ≤ b.
Lemma gt_ge a b : (∀ x, b < x → a < x) → a ≤ b.
The AGM, unscaled but without the nth root.
Lemma real_leif_mean_square x y :
x \is real → y \is real → x × y ≤ mid (x ^+ 2) (y ^+ 2) ?= iff (x == y).
Lemma real_leif_AGM2 x y :
x \is real → y \is real → x × y ≤ mid x y ^+ 2 ?= iff (x == y).
Lemma leif_AGM (I : finType) (A : {pred I}) (E : I → F) :
let n := #|A| in let mu := (\sum_(i in A) E i) / n%:R in
{in A, ∀ i, 0 ≤ E i} →
\prod_(i in A) E i ≤ mu ^+ n
?= iff [∀ i in A, ∀ j in A, E i == E j].
Implicit Type p : {poly F}.
Lemma Cauchy_root_bound p : p != 0 → {b | ∀ x, root p x → `|x| ≤ b}.
Lemma natf_indexg (gT : finGroupType) (G H : {group gT}) :
H \subset G → #|G : H|%:R = (#|G|%:R / #|H|%:R)%R :> F.
End NumFieldTheory.
Section RealField.
Variables F : realFieldType.
Implicit Type x y : F.
Lemma leif_mean_square x y : x × y ≤ (x ^+ 2 + y ^+ 2) / 2 ?= iff (x == y).
Lemma leif_AGM2 x y : x × y ≤ ((x + y) / 2)^+ 2 ?= iff (x == y).
Section MinMax.
Lemma maxr_absE x y : Num.max x y = (x + y + `|x - y|) / 2.
Lemma minr_absE x y : Num.min x y = (x + y - `|x - y|) / 2.
End MinMax.
End RealField.
Section RealClosedFieldTheory.
Variable R : rcfType.
Implicit Types a x y : R.
Lemma poly_ivt : real_closed_axiom R.
Square Root theory
Lemma sqrtr_ge0 a : 0 ≤ sqrt a.
Hint Resolve sqrtr_ge0 : core.
Lemma sqr_sqrtr a : 0 ≤ a → sqrt a ^+ 2 = a.
Lemma ler0_sqrtr a : a ≤ 0 → sqrt a = 0.
Lemma ltr0_sqrtr a : a < 0 → sqrt a = 0.
Variant sqrtr_spec a : R → bool → bool → R → Type :=
| IsNoSqrtr of a < 0 : sqrtr_spec a a false true 0
| IsSqrtr b of 0 ≤ b : sqrtr_spec a (b ^+ 2) true false b.
Lemma sqrtrP a : sqrtr_spec a a (0 ≤ a) (a < 0) (sqrt a).
Lemma sqrtr_sqr a : sqrt (a ^+ 2) = `|a|.
Lemma sqrtrM a b : 0 ≤ a → sqrt (a × b) = sqrt a × sqrt b.
Lemma sqrtr0 : sqrt 0 = 0 :> R.
Lemma sqrtr1 : sqrt 1 = 1 :> R.
Lemma sqrtr_eq0 a : (sqrt a == 0) = (a ≤ 0).
Lemma sqrtr_gt0 a : (0 < sqrt a) = (0 < a).
Lemma eqr_sqrt a b : 0 ≤ a → 0 ≤ b → (sqrt a == sqrt b) = (a == b).
Lemma ler_wsqrtr : {homo @sqrt R : a b / a ≤ b}.
Lemma ler_psqrt : {in @nneg R &, {mono sqrt : a b / a ≤ b}}.
Lemma ler_sqrt a b : 0 ≤ b → (sqrt a ≤ sqrt b) = (a ≤ b).
Lemma ltr_sqrt a b : 0 < b → (sqrt a < sqrt b) = (a < b).
Lemma sqrtrV x : 0 ≤ x → sqrt (x^-1) = (sqrt x)^-1.
End RealClosedFieldTheory.
Section ClosedFieldTheory.
Variable C : numClosedFieldType.
Implicit Types a x y z : C.
Definition normCK : ∀ x, `|x| ^+ 2 = x × x^* := normCK_subdef.
Definition sqrCi : 'i ^+ 2 = -1 :> C := sqrCi.
Lemma mulCii : 'i × 'i = -1 :> C.
Lemma conjCK : involutive (@conj C).
Let Re2 z := z + z^*.
Definition nnegIm z := (0 ≤ 'i × (z^* - z)).
Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z ≤ Re2 y).
Variant rootC_spec n (x : C) : Type :=
RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0
& ∀ z, (n > 0)%N → z ^+ n = x → argCle y z.
Fact rootC_subproof n x : rootC_spec n x.
Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y.
Notation "n .-root" := (nthroot n) : ring_scope.
Notation sqrtC := 2.-root.
Fact Re_lock : unit.
Fact Im_lock : unit.
Definition Re z := locked_with Re_lock ((z + z^*) / 2%:R).
Definition Im z := locked_with Im_lock ('i × (z^* - z) / 2%:R).
Notation "'Re z" := (Re z) : ring_scope.
Notation "'Im z" := (Im z) : ring_scope.
Lemma ReE z : 'Re z = (z + z^*) / 2%:R.
Lemma ImE z : 'Im z = 'i × (z^* - z) / 2%:R.
Let nz2 : 2 != 0 :> C.
Lemma normCKC x : `|x| ^+ 2 = x^* × x.
Lemma mul_conjC_ge0 x : 0 ≤ x × x^*.
Lemma mul_conjC_gt0 x : (0 < x × x^* ) = (x != 0).
Lemma mul_conjC_eq0 x : (x × x^* == 0) = (x == 0).
Lemma conjC_ge0 x : (0 ≤ x^* ) = (0 ≤ x).
Lemma conjC_nat n : (n%:R)^* = n%:R :> C.
Lemma conjC0 : 0^* = 0 :> C.
Lemma conjC1 : 1^* = 1 :> C.
Lemma conjCN1 : (- 1)^* = - 1 :> C.
Lemma conjC_eq0 x : (x^* == 0) = (x == 0).
Lemma invC_norm x : x^-1 = `|x| ^- 2 × x^*.
Real number subset.
Lemma CrealE x : (x \is real) = (x^* == x).
Lemma CrealP {x} : reflect (x^* = x) (x \is real).
Lemma conj_Creal x : x \is real → x^* = x.
Lemma conj_normC z : `|z|^* = `|z|.
Lemma CrealJ : {mono (@conj C) : x / x \is Num.real}.
Lemma geC0_conj x : 0 ≤ x → x^* = x.
Lemma geC0_unit_exp x n : 0 ≤ x → (x ^+ n.+1 == 1) = (x == 1).
Elementary properties of roots.
Ltac case_rootC := rewrite /nthroot; case: (rootC_subproof _ _).
Lemma root0C x : 0.-root x = 0.
Lemma rootCK n : (n > 0)%N → cancel n.-root (fun x ⇒ x ^+ n).
Lemma root1C x : 1.-root x = x.
Lemma rootC0 n : n.-root 0 = 0.
Lemma rootC_inj n : (n > 0)%N → injective n.-root.
Lemma eqr_rootC n : (n > 0)%N → {mono n.-root : x y / x == y}.
Lemma rootC_eq0 n x : (n > 0)%N → (n.-root x == 0) = (x == 0).
Rectangular coordinates.
Lemma nonRealCi : ('i : C) \isn't real.
Lemma neq0Ci : 'i != 0 :> C.
Lemma normCi : `|'i| = 1 :> C.
Lemma invCi : 'i^-1 = - 'i :> C.
Lemma conjCi : 'i^* = - 'i :> C.
Lemma Crect x : x = 'Re x + 'i × 'Im x.
Lemma eqCP x y : x = y ↔ ('Re x = 'Re y) ∧ ('Im x = 'Im y).
Lemma eqC x y : (x == y) = ('Re x == 'Re y) && ('Im x == 'Im y).
Lemma Creal_Re x : 'Re x \is real.
Lemma Creal_Im x : 'Im x \is real.
Hint Resolve Creal_Re Creal_Im : core.
Fact Re_is_zmod_morphism : zmod_morphism Re.
#[export]
HB.instance Definition _ := GRing.isZmodMorphism.Build C C Re Re_is_zmod_morphism.
#[warning="-deprecated-since-mathcomp-2.5.0", deprecated(since="mathcomp 2.5.0",
note="use `Re_is_zmod_morphism` instead")]
Definition Re_is_additive := Re_is_zmod_morphism.
Fact Im_is_zmod_morphism : zmod_morphism Im.
#[export]
HB.instance Definition _ := GRing.isZmodMorphism.Build C C Im Im_is_zmod_morphism.
#[warning="-deprecated-since-mathcomp-2.5.0", deprecated(since="mathcomp 2.5.0",
note="use `Im_is_zmod_morphism` instead")]
Definition Im_is_additive := Im_is_zmod_morphism.
Lemma Creal_ImP z : reflect ('Im z = 0) (z \is real).
Lemma Creal_ReP z : reflect ('Re z = z) (z \in real).
Lemma ReMl : {in real, ∀ x, {morph Re : z / x × z}}.
Lemma ReMr : {in real, ∀ x, {morph Re : z / z × x}}.
Lemma ImMl : {in real, ∀ x, {morph Im : z / x × z}}.
Lemma ImMr : {in real, ∀ x, {morph Im : z / z × x}}.
Lemma Re_i : 'Re 'i = 0.
Lemma Im_i : 'Im 'i = 1.
Lemma Re_conj z : 'Re z^* = 'Re z.
Lemma Im_conj z : 'Im z^* = - 'Im z.
Lemma Re_rect : {in real &, ∀ x y, 'Re (x + 'i × y) = x}.
Lemma Im_rect : {in real &, ∀ x y, 'Im (x + 'i × y) = y}.
Lemma conjC_rect : {in real &, ∀ x y, (x + 'i × y)^* = x - 'i × y}.
Lemma addC_rect x1 y1 x2 y2 :
(x1 + 'i × y1) + (x2 + 'i × y2) = x1 + x2 + 'i × (y1 + y2).
Lemma oppC_rect x y : - (x + 'i × y) = - x + 'i × (- y).
Lemma subC_rect x1 y1 x2 y2 :
(x1 + 'i × y1) - (x2 + 'i × y2) = x1 - x2 + 'i × (y1 - y2).
Lemma mulC_rect x1 y1 x2 y2 : (x1 + 'i × y1) × (x2 + 'i × y2) =
x1 × x2 - y1 × y2 + 'i × (x1 × y2 + x2 × y1).
Lemma ImM x y : 'Im (x × y) = 'Re x × 'Im y + 'Re y × 'Im x.
Lemma ImMil x : 'Im ('i × x) = 'Re x.
Lemma ReMil x : 'Re ('i × x) = - 'Im x.
Lemma ReMir x : 'Re (x × 'i) = - 'Im x.
Lemma ImMir x : 'Im (x × 'i) = 'Re x.
Lemma ReM x y : 'Re (x × y) = 'Re x × 'Re y - 'Im x × 'Im y.
Lemma normC2_rect :
{in real &, ∀ x y, `|x + 'i × y| ^+ 2 = x ^+ 2 + y ^+ 2}.
Lemma normC2_Re_Im z : `|z| ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2.
Lemma invC_Crect x y : (x + 'i × y)^-1 = (x^* - 'i × y^*) / `|x + 'i × y| ^+ 2.
Lemma invC_rect :
{in real &, ∀ x y, (x + 'i × y)^-1 = (x - 'i × y) / (x ^+ 2 + y ^+ 2)}.
Lemma ImV x : 'Im x^-1 = - 'Im x / `|x| ^+ 2.
Lemma ReV x : 'Re x^-1 = 'Re x / `|x| ^+ 2.
Lemma rectC_mulr x y z : (x + 'i × y) × z = x × z + 'i × (y × z).
Lemma rectC_mull x y z : z × (x + 'i × y) = z × x + 'i × (z × y).
Lemma divC_Crect x1 y1 x2 y2 :
(x1 + 'i × y1) / (x2 + 'i × y2) =
(x1 × x2^* + y1 × y2^* + 'i × (x2^* × y1 - x1 × y2^*)) /
`|x2 + 'i × y2| ^+ 2.
Lemma divC_rect x1 y1 x2 y2 :
x1 \is real → y1 \is real → x2 \is real → y2 \is real →
(x1 + 'i × y1) / (x2 + 'i × y2) =
(x1 × x2 + y1 × y2 + 'i × (x2 × y1 - x1 × y2)) /
(x2 ^+ 2 + y2 ^+ 2).
Lemma Im_div x y : 'Im (x / y) = ('Re y × 'Im x - 'Re x × 'Im y) / `|y| ^+ 2.
Lemma Re_div x y : 'Re (x / y) = ('Re x × 'Re y + 'Im x × 'Im y) / `|y| ^+ 2.
Lemma leif_normC_Re_Creal z : `|'Re z| ≤ `|z| ?= iff (z \is real).
Lemma leif_Re_Creal z : 'Re z ≤ `|z| ?= iff (0 ≤ z).
Equality from polar coordinates, for the upper plane.
Nth roots.
Let argCleP y z :
reflect (0 ≤ 'Im z → 0 ≤ 'Im y ∧ 'Re z ≤ 'Re y) (argCle y z).
Lemma rootC_Re_max n x y :
(n > 0)%N → y ^+ n = x → 0 ≤ 'Im y → 'Re y ≤ 'Re (n.-root x).
Let neg_unity_root n : (n > 1)%N → exists2 w : C, w ^+ n = 1 & 'Re w < 0.
Lemma Im_rootC_ge0 n x : (n > 1)%N → 0 ≤ 'Im (n.-root x).
Lemma rootC_lt0 n x : (1 < n)%N → (n.-root x < 0) = false.
Lemma rootC_ge0 n x : (n > 0)%N → (0 ≤ n.-root x) = (0 ≤ x).
Lemma rootC_gt0 n x : (n > 0)%N → (n.-root x > 0) = (x > 0).
Lemma rootC_le0 n x : (1 < n)%N → (n.-root x ≤ 0) = (x == 0).
Lemma ler_rootCl n : (n > 0)%N → {in Num.nneg, {mono n.-root : x y / x ≤ y}}.
Lemma ler_rootC n : (n > 0)%N → {in Num.nneg &, {mono n.-root : x y / x ≤ y}}.
Lemma ltr_rootCl n : (n > 0)%N → {in Num.nneg, {mono n.-root : x y / x < y}}.
Lemma ltr_rootC n : (n > 0)%N → {in Num.nneg &, {mono n.-root : x y / x < y}}.
Lemma exprCK n x : (0 < n)%N → 0 ≤ x → n.-root (x ^+ n) = x.
Lemma norm_rootC n x : `|n.-root x| = n.-root `|x|.
Lemma rootCX n x k : (n > 0)%N → 0 ≤ x → n.-root (x ^+ k) = n.-root x ^+ k.
Lemma rootC1 n : (n > 0)%N → n.-root 1 = 1.
Lemma rootCpX n x k : (k > 0)%N → 0 ≤ x → n.-root (x ^+ k) = n.-root x ^+ k.
Lemma rootCV n x : 0 ≤ x → n.-root x^-1 = (n.-root x)^-1.
Lemma rootC_eq1 n x : (n > 0)%N → (n.-root x == 1) = (x == 1).
Lemma rootC_ge1 n x : (n > 0)%N → (n.-root x ≥ 1) = (x ≥ 1).
Lemma rootC_gt1 n x : (n > 0)%N → (n.-root x > 1) = (x > 1).
Lemma rootC_le1 n x : (n > 0)%N → 0 ≤ x → (n.-root x ≤ 1) = (x ≤ 1).
Lemma rootC_lt1 n x : (n > 0)%N → 0 ≤ x → (n.-root x < 1) = (x < 1).
Lemma rootCMl n x z : 0 ≤ x → n.-root (x × z) = n.-root x × n.-root z.
Lemma rootCMr n x z : 0 ≤ x → n.-root (z × x) = n.-root z × n.-root x.
Lemma imaginaryCE : 'i = sqrtC (-1).
More properties of n.-root will be established in cyclotomic.v.
The proper form of the Arithmetic - Geometric Mean inequality.
Lemma leif_rootC_AGM (I : finType) (A : {pred I}) (n := #|A|) E :
{in A, ∀ i, 0 ≤ E i} →
n.-root (\prod_(i in A) E i) ≤ (\sum_(i in A) E i) / n%:R
?= iff [∀ i in A, ∀ j in A, E i == E j].
Square root.
Lemma sqrtC0 : sqrtC 0 = 0.
Lemma sqrtC1 : sqrtC 1 = 1.
Lemma sqrtCK x : sqrtC x ^+ 2 = x.
Lemma sqrCK x : 0 ≤ x → sqrtC (x ^+ 2) = x.
Lemma sqrtC_ge0 x : (0 ≤ sqrtC x) = (0 ≤ x).
Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0).
Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0).
Lemma sqrtC_lt0 x : (sqrtC x < 0) = false.
Lemma sqrtC_le0 x : (sqrtC x ≤ 0) = (x == 0).
Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x ≤ y}}.
Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y}}.
Lemma eqr_sqrtC : {mono sqrtC : x y / x == y}.
Lemma sqrtC_inj : injective sqrtC.
Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x × y}}.
Lemma sqrtC_real x : 0 ≤ x → sqrtC x \in Num.real.
Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 ≤ 'Im x) && ~~ (x < 0)).
Lemma normC_def x : `|x| = sqrtC (x × x^* ).
Lemma norm_conjC x : `|x^*| = `|x|.
Lemma normC_rect :
{in real &, ∀ x y, `|x + 'i × y| = sqrtC (x ^+ 2 + y ^+ 2)}.
Lemma normC_Re_Im z : `|z| = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2).
Norm sum (in)equalities.
Lemma normCDeq x y :
`|x + y| = `|x| + `|y| →
{t : C | `|t| == 1 & (x, y) = (`|x| × t, `|y| × t)}.
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 & ∀ i, P i → F i = `|F i| × t}.
Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I → C) :
`|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) →
(∀ i, P i → `|F i| = 1) →
{t : C | `|t| == 1 & ∀ i, P i → F i = t}.
Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I → C) :
(∀ i, P i → `|F i| ≤ G i) →
\sum_(i | P i) F i = \sum_(i | P i) G i →
∀ i, P i → F i = G i.
Lemma normCBeq x y :
`|x - y| = `|x| - `|y| → {t | `|t| == 1 & (x, y) = (`|x| × t, `|y| × t)}.
End ClosedFieldTheory.
Notation "n .-root" := (@nthroot _ n).
Notation sqrtC := 2.-root.
Notation "'i" := imaginary : ring_scope.
Notation "'Re z" := (Re z) : ring_scope.
Notation "'Im z" := (Im z) : ring_scope.
Arguments conjCK {C} x.
Arguments sqrCK {C} [x] le0x.
Arguments sqrCK_P {C x}.
#[global] Hint Extern 0 (is_true (in_mem ('Re _) _)) ⇒
solve [apply: Creal_Re] : core.
#[global] Hint Extern 0 (is_true (in_mem ('Im _) _)) ⇒
solve [apply: Creal_Im] : core.
Module Export Pdeg2.
Module NumClosed.
Section Pdeg2NumClosed.
Variables (F : numClosedFieldType) (p : {poly F}).
Hypothesis degp : size p = 3.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × a × c.
Let r1 := (- b - sqrtC delta) / (2 × a).
Let r2 := (- b + sqrtC delta) / (2 × a).
Lemma deg2_poly_factor : p = a *: ('X - r1%:P) × ('X - r2%:P).
Lemma deg2_poly_root1 : root p r1.
Lemma deg2_poly_root2 : root p r2.
End Pdeg2NumClosed.
End NumClosed.
Module NumClosedMonic.
Export FieldMonic.
Section Pdeg2NumClosedMonic.
Variables (F : numClosedFieldType) (p : {poly F}).
Hypothesis degp : size p = 3.
Hypothesis monicp : p \is monic.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × c.
Let r1 := (- b - sqrtC delta) / 2.
Let r2 := (- b + sqrtC delta) / 2.
Lemma deg2_poly_factor : p = ('X - r1%:P) × ('X - r2%:P).
Lemma deg2_poly_root1 : root p r1.
Lemma deg2_poly_root2 : root p r2.
End Pdeg2NumClosedMonic.
End NumClosedMonic.
Module Real.
Section Pdeg2Real.
Variable F : realFieldType.
Section Pdeg2RealConvex.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Hypothesis age0 : 0 ≤ a.
Let delta := b ^+ 2 - 4 × a × c.
Let pneq0 : p != 0.
Let aneq0 : a != 0.
Let agt0 : 0 < a.
Let a4gt0 : 0 < 4 × a.
Lemma deg2_poly_min x : p.[- b / (2 × a)] ≤ p.[x].
Lemma deg2_poly_minE : p.[- b / (2 × a)] = - delta / (4 × a).
Lemma deg2_poly_gt0 : reflect (∀ x, 0 < p.[x]) (delta < 0).
Lemma deg2_poly_ge0 : reflect (∀ x, 0 ≤ p.[x]) (delta ≤ 0).
End Pdeg2RealConvex.
Section Pdeg2RealConcave.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Hypothesis ale0 : a ≤ 0.
Let delta := b ^+ 2 - 4 × a × c.
Let degpN : size (- p) = 3.
Let b2a : - (- p)`_1 / (2 × (- p)`_2) = - b / (2 × a).
Let deltaN : (- p)`_1 ^+ 2 - 4 × (- p)`_2 × (- p)`_0 = delta.
Lemma deg2_poly_max x : p.[x] ≤ p.[- b / (2 × a)].
Lemma deg2_poly_maxE : p.[- b / (2 × a)] = - delta / (4 × a).
Lemma deg2_poly_lt0 : reflect (∀ x, p.[x] < 0) (delta < 0).
Lemma deg2_poly_le0 : reflect (∀ x, p.[x] ≤ 0) (delta ≤ 0).
End Pdeg2RealConcave.
End Pdeg2Real.
Section Pdeg2RealClosed.
Variable F : rcfType.
Section Pdeg2RealClosedConvex.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let pneq0 : p != 0.
Let aneq0 : a != 0.
Let sqa2 : 4 × a ^+ 2 = (2 × a) ^+ 2.
Let nz2 : 2 != 0 :> F.
Let delta := b ^+ 2 - 4 × a × c.
Let r1 := (- b - sqrt delta) / (2 × a).
Let r2 := (- b + sqrt delta) / (2 × a).
Lemma deg2_poly_factor : 0 ≤ delta → p = a *: ('X - r1%:P) × ('X - r2%:P).
Lemma deg2_poly_root1 : 0 ≤ delta → root p r1.
Lemma deg2_poly_root2 : 0 ≤ delta → root p r2.
Lemma deg2_poly_noroot : reflect (∀ x, ~~ root p x) (delta < 0).
Hypothesis age0 : 0 ≤ a.
Let agt0 : 0 < a.
Let a2gt0 : 0 < 2 × a.
Let a4gt0 : 0 < 4 × a.
Let aa4gt0 : 0 < 4 × a × a.
Let xb4 x : (x + b / (2 × a)) ^+ 2 × (4 × a × a) = (x × (2 × a) + b) ^+ 2.
Lemma deg2_poly_gt0l x : x < r1 → 0 < p.[x].
Lemma deg2_poly_gt0r x : r2 < x → 0 < p.[x].
Lemma deg2_poly_lt0m x : r1 < x < r2 → p.[x] < 0.
Lemma deg2_poly_ge0l x : x ≤ r1 → 0 ≤ p.[x].
Lemma deg2_poly_ge0r x : r2 ≤ x → 0 ≤ p.[x].
Lemma deg2_poly_le0m x : 0 ≤ delta → r1 ≤ x ≤ r2 → p.[x] ≤ 0.
End Pdeg2RealClosedConvex.
Section Pdeg2RealClosedConcave.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × a × c.
Let r1 := (- b + sqrt delta) / (2 × a).
Let r2 := (- b - sqrt delta) / (2 × a).
Hypothesis ale0 : a ≤ 0.
Let degpN : size (- p) = 3.
Let aNge0 : 0 ≤ (- p)`_2.
Let deltaN : (- p)`_1 ^+ 2 - 4 × (- p)`_2 × (- p)`_0 = delta.
Let r1N : (- (- p)`_1 - sqrt delta) / (2 × (- p)`_2) = r1.
Let r2N : (- (- p)`_1 + sqrt delta) / (2 × (- p)`_2) = r2.
Lemma deg2_poly_lt0l x : x < r1 → p.[x] < 0.
Lemma deg2_poly_lt0r x : r2 < x → p.[x] < 0.
Lemma deg2_poly_gt0m x : r1 < x < r2 → 0 < p.[x].
Lemma deg2_poly_le0l x : x ≤ r1 → p.[x] ≤ 0.
Lemma deg2_poly_le0r x : r2 ≤ x → p.[x] ≤ 0.
Lemma deg2_poly_ge0m x : 0 ≤ delta → r1 ≤ x ≤ r2 → 0 ≤ p.[x].
End Pdeg2RealClosedConcave.
End Pdeg2RealClosed.
End Real.
Module RealMonic.
Import Real.
Export FieldMonic.
Section Pdeg2RealMonic.
Variable F : realFieldType.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Hypothesis monicp : p \is monic.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × c.
Let a1 : a = 1.
Let a2 : 2 × a = 2.
Let a4 : 4 × a = 4.
Lemma deg2_poly_min x : p.[- b / 2] ≤ p.[x].
Let deltam : delta = b ^+ 2 - 4 × a × c.
Lemma deg2_poly_minE : p.[- b / 2] = - delta / 4.
Lemma deg2_poly_gt0 : reflect (∀ x, 0 < p.[x]) (delta < 0).
Lemma deg2_poly_ge0 : reflect (∀ x, 0 ≤ p.[x]) (delta ≤ 0).
End Pdeg2RealMonic.
Section Pdeg2RealClosedMonic.
Variables (F : rcfType) (p : {poly F}).
Hypothesis degp : size p = 3.
Hypothesis monicp : p \is monic.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let a1 : a = 1.
Let delta := b ^+ 2 - 4 × c.
Let deltam : delta = b ^+ 2 - 4 × a × c.
Let r1 := (- b - sqrt delta) / 2.
Let r2 := (- b + sqrt delta) / 2.
Let nz2 : 2 != 0 :> F.
Lemma deg2_poly_factor : 0 ≤ delta → p = ('X - r1%:P) × ('X - r2%:P).
Lemma deg2_poly_root1 : 0 ≤ delta → root p r1.
Lemma deg2_poly_root2 : 0 ≤ delta → root p r2.
Lemma deg2_poly_noroot : reflect (∀ x, ~~ root p x) (delta < 0).
Lemma deg2_poly_gt0l x : x < r1 → 0 < p.[x].
Lemma deg2_poly_gt0r x : r2 < x → 0 < p.[x].
Lemma deg2_poly_lt0m x : r1 < x < r2 → p.[x] < 0.
Lemma deg2_poly_ge0l x : x ≤ r1 → 0 ≤ p.[x].
Lemma deg2_poly_ge0r x : r2 ≤ x → 0 ≤ p.[x].
Lemma deg2_poly_le0m x : 0 ≤ delta → r1 ≤ x ≤ r2 → p.[x] ≤ 0.
End Pdeg2RealClosedMonic.
End RealMonic.
End Pdeg2.
Section Degle2PolyRealConvex.
Variable (F : realFieldType) (p : {poly F}).
Hypothesis degp : (size p ≤ 3)%N.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × a × c.
Lemma deg_le2_poly_delta_ge0 : 0 ≤ a → (∀ x, 0 ≤ p.[x]) → delta ≤ 0.
End Degle2PolyRealConvex.
Section Degle2PolyRealConcave.
Variable (F : realFieldType) (p : {poly F}).
Hypothesis degp : (size p ≤ 3)%N.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × a × c.
Lemma deg_le2_poly_delta_le0 : a ≤ 0 → (∀ x, p.[x] ≤ 0) → delta ≤ 0.
End Degle2PolyRealConcave.
Section Degle2PolyRealClosedConvex.
Variable (F : rcfType) (p : {poly F}).
Hypothesis degp : (size p ≤ 3)%N.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × a × c.
Lemma deg_le2_poly_ge0 : (∀ x, 0 ≤ p.[x]) → delta ≤ 0.
End Degle2PolyRealClosedConvex.
Section Degle2PolyRealClosedConcave.
Variable (F : rcfType) (p : {poly F}).
Hypothesis degp : (size p ≤ 3)%N.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let delta := b ^+ 2 - 4 × a × c.
Lemma deg_le2_poly_le0 : (∀ x, p.[x] ≤ 0) → delta ≤ 0.
End Degle2PolyRealClosedConcave.
End Theory.
Module Exports. End Exports.
End Num.
Export Num.Exports Num.Syntax.