proposition: Lemma expStream_zl : -1 <= a <= 0 -> Limit_zero _ expStream (xH,1) (fun e:Qpos => Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ (proj1_sig e)))))).
proof: Proof. intros aneg [e epos]; unfold proj1_sig. rewrite Str_pth_expStream. rewrite Qabs_Qmult, Qmult_comm. apply (Qle_trans _ (1 * Qabs (1 # Pos.of_nat (fact (Pos.to_nat (Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ e)))))))))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. - generalize (Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ e))))). intro p. rewrite Qabs_Qpower. apply Qpower_le_1. split. apply Qabs_nonneg. apply Qabs_Qle_condition. split. apply aneg. apply (Qle_trans _ 0). apply aneg. discriminate. - rewrite Qmult_1_l. clear aneg a. simpl. rewrite <- (Qinv_involutive e) at 2. assert (0 < /e) as H. { apply Qinv_lt_0_compat, epos. } apply (@Qinv_le_compat (/e) ((Pos.of_nat (fact (Pos.to_nat (Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ e)))))))) # 1)). exact H. apply Qceiling_fact_le, H. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra