Library Coquelicot.Complex
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
From Coq Require Import Reals ssreflect.
Require Import Rcomplements Rbar Continuity Derive Hierarchy.
This file defines complex numbers C as R × R. Operations are
given, and C is proved to be a field, a normed module, and a
complete space.
The set of complex numbers
Definition C := (R × R)%type.
Definition RtoC (x : R) : C := (x,0).
Coercion RtoC : R >-> C.
Lemma RtoC_inj : ∀ (x y : R),
RtoC x = RtoC y → x = y.
Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 ≠ z2 }.
Definition Cplus (x y : C) : C := (fst x + fst y, snd x + snd y).
Definition Copp (x : C) : C := (-fst x, -snd x).
Definition Cminus (x y : C) : C := Cplus x (Copp y).
Definition Cmult (x y : C) : C := (fst x × fst y - snd x × snd y, fst x × snd y + snd x × fst y).
Definition Cinv (x : C) : C := (fst x / (fst x ^ 2 + snd x ^ 2), - snd x / (fst x ^ 2 + snd x ^ 2)).
Definition Cdiv (x y : C) : C := Cmult x (Cinv y).
Delimit Scope C_scope with C.
Bind Scope C_scope with C.
Local Open Scope C_scope.
Infix "+" := Cplus : C_scope.
Notation "- x" := (Copp x) : C_scope.
Infix "-" := Cminus : C_scope.
Infix "×" := Cmult : C_scope.
Notation "/ x" := (Cinv x) : C_scope.
Infix "/" := Cdiv : C_scope.
Definition Re (z : C) : R := fst z.
Definition Im (z : C) : R := snd z.
Definition Cmod (x : C) : R := sqrt (fst x ^ 2 + snd x ^ 2).
Definition Cconj (x : C) : C := (fst x, (- snd x)%R).
Lemma Cmod_0 : Cmod 0 = 0.
Lemma Cmod_1 : Cmod 1 = 1.
Lemma Cmod_Ci : Cmod Ci = 1.
Lemma Cmod_opp : ∀ x, Cmod (-x) = Cmod x.
Lemma Cmod_triangle : ∀ x y, Cmod (x + y) ≤ Cmod x + Cmod y.
Lemma Cmod_mult : ∀ x y, Cmod (x × y) = (Cmod x × Cmod y)%R.
Lemma Rmax_Cmod : ∀ x,
Rmax (Rabs (fst x)) (Rabs (snd x)) ≤ Cmod x.
Lemma Cmod_2Rmax : ∀ x,
Cmod x ≤ sqrt 2 × Rmax (Rabs (fst x)) (Rabs (snd x)).
Lemma RtoC_plus (x y : R) :
RtoC (x + y) = RtoC x + RtoC y.
Lemma RtoC_opp (x : R) :
RtoC (- x) = - RtoC x.
Lemma RtoC_minus (x y : R) :
RtoC (x - y) = RtoC x - RtoC y.
Lemma RtoC_mult (x y : R) :
RtoC (x × y) = RtoC x × RtoC y.
Lemma RtoC_inv (x : R) : (x ≠ 0)%R → RtoC (/ x) = / RtoC x.
Lemma RtoC_div (x y : R) : (y ≠ 0)%R → RtoC (x / y) = RtoC x / RtoC y.
Lemma Cplus_comm (x y : C) : x + y = y + x.
Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.
Lemma Cplus_0_r (x : C) : x + 0 = x.
Lemma Cplus_0_l (x : C) : 0 + x = x.
Lemma Cplus_opp_r (x : C) : x + -x = 0.
Lemma Copp_plus_distr (z1 z2 : C) : - (z1 + z2) = (- z1 + - z2).
Lemma Copp_minus_distr (z1 z2 : C) : - (z1 - z2) = z2 - z1.
Lemma Cmult_comm (x y : C) : x × y = y × x.
Lemma Cmult_assoc (x y z : C) : x × (y × z) = (x × y) × z.
Lemma Cmult_0_r (x : C) : x × 0 = 0.
Lemma Cmult_0_l (x : C) : 0 × x = 0.
Lemma Cmult_1_r (x : C) : x × 1 = x.
Lemma Cmult_1_l (x : C) : 1 × x = x.
Lemma Cinv_r (r : C) : r ≠ 0 → r × /r = 1.
Lemma Cinv_l (r : C) : r ≠ 0 → /r × r = 1.
Lemma Cmult_plus_distr_l (x y z : C) : x × (y + z) = x × y + x × z.
Lemma Cmult_plus_distr_r (x y z : C) : (x + y) × z = x × z + y × z.
Definition C_AbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ Cplus_comm Cplus_assoc Cplus_0_r.
Canonical C_AbelianMonoid :=
AbelianMonoid.Pack C C_AbelianMonoid_mixin C.
Definition C_AbelianGroup_mixin :=
AbelianGroup.Mixin _ _ Cplus_opp_r.
Canonical C_AbelianGroup :=
AbelianGroup.Pack C (AbelianGroup.Class _ _ C_AbelianGroup_mixin) C.
Lemma Copp_0 : Copp 0 = 0.
Definition C_Ring_mixin :=
Ring.Mixin _ _ _ Cmult_assoc Cmult_1_r Cmult_1_l Cmult_plus_distr_r Cmult_plus_distr_l.
Canonical C_Ring :=
Ring.Pack C (Ring.Class _ _ C_Ring_mixin) C.
Lemma Cmod_m1 :
Cmod (Copp 1) = 1.
Lemma Cmod_eq_0 :
∀ x, Cmod x = 0 → x = 0.
Definition C_AbsRing_mixin :=
AbsRing.Mixin _ _ Cmod_0 Cmod_m1 Cmod_triangle (fun x y ⇒ Req_le _ _ (Cmod_mult x y)) Cmod_eq_0.
Canonical C_AbsRing :=
AbsRing.Pack C (AbsRing.Class _ _ C_AbsRing_mixin) C.
Lemma Cmod_ge_0 :
∀ x, 0 ≤ Cmod x.
Lemma Cmod_gt_0 :
∀ (x : C), x ≠ 0 ↔ 0 < Cmod x.
Lemma Cmod_norm :
∀ x : C, Cmod x = (@norm R_AbsRing _ x).
Lemma Cmod_R :
∀ x : R, Cmod x = Rabs x.
Lemma Cmod_inv :
∀ x : C, x ≠ 0 → Cmod (/ x) = Rinv (Cmod x).
Lemma Cmod_div (x y : C) : y ≠ 0 →
Cmod (x / y) = Rdiv (Cmod x) (Cmod y).
Lemma Cmult_neq_0 (z1 z2 : C) : z1 ≠ 0 → z2 ≠ 0 → z1 × z2 ≠ 0.
Lemma Ceq_minus (c c' : C) : c = c' ↔ c-c' = 0.
Lemma Cminus_eq_contra : ∀ r1 r2 : C, r1 ≠ r2 → r1 - r2 ≠ 0.
Lemma C1_nz : RtoC 1 ≠ 0.
Lemma Ci_nz : Ci ≠ 0.
A power function : c^n
Fixpoint Cpow (c : C) n : C :=
match n with
| O ⇒ 1
| S n ⇒ c × Cpow c n
end.
Infix "^" := Cpow : C_scope.
Lemma Cpow_1_l n : 1^n = 1.
Lemma Cpow_1_r c : c^1 = c.
Lemma Cpow_S c n : c^(S n) = c×c^n.
Lemma Cpow_add_r c n m : c^(n+m) = c^n×c^m.
Lemma Cpow_mult_l a b n : (a×b)^n = a^n × b^n.
Lemma Cpow_mult_r c n m : c^(n×m) = (c^n)^m.
Lemma Cpow_nz (c:C) n : c ≠ 0 → c^n ≠ 0.
Lemma Cmod_pow (c:C) n : Cmod (c^n) = (Cmod c ^n)%R.
Definition C_ring_morph :
ring_morph (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp (@eq C)
0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb (fun z ⇒ RtoC (IZR z)).
Lemma C_power_theory : @power_theory C 1 Cmult (@eq C) _ N.to_nat Cpow.
Ltac RtoC_IZR_tac t :=
match t with
| RtoC ?x ⇒ IZR_tac x
| _ ⇒ constr:(NotConstant)
end.
Lemma C_ring_theory : ring_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp eq.
Add Ring C_ring_ring :
C_ring_theory
(morphism C_ring_morph,
constants [RtoC_IZR_tac],
power_tac C_power_theory [Rpow_tac]).
Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.
Lemma Zeqb_Ccomplete z z' : RtoC (IZR z) = RtoC (IZR z') → Z.eqb z z' = true.
Add Field C_field_field :
C_field_theory
(morphism C_ring_morph,
completeness Zeqb_Ccomplete,
constants [RtoC_IZR_tac],
power_tac C_power_theory [Rpow_tac]).
Some other basic properties
Lemma Cpow_inv (c:C) n : c≠0 → (/c)^n = /(c^n).
Lemma Cmod2_alt (c:C) : (Cmod c ^2 = Re c ^2 + Im c ^2)%R.
Lemma Cmod2_conj (c:C) : RtoC (Cmod c ^2) = c × Cconj c.
Lemma re_alt (c:C) : RtoC (Re c) = (c + Cconj c)/2.
Lemma im_alt (c:C) : RtoC (Im c) = (c - Cconj c)/(2×Ci).
Lemma im_alt' (c:C) : c - Cconj c = 2×Ci×Im c.
Lemma re_conj (c:C) : Re (Cconj c) = Re c.
Lemma im_conj (c:C) : Im (Cconj c) = (- Im c)%R.
Lemma re_plus a b : (Re (a+b) = Re a + Re b)%R.
Lemma re_opp a : (Re (-a) = - Re a)%R.
Lemma re_mult a b : (Re (a×b) = Re a × Re b - Im a × Im b)%R.
Lemma im_plus a b : (Im (a+b) = Im a + Im b)%R.
Lemma im_opp a : (Im (-a) = - Im a)%R.
Lemma im_mult a b : (Im (a×b) = Re a × Im b + Im a × Re b)%R.
Lemma re_RtoC (r:R) : Re (RtoC r) = r.
Lemma im_RtoC (r:R) : Im (RtoC r) = 0.
Lemma re_scal_l (r:R)(c:C) : (Re (r×c) = r × Re c)%R.
Lemma re_scal_r (c:C)(r:R) : (Re (c×r) = Re c × r)%R.
Lemma im_scal_l (r:R)(c:C) : (Im (r×c) = r × Im c)%R.
Lemma im_scal_r (c:C)(r:R) : (Im (c×r) = Im c × r)%R.
Lemma Cconj_conj (c:C) : Cconj (Cconj c) = c.
Lemma Cplus_conj a b : Cconj (a+b) = Cconj a + Cconj b.
Lemma Cmult_conj a b : Cconj (a×b) = Cconj a × Cconj b.
Lemma Copp_conj a : Cconj (-a) = - Cconj a.
Lemma Cminus_conj a b : Cconj (a-b) = Cconj a - Cconj b.
Lemma Cinv_conj (a:C) : a≠0 → Cconj (/a) = /Cconj a.
Lemma Cdiv_conj (a b : C) : b≠0 → Cconj (a/b) = Cconj a / Cconj b.
Lemma Cpow_conj a n : Cconj (a^n) = (Cconj a)^n.
Lemma Cmod_conj (c:C) : Cmod (Cconj c) = Cmod c.
Lemma RtoC_pow (a:R)(n:nat) : RtoC (a^n) = (RtoC a)^n.
Lemma Ci_inv : /Ci = -Ci.
Lemma re_mult_Ci (c:C) : (Re (c×Ci) = - Im c)%R.
Lemma re_le_Cmod (c:C) : Rabs (Re c) ≤ Cmod c.
on C (with the balls of R^2)
Canonical C_ModuleSpace :=
ModuleSpace.Pack C_Ring C (ModuleSpace.class _ (Ring_ModuleSpace C_Ring)) C.
Canonical C_NormedModuleAux :=
NormedModuleAux.Pack C_AbsRing C (NormedModuleAux.Class C_AbsRing _ (ModuleSpace.class _ C_ModuleSpace) (UniformSpace.class C_UniformSpace)) C.
Lemma C_NormedModule_mixin_compat1 :
∀ (x y : C) (eps : R),
Cmod (minus y x) < eps → ball x eps y.
Lemma C_NormedModule_mixin_compat2 :
∀ (x y : C_NormedModuleAux) (eps : posreal),
ball x eps y → Cmod (minus y x) < sqrt 2 × eps.
Definition C_NormedModule_mixin :=
NormedModule.Mixin _ C_NormedModuleAux _ _ Cmod_triangle (fun x y ⇒ Req_le _ _ (Cmod_mult x y))
C_NormedModule_mixin_compat1 C_NormedModule_mixin_compat2 Cmod_eq_0.
Canonical C_NormedModule :=
NormedModule.Pack C_AbsRing C (NormedModule.Class _ _ _ C_NormedModule_mixin) C.
on R
Canonical C_R_ModuleSpace :=
ModuleSpace.Pack R_Ring C (ModuleSpace.class _ (prod_ModuleSpace R_Ring R_ModuleSpace R_ModuleSpace)) C.
Canonical C_R_NormedModuleAux :=
NormedModuleAux.Pack R_AbsRing C (NormedModuleAux.Class R_AbsRing _ (ModuleSpace.class _ C_R_ModuleSpace) (UniformSpace.class _)) C.
Canonical C_R_NormedModule :=
NormedModule.Pack R_AbsRing C (NormedModule.class _ (prod_NormedModule _ _ _)) C.
Lemma scal_R_Cmult :
∀ (x : R) (y : C),
scal (V := C_R_ModuleSpace) x y = Cmult x y.
Definition C_complete_lim (F : (C → Prop) → Prop) :=
(R_complete_lim (fun P ⇒ F (fun z ⇒ P (Re z))), R_complete_lim (fun P ⇒ F (fun z ⇒ P (Im z)))).
Lemma C_complete_ax1 :
∀ F : (C → Prop) → Prop,
ProperFilter F →
(∀ eps : posreal, ∃ x : C, F (ball x eps)) →
∀ eps : posreal, F (ball (C_complete_lim F) eps).
Lemma C_complete_ax2 :
∀ F1 F2 : (C → Prop) → Prop,
filter_le F1 F2 →
filter_le F2 F1 →
close (C_complete_lim F1) (C_complete_lim F2).
Definition C_CompleteSpace_mixin :=
CompleteSpace.Mixin _ C_complete_lim C_complete_ax1 C_complete_ax2.
Canonical C_CompleteNormedModule :=
CompleteNormedModule.Pack _ C (CompleteNormedModule.Class C_AbsRing _ (NormedModule.class _ C_NormedModule) C_CompleteSpace_mixin) C.
Canonical C_R_CompleteNormedModule :=
CompleteNormedModule.Pack _ C (CompleteNormedModule.Class R_AbsRing _ (NormedModule.class _ C_R_NormedModule) C_CompleteSpace_mixin) C.
Lemma locally_C x P :
locally (T := C_UniformSpace) x P ↔ locally (T := AbsRing_UniformSpace C_AbsRing) x P.