Require Export CComplex.

Section AbsCC_properties.

Lemma AbsCC_nonneg : ∀ x : CC, [0] [<=] AbsCC x.
Proof.
 unfold AbsCC in |- ×. intros.
 apply sqrt_nonneg.
Qed.

Lemma AbsCC_ap_zero_imp_pos : ∀ z : CC, AbsCC z [#] [0] → [0] [<] AbsCC z.
Proof.
 intros z H.
 apply leEq_not_eq.
  apply AbsCC_nonneg.
 apply ap_symmetric_unfolded. assumption.
Qed.

Lemma AbsCC_wd : ∀ x y : CC, x [=] y → AbsCC x [=] AbsCC y.
Proof.
 intros x y. elim x. intros x1 x2. elim y. intros y1 y2.
 simpl in |- ×. unfold cc_eq in |- ×. unfold AbsCC in |- ×. simpl in |- ×. intros.
 change (sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2) [=]
   sqrt (y1[^]2[+]y2[^]2) (cc_abs_aid _ y1 y2)) in |- ×.
 elim H. clear H. intros.
 apply sqrt_wd. algebra.
Qed.

Hint Resolve AbsCC_wd: algebra_c.

Lemma cc_inv_abs : ∀ x : CC, AbsCC [--]x [=] AbsCC x.
Proof.
 intros.
 unfold AbsCC in |- ×.
 apply sqrt_wd.
 apply bin_op_wd_unfolded.
  Step_final ( [--] (Re x) [^]2).
 Step_final ( [--] (Im x) [^]2).
Qed.

Hint Resolve cc_inv_abs: algebra.

Lemma cc_minus_abs : ∀ x y : CC, AbsCC (x[-]y) [=] AbsCC (y[-]x).
Proof.
 intros.
 apply eq_transitive_unfolded with (AbsCC [--] (y[-]x)).
  apply AbsCC_wd. rational.
  apply cc_inv_abs.
Qed.

Lemma cc_mult_abs : ∀ x y : CC, AbsCC (x[*]y) [=] AbsCC x[*]AbsCC y.
Proof.
 intros x y. elim x. intros x1 x2. elim y. intros y1 y2. intros.
 unfold AbsCC in |- ×.
 apply sqrt_mult_wd.
 simpl in |- ×.
 rational.
Qed.

Hint Resolve cc_mult_abs: algebra.

Lemma AbsCC_minzero : ∀ x : CC, AbsCC (x[-][0]) [=] AbsCC x.
Proof.
 intros.
 apply AbsCC_wd.
 algebra.
Qed.

Lemma AbsCC_IR : ∀ x : IR, [0] [<=] x → AbsCC (cc_IR x) [=] x.
Proof.
 intros. unfold AbsCC in |- ×.
 change (sqrt (x[^]2[+][0][^]2) (cc_abs_aid _ x [0]) [=] x) in |- ×.
 apply eq_transitive_unfolded with (sqrt (x[^]2) (sqr_nonneg _ x)).
  apply sqrt_wd. rational.
  apply sqrt_to_nonneg. auto.
Qed.

Hint Resolve AbsCC_IR: algebra.

Lemma cc_div_abs : ∀ (x y : CC) y_ y__, AbsCC (x[/] y[//]y_) [=] (AbsCC x[/] AbsCC y[//]y__).
Proof.
 intros x y nz anz.
 rstepl (AbsCC y[*]AbsCC (x[/] y[//]nz) [/] AbsCC y[//]anz).
 apply div_wd. 2: algebra.
  astepl (AbsCC (y[*] (x[/] y[//]nz))).
 apply AbsCC_wd. rational.
Qed.

Lemma cc_div_abs' : ∀ (x : CC) (y : IR) y_ y__,
 [0] [<=] y → AbsCC (x[/] cc_IR y[//]y__) [=] (AbsCC x[/] y[//]y_).
Proof.
 intros x y nz cnz H.
 rstepl (y[*]AbsCC (x[/] cc_IR y[//]cnz) [/] y[//]nz).
 apply div_wd. 2: algebra.
  astepl (AbsCC (cc_IR y) [*]AbsCC (x[/] cc_IR y[//]cnz)).
 astepl (AbsCC (cc_IR y[*] (x[/] cc_IR y[//]cnz))).
 apply AbsCC_wd.
 rational.
Qed.

Lemma AbsCC_zero : AbsCC [0] [=] [0].
Proof.
 astepl (AbsCC (cc_IR [0])).
 apply AbsCC_IR.
 apply leEq_reflexive.
Qed.

Hint Resolve AbsCC_zero: algebra.

Lemma AbsCC_one : AbsCC [1] [=] [1].
Proof.
 astepl (AbsCC (cc_IR [1])).
 apply AbsCC_IR.
 apply less_leEq. apply pos_one.
Qed.

Lemma cc_pow_abs : ∀ (x : CC) (n : nat), AbsCC (x[^]n) [=] AbsCC x[^]n.
Proof.
 intros. induction n as [| n Hrecn]; intros.
 simpl in |- ×. apply AbsCC_one.
  simpl in |- ×. Step_final (AbsCC (x[^]n) [*]AbsCC x).
Qed.

Lemma AbsCC_pos : ∀ x : CC, x [#] [0] → [0] [<] AbsCC x.
Proof.
 intro. elim x. intros x1 x2.
 unfold AbsCC in |- ×. simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. intros H.
 change ([0] [<] sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2)) in |- ×.
 apply power_cancel_less with 2. apply sqrt_nonneg.
  astepl ZeroR.
 astepr (x1[^]2[+]x2[^]2).
 elim H; clear H; intros.
  apply plus_resp_pos_nonneg.
   apply pos_square. auto. apply sqr_nonneg.
   apply plus_resp_nonneg_pos.
  apply sqr_nonneg. apply pos_square. auto.
Qed.

Lemma AbsCC_ap_zero : ∀ x : CC, [0] [#] AbsCC x → x [#] [0].
Proof.
 intro. elim x. intros x1 x2. simpl in |- ×. unfold AbsCC in |- ×. unfold cc_ap in |- ×.
 change ([0] [#] sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2) → x1 [#] [0] or x2 [#] [0]) in |- ×.
 intros H.
 cut (x1[^]2 [#] [0] or x2[^]2 [#] [0]). intro H0.
  elim H0; clear H0; intros.
   left.
   apply cring_mult_ap_zero with x1.
   astepl (x1[^]2). auto.
   right.
  apply cring_mult_ap_zero with x2.
  astepl (x2[^]2). auto.
  apply cg_add_ap_zero.
 astepl (sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2) [^]2).
 apply nexp_resp_ap_zero.
 apply ap_symmetric_unfolded. auto.
Qed.

Lemma AbsCC_small_imp_eq : ∀ x : CC, (∀ e, [0] [<] e → AbsCC x [<] e) → x [=] [0].
Proof.
 intros x H.
 apply not_ap_imp_eq. intro.
 elim (less_irreflexive_unfolded _ (AbsCC x)).
 apply H.
 apply AbsCC_pos. auto.
Qed.


Hint Resolve l_1_1_2: algebra.

Lemma AbsCC_square_Re_Im : ∀ x y : IR, x[^]2[+]y[^]2 [=] AbsCC (x[+I*]y) [^]2.
Proof.
 intros. unfold AbsCC in |- ×.
 Step_final (Re (x[+I*]y) [^]2[+]Im (x[+I*]y) [^]2).
Qed.

Hint Resolve AbsCC_square_Re_Im: algebra.


Hint Resolve l_1_2_3_CC: algebra.

Lemma AbsCC_mult_conj : ∀ z : CC, z[*]CC_conj z [=] cc_IR (AbsCC z[^]2).
Proof.
 intro z. unfold cc_IR in |- ×.
 elim z. intros x y.
 apply eq_transitive_unfolded with (S := cc_csetoid) (y := cc_IR (x[^]2[+]y[^]2)).
  eapply l_1_1_2 with (x := x) (y := y).
 split; simpl in |- ×.
  2: algebra.
 eapply AbsCC_square_Re_Im with (x := x) (y := y).
Qed.

Hint Resolve CC_conj_mult: algebra.


Lemma AbsCC_mult_square : ∀ x y : CC, AbsCC (x[*]y) [^]2 [=] AbsCC x[^]2[*]AbsCC y[^]2.
Proof.
 intros. rstepr ((AbsCC x[*]AbsCC y) [^]2). algebra.
Qed.

Lemma AbsCC_square_ap_zero : ∀ z : CC, z [#] [0] → AbsCC z[^]2 [#] [0].
Proof.
 intros z H.
 astepl (Re z[^]2[+]Im z[^]2).
  apply (cc_inv_aid (Re z) (Im z) H).
 apply AbsCC_square_Re_Im with (x := Re z) (y := Im z).
Qed.

Lemma cc_recip_char : ∀ (z : CC) z_ z__,
 cc_recip z z_ [=] (CC_conj z[/] cc_IR (AbsCC z[^]2) [//]z__).
Proof.
 intros z z_ HAbsCCz.
 unfold cc_recip in |- ×.
 astepl (Re z[+I*][--] (Im z) [/] _[//] cc_IR_resp_ap _ _ (cc_inv_aid _ _ (cc_ap_zero _ z_))).
  2: simpl in |- *; split; simpl in |- *; rational.
 apply div_wd with (F := CC) (x := Re z[+I*][--] (Im z)) (y := cc_IR (Re z[^]2[+]Im z[^]2))
   (x' := CC_conj z) (y' := cc_IR (AbsCC z[^]2)).
  elim z. intros x y. simpl in |- ×. split; simpl in |- *; algebra.
  apply cc_IR_wd.
 apply AbsCC_square_Re_Im with (x := Re z) (y := Im z).
Qed.

Lemma AbsCC_strext : fun_strext AbsCC.
Proof.
 unfold fun_strext in |- ×.
 intros z1 z2 H.
 cut (AbsCC z1[^]2 [#] AbsCC z2[^]2).
  elim z1. intros x1 y1. elim z2. intros x2 y2.
  intro H'.
  assert (H'' : x1[^]2[+]y1[^]2 [#] x2[^]2[+]y2[^]2).
   astepl (AbsCC (x1[+I*]y1) [^]2). astepr (AbsCC (x2[+I*]y2) [^]2). assumption.
   cut (x1[^]2 [#] x2[^]2 or y1[^]2 [#] y2[^]2).
   intros H'''. elim H'''; intro H0.
   cut (x1 [#] x2).
     intro H1.
     simpl in |- ×. unfold cc_ap in |- ×. unfold Re, Im in |- ×.
     left.
     assumption.
    apply (nexp_strong_ext IR 2).
    assumption.
   simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×.
   right.
   apply (nexp_strong_ext IR 2).
   assumption.
  apply (bin_op_strext_unfolded _ _ _ _ _ _ H'').
 assert (H1 : AbsCC z1[-]AbsCC z2 [#] [0]).
  cut (AbsCC z1[-]AbsCC z2 [#] AbsCC z2[-]AbsCC z2).
   intro H0. astepr (AbsCC z2[-]AbsCC z2). assumption.
   apply minus_resp_ap_rht. assumption.
  assert (H2 : AbsCC z1[+]AbsCC z2 [#] [0]).
  apply Greater_imp_ap.
  assert (H0 : AbsCC z1 [#] [0] or [0] [#] AbsCC z2).
   apply ap_cotransitive_unfolded. assumption.
   elim H0.
   intro H'.
   assert (H'' : [0] [<] AbsCC z1).
    apply (AbsCC_ap_zero_imp_pos _ H').
   apply leEq_less_trans with (y := AbsCC z2).
    apply AbsCC_nonneg.
   rstepl (AbsCC z2[+][0]).
   rstepr (AbsCC z2[+]AbsCC z1).
   apply plus_resp_less_lft.
   assumption.
  intro H'.
  assert (H'' : [0] [<] AbsCC z2).
   apply AbsCC_ap_zero_imp_pos.
   apply ap_symmetric_unfolded. assumption.
   apply leEq_less_trans with (y := AbsCC z1).
   apply AbsCC_nonneg.
  rstepl (AbsCC z1[+][0]).
  apply plus_resp_less_lft.
  assumption.
 cut (AbsCC z1[^]2[-]AbsCC z2[^]2 [#] [0]).
  intro H3.
  cut (AbsCC z1[^]2[-]AbsCC z2[^]2 [#] AbsCC z2[^]2[-]AbsCC z2[^]2).
   intro H4.
   rstepl (AbsCC z1[^]2[-]AbsCC z2[^]2[+]AbsCC z2[^]2).
   rstepr ([0][+]AbsCC z2[^]2).
   apply op_rht_resp_ap with (x := AbsCC z1[^]2[-]AbsCC z2[^]2) (y := ZeroR) (z := AbsCC z2[^]2).
   rstepr (AbsCC z2[^]2[-]AbsCC z2[^]2).
   assumption.
  rstepr ZeroR.
  assumption.
 astepl ((AbsCC z1[-]AbsCC z2) [*] (AbsCC z1[+]AbsCC z2)).
 apply mult_resp_ap_zero; assumption.
Qed.

Definition AbsSmallCC (e : IR) (x : CC) := AbsCC x [<=] e.

Lemma Cexis_AFS_CC : ∀ x y eps, [0] [<] eps → {y' : CC | AbsSmallCC eps (y'[-]y) | y' [#] x}.
Proof.
 unfold AbsSmallCC in |- ×. intros.
 set (e := cc_IR eps) in ×.
 elim (ap_cotransitive_unfolded _ (y[-]e) (y[+]e)) with x; try intro H0.
   ∃ (y[-]e).
    apply leEq_wdl with (AbsCC [--]e).
     unfold e in |- ×.
     astepl (AbsCC (cc_IR eps)).
     apply eq_imp_leEq.
     apply AbsCC_IR.
     apply less_leEq; auto.
    apply AbsCC_wd. rational.
    auto.
  ∃ (y[+]e).
   apply leEq_wdl with (AbsCC e).
    apply eq_imp_leEq.
    unfold e in |- *; apply AbsCC_IR.
    apply less_leEq; auto.
   apply AbsCC_wd. rational.
   apply ap_symmetric_unfolded. auto.
  apply zero_minus_apart.
 apply ap_wdl_unfolded with (cc_IR ( [--]Two[*]eps)).
  astepr (cc_IR [0]).
  apply cc_IR_resp_ap. apply mult_resp_ap_zero.
  apply inv_resp_ap_zero. apply two_ap_zero.
   apply pos_ap_zero; auto.
 unfold e in |- ×.
 astepl (cc_IR [--]Two[*]cc_IR eps).
 rstepr ( [--]Two[*]cc_IR eps).
 apply mult_wdl.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×.
 split; [ algebra | rational ].
Qed.



End AbsCC_properties.

Hint Resolve AbsCC_wd: algebra_c.
Hint Resolve cc_inv_abs cc_mult_abs cc_div_abs cc_div_abs' cc_pow_abs
  AbsCC_zero AbsCC_one AbsCC_IR AbsCC_mult_conj AbsCC_mult_square
  cc_recip_char: algebra.

Lemma triangle : ∀ x y : CC, AbsCC (x[+]y) [<=] AbsCC x[+]AbsCC y.
Proof.
 intros.
 elim x. intros x1 x2.
 elim y. intros y1 y2.
 unfold AbsCC in |- ×. simpl in |- ×.
 apply power_cancel_leEq with 2. auto.
   astepl ([0][+]ZeroR).
  apply plus_resp_leEq_both; apply sqrt_nonneg.
 astepl ([1][*](x1[+]y1)[*](x1[+]y1)[+][1][*](x2[+]y2)[*](x2[+]y2)).
 rstepr (sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[^]2[+]
   sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)[^]2[+]
     Two[*]sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[*]
       sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)).
 astepr ([1][*]x1[*]x1[+][1][*]x2[*]x2[+]([1][*]y1[*]y1[+][1][*]y2[*]y2)[+]
   Two[*]sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[*]
     sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)).
 apply shift_leEq_rht.
 rstepr (Two[*] (sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[*]
   sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)[-] (x1[*]y1[+]x2[*]y2))).
 apply mult_resp_nonneg. apply less_leEq. apply pos_two.
  apply shift_leEq_lft.
 apply power_cancel_leEq with 2. auto.
   apply mult_resp_nonneg; apply sqrt_nonneg.
 astepr (sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[^]2[*]
   sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)[^]2).
 astepr (([1][*]x1[*]x1[+][1][*]x2[*]x2)[*]([1][*]y1[*]y1[+][1][*]y2[*]y2)).
 apply shift_leEq_rht.
 rstepr ((x1[*]y2[-]x2[*]y1)[^]2).
 apply sqr_nonneg.
Qed.

Lemma triangle_Sum : ∀ m n (z : nat → CC),
 m ≤ S n → AbsCC (Sum m n z) [<=] Sum m n (fun i ⇒ AbsCC (z i)).
Proof.
 intros. induction n as [| n Hrecn]; intros.
 generalize (toCle _ _ H); clear H; intro H.
  inversion H as [|m0 H1 H2].
   unfold Sum in |- ×. unfold Sum1 in |- ×.
   astepl (AbsCC [0]).
   astepr ZeroR.
   astepr (AbsCC [0]).
   apply leEq_reflexive.
  inversion H1.
  unfold Sum in |- ×. unfold Sum1 in |- ×. simpl in |- ×.
  cut (AbsCC ([0][+]z 0[-][0])[<=][0][+]AbsCC (z 0)[-][0]).
   auto.
  apply eq_imp_leEq.
  rstepr (AbsCC (z 0)).
  apply AbsCC_wd.
  rational.
 elim (le_lt_eq_dec _ _ H); intro y.
  astepl (AbsCC (Sum m n z[+]z (S n))).
  apply leEq_wdr with (Sum m n (fun i : nat ⇒ AbsCC (z i))[+]AbsCC (z (S n))).
   apply leEq_transitive with (AbsCC (Sum m n z)[+]AbsCC (z (S n))).
    apply triangle.
   apply plus_resp_leEq.
   apply Hrecn. auto with arith.
   apply eq_symmetric_unfolded. apply Sum_last with (f := fun i : nat ⇒ AbsCC (z i)).
  rewrite y. unfold Sum in |- ×. unfold Sum1 in |- ×.
 astepl (AbsCC [0]).
 astepr ZeroR.
 astepr (AbsCC [0]).
 apply leEq_reflexive.
Qed.