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