proposition: Theorem abs_correct u (Y : I.type) tf f : approximates Y tf f -> approximates Y (abs u Y tf) (fun x => Xabs (f x)).
proof: Proof. move=> Hf. rewrite /abs. case: I.sign_large (@Isign_large_Xabs u tf Y Y f Hf) => Habs; case: tf Hf => [cf| |tf] Hmain //. - move=> Hne. case: (Hmain Hne) => [Hf|Hf]. now left. right. apply: is_const_ext Hf. intros x Hx. now apply Habs. - byp' Habs Hmain. - move=> Hne; apply: (@TM_fun_eq f). byp Habs Hf. exact: Hmain. - move=> Hne; destruct (Hmain Hne) as [Hf|[y Hy1 Hy2]]. left. now apply J.neg_propagate. right. exists (Xneg y). exact: I.neg_correct. move => /= x Hx. by rewrite -Habs // Hy2. - red=> Hne. apply (TM_fun_eq Habs). apply: TM_opp_correct. apply: TM_var_correct_strong =>//. exact: J.subset_midpoint. exact: J.contains_midpoint. exact: Hmain Hne. - red=> Hne. apply (TM_fun_eq Habs). apply: TM_opp_correct. exact: Hmain. - move=> Hne; destruct (Hmain Hne) as [Hf|[y Hy1 Hy2]]. now left. right. exists y => //= x Hx. by rewrite -Habs // Hy2. - byp' Habs Hmain. - move=> Hne; move: (Hmain Hne); apply: TM_fun_eq; byp Habs Hmain. - foo. - foo. - foo. 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