proposition: Lemma TM_mul_mixed_correct (a : I.type) M (x0 : R) (X : interval) f (y : R) : a >: y -> i_validTM x0 X M f -> i_validTM x0 X (TM_mul_mixed a M) (fun x => Xmul (Xreal y) (f x)).
proof: Proof. move=> Hy [Hdef Hnai Hzero Hsubs Hmain]. split=>//. move=> x Hx Dx; apply/contains_Xnan. rewrite I.mul_propagate_r //. apply (Hdef x Hx). by case: (f x) Dx. by move=> HX; rewrite I.mul_propagate_r // Hnai. have->: (Xreal 0) = (Xmul (Xreal y) (Xreal 0)) by simpl; congr Xreal; ring. exact: I.mul_correct. have [q H1 H2] := Hmain. exists (PolR.map (Rmult y) q). - apply: Pol.map_correct =>//. by rewrite Rmult_0_r. by move=> *; apply: J.mul_correct. - move=> x Hx. move/(_ x Hx) in H2. rewrite PolR.horner_mul_mixed. case Dx: (f x) => [|fx]. by rewrite I.mul_propagate_r // (Hdef x Hx Dx). rewrite /Xbind2 /proj_val. replace (y * fx - y * q.[x - x0])%R with (y * (fx - q.[x - x0]))%R by ring. rewrite Dx in H2. exact: J.mul_correct. Qed.
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