]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / MoreIntegrals.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntegrals".
18
19 include "CoRN.ma".
20
21 (* $Id: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
22
23 include "ftc/Integral.ma".
24
25 include "ftc/MoreFunctions.ma".
26
27 (* UNEXPORTED
28 Section Lemmas
29 *)
30
31 (*#* printing Integral %\ensuremath{\int}% #∫# *)
32
33 (*#* printing integral' %\ensuremath{\int}% #∫# *)
34
35 (*#* *The generalized integral
36
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.
41
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)]].
44 %\end{convention}%
45
46 ** Definitions
47
48 Before we define the new integral we need to some trivial interval inclusions.
49 *)
50
51 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/a.var".
52
53 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/b.var".
54
55 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/Hab.var".
56
57 inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con".
58
59 inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con".
60
61 (* UNEXPORTED
62 End Lemmas
63 *)
64
65 (* UNEXPORTED
66 Section Definitions
67 *)
68
69 (*#*
70 The integral is defined by the formula
71 $\int_a^bf=\int_{\min(a,b)}^bf-\int_{\min(a,b)}^af$#&int;<sub>a</sub><sup>b</sup>f=&int;<sub>min(a,b)</sub><sup>b</sup>f-&int;<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
74  [<=]  b].
75 *)
76
77 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/a.var".
78
79 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/b.var".
80
81 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/Hab.var".
82
83 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/F.var".
84
85 alias id "HF" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/HF.var".
86
87 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con".
88
89 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con".
90
91 inline "cic:/CoRN/ftc/MoreIntegrals/Integral.con".
92
93 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con".
94
95 (* UNEXPORTED
96 End Definitions
97 *)
98
99 (* UNEXPORTED
100 Implicit Arguments Integral [a b Hab F].
101 *)
102
103 (* UNEXPORTED
104 Section Properties_of_Integral
105 *)
106
107 (*#* **Properties of the Integral
108
109 All our old properties carry over to this new definition---and some
110 new ones, too.  We begin with (strong) extensionality.
111 *)
112
113 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/a.var".
114
115 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/b.var".
116
117 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/Hab.var".
118
119 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/F.var".
120
121 alias id "G" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/G.var".
122
123 alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contF.var".
124
125 alias id "contG" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contG.var".
126
127 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con".
128
129 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con".
130
131 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con".
132
133 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con".
134
135 (*#*
136 The integral is a linear operator.
137 *)
138
139 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con".
140
141 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con".
142
143 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con".
144
145 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con".
146
147 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con".
148
149 inline "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con".
150
151 (*#*
152 If the endpoints are equal then the integral vanishes.
153 *)
154
155 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con".
156
157 (*#*
158 And the norm provides an upper bound for the absolute value of the integral.
159 *)
160
161 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con".
162
163 (* UNEXPORTED
164 End Properties_of_Integral
165 *)
166
167 (* UNEXPORTED
168 Section More_Properties
169 *)
170
171 (*#*
172 Two other ways of stating the addition law for domains.
173 *)
174
175 inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con".
176
177 inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con".
178
179 (*#*
180 And now we can prove the addition law for domains with our general operator.
181
182 %\begin{convention}% Assume [c : IR].
183 %\end{convention}%
184 *)
185
186 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/a.var".
187
188 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/b.var".
189
190 alias id "c" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/c.var".
191
192 (* begin show *)
193
194 alias id "Hab'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab'.var".
195
196 alias id "Hac'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac'.var".
197
198 alias id "Hcb'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb'.var".
199
200 alias id "Habc'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc'.var".
201
202 (* end show *)
203
204 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/F.var".
205
206 (* begin show *)
207
208 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab.var".
209
210 alias id "Hac" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac.var".
211
212 alias id "Hcb" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb.var".
213
214 alias id "Habc" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc.var".
215
216 (* end show *)
217
218 (* begin hide *)
219
220 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ab.con" "More_Properties__".
221
222 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ac.con" "More_Properties__".
223
224 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_cb.con" "More_Properties__".
225
226 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_a.con" "More_Properties__".
227
228 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_b.con" "More_Properties__".
229
230 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_c.con" "More_Properties__".
231
232 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_a.con" "More_Properties__".
233
234 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_c.con" "More_Properties__".
235
236 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_a.con" "More_Properties__".
237
238 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_b.con" "More_Properties__".
239
240 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_b.con" "More_Properties__".
241
242 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_c.con" "More_Properties__".
243
244 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_abc.con" "More_Properties__".
245
246 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ab.con" "More_Properties__".
247
248 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ac.con" "More_Properties__".
249
250 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_cb.con" "More_Properties__".
251
252 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_a.con" "More_Properties__".
253
254 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_b.con" "More_Properties__".
255
256 inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_c.con" "More_Properties__".
257
258 (* end hide *)
259
260 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con".
261
262 (*#*
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.
265 *)
266
267 (* UNEXPORTED
268 End More_Properties
269 *)
270
271 (* UNEXPORTED
272 Section Corollaries
273 *)
274
275 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/a.var".
276
277 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/b.var".
278
279 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/Hab.var".
280
281 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/F.var".
282
283 alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/contF.var".
284
285 (*#* As a corollary, we get the following rule: *)
286
287 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con".
288
289 (*#* Finally, some miscellaneous results: *)
290
291 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con".
292
293 inline "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con".
294
295 (* UNEXPORTED
296 End Corollaries
297 *)
298
299 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con".
300
301 inline "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con".
302