proposition: Lemma TM_cos_correct (x0 : R) (X0 X : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (TM_cos X0 X n) (fun x => Xreal (cos x)).
proof: Proof. move=> Hsubset Hex. apply i_validTM_Ztech with (TR.T_cos tt); last 2 first =>//. exact: I.cos_correct. constructor. - by move=> x m; rewrite /TR.T_cos PolR.size_rec2. - move=> x m k Dx Hk; rewrite /TR.T_cos. rewrite /PolR.nth /PolR.rec2; clear - Hk. { move: k Hk; apply: nat_ind2. - by move=> _; rewrite (nth_rec2up_indep _ _ _ _ 0%R (m2 := 0)) //= Rdiv_1. - move=> Hm; rewrite (nth_rec2up_indep _ _ _ _ 0%R (m2 := 1)) //=. by rewrite Rdiv_1; symmetry; apply: is_derive_unique; auto_derive; auto with real. - move=> k Hk0 Hk1 Hm. rewrite (nth_rec2up_indep _ _ _ _ 0%R (m2 := k.+2)) // nth_rec2upSS'. rewrite /TR.cos_rec in Hk0 Hk1 *. set F := (fun (a _ : FullR.T) (n : nat) => - a / (INR n * INR n.-1))%R in Hk0 Hk1 *. have Hkm : k <= m by do 2![apply: ltnW]. move/(_ Hkm) in Hk0. rewrite (nth_rec2up_indep _ _ _ _ 0%R (m2 := k)) // in Hk0. rewrite Hk0 !Derive_nS; clear. rewrite [in RHS](Derive_n_ext _ (fun x => - cos x)); last first. move=> t; change (Derive _ t) with (Derive_n cos 2 t). rewrite (is_derive_n_unique _ _ _ _ (is_derive_n_cos _ _)) /= Rmult_1_r. by rewrite Ropp_mult_distr_l_reverse Rmult_1_l. rewrite Derive_n_opp 2!fact_simpl 2!mult_INR. change (Derive_n (fun x => _)) with (Derive_n cos). simpl (k.+2.-1). change eq with (@eq R); field; split. apply INR_fact_neq_0. split ; exact: not_0_INR. } constructor. - by move=> x m k; rewrite /TR.T_cos Pol.size_rec2 PolR.size_rec2. - by move=> Y x m Hx; apply: Pol.rec2_correct; first move=> ai bi a b l Ha Hb; repeat first [apply: J.div_correct| apply: J.neg_correct| apply: J.mul_correct| apply: R_from_nat_correct| apply: J.sin_correct| apply: J.cos_correct]. - done. - move=> *; apply/ex_derive_n_is_derive_n/is_derive_n_cos. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound