proposition: Lemma AltSeries_correct : forall (X:Type) (f : X*Q->X*Q) x cvmod (fdecr : Str_alt_decr X f x) (flz : Limit_zero X f x cvmod) (g:nat -> IR) (H : convergent g), (forall n:positive, inj_Q IR (Str_pth _ f n x)%Q [=] g (Pos.to_nat n)) -> (IRasCR (g O) + AltSeries _ f x cvmod fdecr flz == IRasCR (series_sum g H))%CR.
proof: Proof. intros. unfold series_sum. rewrite -> IR_Lim_as_CR. apply (SeqLimit_unique CRasCReals). intros e He. generalize (IR_Cauchy_prop_as_CR (Build_CauchySeq IR (seq_part_sum g) H)). intro C. destruct (C _ (pos_div_two CRasCOrdField _ He)) as [n Hn]. exists (S (S n)). intros m Hm. unfold CS_seq in *. clear C. unfold seq_part_sum in *. destruct m. exfalso; inversion Hm. apply le_S_n in Hm. assert (forall k:positive, le n (Pos.to_nat k) -> AbsSmall e (inject_Q_CR (Str_pth _ f k x))) as kSmall. { intros. stepr (IRasCR (g (Pos.to_nat k))). setoid_replace (IRasCR (g (Pos.to_nat k))) with (@Sum CRasCAbGroup (Pos.to_nat k) (Pos.to_nat k) (fun n => IRasCR (g n))) by (rewrite Sum_one; reflexivity). unfold Sum, Sum1. rewrite <- IR_Sum0_as_CR, <- IR_Sum0_as_CR. stepr ((IRasCR (Sum0 (G:=IR) (S (Pos.to_nat k)) g) - (IRasCR (Sum0 (G:=IR) n g))) + (IRasCR (Sum0 (G:=IR) n g) - IRasCR (Sum0 (G:=IR) (Pos.to_nat k) g)))%CR by (unfold cg_minus; simpl; unfold msp_Equiv; ring). apply (AbsSmall_eps_div_two CRasCOrdField e (IRasCR (Sum0 (S (Pos.to_nat k)) g) - IRasCR (Sum0 n g)) (IRasCR (Sum0 n g) - IRasCR (Sum0 (Pos.to_nat k) g)))%CR. apply (Hn (S (Pos.to_nat k))). apply le_S, H1. apply (AbsSmall_minus CRasCOrdField (e [/]TwoNZ) (IRasCR (Sum0 (Pos.to_nat k) g)) (IRasCR (Sum0 n g))). apply Hn. exact H1. rewrite <- IR_inj_Q_as_CR. apply IRasCR_wd. symmetry. apply H0. } stepr (IRasCR (Sum0 (S m) g) - IRasCR (g 0%nat) - AltSeries X f x cvmod fdecr flz)%CR by (unfold cg_minus; simpl; unfold msp_Equiv; ring). setoid_replace (IRasCR (Sum0 (S m) g) - IRasCR (g 0%nat))%CR with (inject_Q_CR (snd (CRstreams.iterate _ (λ y : X * Q * Q, let (z0, r1) := f (fst y) in (z0, r1, Qred (r1 + snd y))) (Pos.of_nat m) (x,0%Q)))). - apply AltSeries_remainder. apply kSmall. rewrite Nat2Pos.id. apply (Nat.le_trans _ (S n)). apply le_S, Nat.le_refl. exact Hm. destruct m. inversion Hm. discriminate. - clear kSmall. replace (S m) with (S (Pos.to_nat (Pos.of_nat m))). generalize (Pos.of_nat m). clear Hm m. apply Pos.peano_ind. + rewrite SumStream_red. rewrite CRstreams.iterate_one. specialize (H0 xH). unfold Str_pth, Pos.to_nat in H0. simpl in H0. simpl. destruct (f x). simpl. simpl in H0. rewrite <- IR_minus_as_CR, <- IR_inj_Q_as_CR. apply IRasCR_wd. rewrite cm_lft_unit, cag_commutes. unfold cg_minus. rewrite <- CSemiGroups.plus_assoc. rewrite cg_rht_inv_unfolded, cm_rht_unit. rewrite <- H0. apply inj_Q_wd. rewrite Qplus_0_r. reflexivity. + intros p IHp. simpl (Sum0 (S (Pos.to_nat (Pos.succ p))) g). rewrite IR_plus_as_CR. rewrite (CRplus_comm (IRasCR (Sum0 (Pos.to_nat (Pos.succ p)) g))). rewrite Pos2Nat.inj_succ. rewrite <- CRplus_assoc, IHp. clear IHp. rewrite SumStream_red. rewrite SumStream_red. rewrite CRstreams.iterate_succ. rewrite SumStream_fst. simpl. rewrite <- CRstreams.iterate_succ. specialize (H0 (Pos.succ p)). unfold Str_pth in H0. destruct (CRstreams.iterate (X and Q) f (Pos.succ p) x). simpl. simpl in H0. rewrite Pos2Nat.inj_succ in H0. rewrite <- CRplus_Qplus. apply CRplus_eq_l. rewrite <- IR_inj_Q_as_CR. apply IRasCR_wd. symmetry. exact H0. + rewrite Nat2Pos.id. reflexivity. destruct m. inversion Hm. discriminate. 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