]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/Composition.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / Composition.mma
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 include "CoRN.ma".
18
19 (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
20
21 include "ftc/MoreFunctions.ma".
22
23 (* UNEXPORTED
24 Section Maps_into_Compacts
25 *)
26
27 (* UNEXPORTED
28 Section Part_Funct
29 *)
30
31 (*#* *Composition
32
33 Preservation results for functional composition are treated in this
34 separate file.  We start by defining some auxiliary predicates, and
35 then prove the preservation of continuity through composition and the
36 chain rule for differentiation, both for compact and arbitrary
37 intervals.
38
39 %\begin{convention}% Throughout this section:
40 - [a, b : IR] and [I] will denote [[a,b]];
41 - [c, d : IR] and [J] will denote [[c,d]];
42 - [F, F', G, G'] will be partial functions.
43
44 %\end{convention}%
45
46 ** Maps into Compacts
47
48 Both continuity and differentiability proofs require extra hypothesis
49 on the functions involved---namely, that every compact interval is
50 mapped into another compact interval.  We define this concept for
51 partial functions, and prove some trivial results.
52 *)
53
54 (* UNEXPORTED
55 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var
56 *)
57
58 (* UNEXPORTED
59 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var
60 *)
61
62 (* UNEXPORTED
63 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var
64 *)
65
66 (* UNEXPORTED
67 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var
68 *)
69
70 (* UNEXPORTED
71 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var
72 *)
73
74 (* UNEXPORTED
75 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var
76 *)
77
78 (* UNEXPORTED
79 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var
80 *)
81
82 (* UNEXPORTED
83 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var
84 *)
85
86 (* begin hide *)
87
88 inline procedural "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__" as definition.
89
90 (* end hide *)
91
92 (* begin show *)
93
94 (* UNEXPORTED
95 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var
96 *)
97
98 (* end show *)
99
100 inline procedural "cic:/CoRN/ftc/Composition/maps_into_compacts.con" as definition.
101
102 (* begin show *)
103
104 (* UNEXPORTED
105 cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.var
106 *)
107
108 (* end show *)
109
110 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma'.con" as lemma.
111
112 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma.con" as lemma.
113
114 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_less.con" as lemma.
115
116 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_inc.con" as lemma.
117
118 (* UNEXPORTED
119 End Part_Funct
120 *)
121
122 (* UNEXPORTED
123 End Maps_into_Compacts
124 *)
125
126 (* UNEXPORTED
127 Section Mapping
128 *)
129
130 (*#*
131 As was the case for division of partial functions, this condition
132 completely characterizes the domain of the composite function.
133 *)
134
135 (* UNEXPORTED
136 cic:/CoRN/ftc/Composition/Mapping/F.var
137 *)
138
139 (* UNEXPORTED
140 cic:/CoRN/ftc/Composition/Mapping/G.var
141 *)
142
143 (* UNEXPORTED
144 cic:/CoRN/ftc/Composition/Mapping/a.var
145 *)
146
147 (* UNEXPORTED
148 cic:/CoRN/ftc/Composition/Mapping/b.var
149 *)
150
151 (* UNEXPORTED
152 cic:/CoRN/ftc/Composition/Mapping/Hab.var
153 *)
154
155 (* UNEXPORTED
156 cic:/CoRN/ftc/Composition/Mapping/c.var
157 *)
158
159 (* UNEXPORTED
160 cic:/CoRN/ftc/Composition/Mapping/d.var
161 *)
162
163 (* UNEXPORTED
164 cic:/CoRN/ftc/Composition/Mapping/Hcd.var
165 *)
166
167 (* begin show *)
168
169 (* UNEXPORTED
170 cic:/CoRN/ftc/Composition/Mapping/Hf.var
171 *)
172
173 (* UNEXPORTED
174 cic:/CoRN/ftc/Composition/Mapping/Hg.var
175 *)
176
177 (* UNEXPORTED
178 cic:/CoRN/ftc/Composition/Mapping/maps.var
179 *)
180
181 (* end show *)
182
183 inline procedural "cic:/CoRN/ftc/Composition/included_comp.con" as lemma.
184
185 (* UNEXPORTED
186 End Mapping
187 *)
188
189 (* UNEXPORTED
190 Section Interval_Continuity
191 *)
192
193 (*#* **Continuity
194
195 We now prove that the composition of two continuous partial functions is continuous.
196 *)
197
198 (* UNEXPORTED
199 cic:/CoRN/ftc/Composition/Interval_Continuity/a.var
200 *)
201
202 (* UNEXPORTED
203 cic:/CoRN/ftc/Composition/Interval_Continuity/b.var
204 *)
205
206 (* UNEXPORTED
207 cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var
208 *)
209
210 (* begin hide *)
211
212 inline procedural "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__" as definition.
213
214 (* end hide *)
215
216 (* UNEXPORTED
217 cic:/CoRN/ftc/Composition/Interval_Continuity/c.var
218 *)
219
220 (* UNEXPORTED
221 cic:/CoRN/ftc/Composition/Interval_Continuity/d.var
222 *)
223
224 (* UNEXPORTED
225 cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var
226 *)
227
228 (* UNEXPORTED
229 cic:/CoRN/ftc/Composition/Interval_Continuity/F.var
230 *)
231
232 (* UNEXPORTED
233 cic:/CoRN/ftc/Composition/Interval_Continuity/G.var
234 *)
235
236 (* begin show *)
237
238 (* UNEXPORTED
239 cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var
240 *)
241
242 (* UNEXPORTED
243 cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var
244 *)
245
246 (* UNEXPORTED
247 cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var
248 *)
249
250 (* end show *)
251
252 inline procedural "cic:/CoRN/ftc/Composition/Continuous_I_comp.con" as lemma.
253
254 (* UNEXPORTED
255 End Interval_Continuity
256 *)
257
258 (* UNEXPORTED
259 Section Derivative
260 *)
261
262 (*#* **Derivative
263
264 We now work with the derivative relation and prove the chain rule for partial functions.
265 *)
266
267 (* UNEXPORTED
268 cic:/CoRN/ftc/Composition/Derivative/F.var
269 *)
270
271 (* UNEXPORTED
272 cic:/CoRN/ftc/Composition/Derivative/F'.var
273 *)
274
275 (* UNEXPORTED
276 cic:/CoRN/ftc/Composition/Derivative/G.var
277 *)
278
279 (* UNEXPORTED
280 cic:/CoRN/ftc/Composition/Derivative/G'.var
281 *)
282
283 (* UNEXPORTED
284 cic:/CoRN/ftc/Composition/Derivative/a.var
285 *)
286
287 (* UNEXPORTED
288 cic:/CoRN/ftc/Composition/Derivative/b.var
289 *)
290
291 (* UNEXPORTED
292 cic:/CoRN/ftc/Composition/Derivative/Hab'.var
293 *)
294
295 (* UNEXPORTED
296 cic:/CoRN/ftc/Composition/Derivative/c.var
297 *)
298
299 (* UNEXPORTED
300 cic:/CoRN/ftc/Composition/Derivative/d.var
301 *)
302
303 (* UNEXPORTED
304 cic:/CoRN/ftc/Composition/Derivative/Hcd'.var
305 *)
306
307 (* begin hide *)
308
309 inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__" as definition.
310
311 inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__" as definition.
312
313 inline procedural "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__" as definition.
314
315 (* end hide *)
316
317 (* begin show *)
318
319 (* UNEXPORTED
320 cic:/CoRN/ftc/Composition/Derivative/derF.var
321 *)
322
323 (* UNEXPORTED
324 cic:/CoRN/ftc/Composition/Derivative/derG.var
325 *)
326
327 (* UNEXPORTED
328 cic:/CoRN/ftc/Composition/Derivative/Hmap.var
329 *)
330
331 (* end show *)
332
333 inline procedural "cic:/CoRN/ftc/Composition/included_comp'.con" as lemma.
334
335 inline procedural "cic:/CoRN/ftc/Composition/maps'.con" as lemma.
336
337 inline procedural "cic:/CoRN/ftc/Composition/Derivative_I_comp.con" as lemma.
338
339 (*#*
340 The next lemma will be useful when we move on to differentiability.
341 *)
342
343 inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con" as lemma.
344
345 (* UNEXPORTED
346 End Derivative
347 *)
348
349 (* UNEXPORTED
350 Section Differentiability
351 *)
352
353 (*#* **Differentiability
354
355 Finally, we move on to differentiability.
356 *)
357
358 (* UNEXPORTED
359 cic:/CoRN/ftc/Composition/Differentiability/F.var
360 *)
361
362 (* UNEXPORTED
363 cic:/CoRN/ftc/Composition/Differentiability/G.var
364 *)
365
366 (* UNEXPORTED
367 cic:/CoRN/ftc/Composition/Differentiability/a.var
368 *)
369
370 (* UNEXPORTED
371 cic:/CoRN/ftc/Composition/Differentiability/b.var
372 *)
373
374 (* UNEXPORTED
375 cic:/CoRN/ftc/Composition/Differentiability/Hab'.var
376 *)
377
378 (* UNEXPORTED
379 cic:/CoRN/ftc/Composition/Differentiability/c.var
380 *)
381
382 (* UNEXPORTED
383 cic:/CoRN/ftc/Composition/Differentiability/d.var
384 *)
385
386 (* UNEXPORTED
387 cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var
388 *)
389
390 (* begin hide *)
391
392 inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__" as definition.
393
394 inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__" as definition.
395
396 inline procedural "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__" as definition.
397
398 (* end hide *)
399
400 (* begin show *)
401
402 (* UNEXPORTED
403 cic:/CoRN/ftc/Composition/Differentiability/diffF.var
404 *)
405
406 (* UNEXPORTED
407 cic:/CoRN/ftc/Composition/Differentiability/diffG.var
408 *)
409
410 (* UNEXPORTED
411 cic:/CoRN/ftc/Composition/Differentiability/Hmap.var
412 *)
413
414 (* end show *)
415
416 inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp.con" as lemma.
417
418 (* UNEXPORTED
419 End Differentiability
420 *)
421
422 (* UNEXPORTED
423 Section Generalized_Intervals
424 *)
425
426 (*#* **Generalizations
427
428 We now generalize this results to arbitrary intervals.  We begin by generalizing the notion of mapping compacts into compacts.
429
430 %\begin{convention}% We assume [I,J] to be proper intervals.
431 %\end{convention}%
432 *)
433
434 (* UNEXPORTED
435 cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var
436 *)
437
438 (* UNEXPORTED
439 cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var
440 *)
441
442 (* UNEXPORTED
443 cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var
444 *)
445
446 (* UNEXPORTED
447 cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var
448 *)
449
450 inline procedural "cic:/CoRN/ftc/Composition/maps_compacts_into.con" as definition.
451
452 (*#*
453 Now everything comes naturally:
454 *)
455
456 inline procedural "cic:/CoRN/ftc/Composition/comp_inc_lemma.con" as lemma.
457
458 (* UNEXPORTED
459 cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var
460 *)
461
462 (* UNEXPORTED
463 cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var
464 *)
465
466 (* UNEXPORTED
467 cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var
468 *)
469
470 (* UNEXPORTED
471 cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var
472 *)
473
474 (* begin show *)
475
476 (* UNEXPORTED
477 cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var
478 *)
479
480 (* end show *)
481
482 inline procedural "cic:/CoRN/ftc/Composition/Continuous_comp.con" as lemma.
483
484 (* begin show *)
485
486 (* UNEXPORTED
487 cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var
488 *)
489
490 (* end show *)
491
492 inline procedural "cic:/CoRN/ftc/Composition/Derivative_comp.con" as lemma.
493
494 (* UNEXPORTED
495 End Generalized_Intervals
496 *)
497
498 (* UNEXPORTED
499 Section Corollaries
500 *)
501
502 (*#*
503 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
504 *)
505
506 inline procedural "cic:/CoRN/ftc/Composition/positive_fun.con" as definition.
507
508 inline procedural "cic:/CoRN/ftc/Composition/negative_fun.con" as definition.
509
510 inline procedural "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con" as lemma.
511
512 inline procedural "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con" as lemma.
513
514 inline procedural "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con" as lemma.
515
516 (*#*
517 As a corollary, we get the generalization of differentiability property.
518 *)
519
520 inline procedural "cic:/CoRN/ftc/Composition/Diffble_comp.con" as lemma.
521
522 (* UNEXPORTED
523 End Corollaries
524 *)
525
526 (* UNEXPORTED
527 Hint Immediate included_comp: included.
528 *)
529
530 (* UNEXPORTED
531 Hint Immediate Continuous_I_comp Continuous_comp: continuous.
532 *)
533