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: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
21 include "ftc/MoreFunctions.ma".
24 Section Maps_into_Compacts
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
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.
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.
54 alias id "F" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var".
56 alias id "G" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var".
58 alias id "a" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var".
60 alias id "b" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var".
62 alias id "Hab" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var".
64 alias id "c" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var".
66 alias id "d" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var".
68 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var".
72 inline procedural "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__" as definition.
78 alias id "Hf" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var".
82 inline procedural "cic:/CoRN/ftc/Composition/maps_into_compacts.con" as definition.
86 alias id "maps" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.var".
90 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma'.con" as lemma.
92 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma.con" as lemma.
94 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_less.con" as lemma.
96 inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_inc.con" as lemma.
103 End Maps_into_Compacts
111 As was the case for division of partial functions, this condition
112 completely characterizes the domain of the composite function.
115 alias id "F" = "cic:/CoRN/ftc/Composition/Mapping/F.var".
117 alias id "G" = "cic:/CoRN/ftc/Composition/Mapping/G.var".
119 alias id "a" = "cic:/CoRN/ftc/Composition/Mapping/a.var".
121 alias id "b" = "cic:/CoRN/ftc/Composition/Mapping/b.var".
123 alias id "Hab" = "cic:/CoRN/ftc/Composition/Mapping/Hab.var".
125 alias id "c" = "cic:/CoRN/ftc/Composition/Mapping/c.var".
127 alias id "d" = "cic:/CoRN/ftc/Composition/Mapping/d.var".
129 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Mapping/Hcd.var".
133 alias id "Hf" = "cic:/CoRN/ftc/Composition/Mapping/Hf.var".
135 alias id "Hg" = "cic:/CoRN/ftc/Composition/Mapping/Hg.var".
137 alias id "maps" = "cic:/CoRN/ftc/Composition/Mapping/maps.var".
141 inline procedural "cic:/CoRN/ftc/Composition/included_comp.con" as lemma.
148 Section Interval_Continuity
153 We now prove that the composition of two continuous partial functions is continuous.
156 alias id "a" = "cic:/CoRN/ftc/Composition/Interval_Continuity/a.var".
158 alias id "b" = "cic:/CoRN/ftc/Composition/Interval_Continuity/b.var".
160 alias id "Hab" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var".
164 inline procedural "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__" as definition.
168 alias id "c" = "cic:/CoRN/ftc/Composition/Interval_Continuity/c.var".
170 alias id "d" = "cic:/CoRN/ftc/Composition/Interval_Continuity/d.var".
172 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var".
174 alias id "F" = "cic:/CoRN/ftc/Composition/Interval_Continuity/F.var".
176 alias id "G" = "cic:/CoRN/ftc/Composition/Interval_Continuity/G.var".
180 alias id "contF" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var".
182 alias id "contG" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var".
184 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var".
188 inline procedural "cic:/CoRN/ftc/Composition/Continuous_I_comp.con" as lemma.
191 End Interval_Continuity
200 We now work with the derivative relation and prove the chain rule for partial functions.
203 alias id "F" = "cic:/CoRN/ftc/Composition/Derivative/F.var".
205 alias id "F'" = "cic:/CoRN/ftc/Composition/Derivative/F'.var".
207 alias id "G" = "cic:/CoRN/ftc/Composition/Derivative/G.var".
209 alias id "G'" = "cic:/CoRN/ftc/Composition/Derivative/G'.var".
211 alias id "a" = "cic:/CoRN/ftc/Composition/Derivative/a.var".
213 alias id "b" = "cic:/CoRN/ftc/Composition/Derivative/b.var".
215 alias id "Hab'" = "cic:/CoRN/ftc/Composition/Derivative/Hab'.var".
217 alias id "c" = "cic:/CoRN/ftc/Composition/Derivative/c.var".
219 alias id "d" = "cic:/CoRN/ftc/Composition/Derivative/d.var".
221 alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var".
225 inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__" as definition.
227 inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__" as definition.
229 inline procedural "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__" as definition.
235 alias id "derF" = "cic:/CoRN/ftc/Composition/Derivative/derF.var".
237 alias id "derG" = "cic:/CoRN/ftc/Composition/Derivative/derG.var".
239 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Derivative/Hmap.var".
243 inline procedural "cic:/CoRN/ftc/Composition/included_comp'.con" as lemma.
245 inline procedural "cic:/CoRN/ftc/Composition/maps'.con" as lemma.
247 inline procedural "cic:/CoRN/ftc/Composition/Derivative_I_comp.con" as lemma.
250 The next lemma will be useful when we move on to differentiability.
253 inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con" as lemma.
260 Section Differentiability
263 (*#* **Differentiability
265 Finally, we move on to differentiability.
268 alias id "F" = "cic:/CoRN/ftc/Composition/Differentiability/F.var".
270 alias id "G" = "cic:/CoRN/ftc/Composition/Differentiability/G.var".
272 alias id "a" = "cic:/CoRN/ftc/Composition/Differentiability/a.var".
274 alias id "b" = "cic:/CoRN/ftc/Composition/Differentiability/b.var".
276 alias id "Hab'" = "cic:/CoRN/ftc/Composition/Differentiability/Hab'.var".
278 alias id "c" = "cic:/CoRN/ftc/Composition/Differentiability/c.var".
280 alias id "d" = "cic:/CoRN/ftc/Composition/Differentiability/d.var".
282 alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var".
286 inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__" as definition.
288 inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__" as definition.
290 inline procedural "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__" as definition.
296 alias id "diffF" = "cic:/CoRN/ftc/Composition/Differentiability/diffF.var".
298 alias id "diffG" = "cic:/CoRN/ftc/Composition/Differentiability/diffG.var".
300 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Differentiability/Hmap.var".
304 inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp.con" as lemma.
307 End Differentiability
311 Section Generalized_Intervals
314 (*#* **Generalizations
316 We now generalize this results to arbitrary intervals. We begin by generalizing the notion of mapping compacts into compacts.
318 %\begin{convention}% We assume [I,J] to be proper intervals.
322 alias id "I" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var".
324 alias id "J" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var".
326 alias id "pI" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var".
328 alias id "pJ" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var".
330 inline procedural "cic:/CoRN/ftc/Composition/maps_compacts_into.con" as definition.
333 Now everything comes naturally:
336 inline procedural "cic:/CoRN/ftc/Composition/comp_inc_lemma.con" as lemma.
338 alias id "F" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var".
340 alias id "F'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var".
342 alias id "G" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var".
344 alias id "G'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var".
348 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var".
352 inline procedural "cic:/CoRN/ftc/Composition/Continuous_comp.con" as lemma.
356 alias id "Hmap'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var".
360 inline procedural "cic:/CoRN/ftc/Composition/Derivative_comp.con" as lemma.
363 End Generalized_Intervals
371 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
374 inline procedural "cic:/CoRN/ftc/Composition/positive_fun.con" as definition.
376 inline procedural "cic:/CoRN/ftc/Composition/negative_fun.con" as definition.
378 inline procedural "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con" as lemma.
380 inline procedural "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con" as lemma.
382 inline procedural "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con" as lemma.
385 As a corollary, we get the generalization of differentiability property.
388 inline procedural "cic:/CoRN/ftc/Composition/Diffble_comp.con" as lemma.
395 Hint Immediate included_comp: included.
399 Hint Immediate Continuous_I_comp Continuous_comp: continuous.