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