fact: Definition eval_RInt_init prec deg hyps pf pu pv cf cu cv := let fi := let bounds := hyps ++ map (T.eval_bnd prec) cf in fun b => nth 0 (A.BndValuator.eval prec pf (b :: bounds)) I.nai in let ui := let bounds := hyps ++ map (T.eval_bnd prec) cu in nth 0 (A.BndValuator.eval prec pu bounds) I.nai in let vi := let bounds := hyps ++ map (T.eval_bnd prec) cv in nth 0 (A.BndValuator.eval prec pv bounds) I.nai in let cb := fun x => match x with IR.IBu => ui | IR.IBv => vi | IR.IBp x => I.singleton x end in let mid := fun u v => let u := cb u in let v := cb v in I.midpoint (I.join u v) in let Fi := let bounds := hyps ++ map (T.eval_bnd prec) cf in let bounds := map A.TaylorValuator.TM.const bounds in fun u v => let u := cb u in let v := cb v in let xi := I.join u v in let gi := A.TaylorValuator.TM.get_tm (prec, deg) xi (nth 0 (A.TaylorValuator.eval prec deg xi pf (A.TaylorValuator.TM.var :: bounds)) A.TaylorValuator.TM.dummy) in IT.taylor_integral_naive_intersection prec fi gi xi u v in (mid, Fi).
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Coquelicot(Coquelicot) Stdlib Coquelicot Xreal Basic Sig Interval Integral Eval Bertrand Tree Prog Reify Refine Interval_helper