helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma

   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 set "baseuri" "cic:/matita/CoRN-Decl/transc/TaylorSeries".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *)
  22
  23 include "transc/PowerSeries.ma".
  24
  25 include "ftc/Taylor.ma".
  26
  27 (*#* *Taylor Series
  28
  29 We now generalize our work on Taylor's theorem to define the Taylor
  30 series of an infinitely many times differentiable function as a power
  31 series.  We prove convergence (always) of the Taylor series and give
  32 criteria for when the sum of this series is the original function.
  33
  34 **Definitions
  35
  36 %\begin{convention}% Let [J] be a proper interval and [F] an
  37 infinitely many times differentiable function in [J].  Let [a] be a
  38 point of [J].
  39 %\end{convention}%
  40 *)
  41
  42 (* UNEXPORTED
  43 Section Definitions.
  44 *)
  45
  46 inline "cic:/CoRN/transc/TaylorSeries/J.var".
  47
  48 inline "cic:/CoRN/transc/TaylorSeries/pJ.var".
  49
  50 inline "cic:/CoRN/transc/TaylorSeries/F.var".
  51
  52 inline "cic:/CoRN/transc/TaylorSeries/diffF.var".
  53
  54 inline "cic:/CoRN/transc/TaylorSeries/a.var".
  55
  56 inline "cic:/CoRN/transc/TaylorSeries/Ha.var".
  57
  58 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con".
  59
  60 (*#*
  61 %\begin{convention}% Assume also that [f] is the sequence of
  62 derivatives of [F].
  63 %\end{convention}%
  64 *)
  65
  66 inline "cic:/CoRN/transc/TaylorSeries/f.var".
  67
  68 inline "cic:/CoRN/transc/TaylorSeries/derF.var".
  69
  70 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con".
  71
  72 (* UNEXPORTED
  73 Opaque N_Deriv.
  74 *)
  75
  76 (*#* Characterizations of the Taylor remainder. *)
  77
  78 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con".
  79
  80 inline "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con".
  81
  82 (* UNEXPORTED
  83 End Definitions.
  84 *)
  85
  86 (* UNEXPORTED
  87 Section Convergence_in_IR.
  88 *)
  89
  90 (*#* **Convergence
  91
  92 Our interval is now the real line.  We begin by proving some helpful
  93 continuity properties, then define a boundedness condition for the
  94 derivatives of [F] that guarantees convergence of its Taylor series to
  95 [F].
  96 *)
  97
  98 inline "cic:/CoRN/transc/TaylorSeries/H.var".
  99
 100 inline "cic:/CoRN/transc/TaylorSeries/F.var".
 101
 102 inline "cic:/CoRN/transc/TaylorSeries/a.var".
 103
 104 inline "cic:/CoRN/transc/TaylorSeries/Ha.var".
 105
 106 inline "cic:/CoRN/transc/TaylorSeries/f.var".
 107
 108 inline "cic:/CoRN/transc/TaylorSeries/derF.var".
 109
 110 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con".
 111
 112 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con".
 113
 114 inline "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con".
 115
 116 (* begin show *)
 117
 118 inline "cic:/CoRN/transc/TaylorSeries/bndf.var".
 119
 120 (* end show *)
 121
 122 (* UNEXPORTED
 123 Opaque nexp_op fac.
 124 *)
 125
 126 (* begin hide *)
 127
 128 inline "cic:/CoRN/transc/TaylorSeries/H1.con".
 129
 130 (* UNEXPORTED
 131 Transparent nexp_op.
 132 *)
 133
 134 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con".
 135
 136 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con".
 137
 138 (* end hide *)
 139
 140 (*#* The Taylor series always converges on the realline. *)
 141
 142 (* UNEXPORTED
 143 Transparent nexp_op.
 144 *)
 145
 146 (* UNEXPORTED
 147 Opaque nexp_op.
 148 *)
 149
 150 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con".
 151
 152 (* begin hide *)
 153
 154 (* UNEXPORTED
 155 Transparent nexp_op.
 156 *)
 157
 158 inline "cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con".
 159
 160 (* UNEXPORTED
 161 Opaque N_Deriv fac.
 162 *)
 163
 164 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con".
 165
 166 (* end hide *)
 167
 168 (*#*
 169 We now prove that, under our assumptions, it actually converges to the
 170 original function.  For generality and also usability, however, we
 171 will separately assume convergence.
 172 *)
 173
 174 (* begin show *)
 175
 176 inline "cic:/CoRN/transc/TaylorSeries/Hf.var".
 177
 178 (* end show *)
 179
 180 (* UNEXPORTED
 181 Transparent fac.
 182 *)
 183
 184 (* UNEXPORTED
 185 Opaque mult.
 186 *)
 187
 188 inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con".
 189
 190 (* UNEXPORTED
 191 End Convergence_in_IR.
 192 *)
 193
 194 (* UNEXPORTED
 195 Section Other_Results.
 196 *)
 197
 198 (*#*
 199 The condition for the previous lemma is not very easy to prove.  We
 200 give some helpful lemmas.
 201 *)
 202
 203 inline "cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con".
 204
 205 (* begin hide *)
 206
 207 (* UNEXPORTED
 208 Opaque nexp_op.
 209 *)
 210
 211 inline "cic:/CoRN/transc/TaylorSeries/convergence_lemma.con".
 212
 213 (* end hide *)
 214
 215 inline "cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con".
 216
 217 (*#*
 218 Finally, a uniqueness criterium: two functions [F] and [G] are equal,
 219 provided that their derivatives coincide at a given point and their
 220 Taylor series converge to themselves.
 221 *)
 222
 223 inline "cic:/CoRN/transc/TaylorSeries/F.var".
 224
 225 inline "cic:/CoRN/transc/TaylorSeries/G.var".
 226
 227 inline "cic:/CoRN/transc/TaylorSeries/a.var".
 228
 229 inline "cic:/CoRN/transc/TaylorSeries/f.var".
 230
 231 inline "cic:/CoRN/transc/TaylorSeries/g.var".
 232
 233 inline "cic:/CoRN/transc/TaylorSeries/derF.var".
 234
 235 inline "cic:/CoRN/transc/TaylorSeries/derG.var".
 236
 237 inline "cic:/CoRN/transc/TaylorSeries/bndf.var".
 238
 239 inline "cic:/CoRN/transc/TaylorSeries/bndg.var".
 240
 241 (* begin show *)
 242
 243 inline "cic:/CoRN/transc/TaylorSeries/Heq.var".
 244
 245 (* end show *)
 246
 247 (* begin hide *)
 248
 249 inline "cic:/CoRN/transc/TaylorSeries/Hf.con".
 250
 251 (* end hide *)
 252
 253 inline "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con".
 254
 255 (* UNEXPORTED
 256 End Other_Results.
 257 *)
 258