]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/TaylorLemma.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / TaylorLemma.mma
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 include "CoRN.ma".
18
19 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
20
21 include "ftc/Rolle.ma".
22
23 (* UNEXPORTED
24 Opaque Min.
25 *)
26
27 (* UNEXPORTED
28 Section Taylor_Defs
29 *)
30
31 (*#* *Taylor's Theorem
32
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.
37
38 ** First case
39
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)]].
43 *)
44
45 (* UNEXPORTED
46 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/a.var
47 *)
48
49 (* UNEXPORTED
50 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/b.var
51 *)
52
53 (* UNEXPORTED
54 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hap.var
55 *)
56
57 (* begin hide *)
58
59 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab'.con" "Taylor_Defs__" as definition.
60
61 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab.con" "Taylor_Defs__" as definition.
62
63 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/I.con" "Taylor_Defs__" as definition.
64
65 (* end hide *)
66
67 (* UNEXPORTED
68 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/F.var
69 *)
70
71 (* UNEXPORTED
72 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Ha.var
73 *)
74
75 (* UNEXPORTED
76 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hb.var
77 *)
78
79 (* begin show *)
80
81 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/fi.con" "Taylor_Defs__" as definition.
82
83 (* end show *)
84
85 (*#*
86 This last local definition is simply:
87 $f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
88 *)
89
90 (* begin hide *)
91
92 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con" as lemma.
93
94 (* end hide *)
95
96 (*#*
97 Now we can define the Taylor sequence around [a].  The auxiliary
98 definition gives, for any [i], the function expressed by the rule
99 %\[g(x)=\frac{f^{(i)}
100 (a)}{i!}*(x-a)^i.\]%#g(x)=f<sup>(i)</sup>(a)/i!*(x-a)<sup>i</sup>.#
101 We denote by [A] and [B] the elements of [[Min(a,b),Max(a,b)]]
102 corresponding to [a] and [b].
103 *)
104
105 (* begin hide *)
106
107 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_a.con" "Taylor_Defs__" as definition.
108
109 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_b.con" "Taylor_Defs__" as definition.
110
111 (* NOTATION
112 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
113 *)
114
115 (* NOTATION
116 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
117 *)
118
119 (* end hide *)
120
121 (* begin show *)
122
123 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i.con" "Taylor_Defs__" as definition.
124
125 (* end show *)
126
127 (* begin hide *)
128
129 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i'.con" "Taylor_Defs__" as definition.
130
131 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con" as lemma.
132
133 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con" as lemma.
134
135 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con" as lemma.
136
137 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con" as lemma.
138
139 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con" as lemma.
140
141 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con" as lemma.
142
143 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con" as lemma.
144
145 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con" as lemma.
146
147 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con" as lemma.
148
149 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con" as lemma.
150
151 (* end hide *)
152
153 (*#*
154 Adding the previous expressions up to a given bound [n] gives us the
155 Taylor sum of order [n].
156 *)
157
158 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con" as definition.
159
160 (* begin hide *)
161
162 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Taylor_seq'_aux.con" "Taylor_Defs__" as definition.
163
164 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con" as lemma.
165
166 (* end hide *)
167
168 (*#*
169 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].
170 *)
171
172 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con" as lemma.
173
174 (* begin hide *)
175
176 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con" as lemma.
177
178 inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con" as lemma.
179
180 (* end hide *)
181
182 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con" as definition.
183
184 (* begin hide *)
185
186 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g.con" "Taylor_Defs__" as definition.
187
188 (* UNEXPORTED
189 Opaque Taylor_seq'_aux Taylor_rem.
190 *)
191
192 (* UNEXPORTED
193 Transparent Taylor_rem.
194 *)
195
196 (* UNEXPORTED
197 Opaque Taylor_seq'.
198 *)
199
200 (* UNEXPORTED
201 Transparent Taylor_seq' Taylor_seq'_aux.
202 *)
203
204 (* UNEXPORTED
205 Opaque funct_i'.
206 *)
207
208 (* UNEXPORTED
209 Opaque funct_i.
210 *)
211
212 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con" as lemma.
213
214 (* UNEXPORTED
215 Transparent funct_i funct_i'.
216 *)
217
218 (* UNEXPORTED
219 Opaque Taylor_seq'_aux.
220 *)
221
222 (* UNEXPORTED
223 Transparent Taylor_seq'_aux.
224 *)
225
226 (* UNEXPORTED
227 Opaque FSumx.
228 *)
229
230 (* UNEXPORTED
231 Opaque funct_i'.
232 *)
233
234 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con" as lemma.
235
236 (* UNEXPORTED
237 Transparent funct_i' FSumx.
238 *)
239
240 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_aux.con" "Taylor_Defs__" as definition.
241
242 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con" as lemma.
243
244 (* UNEXPORTED
245 Ltac Lazy_Included :=
246   repeat first
247    [ apply included_IR
248    | apply included_FPlus
249    | apply included_FInv
250    | apply included_FMinus
251    | apply included_FMult
252    | apply included_FNth
253    | apply included_refl ].
254 *)
255
256 (* UNEXPORTED
257 Ltac Lazy_Eq :=
258   repeat first
259    [ apply bin_op_wd_unfolded
260    | apply un_op_wd_unfolded
261    | apply cg_minus_wd
262    | apply div_wd
263    | apply csf_wd_unfolded ]; Algebra.
264 *)
265
266 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con" as lemma.
267
268 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con" as lemma.
269
270 (* UNEXPORTED
271 Opaque funct_aux.
272 *)
273
274 (* UNEXPORTED
275 Transparent funct_aux.
276 *)
277
278 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con" as lemma.
279
280 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g'.con" "Taylor_Defs__" as definition.
281
282 (* UNEXPORTED
283 Opaque Taylor_rem funct_aux.
284 *)
285
286 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con" as lemma.
287
288 (* UNEXPORTED
289 Transparent Taylor_rem funct_aux.
290 *)
291
292 (* end hide *)
293
294 (*#*
295 Now Taylor's theorem.
296
297 %\begin{convention}% Let [e] be a positive real number.
298 %\end{convention}%
299 *)
300
301 (* UNEXPORTED
302 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/e.var
303 *)
304
305 (* UNEXPORTED
306 cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/He.var
307 *)
308
309 (* begin hide *)
310
311 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con" as lemma.
312
313 (* end hide *)
314
315 (* begin show *)
316
317 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/deriv_Sn'.con" "Taylor_Defs__" as definition.
318
319 (* end show *)
320
321 (* begin hide *)
322
323 inline procedural "cic:/CoRN/ftc/TaylorLemma/TLH.con" as lemma.
324
325 (* end hide *)
326
327 (* UNEXPORTED
328 Opaque funct_aux.
329 *)
330
331 (* UNEXPORTED
332 Opaque Taylor_rem.
333 *)
334
335 (* UNEXPORTED
336 Transparent Taylor_rem funct_aux.
337 *)
338
339 inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con" as lemma.
340
341 (* UNEXPORTED
342 End Taylor_Defs
343 *)
344