proposition: Lemma TM_comp_correct (x0 : R) (X0 X : I.type) (TMg : TM_type) (Mf : rpa) g f : contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) Mf f -> (forall y0 Y0 Y k, subset' (I.convert Y0) (I.convert Y) -> contains (I.convert Y0) (Xreal y0) -> i_validTM y0 (I.convert Y) (TMg Y0 Y k) g) -> forall n, i_validTM x0 (I.convert X) (TM_comp TMg Mf X0 X n) (fun xr => Xbind g (f xr)).
proof: Proof. move=> Hne Hf Hg n; rewrite /TM_comp. set A0 := Pol.nth (approx Mf) 0. set a0 := J.midpoint A0. set Bf := Bnd.ComputeBound prec (approx Mf) (I.sub prec X X0). set BfMf := I.add prec Bf (error Mf). set Mg := TMg a0 (I.add prec Bf (error Mf)) n. set M1 := TMset0 Mf (I.sub prec A0 a0). set M0 := TM_horner n (approx Mg) M1 X0 X. have [Fdef Fnai Fzero Hsubs Fmain] := Hf. have ne_A0 : not_empty (I.convert A0). have [q hq1 hq2] := Fmain. by eexists; eapply hq1. pose alpha0 := proj_val (I.F.convert (I.midpoint A0)). have in_a0 : a0 >: alpha0. exact: J.contains_midpoint. have subs_a0 : subset' (I.convert a0) (I.convert BfMf). rewrite /a0 /BfMf. move=> [|v] Hv. apply/contains_Xnan; rewrite I.add_propagate_r //. rewrite /A0 in Hv. apply/contains_Xnan. rewrite J.midpoint_correct in Hv. easy. have [Q HQ1 _] := Fmain. move/(_ 0) in HQ1. by exists (PolR.nth Q O). rewrite /Bf. step_xr (Xadd (Xreal v) (Xreal 0)); last by rewrite Xadd_0_r. apply: I.add_correct =>//. have [qf hq1 hq2] := Fmain. apply: (@ComputeBound_nth0 _ _ qf) =>//. rewrite <- (Rminus_eq_0 x0). now apply J.sub_correct. exact: J.subset_midpoint. have [Gdef Gnai Gzero Gsubs Gmain] := Hg alpha0 a0 BfMf n subs_a0 in_a0. have inBfMf : forall x : R, X >: x -> contains (I.convert BfMf) (f x). move=> x Hx; rewrite /BfMf /Bf. have [qf hq1 hq2] := Fmain. move/(_ x Hx) in hq2. step_xr (Xreal (qf.[x - x0]) + (f x - Xreal (qf.[x - x0])))%XR =>//. apply: I.add_correct. apply: Bnd.ComputeBound_correct =>//. exact: J.sub_correct. case Df: (f x) => [|fx]. by rewrite (Fdef x Hx Df). by rewrite Df in hq2. case: (f) =>// r; simpl; congr Xreal; ring. have HM1 : i_validTM x0 (I.convert X) M1 (fun x => f x - Xreal (alpha0)). exact: TMset0_correct. split=>//=. - move=> x Hx Dx. rewrite I.add_propagate_r //. case Efx: (f x) => [|r]. rewrite Gnai // /Bf. rewrite I.add_propagate_r //. exact: Fdef Efx. rewrite Efx in Dx. apply: Gdef Dx. rewrite -Efx. exact: inBfMf. - move=> HX; rewrite I.add_propagate_r // Gnai //. by rewrite I.add_propagate_r // Fnai. rewrite /M0 /Mg /Bf. step_xr (Xreal 0 + Xreal 0)%XR; last by rewrite /= Rplus_0_l. have [Q HQ1 HQ2] := Gmain. have [F HF1 HF2] := Fmain. apply: I.add_correct =>//. apply (@TM_horner_correct x0 X0 X M1 _ (approx Mg) Q n Hne HM1 HQ1). have HMg : i_validTM alpha0 (I.convert BfMf) Mg g by exact: Hg. have [M1def M1nai M1zero M1subs M1main] := HM1. have [Ga0 HGa0 HGa0'] := Gmain. pose f0 := (fun x => f x - Xreal alpha0). have HM0 : i_validTM x0 (I.convert X) M0 (fun r => Xreal Ga0.[proj_val (f0 r)]). exact: TM_horner_correct. have [M0def M0nai M0zero M0subs M0main] := HM0. have [Q0 HQ0 HQ0'] := M0main. exists Q0 =>//. move=> x Hx. case Enai: (I.convert (I.add prec (error M0) (error Mg))) => [|el eu] //. rewrite -Enai. case Efx: (f x) => [|fx]. rewrite I.add_propagate_r //. apply/Gnai/contains_Xnan. rewrite -Efx; exact: inBfMf. rewrite /Xbind. case Egfx: (g fx) => [|gfx]. rewrite I.add_propagate_r //. apply: Gdef Egfx. rewrite -Efx; exact: inBfMf. pose intermed := Ga0.[proj_val (f0 x)]. rewrite /proj_val. replace (gfx - Q0.[x - x0])%R with (intermed - Q0.[x - x0] + (gfx - intermed))%R by ring. apply: J.add_correct. exact: HQ0'. rewrite /intermed /f0 Efx /=. rewrite -[gfx](f_equal proj_val Egfx). apply: HGa0'. rewrite -Efx. exact: inBfMf. 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