proposition: Lemma InfiniteGeometricSum_raw_prf : forall series, GeometricSeries series -> is_RegularFunction Qball (InfiniteGeometricSum_raw series).
proof: Proof. intros series H e0 e1. rewrite InfiniteGeometricSum_raw_correct. rewrite InfiniteGeometricSum_raw_correct. 2: exact H. 2: exact H. pose proof (InfiniteGeometricSum_maxIter_correct e0 H) as H0. pose proof (InfiniteGeometricSum_maxIter_correct e1 H) as H1. destruct (Qle_total (proj1_sig e1) (proj1_sig e0)). - apply ball_weak. apply Qpos_nonneg. apply (err_prop_tail_correct _ _ H q H0 H1). - rewrite Qplus_comm. apply ball_weak. apply Qpos_nonneg. apply ball_sym. apply (err_prop_tail_correct _ _ H q H1 H0). 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