proposition: Lemma Rpser_alembert_finite_eventually : forall (An : Rseq) (lambda : R), lambda <> 0 -> Rseq_eventually (fun un => forall n, un n <> 0) An -> Rseq_cv (fun n => Rabs (An (S n) / An n)) lambda -> finite_cv_radius An (/ lambda).
proof: Proof. intros An lam lam_neq An_neq An_l. assert (lam_pos : 0 < / lam). apply Rinv_0_lt_compat ; apply Rle_neq_lt ; [| symmetry ; exact lam_neq]. eapply Rseq_positive_limit ; [| eassumption] ; intro n ; compute ; apply Rabs_pos. split. intros r' [r'_pos r'_bd] ; apply Rpser_alembert_weak_eventually with lam ; [| | | rewrite Rabs_pos_eq] ; assumption. intros r' r'_lb ; apply Rpser_alembert_weak_reciprocal_eventually with lam ; [| | | rewrite Rabs_pos_eq ; [| left ; apply Rlt_trans with (/ lam)] ] ; 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