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: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)
21 include "ftc/RefLemma.ma".
23 (*#* printing integral %\ensuremath{\int_I}% #∫<sub>I</sub># *)
25 (*#* printing Integral %\ensuremath{\int_I}% #∫<sub>I</sub># *)
33 inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__" as definition.
35 inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con" as lemma.
49 Having proved the main properties of partitions and refinements, we
50 will define the integral of a continuous function [F] in the interval
51 [[a,b]] as the limit of the sequence of Sums of $F$ for even
52 partitions of increasing number of points.
54 %\begin{convention}% All throughout, [a,b] will be real numbers, the
55 interval [[a,b]] will be denoted by [I] and [F,G] will be
56 continuous functions in [I].
61 cic:/CoRN/ftc/Integral/Integral/a.var
65 cic:/CoRN/ftc/Integral/Integral/b.var
69 cic:/CoRN/ftc/Integral/Integral/Hab.var
74 inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__" as definition.
77 cic:/CoRN/ftc/Integral/Integral/F.var
81 cic:/CoRN/ftc/Integral/Integral/contF.var
84 inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__" as definition.
92 inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con" as definition.
94 inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con" as lemma.
96 inline procedural "cic:/CoRN/ftc/Integral/integral.con" as definition.
107 The following shows that in fact the integral of [F] is the limit of
108 any sequence of partitions of mesh converging to 0.
110 %\begin{convention}% Let [e] be a positive real number and [P] be a
111 partition of [I] with [n] points and mesh smaller than the
112 modulus of continuity of [F] for [e]. Let [fP] be a choice of points
118 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var
122 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var
126 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var
130 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var
135 inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__" as definition.
140 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var
144 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var
148 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var
152 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var
156 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var
159 inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con" as lemma.
170 Section Basic_Properties
174 The usual extensionality and strong extensionality results hold.
178 cic:/CoRN/ftc/Integral/Basic_Properties/a.var
182 cic:/CoRN/ftc/Integral/Basic_Properties/b.var
186 cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var
191 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__" as definition.
196 Notation Integral := (integral _ _ Hab).
200 Section Well_Definedness
204 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var
208 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var
212 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var
216 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var
219 inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con" as lemma.
221 inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con" as lemma.
223 inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con" as lemma.
225 inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con" as lemma.
232 Section Linearity_and_Monotonicity
236 Opaque Even_Partition.
240 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$#∫<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#∫<sub>a</sub><sup>a</sup>=0#.
243 inline procedural "cic:/CoRN/ftc/Integral/integral_one.con" as lemma.
246 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var
250 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var
254 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var
258 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var
261 inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con" as lemma.
263 inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con" as lemma.
266 Transparent Even_Partition.
269 inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con" as lemma.
272 End Linearity_and_Monotonicity
276 Section Linearity_and_Monotonicity'
280 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var
284 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var
288 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var
292 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var
296 %\begin{convention}% Let [alpha, beta : IR] and assume that
297 [h := alpha{**}F{+}beta{**}G] is continuous.
302 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var
306 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var
311 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__" as definition.
316 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var
319 inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con" as lemma.
325 inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con" as lemma.
332 End Linearity_and_Monotonicity'
340 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var
344 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var
348 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var
352 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var
356 As corollaries we can calculate integrals of group operations applied to functions.
359 inline procedural "cic:/CoRN/ftc/Integral/integral_const.con" as lemma.
361 inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con" as lemma.
363 inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con" as lemma.
366 We can also bound integrals by bounding the integrated functions.
369 inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con" as lemma.
371 inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con" as lemma.
373 inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con" as lemma.
384 We now relate the sum of integrals in adjoining intervals to the
385 integral over the union of those intervals.
387 %\begin{convention}% Let [c] be a real number such that
388 $c\in[a,b]$#c∈[a,b]#.
393 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var
397 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var
401 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var
405 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var
409 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var
413 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var
417 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var
421 Section Partition_Join
425 We first prove that every pair of partitions, one of [[a,c]]
426 and another of [[c,b]] defines a partition of [[a,b]] the mesh
427 of which is less or equal to the maximum of the mesh of the original
428 partitions (actually it is equal, but we don't need the other
431 %\begin{convention}% Let [P,Q] be partitions respectively of
432 [[a,c]] and [[c,b]] with [n] and [m] points.
437 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var
441 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var
445 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var
449 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var
454 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con" as lemma.
458 inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con" as definition.
462 inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con" as lemma.
464 inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con" as lemma.
466 inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con" as lemma.
468 inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con" as lemma.
470 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con" as lemma.
472 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con" as lemma.
474 inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con" as lemma.
476 inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con" as lemma.
478 inline procedural "cic:/CoRN/ftc/Integral/partition_join.con" as definition.
483 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
488 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var
492 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var
496 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var
500 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var
504 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var
508 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var
513 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con" as lemma.
517 inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con" as definition.
521 inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con" as lemma.
523 inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con" as lemma.
525 inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con" as lemma.
529 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con" as lemma.
531 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con" as lemma.
534 Opaque partition_join.
538 Transparent partition_join.
557 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con" as lemma.
559 inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con" as lemma.
566 With these results in mind, the following is a trivial consequence:
570 Opaque Even_Partition.
573 inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con" as lemma.
580 Transparent Even_Partition.
588 The following are simple consequences of this result and of previous ones.
591 inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con" as lemma.
595 inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con" as lemma.
599 (*#* remove printing Integral *)