proposition: Lemma Taylor_lemma_ap : forall n Hf Hf' Ha', Taylor_Rem n Hf'[-]deriv_Sn b n Hf a Ha'[*] (b[-]a) [#] [0] -> a [#] b.
proof: Proof. intros. rename X into H. set (Hpred := Diffble_n_imp_inc _ _ _ _ Hf') in *. cut (Taylor_Rem n Hf'[-]Part _ _ Ha'[*] (b[-]a) [#] [0][-][0]). 2: astepr ZeroR; auto. clear H; intros. rename X into H. elim (cg_minus_strext _ _ _ _ _ H); clear H; intro H. unfold Taylor_Rem, Taylor_Seq', funct_i in H. cut (Dom (FSumx n (fun i (Hi : i < n) => [-C-] (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//] nring_fac_ap_zero IR (S i)) {*} (FId{-} [-C-]a) {^}S i)) b). 2: apply FSumx_pred'; repeat split. intro H0. cut (F b (Hpred b Hb) [-]F a (Hpred a Ha) [#] [0] or Part _ _ H0 [#] [0]). intro H1. elim H1; clear H H1; intro H. apply pfstrx with (Hx := Hpred a Ha) (Hy := Hpred b Hb). apply ap_symmetric_unfolded; apply zero_minus_apart; auto. cut (ext_fun_seq' (fun i (Hi : i < n) => [-C-] (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) {*} (FId{-} [-C-]a) {^}S i)). 2: red in |- *; repeat split. intro H1. cut (Sumx (fun i (Hi : i < n) => Part _ _ (FSumx_pred n _ H1 _ H0 i Hi)) [#] Sumx (fun i (Hi : i < n) => [0])). intro H2. 2: eapply ap_wdl_unfolded. 2: eapply ap_wdr_unfolded. 2: apply H. 2: apply eq_symmetric_unfolded; eapply eq_transitive_unfolded; [ apply sumx_const | algebra ]. 2: exact (FSumx_char _ _ _ _ H1). simpl in H2. cut (nat_less_n_fun (fun i (Hi : i < n) => (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) [*] (nexp IR i (b[+][--]a) [*] (b[+][--]a)))); intros. cut (nat_less_n_fun (fun i (Hi : i < n) => ([0]:IR))); intros. elim (Sumx_strext _ _ _ _ H3 H4 H2); clear H H0 H1 H2 H3 H4; intros N HN. elim HN; clear HN; intros HN H. cut (b[+][--]a [#] [0]). intro H3. 2: eapply cring_mult_ap_zero_op; eapply cring_mult_ap_zero_op; apply H. apply ap_symmetric_unfolded; apply zero_minus_apart; auto. red in |- *; algebra. red in |- *; do 3 intro. rewrite H3; intros; unfold fi in |- *. apply mult_wdl. apply div_wd. 2: algebra. apply Feq_imp_eq with I. apply Derivative_n_unique with pI (S j) F; apply N_Deriv_lemma. auto. apply cg_minus_strext. astepr ZeroR. apply ap_wdl_unfolded with (Part _ _ (Hpred b Hb) [-]Part _ _ (TaylorB n Hf')); auto. unfold Taylor_Seq', funct_i in |- *. cut (ext_fun_seq' (fun i Hi => [-C-] (fi n Hf' i Hi a Ha[/] _[//]nring_fac_ap_zero IR i) {*} (FId{-} [-C-]a) {^}i)). intro H1. apply eq_transitive_unfolded with (Part _ _ (Hpred b Hb) [-] Sumx (fun i Hi => Part _ _ (FSumx_pred _ _ H1 b (TaylorB n Hf') i Hi))). apply cg_minus_wd. algebra. exact (FSumx_char _ _ _ _ H1). cut (ext_fun_seq' (fun i (Hi : i < n) => [-C-] (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) {*} (FId{-} [-C-]a) {^}S i)). intro H2. apply eq_transitive_unfolded with (Part _ _ (Hpred b Hb) [-]Part _ _ (Hpred a Ha) [-] Sumx (fun i (Hi : i < n) => Part _ _ (FSumx_pred _ _ H2 b H0 i Hi))). 2: apply cg_minus_wd. 2: algebra. 2: apply eq_symmetric_unfolded; exact (FSumx_char _ _ _ _ H2). apply Taylor_Sumx_lemma. intros; simpl in |- *. unfold fi in |- *. rstepr ((Part _ _ (Hpred a Ha) [/] [0][+][1][//]nring_fac_ap_zero IR 0) [*][1]). apply mult_wdl; apply div_wd. 2: algebra. apply Feq_imp_eq with I. apply Derivative_n_unique with pI 0 F. apply N_Deriv_lemma. split; auto. split; auto. intros; simpl in |- *. apply Feq_reflexive; Included. auto. intros; simpl in |- *. apply mult_wdl; apply div_wd. 2: algebra. unfold fi in |- *. apply Feq_imp_eq with I. apply Derivative_n_unique with pI (S i) F; apply N_Deriv_lemma; auto. auto. repeat split. repeat split. apply ap_symmetric_unfolded; apply zero_minus_apart. eapply cring_mult_ap_zero_op; apply H. Qed.
imports: CoRN.ftc.TaylorLemma