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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/Integral".
19 include "CoRN_notation.ma".
21 (* $Id: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)
23 include "ftc/RefLemma.ma".
25 (*#* printing integral %\ensuremath{\int_I}% #∫<sub>I</sub># *)
27 (*#* printing Integral %\ensuremath{\int_I}% #∫<sub>I</sub># *)
35 inline "cic:/CoRN/ftc/Integral/Sumx_wd_weird.con".
37 inline "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con".
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.
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].
62 inline "cic:/CoRN/ftc/Integral/a.var".
64 inline "cic:/CoRN/ftc/Integral/b.var".
66 inline "cic:/CoRN/ftc/Integral/Hab.var".
70 inline "cic:/CoRN/ftc/Integral/I.con".
72 inline "cic:/CoRN/ftc/Integral/F.var".
74 inline "cic:/CoRN/ftc/Integral/contF.var".
76 inline "cic:/CoRN/ftc/Integral/contF'.con".
84 inline "cic:/CoRN/ftc/Integral/integral_seq.con".
86 inline "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con".
88 inline "cic:/CoRN/ftc/Integral/integral.con".
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.
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
109 inline "cic:/CoRN/ftc/Integral/n.var".
111 inline "cic:/CoRN/ftc/Integral/P.var".
113 inline "cic:/CoRN/ftc/Integral/e.var".
115 inline "cic:/CoRN/ftc/Integral/He.var".
119 inline "cic:/CoRN/ftc/Integral/d.con".
123 inline "cic:/CoRN/ftc/Integral/HmeshP.var".
125 inline "cic:/CoRN/ftc/Integral/fP.var".
127 inline "cic:/CoRN/ftc/Integral/HfP.var".
129 inline "cic:/CoRN/ftc/Integral/HfP'.var".
131 inline "cic:/CoRN/ftc/Integral/incF.var".
133 inline "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con".
144 Section Basic_Properties.
148 The usual extensionality and strong extensionality results hold.
151 inline "cic:/CoRN/ftc/Integral/a.var".
153 inline "cic:/CoRN/ftc/Integral/b.var".
155 inline "cic:/CoRN/ftc/Integral/Hab.var".
159 inline "cic:/CoRN/ftc/Integral/I.con".
164 Section Well_Definedness.
167 inline "cic:/CoRN/ftc/Integral/F.var".
169 inline "cic:/CoRN/ftc/Integral/G.var".
171 inline "cic:/CoRN/ftc/Integral/contF.var".
173 inline "cic:/CoRN/ftc/Integral/contG.var".
175 inline "cic:/CoRN/ftc/Integral/integral_strext.con".
177 inline "cic:/CoRN/ftc/Integral/integral_strext'.con".
179 inline "cic:/CoRN/ftc/Integral/integral_wd.con".
181 inline "cic:/CoRN/ftc/Integral/integral_wd'.con".
184 End Well_Definedness.
188 Section Linearity_and_Monotonicity.
192 Opaque Even_Partition.
196 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#.
199 inline "cic:/CoRN/ftc/Integral/integral_one.con".
201 inline "cic:/CoRN/ftc/Integral/F.var".
203 inline "cic:/CoRN/ftc/Integral/G.var".
205 inline "cic:/CoRN/ftc/Integral/contF.var".
207 inline "cic:/CoRN/ftc/Integral/contG.var".
209 inline "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
211 inline "cic:/CoRN/ftc/Integral/integral_plus.con".
214 Transparent Even_Partition.
217 inline "cic:/CoRN/ftc/Integral/integral_empty.con".
220 End Linearity_and_Monotonicity.
224 Section Linearity_and_Monotonicity'.
227 inline "cic:/CoRN/ftc/Integral/F.var".
229 inline "cic:/CoRN/ftc/Integral/G.var".
231 inline "cic:/CoRN/ftc/Integral/contF.var".
233 inline "cic:/CoRN/ftc/Integral/contG.var".
236 %\begin{convention}% Let [alpha, beta : IR] and assume that
237 [h := alpha{**}F{+}beta{**}G] is continuous.
241 inline "cic:/CoRN/ftc/Integral/alpha.var".
243 inline "cic:/CoRN/ftc/Integral/beta.var".
247 inline "cic:/CoRN/ftc/Integral/h.con".
251 inline "cic:/CoRN/ftc/Integral/contH.var".
253 inline "cic:/CoRN/ftc/Integral/linear_integral.con".
259 inline "cic:/CoRN/ftc/Integral/monotonous_integral.con".
266 End Linearity_and_Monotonicity'.
273 inline "cic:/CoRN/ftc/Integral/F.var".
275 inline "cic:/CoRN/ftc/Integral/G.var".
277 inline "cic:/CoRN/ftc/Integral/contF.var".
279 inline "cic:/CoRN/ftc/Integral/contG.var".
282 As corollaries we can calculate integrals of group operations applied to functions.
285 inline "cic:/CoRN/ftc/Integral/integral_const.con".
287 inline "cic:/CoRN/ftc/Integral/integral_minus.con".
289 inline "cic:/CoRN/ftc/Integral/integral_inv.con".
292 We can also bound integrals by bounding the integrated functions.
295 inline "cic:/CoRN/ftc/Integral/lb_integral.con".
297 inline "cic:/CoRN/ftc/Integral/ub_integral.con".
299 inline "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
306 Section Integral_Sum.
310 We now relate the sum of integrals in adjoining intervals to the
311 integral over the union of those intervals.
313 %\begin{convention}% Let [c] be a real number such that
314 $c\in[a,b]$#c∈[a,b]#.
318 inline "cic:/CoRN/ftc/Integral/F.var".
320 inline "cic:/CoRN/ftc/Integral/c.var".
322 inline "cic:/CoRN/ftc/Integral/Hac.var".
324 inline "cic:/CoRN/ftc/Integral/Hcb.var".
326 inline "cic:/CoRN/ftc/Integral/Hab'.var".
328 inline "cic:/CoRN/ftc/Integral/Hac'.var".
330 inline "cic:/CoRN/ftc/Integral/Hcb'.var".
333 Section Partition_Join.
337 We first prove that every pair of partitions, one of [[a,c]]
338 and another of [[c,b]] defines a partition of [[a,b]] the mesh
339 of which is less or equal to the maximum of the mesh of the original
340 partitions (actually it is equal, but we don't need the other
343 %\begin{convention}% Let [P,Q] be partitions respectively of
344 [[a,c]] and [[c,b]] with [n] and [m] points.
348 inline "cic:/CoRN/ftc/Integral/n.var".
350 inline "cic:/CoRN/ftc/Integral/m.var".
352 inline "cic:/CoRN/ftc/Integral/P.var".
354 inline "cic:/CoRN/ftc/Integral/Q.var".
358 inline "cic:/CoRN/ftc/Integral/partition_join_aux.con".
362 inline "cic:/CoRN/ftc/Integral/partition_join_fun.con".
366 inline "cic:/CoRN/ftc/Integral/pjf_1.con".
368 inline "cic:/CoRN/ftc/Integral/pjf_2.con".
370 inline "cic:/CoRN/ftc/Integral/pjf_2'.con".
372 inline "cic:/CoRN/ftc/Integral/pjf_3.con".
374 inline "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
376 inline "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
378 inline "cic:/CoRN/ftc/Integral/partition_join_start.con".
380 inline "cic:/CoRN/ftc/Integral/partition_join_finish.con".
382 inline "cic:/CoRN/ftc/Integral/partition_join.con".
387 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
391 inline "cic:/CoRN/ftc/Integral/fP.var".
393 inline "cic:/CoRN/ftc/Integral/HfP.var".
395 inline "cic:/CoRN/ftc/Integral/HfP'.var".
397 inline "cic:/CoRN/ftc/Integral/fQ.var".
399 inline "cic:/CoRN/ftc/Integral/HfQ.var".
401 inline "cic:/CoRN/ftc/Integral/HfQ'.var".
405 inline "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
409 inline "cic:/CoRN/ftc/Integral/partition_join_pts.con".
413 inline "cic:/CoRN/ftc/Integral/pjp_1.con".
415 inline "cic:/CoRN/ftc/Integral/pjp_2.con".
417 inline "cic:/CoRN/ftc/Integral/pjp_3.con".
421 inline "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
423 inline "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
426 Opaque partition_join.
430 Transparent partition_join.
449 inline "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
451 inline "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
458 With these results in mind, the following is a trivial consequence:
462 Opaque Even_Partition.
465 inline "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
472 Transparent Even_Partition.
476 End Basic_Properties.
480 The following are simple consequences of this result and of previous ones.
483 inline "cic:/CoRN/ftc/Integral/integral_less_norm.con".
487 inline "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
491 (*#* remove printing Integral *)