proposition: Lemma AltSeries_raw_prf : forall (cvmod : Qpos -> positive), Str_alt_decr _ g gInit -> 0 < snd fInit -> Limit_zero _ g gInit cvmod -> is_RegularFunction (@ball AQ_as_MetricSpace) (AltSeries_raw fInit cvmod).
proof: Proof. intros cvmod g_decr xpos lz e1 e2. setoid_replace (`e1 + `e2)%Q with (`e1*(1#2) + (`e1*(1#2) + `e2*(1#2) + `e2*(1#2)))%Q by ring. apply (ball_triangle Q_as_MetricSpace _ _ _ (SumStream _ g gInit (cvmod (e1 * (1 # 2))%Qpos) (AQposAsQpos (exist _ _ (app_inverse_below_pos (e1 * (1 # 2))%Qpos))))). 2: apply (ball_triangle Q_as_MetricSpace _ _ _ (SumStream _ g gInit (cvmod (e2 * (1 # 2))%Qpos) (AQposAsQpos (exist _ _ (app_inverse_below_pos (e2 * (1 # 2))%Qpos))))). - exact (AltSeries_raw_correct _ _ xpos). - apply (AltSeries_further _ g gInit _ _ _ _ (e1 * (1 # 2))%Qpos (e2 * (1 # 2))%Qpos g_decr). apply lz. apply lz. apply app_inverse_below_correct. apply app_inverse_below_correct. - apply ball_sym, (AltSeries_raw_correct _ _ xpos). Qed.
imports: Coq.QArith.Qabs CoRN.util.Qdlog CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.model.reals.CRreal CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.ARArith