]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/CoRN-Decl/ftc/Integral.ma
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
[helm.git] / matitaB / matita / contribs / CoRN-Decl / ftc / Integral.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/Integral".
18
19 include "CoRN.ma".
20
21 (* $Id: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)
22
23 include "ftc/RefLemma.ma".
24
25 (*#* printing integral %\ensuremath{\int_I}% #&int;<sub>I</sub># *)
26
27 (*#* printing Integral %\ensuremath{\int_I}% #&int;<sub>I</sub># *)
28
29 (* begin hide *)
30
31 (* UNEXPORTED
32 Section Lemmas
33 *)
34
35 inline "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__".
36
37 inline "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con".
38
39 (* UNEXPORTED
40 End Lemmas
41 *)
42
43 (* end hide *)
44
45 (* UNEXPORTED
46 Section Integral
47 *)
48
49 (*#* *Integral
50
51 Having proved the main properties of partitions and refinements, we
52 will define the integral of a continuous function [F] in the interval
53 [[a,b]] as the limit of the sequence of Sums of $F$ for even
54 partitions of increasing number of points.
55
56 %\begin{convention}% All throughout, [a,b] will be real numbers, the
57 interval [[a,b]] will be denoted by [I] and [F,G] will be
58 continuous functions in [I].
59 %\end{convention}%
60 *)
61
62 alias id "a" = "cic:/CoRN/ftc/Integral/Integral/a.var".
63
64 alias id "b" = "cic:/CoRN/ftc/Integral/Integral/b.var".
65
66 alias id "Hab" = "cic:/CoRN/ftc/Integral/Integral/Hab.var".
67
68 (* begin hide *)
69
70 inline "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__".
71
72 alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var".
73
74 alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var".
75
76 inline "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__".
77
78 (* end hide *)
79
80 (* UNEXPORTED
81 Section Darboux_Sum
82 *)
83
84 inline "cic:/CoRN/ftc/Integral/integral_seq.con".
85
86 inline "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con".
87
88 inline "cic:/CoRN/ftc/Integral/integral.con".
89
90 (* UNEXPORTED
91 End Darboux_Sum
92 *)
93
94 (* UNEXPORTED
95 Section Integral_Thm
96 *)
97
98 (*#*
99 The following shows that in fact the integral of [F] is the limit of
100 any sequence of partitions of mesh converging to 0.
101
102 %\begin{convention}% Let [e] be a positive real number and [P] be a
103 partition of [I] with [n] points and mesh smaller than the
104 modulus of continuity of [F] for [e].  Let [fP] be a choice of points
105 respecting [P].
106 %\end{convention}%
107 *)
108
109 alias id "n" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var".
110
111 alias id "P" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var".
112
113 alias id "e" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var".
114
115 alias id "He" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var".
116
117 (* begin hide *)
118
119 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__".
120
121 (* end hide *)
122
123 alias id "HmeshP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var".
124
125 alias id "fP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var".
126
127 alias id "HfP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var".
128
129 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var".
130
131 alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var".
132
133 inline "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con".
134
135 (* UNEXPORTED
136 End Integral_Thm
137 *)
138
139 (* UNEXPORTED
140 End Integral
141 *)
142
143 (* UNEXPORTED
144 Section Basic_Properties
145 *)
146
147 (*#*
148 The usual extensionality and strong extensionality results hold.
149 *)
150
151 alias id "a" = "cic:/CoRN/ftc/Integral/Basic_Properties/a.var".
152
153 alias id "b" = "cic:/CoRN/ftc/Integral/Basic_Properties/b.var".
154
155 alias id "Hab" = "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var".
156
157 (* begin hide *)
158
159 inline "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__".
160
161 (* end hide *)
162
163 (* NOTATION
164 Notation Integral := (integral _ _ Hab).
165 *)
166
167 (* UNEXPORTED
168 Section Well_Definedness
169 *)
170
171 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var".
172
173 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var".
174
175 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var".
176
177 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var".
178
179 inline "cic:/CoRN/ftc/Integral/integral_strext.con".
180
181 inline "cic:/CoRN/ftc/Integral/integral_strext'.con".
182
183 inline "cic:/CoRN/ftc/Integral/integral_wd.con".
184
185 inline "cic:/CoRN/ftc/Integral/integral_wd'.con".
186
187 (* UNEXPORTED
188 End Well_Definedness
189 *)
190
191 (* UNEXPORTED
192 Section Linearity_and_Monotonicity
193 *)
194
195 (* UNEXPORTED
196 Opaque Even_Partition.
197 *)
198
199 (*#*
200 The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities $\int_a^bdx=b-a$#&int;<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#&int;<sub>a</sub><sup>a</sup>=0#.
201 *)
202
203 inline "cic:/CoRN/ftc/Integral/integral_one.con".
204
205 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var".
206
207 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var".
208
209 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var".
210
211 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var".
212
213 inline "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
214
215 inline "cic:/CoRN/ftc/Integral/integral_plus.con".
216
217 (* UNEXPORTED
218 Transparent Even_Partition.
219 *)
220
221 inline "cic:/CoRN/ftc/Integral/integral_empty.con".
222
223 (* UNEXPORTED
224 End Linearity_and_Monotonicity
225 *)
226
227 (* UNEXPORTED
228 Section Linearity_and_Monotonicity'
229 *)
230
231 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var".
232
233 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var".
234
235 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var".
236
237 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var".
238
239 (*#*
240 %\begin{convention}% Let [alpha, beta : IR] and assume that
241 [h := alpha{**}F{+}beta{**}G] is continuous.
242 %\end{convention}%
243 *)
244
245 alias id "alpha" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var".
246
247 alias id "beta" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var".
248
249 (* begin hide *)
250
251 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__".
252
253 (* end hide *)
254
255 alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var".
256
257 inline "cic:/CoRN/ftc/Integral/linear_integral.con".
258
259 (* UNEXPORTED
260 Opaque nring.
261 *)
262
263 inline "cic:/CoRN/ftc/Integral/monotonous_integral.con".
264
265 (* UNEXPORTED
266 Transparent nring.
267 *)
268
269 (* UNEXPORTED
270 End Linearity_and_Monotonicity'
271 *)
272
273 (* UNEXPORTED
274 Section Corollaries
275 *)
276
277 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var".
278
279 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var".
280
281 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var".
282
283 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var".
284
285 (*#*
286 As corollaries we can calculate integrals of group operations applied to functions.
287 *)
288
289 inline "cic:/CoRN/ftc/Integral/integral_const.con".
290
291 inline "cic:/CoRN/ftc/Integral/integral_minus.con".
292
293 inline "cic:/CoRN/ftc/Integral/integral_inv.con".
294
295 (*#*
296 We can also bound integrals by bounding the integrated functions.
297 *)
298
299 inline "cic:/CoRN/ftc/Integral/lb_integral.con".
300
301 inline "cic:/CoRN/ftc/Integral/ub_integral.con".
302
303 inline "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
304
305 (* UNEXPORTED
306 End Corollaries
307 *)
308
309 (* UNEXPORTED
310 Section Integral_Sum
311 *)
312
313 (*#*
314 We now relate the sum of integrals in adjoining intervals to the
315 integral over the union of those intervals.
316
317 %\begin{convention}% Let [c] be a real number such that
318 $c\in[a,b]$#c&isin;[a,b]#.
319 %\end{convention}%
320 *)
321
322 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var".
323
324 alias id "c" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var".
325
326 alias id "Hac" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var".
327
328 alias id "Hcb" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var".
329
330 alias id "Hab'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var".
331
332 alias id "Hac'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var".
333
334 alias id "Hcb'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var".
335
336 (* UNEXPORTED
337 Section Partition_Join
338 *)
339
340 (*#*
341 We first prove that every pair of partitions, one of [[a,c]]
342 and another of [[c,b]] defines a partition of [[a,b]] the mesh
343 of which is less or equal to the maximum of the mesh of the original
344 partitions (actually it is equal, but we don't need the other
345 inequality).
346
347 %\begin{convention}% Let [P,Q] be partitions respectively of
348 [[a,c]] and [[c,b]] with [n] and [m] points.
349 %\end{convention}%
350 *)
351
352 alias id "n" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var".
353
354 alias id "m" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var".
355
356 alias id "P" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var".
357
358 alias id "Q" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var".
359
360 (* begin hide *)
361
362 inline "cic:/CoRN/ftc/Integral/partition_join_aux.con".
363
364 (* end hide *)
365
366 inline "cic:/CoRN/ftc/Integral/partition_join_fun.con".
367
368 (* begin hide *)
369
370 inline "cic:/CoRN/ftc/Integral/pjf_1.con".
371
372 inline "cic:/CoRN/ftc/Integral/pjf_2.con".
373
374 inline "cic:/CoRN/ftc/Integral/pjf_2'.con".
375
376 inline "cic:/CoRN/ftc/Integral/pjf_3.con".
377
378 inline "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
379
380 inline "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
381
382 inline "cic:/CoRN/ftc/Integral/partition_join_start.con".
383
384 inline "cic:/CoRN/ftc/Integral/partition_join_finish.con".
385
386 inline "cic:/CoRN/ftc/Integral/partition_join.con".
387
388 (* end hide *)
389
390 (*#*
391 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
392 %\end{convention}%
393 *)
394
395 alias id "fP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var".
396
397 alias id "HfP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var".
398
399 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var".
400
401 alias id "fQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var".
402
403 alias id "HfQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var".
404
405 alias id "HfQ'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var".
406
407 (* begin hide *)
408
409 inline "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
410
411 (* end hide *)
412
413 inline "cic:/CoRN/ftc/Integral/partition_join_pts.con".
414
415 (* begin hide *)
416
417 inline "cic:/CoRN/ftc/Integral/pjp_1.con".
418
419 inline "cic:/CoRN/ftc/Integral/pjp_2.con".
420
421 inline "cic:/CoRN/ftc/Integral/pjp_3.con".
422
423 (* end hide *)
424
425 inline "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
426
427 inline "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
428
429 (* UNEXPORTED
430 Opaque partition_join.
431 *)
432
433 (* UNEXPORTED
434 Transparent partition_join.
435 *)
436
437 (* UNEXPORTED
438 Opaque minus.
439 *)
440
441 (* UNEXPORTED
442 Transparent minus.
443 *)
444
445 (* UNEXPORTED
446 Opaque minus.
447 *)
448
449 (* UNEXPORTED
450 Transparent minus.
451 *)
452
453 inline "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
454
455 inline "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
456
457 (* UNEXPORTED
458 End Partition_Join
459 *)
460
461 (*#*
462 With these results in mind, the following is a trivial consequence:
463 *)
464
465 (* UNEXPORTED
466 Opaque Even_Partition.
467 *)
468
469 inline "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
470
471 (* UNEXPORTED
472 End Integral_Sum
473 *)
474
475 (* UNEXPORTED
476 Transparent Even_Partition.
477 *)
478
479 (* UNEXPORTED
480 End Basic_Properties
481 *)
482
483 (*#*
484 The following are simple consequences of this result and of previous ones.
485 *)
486
487 inline "cic:/CoRN/ftc/Integral/integral_less_norm.con".
488
489 (* end hide *)
490
491 inline "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
492
493 (* end hide *)
494
495 (*#* remove printing Integral *)
496