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