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/MoreIntegrals".
21 (* $Id: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
23 include "ftc/Integral.ma".
25 include "ftc/MoreFunctions.ma".
31 (*#* printing Integral %\ensuremath{\int}% #∫# *)
33 (*#* printing integral' %\ensuremath{\int}% #∫# *)
35 (*#* *The generalized integral
37 In this file we extend the definition of integral to allow for
38 arbitrary integration domains (that is, not requiring that the lower
39 endpoint of integration be less or equal than the upper endpoint) and
40 we prove the fundamental properties of the new operator.
42 %\begin{convention}% Let [a, b : IR] and assume that [F] and [G] are two
43 partial functions continuous in [[Min(a,b),Max(a,b)]].
48 Before we define the new integral we need to some trivial interval inclusions.
51 inline "cic:/CoRN/ftc/MoreIntegrals/a.var".
53 inline "cic:/CoRN/ftc/MoreIntegrals/b.var".
55 inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var".
57 inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con".
59 inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con".
70 The integral is defined by the formula
71 $\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#,
72 inspired by the domain union rule; obviously it coincides with the
73 classical definition, and it collapses to the old one in the case [a
77 inline "cic:/CoRN/ftc/MoreIntegrals/a.var".
79 inline "cic:/CoRN/ftc/MoreIntegrals/b.var".
81 inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var".
83 inline "cic:/CoRN/ftc/MoreIntegrals/F.var".
85 inline "cic:/CoRN/ftc/MoreIntegrals/HF.var".
87 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con".
89 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con".
91 inline "cic:/CoRN/ftc/MoreIntegrals/Integral.con".
93 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con".
100 Implicit Arguments Integral [a b Hab F].
104 Section Properties_of_Integral.
107 (*#* **Properties of the Integral
109 All our old properties carry over to this new definition---and some
110 new ones, too. We begin with (strong) extensionality.
113 inline "cic:/CoRN/ftc/MoreIntegrals/a.var".
115 inline "cic:/CoRN/ftc/MoreIntegrals/b.var".
117 inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var".
119 inline "cic:/CoRN/ftc/MoreIntegrals/F.var".
121 inline "cic:/CoRN/ftc/MoreIntegrals/G.var".
123 inline "cic:/CoRN/ftc/MoreIntegrals/contF.var".
125 inline "cic:/CoRN/ftc/MoreIntegrals/contG.var".
127 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con".
129 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con".
131 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con".
133 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con".
136 The integral is a linear operator.
139 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con".
141 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con".
143 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con".
145 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con".
147 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con".
149 inline "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con".
152 If the endpoints are equal then the integral vanishes.
155 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con".
158 And the norm provides an upper bound for the absolute value of the integral.
161 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con".
164 End Properties_of_Integral.
168 Section More_Properties.
172 Two other ways of stating the addition law for domains.
175 inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con".
177 inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con".
180 And now we can prove the addition law for domains with our general operator.
182 %\begin{convention}% Assume [c : IR].
186 inline "cic:/CoRN/ftc/MoreIntegrals/a.var".
188 inline "cic:/CoRN/ftc/MoreIntegrals/b.var".
190 inline "cic:/CoRN/ftc/MoreIntegrals/c.var".
194 inline "cic:/CoRN/ftc/MoreIntegrals/Hab'.var".
196 inline "cic:/CoRN/ftc/MoreIntegrals/Hac'.var".
198 inline "cic:/CoRN/ftc/MoreIntegrals/Hcb'.var".
200 inline "cic:/CoRN/ftc/MoreIntegrals/Habc'.var".
204 inline "cic:/CoRN/ftc/MoreIntegrals/F.var".
208 inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var".
210 inline "cic:/CoRN/ftc/MoreIntegrals/Hac.var".
212 inline "cic:/CoRN/ftc/MoreIntegrals/Hcb.var".
214 inline "cic:/CoRN/ftc/MoreIntegrals/Habc.var".
220 inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_ab.con".
222 inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_ac.con".
224 inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_cb.con".
226 inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_a.con".
228 inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_b.con".
230 inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_c.con".
232 inline "cic:/CoRN/ftc/MoreIntegrals/le_ab_a.con".
234 inline "cic:/CoRN/ftc/MoreIntegrals/le_cb_c.con".
236 inline "cic:/CoRN/ftc/MoreIntegrals/le_ac_a.con".
238 inline "cic:/CoRN/ftc/MoreIntegrals/le_ab_b.con".
240 inline "cic:/CoRN/ftc/MoreIntegrals/le_cb_b.con".
242 inline "cic:/CoRN/ftc/MoreIntegrals/le_ac_c.con".
244 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_abc.con".
246 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_ab.con".
248 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_ac.con".
250 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_cb.con".
252 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_a.con".
254 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_b.con".
256 inline "cic:/CoRN/ftc/MoreIntegrals/Habc_c.con".
260 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con".
263 Notice that, unlike in the classical case, an extra hypothesis (the
264 continuity of [F] in the interval [[Min(a,b,c),Max(a,b,c)]]) must be assumed.
275 inline "cic:/CoRN/ftc/MoreIntegrals/a.var".
277 inline "cic:/CoRN/ftc/MoreIntegrals/b.var".
279 inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var".
281 inline "cic:/CoRN/ftc/MoreIntegrals/F.var".
283 inline "cic:/CoRN/ftc/MoreIntegrals/contF.var".
285 (*#* As a corollary, we get the following rule: *)
287 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con".
289 (*#* Finally, some miscellaneous results: *)
291 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con".
293 inline "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con".
299 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con".
301 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con".