fact: Definition Ztech (P : Pol.T) F (X0 X : I.type) n := let N := S n in let NthCoeff := Pol.nth (Tcoeffs X N) N in if isNNegOrNPos NthCoeff && I.bounded X then let a := I.lower X in let b := I.upper X in let A := I.bnd a a in let B := I.bnd b b in let Da := I.sub prec (F A) (Pol.horner prec P (I.sub prec A X0)) in let Db := I.sub prec (F B) (Pol.horner prec P (I.sub prec B X0)) in let Dx0 := I.sub prec (F X0) (Pol.nth P 0) in I.join (I.join Da Db) Dx0 else let NthPower := I.power_int prec (I.sub prec X X0) (Z_of_nat N) in I.mul prec NthCoeff NthPower.
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