helm/software/matita/contribs/CoRN-Procedural/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 alias id "J" = "cic:/CoRN/transc/TaylorSeries/Definitions/J.var".
  45
  46 alias id "pJ" = "cic:/CoRN/transc/TaylorSeries/Definitions/pJ.var".
  47
  48 alias id "F" = "cic:/CoRN/transc/TaylorSeries/Definitions/F.var".
  49
  50 alias id "diffF" = "cic:/CoRN/transc/TaylorSeries/Definitions/diffF.var".
  51
  52 alias id "a" = "cic:/CoRN/transc/TaylorSeries/Definitions/a.var".
  53
  54 alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Definitions/Ha.var".
  55
  56 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con" as definition.
  57
  58 (*#*
  59 %\begin{convention}% Assume also that [f] is the sequence of
  60 derivatives of [F].
  61 %\end{convention}%
  62 *)
  63
  64 alias id "f" = "cic:/CoRN/transc/TaylorSeries/Definitions/f.var".
  65
  66 alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Definitions/derF.var".
  67
  68 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con" as definition.
  69
  70 (* UNEXPORTED
  71 Opaque N_Deriv.
  72 *)
  73
  74 (*#* Characterizations of the Taylor remainder. *)
  75
  76 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con" as lemma.
  77
  78 inline procedural "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con" as lemma.
  79
  80 (* UNEXPORTED
  81 End Definitions
  82 *)
  83
  84 (* UNEXPORTED
  85 Section Convergence_in_IR
  86 *)
  87
  88 (*#* **Convergence
  89
  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
  93 [F].
  94 *)
  95
  96 alias id "H" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H.var".
  97
  98 alias id "F" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/F.var".
  99
 100 alias id "a" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/a.var".
 101
 102 alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Ha.var".
 103
 104 alias id "f" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/f.var".
 105
 106 alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/derF.var".
 107
 108 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con" as lemma.
 109
 110 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con" as lemma.
 111
 112 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con" as definition.
 113
 114 (* begin show *)
 115
 116 alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/bndf.var".
 117
 118 (* end show *)
 119
 120 (* UNEXPORTED
 121 Opaque nexp_op fac.
 122 *)
 123
 124 (* begin hide *)
 125
 126 inline procedural "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H1.con" "Convergence_in_IR__" as definition.
 127
 128 (* UNEXPORTED
 129 Transparent nexp_op.
 130 *)
 131
 132 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con" as lemma.
 133
 134 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con" as lemma.
 135
 136 (* end hide *)
 137
 138 (*#* The Taylor series always converges on the realline. *)
 139
 140 (* UNEXPORTED
 141 Transparent nexp_op.
 142 *)
 143
 144 (* UNEXPORTED
 145 Opaque nexp_op.
 146 *)
 147
 148 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con" as lemma.
 149
 150 (* begin hide *)
 151
 152 (* UNEXPORTED
 153 Transparent nexp_op.
 154 *)
 155
 156 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con" as lemma.
 157
 158 (* UNEXPORTED
 159 Opaque N_Deriv fac.
 160 *)
 161
 162 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con" as lemma.
 163
 164 (* end hide *)
 165
 166 (*#*
 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.
 170 *)
 171
 172 (* begin show *)
 173
 174 alias id "Hf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Hf.var".
 175
 176 (* end show *)
 177
 178 (* UNEXPORTED
 179 Transparent fac.
 180 *)
 181
 182 (* UNEXPORTED
 183 Opaque mult.
 184 *)
 185
 186 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con" as lemma.
 187
 188 (* UNEXPORTED
 189 End Convergence_in_IR
 190 *)
 191
 192 (* UNEXPORTED
 193 Section Other_Results
 194 *)
 195
 196 (*#*
 197 The condition for the previous lemma is not very easy to prove.  We
 198 give some helpful lemmas.
 199 *)
 200
 201 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con" as lemma.
 202
 203 (* begin hide *)
 204
 205 (* UNEXPORTED
 206 Opaque nexp_op.
 207 *)
 208
 209 inline procedural "cic:/CoRN/transc/TaylorSeries/convergence_lemma.con" as lemma.
 210
 211 (* end hide *)
 212
 213 inline procedural "cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con" as lemma.
 214
 215 (*#*
 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.
 219 *)
 220
 221 alias id "F" = "cic:/CoRN/transc/TaylorSeries/Other_Results/F.var".
 222
 223 alias id "G" = "cic:/CoRN/transc/TaylorSeries/Other_Results/G.var".
 224
 225 alias id "a" = "cic:/CoRN/transc/TaylorSeries/Other_Results/a.var".
 226
 227 alias id "f" = "cic:/CoRN/transc/TaylorSeries/Other_Results/f.var".
 228
 229 alias id "g" = "cic:/CoRN/transc/TaylorSeries/Other_Results/g.var".
 230
 231 alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derF.var".
 232
 233 alias id "derG" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derG.var".
 234
 235 alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndf.var".
 236
 237 alias id "bndg" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndg.var".
 238
 239 (* begin show *)
 240
 241 alias id "Heq" = "cic:/CoRN/transc/TaylorSeries/Other_Results/Heq.var".
 242
 243 (* end show *)
 244
 245 (* begin hide *)
 246
 247 inline procedural "cic:/CoRN/transc/TaylorSeries/Other_Results/Hf.con" "Other_Results__" as definition.
 248
 249 (* end hide *)
 250
 251 inline procedural "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con" as lemma.
 252
 253 (* UNEXPORTED
 254 End Other_Results
 255 *)
 256