proposition: Lemma Cexp_trigo_compat : forall a, Cexp (0 +i a) = cos a +i sin a.
proof: 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] ; exists (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 ; lia. 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 ; lia. 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]. exists 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] ; exists (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 ; lia. 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 ; lia. 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 ; lia. 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.
imports: Lia Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_usual_facts Rtactic MyRIneq Cprop_base Csequence Csequence_facts Cpser_def Cpser_base_facts Cpser_facts Cseries Cseries_facts Cdefinitions Canalysis_def