proposition: Lemma div_approx_error : ∀ (p:positive) (e:Qpos), Qball (` e * inject_Z (Zpos p)) (AQtoQ (snd (CRstreams.iterate _ (fSsum (Qdlog2 (` e))) p (1%positive, fInit, 0)))) (snd (CRstreams.iterate _ (fun y : X*Q*Q => let (z, r) := g (fst y) in (z, r, Qred (r + snd y))) p (gInit, 0))).
proof: Proof. apply (Pos.peano_ind (fun p => forall (e:Qpos), Qball (` e * inject_Z (Zpos p)) (AQtoQ (snd (CRstreams.iterate _ (fSsum (Qdlog2 (` e))) p (1%positive, fInit, 0)))) (snd (CRstreams.iterate _ (fun y : X*Q*Q => let (z, r) := g (fst y) in (z, r, Qred (r + snd y))) p (gInit, 0))))). - intros. rewrite iterate_one, iterate_one. rewrite Qmult_1_r. unfold fSsum, fS. unfold snd at 1. unfold fst at 2. pose proof (g_pth 1). unfold Str_pth in H5. simpl in H5. unfold snd at 3. replace (snd (let (z, r) := g gInit in (z, r, Qred (r + zero)))) with (Qred (snd (g gInit) + 0)) by (destruct (g gInit); reflexivity). rewrite Qred_correct, Qplus_0_r, H5. clear H5. destruct (f (1%positive, fInit)) as [u v]. unfold snd, fst. rewrite rings.plus_0_l. apply ball_weak_le with (e:= (2 ^ Qdlog2 (` e0))%Q). apply Qdlog2_spec, Qpos_ispos. apply aq_div. - intros. rewrite iterate_succ. unfold fSsum at 1. specialize (H5 e0). pose proof (fSsum_fst p (Qdlog2 (` e0))). destruct (CRstreams.iterate _ (fSsum (Qdlog2 (` e0))) p (1%positive, fInit, 0)) as [u approx_sum]. unfold snd in H5 at 1. unfold fst in H6. change (snd (let (a, b) := fS u in (a, b, approx_sum + app_div (fst b) (snd b) (Qdlog2 (` e0))))) with (approx_sum + app_div (fst (snd (fS u))) (snd (snd (fS u))) (Qdlog2 (` e0))). rewrite iterate_succ, SumStream_fst_red. unfold fst at 2. rewrite <- iterate_succ. pose proof (g_pth (Pos.succ p)) as H7. unfold Str_pth in H7. destruct (CRstreams.iterate (X and Q) g (Pos.succ p) gInit). unfold snd at 4. unfold snd in H7 at 1. rewrite Qred_correct, H7. clear H7 q x. rewrite iterate_succ. rewrite <- H6. clear H6. destruct (fS u) as [v w]. change (snd (v,w)) with w. clear v. destruct (CRstreams.iterate _ (fun y : (X and Q) and Q => let (z, r) := g (fst y) in (z, r, Qred (r + snd y))) p (gInit, 0)) as [v exact_sum]. unfold snd in H5. unfold snd at 3. clear v. destruct w as [v w]. unfold fst, snd. rewrite rings.preserves_plus. apply AbsSmall_Qabs. apply AbsSmall_Qabs in H5. setoid_replace ((AQtoQ approx_sum + AQtoQ (app_div v w (Qdlog2 (` e0)))) - (AQtoQ v / AQtoQ w + exact_sum))%Q with (AQtoQ approx_sum - exact_sum + (AQtoQ (app_div v w (Qdlog2 (` e0))) - (AQtoQ v / AQtoQ w)))%Q by ring. apply (Qle_trans _ _ _ (Qabs_triangle _ _)). rewrite <- Pos.add_1_r, Pos2Z.inj_add, inject_Z_plus. rewrite Qmult_plus_distr_r, Qmult_1_r. apply Qplus_le_compat. exact H5. apply AbsSmall_Qabs. change (Qball (` e0) (AQtoQ (app_div v w (Qdlog2 (` e0)))) (AQtoQ v / AQtoQ w)). apply ball_weak_le with (e:= (2 ^ Qdlog2 (` e0))%Q). apply Qdlog2_spec, Qpos_ispos. apply aq_div. 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