proposition: Lemma Cpser_abel : forall (An : nat -> C) (r : R), Cv_radius_weak An r -> forall x, Cnorm x < r -> {l | Cpser An x l}.
proof: Proof. intros An r Rho x x_ub. case (Req_or_neq r) ; intro r_0. exists 0 ; apply False_ind ; rewrite r_0 in x_ub ; assert (0 <= Cnorm x). apply Cnorm_pos. lra. assert (Hrew_abs : (Cnorm (x / r) = Cnorm x / r)%R). unfold Cdiv, Rdiv ; rewrite Cnorm_Cmult ; apply Rmult_eq_compat_l ; replace (/r) with (IRC (/r)). rewrite Cnorm_IRC_Rabs. apply Rabs_right. left ; apply Rinv_0_lt_compat ; apply Rle_lt_trans with (Cnorm x) ; [apply Cnorm_pos | assumption]. CusingR_f ; assumption. assert (Rabsx_r_lt_1 : Cnorm x / r < 1). apply Rle_lt_trans with (Cnorm x / r * (r / r))%R. right ; field ; assumption. replace 1%R with (r / r)%R by (field ; assumption). unfold Rdiv ; rewrite <- Rmult_assoc. apply Rmult_lt_compat_r. apply Rinv_0_lt_compat ; apply Rle_lt_trans with (Cnorm x) ; [apply Cnorm_pos | assumption]. rewrite Rmult_assoc ; rewrite Rinv_l ; [| assumption] ; rewrite Rmult_1_r ; assumption. assert (Rho' : Rpser_def.Cv_radius_weak (fun n : nat => Cnorm (An n)) r). destruct Rho as [M HM] ; exists M. intros u [n Hn] ; rewrite Hn ; unfold gt_abs_pser, Rpser_def.gt_pser, Rseq_abs, Rseq_mult. unfold gt_norm_pser, gt_pser, Cseq_norm, Cseq_mult in HM. replace (Rabs (Cnorm (An n) * r ^ n))%R with (Cnorm (An n * r ^ n))%R. apply HM ; exists n ; reflexivity. rewrite Rabs_mult ; replace (Rabs (r ^ n))%R with (Rabs (Cnorm r ^ n))%R. rewrite <- Rabs_mult, <- Cnorm_pow, <- Cnorm_Cmult, Rabs_Cnorm ; reflexivity. rewrite <- Cnorm_pow, IRC_pow_compat, Cnorm_IRC_Rabs, Rabs_Rabsolu ; reflexivity. rewrite <- Rabs_Cnorm in x_ub. assert (Cnorm_cauchy := Cauchy_crit_Rseq_pps (fun n => Cnorm (An n)) r Rho' (Cnorm x) x_ub). assert (T : Rseries.Cauchy_crit (sum_f_R0 (fun n : nat => Cnorm (An n * x ^ n)))). intros eps eps_pos ; destruct (Cnorm_cauchy eps eps_pos) as [N HN] ; exists N ; intros m n m_lb n_lb. assert (Hrew : forall An x n, sum_f_R0 (fun n0 : nat => Cnorm (An n0 * x ^ n0)) n = sum_f_R0 (Rpser_def.gt_pser (fun n0 : nat => Cnorm (An n0)) (Cnorm x)) n). clear ; intros An x n ; induction n. unfold Rpser_def.gt_pser ; simpl ; rewrite Cnorm_Cmult, Cnorm_C1 ; reflexivity. simpl sum_f_R0 ; rewrite IHn ; apply Rplus_eq_compat_l ; unfold Rpser_def.gt_pser ; simpl ; repeat rewrite Cnorm_Cmult ; rewrite Cnorm_pow ; reflexivity. repeat rewrite Hrew ; rewrite R_dist_sym ; apply HN ; assumption. destruct (Cseq_norm_Rseq (fun n => An n * x ^ n) (R_complete _ T)) as [l Hl] ; exists l ; apply Hl. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts