proposition: Lemma Taylor_Series_conv_IR : fun_series_convergent_IR realline (Taylor_Series _ _ _ a Ha _ derF).
proof: Proof. red in |- *; intros. unfold Taylor_Series, FPowerSeries' in |- *. apply fun_str_comparison with (fun n : nat => Fconst (S:=IR) (([1] [/]TwoNZ) [^]n)). Contin. apply conv_fun_const_series with (x := fun n : nat => (OneR [/]TwoNZ) [^]n). apply ratio_test_conv. exists 0; exists (OneR [/]TwoNZ); repeat split. apply pos_div_two'; apply pos_one. apply less_leEq; fold (Half:IR) in |- *; apply pos_half. intros; apply eq_imp_leEq. eapply eq_transitive_unfolded. 2: apply mult_commutes. eapply eq_transitive_unfolded. 2: apply AbsIR_mult_pos; apply less_leEq; fold (Half (R:=IR)) in |- *; apply pos_half. Transparent nexp_op. apply AbsIR_wd; simpl in |- *; rational. Opaque nexp_op. elim (Taylor_Series_conv_lemma2 _ _ Hab [1] (pos_one _)); intros N HN; exists N; intros n H0 x X Hx Hx'. eapply leEq_wdr. eapply leEq_wdl. apply (HN _ H0 _ X Hx). apply AbsIR_wd; algebra. simpl in |- *; algebra. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor