proposition: Theorem i_validTM_TLrem (x0 : R) (X0 : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (RPA (IP X0 n) (TLrem IP X0 X n)) xf.
proof: Proof. move=> Hsubs Hx0. pose err := TLrem IP X0 X n. have H0 : X >: x0 by exact: Hsubs. split=>//=. move=> x Hx Nx. rewrite /TLrem. apply I.mul_propagate_l. exact: (IPoly_nai Hx Nx). move=> HX; rewrite /TLrem. by rewrite I.mul_propagate_r // J.power_int_propagate // I.sub_propagate_l. set V := (I.power_int prec (I.sub prec X X0) (Z_of_nat n.+1)). apply (mul_0_contains_0_r _ (y := Xreal (PolR.nth (P x0 n.+1) n.+1))). apply: IPoly_nth =>//. apply: pow_contains_0 =>//. exact: subset_sub_contains_0 Hx0 Hsubs. exists (P x0 n); first by apply: IPoly_nth. move=> x Hx. rewrite PolR.hornerE Poly_size //. have Hbig : \big[Rplus/R0]_(0 <= i < n.+1) (PolR.nth (P x0 n) i * (x - x0) ^ i)%R = \big[Rplus/R0]_(0 <= i < n.+1) (Dn i x0 / INR (fact i) * (x - x0)^i)%R. by apply: eq_big_nat => i Hi; rewrite Poly_nth. rewrite Hbig. have Hder' : forall n r, X >: r -> ex_derive_n f0 n r. move=> m r Hr. exact: Hder_n. have [c [Hcin [Hc Hc']]] := (@ITaylor_Lagrange xf _ (contains_connected (I.convert X)) n Hder' x0 x H0 Hx). rewrite Hc /TLrem. apply: J.mul_correct=>//. rewrite -(@Poly_nth _ c n.+1 n.+1) //; exact: IPoly_nth. rewrite pow_powerRZ. apply: J.power_int_correct. exact: J.sub_correct. 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