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.

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 yReq_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)
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 PF (fun zP (Re z))), R_complete_lim (fun PF (fun zP (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

Limits


Definition C_lim (f : C C) (z : C) : C :=
  (real (Lim (fun xfst (f (x, snd z))) (fst z)),
  real (Lim (fun xsnd (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).