1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/TaylorLemma".
21 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
23 include "ftc/Rolle.ma".
33 (*#* *Taylor's Theorem
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.
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)]].
47 inline "cic:/CoRN/ftc/TaylorLemma/a.var".
49 inline "cic:/CoRN/ftc/TaylorLemma/b.var".
51 inline "cic:/CoRN/ftc/TaylorLemma/Hap.var".
55 inline "cic:/CoRN/ftc/TaylorLemma/Hab'.con".
57 inline "cic:/CoRN/ftc/TaylorLemma/Hab.con".
59 inline "cic:/CoRN/ftc/TaylorLemma/I.con".
63 inline "cic:/CoRN/ftc/TaylorLemma/F.var".
65 inline "cic:/CoRN/ftc/TaylorLemma/Ha.var".
67 inline "cic:/CoRN/ftc/TaylorLemma/Hb.var".
71 inline "cic:/CoRN/ftc/TaylorLemma/fi.con".
76 This last local definition is simply:
77 $f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
82 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con".
87 Now we can define the Taylor sequence around [a]. The auxiliary
88 definition gives, for any [i], the function expressed by the rule
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].
97 inline "cic:/CoRN/ftc/TaylorLemma/TL_compact_a.con".
99 inline "cic:/CoRN/ftc/TaylorLemma/TL_compact_b.con".
105 inline "cic:/CoRN/ftc/TaylorLemma/funct_i.con".
111 inline "cic:/CoRN/ftc/TaylorLemma/funct_i'.con".
113 inline "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con".
115 inline "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con".
117 inline "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con".
119 inline "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con".
121 inline "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con".
123 inline "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con".
125 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con".
127 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con".
129 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con".
131 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con".
136 Adding the previous expressions up to a given bound [n] gives us the
137 Taylor sum of order [n].
140 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con".
144 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'_aux.con".
146 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con".
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].
154 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con".
158 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con".
160 inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con".
164 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con".
168 inline "cic:/CoRN/ftc/TaylorLemma/g.con".
171 Opaque Taylor_seq'_aux Taylor_rem.
175 Transparent Taylor_rem.
183 Transparent Taylor_seq' Taylor_seq'_aux.
194 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con".
197 Transparent funct_i funct_i'.
201 Opaque Taylor_seq'_aux.
205 Transparent Taylor_seq'_aux.
216 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con".
219 Transparent funct_i' FSumx.
222 inline "cic:/CoRN/ftc/TaylorLemma/funct_aux.con".
224 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con".
227 Ltac Lazy_Included :=
230 | apply included_FPlus
231 | apply included_FInv
232 | apply included_FMinus
233 | apply included_FMult
234 | apply included_FNth
235 | apply included_refl ].
241 [ apply bin_op_wd_unfolded
242 | apply un_op_wd_unfolded
245 | apply csf_wd_unfolded ]; Algebra.
248 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con".
250 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con".
257 Transparent funct_aux.
260 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con".
262 inline "cic:/CoRN/ftc/TaylorLemma/g'.con".
265 Opaque Taylor_rem funct_aux.
268 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con".
271 Transparent Taylor_rem funct_aux.
277 Now Taylor's theorem.
279 %\begin{convention}% Let [e] be a positive real number.
283 inline "cic:/CoRN/ftc/TaylorLemma/e.var".
285 inline "cic:/CoRN/ftc/TaylorLemma/He.var".
289 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con".
295 inline "cic:/CoRN/ftc/TaylorLemma/deriv_Sn'.con".
301 inline "cic:/CoRN/ftc/TaylorLemma/TLH.con".
314 Transparent Taylor_rem funct_aux.
317 inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con".