proposition: Lemma Cpser_bound_criteria : forall (An : nat -> C) (z l : C), Cpser An z l -> Cv_radius_weak An (Cnorm z).
proof: Proof. intros An z l Hzl. destruct Hzl with R1 as (N, HN) ; [lra |]. assert (H1 : forall n : nat, (n >= S N)%nat -> gt_norm_pser An z n <= Rmax 2 (Cnorm (An 0%nat) + 1)). intros n Hn ; case_eq n ; unfold_gt. intro H ; simpl ; rewrite Cmult_1_r ; apply Rle_trans with (Cnorm (An 0%nat) +1)%R ; [intuition | apply RmaxLess2]. intros m Hrew ; replace (Cnorm (An (S m) * z ^ S m)) with (Cnorm ((sum_f_C0 (fun n0 : nat => An n0 * z ^ n0) (S m) - l) + (l - sum_f_C0 (fun n0 : nat => An n0 * z ^ n0) m))). apply Rle_trans with (Rplus (Cnorm (sum_f_C0 (fun n0 : nat => An n0 * z ^ n0)%C (S m) - l)) (Cnorm (l - sum_f_C0 (fun n0 : nat => An n0 * z ^ n0) m))). apply Cnorm_triang. apply Rle_trans with 2 ; [|apply RmaxLess1] ; apply Rlt_le ; apply Rplus_lt_compat ; [| rewrite Cnorm_minus_sym]. apply Rle_lt_trans with (dist C_met (sum_f_C0 (fun n0 : nat => An n0 * z ^ n0) (S m)) l). right ; simpl ; unfold C_dist ; reflexivity. simpl (dist C_met) ;unfold C_dist ; unfold Cseq_sum, gt_pser, Cseq_mult in HN ; apply HN ; intuition. apply Rle_lt_trans with (dist C_met (sum_f_C0 (fun n0 : nat => An n0 * z ^ n0) m) l). right ; simpl ; unfold C_dist ; reflexivity. simpl (dist C_met) ;unfold C_dist ; unfold Cseq_sum, gt_pser, Cseq_mult in HN ; apply HN ; intuition. simpl sum_f_C0 ; apply Cnorm_eq_compat. simpl ; ring. destruct (Cseq_partial_bound (gt_pser An z) (S N)) as (B,HB). exists (Rmax B (Rmax 2 (Cnorm (An 0%nat) + 1))). intros y Hy ; destruct Hy as [u Hu] ; rewrite Hu. case (le_lt_dec u (S N)) ; intro Hu_b. apply Rle_trans with B. unfold_gt ; rewrite Cnorm_Cmult, Cnorm_pow, Cnorm_invol. rewrite <- Cnorm_pow. rewrite <- Cnorm_Cmult. apply HB ; assumption. apply RmaxLess1. unfold_gt ; rewrite Cnorm_Cmult. rewrite Cnorm_pow, Cnorm_invol, <- Cnorm_pow, <- Cnorm_Cmult. apply Rle_trans with (Rmax 2 (Cnorm (An 0%nat) + 1)) ; [apply H1 | apply RmaxLess2] ; intuition. 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