proposition: Lemma GeometricSeries_convergent : forall (a : Q) (apos : 0 <= a) (aone : a < 1) (series:Stream Q), GeometricSeries a series -> convergent (fun n => inj_Q IR (Str_nth n series)).
proof: Proof. intros a apos aone series H. apply ratio_test_conv. exists 0%nat. exists (inj_Q IR a). rstepr (nring 1:IR). stepr (inj_Q IR (nring 1)); [| now apply (inj_Q_nring IR 1)]. apply inj_Q_less. assumption. assert (Ha0':[0][<=]inj_Q IR a). rstepl (nring 0:IR). stepl (inj_Q IR (nring 0)); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_leEq. assumption. split. assumption. intros n _. destruct (ForAll_Str_nth_tl n H) as [H0 _]. stepr (inj_Q IR a[*](inj_Q IR (Qabs (Str_nth n series)))); [| now apply mult_wdr; apply eq_symmetric; apply AbsIR_Qabs]. stepl (inj_Q IR (Qabs (Str_nth (S n) series))); [| now apply eq_symmetric; apply AbsIR_Qabs]. rewrite <- inj_Q_mult. apply inj_Q_leEq. replace (S n) with (1+n)%nat by auto with *. rewrite <- Str_nth_plus. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.iso_CReals CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRGeometricSum CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qabs Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.Q_in_CReals CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.transc.ArTanH CoRN.reals.fast.CRarctan_small CoRN.tactics.Qauto CoRN.tactics.CornTac