proposition: Lemma InfiniteGeometricSum_step : forall series (Gs:GeometricSeries series), (InfiniteGeometricSum Gs == ('(hd series))+(InfiniteGeometricSum (ForAll_Str_nth_tl 1%nat Gs)))%CR.
proof: Proof. intros series Gs. rewrite -> CRplus_translate. apply regFunEq_equiv, regFunEq_e. intros e. change (approximate (InfiniteGeometricSum Gs) e) with (InfiniteGeometricSum_raw series e). rewrite InfiniteGeometricSum_raw_correct. 2: exact Gs. simpl (InfiniteGeometricSum (ForAll_Str_nth_tl 1 Gs)). change (approximate (translate (hd series) (InfiniteGeometricSum (ForAll_Str_nth_tl 1 Gs))) e) with (hd series + (InfiniteGeometricSum_raw (tl series) e)). rewrite InfiniteGeometricSum_raw_correct. 2: apply Gs. simpl. rewrite InfiniteSum_fat_extend. 2: apply InfiniteGeometricSum_maxIter_correct, Gs. simpl. case_eq (err_prop (proj1_sig e) series); intros He. - apply ball_sym. simpl. unfold Qball. rewrite <- AbsSmall_Qabs. unfold Qminus. rewrite Qplus_0_r. eapply Qle_trans. apply Qabs_triangle. apply Qplus_le_compat; simpl. rewrite -> err_prop_prop in He. unfold err_bound in He. assert (X:0 < 1 - a). change (0 < 1 + - a). rewrite <- Qlt_minus_iff. assumption. clear - He Ha0 X. setoid_replace (Qabs (hd series)) with ((Qabs (hd series)/(1-a))*(1-a)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field). 2: auto with *. apply (Qle_trans _ ((proj1_sig e) * (1-a))). apply Qmult_le_compat_r. exact He. apply Qlt_le_weak, X. rewrite <- (Qmult_1_r (proj1_sig e)) at 2. apply Qmult_le_l. apply Qpos_ispos. rewrite <- (Qplus_0_r 1) at 2. apply Qplus_le_r. apply (Qopp_le_compat 0), Ha0. apply err_prop_correct. destruct Gs; assumption. apply err_prop_monotone'; assumption. - assert (Qplus' 0 (hd series) == hd series). { rewrite Qplus'_correct. apply Qplus_0_l. } rewrite (InfiniteSum_fat_wd _ _ _ H). rewrite InfiniteSum_fat_plus. rewrite (@InfiniteSum_fat_add_stop (Pos.to_nat (InfiniteGeometricSum_maxIter series e)) (Pos.to_nat (InfiniteGeometricSum_maxIter (tl series) e))). apply Qball_Reflexive. apply (Qpos_nonneg (e+e)). apply Pos2Nat.inj_le. apply (@InfiniteGeometricSum_maxIter_monotone series e), Gs. apply InfiniteGeometricSum_maxIter_correct, Gs. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv