proposition: Theorem TM_any_correct (x0 : R) (Y X : I.type) (n : nat) (f : R -> ExtendedR) : contains (I.convert X) (Xreal x0) -> (forall x : R, contains (I.convert X) (Xreal x) -> contains (I.convert Y) (f x)) -> i_validTM x0 (I.convert X) (TM_any Y X n) f.
proof: Proof. move=> H0 Hf. have Hrr := Hf _ H0. set r := proj_val (f x0). have Hr : contains (I.convert Y) (Xreal r). exact: contains_Xreal. set (m := proj_val (I.F.convert (I.midpoint Y))). assert (Hm': contains (I.convert (J.midpoint Y)) (Xreal m)). apply J.contains_midpoint. now exists r. split=>//. move=> /= x Hx Nx. rewrite /TM_any /= in Nx. apply I.mask_propagate_l, I.sub_propagate_l, contains_Xnan. rewrite -Nx. exact: Hf. apply I.mask_propagate_r. apply I.mask_correct'. apply: subset_sub_contains_0 Hm' _. apply J.subset_midpoint. now exists r. set pol0 := PolR.polyC m. set pol' := if n == 0 then pol0 else PolR.set_nth pol0 n 0%R. exists pol'. rewrite /pol' {pol'} /pol0 /TM_any /=. + case: ifP => H. exact: Pol.polyC_correct. apply: Pol.set_nth_correct. exact: Pol.polyC_correct. exact: J.zero_correct. + move=> x Hx /=. apply I.mask_correct', J.sub_correct. now apply contains_Xreal, Hf. rewrite /pol' /pol0; case: ifP => H. by rewrite PolR.horner_polyC. rewrite PolR.hornerE !sizes maxnSS maxn0. step_r (pol0.[x - x0])%R. by rewrite PolR.horner_polyC. rewrite /pol0 (@PolR.hornerE_wide n.+1) ?sizes //. apply: eq_bigr => i _. congr Rmult. rewrite PolR.polyCE !(PolR.nth_polyCons, PolR.nth_set_nth). case: i => [//|i]; first by rewrite eq_sym H. by rewrite PolR.nth_polyNil if_same. 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