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: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
21 include "ftc/Integral.ma".
23 include "ftc/MoreFunctions.ma".
29 (*#* printing Integral %\ensuremath{\int}% #∫# *)
31 (*#* printing integral' %\ensuremath{\int}% #∫# *)
33 (*#* *The generalized integral
35 In this file we extend the definition of integral to allow for
36 arbitrary integration domains (that is, not requiring that the lower
37 endpoint of integration be less or equal than the upper endpoint) and
38 we prove the fundamental properties of the new operator.
40 %\begin{convention}% Let [a, b : IR] and assume that [F] and [G] are two
41 partial functions continuous in [[Min(a,b),Max(a,b)]].
46 Before we define the new integral we need to some trivial interval inclusions.
50 cic:/CoRN/ftc/MoreIntegrals/Lemmas/a.var
54 cic:/CoRN/ftc/MoreIntegrals/Lemmas/b.var
58 cic:/CoRN/ftc/MoreIntegrals/Lemmas/Hab.var
61 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con" as lemma.
63 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con" as lemma.
74 The integral is defined by the formula
75 $\int_a^bf=\int_{\min(a,b)}^bf-\int_{\min(a,b)}^af$#∫<sub>a</sub><sup>b</sup>f=∫<sub>min(a,b)</sub><sup>b</sup>f-∫<sub>min(a,b)</sub><sup>a</sup>f#,
76 inspired by the domain union rule; obviously it coincides with the
77 classical definition, and it collapses to the old one in the case [a
82 cic:/CoRN/ftc/MoreIntegrals/Definitions/a.var
86 cic:/CoRN/ftc/MoreIntegrals/Definitions/b.var
90 cic:/CoRN/ftc/MoreIntegrals/Definitions/Hab.var
94 cic:/CoRN/ftc/MoreIntegrals/Definitions/F.var
98 cic:/CoRN/ftc/MoreIntegrals/Definitions/HF.var
101 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con" as lemma.
103 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con" as lemma.
105 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral.con" as definition.
107 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con" as lemma.
114 Implicit Arguments Integral [a b Hab F].
118 Section Properties_of_Integral
121 (*#* **Properties of the Integral
123 All our old properties carry over to this new definition---and some
124 new ones, too. We begin with (strong) extensionality.
128 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/a.var
132 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/b.var
136 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/Hab.var
140 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/F.var
144 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/G.var
148 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contF.var
152 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contG.var
155 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con" as lemma.
157 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con" as lemma.
159 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con" as lemma.
161 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con" as lemma.
164 The integral is a linear operator.
167 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con" as lemma.
169 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con" as lemma.
171 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con" as lemma.
173 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con" as lemma.
175 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con" as lemma.
177 inline procedural "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con" as lemma.
180 If the endpoints are equal then the integral vanishes.
183 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con" as lemma.
186 And the norm provides an upper bound for the absolute value of the integral.
189 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con" as lemma.
192 End Properties_of_Integral
196 Section More_Properties
200 Two other ways of stating the addition law for domains.
203 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con" as lemma.
205 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con" as lemma.
208 And now we can prove the addition law for domains with our general operator.
210 %\begin{convention}% Assume [c : IR].
215 cic:/CoRN/ftc/MoreIntegrals/More_Properties/a.var
219 cic:/CoRN/ftc/MoreIntegrals/More_Properties/b.var
223 cic:/CoRN/ftc/MoreIntegrals/More_Properties/c.var
229 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab'.var
233 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac'.var
237 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb'.var
241 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc'.var
247 cic:/CoRN/ftc/MoreIntegrals/More_Properties/F.var
253 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab.var
257 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac.var
261 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb.var
265 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc.var
272 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ab.con" "More_Properties__" as definition.
274 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ac.con" "More_Properties__" as definition.
276 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_cb.con" "More_Properties__" as definition.
278 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_a.con" "More_Properties__" as definition.
280 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_b.con" "More_Properties__" as definition.
282 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_c.con" "More_Properties__" as definition.
284 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_a.con" "More_Properties__" as definition.
286 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_c.con" "More_Properties__" as definition.
288 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_a.con" "More_Properties__" as definition.
290 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_b.con" "More_Properties__" as definition.
292 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_b.con" "More_Properties__" as definition.
294 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_c.con" "More_Properties__" as definition.
296 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_abc.con" "More_Properties__" as definition.
298 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ab.con" "More_Properties__" as definition.
300 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ac.con" "More_Properties__" as definition.
302 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_cb.con" "More_Properties__" as definition.
304 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_a.con" "More_Properties__" as definition.
306 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_b.con" "More_Properties__" as definition.
308 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_c.con" "More_Properties__" as definition.
312 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con" as lemma.
315 Notice that, unlike in the classical case, an extra hypothesis (the
316 continuity of [F] in the interval [[Min(a,b,c),Max(a,b,c)]]) must be assumed.
328 cic:/CoRN/ftc/MoreIntegrals/Corollaries/a.var
332 cic:/CoRN/ftc/MoreIntegrals/Corollaries/b.var
336 cic:/CoRN/ftc/MoreIntegrals/Corollaries/Hab.var
340 cic:/CoRN/ftc/MoreIntegrals/Corollaries/F.var
344 cic:/CoRN/ftc/MoreIntegrals/Corollaries/contF.var
347 (*#* As a corollary, we get the following rule: *)
349 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con" as lemma.
351 (*#* Finally, some miscellaneous results: *)
353 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con" as lemma.
355 inline procedural "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con" as lemma.
361 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con" as lemma.
363 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con" as lemma.