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