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
44 alias id "J" = "cic:/CoRN/transc/TaylorSeries/Definitions/J.var".
46 alias id "pJ" = "cic:/CoRN/transc/TaylorSeries/Definitions/pJ.var".
48 alias id "F" = "cic:/CoRN/transc/TaylorSeries/Definitions/F.var".
50 alias id "diffF" = "cic:/CoRN/transc/TaylorSeries/Definitions/diffF.var".
52 alias id "a" = "cic:/CoRN/transc/TaylorSeries/Definitions/a.var".
54 alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Definitions/Ha.var".
56 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con".
59 %\begin{convention}% Assume also that [f] is the sequence of
64 alias id "f" = "cic:/CoRN/transc/TaylorSeries/Definitions/f.var".
66 alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Definitions/derF.var".
68 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con".
74 (*#* Characterizations of the Taylor remainder. *)
76 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con".
78 inline procedural "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con".
85 Section Convergence_in_IR
90 Our interval is now the real line. We begin by proving some helpful
91 continuity properties, then define a boundedness condition for the
92 derivatives of [F] that guarantees convergence of its Taylor series to
96 alias id "H" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H.var".
98 alias id "F" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/F.var".
100 alias id "a" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/a.var".
102 alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Ha.var".
104 alias id "f" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/f.var".
106 alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/derF.var".
108 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con".
110 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con".
112 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con".
116 alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/bndf.var".
126 inline procedural "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H1.con" "Convergence_in_IR__".
132 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con".
134 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con".
138 (*#* The Taylor series always converges on the realline. *)
148 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con".
156 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con".
162 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con".
167 We now prove that, under our assumptions, it actually converges to the
168 original function. For generality and also usability, however, we
169 will separately assume convergence.
174 alias id "Hf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Hf.var".
186 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con".
189 End Convergence_in_IR
193 Section Other_Results
197 The condition for the previous lemma is not very easy to prove. We
198 give some helpful lemmas.
201 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con".
209 inline procedural "cic:/CoRN/transc/TaylorSeries/convergence_lemma.con".
213 inline procedural "cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con".
216 Finally, a uniqueness criterium: two functions [F] and [G] are equal,
217 provided that their derivatives coincide at a given point and their
218 Taylor series converge to themselves.
221 alias id "F" = "cic:/CoRN/transc/TaylorSeries/Other_Results/F.var".
223 alias id "G" = "cic:/CoRN/transc/TaylorSeries/Other_Results/G.var".
225 alias id "a" = "cic:/CoRN/transc/TaylorSeries/Other_Results/a.var".
227 alias id "f" = "cic:/CoRN/transc/TaylorSeries/Other_Results/f.var".
229 alias id "g" = "cic:/CoRN/transc/TaylorSeries/Other_Results/g.var".
231 alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derF.var".
233 alias id "derG" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derG.var".
235 alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndf.var".
237 alias id "bndg" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndg.var".
241 alias id "Heq" = "cic:/CoRN/transc/TaylorSeries/Other_Results/Heq.var".
247 inline procedural "cic:/CoRN/transc/TaylorSeries/Other_Results/Hf.con" "Other_Results__".
251 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con".