matita/contribs/CoRN-Decl/ftc/TaylorLemma.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/ftc/TaylorLemma".
  18
  19 include "CoRN_notation.ma".
  20
  21 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
  22
  23 include "ftc/Rolle.ma".
  24
  25 (* UNEXPORTED
  26 Opaque Min.
  27 *)
  28
  29 (* UNEXPORTED
  30 Section Taylor_Defs.
  31 *)
  32
  33 (*#* *Taylor's Theorem
  34
  35 We now prove Taylor's theorem for the remainder of the Taylor
  36 series.  This proof is done in two steps: first, we prove the lemma
  37 for a proper compact interval; next we generalize the result to two
  38 arbitrary (eventually equal) points in a proper interval.
  39
  40 ** First case
  41
  42 We assume two different points [a] and [b] in the domain of [F] and
  43 define the nth order derivative of [F] in the interval
  44 [[Min(a,b),Max(a,b)]].
  45 *)
  46
  47 inline "cic:/CoRN/ftc/TaylorLemma/a.var".
  48
  49 inline "cic:/CoRN/ftc/TaylorLemma/b.var".
  50
  51 inline "cic:/CoRN/ftc/TaylorLemma/Hap.var".
  52
  53 (* begin hide *)
  54
  55 inline "cic:/CoRN/ftc/TaylorLemma/Hab'.con".
  56
  57 inline "cic:/CoRN/ftc/TaylorLemma/Hab.con".
  58
  59 inline "cic:/CoRN/ftc/TaylorLemma/I.con".
  60
  61 (* end hide *)
  62
  63 inline "cic:/CoRN/ftc/TaylorLemma/F.var".
  64
  65 inline "cic:/CoRN/ftc/TaylorLemma/Ha.var".
  66
  67 inline "cic:/CoRN/ftc/TaylorLemma/Hb.var".
  68
  69 (* begin show *)
  70
  71 inline "cic:/CoRN/ftc/TaylorLemma/fi.con".
  72
  73 (* end show *)
  74
  75 (*#*
  76 This last local definition is simply:
  77 $f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
  78 *)
  79
  80 (* begin hide *)
  81
  82 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con".
  83
  84 (* end hide *)
  85
  86 (*#*
  87 Now we can define the Taylor sequence around [a].  The auxiliary
  88 definition gives, for any [i], the function expressed by the rule
  89 %\[g(x)=\frac{f^{(i)}
  90 (a)}{i!}*(x-a)^i.\]%#g(x)=f<sup>(i)</sup>(a)/i!*(x-a)<sup>i</sup>.#
  91 We denote by [A] and [B] the elements of [[Min(a,b),Max(a,b)]]
  92 corresponding to [a] and [b].
  93 *)
  94
  95 (* begin hide *)
  96
  97 inline "cic:/CoRN/ftc/TaylorLemma/TL_compact_a.con".
  98
  99 inline "cic:/CoRN/ftc/TaylorLemma/TL_compact_b.con".
 100
 101 (* end hide *)
 102
 103 (* begin show *)
 104
 105 inline "cic:/CoRN/ftc/TaylorLemma/funct_i.con".
 106
 107 (* end show *)
 108
 109 (* begin hide *)
 110
 111 inline "cic:/CoRN/ftc/TaylorLemma/funct_i'.con".
 112
 113 inline "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con".
 114
 115 inline "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con".
 116
 117 inline "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con".
 118
 119 inline "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con".
 120
 121 inline "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con".
 122
 123 inline "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con".
 124
 125 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con".
 126
 127 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con".
 128
 129 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con".
 130
 131 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con".
 132
 133 (* end hide *)
 134
 135 (*#*
 136 Adding the previous expressions up to a given bound [n] gives us the
 137 Taylor sum of order [n].
 138 *)
 139
 140 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con".
 141
 142 (* begin hide *)
 143
 144 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'_aux.con".
 145
 146 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con".
 147
 148 (* end hide *)
 149
 150 (*#*
 151 It is easy to show that [b] is in the domain of this series, which allows us to write down the Taylor remainder around [b].
 152 *)
 153
 154 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con".
 155
 156 (* begin hide *)
 157
 158 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con".
 159
 160 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con".
 161
 162 (* end hide *)
 163
 164 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con".
 165
 166 (* begin hide *)
 167
 168 inline "cic:/CoRN/ftc/TaylorLemma/g.con".
 169
 170 (* UNEXPORTED
 171 Opaque Taylor_seq'_aux Taylor_rem.
 172 *)
 173
 174 (* UNEXPORTED
 175 Transparent Taylor_rem.
 176 *)
 177
 178 (* UNEXPORTED
 179 Opaque Taylor_seq'.
 180 *)
 181
 182 (* UNEXPORTED
 183 Transparent Taylor_seq' Taylor_seq'_aux.
 184 *)
 185
 186 (* UNEXPORTED
 187 Opaque funct_i'.
 188 *)
 189
 190 (* UNEXPORTED
 191 Opaque funct_i.
 192 *)
 193
 194 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con".
 195
 196 (* UNEXPORTED
 197 Transparent funct_i funct_i'.
 198 *)
 199
 200 (* UNEXPORTED
 201 Opaque Taylor_seq'_aux.
 202 *)
 203
 204 (* UNEXPORTED
 205 Transparent Taylor_seq'_aux.
 206 *)
 207
 208 (* UNEXPORTED
 209 Opaque FSumx.
 210 *)
 211
 212 (* UNEXPORTED
 213 Opaque funct_i'.
 214 *)
 215
 216 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con".
 217
 218 (* UNEXPORTED
 219 Transparent funct_i' FSumx.
 220 *)
 221
 222 inline "cic:/CoRN/ftc/TaylorLemma/funct_aux.con".
 223
 224 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con".
 225
 226 (* UNEXPORTED
 227 Ltac Lazy_Included :=
 228   repeat first
 229    [ apply included_IR
 230    | apply included_FPlus
 231    | apply included_FInv
 232    | apply included_FMinus
 233    | apply included_FMult
 234    | apply included_FNth
 235    | apply included_refl ].
 236 *)
 237
 238 (* UNEXPORTED
 239 Ltac Lazy_Eq :=
 240   repeat first
 241    [ apply bin_op_wd_unfolded
 242    | apply un_op_wd_unfolded
 243    | apply cg_minus_wd
 244    | apply div_wd
 245    | apply csf_wd_unfolded ]; Algebra.
 246 *)
 247
 248 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con".
 249
 250 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con".
 251
 252 (* UNEXPORTED
 253 Opaque funct_aux.
 254 *)
 255
 256 (* UNEXPORTED
 257 Transparent funct_aux.
 258 *)
 259
 260 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con".
 261
 262 inline "cic:/CoRN/ftc/TaylorLemma/g'.con".
 263
 264 (* UNEXPORTED
 265 Opaque Taylor_rem funct_aux.
 266 *)
 267
 268 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con".
 269
 270 (* UNEXPORTED
 271 Transparent Taylor_rem funct_aux.
 272 *)
 273
 274 (* end hide *)
 275
 276 (*#*
 277 Now Taylor's theorem.
 278
 279 %\begin{convention}% Let [e] be a positive real number.
 280 %\end{convention}%
 281 *)
 282
 283 inline "cic:/CoRN/ftc/TaylorLemma/e.var".
 284
 285 inline "cic:/CoRN/ftc/TaylorLemma/He.var".
 286
 287 (* begin hide *)
 288
 289 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con".
 290
 291 (* end hide *)
 292
 293 (* begin show *)
 294
 295 inline "cic:/CoRN/ftc/TaylorLemma/deriv_Sn'.con".
 296
 297 (* end show *)
 298
 299 (* begin hide *)
 300
 301 inline "cic:/CoRN/ftc/TaylorLemma/TLH.con".
 302
 303 (* end hide *)
 304
 305 (* UNEXPORTED
 306 Opaque funct_aux.
 307 *)
 308
 309 (* UNEXPORTED
 310 Opaque Taylor_rem.
 311 *)
 312
 313 (* UNEXPORTED
 314 Transparent Taylor_rem funct_aux.
 315 *)
 316
 317 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con".
 318
 319 (* UNEXPORTED
 320 End Taylor_Defs.
 321 *)
 322