proposition: Lemma Isign_large_Xabs (u : U) (tf : T) (Y X : I.type) f : approximates Y tf f -> match I.sign_large (eval u tf Y X) with | Xeq => forall x, contains (I.convert X) (Xreal x) -> f x = Xabs (f x) | Xgt => forall x, contains (I.convert X) (Xreal x) -> f x = Xabs (f x) | Xlt => forall x, contains (I.convert X) (Xreal x) -> Xneg (f x) = Xabs (f x) | Xund => True end.
proof: Proof. intros Hmain. case: I.sign_large (I.sign_large_correct (eval u tf Y X)) =>//. - move=> H x Hx. rewrite (H (f x)) /= ?Rabs_R0 //. exact: eval_correct Hx. - move=> H x Hx. set fx := f x. have [|Hfx Hsign] := H fx. exact: eval_correct Hx. rewrite /Xabs Hfx /=; congr Xreal. by rewrite Rabs_left1. move=> H x Hx. set fx := f x. have [|Hfx Hsign] := H fx. exact: eval_correct Hx. rewrite /Xabs Hfx /=; congr Xreal. by rewrite Rabs_right; auto with real. 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