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].
60 alias id "a" = "cic:/CoRN/ftc/Integral/Integral/a.var".
62 alias id "b" = "cic:/CoRN/ftc/Integral/Integral/b.var".
64 alias id "Hab" = "cic:/CoRN/ftc/Integral/Integral/Hab.var".
68 inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__" as definition.
70 alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var".
72 alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var".
74 inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__" as definition.
82 inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con" as definition.
84 inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con" as lemma.
86 inline procedural "cic:/CoRN/ftc/Integral/integral.con" as definition.
97 The following shows that in fact the integral of [F] is the limit of
98 any sequence of partitions of mesh converging to 0.
100 %\begin{convention}% Let [e] be a positive real number and [P] be a
101 partition of [I] with [n] points and mesh smaller than the
102 modulus of continuity of [F] for [e]. Let [fP] be a choice of points
107 alias id "n" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var".
109 alias id "P" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var".
111 alias id "e" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var".
113 alias id "He" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var".
117 inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__" as definition.
121 alias id "HmeshP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var".
123 alias id "fP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var".
125 alias id "HfP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var".
127 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var".
129 alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var".
131 inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con" as lemma.
142 Section Basic_Properties
146 The usual extensionality and strong extensionality results hold.
149 alias id "a" = "cic:/CoRN/ftc/Integral/Basic_Properties/a.var".
151 alias id "b" = "cic:/CoRN/ftc/Integral/Basic_Properties/b.var".
153 alias id "Hab" = "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var".
157 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__" as definition.
162 Notation Integral := (integral _ _ Hab).
166 Section Well_Definedness
169 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var".
171 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var".
173 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var".
175 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var".
177 inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con" as lemma.
179 inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con" as lemma.
181 inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con" as lemma.
183 inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con" as lemma.
190 Section Linearity_and_Monotonicity
194 Opaque Even_Partition.
198 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#.
201 inline procedural "cic:/CoRN/ftc/Integral/integral_one.con" as lemma.
203 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var".
205 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var".
207 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var".
209 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var".
211 inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con" as lemma.
213 inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con" as lemma.
216 Transparent Even_Partition.
219 inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con" as lemma.
222 End Linearity_and_Monotonicity
226 Section Linearity_and_Monotonicity'
229 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var".
231 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var".
233 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var".
235 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var".
238 %\begin{convention}% Let [alpha, beta : IR] and assume that
239 [h := alpha{**}F{+}beta{**}G] is continuous.
243 alias id "alpha" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var".
245 alias id "beta" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var".
249 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__" as definition.
253 alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var".
255 inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con" as lemma.
261 inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con" as lemma.
268 End Linearity_and_Monotonicity'
275 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var".
277 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var".
279 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var".
281 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var".
284 As corollaries we can calculate integrals of group operations applied to functions.
287 inline procedural "cic:/CoRN/ftc/Integral/integral_const.con" as lemma.
289 inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con" as lemma.
291 inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con" as lemma.
294 We can also bound integrals by bounding the integrated functions.
297 inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con" as lemma.
299 inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con" as lemma.
301 inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con" as lemma.
312 We now relate the sum of integrals in adjoining intervals to the
313 integral over the union of those intervals.
315 %\begin{convention}% Let [c] be a real number such that
316 $c\in[a,b]$#c∈[a,b]#.
320 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var".
322 alias id "c" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var".
324 alias id "Hac" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var".
326 alias id "Hcb" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var".
328 alias id "Hab'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var".
330 alias id "Hac'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var".
332 alias id "Hcb'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var".
335 Section Partition_Join
339 We first prove that every pair of partitions, one of [[a,c]]
340 and another of [[c,b]] defines a partition of [[a,b]] the mesh
341 of which is less or equal to the maximum of the mesh of the original
342 partitions (actually it is equal, but we don't need the other
345 %\begin{convention}% Let [P,Q] be partitions respectively of
346 [[a,c]] and [[c,b]] with [n] and [m] points.
350 alias id "n" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var".
352 alias id "m" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var".
354 alias id "P" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var".
356 alias id "Q" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var".
360 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con" as lemma.
364 inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con" as definition.
368 inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con" as lemma.
370 inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con" as lemma.
372 inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con" as lemma.
374 inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con" as lemma.
376 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con" as lemma.
378 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con" as lemma.
380 inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con" as lemma.
382 inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con" as lemma.
384 inline procedural "cic:/CoRN/ftc/Integral/partition_join.con" as definition.
389 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
393 alias id "fP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var".
395 alias id "HfP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var".
397 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var".
399 alias id "fQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var".
401 alias id "HfQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var".
403 alias id "HfQ'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var".
407 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con" as lemma.
411 inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con" as definition.
415 inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con" as lemma.
417 inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con" as lemma.
419 inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con" as lemma.
423 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con" as lemma.
425 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con" as lemma.
428 Opaque partition_join.
432 Transparent partition_join.
451 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con" as lemma.
453 inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con" as lemma.
460 With these results in mind, the following is a trivial consequence:
464 Opaque Even_Partition.
467 inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con" as lemma.
474 Transparent Even_Partition.
482 The following are simple consequences of this result and of previous ones.
485 inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con" as lemma.
489 inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con" as lemma.
493 (*#* remove printing Integral *)