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.
49 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/a.var".
51 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/b.var".
53 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/Hab.var".
55 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con".
57 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con".
68 The integral is defined by the formula
69 $\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#,
70 inspired by the domain union rule; obviously it coincides with the
71 classical definition, and it collapses to the old one in the case [a
75 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/a.var".
77 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/b.var".
79 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/Hab.var".
81 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/F.var".
83 alias id "HF" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/HF.var".
85 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con".
87 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con".
89 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral.con".
91 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con".
98 Implicit Arguments Integral [a b Hab F].
102 Section Properties_of_Integral
105 (*#* **Properties of the Integral
107 All our old properties carry over to this new definition---and some
108 new ones, too. We begin with (strong) extensionality.
111 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/a.var".
113 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/b.var".
115 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/Hab.var".
117 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/F.var".
119 alias id "G" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/G.var".
121 alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contF.var".
123 alias id "contG" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contG.var".
125 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con".
127 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con".
129 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con".
131 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con".
134 The integral is a linear operator.
137 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con".
139 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con".
141 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con".
143 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con".
145 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con".
147 inline procedural "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con".
150 If the endpoints are equal then the integral vanishes.
153 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con".
156 And the norm provides an upper bound for the absolute value of the integral.
159 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con".
162 End Properties_of_Integral
166 Section More_Properties
170 Two other ways of stating the addition law for domains.
173 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con".
175 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con".
178 And now we can prove the addition law for domains with our general operator.
180 %\begin{convention}% Assume [c : IR].
184 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/a.var".
186 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/b.var".
188 alias id "c" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/c.var".
192 alias id "Hab'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab'.var".
194 alias id "Hac'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac'.var".
196 alias id "Hcb'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb'.var".
198 alias id "Habc'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc'.var".
202 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/F.var".
206 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab.var".
208 alias id "Hac" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac.var".
210 alias id "Hcb" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb.var".
212 alias id "Habc" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc.var".
218 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ab.con" "More_Properties__".
220 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ac.con" "More_Properties__".
222 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_cb.con" "More_Properties__".
224 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_a.con" "More_Properties__".
226 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_b.con" "More_Properties__".
228 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_c.con" "More_Properties__".
230 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_a.con" "More_Properties__".
232 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_c.con" "More_Properties__".
234 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_a.con" "More_Properties__".
236 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_b.con" "More_Properties__".
238 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_b.con" "More_Properties__".
240 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_c.con" "More_Properties__".
242 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_abc.con" "More_Properties__".
244 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ab.con" "More_Properties__".
246 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ac.con" "More_Properties__".
248 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_cb.con" "More_Properties__".
250 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_a.con" "More_Properties__".
252 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_b.con" "More_Properties__".
254 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_c.con" "More_Properties__".
258 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con".
261 Notice that, unlike in the classical case, an extra hypothesis (the
262 continuity of [F] in the interval [[Min(a,b,c),Max(a,b,c)]]) must be assumed.
273 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/a.var".
275 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/b.var".
277 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/Hab.var".
279 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/F.var".
281 alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/contF.var".
283 (*#* As a corollary, we get the following rule: *)
285 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con".
287 (*#* Finally, some miscellaneous results: *)
289 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con".
291 inline procedural "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con".
297 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con".
299 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con".