proposition: Lemma TM_integral_correct (x0 : Rdefinitions.R) : contains iX0 (Xreal x0) -> i_validTM x0 iX Mf xF -> i_validTM x0 iX TM_integral (fun x => Xreal (RInt f x0 x)).
proof: Proof. move => Hx0X0 [Hdef Hnai ErrMf0 HX0X HPol] /= ; split =>//. rewrite /TM_integral /TM_integral_error /= /iX => H. by rewrite I.mul_propagate_l // I.sub_propagate_l. by apply: (@TM_integral_error_0 _ Hx0X0). case: HPol => [p Hcontains H3]. exists (PolR.primitive tt 0 p). - by apply: Pol.primitive_correct; first exact: J.zero_correct. - move => x hxX. have -> : (PolR.primitive tt 0 p).[x - x0] = RInt (fun t => p.[t - x0]) x0 x. + rewrite RInt_translation_sub. have -> : (PolR.primitive tt 0 p).[x - x0] = (PolR.primitive tt 0 p).[x - x0] - (PolR.primitive tt 0 p).[x0 - x0]. * rewrite Rminus_eq_0. set t0 := (X in (_ = _ - X)). have->: t0 = 0; last by rewrite Rminus_0_r. rewrite /t0 PolR.hornerE PolR.size_primitive big1 // => i _. rewrite PolR.nth_primitive. case: ifP; first by rewrite Rmult_0_l. rewrite /PolR.int_coeff; case: i; first by rewrite Rmult_0_l. by move=> *; rewrite /= Rmult_0_l Rmult_0_r. by rewrite Rpol_integral_0. exact: Rpol_integrable. set i1 := (X in (X - _)). set i2 := (X in (_ - X)). have -> : i1 - i2 = RInt (fun t => f t - p.[t - x0]) x0 x. apply sym_eq. apply is_RInt_unique. apply: is_RInt_minus ; apply RInt_correct. + by apply: f_int. + have {2}-> : x0 = (0 + x0) by ring. have -> : x = (x - x0) + x0 by ring. apply: ex_RInt_translation_sub. exact: Rpol_integrable. rewrite /TM_integral_error {i1 i2}. apply: J.contains_RInt => //. apply: ex_RInt_minus. exact: f_int. exact: pol_int_sub. move => x2 Hx2. apply: H3. apply: contains_connected Hx2. now apply Rmin_case. now apply Rmax_case. 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