proposition: Lemma Cpser_abel2_prelim : forall (An : nat -> C) (r : R), Cv_radius_weak An r -> forall x, Cnorm x < r -> { l | Cpser_norm An x l}.
proof: Proof. intros An r Rho x x_bd. assert (Rho' : Rpser_def.Cv_radius_weak (fun n => Cnorm (An n)) r). destruct Rho as [B HB] ; exists B ; intros u [n Hn] ; rewrite Hn ; apply HB ; exists n ; unfold_gt ; unfold gt_abs_pser, Rpser_def.gt_pser, Rseq_mult, Rseq_abs. rewrite Rabs_mult, Cnorm_Cmult, Rabs_Cnorm ; apply Rmult_eq_compat_l ; rewrite IRC_pow_compat, Cnorm_IRC_Rabs ; reflexivity. rewrite <- Rabs_Cnorm in x_bd ; pose (l := Rpser_sums.weaksum_r _ _ Rho' (Cnorm x)) ; exists l ; unfold Cpser_norm, Pser, infinite_sum. assert (Hl := Rpser_sums.weaksum_r_sums _ _ Rho' (Cnorm x) x_bd) ; unfold Rseries.Pser, Rfunctions.infinite_sum in Hl. assert (Hrew : forall n, IRC (sum_f_R0 (fun n0 : nat => (Cnorm (An n0) * Cnorm x ^ n0)%R) n) = sum_f_C0 (fun n0 : nat => Cnorm (An n0 * x ^ n0)) n). clear ; intro n ; induction n. simpl ; rewrite Cmult_1_r, Rmult_1_r ; reflexivity. simpl ; rewrite <- IHn. rewrite Cadd_IRC_Rplus ; apply Cadd_eq_compat_l. repeat rewrite Cnorm_Cmult ; repeat rewrite Cmult_IRC_Rmult ; apply Cmult_eq_compat_l ; rewrite Cnorm_pow ; reflexivity. intros eps eps_pos ; destruct (Hl _ eps_pos) as [N HN] ; exists N ; intros n n_lb ; simpl ; unfold C_dist. unfold_gt. rewrite <- Hrew, <- Cminus_IRC_Rminus, Cnorm_IRC_Rabs ; apply HN ; assumption. 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