proposition: Lemma Cpser_alembert_prelim : forall (An : nat -> C) (M : R), 0 < M -> (forall n : nat, An n <> C0) -> Cseq_bound (fun n => (An (S n) / An n)) M -> forall r, Rabs r < / M -> Cv_radius_weak An r.
proof: Proof. intros An M M_pos An_neq An_frac_ub r r_bd. assert (r_lb := Rabs_pos r) ; case r_lb ; clear r_lb ; intro rabs_lb. assert (my_lam : 0 < /Rabs r - M). apply Rgt_minus ; rewrite <- Rinv_involutive. apply Rinv_lt_contravar. apply Rmult_lt_0_compat ; [| apply Rlt_trans with (Rabs r)] ; assumption. assumption. apply Rgt_not_eq ; assumption. exists (Cnorm (An 0%nat)) ; intros x Hyp ; elim Hyp ; intros n Hn ; rewrite Hn ; unfold_gt ; rewrite Cnorm_Cmult. clear Hn ; induction n. simpl ; rewrite Cnorm_C1 ; rewrite Rmult_1_r ; right ; reflexivity. apply Rle_trans with (Cnorm (An (S n) / (An n)) * Cnorm (An n) * Cnorm (r ^ S n))%R. right ; repeat rewrite <- Cnorm_Cmult ; apply Cnorm_eq_compat ; field ; apply An_neq. apply Rle_trans with (M * Cnorm (An n) * Cnorm (r ^ S n))%R. repeat apply Rmult_le_compat_r ; [| | apply An_frac_ub] ; apply Cnorm_pos. simpl ; rewrite Cnorm_Cmult. apply Rle_trans with (M * Cnorm (An n) * (/M * Cnorm (r ^ n)))%R. repeat rewrite <- Rmult_assoc ; apply Rmult_le_compat_r ; [apply Cnorm_pos | repeat rewrite Rmult_assoc ; repeat apply Rmult_le_compat_l]. left ; assumption. apply Cnorm_pos. rewrite Cnorm_IRC_Rabs ; left ; assumption. apply Rle_trans with (Cnorm (An n) * Cnorm (r ^ n))%R ; [right ; field ; apply Rgt_not_eq |] ; assumption. exists (Cnorm (An 0%nat)). intros x Hx ; destruct Hx as (n,Hn) ; rewrite Hn ; unfold_gt ; destruct n. right ; apply Cnorm_eq_compat ; ring. destruct (Req_dec r 0) as [Hr | Hf]. rewrite Hr ; unfold gt_norm_pser ; rewrite Cnorm_Cmult, Cnorm_pow, Cnorm_IRC_Rabs, RPow_abs, pow_i, Rabs_R0, Rmult_0_r ; [apply Cnorm_pos | intuition]. apply False_ind ; assert (T := Rabs_no_R0 _ Hf) ; apply T ; symmetry ; 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