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/Composition".
19 (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
26 Section Maps_into_Compacts.
35 Preservation results for functional composition are treated in this
36 separate file. We start by defining some auxiliary predicates, and
37 then prove the preservation of continuity through composition and the
38 chain rule for differentiation, both for compact and arbitrary
41 %\begin{convention}% Throughout this section:
42 - [a, b : IR] and [I] will denote [[a,b]];
43 - [c, d : IR] and [J] will denote [[c,d]];
44 - [F, F', G, G'] will be partial functions.
50 Both continuity and differentiability proofs require extra hypothesis
51 on the functions involved---namely, that every compact interval is
52 mapped into another compact interval. We define this concept for
53 partial functions, and prove some trivial results.
56 inline cic:/CoRN/ftc/Composition/F.var.
58 inline cic:/CoRN/ftc/Composition/G.var.
60 inline cic:/CoRN/ftc/Composition/a.var.
62 inline cic:/CoRN/ftc/Composition/b.var.
64 inline cic:/CoRN/ftc/Composition/Hab.var.
66 inline cic:/CoRN/ftc/Composition/c.var.
68 inline cic:/CoRN/ftc/Composition/d.var.
70 inline cic:/CoRN/ftc/Composition/Hcd.var.
74 inline cic:/CoRN/ftc/Composition/I.con.
80 inline cic:/CoRN/ftc/Composition/Hf.var.
84 inline cic:/CoRN/ftc/Composition/maps_into_compacts.con.
88 inline cic:/CoRN/ftc/Composition/maps.var.
92 inline cic:/CoRN/ftc/Composition/maps_lemma'.con.
94 inline cic:/CoRN/ftc/Composition/maps_lemma.con.
96 inline cic:/CoRN/ftc/Composition/maps_lemma_less.con.
98 inline cic:/CoRN/ftc/Composition/maps_lemma_inc.con.
105 End Maps_into_Compacts.
113 As was the case for division of partial functions, this condition
114 completely characterizes the domain of the composite function.
117 inline cic:/CoRN/ftc/Composition/F.var.
119 inline cic:/CoRN/ftc/Composition/G.var.
121 inline cic:/CoRN/ftc/Composition/a.var.
123 inline cic:/CoRN/ftc/Composition/b.var.
125 inline cic:/CoRN/ftc/Composition/Hab.var.
127 inline cic:/CoRN/ftc/Composition/c.var.
129 inline cic:/CoRN/ftc/Composition/d.var.
131 inline cic:/CoRN/ftc/Composition/Hcd.var.
135 inline cic:/CoRN/ftc/Composition/Hf.var.
137 inline cic:/CoRN/ftc/Composition/Hg.var.
139 inline cic:/CoRN/ftc/Composition/maps.var.
143 inline cic:/CoRN/ftc/Composition/included_comp.con.
150 Section Interval_Continuity.
155 We now prove that the composition of two continuous partial functions is continuous.
158 inline cic:/CoRN/ftc/Composition/a.var.
160 inline cic:/CoRN/ftc/Composition/b.var.
162 inline cic:/CoRN/ftc/Composition/Hab.var.
166 inline cic:/CoRN/ftc/Composition/I.con.
170 inline cic:/CoRN/ftc/Composition/c.var.
172 inline cic:/CoRN/ftc/Composition/d.var.
174 inline cic:/CoRN/ftc/Composition/Hcd.var.
176 inline cic:/CoRN/ftc/Composition/F.var.
178 inline cic:/CoRN/ftc/Composition/G.var.
182 inline cic:/CoRN/ftc/Composition/contF.var.
184 inline cic:/CoRN/ftc/Composition/contG.var.
186 inline cic:/CoRN/ftc/Composition/Hmap.var.
190 inline cic:/CoRN/ftc/Composition/Continuous_I_comp.con.
193 End Interval_Continuity.
202 We now work with the derivative relation and prove the chain rule for partial functions.
205 inline cic:/CoRN/ftc/Composition/F.var.
207 inline cic:/CoRN/ftc/Composition/F'.var.
209 inline cic:/CoRN/ftc/Composition/G.var.
211 inline cic:/CoRN/ftc/Composition/G'.var.
213 inline cic:/CoRN/ftc/Composition/a.var.
215 inline cic:/CoRN/ftc/Composition/b.var.
217 inline cic:/CoRN/ftc/Composition/Hab'.var.
219 inline cic:/CoRN/ftc/Composition/c.var.
221 inline cic:/CoRN/ftc/Composition/d.var.
223 inline cic:/CoRN/ftc/Composition/Hcd'.var.
227 inline cic:/CoRN/ftc/Composition/Hab.con.
229 inline cic:/CoRN/ftc/Composition/Hcd.con.
231 inline cic:/CoRN/ftc/Composition/I.con.
237 inline cic:/CoRN/ftc/Composition/derF.var.
239 inline cic:/CoRN/ftc/Composition/derG.var.
241 inline cic:/CoRN/ftc/Composition/Hmap.var.
245 inline cic:/CoRN/ftc/Composition/included_comp'.con.
247 inline cic:/CoRN/ftc/Composition/maps'.con.
249 inline cic:/CoRN/ftc/Composition/Derivative_I_comp.con.
252 The next lemma will be useful when we move on to differentiability.
255 inline cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con.
262 Section Differentiability.
265 (*#* **Differentiability
267 Finally, we move on to differentiability.
270 inline cic:/CoRN/ftc/Composition/F.var.
272 inline cic:/CoRN/ftc/Composition/G.var.
274 inline cic:/CoRN/ftc/Composition/a.var.
276 inline cic:/CoRN/ftc/Composition/b.var.
278 inline cic:/CoRN/ftc/Composition/Hab'.var.
280 inline cic:/CoRN/ftc/Composition/c.var.
282 inline cic:/CoRN/ftc/Composition/d.var.
284 inline cic:/CoRN/ftc/Composition/Hcd'.var.
288 inline cic:/CoRN/ftc/Composition/Hab.con.
290 inline cic:/CoRN/ftc/Composition/Hcd.con.
292 inline cic:/CoRN/ftc/Composition/I.con.
298 inline cic:/CoRN/ftc/Composition/diffF.var.
300 inline cic:/CoRN/ftc/Composition/diffG.var.
302 inline cic:/CoRN/ftc/Composition/Hmap.var.
306 inline cic:/CoRN/ftc/Composition/Diffble_I_comp.con.
309 End Differentiability.
313 Section Generalized_Intervals.
316 (*#* **Generalizations
318 We now generalize this results to arbitrary intervals. We begin by generalizing the notion of mapping compacts into compacts.
320 %\begin{convention}% We assume [I,J] to be proper intervals.
324 inline cic:/CoRN/ftc/Composition/I.var.
326 inline cic:/CoRN/ftc/Composition/J.var.
328 inline cic:/CoRN/ftc/Composition/pI.var.
330 inline cic:/CoRN/ftc/Composition/pJ.var.
332 inline cic:/CoRN/ftc/Composition/maps_compacts_into.con.
335 Now everything comes naturally:
338 inline cic:/CoRN/ftc/Composition/comp_inc_lemma.con.
340 inline cic:/CoRN/ftc/Composition/F.var.
342 inline cic:/CoRN/ftc/Composition/F'.var.
344 inline cic:/CoRN/ftc/Composition/G.var.
346 inline cic:/CoRN/ftc/Composition/G'.var.
350 inline cic:/CoRN/ftc/Composition/Hmap.var.
354 inline cic:/CoRN/ftc/Composition/Continuous_comp.con.
358 inline cic:/CoRN/ftc/Composition/Hmap'.var.
362 inline cic:/CoRN/ftc/Composition/Derivative_comp.con.
365 End Generalized_Intervals.
373 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
376 inline cic:/CoRN/ftc/Composition/positive_fun.con.
378 inline cic:/CoRN/ftc/Composition/negative_fun.con.
380 inline cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con.
382 inline cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con.
384 inline cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con.
387 As a corollary, we get the generalization of differentiability property.
390 inline cic:/CoRN/ftc/Composition/Diffble_comp.con.
397 Hint Immediate included_comp: included.
401 Hint Immediate Continuous_I_comp Continuous_comp: continuous.