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".
19 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
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.