proposition: Lemma InfiniteGeometricSum_maxIter_monotone : forall series (err:Qpos), GeometricSeries series -> (InfiniteGeometricSum_maxIter (tl series) err <= InfiniteGeometricSum_maxIter series err)%positive.
proof: Proof. intros series err Gs. unfold InfiniteGeometricSum_maxIter. cut ((Qabs (hd (tl series)) / (proj1_sig err * (1 - a) * (1 - a))) <= (Qabs (hd series) / (proj1_sig err * (1 - a) * (1 - a)))). - generalize (Qabs (hd (tl series)) / (proj1_sig err * (1 - a) * (1 - a))) (Qabs (hd series) / (proj1_sig err * (1 - a) * (1 - a))). intros [na da] [nb db] H. cut (Z.succ (na/Zpos da) <= Z.succ (nb/Zpos db))%Z. generalize (Z.succ (na / Zpos da)) (Z.succ (nb/Zpos db)). intros [|x|x] [|y|y] Hxy; try solve [apply Hxy | apply Qle_refl | elim Hxy; constructor | unfold Qle; simpl; repeat rewrite Pmult_1_r]. apply Pos.le_1_l. discriminate. apply Pos.le_1_l. discriminate. apply Zsucc_le_compat. unfold Qle in H. simpl in H. rewrite <- (Zdiv_mult_cancel_r na (Zpos da) (Zpos db)). 2: discriminate. rewrite <- (Zdiv_mult_cancel_r nb (Zpos db) (Zpos da)). 2: discriminate. rewrite (Zmult_comm (Zpos db) (Zpos da)). apply Z_div_le. reflexivity. exact H. - assert (X:0 < 1 - a). change (0 < 1 + - a). rewrite <- Qlt_minus_iff. assumption. apply Qle_shift_div_l. apply (Qpos_ispos (err * (exist _ _ X) * (exist _ _ X))). unfold Qdiv. rewrite <- Qmult_assoc. rewrite <- (Qmult_comm (proj1_sig err * (1 - a) * (1 - a))). rewrite Qmult_inv_r, Qmult_1_r. destruct Gs as [H _]. eapply Qle_trans. apply H. rewrite <- (Qmult_1_l (Qabs (hd series))) at 2. apply Qmult_le_compat_r. apply Qlt_le_weak, Ha1. apply Qabs_nonneg. apply (Qpos_nonzero (err * (exist _ _ X) * (exist _ _ X))). 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