proposition: Lemma Rpser_alembert_weak : forall (An : Rseq) (lambda : R), lambda <> 0 -> (forall n : nat, An n <> 0) -> Rseq_cv (fun n : nat => Rabs (An (S n) / An n)) lambda -> forall r, Rabs r < / lambda -> Cv_radius_weak An r.
proof: Proof. intros An lam lam_neq An_neq An_frac_cv r r_bd. assert (lam_pos : 0 < lam). apply Rle_neq_lt ; [| symmetry ; exact lam_neq]. eapply Rseq_positive_limit ; [| eassumption] ; intro n ; compute ; apply Rabs_pos. 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) (/ lam)). apply Rle_lt_trans with (Rabs r) ; [apply Rabs_pos | assumption]. pose (eps := (/ (middle (Rabs r) (/ lam)) - lam)%R). assert (eps_pos : 0 < eps). apply Rgt_minus ; rewrite <- Rinv_inv. apply Rinv_lt_contravar. apply Rmult_lt_0_compat ; [| apply Rinv_0_lt_compat] ; assumption. assumption. apply Rpser_alembert_prelim2 with (lam + eps)%R. lra. apply An_neq. destruct (An_frac_cv (/ (middle (Rabs r) (/ lam)) - lam))%R as [N HN]. assumption. exists N ; intro n ; unfold Rseq_shifts. transitivity (lam + (Rabs (An (S (N + n)) / An (N + n)%nat) - lam))%R. right ; ring. apply Rplus_le_compat_l ; apply Rle_trans with (R_dist (Rabs (An (S (N + n)) / An (N + n)%nat)) lam)%R. apply RRle_abs. left ; apply HN ; intuition (auto with arith). replace (lam + eps)%R with (/ (middle (Rabs r) (/ lam)))%R. rewrite Rinv_inv ; assumption. unfold eps ; ring. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics