proposition: Lemma Taylor_Series_conv_to_fun : Feq realline F (FSeries_Sum Hf).
proof: Proof. cut (Continuous realline (FSeries_Sum Hf)). intro H0. cut (forall n : nat, Continuous realline (FSum0 n (Taylor_Series _ _ _ _ Ha _ derF))). intro H2. cut (Continuous realline F). intro H3. eapply FLim_unique_IR with (HG := H0) (HF := H3) (f := fun n : nat => FSum0 n (Taylor_Series _ _ _ _ Ha _ derF)) (contf := H2). 2: apply FSeries_conv. 3: Contin. 2: apply Derivative_imp_Continuous with H (f 1). 2: apply Derivative_n_Sn with F 0. 2: apply Derivative_n_O; eapply Derivative_n_imp_inc; apply (derF 0). 2: auto. 2: unfold Taylor_Series in |- *; Contin. intros a0 b Hab Hinc e H4. set (Hab' := Min_leEq_Max' a0 b a) in *. elim (Taylor_Series_conv_lemma1 a _ _ Hab _ (pos_div_two _ _ H4)); intros N HN. exists (S N); intros p Hp. cut (p = S (pred p)); [ intro Hn | symmetry; apply Nat.lt_succ_pred with N; auto ]. set (n := pred p) in *; clearbody n. generalize Hp; clear Hp; rewrite Hn; clear Hn p. intros. cut ([0] [<] nring (S n) [*]e [/]TwoNZ); [ intro He | apply mult_resp_pos ]. 2: apply pos_nring_S. 2: apply pos_div_two; auto. elim (Taylor' _ _ _ _ _ Ha (Hinc x Hx) n (Derivative_n_imp_Diffble_n _ _ _ _ _ (derF (S n))) (Derivative_n_imp_Diffble_n _ _ _ _ _ (derF n)) _ ( pos_div_two _ _ H4)). intros y H5 H6. set (H7 := pair (I, I) (I, I) :Dom (N_Deriv _ _ _ _ (Derivative_n_imp_Diffble_n _ _ _ _ _ (derF (S n))) {*} [-C-] ([1][/] _[//]nring_fac_ap_zero _ n) {*} ( [-C-]x{-}FId) {^}n) y) in *. eapply leEq_wdl. 2: apply AbsIR_minus. cut (forall z w : IR, AbsIR z [<=] AbsIR (z[-]w) [+]AbsIR w); intros. 2: eapply leEq_wdl. 2: apply triangle_IR. 2: apply AbsIR_wd; rational. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply (abs_Taylor_Rem_char realline H F a Ha f derF n (Derivative_n_imp_Diffble_n _ _ _ _ _ (derF n)) x (contin_imp_inc _ _ _ _ (included_imp_Continuous _ _ H3 _ _ _ Hinc) _ Hx) (contin_imp_inc _ _ _ _ (included_imp_Continuous _ _ (H2 (S n)) _ _ _ Hinc) _ Hx) (Hinc _ Hx)). rstepr (e [/]TwoNZ[+]e [/]TwoNZ). eapply leEq_transitive. apply H8 with (w := Part (N_Deriv _ _ _ _ (Derivative_n_imp_Diffble_n _ _ _ _ _ (derF (S n))) {*} [-C-] ([1][/] _[//]nring_fac_ap_zero _ n) {*} ( [-C-]x{-}FId) {^}n) y H7[*] (x[-]a)). apply plus_resp_leEq_both; auto. eapply leEq_transitive. 2: apply Taylor_majoration_lemma with (n := S n); apply pos_div_two; auto. rstepr (nring (S n) [*] (e [/]TwoNZ[/] _[//]H1 (S n))). apply shift_leEq_mult' with (pos_ap_zero _ _ (pos_nring_S IR n)). apply pos_nring_S. set (H9 := pair I (pair (I, I) (I, I))) in *. eapply leEq_wdl. apply HN with (n := n) (w := y) (z := x) (Hw := I) (Hz := H9); auto with arith. inversion_clear Hx; inversion_clear H5; split. apply leEq_transitive with (Min a x); auto. apply leEq_Min. apply Min_leEq_rht. apply leEq_transitive with a0; auto. apply Min_leEq_lft. apply leEq_transitive with (Max a x); auto. apply Max_leEq. apply rht_leEq_Max. apply leEq_transitive with b; auto. apply lft_leEq_Max. simpl in |- *. unfold Taylor_Rem in |- *; simpl in |- *. clear H8 H6 H4 He Hx Hp HN Hab' H3 H2 H0 bndf. set (fy := Part _ _ (Derivative_n_imp_inc' _ _ _ _ _ (derF (S n)) y I)) in *. set (Fy := Part (N_Deriv _ _ _ _ (Derivative_n_imp_Diffble_n _ _ _ _ _ (derF (S n)))) y (ProjIR1 (ProjIR1 H7))) in *. astepr (AbsIR (Fy[*] ([1][/] _[//]nring_fac_ap_zero _ n) [*] (x[+][--]y) [^]n[*] (x[-]a)) [/] _[//]pos_ap_zero _ _ (pos_nring_S _ n)). unfold cg_minus in |- *. apply eq_symmetric_unfolded; apply Taylor_Series_conv_lemma3. unfold fy, Fy in |- *. apply Feq_imp_eq with realline; auto. apply Derivative_n_unique with H (S n) F; Deriv. eapply eq_transitive_unfolded. 2: apply nring_comm_mult. Transparent fact. replace (fact (S n)) with (fact n * S n). algebra. Opaque mult. unfold fact in |- *; fold (fact n) in |- *. auto with arith. apply nring_nonneg. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor