proposition: Lemma InfiniteGeometricSum_correct : forall (a : Q) (apos : 0 <= a) (aone : a < 1) (series:Stream Q) (x:nat -> IR), (forall n:nat, inj_Q IR (Str_nth n series)%Q[=]x n) -> forall (Gs:GeometricSeries a series) H, (InfiniteGeometricSum apos aone Gs==IRasCR (series_sum x H))%CR.
proof: Proof. intros a apos aone seq x Hx Gs H. 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 x) H)). intros C. destruct (C _ (pos_div_two _ _ He)) as [n Hn]. exists n. intros m Hm. unfold CS_seq in *. clear C. unfold seq_part_sum in *. setoid_replace (@cg_minus CRasCGroup (IRasCR (Sum0 m x)) (InfiniteGeometricSum apos aone Gs)) with (((IRasCR (Sum0 (G:=IR) m x) - (IRasCR (Sum0 (G:=IR) n x))) + ((IRasCR (Sum0 (G:=IR) n x) - InfiniteGeometricSum apos aone Gs))))%CR by (unfold cg_minus; simpl; ring). apply (AbsSmall_eps_div_two CRasCOrdField e (IRasCR (Sum0 m x) - IRasCR (Sum0 n x)) (IRasCR (Sum0 n x) - InfiniteGeometricSum apos aone Gs))%CR. exact (Hn m Hm). clear m Hm. setoid_replace (IRasCR (Sum0 n x)) with ('(@Sum0 Q_as_CAbGroup n (fun n => (Str_nth n seq))%Q))%CR. revert seq x H Hx Gs Hn. induction n. intros seq x H Hx Gs Hn. simpl (Sum0 0 (fun n : nat => Str_nth n seq)). apply (AbsSmall_minus CRasCOrdField (e [/]TwoNZ) (InfiniteGeometricSum apos aone Gs) 0%CR). setoid_replace (@cg_minus CRasCOrdField (InfiniteGeometricSum apos aone Gs) 0%CR) with (InfiniteGeometricSum apos aone Gs) by (unfold cg_minus; simpl; ring). assert (Hn' : forall m : nat, (0 <= m)%nat -> AbsSmall (R:=CRasCOrdField) (e [/]TwoNZ) (IRasCR (Sum0 (G:=IR) m x))). { intros m Hm. setoid_replace (IRasCR (Sum0 m x)) with (@cg_minus CRasCOrdField (IRasCR (Sum0 (G:=IR) m x)) (IRasCR (Sum0 (G:=IR) 0 x))). apply Hn; assumption. unfold cg_minus. simpl. rewrite -> IR_Zero_as_CR. ring. } stepl (IRasCR (CRasIR (e[/]TwoNZ)))%CR; [| now apply CRasIRasCR_id]. stepr (IRasCR (CRasIR (InfiniteGeometricSum apos aone Gs)))%CR; [| now apply CRasIRasCR_id]. rewrite <- IR_AbsSmall_as_CR. apply AbsSmall_approach. intros d Hd. rewrite -> IR_AbsSmall_as_CR. stepr (InfiniteGeometricSum apos aone Gs); [| now apply eq_symmetric; apply CRasIRasCR_id]. destruct (Q_dense_in_CReals IR d) as [q Hq0 Hq]. assumption. assert (Hq0': 0 < q). apply (less_inj_Q IR). stepl ([0]:IR). assumption. apply eq_symmetric; apply (inj_Q_nring IR 0). destruct (InfiniteGeometricSum_small_tail apos aone (exist _ _ Hq0') Gs) as [m Hm]. setoid_replace (InfiniteGeometricSum apos aone Gs) with ((IRasCR (Sum0 (G:=IR) m x)) + ((InfiniteGeometricSum apos aone Gs) - (IRasCR (Sum0 (G:=IR) m x))))%CR by ring. stepl (IRasCR (CRasIR (e [/]TwoNZ)) + (IRasCR d))%CR; [| now apply eq_symmetric; apply IR_plus_as_CR]. apply (AbsSmall_plus CRasCOrdField (IRasCR (CRasIR (e [/]TwoNZ))) (IRasCR d) (IRasCR (Sum0 m x)) (InfiniteGeometricSum apos aone Gs - IRasCR (Sum0 m x)))%CR. stepl (e [/]TwoNZ); [| now apply eq_symmetric; apply CRasIRasCR_id]. apply Hn'; auto with *. apply AbsSmall_leEq_trans with ('q)%CR. stepl (IRasCR (inj_Q IR q)); [| now apply IR_inj_Q_as_CR]. rewrite <- IR_leEq_as_CR. apply less_leEq. assumption. simpl in Hm. clear - Hm Hx. revert seq x Hx Gs Hm. induction m. intros seq x Hx Gs Hm. stepr (InfiniteGeometricSum apos aone Gs). apply Hm. unfold cg_minus. simpl. rewrite -> IR_Zero_as_CR. unfold msp_Equiv; ring. intros seq x Hx Gs Hm. setoid_replace (InfiniteGeometricSum apos aone Gs - IRasCR (Sum0 (S m) x))%CR with (InfiniteGeometricSum apos aone (ForAll_Str_nth_tl 1 Gs) - IRasCR (Sum0 (G:=IR) m (fun n => (x (S n)))))%CR. apply IHm. intros n. stepl ((inj_Q IR (Str_nth (S n) seq)%Q)). apply Hx. apply eq_reflexive. intros. apply Hm. rewrite -> InfiniteGeometricSum_step. setoid_replace (IRasCR (Sum0 (G:=IR) (S m) x)) with (IRasCR (inj_Q _ (CoqStreams.hd seq) [+](Sum0 (G:=IR) m (fun n0 : nat => (x (S n0)))%Q))). rewrite -> (IR_plus_as_CR). rewrite -> IR_inj_Q_as_CR. ring. apply IRasCR_wd. apply eq_symmetric. stepl (x O[+]Sum0 (G:=IR) m (fun n0 : nat => (x (S n0)))). apply Sum0_shift. intros i. apply eq_reflexive. apply bin_op_wd_unfolded. apply eq_symmetric. apply (Hx O). apply eq_reflexive. intros seq x H Hx Gs Hn. set (y:=(fun n => (x (n + 1)%nat))). setoid_replace (' Sum0 (S n) (fun n0 : nat => Str_nth n0 seq) - InfiniteGeometricSum apos aone Gs)%CR with (('(((Sum0 (G:=Q_as_CAbGroup) n (fun n0 : nat => Str_nth n0 (CoqStreams.tl seq))%Q)))%CR) - InfiniteGeometricSum apos aone (ForAll_Str_nth_tl 1 Gs))%CR. apply (IHn (CoqStreams.tl seq) y ). apply tail_series with x. assumption. exists 1%nat. exists 0%nat. intros; apply eq_reflexive. intros m. unfold y. stepr ((inj_Q IR (Str_nth (m+1) seq))); [| now apply (Hx (m + 1)%nat)]. rewrite <- Str_nth_plus. apply eq_reflexive. intros m Hm. setoid_replace (@cg_minus CRasCOrdField (IRasCR (Sum0 m y)) (IRasCR (Sum0 n y))) with (IRasCR (Sum0 (G:=IR) (S m) x) - IRasCR (Sum0 (G:=IR) (S n) x))%CR. apply (Hn (S m)). apply le_n_S, Hm. symmetry. change (@cg_minus CRasCOrdField (IRasCR (Sum0 m y)) (IRasCR (Sum0 n y))) with (IRasCR (Sum0 m y) - IRasCR (Sum0 n y))%CR. do 2 rewrite <- IR_minus_as_CR. apply IRasCR_wd. stepr ((x O[+]Sum0 (G:=IR) m y[-](x O[+]Sum0 (G:=IR) n y))). apply bin_op_wd_unfolded;[|apply un_op_wd_unfolded]; apply eq_symmetric; apply Sum0_shift; intros; unfold y;rewrite Nat.add_comm; apply eq_reflexive. rational. rewrite -> InfiniteGeometricSum_step. set (z:=(fun n0 : nat => (Str_nth n0 seq)%Q)). setoid_replace ((Sum0 (G:=Q_as_CAbGroup) (S n) z):Q) with ((z O + (Sum0 (G:=Q_as_CAbGroup) n (fun n0 : nat => (Str_nth n0 (CoqStreams.tl seq))%Q)))). rewrite <- (CRplus_Qplus (z O)). unfold z, Str_nth. simpl. ring. symmetry. apply (@Sum0_shift Q_as_CAbGroup). intros i. reflexivity. clear - Hx. induction n. exact IR_Zero_as_CR. simpl. rewrite IR_plus_as_CR, IHn. rewrite <- CRplus_Qplus. apply CRplus_eq_r. transitivity (IRasCR (inj_Q IR (Str_nth n seq)%Q)). apply IRasCR_wd; symmetry; apply Hx. apply IR_inj_Q_as_CR. 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