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