proposition: Lemma fun_gen_correct (fi : I.precision -> I.type -> I.type) (ftm : I.precision -> TM_type) (fx : R -> ExtendedR) (ft := fun_gen fi ftm) : (forall prec : I.precision, I.extension (Xbind fx) (fi prec)) -> (forall prec X0 X n, tmsize (ftm prec X0 X n) = n.+1) -> (forall prec x0 X0 X n, subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (ftm prec X0 X n) fx) -> forall (u : U) (X : I.type) (tf : T) (f : R -> ExtendedR), approximates X tf f -> approximates X (ft u X tf) (fun x => Xbind fx (f x)).
proof: Proof. move=> Hext Hsiz Hvalid u X [c| |tm] f Hmain Hne. - destruct (Hmain Hne) as [Hf|[y Hy1 Hy2]]. left. { apply contains_Xnan. apply (Hext u.1 c (Xbind fx Xnan)). now apply contains_Xnan. } right. exists (Xbind fx y); first exact: Hext. by move=> x Hx; rewrite /= Hy2. - apply: (@TM_fun_eq fx). by move=> *; rewrite Hmain. apply: Hvalid. exact: J.subset_midpoint. exact: J.contains_midpoint. - move/(_ Hne) in Hmain. have [Hdef Hnai Hzero Hsubset Htm] := Hmain. apply (TM_comp_correct u.1) =>//. exact: J.contains_midpoint. move=> *; exact: Hvalid. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig