proposition: Theorem Rpser_alembert_weak_eventually : forall (An : Rseq) (lambda : R), lambda <> 0 -> Rseq_eventually (fun un => forall n : nat, un n <> 0) An -> 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 [N An_neq] An_frac_cv r r_bd. rewrite Cv_radius_weak_shifts_compat ; apply Rpser_alembert_weak with lam ; try (assumption || apply An_neq). apply Rseq_cv_eq_compat with (Rseq_shifts (fun n => Rabs (An (S n) / An n)) N). intro n ; unfold Rseq_shifts ; rewrite plus_n_Sm ; reflexivity. apply Rseq_cv_shifts_compat_reciprocal ; assumption. 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