Library Coqtail.Complex.Cexp
Require Import Rsequence_def.
Require Import Rsequence_facts.
Require Import Rsequence_cv_facts.
Require Import Rsequence_usual_facts.
Require Import Rtactic.
Require Import MyRIneq.
Require Import Cprop_base.
Require Import Csequence.
Require Import Csequence_facts.
Require Import Cpser_def Cpser_base_facts Cpser_facts.
Require Import Canalysis_def.
Require Import Cseries.
Require Import Cseries_facts.
Open Scope C_scope.
Definition exp_seq (n : nat) := / INC (fact n).
Lemma exp_seq_neq : ∀ n : nat, exp_seq n ≠ 0.
Proof.
intro n ; unfold exp_seq ; apply Cinv_neq_0_compat ;
apply not_0_INC ; apply fact_neq_0.
Qed.
Lemma Cdiv_exp_seq_simpl : ∀ n, (exp_seq (S n)) / (exp_seq n) = / INC (S n).
Proof.
intros n ; unfold exp_seq.
replace (fact (S n))%nat with ((S n) × fact n)%nat by reflexivity ;
unfold Cdiv ; rewrite mult_INC, Cinv_involutive ;
[rewrite Cinv_mult_distr ;
[rewrite Cmult_assoc, Cinv_l, Cmult_1_r ;
[reflexivity |] | |] |] ;
apply not_0_INC ; auto ; apply fact_neq_0.
Qed.
Lemma Deriv_exp_seq_simpl : ∀ n, An_deriv exp_seq n = exp_seq n.
Proof.
intro n ; unfold exp_seq, An_deriv, Cseq_shift, Cseq_mult.
replace (fact (S n))%nat with ((S n) × fact n)%nat by reflexivity.
rewrite mult_INC, Cinv_mult_distr, <- Cmult_assoc, Cinv_r, Cmult_1_l ;
[reflexivity | | |] ; replace C0 with (INC O) by reflexivity ; apply not_INC ;
try apply fact_neq_0 ; intuition.
Qed.
Lemma exp_infinite_cv_radius : infinite_cv_radius exp_seq.
Proof.
intros r.
pose (M := (/ (Rabs r + 1))%R) ; assert (M_pos : 0 < M).
unfold M ; apply Rinv_0_lt_compat ;
apply Rplus_le_lt_0_compat ; [apply Rabs_pos | apply Rlt_0_1].
apply (Cpser_alembert_prelim2 exp_seq M M_pos exp_seq_neq).
assert (t : (1 > 0)%nat) by constructor ;
assert (H := Rseq_poly_cv 1 t) ;
assert (H2 := Rseq_cv_pos_infty_shift_compat_reciprocal _ H) ;
assert (H3 := Rseq_cv_pos_infty_inv_compat _ H2) ;
clear t H H2 ; destruct (H3 _ M_pos) as [N HN] ; ∃ N ;
intros n.
rewrite Cdiv_exp_seq_simpl, <- IRC_INR_INC, <- Cinv_IRC_Rinv.
rewrite Cnorm_IRC_Rabs.
apply Rle_trans with (R_dist ((/ Rseq_shift (Rseq_poly 1))%Rseq (N + n)%nat) 0).
right ; unfold R_dist, Rseq_shift, Rseq_poly, pow ; apply Rabs_eq_compat ;
rewrite Rminus_0_r, <- (Rmult_1_r (INR (S (N + n)))) ; reflexivity.
left ; apply HN ; intuition.
apply not_0_INR ; intuition.
unfold M ; rewrite Rinv_involutive ; [| apply Rgt_not_eq ; apply Rplus_le_lt_0_compat ;
[apply Rabs_pos | apply Rlt_0_1]] ; intuition.
Qed.
Definition Cexp (z : C) := sum _ exp_infinite_cv_radius z.
Definition Deriv_Cexp (z : C) := sum_derive _ exp_infinite_cv_radius z.
Lemma Cexp_eq_Deriv_Cexp : ∀ z, Cexp z = Deriv_Cexp z.
Proof.
intro z.
assert (T1 := sum_sums _ exp_infinite_cv_radius z) ;
assert (T2 := sum_derive_sums _ exp_infinite_cv_radius z).
symmetry ; eapply Cpser_unique_extentionality.
apply Deriv_exp_seq_simpl.
apply T2.
apply T1.
Qed.
Lemma derivable_pt_lim_Cexp : ∀ z, derivable_pt_lim Cexp z (Cexp z).
Proof.
intro z ; rewrite Cexp_eq_Deriv_Cexp ;
apply derivable_pt_lim_sum.
Qed.
Lemma Cexp_exp_compat : ∀ a : R, Cexp a = exp a.
Proof.
intros a ; unfold exp, Cexp ; destruct (exist_exp a) as (l, H).
pose (l1 := sum exp_seq exp_infinite_cv_radius (a +i 0)) ;
assert (H1 := sum_sums _ exp_infinite_cv_radius (a +i 0)) ;
replace (sum exp_seq exp_infinite_cv_radius (a +i 0)) with l1 in × by reflexivity.
rewrite <- Ceq ; simpl.
split.
apply (Rseq_cv_unique (sum_f_R0 (fun j : nat ⇒ (/ INR (fact j) × a ^ j)%R))).
apply Rseq_cv_eq_compat with (fun n ⇒ Cre (sum_f_C0 (fun j : nat ⇒ / INC (fact j) × (a +i 0) ^ j) n)).
intro n ; induction n.
simpl ; field.
rewrite sum_f_C0_simpl, tech5, <- Cre_add_compat, IHn ;
apply Rplus_eq_compat_l.
rewrite Cre_mul, Cpow_Cim_0, Cpow_Cre_0, Rmult_0_r, Rminus_0_r.
rewrite INC_inv_Cre_INR ; [reflexivity | apply fact_neq_0].
apply (Cseq_Rseq_Rseq_equiv _ _) ; apply Pser_Cseqcv_link ; unfold exp_seq in H1 ; apply H1.
apply H.
apply (Rseq_cv_unique (fun n ⇒ Cim (sum_f_C0 (fun j : nat ⇒ / INC (fact j) × (a +i 0) ^ j) n))).
apply (Cseq_Rseq_Rseq_equiv _ _) ; apply Pser_Cseqcv_link ; unfold exp_seq in H1 ; apply H1.
apply (Rseq_cv_eq_compat R0) ; [| apply Rseq_constant_cv].
intro n ; induction n ; unfold Rseq_constant in ×.
simpl ; field.
rewrite sum_f_C0_simpl, <- Cim_add_compat, <- IHn, Cim_mul, Cpow_Cim_0,
Cpow_Cre_0, INC_inv_Cim_INR ; [ring | apply fact_neq_0].
Qed.
Lemma Cre_Cpow_2 : ∀ (a : R) (n : nat), Cre ((0 +i a) ^ (2 × n)) = ((-1) ^ n × a ^ (2×n))%R.
Proof.
intros a n ; induction n.
simpl ; ring.
replace (2 × S n)%nat with (S (S (2 × n))) by intuition.
do 2 rewrite Cpow_S, Cre_mul ; rewrite IHn.
rewrite Cim_mul.
replace (Cre (0 +i a)) with R0 by reflexivity.
repeat rewrite IHn ; simpl ; ring.
Qed.
Lemma Cim_Cpow_2 : ∀ (a : R) (n : nat), Cim ((0 +i a) ^ (2 × n)) = R0.
Proof.
intros a n ; induction n.
simpl ; ring.
replace (2 × S n)%nat with (S (S (2 × n))) by intuition.
do 2 rewrite Cpow_S, Cim_mul ; rewrite IHn.
rewrite Cre_mul.
replace (Cre (0 +i a)) with R0 by reflexivity.
repeat rewrite IHn ; ring.
Qed.
Lemma Cre_Cpow_S2 : ∀ (a : R) (p : nat), Cre ((0 +i a) ^ S (2 × p)) = R0.
Proof.
intros a n ; induction n.
simpl ; ring.
replace (2 × S n)%nat with (S (S (2 × n))) by intuition.
do 2 rewrite Cpow_S, Cre_mul ; rewrite IHn.
rewrite Cim_mul.
replace (Cre (0 +i a)) with R0 by reflexivity.
repeat rewrite IHn ; ring.
Qed.
Lemma Cim_Cpow_S2 : ∀ (a : R) (n : nat), Cim ((0 +i a) ^ (S (2 × n))) = ((-1) ^ n × a ^ S (2×n))%R.
Proof.
intros a n ; induction n.
simpl ; ring.
replace (2 × S n)%nat with (S (S (2 × n))) by intuition.
do 2 rewrite Cpow_S, Cim_mul ; rewrite IHn.
rewrite Cre_mul.
replace (Cre (0 +i a)) with R0 by reflexivity.
repeat rewrite IHn ; simpl ; ring.
Qed.
Lemma Cexp_trigo_compat : ∀ a, Cexp (0 +i a) = cos a +i sin a.
Proof.
intros a ; rewrite <- Ceq ; split ; simpl ;
pose (l := sum _ exp_infinite_cv_radius (0 +i a)) ;
replace (Cexp (0 +i a)) with l by reflexivity.
unfold cos ; destruct (exist_cos (Rsqr a)) as (l', Hl') ; unfold cos_in, cos_n in Hl'.
apply Rseq_cv_unique with (fun N ⇒ Cre (sum_f_C0 (gt_pser exp_seq (0 +i a)) N)).
apply (Cseq_Rseq_Rseq_equiv _ _) ; apply Pser_Cseqcv_link ; apply sum_sums.
intros eps eps_pos ; destruct (Hl' _ eps_pos) as [N HN] ; ∃ (2 × N)%nat ;
intros n n_lb ; unfold R_dist.
destruct (n_modulo_2 n) as [H|H] ; destruct H as [p Hp] ; rewrite Hp.
replace (Cre (sum_f_C0 (gt_pser exp_seq (0 +i a)) (2 × p))) with
(sum_f_R0 (fun i : nat ⇒ ((-1) ^ i / INR (fact (2 × i)) × a² ^ i)%R) p).
apply HN ; omega.
clear ; induction p.
simpl ; field.
replace (2 × S p)%nat with (S (S (2 × p)))%nat by intuition.
do 2 rewrite sum_f_C0_simpl ; rewrite tech5 ; do 2 rewrite<- Cre_add_compat ;
rewrite <- IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
replace ((-1) ^ S p / INR (fact (2 × S p)) × a² ^ S p)%R
with (Cre (gt_pser exp_seq (0 +i a) (S (S (2 × p))))).
replace (Cre (gt_pser exp_seq (0 +i a) (S (2 × p))))%R with R0.
symmetry ; apply Rplus_0_l.
unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
replace (S (S (2 × p))) with (2 × S p)%nat by intuition.
rewrite Cim_inv_INC, Rmult_0_l, Cre_Cpow_S2 ; ring.
unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
replace (S (S (2 × p))) with (2 × S p)%nat by intuition.
rewrite Cre_Cpow_2, Cim_Cpow_2, INC_inv_Cre_INR.
unfold Rsqr ; rewrite pow_mult, Rmult_0_r, Rminus_0_r.
rewrite Rmult_comm ; unfold Rdiv ; do 2 rewrite Rmult_assoc ;
apply Rmult_eq_compat_l.
rewrite Rmult_comm ; simpl (pow a (S (S O))) ;
rewrite Rmult_1_r ; reflexivity.
apply fact_neq_0.
replace (Cre (sum_f_C0 (gt_pser exp_seq (0 +i a)) (S (2 × p)))) with
(sum_f_R0 (fun i : nat ⇒ ((-1) ^ i / INR (fact (2 × i)) × a² ^ i)%R) p).
apply HN ; omega.
clear ; induction p.
simpl ; field.
replace (2 × S p)%nat with (S (S (2 × p)))%nat by intuition.
do 2 rewrite sum_f_C0_simpl ; rewrite tech5 ; do 2 rewrite<- Cre_add_compat ;
rewrite <- IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
replace ((-1) ^ S p / INR (fact (2 × S p)) × a² ^ S p)%R
with (Cre (gt_pser exp_seq (0 +i a) (S (S (2 × p))))).
replace (Cre (gt_pser exp_seq (0 +i a) (S (S (S (2 × p))))))%R with R0.
symmetry ; apply Rplus_0_r.
unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
replace (S (S (2 × p))) with (2 × S p)%nat by intuition.
rewrite Cim_inv_INC, Rmult_0_l, Cre_Cpow_S2 ; ring.
unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
replace (S (S (2 × p))) with (2 × S p)%nat by intuition.
rewrite Cre_Cpow_2, Cim_Cpow_2, INC_inv_Cre_INR.
unfold Rsqr ; rewrite pow_mult, Rmult_0_r, Rminus_0_r.
rewrite Rmult_comm ; unfold Rdiv ; do 2 rewrite Rmult_assoc ;
apply Rmult_eq_compat_l.
rewrite Rmult_comm ; simpl (pow a (S (S O))) ;
rewrite Rmult_1_r ; reflexivity.
apply fact_neq_0.
unfold sin ; destruct (exist_sin (Rsqr a)) as (l', Hl') ; unfold sin_in, sin_n in Hl'.
apply Rseq_cv_unique with (fun N ⇒ Cim (sum_f_C0 (gt_pser exp_seq (0 +i a)) N)).
apply (Cseq_Rseq_Rseq_equiv _ _) ; apply Pser_Cseqcv_link ; apply sum_sums.
intros eps eps_pos ; destruct (Req_dec a 0) as [a_eq | a_neq].
∃ O ; intros n n_lb ; unfold R_dist, gt_pser ; rewrite a_eq, Rmult_0_l.
apply Rle_lt_trans with (Rabs (0 - 0)) ;
[| rewrite Rminus_0_r, Rabs_R0 ; assumption].
right ; apply Rabs_eq_compat ; apply Rminus_eq_compat ; [| reflexivity].
induction n.
simpl ; field.
rewrite sum_f_C0_simpl, <- Cim_add_compat, IHn, Rplus_0_l ;
unfold gt_pser ; replace (0 +i 0) with C0 by reflexivity.
unfold Cseq_mult ; rewrite C0_pow, Cmult_0_r ; simpl ; intuition.
intuition.
pose (eps' := (eps / Rabs a)%R) ; assert (eps'_pos : 0 < eps').
unfold eps', Rdiv ; apply Rlt_mult_inv_pos ; [| apply Rabs_pos_lt] ; assumption.
destruct (Hl' _ eps'_pos) as [N HN] ; ∃ (S (2 × N))%nat ;
intros n n_lb ; unfold R_dist.
destruct (n_modulo_2 n) as [H|H] ; destruct H as [p Hp] ; rewrite Hp.
destruct p.
apply False_ind ; clear -n_lb Hp ; omega.
replace (Cim (sum_f_C0 (gt_pser exp_seq (0 +i a)) (2 × S p))) with
(a × sum_f_R0 (fun i : nat ⇒ ((-1) ^ i / INR (fact (2 × i + 1)) × a² ^ i)%R) p)%R.
rewrite <- Rmult_minus_distr_l, Rabs_mult ; apply Rlt_le_trans with (Rabs a × eps')%R.
apply Rmult_lt_compat_l ; [apply Rabs_pos_lt ; assumption|] ; apply HN ; omega.
unfold eps' ; right ; field ; apply Rabs_no_R0 ; assumption.
rewrite scal_sum.
clear ; induction p.
simpl ; field.
replace (2 × S (S p))%nat with (S (S (2 × S p))) by intuition.
rewrite tech5 ; do 2 rewrite sum_f_C0_simpl, <- Cim_add_compat.
rewrite IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
replace (Cim (gt_pser exp_seq (0 +i a) (S (S (2 × S p)))))%R with R0.
unfold_gt ; unfold exp_seq.
rewrite Cim_mul, Cre_Cpow_S2, Cim_Cpow_S2, Rmult_0_l, Rplus_0_r,
Rplus_0_r.
unfold Rsqr.
rewrite INC_inv_Cre_INR.
replace (a ^ S (2 × S p))%R with (a × (a ^ 2) ^ (S p))%R.
replace (2 × S p + 1)%nat with (S (2 × S p)) by intuition.
rewrite (Rmult_comm (/ INR (fact (S (2 × S p)))) _) ; unfold Rdiv ;
repeat rewrite Rmult_assoc ; apply Rmult_eq_compat_l.
rewrite Rmult_comm, <- Rmult_assoc ; apply Rmult_eq_compat_r.
rewrite Rmult_comm ; apply Rmult_eq_compat_l.
simpl ; repeat rewrite Rmult_1_r ; reflexivity.
rewrite <- pow_mult ; simpl ; reflexivity.
apply fact_neq_0.
unfold_gt ; unfold exp_seq ; rewrite Cim_mul ;
replace ( S (S (2 × S p))) with (2 × (S (S p)))%nat by intuition ;
rewrite Cim_Cpow_2, INC_inv_Cim_INR.
do 2 rewrite Rmult_0_r ; ring.
apply fact_neq_0.
replace (Cim (sum_f_C0 (gt_pser exp_seq (0 +i a)) (S (2 × p)))) with
(a × sum_f_R0 (fun i : nat ⇒ ((-1) ^ i / INR (fact (2 × i + 1)) × a² ^ i)%R) p)%R.
rewrite <- Rmult_minus_distr_l, Rabs_mult ; apply Rlt_le_trans with (Rabs a × eps')%R.
apply Rmult_lt_compat_l ; [apply Rabs_pos_lt ; assumption|] ; apply HN ; omega.
unfold eps' ; right ; field ; apply Rabs_no_R0 ; assumption.
rewrite scal_sum.
clear ; induction p.
simpl ; field.
replace (2 × (S p))%nat with (S (S (2 × p))) by intuition.
rewrite tech5 ; do 2 rewrite sum_f_C0_simpl, <- Cim_add_compat.
rewrite IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
replace (Cim (gt_pser exp_seq (0 +i a) (S (S (2 × p)))))%R with R0.
unfold_gt ; unfold exp_seq.
replace (S (S (S (2 × p)))) with (S (2 × (S p))) by intuition.
rewrite Cim_mul, Cre_Cpow_S2, Cim_Cpow_S2, Rmult_0_l,
Rplus_0_l, Rplus_0_r.
unfold Rsqr.
rewrite INC_inv_Cre_INR.
replace (a ^ S (2 × S p))%R with (a × (a ^ 2) ^ (S p))%R.
replace (2 × S p + 1)%nat with (S (2 × S p)) by intuition.
rewrite (Rmult_comm (/ INR (fact (S (2 × S p)))) _) ; unfold Rdiv ;
repeat rewrite Rmult_assoc ; apply Rmult_eq_compat_l.
rewrite Rmult_comm, <- Rmult_assoc ; apply Rmult_eq_compat_r.
rewrite Rmult_comm ; apply Rmult_eq_compat_l.
simpl ; repeat rewrite Rmult_1_r ; reflexivity.
rewrite <- pow_mult ; simpl ; reflexivity.
apply fact_neq_0.
unfold_gt ; unfold exp_seq ; rewrite Cim_mul ;
replace (S (S (2 × p))) with (2 × (S p))%nat by intuition ;
rewrite Cim_Cpow_2, INC_inv_Cim_INR.
do 2 rewrite Rmult_0_r ; ring.
apply fact_neq_0.
Qed.
Lemma Cexp_abs_cv : ∀ z, {l | Cser_abs_cv (gt_pser exp_seq z) l}.
Proof.
intro z ; assert (z_bd : Cnorm z < Cnorm z + 1) by intuition ;
destruct (Cpser_abel2_prelim _ _ (exp_infinite_cv_radius (Cnorm z + 1)%R) _ z_bd) as [l Hl].
unfold Cpser_norm in Hl.
∃ (Cnorm l) ; unfold Cser_abs_cv.
apply Rseq_cv_eq_compat with
(fun n ⇒ Cre (sum_f_C0 (fun n : nat ⇒ Cnorm (gt_pser exp_seq z n)) n)).
intro n ; rewrite <- sum_f_C0_Cre_compat ; simpl ; reflexivity.
replace (Cnorm l) with (Cre (Cnorm l)) by auto ; apply Cseq_cv_re_compat.
Admitted.
Lemma binomial_diag : ∀ n, Binomial.C n n = 1.
Proof.
intros n.
unfold Binomial.C.
rewrite minus_diag.
simpl.
field.
INR_solve; apply fact_neq_0.
Qed.
Lemma binomial_zero : ∀ n, Binomial.C n 0 = 1.
Proof.
intros n.
unfold Binomial.C.
simpl.
rewrite <- minus_n_O.
field.
INR_solve; apply fact_neq_0.
Qed.
Open Scope C_scope.
Lemma binomial_sum : ∀ (x y:C) n,
(x + y) ^ n = sum_f_C0 (fun p ⇒ IRC (Binomial.C n p) × x ^ p × y ^ (n - p)) n.
Proof.
intros x y n.
induction n.
unfold Binomial.C; simpl.
rewrite <- Ceq; simpl; split; field.
destruct n.
unfold Binomial.C; simpl.
rewrite <- Ceq; simpl; split; field.
rewrite sum_f_C0_simpl.
rewrite <- sum_f_C0_reindex.
rewrite Csum_eq_compat with _ (fun k ⇒
Binomial.C (S n) k × x ^ S k × y ^ (S (S n) - S k) +
Binomial.C (S n) (S k) × x ^ S k × y ^ (S (S n) - S k)) _.
rewrite sum_f_C0_add_compat.
rewrite Cpow_S.
rewrite IHn.
rewrite Cmult_add_distr_l.
do 2 (rewrite Cmult_comm; rewrite sum_f_C0_mult).
assert (AP:∀ a b c d e f, a = d + f → b = c + e → a + b = c + (d + e) + f)
by (intros; subst; ring); apply AP; clear AP.
rewrite sum_f_C0_simpl.
repeat rewrite binomial_diag.
repeat rewrite minus_diag.
apply Cadd_eq_compat.
apply Csum_eq_compat_weak; intro; simpl; ring.
simpl; ring.
rewrite <- sum_f_C0_reindex.
apply Cadd_eq_compat.
simpl; repeat rewrite binomial_zero; ring.
apply Csum_eq_compat; intros j Hj.
rewrite <- minus_Sn_m with (S n) _; [|omega].
simpl; ring.
intros j Hj.
repeat rewrite <- Cmult_add_distr_r.
rewrite <- Binomial.pascal; [|omega].
rewrite Cadd_IRC_Rplus; trivial.
Qed.
Lemma Cexp_add : ∀ a b, Cexp (a + b) = (Cexp a × Cexp b)%C.
Proof.
intros a b.
unfold Cexp.
pose (gt_pser exp_seq) as tg.
apply Cser_cv_unique with (tg (a + b)).
apply sum_sums.
destruct (Cexp_abs_cv a) as [lna Hlna].
eapply Cser_cv_eq_compat.
2:eapply (Ccauchy_product (tg a) (tg b)) ; try apply sum_sums.
intro n; simpl.
unfold tg, exp_seq ; unfold_gt.
rewrite binomial_sum.
rewrite sum_f_C0_mult.
apply Csum_eq_compat_weak; intros p.
unfold Binomial.C.
rewrite Cdiv_IRC_Rdiv.
repeat rewrite Cmult_IRC_Rmult.
repeat rewrite IRC_INR_INC.
field; repeat split; replace C0 with (INC O)%C by trivial;
apply not_INC; apply fact_neq_0.
apply Rmult_integral_contrapositive.
INR_solve; apply fact_neq_0.
apply Hlna.
Qed.
Lemma Cexp_0 : Cexp C0 = C1.
Proof.
replace C0 with (IRC R0) by auto.
rewrite Cexp_exp_compat ; rewrite exp_0 ; auto.
Qed.
Lemma Cexp_mult : ∀ a n, Cexp (INC n × a) = (Cexp a) ^ n.
Proof.
intros a n ; induction n.
simpl ; rewrite Cmult_0_l ; apply Cexp_0.
rewrite S_INC, Cpow_S, Cmult_add_distr_r,
Cmult_1_l, Cexp_add, IHn ; ring.
Qed.