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 *********************)
19 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
21 include "ftc/Rolle.ma".
31 (*#* *Taylor's Theorem
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.
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)]].
45 alias id "a" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/a.var".
47 alias id "b" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/b.var".
49 alias id "Hap" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hap.var".
53 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab'.con" "Taylor_Defs__".
55 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab.con" "Taylor_Defs__".
57 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/I.con" "Taylor_Defs__".
61 alias id "F" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/F.var".
63 alias id "Ha" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Ha.var".
65 alias id "Hb" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hb.var".
69 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/fi.con" "Taylor_Defs__".
74 This last local definition is simply:
75 $f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
80 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con".
85 Now we can define the Taylor sequence around [a]. The auxiliary
86 definition gives, for any [i], the function expressed by the rule
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].
95 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_a.con" "Taylor_Defs__".
97 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_b.con" "Taylor_Defs__".
100 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
104 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
111 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i.con" "Taylor_Defs__".
117 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i'.con" "Taylor_Defs__".
119 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con".
121 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con".
123 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con".
125 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con".
127 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con".
129 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con".
131 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con".
133 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con".
135 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con".
137 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con".
142 Adding the previous expressions up to a given bound [n] gives us the
143 Taylor sum of order [n].
146 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con".
150 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Taylor_seq'_aux.con" "Taylor_Defs__".
152 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con".
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].
160 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con".
164 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con".
166 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con".
170 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con".
174 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g.con" "Taylor_Defs__".
177 Opaque Taylor_seq'_aux Taylor_rem.
181 Transparent Taylor_rem.
189 Transparent Taylor_seq' Taylor_seq'_aux.
200 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con".
203 Transparent funct_i funct_i'.
207 Opaque Taylor_seq'_aux.
211 Transparent Taylor_seq'_aux.
222 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con".
225 Transparent funct_i' FSumx.
228 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_aux.con" "Taylor_Defs__".
230 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con".
233 Ltac Lazy_Included :=
236 | apply included_FPlus
237 | apply included_FInv
238 | apply included_FMinus
239 | apply included_FMult
240 | apply included_FNth
241 | apply included_refl ].
247 [ apply bin_op_wd_unfolded
248 | apply un_op_wd_unfolded
251 | apply csf_wd_unfolded ]; Algebra.
254 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con".
256 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con".
263 Transparent funct_aux.
266 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con".
268 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g'.con" "Taylor_Defs__".
271 Opaque Taylor_rem funct_aux.
274 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con".
277 Transparent Taylor_rem funct_aux.
283 Now Taylor's theorem.
285 %\begin{convention}% Let [e] be a positive real number.
289 alias id "e" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/e.var".
291 alias id "He" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/He.var".
295 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con".
301 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/deriv_Sn'.con" "Taylor_Defs__".
307 inline procedural "cic:/CoRN/ftc/TaylorLemma/TLH.con".
320 Transparent Taylor_rem funct_aux.
323 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con".