helm/software/matita/contribs/procedural/CoRN/transc/TaylorSeries.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *)
  20
  21 include "transc/PowerSeries.ma".
  22
  23 include "ftc/Taylor.ma".
  24
  25 (*#* *Taylor Series
  26
  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.
  31
  32 **Definitions
  33
  34 %\begin{convention}% Let [J] be a proper interval and [F] an
  35 infinitely many times differentiable function in [J].  Let [a] be a
  36 point of [J].
  37 %\end{convention}%
  38 *)
  39
  40 (* UNEXPORTED
  41 Section Definitions
  42 *)
  43
  44 (* UNEXPORTED
  45 cic:/CoRN/transc/TaylorSeries/Definitions/J.var
  46 *)
  47
  48 (* UNEXPORTED
  49 cic:/CoRN/transc/TaylorSeries/Definitions/pJ.var
  50 *)
  51
  52 (* UNEXPORTED
  53 cic:/CoRN/transc/TaylorSeries/Definitions/F.var
  54 *)
  55
  56 (* UNEXPORTED
  57 cic:/CoRN/transc/TaylorSeries/Definitions/diffF.var
  58 *)
  59
  60 (* UNEXPORTED
  61 cic:/CoRN/transc/TaylorSeries/Definitions/a.var
  62 *)
  63
  64 (* UNEXPORTED
  65 cic:/CoRN/transc/TaylorSeries/Definitions/Ha.var
  66 *)
  67
  68 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con" as definition.
  69
  70 (*#*
  71 %\begin{convention}% Assume also that [f] is the sequence of
  72 derivatives of [F].
  73 %\end{convention}%
  74 *)
  75
  76 (* UNEXPORTED
  77 cic:/CoRN/transc/TaylorSeries/Definitions/f.var
  78 *)
  79
  80 (* UNEXPORTED
  81 cic:/CoRN/transc/TaylorSeries/Definitions/derF.var
  82 *)
  83
  84 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con" as definition.
  85
  86 (* UNEXPORTED
  87 Opaque N_Deriv.
  88 *)
  89
  90 (*#* Characterizations of the Taylor remainder. *)
  91
  92 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con" as lemma.
  93
  94 inline procedural "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con" as lemma.
  95
  96 (* UNEXPORTED
  97 End Definitions
  98 *)
  99
 100 (* UNEXPORTED
 101 Section Convergence_in_IR
 102 *)
 103
 104 (*#* **Convergence
 105
 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
 109 [F].
 110 *)
 111
 112 (* UNEXPORTED
 113 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H.var
 114 *)
 115
 116 (* UNEXPORTED
 117 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/F.var
 118 *)
 119
 120 (* UNEXPORTED
 121 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/a.var
 122 *)
 123
 124 (* UNEXPORTED
 125 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Ha.var
 126 *)
 127
 128 (* UNEXPORTED
 129 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/f.var
 130 *)
 131
 132 (* UNEXPORTED
 133 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/derF.var
 134 *)
 135
 136 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con" as lemma.
 137
 138 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con" as lemma.
 139
 140 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con" as definition.
 141
 142 (* begin show *)
 143
 144 (* UNEXPORTED
 145 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/bndf.var
 146 *)
 147
 148 (* end show *)
 149
 150 (* UNEXPORTED
 151 Opaque nexp_op fac.
 152 *)
 153
 154 (* begin hide *)
 155
 156 inline procedural "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H1.con" "Convergence_in_IR__" as definition.
 157
 158 (* UNEXPORTED
 159 Transparent nexp_op.
 160 *)
 161
 162 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con" as lemma.
 163
 164 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con" as lemma.
 165
 166 (* end hide *)
 167
 168 (*#* The Taylor series always converges on the realline. *)
 169
 170 (* UNEXPORTED
 171 Transparent nexp_op.
 172 *)
 173
 174 (* UNEXPORTED
 175 Opaque nexp_op.
 176 *)
 177
 178 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con" as lemma.
 179
 180 (* begin hide *)
 181
 182 (* UNEXPORTED
 183 Transparent nexp_op.
 184 *)
 185
 186 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con" as lemma.
 187
 188 (* UNEXPORTED
 189 Opaque N_Deriv fac.
 190 *)
 191
 192 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con" as lemma.
 193
 194 (* end hide *)
 195
 196 (*#*
 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.
 200 *)
 201
 202 (* begin show *)
 203
 204 (* UNEXPORTED
 205 cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Hf.var
 206 *)
 207
 208 (* end show *)
 209
 210 (* UNEXPORTED
 211 Transparent fac.
 212 *)
 213
 214 (* UNEXPORTED
 215 Opaque mult.
 216 *)
 217
 218 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con" as lemma.
 219
 220 (* UNEXPORTED
 221 End Convergence_in_IR
 222 *)
 223
 224 (* UNEXPORTED
 225 Section Other_Results
 226 *)
 227
 228 (*#*
 229 The condition for the previous lemma is not very easy to prove.  We
 230 give some helpful lemmas.
 231 *)
 232
 233 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con" as lemma.
 234
 235 (* begin hide *)
 236
 237 (* UNEXPORTED
 238 Opaque nexp_op.
 239 *)
 240
 241 inline procedural "cic:/CoRN/transc/TaylorSeries/convergence_lemma.con" as lemma.
 242
 243 (* end hide *)
 244
 245 inline procedural "cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con" as lemma.
 246
 247 (*#*
 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.
 251 *)
 252
 253 (* UNEXPORTED
 254 cic:/CoRN/transc/TaylorSeries/Other_Results/F.var
 255 *)
 256
 257 (* UNEXPORTED
 258 cic:/CoRN/transc/TaylorSeries/Other_Results/G.var
 259 *)
 260
 261 (* UNEXPORTED
 262 cic:/CoRN/transc/TaylorSeries/Other_Results/a.var
 263 *)
 264
 265 (* UNEXPORTED
 266 cic:/CoRN/transc/TaylorSeries/Other_Results/f.var
 267 *)
 268
 269 (* UNEXPORTED
 270 cic:/CoRN/transc/TaylorSeries/Other_Results/g.var
 271 *)
 272
 273 (* UNEXPORTED
 274 cic:/CoRN/transc/TaylorSeries/Other_Results/derF.var
 275 *)
 276
 277 (* UNEXPORTED
 278 cic:/CoRN/transc/TaylorSeries/Other_Results/derG.var
 279 *)
 280
 281 (* UNEXPORTED
 282 cic:/CoRN/transc/TaylorSeries/Other_Results/bndf.var
 283 *)
 284
 285 (* UNEXPORTED
 286 cic:/CoRN/transc/TaylorSeries/Other_Results/bndg.var
 287 *)
 288
 289 (* begin show *)
 290
 291 (* UNEXPORTED
 292 cic:/CoRN/transc/TaylorSeries/Other_Results/Heq.var
 293 *)
 294
 295 (* end show *)
 296
 297 (* begin hide *)
 298
 299 inline procedural "cic:/CoRN/transc/TaylorSeries/Other_Results/Hf.con" "Other_Results__" as definition.
 300
 301 (* end hide *)
 302
 303 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con" as lemma.
 304
 305 (* UNEXPORTED
 306 End Other_Results
 307 *)
 308