proposition: Lemma AltSeries_raw_correct : forall (e:Qpos) (cvmod : Qpos -> positive), 0 < snd fInit -> Qball (` e * (1 # 2)) (AQtoQ (AltSeries_raw fInit cvmod (Qpos2QposInf e))) (SumStream _ g gInit (cvmod (e * (1 # 2))%Qpos) (AQposAsQpos (exist _ _ (app_inverse_below_pos (e * (1 # 2))%Qpos)))).
proof: Proof. intros e0 cvmod xpos. unfold SumStream. change (` (AQposAsQpos (app_inverse_below (e0 * (1 # 2))%Qpos ↾ app_inverse_below_pos (e0 * (1 # 2))%Qpos))) with (AQtoQ (app_inverse_below (e0 * (1 # 2))%Qpos)). pose proof (iterate_stop_correct _ (fun y : (X and Q) and Q => let (z, r) := g (fst y) in (z, r, Qred (r + snd y))) (fun y : (X and Q) and Q => Qle_bool (Qabs (snd (fst y))) (AQtoQ (app_inverse_below (e0 * (1 # 2) ↾ eq_refl)))) (cvmod (e0 * (1 # 2))%Qpos) (gInit,0)) as [p [qeq [H5 H6]]]. rewrite qeq. clear qeq. unfold AltSeries_raw. replace (StopIndex fInit (app_inverse_below (e0 * (1 # 2) ↾ eq_refl)) (cvmod (e0 * (1 # 2))%Qpos)) with p. setoid_replace (` e0 * (1 # 2))%Q with (` e0 * (1 # 2 * p) * inject_Z (Zpos p))%Q. apply (div_approx_error p (e0*(1#2*p))). rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity. unfold Qmult, Qeq; simpl. rewrite Pos.mul_1_r, Pos.mul_comm. reflexivity. rewrite SumStream_fst_red in H6. destruct H6 as [fuel | predicate]. - subst p. symmetry. apply StopIndex_stop_fuel. intros. specialize (H5 p H6). rewrite SumStream_fst_red in H5. unfold fst in H5. unfold IsStopIndex. intro abs. pose proof (g_pth p). unfold Str_pth in H7. rewrite H7 in H5. clear H7. pose proof (denomPos_iter p (xH,fInit) xpos). destruct (CRstreams.iterate _ fS p (1%positive, fInit)) as [u v]. apply abs_div_aqtoq_shift in abs. apply Qle_bool_iff in abs. rewrite abs in H5. discriminate. exact H7. - assert (IsStopIndex fInit (app_inverse_below (e0 * (1 # 2))%Qpos) p) as pstop. { destruct predicate as [_ predicate]. unfold IsStopIndex. apply Qle_bool_iff in predicate. simpl in predicate. pose proof (g_pth p). unfold Str_pth in H6. rewrite H6 in predicate. clear H6. pose proof (denomPos_iter p (xH,fInit) xpos). destruct (CRstreams.iterate _ fS p (1%positive, fInit)). apply abs_div_aqtoq_shift. exact H6. exact predicate. } symmetry. apply StopIndex_correct. exact pstop. intros. unfold IsStopIndex. specialize (H5 q H6). rewrite SumStream_fst_red in H5. unfold fst in H5. pose proof (g_pth q). unfold Str_pth in H7. rewrite H7 in H5. clear H7. pose proof (denomPos_iter q (xH,fInit) xpos). destruct (CRstreams.iterate _ fS q (1%positive, fInit)). intro abs. apply abs_div_aqtoq_shift in abs. apply Qle_bool_iff in abs. rewrite abs in H5. discriminate. exact H7. apply Pos.lt_le_incl, predicate. 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