proposition: Lemma Cpser_abel2 : forall (An : nat -> C) (r : R), Cv_radius_weak An r -> forall r0 : posreal, r0 < r -> CVN_r (fun n x => gt_pser An x n) r0.
proof: Proof. intros An r Pr r0 r0_ub. destruct r0 as (a,a_pos). assert (a_bd : Rabs a < r). rewrite Rabs_right ; [| apply Rgt_ge ; apply Rlt_gt] ; assumption. assert (r_pos : 0 < r). apply Rlt_trans with a ; assumption. assert (r'_bd : Rabs ((a + r) / 2) < r). rewrite Rabs_right. assert (Hrew : r = ((r+r)/2)%R) by field ; rewrite Hrew at 2; unfold Rdiv ; apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat ; intuition |] ; apply Rplus_lt_compat_r ; rewrite Rabs_right in a_bd ; intuition. apply Rle_ge ; unfold Rdiv ; replace 0%R with (0 * /2)%R by field ; apply Rmult_le_compat_r ; lra. assert (r'_bd2 : Cnorm (Rabs ((a + r) / 2)) < r). rewrite Cnorm_IRC_Rabs, Rabs_Rabsolu ; assumption. assert (Pr' := Cv_radius_weak_Cnorm_compat2 _ _ Pr). exists (gt_abs_pser (fun n => Cnorm (An n)) ((a+r)/2)). exists (Rpser_sums.weaksum_r (fun n => Cnorm (An n)) r Pr' (Rabs ((a+r)/2))) ; split. rewrite Cnorm_IRC_Rabs in r'_bd2 ; assert (H := Rpser_sums.weaksum_r_sums (fun n => Cnorm (An n)) r Pr' (Rabs ((a + r) / 2)) r'_bd2). unfold Rpser in H. intros eps eps_pos ; destruct (H eps eps_pos) as (N, HN) ; exists N. assert (Hrew : forall k, Cnorm (gt_abs_pser (fun n => Cnorm (An n)) ((a + r) / 2) k) = Rpser_def.gt_pser (fun n0 : nat => Cnorm (An n0)) (Rabs ((a + r) / 2)) k). intro k ; unfold gt_abs_pser, Rpser_def.gt_pser, Rseq_mult, Rseq_abs. rewrite Cnorm_IRC_Rabs, Rabs_Rabsolu, Rabs_mult, <- RPow_abs, Rabs_Cnorm ; reflexivity. assert (Temp : forall n, sum_f_R0 (fun k : nat => Cnorm (gt_abs_pser (fun n0 : nat => Cnorm (An n0)) ((a + r) / 2) k)) n = sum_f_R0 (Rpser_def.gt_pser (fun n0 : nat => Cnorm (An n0)) (Rabs ((a + r) / 2))) n). intros n ; clear -Hrew ; induction n ; simpl ; rewrite Hrew ; [| rewrite IHn] ; reflexivity. intros n n_lb ; rewrite Temp ; apply HN ; assumption. intros n y Hyp ; unfold_gt ; unfold gt_abs_pser, Rpser_def.gt_pser, Rseq_abs, Rseq_mult. rewrite Rabs_mult, Rabs_Cnorm ; repeat rewrite Cnorm_Cmult, Cnorm_IRC_Rabs, Rabs_mult, Rabs_right. apply Rmult_le_compat_l. apply Cnorm_pos. rewrite Rabs_Rabsolu. rewrite <- Cnorm_IRC_Rabs ; rewrite <- IRC_pow_compat ; repeat rewrite Cnorm_pow ; apply pow_incr ; split ; [apply Cnorm_pos |]. unfold Boule in Hyp ; simpl in Hyp ; unfold C_dist in Hyp ; rewrite Cnorm_minus_sym, Cminus_0_r in Hyp. apply Rle_trans with a ; [left ; assumption |]. rewrite Cnorm_IRC_Rabs, Rabs_right. apply Rle_trans with ((a + a) / 2)%R ; [right ; field | unfold Rdiv ; apply Rmult_le_compat_r ; [lra | apply Rplus_le_compat_l ; left ; assumption]]. unfold Rdiv ; apply Rle_ge ; apply Rle_mult_inv_pos ; lra. apply Rle_ge ; apply Cnorm_pos. 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