Complex Numbers

Algebraic structure

Section Complex_Numbers.
Record CC_set : Type :=
  {ℜ : IR;
   ℑ : IR}.

Definition cc_ap (x y : CC_set) : CProp := ℜ x [#] ℜ y or ℑ x [#] ℑ y.

Definition cc_eq (x y : CC_set) : Prop := ℜ x [=] ℜ y /\ ℑ x [=] ℑ y.

Lemma cc_is_CSetoid : is_CSetoid _ cc_eq cc_ap.

Definition cc_csetoid := Build_CSetoid CC_set cc_eq cc_ap cc_is_CSetoid.

Definition cc_plus x y := Build_CC_set (ℜ x[+]ℜ y) (ℑ x[+]ℑ y).

Definition cc_mult x y := Build_CC_set (ℜ x[*]ℜ y[-]ℑ x[*]ℑ y) (ℜ x[*]ℑ y[+]ℑ x[*]ℜ y).

Definition cc_zero := Build_CC_set 0 0.

Definition cc_one := Build_CC_set 1 0.

Definition cc_i := Build_CC_set 0 1.

Definition cc_inv (x : CC_set) : CC_set := Build_CC_set [--] (ℜ x) [--] (ℑ x).

Lemma cc_inv_strext : un_op_strext cc_csetoid cc_inv.

Lemma cc_plus_strext : bin_op_strext cc_csetoid cc_plus.

Lemma cc_mult_strext : bin_op_strext cc_csetoid cc_mult.

Definition cc_inv_op := Build_CSetoid_un_op _ _ cc_inv_strext.

Definition cc_plus_op := Build_CSetoid_bin_op _ _ cc_plus_strext.

Definition cc_mult_op := Build_CSetoid_bin_op _ _ cc_mult_strext.

Lemma cc_csg_associative : associative cc_plus_op.

Lemma cc_cr_mult_associative : associative cc_mult_op.

Definition cc_csemi_grp := Build_CSemiGroup cc_csetoid _ cc_csg_associative.

Lemma cc_cm_proof : is_CMonoid cc_csemi_grp cc_zero.

Definition cc_cmonoid := Build_CMonoid _ _ cc_cm_proof.

Lemma cc_cg_proof : is_CGroup cc_cmonoid cc_inv_op.

Lemma cc_cr_dist : distributive cc_mult_op cc_plus_op.

Lemma cc_cr_non_triv : cc_ap cc_one cc_zero.

Definition cc_cgroup := Build_CGroup cc_cmonoid cc_inv_op cc_cg_proof.

Definition cc_cabgroup : CAbGroup.
Defined.

Lemma cc_cr_mult_mon : is_CMonoid
   (Build_CSemiGroup (csg_crr cc_cgroup) _ cc_cr_mult_associative) cc_one.

Lemma cc_mult_commutes : commutes cc_mult_op.

Lemma cc_isCRing : is_CRing cc_cabgroup cc_one cc_mult_op.

Definition cc_cring : CRing := Build_CRing _ _ _ cc_isCRing.

Lemma cc_ap_zero : forall z : cc_cring, z [#] 0 -> ℜ z [#] 0 or ℑ z [#] 0.

Lemma cc_inv_aid : forall x y : IR, x [#] 0 or y [#] 0 -> x[^]2[+]y[^]2 [#] 0.

If x ≠ 0 or y ≠ 0, then x / x^2 + y^2 ≠ 0 or −y/x^2+y^2 ≠ 0.

Lemma cc_inv_aid2 : forall (x y : IR) (H : x [#] 0 or y [#] 0),
(x[/] _[//]cc_inv_aid _ _ H) [#] 0 or ( [--]y[/] _[//]cc_inv_aid _ _ H) [#] 0.

Definition cc_recip : forall z : cc_cring, z [#] 0 -> cc_cring.
Defined.

Lemma cc_cfield_proof : is_CField cc_cring cc_recip.

Lemma cc_Recip_proof : forall x y x_ y_, cc_recip x x_ [#] cc_recip y y_ -> x [#] y.

Definition cc_cfield := Build_CField _ _ cc_cfield_proof cc_Recip_proof.

Definition C := cc_cfield.

Maps from reals to complex and vice-versa are defined, as well as conjugate, absolute value and the imaginary unit I

Definition cc_set_CC : IR -> IR -> C := Build_CC_set.

Definition cc_IR (x : IR) : C := cc_set_CC x 0.

Definition CC_conj : C -> C := fun z : CC_set =>
  match z with
  | Build_CC_set Re0 Im0 => Build_CC_set Re0 [--]Im0
  end.

Definition AbsCC (z : C) : IR := sqrt (ℜ z[^]2[+]ℑ z[^]2) (cc_abs_aid _ (ℜ z) (ℑ z)).

Lemma TwoCC_ap_zero : (2:CC) [#] 0.

End Complex_Numbers.

Definition i : C := cc_i.

Infix "[+I*]" := cc_set_CC (at level 48, no associativity).

Properties of i

Section I_properties.

Lemma I_square : i[*]i [=] [--]1.

Lemma I_square' : i[^]2 [=] [--]1.

Lemma I_recip_lft : [--]i[*]i [=] 1.

Lemma I_recip_rht : i[*][--]i [=] 1.

Lemma mult_I : forall x y : IR, (x[+I*]y) [*]i [=] [--]y[+I*]x.

Lemma I_wd : forall x x' y y' : IR, x [=] x' -> y [=] y' -> x[+I*]y [=] x'[+I*]y'.

Properties of ℜ and ℑ

Lemma calculate_norm : forall x y : IR, (x[+I*]y) [*]CC_conj (x[+I*]y) [=] cc_IR (x[^]2[+]y[^]2).

Lemma calculate_Re : forall c : C, cc_IR (ℜ c) [*]2 [=] c[+]CC_conj c.

Lemma calculate_Im : forall c : C, cc_IR (ℑ c) [*] (2[*]i) [=] c[-]CC_conj c.

Lemma Re_wd : forall c c' : C, c [=] c' -> ℜ c [=] ℜ c'.

Lemma Im_wd : forall c c' : C, c [=] c' -> ℑ c [=] ℑ c'.

Lemma Re_resp_plus : forall x y : C, ℜ (x[+]y) [=] ℜ x[+]ℜ y.

Lemma Re_resp_inv : forall x y : C, ℜ (x[-]y) [=] ℜ x[-]ℜ y.

Lemma Im_resp_plus : forall x y : C, ℑ (x[+]y) [=] ℑ x[+]ℑ y.

Lemma Im_resp_inv : forall x y : C, ℑ (x[-]y) [=] ℑ x[-]ℑ y.

Lemma cc_calculate_square : forall x y, (x[+I*]y) [^]2 [=] (x[^]2[-]y[^]2) [+I*]x[*]y[*]2.

End I_properties.

Properties of conjugation

Section Conj_properties.

Lemma CC_conj_plus : forall c c' : C, CC_conj (c[+]c') [=] CC_conj c[+]CC_conj c'.

Lemma CC_conj_mult : forall c c' : C, CC_conj (c[*]c') [=] CC_conj c[*]CC_conj c'.

Lemma CC_conj_strext : forall c c' : C, CC_conj c [#] CC_conj c' -> c [#] c'.

Lemma CC_conj_conj : forall c : C, CC_conj (CC_conj c) [=] c.

Lemma CC_conj_zero : CC_conj 0 [=] 0.

Lemma CC_conj_one : CC_conj 1 [=] 1.

Lemma CC_conj_nexp : forall (c : C) n, CC_conj (c[^]n) [=] CC_conj c[^]n.

End Conj_properties.

Properties of the real axis

Section cc_IR_properties.

Lemma Re_cc_IR : forall x : IR, ℜ (cc_IR x) [=] x.

Lemma Im_cc_IR : forall x : IR, ℑ (cc_IR x) [=] 0.

Lemma cc_IR_wd : forall x y : IR, x [=] y -> cc_IR x [=] cc_IR y.

Lemma cc_IR_resp_ap : forall x y : IR, x [#] y -> cc_IR x [#] cc_IR y.

Lemma cc_IR_mult : forall x y : IR, cc_IR x[*]cc_IR y [=] cc_IR (x[*]y).

Lemma cc_IR_mult_lft : forall x y z, (x[+I*]y) [*]cc_IR z [=] x[*]z[+I*]y[*]z.

Lemma cc_IR_mult_rht : forall x y z, cc_IR z[*] (x[+I*]y) [=] z[*]x[+I*]z[*]y.

Lemma cc_IR_plus : forall x y : IR, cc_IR x[+]cc_IR y [=] cc_IR (x[+]y).

Lemma cc_IR_minus : forall x y : IR, cc_IR x[-]cc_IR y [=] cc_IR (x[-]y).

Lemma cc_IR_zero : cc_IR 0 [=] 0.

Lemma cc_IR_one : cc_IR 1 [=] 1.

Lemma cc_IR_nring : forall n : N, cc_IR (nring n) [=] nring n.

Lemma cc_IR_nexp : forall (x : IR) (n : N), cc_IR x[^]n [=] cc_IR (x[^]n).

End cc_IR_properties.

C has characteristic zero

Lemma char0_CC : Char0 C.

Lemma poly_apzero_CC : forall f : C[X], f [#] 0 -> {c : C | f ! c [#] 0}.

Lemma poly_CC_extensional : forall p q : C[X], (forall x, p ! x [=] q ! x) -> p [=] q.