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".
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/Lemmas/Sumx_wd_weird.con" "Lemmas__".
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/Integral/a.var" "Integral__".
64 inline "cic:/CoRN/ftc/Integral/Integral/b.var" "Integral__".
66 inline "cic:/CoRN/ftc/Integral/Integral/Hab.var" "Integral__".
70 inline "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__".
72 inline "cic:/CoRN/ftc/Integral/Integral/F.var" "Integral__".
74 inline "cic:/CoRN/ftc/Integral/Integral/contF.var" "Integral__".
76 inline "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__".
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/Integral/Integral_Thm/n.var" "Integral__Integral_Thm__".
111 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var" "Integral__Integral_Thm__".
113 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var" "Integral__Integral_Thm__".
115 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var" "Integral__Integral_Thm__".
119 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__".
123 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var" "Integral__Integral_Thm__".
125 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var" "Integral__Integral_Thm__".
127 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var" "Integral__Integral_Thm__".
129 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var" "Integral__Integral_Thm__".
131 inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var" "Integral__Integral_Thm__".
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/Basic_Properties/a.var" "Basic_Properties__".
153 inline "cic:/CoRN/ftc/Integral/Basic_Properties/b.var" "Basic_Properties__".
155 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var" "Basic_Properties__".
159 inline "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__".
164 Notation Integral := (integral _ _ Hab).
168 Section Well_Definedness
171 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var" "Basic_Properties__Well_Definedness__".
173 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var" "Basic_Properties__Well_Definedness__".
175 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var" "Basic_Properties__Well_Definedness__".
177 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var" "Basic_Properties__Well_Definedness__".
179 inline "cic:/CoRN/ftc/Integral/integral_strext.con".
181 inline "cic:/CoRN/ftc/Integral/integral_strext'.con".
183 inline "cic:/CoRN/ftc/Integral/integral_wd.con".
185 inline "cic:/CoRN/ftc/Integral/integral_wd'.con".
192 Section Linearity_and_Monotonicity
196 Opaque Even_Partition.
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$#∫<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#∫<sub>a</sub><sup>a</sup>=0#.
203 inline "cic:/CoRN/ftc/Integral/integral_one.con".
205 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var" "Basic_Properties__Linearity_and_Monotonicity__".
207 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var" "Basic_Properties__Linearity_and_Monotonicity__".
209 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var" "Basic_Properties__Linearity_and_Monotonicity__".
211 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var" "Basic_Properties__Linearity_and_Monotonicity__".
213 inline "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
215 inline "cic:/CoRN/ftc/Integral/integral_plus.con".
218 Transparent Even_Partition.
221 inline "cic:/CoRN/ftc/Integral/integral_empty.con".
224 End Linearity_and_Monotonicity
228 Section Linearity_and_Monotonicity'
231 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var" "Basic_Properties__Linearity_and_Monotonicity'__".
233 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var" "Basic_Properties__Linearity_and_Monotonicity'__".
235 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var" "Basic_Properties__Linearity_and_Monotonicity'__".
237 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var" "Basic_Properties__Linearity_and_Monotonicity'__".
240 %\begin{convention}% Let [alpha, beta : IR] and assume that
241 [h := alpha{**}F{+}beta{**}G] is continuous.
245 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var" "Basic_Properties__Linearity_and_Monotonicity'__".
247 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var" "Basic_Properties__Linearity_and_Monotonicity'__".
251 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__".
255 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var" "Basic_Properties__Linearity_and_Monotonicity'__".
257 inline "cic:/CoRN/ftc/Integral/linear_integral.con".
263 inline "cic:/CoRN/ftc/Integral/monotonous_integral.con".
270 End Linearity_and_Monotonicity'
277 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var" "Basic_Properties__Corollaries__".
279 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var" "Basic_Properties__Corollaries__".
281 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var" "Basic_Properties__Corollaries__".
283 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var" "Basic_Properties__Corollaries__".
286 As corollaries we can calculate integrals of group operations applied to functions.
289 inline "cic:/CoRN/ftc/Integral/integral_const.con".
291 inline "cic:/CoRN/ftc/Integral/integral_minus.con".
293 inline "cic:/CoRN/ftc/Integral/integral_inv.con".
296 We can also bound integrals by bounding the integrated functions.
299 inline "cic:/CoRN/ftc/Integral/lb_integral.con".
301 inline "cic:/CoRN/ftc/Integral/ub_integral.con".
303 inline "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
314 We now relate the sum of integrals in adjoining intervals to the
315 integral over the union of those intervals.
317 %\begin{convention}% Let [c] be a real number such that
318 $c\in[a,b]$#c∈[a,b]#.
322 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var" "Basic_Properties__Integral_Sum__".
324 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var" "Basic_Properties__Integral_Sum__".
326 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var" "Basic_Properties__Integral_Sum__".
328 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var" "Basic_Properties__Integral_Sum__".
330 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var" "Basic_Properties__Integral_Sum__".
332 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var" "Basic_Properties__Integral_Sum__".
334 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var" "Basic_Properties__Integral_Sum__".
337 Section Partition_Join
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
347 %\begin{convention}% Let [P,Q] be partitions respectively of
348 [[a,c]] and [[c,b]] with [n] and [m] points.
352 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var" "Basic_Properties__Integral_Sum__Partition_Join__".
354 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var" "Basic_Properties__Integral_Sum__Partition_Join__".
356 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var" "Basic_Properties__Integral_Sum__Partition_Join__".
358 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var" "Basic_Properties__Integral_Sum__Partition_Join__".
362 inline "cic:/CoRN/ftc/Integral/partition_join_aux.con".
366 inline "cic:/CoRN/ftc/Integral/partition_join_fun.con".
370 inline "cic:/CoRN/ftc/Integral/pjf_1.con".
372 inline "cic:/CoRN/ftc/Integral/pjf_2.con".
374 inline "cic:/CoRN/ftc/Integral/pjf_2'.con".
376 inline "cic:/CoRN/ftc/Integral/pjf_3.con".
378 inline "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
380 inline "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
382 inline "cic:/CoRN/ftc/Integral/partition_join_start.con".
384 inline "cic:/CoRN/ftc/Integral/partition_join_finish.con".
386 inline "cic:/CoRN/ftc/Integral/partition_join.con".
391 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
395 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var" "Basic_Properties__Integral_Sum__Partition_Join__".
397 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var" "Basic_Properties__Integral_Sum__Partition_Join__".
399 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var" "Basic_Properties__Integral_Sum__Partition_Join__".
401 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var" "Basic_Properties__Integral_Sum__Partition_Join__".
403 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var" "Basic_Properties__Integral_Sum__Partition_Join__".
405 inline "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var" "Basic_Properties__Integral_Sum__Partition_Join__".
409 inline "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
413 inline "cic:/CoRN/ftc/Integral/partition_join_pts.con".
417 inline "cic:/CoRN/ftc/Integral/pjp_1.con".
419 inline "cic:/CoRN/ftc/Integral/pjp_2.con".
421 inline "cic:/CoRN/ftc/Integral/pjp_3.con".
425 inline "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
427 inline "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
430 Opaque partition_join.
434 Transparent partition_join.
453 inline "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
455 inline "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
462 With these results in mind, the following is a trivial consequence:
466 Opaque Even_Partition.
469 inline "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
476 Transparent Even_Partition.
484 The following are simple consequences of this result and of previous ones.
487 inline "cic:/CoRN/ftc/Integral/integral_less_norm.con".
491 inline "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
495 (*#* remove printing Integral *)