proposition: Lemma sinStream_zl : -1 <= a <= 1 -> Limit_zero _ sinStream (xH,a) (fun e:Qpos => Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ (proj1_sig e)))))).
proof: Proof. intro Ha. intros [e epos]. rewrite Str_pth_sinStream, Qabs_Qmult, Qabs_Qmult. rewrite Qabs_Qpower. change (Qabs (-1)) with 1. rewrite Qpower_1, Qmult_1_l. rewrite Qmult_comm. apply (Qle_trans _ (1 * Qabs (1 # Pos.of_nat (fact (1+2*(Pos.to_nat (Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ e))))))))))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. - rewrite (Qabs_Qpower a (1 + 2 * Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ ` (e ↾ epos))))))). apply Qpower_le_1. split. apply Qabs_nonneg. apply Qabs_Qle_condition, Ha. - clear Ha a. rewrite Qmult_1_l. unfold Qabs, Z.abs, proj1_sig. 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 (1+2*(Pos.to_nat (Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ e))))))))) # 1)). exact H. apply (Qle_trans _ _ _ (Qceiling_fact_le H)). generalize (Pos.succ (Z.to_pos (Z.log2_up (Qceiling (/ e))))). clear H epos e. intro p. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. 2: apply fact_neq_0. 2: apply fact_neq_0. apply fact_inc_recurse. apply (Nat.le_trans (Pos.to_nat p) (1 + Pos.to_nat p)). apply le_S, Nat.le_refl. apply le_n_S. rewrite <- (Nat.mul_1_l (Pos.to_nat p)) at 1. apply Nat.mul_le_mono_nonneg_r. apply Nat.le_0_l. apply le_S, Nat.le_refl. Qed.
imports: CoRN.algebra.RSetoid 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.CRexp CoRN.reals.fast.CRpi CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.PowerSeries CoRN.transc.SinCos Coq.NArith.Ndigits CoRN.reals.fast.Compress CoRN.reals.fast.PowerBound CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.util.Qdlog Coq(Lia)