proposition: Theorem Rpser_alembert_weak_reciprocal_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, / lambda < Rabs r -> ~ Cv_radius_weak An r.
proof: Proof. intros An lam lam_neq [N An_neq] An_frac_cv r r_bd Hf. assert (H := proj1 (Cv_radius_weak_shifts_compat _ _ N) Hf). revert H. apply Rpser_alembert_weak_reciprocal with lam ; try assumption. 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