proposition: Lemma InfiniteGeometricSum_maxIter_correct : forall series (err:Qpos), GeometricSeries series -> err_prop (proj1_sig err) (Str_nth_tl (nat_of_P (InfiniteGeometricSum_maxIter series err)) series) = true.
proof: Proof. intros series err H. rewrite -> err_prop_prop. unfold err_bound. assert (X:0 < 1 - a). change (0 < 1 + - a). rewrite <- Qlt_minus_iff. assumption. apply Qle_shift_div_r; try assumption. assert (Y:(Qabs (hd series) * a ^ Zpos (InfiniteGeometricSum_maxIter series err) <= proj1_sig err * (1 - a))). { destruct (Qlt_le_dec 0 (Qabs (hd series))). apply Qmult_lt_0_le_reg_r with (/Qabs (hd series)). apply Qinv_lt_0_compat; assumption. rewrite (Qmult_comm (Qabs (hd series))), <- Qmult_assoc. rewrite Qmult_inv_r, Qmult_1_r. 2: auto with *. cut (a ^ Zpos (InfiniteGeometricSum_maxIter series err) <= proj1_sig (err * exist _ _ X * Qpos_inv (exist _ _ q))%Qpos). autorewrite with QposElim; auto. apply GeometricCovergenceLemma. autorewrite with QposElim. unfold InfiniteGeometricSum_maxIter. simpl (/ (proj1_sig (err * exist (Qlt 0) (1 - a) X * Qpos_inv (exist (Qlt 0) (Qabs (hd series)) q))%Qpos * (1 - a))). setoid_replace (/ (proj1_sig err * (1 - a) * / Qabs (hd series) * (1 - a))) with (Qabs (hd series) / (proj1_sig err * (1 - a) * (1 - a))) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field). 2: repeat split;auto with *;apply Qpos_nonzero. cut (0 < (Qabs (hd series) / (proj1_sig err * (1 - a) * (1 - a)))). generalize (Qabs (hd series) / (proj1_sig err * (1 - a) * (1 - a))). intros [n d] Hnd. apply Qle_trans with (inject_Z (Z.succ (n/Zpos d))). unfold Qle. simpl. unfold Z.succ. apply Zle_0_minus_le. replace ((n / Zpos d + 1) * Zpos d - n * 1)%Z with (Zpos d*(n/Zpos d) + n mod (Zpos d) - n mod (Zpos d) - n + Zpos d)%Z by ring. rewrite <- Z_div_mod_eq_full. replace (n - n mod (Zpos d) - n + Zpos d)%Z with (Zpos d - n mod (Zpos d))%Z by ring. apply Zle_minus_le_0. destruct (Z_mod_lt n (Zpos d)); auto with *. generalize (Z.succ (n/Zpos d)). intros [|z|z]. discriminate. apply Qle_refl. discriminate. cut (0 < proj1_sig ((exist _ _ q) * Qpos_inv(err * (exist _ _ X)*(exist _ _ X)))%Qpos). simpl; auto. apply Q.Qmult_lt_0_compat; auto with *. setoid_replace (Qabs (hd series)) with 0. rewrite Qmult_0_l. apply (Qpos_nonneg (err * (exist _ _ X))). apply Qle_antisym; try assumption. apply Qabs_nonneg. } apply Qle_trans with (Qabs (hd series)*a^Zpos (InfiniteGeometricSum_maxIter series err)); try assumption. clear Y. generalize (InfiniteGeometricSum_maxIter series err). intros p. revert series H. induction p using Pind; intros series H. simpl. destruct H. rewrite -> Qmult_comm. assumption. rewrite nat_of_P_succ_morphism. rewrite Zpos_succ_morphism. unfold Z.succ. rewrite -> Qpower_plus';[|discriminate]. rewrite Qmult_assoc. apply Qle_trans with (Qabs (hd (Str_nth_tl (nat_of_P p) series))*a). change (S (nat_of_P p)) with (1+(nat_of_P p))%nat. rewrite <- Str_nth_tl_plus. cut (GeometricSeries (Str_nth_tl (nat_of_P p) series)). generalize (Str_nth_tl (nat_of_P p) series). intros s [H0 _]. rewrite -> Qmult_comm. assumption. clear -H. induction (nat_of_P p). auto. change (S n) with (1+n)%nat. rewrite <- Str_nth_tl_plus. simpl. destruct IHn; assumption. apply Qmult_le_compat_r; try assumption. apply IHp; assumption. 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