proposition: Theorem Taylor' : forall n Hf Hf' e, [0] [<] e -> {c : IR | Compact (Min_leEq_Max a b) c | forall Hc, AbsIR (Taylor_Rem n Hf'[-]deriv_Sn b n Hf c Hc[*] (b[-]a)) [<=] e}.
proof: Proof. intros. rename X into H. cut (Dom (deriv_Sn b n Hf) a). intro H0. 2: repeat split. 2: simpl in |- *; auto. elim (less_cotransitive_unfolded _ _ _ H (AbsIR (Taylor_Rem n Hf'[-]Part _ _ H0[*] (b[-]a)))). intros. cut (a [#] b). intro H1. clear a0 H0. cut (Diffble_I_n (ap_imp_Min_less_Max _ _ H1) (S n) F). intro H0. 2: apply included_imp_Diffble_n with I pI; auto. cut (Diffble_I_n (ap_imp_Min_less_Max _ _ H1) n F). intro H2. 2: apply le_imp_Diffble_I with (S n); auto. elim (Taylor_lemma a b H1 F (Diffble_n_imp_inc _ _ _ _ Hf b Hb) e H n H2 H0). intros c H3 H4. exists c; auto. intro. cut (Dom (n_deriv_I _ _ _ _ _ H0{*} [-C-] ([1][/] _[//]nring_fac_ap_zero _ n) {*} ( [-C-]b{-}FId) {^}n) c). intro H5. 2: repeat split. 2: apply n_deriv_inc; auto. eapply leEq_wdl. apply (H4 H5). unfold Taylor_rem, Taylor_Rem in |- *. apply AbsIR_wd; repeat apply cg_minus_wd. algebra. simpl in |- *. repeat first [ apply bin_op_wd_unfolded | apply mult_wd | apply div_wd | apply eq_reflexive_unfolded ]. apply FSumx_wd; intros; simpl in |- *. apply mult_wdl. apply div_wd. 2: algebra. apply eq_transitive_unfolded with (PartInt (ProjT1 (Diffble_I_n_imp_deriv_n _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (proj1 (Nat.lt_succ_r _ _) (Nat.lt_lt_succ_r _ _ Hi)) _ H2))) a (compact_Min_lft _ _ (less_leEq _ _ _ (ap_imp_Min_less_Max _ _ H1)))). simpl in |- *; algebra. apply Feq_imp_eq with (Compact (less_leEq _ _ _ (ap_imp_Min_less_Max _ _ H1))). apply Derivative_I_n_unique with i F. apply projT2. unfold fi in |- *. elim (N_Deriv_lemma _ _ _ _ (le_imp_Diffble_n I pI i n (proj1 (Nat.lt_succ_r _ _) (Nat.lt_lt_succ_r _ _ Hi)) _ Hf')); intros incF0 H'. elim H'; intros Hinc derivF; clear H'. apply derivF. simpl in |- *; Included. apply compact_Min_lft. apply eq_transitive_unfolded with (PartInt (ProjT1 (Diffble_I_n_imp_deriv_n _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (proj1 (Nat.lt_succ_r _ _) (Nat.lt_succ_diag_r n)) _ H2))) a (compact_Min_lft _ _ (less_leEq _ _ _ (ap_imp_Min_less_Max _ _ H1)))). simpl in |- *; algebra. apply Feq_imp_eq with (Compact (less_leEq _ _ _ (ap_imp_Min_less_Max _ _ H1))). apply Derivative_I_n_unique with n F. apply projT2. unfold fi in |- *. elim (N_Deriv_lemma _ _ _ _ (le_imp_Diffble_n I pI n n (proj1 (Nat.lt_succ_r _ _) (Nat.lt_succ_diag_r n)) _ Hf')); intros incF0 H'. elim H'; intros Hinc derivF; clear H'. apply derivF. simpl in |- *; Included. apply compact_Min_lft. simpl in |- *. repeat apply mult_wdl. apply Feq_imp_eq with (Compact (less_leEq _ _ _ (ap_imp_Min_less_Max _ _ H1))). apply Derivative_I_n_unique with (S n) F. apply Derivative_I_n_wdr with (n_deriv_I _ _ _ _ _ H0). apply Derivative_I_n_unique with n (n_deriv_I _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (le_n_S _ _ (Nat.le_0_l n)) _ H0)). cut (forall HS HSn, Derivative_I_n (ap_imp_Min_less_Max _ _ H1) n (n_deriv_I _ _ (ap_imp_Min_less_Max _ _ H1) 1 F HS) (n_deriv_I _ _ (ap_imp_Min_less_Max _ _ H1) (S n) F HSn)); auto. cut (S n = n + 1); [ intro | rewrite Nat.add_comm; auto ]. rewrite H6. intros; apply n_deriv_plus. eapply Derivative_I_n_wdl. 2: apply n_deriv_lemma. apply Derivative_I_unique with F. apply projT2. apply Derivative_I_wdl with (n_deriv_I _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (Nat.le_0_l _) F H0)). simpl in |- *. FEQ. apply (included_trans _ (Compact (less_leEq IR (Min a b) (Max a b) (ap_imp_Min_less_Max a b H1))) I); Included. apply n_Sn_deriv. apply n_deriv_lemma. elim (N_Deriv_lemma _ _ _ _ Hf); intros incF0 H'. elim H'; intros Hinc derivF; clear H'. apply derivF. simpl in |- *; Included. elim H5; clear H5; intros H6 H7. elim H6; clear H6; intros H5 H8. exact (n_deriv_inc' _ _ _ _ _ _ _ _ H5). Included. cut (Taylor_Rem n Hf'[-]Part _ _ H0[*] (b[-]a) [#] [0]). intro H1; exact (Taylor_lemma_ap _ _ _ _ H1). astepr ZeroR; apply AbsIR_cancel_ap_zero; apply Greater_imp_ap; auto. intro. exists a. apply compact_Min_lft. intro; eapply leEq_wdl. apply less_leEq; apply b0. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.TaylorLemma