Library Coqtail.Complex.Cpolar


Require Import Rbase.
Require Import AltSeries.
Require Import Rseries_def.
Require Import Rtrigo_facts Ratan.
Require Import Cpow_plus.
Require Export Complex.
Require Import Fourier MyRIneq.

Open Scope R_scope.

Lemma sqrt_no_R0 : z : R, 0 < zsqrt z 0.
Proof.
intros z z_pos Hf ; destruct (Rlt_irrefl 0) ; eapply Rlt_le_trans ;
 [| right ; eapply sqrt_eq_0 ; [left |]] ; eassumption.
Qed.

Lemma Rmult_0_lt_compat : a, a < 0 → 0 < a × a.
Proof.
intros a a_neg ; apply Rlt_le_trans with ((- a) × (- a)) ;
 [| right ; ring] ; apply Rmult_lt_0_compat ; fourier.
Qed.

Lemma Rle_neq_Rlt : a b, a ba ba < b.
Proof.
intros a b a_le a_neq ; destruct (Rlt_le_dec a b) ;
 [| destruct a_neq ; apply Rle_antisym] ; assumption.
Qed.

Lemma sqr_pos_lt : a, a 0 → 0 < a × a.
Proof.
intros a a_neq ; destruct (Rlt_le_dec a 0).
 apply Rmult_0_lt_compat ; assumption.
 apply Rmult_lt_0_compat ; apply Rle_neq_Rlt ;
  (assumption || symmetry ; assumption).
Qed.

Lemma sqr_pos : b, 0 b × b.
Proof.
intro ; rewrite <- Rmult_1_r, Rmult_assoc ; apply sqr_pos.
Qed.

Every complex number has polar coordinate


Lemma exists_polar_form : z : C,
  { r : R & { theta : R | z = r × cos (theta) +i r × sin (theta) } }.
Proof.
intros [a b] ; destruct (total_order_T a R0) as [[a_neg | a_eq] | a_pos].
 assert (Hrew : (sqrt (1 + (b / a) ^ 2) = sqrt (a × a + b × b) / sqrt ((- a) × - a))%R).
  simpl ; repeat rewrite Rmult_1_r ; rewrite <- sqrt_div.
   f_equal ; field ; apply Rlt_not_eq ; assumption.
   left ; apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rlt_not_eq ; assumption |
    apply sqr_pos].
   apply sqr_pos_lt, Rgt_not_eq ; fourier.
  (- Cnorm (a +i b))%R ; (Ratan.atan (Cim (a +i b) / Cre (a +i b))) ;
 CusingR_simpl.
 rewrite cos_atan ; unfold Cnorm, Cnorm_sqr ;
  rewrite Hrew ; simpl ; rewrite sqrt_square.
  field ; split ; [apply Rlt_not_eq | apply sqrt_no_R0].
   assumption.
   apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rlt_not_eq ; assumption |
    apply sqr_pos].
   fourier.
 rewrite sin_atan ; unfold Cnorm, Cnorm_sqr ;
  rewrite Hrew ; simpl ; rewrite sqrt_square.
  field ; split ; [apply Rlt_not_eq | apply sqrt_no_R0].
   assumption.
   apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rlt_not_eq ; assumption |
    apply sqr_pos].
   fourier.
  b ; (PI / 2) ; rewrite cos_PI2, sin_PI2, a_eq ; CusingR.
 assert (Hrew : (sqrt (1 + (b / a) ^ 2) = sqrt (a × a + b × b) / sqrt (a × a))%R).
  simpl ; repeat rewrite Rmult_1_r ; rewrite <- sqrt_div.
   f_equal ; field ; apply Rgt_not_eq ; assumption.
   left ; apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rgt_not_eq ; assumption |
    apply sqr_pos].
   apply sqr_pos_lt, Rgt_not_eq ; fourier.
  (Cnorm (a +i b))%R ; (Ratan.atan (Cim (a +i b) / Cre (a +i b))) ;
 CusingR_simpl.
 rewrite cos_atan ; unfold Cnorm, Cnorm_sqr ;
  rewrite Hrew ; simpl ; rewrite sqrt_square.
  field ; split ; [apply Rgt_not_eq | apply sqrt_no_R0].
   assumption.
   apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rgt_not_eq ; assumption |
    apply sqr_pos].
   fourier.
 rewrite sin_atan ; unfold Cnorm, Cnorm_sqr ;
  rewrite Hrew ; simpl ; rewrite sqrt_square.
  field ; split ; [apply Rgt_not_eq | apply sqrt_no_R0].
   assumption.
   apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rgt_not_eq ; assumption |
    apply sqr_pos].
   fourier.
Qed.

SearchAbout ["modulu"].

Lemma x_modulo_2PI : x, { k | 0 < IZR (k) × (2 × PI) + x 2 × PI }.
Proof.
intros x ; pose (k := - x / (2 × PI)) ; (up k) ;
 destruct (archimed k) as [k_lb k_ub].
 split.
  rewrite Rplus_comm ; apply Rminus_lt_compat_l_rev, Rmult_Rinv_lt_compat_l_rev.
   apply Rmult_lt_0_compat ; [fourier | apply PI_RGT_0].
   rewrite Rminus_0_l ; apply k_lb.
  transitivity ((IZR (up k) - k) × (2 × PI)).
   right ; unfold k ; field ; apply Rgt_not_eq, PI_RGT_0.
   transitivity (1 × (2 × PI)) ; [| right ; ring] ; apply Rmult_le_compat_r.
    left ; apply Rmult_lt_0_compat ; [fourier | apply PI_RGT_0].
    assumption.
Qed.

Lemma exists_principal_polar_form : z : C, { r : R & { theta : R |
  0 r 0 < theta 2 × PI r × cos (theta) +i r × sin (theta) = z } }%R.
Proof.
intro z ; destruct (exists_polar_form z) as [r [theta Hr]] ;
 destruct (Rlt_le_dec r 0) as [r_neg | r_pos].
  (- r) ; destruct (x_modulo_2PI (theta + PI)) as [k Hk] ;
   (theta + PI + 2 × IZR k × PI) ; split ; [| split].
   fourier.
   replace (theta + PI + 2 × IZR k × PI) with (IZR k × (2 × PI) + (theta + PI))
    by ring ; assumption.
   subst ; CusingR.
   rewrite <- cos2PI_period, neg_cos ; ring.
   rewrite <- sin2PI_period, neg_sin ; ring.
  r ; destruct (x_modulo_2PI theta) as [k Hk] ;
   (theta + 2 × IZR k × PI) ; split ; [| split].
   assumption.
   replace (theta + 2 × IZR k × PI) with (IZR k × (2 × PI) + theta)
    by ring ; assumption.
   subst ; CusingR ; [rewrite <- cos2PI_period | rewrite <- sin2PI_period] ; ring.
Qed.