Library Coqtail.Complex.Cdefinitions


Require Export Reals.
Require Export Fourier.

Open Scope R_scope.

Definition of C and basic operations over C


Definition C : Set := (prod R R).

Definition R_R_to_C (a : R) (b : R) : C := (a, b).


Delimit Scope C_scope with C.

Bind Scope C_scope with C.

Open Scope C_scope.

Basic definitions and notations


Definition C0 := R_R_to_C 0 0.
Definition C1 := R_R_to_C 1 0.
Definition Ci := R_R_to_C 0 1.

Notation "0" := C0.
Notation "1" := C1.

Definition Cre (z : C) : R :=
  let (r1, i1) := z in
  r1.

Definition Cim (z : C) : R :=
  let (r1, i1) := z in
  i1.

Definition Cadd (z1 : C) (z2 : C) : C :=
  R_R_to_C (Cre z1 + Cre z2) (Cim z1 + Cim z2).

Definition Cmult (z1 : C) (z2 : C) : C :=
  R_R_to_C (Cre z1 × Cre z2 - Cim z1 × Cim z2) (Cre z1 × Cim z2 + Cim z1 × Cre z2).

Definition Copp (z1 : C) :C :=
  R_R_to_C (-Cre z1) (-Cim z1).

Definition Cinv (z1 : C) : C :=
  R_R_to_C (Cre z1 / (Cre z1 × Cre z1 + Cim z1 × Cim z1)) (-Cim z1 / (Cre z1 × Cre z1 + Cim z1 × Cim z1)).

Definition Cconj (z1 : C) : C :=
  R_R_to_C (Cre z1) (-Cim z1).

Definition Cnorm_sqr (z1 : C) : R :=
  (Cre z1 × Cre z1 + Cim z1 × Cim z1).

Definition Cnorm (z1 : C) : R :=
  (sqrt (Cnorm_sqr z1)).

Definition Cscal (lambda : R) (z : C) : C :=
  R_R_to_C (lambda × Cre z) (lambda × Cim z).

Definition IRC (x : R) : C := (R_R_to_C x 0%R).

Coercion IRC : R >-> C.

Infix "+" := Cadd : C_scope.
Infix "×" := Cmult : C_scope.
Notation "- z" := (Copp z) : C_scope.
Notation "/ z" := (Cinv z) : C_scope.
Infix "`*" := Cscal (at level 0): C_scope.

Definition Cminus (c1 c2 : C) : C := c1 + - c2.

Definition Cdiv (c1 c2 : C) : C := c1 × / c2.

Infix "-" := Cminus : C_scope.
Infix "/" := Cdiv : C_scope.

Infix " '+i' " := R_R_to_C (at level 60) : C_scope.

Injection from N to C


Fixpoint INC (n:nat) : C :=
  match n with
  | O ⇒ 0
  | S O ⇒ 1
  | S nINC n + 1
  end.
Arguments Scope INC [nat_scope].

Injection from Z to C


Definition IZC (z:Z) : C :=
  match z with
  | Z0 ⇒ 0
  | Zpos nINC (nat_of_P n)
  | Zneg n- INC (nat_of_P n)
  end.
Arguments Scope IZC [Z_scope].