helm/software/matita/contribs/CoRN-Decl/ftc/Composition.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/Composition".
  18
  19 (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 MoreFunctions
  23 *)
  24
  25 (* UNEXPORTED
  26 Section Maps_into_Compacts.
  27 *)
  28
  29 (* UNEXPORTED
  30 Section Part_Funct.
  31 *)
  32
  33 (*#* *Composition
  34
  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
  39 intervals.
  40
  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.
  45
  46 %\end{convention}%
  47
  48 ** Maps into Compacts
  49
  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.
  54 *)
  55
  56 inline cic:/CoRN/ftc/Composition/F.var.
  57
  58 inline cic:/CoRN/ftc/Composition/G.var.
  59
  60 inline cic:/CoRN/ftc/Composition/a.var.
  61
  62 inline cic:/CoRN/ftc/Composition/b.var.
  63
  64 inline cic:/CoRN/ftc/Composition/Hab.var.
  65
  66 inline cic:/CoRN/ftc/Composition/c.var.
  67
  68 inline cic:/CoRN/ftc/Composition/d.var.
  69
  70 inline cic:/CoRN/ftc/Composition/Hcd.var.
  71
  72 (* begin hide *)
  73
  74 inline cic:/CoRN/ftc/Composition/I.con.
  75
  76 (* end hide *)
  77
  78 (* begin show *)
  79
  80 inline cic:/CoRN/ftc/Composition/Hf.var.
  81
  82 (* end show *)
  83
  84 inline cic:/CoRN/ftc/Composition/maps_into_compacts.con.
  85
  86 (* begin show *)
  87
  88 inline cic:/CoRN/ftc/Composition/maps.var.
  89
  90 (* end show *)
  91
  92 inline cic:/CoRN/ftc/Composition/maps_lemma'.con.
  93
  94 inline cic:/CoRN/ftc/Composition/maps_lemma.con.
  95
  96 inline cic:/CoRN/ftc/Composition/maps_lemma_less.con.
  97
  98 inline cic:/CoRN/ftc/Composition/maps_lemma_inc.con.
  99
 100 (* UNEXPORTED
 101 End Part_Funct.
 102 *)
 103
 104 (* UNEXPORTED
 105 End Maps_into_Compacts.
 106 *)
 107
 108 (* UNEXPORTED
 109 Section Mapping.
 110 *)
 111
 112 (*#*
 113 As was the case for division of partial functions, this condition
 114 completely characterizes the domain of the composite function.
 115 *)
 116
 117 inline cic:/CoRN/ftc/Composition/F.var.
 118
 119 inline cic:/CoRN/ftc/Composition/G.var.
 120
 121 inline cic:/CoRN/ftc/Composition/a.var.
 122
 123 inline cic:/CoRN/ftc/Composition/b.var.
 124
 125 inline cic:/CoRN/ftc/Composition/Hab.var.
 126
 127 inline cic:/CoRN/ftc/Composition/c.var.
 128
 129 inline cic:/CoRN/ftc/Composition/d.var.
 130
 131 inline cic:/CoRN/ftc/Composition/Hcd.var.
 132
 133 (* begin show *)
 134
 135 inline cic:/CoRN/ftc/Composition/Hf.var.
 136
 137 inline cic:/CoRN/ftc/Composition/Hg.var.
 138
 139 inline cic:/CoRN/ftc/Composition/maps.var.
 140
 141 (* end show *)
 142
 143 inline cic:/CoRN/ftc/Composition/included_comp.con.
 144
 145 (* UNEXPORTED
 146 End Mapping.
 147 *)
 148
 149 (* UNEXPORTED
 150 Section Interval_Continuity.
 151 *)
 152
 153 (*#* **Continuity
 154
 155 We now prove that the composition of two continuous partial functions is continuous.
 156 *)
 157
 158 inline cic:/CoRN/ftc/Composition/a.var.
 159
 160 inline cic:/CoRN/ftc/Composition/b.var.
 161
 162 inline cic:/CoRN/ftc/Composition/Hab.var.
 163
 164 (* begin hide *)
 165
 166 inline cic:/CoRN/ftc/Composition/I.con.
 167
 168 (* end hide *)
 169
 170 inline cic:/CoRN/ftc/Composition/c.var.
 171
 172 inline cic:/CoRN/ftc/Composition/d.var.
 173
 174 inline cic:/CoRN/ftc/Composition/Hcd.var.
 175
 176 inline cic:/CoRN/ftc/Composition/F.var.
 177
 178 inline cic:/CoRN/ftc/Composition/G.var.
 179
 180 (* begin show *)
 181
 182 inline cic:/CoRN/ftc/Composition/contF.var.
 183
 184 inline cic:/CoRN/ftc/Composition/contG.var.
 185
 186 inline cic:/CoRN/ftc/Composition/Hmap.var.
 187
 188 (* end show *)
 189
 190 inline cic:/CoRN/ftc/Composition/Continuous_I_comp.con.
 191
 192 (* UNEXPORTED
 193 End Interval_Continuity.
 194 *)
 195
 196 (* UNEXPORTED
 197 Section Derivative.
 198 *)
 199
 200 (*#* **Derivative
 201
 202 We now work with the derivative relation and prove the chain rule for partial functions.
 203 *)
 204
 205 inline cic:/CoRN/ftc/Composition/F.var.
 206
 207 inline cic:/CoRN/ftc/Composition/F'.var.
 208
 209 inline cic:/CoRN/ftc/Composition/G.var.
 210
 211 inline cic:/CoRN/ftc/Composition/G'.var.
 212
 213 inline cic:/CoRN/ftc/Composition/a.var.
 214
 215 inline cic:/CoRN/ftc/Composition/b.var.
 216
 217 inline cic:/CoRN/ftc/Composition/Hab'.var.
 218
 219 inline cic:/CoRN/ftc/Composition/c.var.
 220
 221 inline cic:/CoRN/ftc/Composition/d.var.
 222
 223 inline cic:/CoRN/ftc/Composition/Hcd'.var.
 224
 225 (* begin hide *)
 226
 227 inline cic:/CoRN/ftc/Composition/Hab.con.
 228
 229 inline cic:/CoRN/ftc/Composition/Hcd.con.
 230
 231 inline cic:/CoRN/ftc/Composition/I.con.
 232
 233 (* end hide *)
 234
 235 (* begin show *)
 236
 237 inline cic:/CoRN/ftc/Composition/derF.var.
 238
 239 inline cic:/CoRN/ftc/Composition/derG.var.
 240
 241 inline cic:/CoRN/ftc/Composition/Hmap.var.
 242
 243 (* end show *)
 244
 245 inline cic:/CoRN/ftc/Composition/included_comp'.con.
 246
 247 inline cic:/CoRN/ftc/Composition/maps'.con.
 248
 249 inline cic:/CoRN/ftc/Composition/Derivative_I_comp.con.
 250
 251 (*#*
 252 The next lemma will be useful when we move on to differentiability.
 253 *)
 254
 255 inline cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con.
 256
 257 (* UNEXPORTED
 258 End Derivative.
 259 *)
 260
 261 (* UNEXPORTED
 262 Section Differentiability.
 263 *)
 264
 265 (*#* **Differentiability
 266
 267 Finally, we move on to differentiability.
 268 *)
 269
 270 inline cic:/CoRN/ftc/Composition/F.var.
 271
 272 inline cic:/CoRN/ftc/Composition/G.var.
 273
 274 inline cic:/CoRN/ftc/Composition/a.var.
 275
 276 inline cic:/CoRN/ftc/Composition/b.var.
 277
 278 inline cic:/CoRN/ftc/Composition/Hab'.var.
 279
 280 inline cic:/CoRN/ftc/Composition/c.var.
 281
 282 inline cic:/CoRN/ftc/Composition/d.var.
 283
 284 inline cic:/CoRN/ftc/Composition/Hcd'.var.
 285
 286 (* begin hide *)
 287
 288 inline cic:/CoRN/ftc/Composition/Hab.con.
 289
 290 inline cic:/CoRN/ftc/Composition/Hcd.con.
 291
 292 inline cic:/CoRN/ftc/Composition/I.con.
 293
 294 (* end hide *)
 295
 296 (* begin show *)
 297
 298 inline cic:/CoRN/ftc/Composition/diffF.var.
 299
 300 inline cic:/CoRN/ftc/Composition/diffG.var.
 301
 302 inline cic:/CoRN/ftc/Composition/Hmap.var.
 303
 304 (* end show *)
 305
 306 inline cic:/CoRN/ftc/Composition/Diffble_I_comp.con.
 307
 308 (* UNEXPORTED
 309 End Differentiability.
 310 *)
 311
 312 (* UNEXPORTED
 313 Section Generalized_Intervals.
 314 *)
 315
 316 (*#* **Generalizations
 317
 318 We now generalize this results to arbitrary intervals.  We begin by generalizing the notion of mapping compacts into compacts.
 319
 320 %\begin{convention}% We assume [I,J] to be proper intervals.
 321 %\end{convention}%
 322 *)
 323
 324 inline cic:/CoRN/ftc/Composition/I.var.
 325
 326 inline cic:/CoRN/ftc/Composition/J.var.
 327
 328 inline cic:/CoRN/ftc/Composition/pI.var.
 329
 330 inline cic:/CoRN/ftc/Composition/pJ.var.
 331
 332 inline cic:/CoRN/ftc/Composition/maps_compacts_into.con.
 333
 334 (*#*
 335 Now everything comes naturally:
 336 *)
 337
 338 inline cic:/CoRN/ftc/Composition/comp_inc_lemma.con.
 339
 340 inline cic:/CoRN/ftc/Composition/F.var.
 341
 342 inline cic:/CoRN/ftc/Composition/F'.var.
 343
 344 inline cic:/CoRN/ftc/Composition/G.var.
 345
 346 inline cic:/CoRN/ftc/Composition/G'.var.
 347
 348 (* begin show *)
 349
 350 inline cic:/CoRN/ftc/Composition/Hmap.var.
 351
 352 (* end show *)
 353
 354 inline cic:/CoRN/ftc/Composition/Continuous_comp.con.
 355
 356 (* begin show *)
 357
 358 inline cic:/CoRN/ftc/Composition/Hmap'.var.
 359
 360 (* end show *)
 361
 362 inline cic:/CoRN/ftc/Composition/Derivative_comp.con.
 363
 364 (* UNEXPORTED
 365 End Generalized_Intervals.
 366 *)
 367
 368 (* UNEXPORTED
 369 Section Corollaries.
 370 *)
 371
 372 (*#*
 373 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
 374 *)
 375
 376 inline cic:/CoRN/ftc/Composition/positive_fun.con.
 377
 378 inline cic:/CoRN/ftc/Composition/negative_fun.con.
 379
 380 inline cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con.
 381
 382 inline cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con.
 383
 384 inline cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con.
 385
 386 (*#*
 387 As a corollary, we get the generalization of differentiability property.
 388 *)
 389
 390 inline cic:/CoRN/ftc/Composition/Diffble_comp.con.
 391
 392 (* UNEXPORTED
 393 End Corollaries.
 394 *)
 395
 396 (* UNEXPORTED
 397 Hint Immediate included_comp: included.
 398 *)
 399
 400 (* UNEXPORTED
 401 Hint Immediate Continuous_I_comp Continuous_comp: continuous.
 402 *)
 403