proposition: Theorem i_validTM_Ztech (x0 : R) (X0 : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (RPA (IP X0 n) (Ztech IP (IP X0 n) F X0 X n)) xf.
proof: Proof. move=> Hsubs Hx0. have H0 : X >: x0 by exact: Hsubs. case E1 : (isNNegOrNPos (Pol.nth (IP X n.+1) n.+1)); last first. rewrite /Ztech E1 /=. exact: i_validTM_TLrem. case E2 : (I.bounded X); last first. rewrite /Ztech E2 andbC /=. exact: i_validTM_TLrem. set err := Ztech IP (IP X0 n) F X0 X n. have Hdef : forall r : R, X >: r -> xf r <> Xnan. move=> r Hr Kr. have Knai := @IPoly_nai validIPoly_ X r Hr Kr n.+1 n.+1 (leqnn _). by rewrite isNNegOrNPos_false in E1. split=>//. - by move=> x Hx /(Hdef x Hx). - have /I.bounded_correct [E1l E1u] := E2. rewrite (proj2 (I.lower_bounded_correct _ _)) =>//. exists x0; exact: Hsubs. - rewrite /= /err /Ztech E1 E2 /=. apply: I.join_correct; right. have E0 : xf x0 = Xreal (PolR.nth (P x0 n) 0). rewrite Poly_nth0 // /f0. by case: (xf x0) (Hdef x0 H0). pose r'0 := PolR.nth (P x0 n) 0. have->: Xreal 0 = Xsub (xf x0) (Xreal r'0) by rewrite E0 /= Rminus_diag_eq. apply: I.sub_correct. exact: F_contains Hx0. exact: IPoly_nth. clear Hdef. exists (P x0 n); first by move=> k; apply: IPoly_nth. pose Rdelta0 := Rdelta n x0. move=> x Hx. rewrite /err /Ztech E1 E2 /=. set Delta := I.join (I.join _ _) _; rewrite -/(Rdelta n x0 x) -/(Rdelta0 x). have [Hbl Hbu] := I.bounded_correct _ E2. have [Hcl _] := I.lower_bounded_correct _ Hbl. have [Hcu _] := I.upper_bounded_correct _ Hbu. set (l := (proj_val (I.F.convert (I.lower X)))) in Hcl. set (u := (proj_val (I.F.convert (I.upper X)))) in Hcu. have HX: I.convert X = Ibnd (Xreal l) (Xreal u). rewrite -Hcl -Hcu. apply I.lower_bounded_correct =>//. exists x0; exact: Hsubs. have {Hcl Hbl} Hlower : Delta >: Rdelta0 l. apply: I.join_correct; left; apply: I.join_correct; left. have Hlower : contains (I.convert (I.bnd (I.lower X) (I.lower X))) (Xreal l). rewrite I.bnd_correct; first last. - apply: I.valid_ub_real. by rewrite Hcl. - apply: I.valid_lb_real. by rewrite Hcl. - rewrite Hcl; split; apply Rle_refl. apply: J.sub_correct. - exact: F_Rcontains. - apply: Pol.horner_correct. exact: IPoly_nth. exact: J.sub_correct. have {Hcu Hbu} Hupper : Delta >: Rdelta0 u. apply: I.join_correct; left; apply: I.join_correct; right. have Hupper : contains (I.convert (I.bnd (I.upper X) (I.upper X))) (Xreal u). rewrite I.bnd_correct; first last. - apply: I.valid_ub_real. by rewrite Hcu. - apply: I.valid_lb_real. by rewrite Hcu. - rewrite Hcu; split; apply Rle_refl. apply: J.sub_correct. - exact: F_Rcontains. - apply: Pol.horner_correct. exact: IPoly_nth. exact: J.sub_correct. have H'x0 : X >: x0 by exact: Hsubs. have HX0 : Delta >: Rdelta0 x0. apply: I.join_correct; right. apply: J.sub_correct; first exact: F_Rcontains. rewrite Rminus_diag_eq //. suff->: ((P x0 n).[0%R]) = PolR.nth (P x0 n) 0 by apply: IPoly_nth. rewrite PolR.hornerE Poly_size big_nat_recl // pow_O Rmult_1_r. rewrite big1 ?(Rplus_0_r, Rmult_1_r) //. move=> i _. by rewrite /= Rmult_0_l Rmult_0_r. clearbody Delta l u. rewrite -> HX in Hx, H'x0. have [||Hlow|Hup] := @intvl_lVu l u x0 x => //. have [|||H1|H2] := @Rmonot_contains _ (@intvl_connected l x0) Rdelta0 _ _ _ _ _ _ Hlow. + have [|||||H _] := @Zumkeller_monot_rem _ (contains_connected (I.convert X)) _ _ _ x0 n => //. apply Poly_size. apply Poly_nth. exact: Ztech_derive_sign. case: H => H ; [left|right] ; intros p q Hp Hq Hpq ; apply H => // ; rewrite HX ; split ; try apply: intvl_connected (intvl_l H'x0) (H'x0) _ _ => // ; try apply Hp ; try apply Hq. exact: intvl_l Hlow. exact: intvl_u Hlow. + exact: contains_connected H1. + exact: contains_connected H2. have [|||H1|H2] := @Rmonot_contains _ (@intvl_connected x0 u) Rdelta0 _ _ _ _ _ _ Hup. + have [|||||_ H] := @Zumkeller_monot_rem _ (contains_connected (I.convert X)) _ _ _ x0 n => //. apply Poly_size. apply Poly_nth. exact: Ztech_derive_sign. case: H => H ; [left|right] ; intros p q Hp Hq Hpq ; apply H => // ; rewrite HX ; split ; try apply: intvl_connected (H'x0) (intvl_u H'x0) _ _ => // ; try apply Hp ; try apply Hq. exact: intvl_l Hup. exact: intvl_u Hup. + exact: contains_connected H1. + exact: contains_connected H2. 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