Library Coquelicot.Complex

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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.

Require Import Reals mathcomp.ssreflect.ssreflect.
Require Import Rcomplements Rbar.
Require Import 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 }.

Constants and usual functions

0 and 1 for complex are defined as RtoC 0 and RtoC 1

Definition Ci : C := (0,1).

Arithmetic operations

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.
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.

Other usual functions

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_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)).

C is a field

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_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Cplus_comm Cplus_assoc Cplus_0_r Cplus_opp_r.

Canonical C_AbelianGroup :=
  AbelianGroup.Pack C 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 Cminus_eq_contra : ∀ r1 r2 : C, r1 ≠ r2 → r1 - r2 ≠ 0.

Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.

Add Field C_field_field : C_field_theory.

C is a NormedModule

Canonical C_UniformSpace :=
UniformSpace.Pack C (UniformSpace.class (prod_UniformSpace _ _)) 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.

C is a CompleteSpace

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.

Locally compat

Lemma locally_C x P :
locally (T := C_UniformSpace) x P ↔ locally (T := AbsRing_UniformSpace C_AbsRing) x P.

Limits

Definition C_lim (f : C → C) (z : C) : C :=
  (real (Lim (fun x ⇒ fst (f (x , snd z ))) (fst z)),
  real (Lim (fun x ⇒ snd (f (x , snd z ))) (fst z))).

Lemma is_C_lim_unique (f : C → C) (z l : C) :
  filterlim f (locally' z) (locally l) → C_lim f z = l.

Derivatives

Definition C_derive (f : C → C) (z : C) := C_lim (fun x ⇒ (f x - f z ) / (x - z )) z.

Lemma is_C_derive_unique (f : C → C) (z l : C) :
is_derive f z l → C_derive f z = l.
Lemma C_derive_correct (f : C → C) (z l : C) :
ex_derive f z → is_derive f z (C_derive f z).