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 *********************)
19 (* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *)
21 include "transc/PowerSeries.ma".
23 include "ftc/Taylor.ma".
27 We now generalize our work on Taylor's theorem to define the Taylor
28 series of an infinitely many times differentiable function as a power
29 series. We prove convergence (always) of the Taylor series and give
30 criteria for when the sum of this series is the original function.
34 %\begin{convention}% Let [J] be a proper interval and [F] an
35 infinitely many times differentiable function in [J]. Let [a] be a
45 cic:/CoRN/transc/TaylorSeries/Definitions/J.var
49 cic:/CoRN/transc/TaylorSeries/Definitions/pJ.var
53 cic:/CoRN/transc/TaylorSeries/Definitions/F.var
57 cic:/CoRN/transc/TaylorSeries/Definitions/diffF.var
61 cic:/CoRN/transc/TaylorSeries/Definitions/a.var
65 cic:/CoRN/transc/TaylorSeries/Definitions/Ha.var
68 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con" as definition.
71 %\begin{convention}% Assume also that [f] is the sequence of
77 cic:/CoRN/transc/TaylorSeries/Definitions/f.var
81 cic:/CoRN/transc/TaylorSeries/Definitions/derF.var
84 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con" as definition.
90 (*#* Characterizations of the Taylor remainder. *)
92 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con" as lemma.
94 inline procedural "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con" as lemma.
101 Section Convergence_in_IR
106 Our interval is now the real line. We begin by proving some helpful
107 continuity properties, then define a boundedness condition for the
108 derivatives of [F] that guarantees convergence of its Taylor series to
113 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H.var
117 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/F.var
121 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/a.var
125 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Ha.var
129 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/f.var
133 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/derF.var
136 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con" as lemma.
138 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con" as lemma.
140 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con" as definition.
145 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/bndf.var
156 inline procedural "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H1.con" "Convergence_in_IR__" as definition.
162 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con" as lemma.
164 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con" as lemma.
168 (*#* The Taylor series always converges on the realline. *)
178 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con" as lemma.
186 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con" as lemma.
192 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con" as lemma.
197 We now prove that, under our assumptions, it actually converges to the
198 original function. For generality and also usability, however, we
199 will separately assume convergence.
205 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Hf.var
218 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con" as lemma.
221 End Convergence_in_IR
225 Section Other_Results
229 The condition for the previous lemma is not very easy to prove. We
230 give some helpful lemmas.
233 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con" as lemma.
241 inline procedural "cic:/CoRN/transc/TaylorSeries/convergence_lemma.con" as lemma.
245 inline procedural "cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con" as lemma.
248 Finally, a uniqueness criterium: two functions [F] and [G] are equal,
249 provided that their derivatives coincide at a given point and their
250 Taylor series converge to themselves.
254 cic:/CoRN/transc/TaylorSeries/Other_Results/F.var
258 cic:/CoRN/transc/TaylorSeries/Other_Results/G.var
262 cic:/CoRN/transc/TaylorSeries/Other_Results/a.var
266 cic:/CoRN/transc/TaylorSeries/Other_Results/f.var
270 cic:/CoRN/transc/TaylorSeries/Other_Results/g.var
274 cic:/CoRN/transc/TaylorSeries/Other_Results/derF.var
278 cic:/CoRN/transc/TaylorSeries/Other_Results/derG.var
282 cic:/CoRN/transc/TaylorSeries/Other_Results/bndf.var
286 cic:/CoRN/transc/TaylorSeries/Other_Results/bndg.var
292 cic:/CoRN/transc/TaylorSeries/Other_Results/Heq.var
299 inline procedural "cic:/CoRN/transc/TaylorSeries/Other_Results/Hf.con" "Other_Results__" as definition.
303 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con" as lemma.