proposition: Lemma AltSeries_shift_pth : forall (p:positive) (X : Type) f x cvmod decr lz, (AltSeries X f x cvmod decr lz == inject_Q_CR (snd (CRstreams.iterate _ (fun y : (X * Q) * Q => let (z0, r1) := f (fst y) in (z0, r1, Qred (r1 + snd y))) p (x, 0%Q))) + AltSeries X f (CRstreams.iterate _ f p x) _ (Str_alt_decr_tl X f x p decr) (Limit_zero_tl X f x cvmod p decr lz))%CR.
proof: Proof. apply (Pos.peano_ind (fun p => forall X f x cvmod decr lz, (AltSeries X f x cvmod decr lz == inject_Q_CR (snd (CRstreams.iterate _ (fun y : (X * Q) * Q => let (z0, r1) := f (fst y) in (z0, r1, Qred (r1 + snd y))) p (x, 0%Q))) + AltSeries X f _ _ (Str_alt_decr_tl X f x p decr) (Limit_zero_tl X f x cvmod p decr lz))%CR)). - intros. rewrite AltSeries_shift. apply CRplus_eq_l. rewrite SumStream_red. rewrite iterate_one. simpl. destruct (f x). simpl. rewrite Qplus_0_r. reflexivity. - intros. setoid_replace (AltSeries X f (CRstreams.iterate (X * Q) f (Pos.succ p) x) (fun e : Qpos => (cvmod e - Pos.succ p)%positive) (Str_alt_decr_tl X f x (Pos.succ p) decr) (Limit_zero_tl X f x cvmod (Pos.succ p) decr lz)) with (AltSeries X f (CRstreams.iterate (X * Q) f p (f x)) _ (Str_alt_decr_tl X f (f x) p (Str_alt_decr_tl X f x 1 decr)) (Limit_zero_tl X f (f x) _ p (Str_alt_decr_tl X f x 1 decr) (Limit_zero_tl X f x _ 1 decr lz))). + setoid_replace (inject_Q_CR (snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, Qred (r1 + snd y))) (Pos.succ p) (x, 0)))) with (inject_Q_CR (snd (f x)) + inject_Q_CR (snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, Qred (r1 + snd y))) p (f x, 0%Q))))%CR. rewrite <- CRplus_assoc, <- (H X f (f x)). rewrite <- AltSeries_shift. reflexivity. clear H. rewrite SumStream_red, SumStream_red. rewrite iterate_succ. rewrite SumStream_fst. simpl. rewrite CRplus_Qplus. apply inject_Q_CR_wd. transitivity (snd (f (CRstreams.iterate (X * Q) f p x) ) + snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z1, r0) := f (fst y) in (z1, r0, r0 + snd y)) p (x, 0))). destruct (f (CRstreams.iterate (X * Q) f p x)); reflexivity. pose proof (SumStream_assoc X f x 1 p). rewrite iterate_one, iterate_one in H. setoid_replace (snd (let (z, r0) := f (fst (x, 0)) in (z, r0, r0 + snd (x, 0)))%Q) with (snd (f x))%Q in H. rewrite <- H. clear H. rewrite Pos.add_1_l, iterate_succ, SumStream_fst. unfold fst. destruct (f (CRstreams.iterate (X * Q) f p x)). simpl. reflexivity. simpl. destruct (f x). simpl. rewrite Qplus_0_r. reflexivity. + apply AltSeries_wd. intros. rewrite iterate_succ, iterate_shift. reflexivity. intro e. rewrite <- Pos.add_1_l. rewrite sym_sub_add_distr. reflexivity. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra