proposition: Lemma AltSeries_convergent_pos : forall (X:Type) (f : X*Q->X*Q) x cvmod (fdecr : Str_alt_decr X f x) (flz : Limit_zero X f x cvmod), 0 <= Str_pth _ f 1 x -> convergent (fun n:nat => inj_Q IR (Str_pth _ f (Pos.of_nat (S n)) x)).
proof: Proof. intros. assert (forall n:nat, [--] [1] [^] n [=] (inj_Q IR ((-1)^n))) as power_neg_one. { intro n. rewrite inj_Q_power. apply nexp_wd. rewrite (inj_Q_inv IR 1), inj_Q_One. reflexivity. } apply (convergent_wd (fun n : nat => [--][1][^]n[*]([--][1][^]n[*]inj_Q IR (Str_pth _ f (Pos.of_nat (S n)) x)))). - intro n. rewrite power_neg_one. rewrite <- inj_Q_mult, <- inj_Q_mult. apply inj_Q_wd. rewrite Qmult_assoc. rewrite <- Qpower_plus. replace (n+n)%Z with (2* Z.of_nat n)%Z. rewrite Qpower_mult. replace ((-1)^2) with 1%Q by reflexivity. rewrite Qpower_1, Qmult_1_l. reflexivity. ring. intro abs. discriminate. - apply alternate_series_conv. + clear flz. intro n. pose proof (Str_alt_decr_pos X f x fdecr n). rewrite power_neg_one. rewrite <- inj_Q_mult, <- inj_Q_Zero. apply inj_Q_leEq, H0, H. + intros e epos. destruct (Q_dense_in_CReals IR e epos) as [q qpos qmaj]. apply (less_wdl IR [0] _ (inj_Q IR 0)) in qpos. apply less_inj_Q in qpos. specialize (flz (exist _ _ qpos)). exists (Pos.to_nat (cvmod (exist _ _ qpos))). intros m H1. apply (AbsSmall_wdr _ _ (inj_Q IR ((-1)^m * Str_pth X f (Pos.of_nat (S m)) x))). 2: rewrite inj_Q_mult, power_neg_one; rational. apply (AbsSmall_trans _ (inj_Q IR q) _ _ qmaj). apply inj_Q_AbsSmall. apply AbsSmall_Qabs. refine (Qle_trans _ _ _ _ flz). clear flz. rewrite Qabs_pos. 2: apply (Str_alt_decr_pos X f x fdecr), H. rewrite <- (Pos2Nat.id (cvmod (q ↾ qpos))). pose proof (Pos2Nat.is_pos (cvmod (q ↾ qpos))). destruct (Pos.to_nat (cvmod (q ↾ qpos))). exfalso; inversion H0. clear H0. rewrite <- (Qmult_1_l (Qabs (Str_pth X f (Pos.of_nat (S n)) x))). rewrite <- (abs_power_neg_one n). rewrite <- Qabs_Qmult, Qabs_pos. 2: apply (Str_alt_decr_pos X f x fdecr), H. revert m n H1. induction m. intros. exfalso; inversion H1. intros. apply Nat.le_succ_r in H1. destruct H1. specialize (IHm n H0). apply (Qle_trans _ _ _ (Str_alt_decr_decr X f x fdecr m H) IHm). inversion H0. subst n. apply Str_alt_decr_decr. exact fdecr. exact H. rewrite inj_Q_Zero. reflexivity. + intro n. rewrite power_neg_one, power_neg_one. rewrite <- inj_Q_mult, <- inj_Q_mult. apply inj_Q_leEq. apply Str_alt_decr_decr; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.iso_CReals CoRN.reals.Q_in_CReals Coq.setoid_ring.ArithRing CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.fast.CRabs Coq.Bool.Bool CoRN.algebra.COrdAbs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax Coq.QArith.Qpower Coq.QArith.Qabs MathClasses.theory.CoqStreams CoRN.transc.PowerSeries CoRN.tactics.CornTac CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.series MathClasses.theory.streams CoRN.reals.fast.CRAlternatingSum