proposition: Lemma sin_bound_correct : forall q, -(3 ^ sin_bound q #1) ≤ q ≤ (3 ^ sin_bound q #1).
proof: Proof. intro q. apply AbsSmall_Qabs. unfold sin_bound. destruct (Qlt_le_dec (Qabs q) 1). - apply (Qle_trans _ 1). apply Qlt_le_weak, q0. rewrite Qdlog2_le1; simpl; try easy. apply Qlt_le_weak, q0. - assert (2 ≤ 3%Z) as H by discriminate. pose proof (Qdlog_spec 3 (Qabs q) H q0) as [_ H0]. clear H. unfold additional_operations.pow, stdlib_rationals.Q_pow in H0. assert (0 <= 1 + Qdlog 3 (Qabs q))%Z. { apply semirings.nonneg_plus_compat; [easy | now apply Qdlog_bounded_nonneg]. } rewrite inj_Zabs_nat, Z.abs_eq. apply Qlt_le_weak. rewrite <- Zpower_Qpower in H0. apply H0. exact H. exact H. 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)