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