proposition: Lemma Rpser_alembert_infinite : forall (An : Rseq), Rseq_eventually (fun un => forall n, un n <> 0) An -> Rseq_cv (fun n : nat => Rabs (An (S n) / An n)) R0 -> infinite_cv_radius An.
proof: Proof. intros An [N1 HN1] An_frac_0 r. assert (eps_pos : 0 < /(Rabs r + 1)). apply Rinv_0_lt_compat ; apply Rplus_le_lt_0_compat ; [apply Rabs_pos | apply Rlt_0_1]. destruct (An_frac_0 (/ (Rabs r + 1))%R eps_pos) as [N2 HN2]. rewrite (Cv_radius_weak_shifts_compat _ _ (Nat.max N1 N2)). apply Rpser_alembert_prelim with (/ (Rabs r + 1)). assumption. intro n ; unfold Rseq_shifts. destruct (max_explicit N1 N2) as [p Hp] ; rewrite Hp, <- Nat.add_assoc ; apply HN1. intro n ; unfold Rseq_shifts ; rewrite Nat.max_comm ; destruct (max_explicit N2 N1) as [p Hp] ; rewrite Hp, <- Rabs_Rabsolu ; replace (N2 + p + S n)%nat with (S (N2 + p + n)) by ring ; assert (Hyp := HN2 (N2 + p + n)%nat) ; unfold R_dist, Rminus in Hyp ; change R0 with (IZR 0) in Hyp; rewrite Ropp_0, Rplus_0_r in Hyp ; left ; apply Hyp. lia. rewrite Rinv_inv ; intuition (auto with real). 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