proposition: Lemma Taylor_Series_conv_lemma1 : forall t x y Hxy (e : IR) (He : [0] [<] e), {N : nat | forall n : nat, N <= n -> forall w z : IR, compact x y Hxy z -> Compact (Min_leEq_Max' x y t) w -> forall Hw Hz, AbsIR (((Part _ _ (Derivative_n_imp_inc' _ _ _ _ _ (derF (S n)) w Hw) [/] _[//] nring_fac_ap_zero _ (S n)) {**} ((FId{-} [-C-]w) {^}n{*} (FId{-} [-C-]a))) z Hz) [<=] (e[/] _[//]H1 (S n))}.
proof: Proof. intros. set (r := Max y (Max a t) [-]Min x (Min a t)) in *. cut (Min x (Min a t) [<=] Max y (Max a t)). intro Hxy'; cut (included (Compact (Min_leEq_Max' x y t)) (Compact Hxy')). intro Hinc'. cut (forall w z : IR, Compact Hxy z -> Compact Hxy' w -> AbsIR (z[+][--]w) [<=] r). intro. 2: intros w z H0 H2; fold (z[-]w) in |- *; unfold r in |- *. set (r' := Two[*]Max r [1]) in *. set (H' := Taylor_Series_lemma_cont r') in *. elim (bndf r' H' _ _ (Min_leEq_Max' x y t) (included_interval' realline _ _ _ _ I I I I _) e He); intros N HN. exists N. intros n H2 w z H3 H4 Hw Hz. simpl in |- *; fold (Two:IR) in |- *. assert (H5 : forall n : nat, [0] [<] r'[^]n). intro; unfold r' in |- *; apply nexp_resp_pos; unfold r' in |- *; apply mult_resp_pos; [ apply pos_two | apply pos_max_one ]. apply leEq_transitive with ((e[/] _[//]pos_ap_zero _ _ (H5 (S n))) [*] AbsIR ((z[+][--]w) [^]n[*] (z[+][--]a))). eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. apply shift_leEq_div. auto. clear Hz H3 z. eapply leEq_transitive. 2: apply (HN (S n) (le_S _ _ H2) w H4). simpl in |- *. cut (forall z : IR, AbsIR z [=] AbsIR (z[-][0])); intros. 2: apply AbsIR_wd; algebra. eapply leEq_wdr. 2: apply H3. clear H3; eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_mult_pos'. eapply leEq_wdr. 2: apply mult_commutes. cut (forall z : IR, AbsIR (z[/] _[//]nring_fac_ap_zero _ (S n)) [*]r'[^]S n [=] AbsIR z[*] (r'[^]S n[/] _[//]nring_fac_ap_zero _ (S n))); intros. eapply leEq_wdr. 2: apply H3. clear H3; apply mult_resp_leEq_rht. apply eq_imp_leEq; apply AbsIR_wd; algebra. apply less_leEq; auto. rstepr ((AbsIR z[/] _[//]nring_fac_ap_zero _ (S n)) [*]r'[^]S n). apply mult_wdl. eapply eq_transitive_unfolded. apply AbsIR_division with (y__ := AbsIR_resp_ap_zero _ (nring_fac_ap_zero _ (S n))). apply div_wd. algebra. apply AbsIR_eq_x. apply nring_nonneg. apply less_leEq; apply div_resp_pos; [ apply pos_nring_fac | auto ]. Transparent nexp_op. apply shift_leEq_div. apply nexp_resp_pos; apply pos_two. unfold r' in |- *. apply leEq_wdl with (e[*] (AbsIR ((z[+][--]w) [^]n[*] (z[+][--]a)) [/] _[//] nexp_resp_ap_zero (S n) (max_one_ap_zero r))). astepr (e[*][1]). apply mult_resp_leEq_lft. 2: apply less_leEq; auto. apply shift_div_leEq. apply nexp_resp_pos; apply pos_max_one. astepr (Max r [1][^]S n). eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. astepr (Max r [1][^]n[*]Max r [1]). apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_nexp_op. apply nexp_resp_leEq. apply AbsIR_nonneg. apply leEq_transitive with r; auto. apply lft_leEq_Max. apply leEq_transitive with r. apply H0; auto. split. eapply leEq_transitive. apply Min_leEq_rht. apply Min_leEq_lft. eapply leEq_transitive. 2: apply rht_leEq_Max. apply lft_leEq_Max. apply lft_leEq_Max. rstepl ((e[/] _[//] mult_resp_ap_zero _ _ _ (nexp_resp_ap_zero (S n) (max_one_ap_zero r)) (H1 (S n))) [*]AbsIR ((z[+][--]w) [^]n[*] (z[+][--]a)) [*] Two[^]S n). repeat apply mult_wdl. apply div_wd; algebra. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply mult_nexp. algebra. apply leEq_wdr with (AbsIR (Max y (Max a t) [-]Min x (Min a t))). apply compact_elements with Hxy'; auto. inversion_clear H0; split. apply leEq_transitive with x; auto; apply Min_leEq_lft. apply leEq_transitive with y; auto; apply lft_leEq_Max. apply AbsIR_eq_x. apply shift_leEq_minus; astepl (Min x (Min a t)); auto. red in |- *; intros z Hz. inversion_clear Hz; split. eapply leEq_transitive. 2: apply H0. apply leEq_Min. apply Min_leEq_lft. eapply leEq_transitive; apply Min_leEq_rht. eapply leEq_transitive. apply H2. apply Max_leEq. apply lft_leEq_Max. eapply leEq_transitive. 2: apply rht_leEq_Max. apply rht_leEq_Max. apply leEq_transitive with t. eapply leEq_transitive; apply Min_leEq_rht. eapply leEq_transitive. 2: apply rht_leEq_Max. apply rht_leEq_Max. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor