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 include "CoRN.ma".
  20
  21 (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
  22
  23 include "ftc/MoreFunctions.ma".
  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/Maps_into_Compacts/Part_Funct/F.var" "Maps_into_Compacts__Part_Funct__".
  57
  58 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var" "Maps_into_Compacts__Part_Funct__".
  59
  60 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var" "Maps_into_Compacts__Part_Funct__".
  61
  62 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var" "Maps_into_Compacts__Part_Funct__".
  63
  64 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var" "Maps_into_Compacts__Part_Funct__".
  65
  66 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var" "Maps_into_Compacts__Part_Funct__".
  67
  68 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var" "Maps_into_Compacts__Part_Funct__".
  69
  70 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var" "Maps_into_Compacts__Part_Funct__".
  71
  72 (* begin hide *)
  73
  74 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__".
  75
  76 (* end hide *)
  77
  78 (* begin show *)
  79
  80 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var" "Maps_into_Compacts__Part_Funct__".
  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_into_Compacts/Part_Funct/maps.var" "Maps_into_Compacts__Part_Funct__".
  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/Mapping/F.var" "Mapping__".
 118
 119 inline "cic:/CoRN/ftc/Composition/Mapping/G.var" "Mapping__".
 120
 121 inline "cic:/CoRN/ftc/Composition/Mapping/a.var" "Mapping__".
 122
 123 inline "cic:/CoRN/ftc/Composition/Mapping/b.var" "Mapping__".
 124
 125 inline "cic:/CoRN/ftc/Composition/Mapping/Hab.var" "Mapping__".
 126
 127 inline "cic:/CoRN/ftc/Composition/Mapping/c.var" "Mapping__".
 128
 129 inline "cic:/CoRN/ftc/Composition/Mapping/d.var" "Mapping__".
 130
 131 inline "cic:/CoRN/ftc/Composition/Mapping/Hcd.var" "Mapping__".
 132
 133 (* begin show *)
 134
 135 inline "cic:/CoRN/ftc/Composition/Mapping/Hf.var" "Mapping__".
 136
 137 inline "cic:/CoRN/ftc/Composition/Mapping/Hg.var" "Mapping__".
 138
 139 inline "cic:/CoRN/ftc/Composition/Mapping/maps.var" "Mapping__".
 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/Interval_Continuity/a.var" "Interval_Continuity__".
 159
 160 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/b.var" "Interval_Continuity__".
 161
 162 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var" "Interval_Continuity__".
 163
 164 (* begin hide *)
 165
 166 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__".
 167
 168 (* end hide *)
 169
 170 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/c.var" "Interval_Continuity__".
 171
 172 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/d.var" "Interval_Continuity__".
 173
 174 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var" "Interval_Continuity__".
 175
 176 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/F.var" "Interval_Continuity__".
 177
 178 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/G.var" "Interval_Continuity__".
 179
 180 (* begin show *)
 181
 182 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var" "Interval_Continuity__".
 183
 184 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var" "Interval_Continuity__".
 185
 186 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var" "Interval_Continuity__".
 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/Derivative/F.var" "Derivative__".
 206
 207 inline "cic:/CoRN/ftc/Composition/Derivative/F'.var" "Derivative__".
 208
 209 inline "cic:/CoRN/ftc/Composition/Derivative/G.var" "Derivative__".
 210
 211 inline "cic:/CoRN/ftc/Composition/Derivative/G'.var" "Derivative__".
 212
 213 inline "cic:/CoRN/ftc/Composition/Derivative/a.var" "Derivative__".
 214
 215 inline "cic:/CoRN/ftc/Composition/Derivative/b.var" "Derivative__".
 216
 217 inline "cic:/CoRN/ftc/Composition/Derivative/Hab'.var" "Derivative__".
 218
 219 inline "cic:/CoRN/ftc/Composition/Derivative/c.var" "Derivative__".
 220
 221 inline "cic:/CoRN/ftc/Composition/Derivative/d.var" "Derivative__".
 222
 223 inline "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var" "Derivative__".
 224
 225 (* begin hide *)
 226
 227 inline "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__".
 228
 229 inline "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__".
 230
 231 inline "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__".
 232
 233 (* end hide *)
 234
 235 (* begin show *)
 236
 237 inline "cic:/CoRN/ftc/Composition/Derivative/derF.var" "Derivative__".
 238
 239 inline "cic:/CoRN/ftc/Composition/Derivative/derG.var" "Derivative__".
 240
 241 inline "cic:/CoRN/ftc/Composition/Derivative/Hmap.var" "Derivative__".
 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/Differentiability/F.var" "Differentiability__".
 271
 272 inline "cic:/CoRN/ftc/Composition/Differentiability/G.var" "Differentiability__".
 273
 274 inline "cic:/CoRN/ftc/Composition/Differentiability/a.var" "Differentiability__".
 275
 276 inline "cic:/CoRN/ftc/Composition/Differentiability/b.var" "Differentiability__".
 277
 278 inline "cic:/CoRN/ftc/Composition/Differentiability/Hab'.var" "Differentiability__".
 279
 280 inline "cic:/CoRN/ftc/Composition/Differentiability/c.var" "Differentiability__".
 281
 282 inline "cic:/CoRN/ftc/Composition/Differentiability/d.var" "Differentiability__".
 283
 284 inline "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var" "Differentiability__".
 285
 286 (* begin hide *)
 287
 288 inline "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__".
 289
 290 inline "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__".
 291
 292 inline "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__".
 293
 294 (* end hide *)
 295
 296 (* begin show *)
 297
 298 inline "cic:/CoRN/ftc/Composition/Differentiability/diffF.var" "Differentiability__".
 299
 300 inline "cic:/CoRN/ftc/Composition/Differentiability/diffG.var" "Differentiability__".
 301
 302 inline "cic:/CoRN/ftc/Composition/Differentiability/Hmap.var" "Differentiability__".
 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/Generalized_Intervals/I.var" "Generalized_Intervals__".
 325
 326 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var" "Generalized_Intervals__".
 327
 328 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var" "Generalized_Intervals__".
 329
 330 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var" "Generalized_Intervals__".
 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/Generalized_Intervals/F.var" "Generalized_Intervals__".
 341
 342 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var" "Generalized_Intervals__".
 343
 344 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var" "Generalized_Intervals__".
 345
 346 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var" "Generalized_Intervals__".
 347
 348 (* begin show *)
 349
 350 inline "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var" "Generalized_Intervals__".
 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/Generalized_Intervals/Hmap'.var" "Generalized_Intervals__".
 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