1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/transc/TaylorSeries".
19 (* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *)
31 We now generalize our work on Taylor's theorem to define the Taylor
32 series of an infinitely many times differentiable function as a power
33 series. We prove convergence (always) of the Taylor series and give
34 criteria for when the sum of this series is the original function.
38 %\begin{convention}% Let [J] be a proper interval and [F] an
39 infinitely many times differentiable function in [J]. Let [a] be a
48 inline cic:/CoRN/transc/TaylorSeries/J.var.
50 inline cic:/CoRN/transc/TaylorSeries/pJ.var.
52 inline cic:/CoRN/transc/TaylorSeries/F.var.
54 inline cic:/CoRN/transc/TaylorSeries/diffF.var.
56 inline cic:/CoRN/transc/TaylorSeries/a.var.
58 inline cic:/CoRN/transc/TaylorSeries/Ha.var.
60 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con.
63 %\begin{convention}% Assume also that [f] is the sequence of
68 inline cic:/CoRN/transc/TaylorSeries/f.var.
70 inline cic:/CoRN/transc/TaylorSeries/derF.var.
72 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series.con.
78 (*#* Characterizations of the Taylor remainder. *)
80 inline cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con.
82 inline cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con.
89 Section Convergence_in_IR.
94 Our interval is now the real line. We begin by proving some helpful
95 continuity properties, then define a boundedness condition for the
96 derivatives of [F] that guarantees convergence of its Taylor series to
100 inline cic:/CoRN/transc/TaylorSeries/H.var.
102 inline cic:/CoRN/transc/TaylorSeries/F.var.
104 inline cic:/CoRN/transc/TaylorSeries/a.var.
106 inline cic:/CoRN/transc/TaylorSeries/Ha.var.
108 inline cic:/CoRN/transc/TaylorSeries/f.var.
110 inline cic:/CoRN/transc/TaylorSeries/derF.var.
112 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con.
114 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con.
116 inline cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con.
120 inline cic:/CoRN/transc/TaylorSeries/bndf.var.
130 inline cic:/CoRN/transc/TaylorSeries/H1.con.
136 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con.
138 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con.
142 (*#* The Taylor series always converges on the realline. *)
152 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con.
160 inline cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con.
166 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con.
171 We now prove that, under our assumptions, it actually converges to the
172 original function. For generality and also usability, however, we
173 will separately assume convergence.
178 inline cic:/CoRN/transc/TaylorSeries/Hf.var.
190 inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con.
193 End Convergence_in_IR.
197 Section Other_Results.
201 The condition for the previous lemma is not very easy to prove. We
202 give some helpful lemmas.
205 inline cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con.
213 inline cic:/CoRN/transc/TaylorSeries/convergence_lemma.con.
217 inline cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con.
220 Finally, a uniqueness criterium: two functions [F] and [G] are equal,
221 provided that their derivatives coincide at a given point and their
222 Taylor series converge to themselves.
225 inline cic:/CoRN/transc/TaylorSeries/F.var.
227 inline cic:/CoRN/transc/TaylorSeries/G.var.
229 inline cic:/CoRN/transc/TaylorSeries/a.var.
231 inline cic:/CoRN/transc/TaylorSeries/f.var.
233 inline cic:/CoRN/transc/TaylorSeries/g.var.
235 inline cic:/CoRN/transc/TaylorSeries/derF.var.
237 inline cic:/CoRN/transc/TaylorSeries/derG.var.
239 inline cic:/CoRN/transc/TaylorSeries/bndf.var.
241 inline cic:/CoRN/transc/TaylorSeries/bndg.var.
245 inline cic:/CoRN/transc/TaylorSeries/Heq.var.
251 inline cic:/CoRN/transc/TaylorSeries/Hf.con.
255 inline cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con.