helm/software/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 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 Rolle
  23 *)
  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