proposition: Lemma Cpser_alembert_prelim3 : forall (An : nat -> C) (lambda : C), 0 < Cnorm (lambda) -> (forall n : nat, An n <> C0) -> Rseq_cv (fun n : nat => Cnorm (An (S n) / An n)) (Cnorm lambda) -> forall r, Rabs r < / (Cnorm lambda) -> Cv_radius_weak An r.
proof: Proof. intros An lam lam_pos An_neq An_frac_cv r r_bd. assert (middle_lb := proj1 (middle_is_in_the_middle _ _ r_bd)). assert (middle_ub := proj2 (middle_is_in_the_middle _ _ r_bd)). assert (middle_pos : 0 < middle (Rabs r) (/Cnorm lam)). apply Rle_lt_trans with (Rabs r) ; [apply Rabs_pos | assumption]. pose (eps := (/ (middle (Rabs r) (/ Cnorm lam)) - Cnorm lam)%R). assert (eps_pos : 0 < eps). apply Rgt_minus ; rewrite <- Rinv_involutive. apply Rinv_lt_contravar. apply Rmult_lt_0_compat ; [| apply Rinv_0_lt_compat] ; assumption. assumption. apply Rgt_not_eq ; assumption. apply Cpser_alembert_prelim2 with (Cnorm lam + eps)%R. lra. apply An_neq. destruct (An_frac_cv (/ (middle (Rabs r) (/ Cnorm lam)) - Cnorm lam))%R as [N HN]. assumption. exists N ; intro n. apply Rle_trans with (Cnorm lam + (Cnorm (An (S (N + n)) / An (N + n)%nat) - Cnorm lam))%R. right ; ring. apply Rplus_le_compat_l ; apply Rle_trans with (R_dist (Cnorm (An (S (N + n)) / An (N + n)%nat)) (Cnorm lam))%R. apply RRle_abs. left ; apply HN ; intuition. replace (Cnorm lam + eps)%R with (/ (middle (Rabs r) (/ Cnorm lam)))%R. rewrite Rinv_involutive ; [| apply Rgt_not_eq] ; assumption. unfold eps ; ring. 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