Library Coqtail.Complex.Cpow_plus

Require Import Ctacfield.
Require Import Cbase.
Require Import Cprop_base.
Require Import Cfunctions.
Require Import Cpow.

Open Scope C_scope.

Lemma binom_add_INC : ∀ n k : nat, (n≥ k)%nat → - INC (fact n) / INC (fact (n-k) × fact k)
 + INC (fact (S n)) / INC (fact k × fact (S (n - k)))
= INC (k × fact n) / INC ( fact k × fact (S (n-k))).
Proof.
intros n k H.
do 2 rewrite fact_simpl.
replace (INC (fact k × (S (n - k) × fact (n - k)))) with (INC (S (n-k)) × INC (fact k × fact (n-k))) by
(rewrite mult_comm ; symmetry ; rewrite mult_comm ; rewrite <- mult_INC ;
rewrite mult_assoc ; reflexivity).

replace (INC (S n × fact n)) with (INC (S n) × INC (fact n))
by (rewrite mult_INC ; reflexivity).

unfold Cdiv. rewrite Cinv_mult_distr.
  apply (Cmult_eq_reg_l (INC (S (n - k)))). apply not_0_INC. intuition.
  rewrite Cmult_add_distr_l. repeat rewrite mult_INC.
  field_simplify.
    rewrite Cmult_comm. rewrite <- Cmult_add_distr_l.
    unfold Cdiv. repeat rewrite Cmult_assoc. apply Cmult_eq_compat_l.
    rewrite Cadd_comm.
    replace (INC (S n) + - INC (S (n - k))) with (INC (S n) - INC (S (n - k))) by intuition.
    rewrite <- minus_INC. intuition.
   intuition.
  split. apply not_0_INC. apply fact_neq_0. split. apply not_0_INC. apply fact_neq_0.
   apply not_0_INC. intuition.
   split. apply not_0_INC. apply fact_neq_0. split. apply not_0_INC. apply fact_neq_0.
   apply not_0_INC. intuition.
 apply not_0_INC. intuition.
apply not_0_INC. intro Habs. apply mult_is_O in Habs. elim Habs; apply fact_neq_0.
Qed.


Lemma Cpow_add_dev : ∀ z : C, ∀ n : nat,
((z ^ n)%C = (sum_f_C0 (fun k ⇒ (Cre z +i 0%R)^k × (0%R +i Cim z) ^ (n-k) × INC (fact n)/INC ((fact k) × fact (n-k))) n))%C.
Proof.
intros z.
induction n.
simpl. CusingR_f.
destruct z as (zR, zI).
replace ((zR, zI) ^ S n) with ((zR, zI) × (zR, zI) ^ n) by (simpl; reflexivity).
rewrite IHn.
replace (Cre (zR, zI)) with zR by (simpl; reflexivity).
replace (Cim (zR, zI)) with zI by (simpl; reflexivity).
rewrite sum_f_C0_mult.
rewrite sum_f_C0_simpl.
apply Cminus_diag_uniq.
assert (H4 : ( ∀ a b c : C, a - (b + c) = (a - b) - c)). intros; ring.
rewrite H4.
rewrite <- sum_f_C0_minus_compat.
replace (zR, zI) with (zR +i zI) by reflexivity.
replace (sum_f_C0
  (fun n0 : nat ⇒
   (zR +i zI) × ((zR +i 0%R) ^ n0 × (0%R +i zI) ^ (n - n0) × INC (fact n) /
    INC (fact n0 × fact (n - n0))) -
   (zR +i 0%R) ^ n0 × (0%R +i zI) ^ (S n - n0) × INC (fact (S n)) /
   INC (fact n0 × fact (S n - n0))) n)
with (sum_f_C0
     (fun n0 : nat ⇒ (zR +i0%R)^ S n0 × (0%R +i zI) ^ (n-n0) × INC (fact n)
     /INC (fact n0 × fact (n - n0)) - (zR +i 0%R) ^ n0 × (0%R +i zI)^ (S n-n0) × INC (n0 × fact n) / INC (fact n0 × fact (n-n0 + 1))) n )
by (rewrite fun_prop_bin_add_INC ; reflexivity).
rewrite sum_f_C0_minus_compat.
destruct n. CusingR_f.
rewrite sum_f_C0_simpl. rewrite <- sum_f_C0_reindex.
replace (sum_f_C0
  (fun n0 : nat ⇒
   (zR +i 0%R) ^ S n0 × (0%R +i zI) ^ (S n - n0) × INC (fact (S n)) /
   INC (fact n0 × fact (S n - n0))) n) with
(sum_f_C0
   (fun k : nat ⇒
    (zR +i 0%R) ^ S k × (0%R +i zI) ^ (S (S n) - S k) ×
    INC (S k × fact (S n)) / INC (fact (S k) × fact (S n - S k + 1))) n).
Focus 2. apply sum_f_C0_eq_seq. intros m H.
repeat rewrite fact_simpl. repeat rewrite mult_INC.
replace (S n - S m + 1)%nat with (S n - m)%nat by intuition.
replace (S (S n) - S m)%nat with (S n - m)%nat by intuition.
field.
split ; try split ; apply not_0_INC ; try apply fact_neq_0 ; intuition.
ring_simplify.
replace (S n - S n)%nat with O by intuition.
replace (S (S n) - S (S n))%nat with O by intuition.
repeat rewrite fact_simpl.
repeat rewrite mult_INC. simpl (INC 0).
field_simplify. unfold Cdiv. repeat rewrite Cmult_0_l. reflexivity.
split ; try split ; try split ; try split ; try apply not_0_INC ; try apply fact_neq_0 ; intuition.
Qed.