matita/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 alias id "F" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var".
  57
  58 alias id "G" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var".
  59
  60 alias id "a" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var".
  61
  62 alias id "b" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var".
  63
  64 alias id "Hab" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var".
  65
  66 alias id "c" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var".
  67
  68 alias id "d" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var".
  69
  70 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var".
  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 alias id "Hf" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var".
  81
  82 (* end show *)
  83
  84 inline "cic:/CoRN/ftc/Composition/maps_into_compacts.con".
  85
  86 (* begin show *)
  87
  88 alias id "maps" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/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 alias id "F" = "cic:/CoRN/ftc/Composition/Mapping/F.var".
 118
 119 alias id "G" = "cic:/CoRN/ftc/Composition/Mapping/G.var".
 120
 121 alias id "a" = "cic:/CoRN/ftc/Composition/Mapping/a.var".
 122
 123 alias id "b" = "cic:/CoRN/ftc/Composition/Mapping/b.var".
 124
 125 alias id "Hab" = "cic:/CoRN/ftc/Composition/Mapping/Hab.var".
 126
 127 alias id "c" = "cic:/CoRN/ftc/Composition/Mapping/c.var".
 128
 129 alias id "d" = "cic:/CoRN/ftc/Composition/Mapping/d.var".
 130
 131 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Mapping/Hcd.var".
 132
 133 (* begin show *)
 134
 135 alias id "Hf" = "cic:/CoRN/ftc/Composition/Mapping/Hf.var".
 136
 137 alias id "Hg" = "cic:/CoRN/ftc/Composition/Mapping/Hg.var".
 138
 139 alias id "maps" = "cic:/CoRN/ftc/Composition/Mapping/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 alias id "a" = "cic:/CoRN/ftc/Composition/Interval_Continuity/a.var".
 159
 160 alias id "b" = "cic:/CoRN/ftc/Composition/Interval_Continuity/b.var".
 161
 162 alias id "Hab" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var".
 163
 164 (* begin hide *)
 165
 166 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__".
 167
 168 (* end hide *)
 169
 170 alias id "c" = "cic:/CoRN/ftc/Composition/Interval_Continuity/c.var".
 171
 172 alias id "d" = "cic:/CoRN/ftc/Composition/Interval_Continuity/d.var".
 173
 174 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var".
 175
 176 alias id "F" = "cic:/CoRN/ftc/Composition/Interval_Continuity/F.var".
 177
 178 alias id "G" = "cic:/CoRN/ftc/Composition/Interval_Continuity/G.var".
 179
 180 (* begin show *)
 181
 182 alias id "contF" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var".
 183
 184 alias id "contG" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var".
 185
 186 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Interval_Continuity/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 alias id "F" = "cic:/CoRN/ftc/Composition/Derivative/F.var".
 206
 207 alias id "F'" = "cic:/CoRN/ftc/Composition/Derivative/F'.var".
 208
 209 alias id "G" = "cic:/CoRN/ftc/Composition/Derivative/G.var".
 210
 211 alias id "G'" = "cic:/CoRN/ftc/Composition/Derivative/G'.var".
 212
 213 alias id "a" = "cic:/CoRN/ftc/Composition/Derivative/a.var".
 214
 215 alias id "b" = "cic:/CoRN/ftc/Composition/Derivative/b.var".
 216
 217 alias id "Hab'" = "cic:/CoRN/ftc/Composition/Derivative/Hab'.var".
 218
 219 alias id "c" = "cic:/CoRN/ftc/Composition/Derivative/c.var".
 220
 221 alias id "d" = "cic:/CoRN/ftc/Composition/Derivative/d.var".
 222
 223 alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var".
 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 alias id "derF" = "cic:/CoRN/ftc/Composition/Derivative/derF.var".
 238
 239 alias id "derG" = "cic:/CoRN/ftc/Composition/Derivative/derG.var".
 240
 241 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Derivative/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 alias id "F" = "cic:/CoRN/ftc/Composition/Differentiability/F.var".
 271
 272 alias id "G" = "cic:/CoRN/ftc/Composition/Differentiability/G.var".
 273
 274 alias id "a" = "cic:/CoRN/ftc/Composition/Differentiability/a.var".
 275
 276 alias id "b" = "cic:/CoRN/ftc/Composition/Differentiability/b.var".
 277
 278 alias id "Hab'" = "cic:/CoRN/ftc/Composition/Differentiability/Hab'.var".
 279
 280 alias id "c" = "cic:/CoRN/ftc/Composition/Differentiability/c.var".
 281
 282 alias id "d" = "cic:/CoRN/ftc/Composition/Differentiability/d.var".
 283
 284 alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var".
 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 alias id "diffF" = "cic:/CoRN/ftc/Composition/Differentiability/diffF.var".
 299
 300 alias id "diffG" = "cic:/CoRN/ftc/Composition/Differentiability/diffG.var".
 301
 302 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Differentiability/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 alias id "I" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var".
 325
 326 alias id "J" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var".
 327
 328 alias id "pI" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var".
 329
 330 alias id "pJ" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/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 alias id "F" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var".
 341
 342 alias id "F'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var".
 343
 344 alias id "G" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var".
 345
 346 alias id "G'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var".
 347
 348 (* begin show *)
 349
 350 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var".
 351
 352 (* end show *)
 353
 354 inline "cic:/CoRN/ftc/Composition/Continuous_comp.con".
 355
 356 (* begin show *)
 357
 358 alias id "Hmap'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/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