proposition: Lemma TM_exp_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_exp X0 X n) (fun x => Xreal (exp x)).
proof: Proof. move=> Hsubset Hex. apply i_validTM_Ztech with (TR.T_exp tt); last 2 first =>//. exact: I.exp_correct. constructor. - by move=> *; rewrite PolR.size_rec1. - { move=> {X0 n Hsubset Hex} x n k Hx Hk; rewrite /PolR.nth. elim: k Hk => [|k IHk] Hk. - by rewrite (nth_rec1up_indep _ _ _ 0%R (m2 := 0)) //= Rdiv_1. rewrite (nth_rec1up_indep _ _ _ 0%R (m2 := k)) // in IHk; last exact: ltnW. rewrite (nth_rec1up_indep _ _ _ 0%R (m2 := k.+1)) // nth_rec1upS. rewrite {}IHk /TR.exp_rec; last exact: ltnW. rewrite !(is_derive_n_unique _ _ _ _ (is_derive_n_exp _ _)). rewrite fact_simpl mult_INR. change eq with (@eq R); field; split. apply INR_fact_neq_0. now apply not_0_INR. } constructor. - by move=> *; rewrite PolR.size_rec1 Pol.size_rec1. - { move => {X0 X n Hsubset Hex} X0 xi0 n Hx. apply: Pol.rec1_correct =>//. by move=> *; repeat first [apply: J.div_correct |apply: R_from_nat_correct ]. exact: J.exp_correct. } - done. - move=> {n} n x Hx; eapply ex_derive_n_is_derive_n; exact: is_derive_n_exp. 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