proposition: Lemma sin_poly_prf : is_UniformlyContinuousFunction (fun x => sin_poly_fun (QboundAbs (1#1) x)) sin_poly_modulus.
proof: Proof. apply (fun a => is_UniformlyContinuousD_Q (Some (-(1))%Q) (Some (1:Q)) eq_refl _ _ DthreeXMinusFourX3 sin_poly_fun a (9#1)). simpl; intros q _ _. apply sin_poly_fun_correct. simpl; intros x' _ [Hx0 Hx1]. set (x:=(inj_Q IR x')) in *. stepr (Nine:IR); [| now (apply eq_symmetric; apply (inj_Q_nring IR 9))]. stepl (ABSIR (Three[-]Twelve[*]x[*]x)); [| now (apply AbsIR_wd; rational)]. apply AbsSmall_imp_AbsIR. split. apply shift_zero_leEq_minus'. rstepr (Twelve[*]((nring 1)[-]x)[*](x[-][--](nring 1))). repeat apply mult_resp_nonneg. apply (nring_nonneg IR 12). apply shift_zero_leEq_minus. stepr (inj_Q IR (nring 1)); [| now apply inj_Q_nring]. assumption. apply shift_zero_leEq_minus. stepl (inj_Q IR (-(1))). assumption. stepr ([--](inj_Q IR 1)). apply inj_Q_inv. apply un_op_wd_unfolded. apply (inj_Q_nring IR 1). rstepr (Nine[-][0]:IR). apply minus_resp_leEq_both. apply nring_leEq. lia. rstepr (Twelve[*]x[^]2). apply mult_resp_nonneg. apply (nring_leEq IR 0 12). lia. apply sqr_nonneg. 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)