proposition: Lemma cos_poly_prf : @is_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace (fun x => cos_poly_fun (QboundAbs (1#1) x)) cos_poly_modulus.
proof: Proof. apply (fun a => is_UniformlyContinuousD_Q (Some (-(1))%Q) (Some (1:Q)) eq_refl _ _ DoneMinusX2 cos_poly_fun a (4#1)). simpl; intros q _ _. apply cos_poly_fun_correct. simpl; intros x' _ [Hx0 Hx1]. set (x:=(inj_Q IR x')) in *. stepr (Four:IR); [| now (apply eq_symmetric; apply (inj_Q_nring IR 4))]. stepl (ABSIR ([--](Four[*]x))); [| now (apply AbsIR_wd; rational)]. stepl (ABSIR (Four[*]x)); [| now apply AbsIR_inv]. rstepr (Four[*][1]:IR). apply AbsSmall_imp_AbsIR. apply mult_resp_AbsSmall. apply nring_nonneg. split. stepl ([--](pring IR 1)[/][0][+][1][//]den_is_nonzero IR (-1#1)). assumption. unfold pring; simpl; rational. stepr (pring IR 1[/][0][+][1][//]den_is_nonzero IR 1). assumption. unfold pring; simpl; rational. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRsin CoRN.reals.fast.CRpi CoRN.reals.fast.CRIR CoRN.reals.fast.Compress Coq.QArith.Qpower CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.SinCos CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra