proposition: Lemma InfiniteGeometricSum_bound : forall series (Gs:GeometricSeries series), (-'(err_bound series) <= InfiniteGeometricSum Gs /\ InfiniteGeometricSum Gs <= '(err_bound series))%CR.
proof: Proof. intros series Gs. assert (Y:0 < 1 - a). { change (0 < 1 + - a). rewrite <- Qlt_minus_iff. assumption. } destruct (Qeq_dec (err_bound series) 0) as [Hq|Hq]. - setoid_replace (InfiniteGeometricSum Gs) with 0%CR. split; simpl; rewrite -> Hq; try apply CRle_refl. rewrite CRopp_0. apply CRle_refl. apply regFunEq_equiv, regFunEq_e. intros e. apply ball_sym. change (approximate (InfiniteGeometricSum Gs) e) with (InfiniteGeometricSum_raw series e). rewrite InfiniteGeometricSum_raw_correct. 2: exact Gs. simpl. unfold Qball. unfold QAbsSmall. setoid_replace (0 - InfiniteSum_fat (err_prop (proj1_sig e)) series 0 (Pos.to_nat (InfiniteGeometricSum_maxIter series e)))%Q with 0. split. apply (Qopp_le_compat 0), (Qpos_nonneg (e+e)). apply (Qpos_nonneg (e+e)). unfold canonical_names.equiv, stdlib_rationals.Q_eq. unfold Qminus. rewrite Qplus_0_l. assert (X:err_prop (proj1_sig e) series = true). rewrite -> err_prop_prop. rewrite -> Hq. apply Qpos_nonneg. destruct (InfiniteGeometricSum_maxIter series e) using Pind. simpl. destruct (err_prop (proj1_sig e) series). reflexivity. discriminate. rewrite Pos2Nat.inj_succ. simpl. destruct (err_prop (proj1_sig e) series). reflexivity. discriminate. - cut (-(' err_bound series) <= InfiniteGeometricSum Gs /\ InfiniteGeometricSum Gs <= 'err_bound series)%CR. + intros [H0 H1]. split; assumption. + setoid_replace (InfiniteGeometricSum Gs) with (InfiniteGeometricSum Gs - 0)%CR by (unfold canonical_names.equiv, msp_Equiv; ring). apply CRAbsSmall_ball. apply regFunBall_e. intros d. change (approximate (InfiniteGeometricSum Gs) d) with (InfiniteGeometricSum_raw series d). rewrite InfiniteGeometricSum_raw_correct. 2: exact Gs. simpl. set (p:=(InfiniteGeometricSum_maxIter series d)). unfold Qball. rewrite <- AbsSmall_Qabs. unfold Qminus. rewrite Qplus_0_r. apply (err_prop_correct _ (proj1_sig d+err_bound series+proj1_sig d)); try assumption. apply err_prop_monotone with (err_bound series). simpl. apply (Qle_trans _ (0 + err_bound series + 0)). rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. apply Qplus_le_compat. apply Qplus_le_compat. apply Qpos_nonneg. apply Qle_refl. apply Qpos_nonneg. rewrite -> err_prop_prop. apply Qle_refl. 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