helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.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/MoreFunctions".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
  22
  23 (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *)
  24
  25 include "ftc/MoreIntervals.ma".
  26
  27 (* UNEXPORTED
  28 Opaque Min Max.
  29 *)
  30
  31 (* UNEXPORTED
  32 Section Basic_Results.
  33 *)
  34
  35 (*#* *More about Functions
  36
  37 Here we state all the main results about properties of functions that
  38 we already proved for compact intervals in the more general setting of
  39 arbitrary intervals.
  40
  41 %\begin{convention}% Let [I:interval] and [F,F',G,G'] be partial functions.
  42 %\end{convention}%
  43
  44 **Continuity
  45 *)
  46
  47 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
  48
  49 (*#*
  50 Trivial stuff.
  51 *)
  52
  53 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con".
  54
  55 (*#*
  56 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
  57 %\end{convention}%
  58 *)
  59
  60 inline "cic:/CoRN/ftc/MoreFunctions/cI.var".
  61
  62 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
  63
  64 inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
  65
  66 inline "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con".
  67
  68 (* begin show *)
  69
  70 inline "cic:/CoRN/ftc/MoreFunctions/Hinc.var".
  71
  72 (* end show *)
  73
  74 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con".
  75
  76 inline "cic:/CoRN/ftc/MoreFunctions/FNorm.con".
  77
  78 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con".
  79
  80 (* UNEXPORTED
  81 End Basic_Results.
  82 *)
  83
  84 (* UNEXPORTED
  85 Hint Resolve Continuous_imp_inc: included.
  86 *)
  87
  88 (* UNEXPORTED
  89 Section Other_Results.
  90 *)
  91
  92 (*#*
  93 The usual stuff.
  94 *)
  95
  96 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
  97
  98 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
  99
 100 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 101
 102 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con".
 103
 104 (* begin show *)
 105
 106 inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
 107
 108 inline "cic:/CoRN/ftc/MoreFunctions/contG.var".
 109
 110 (* end show *)
 111
 112 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con".
 113
 114 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con".
 115
 116 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con".
 117
 118 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con".
 119
 120 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con".
 121
 122 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con".
 123
 124 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con".
 125
 126 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con".
 127
 128 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con".
 129
 130 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con".
 131
 132 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con".
 133
 134 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con".
 135
 136 (* UNEXPORTED
 137 End Other_Results.
 138 *)
 139
 140 (* UNEXPORTED
 141 Hint Resolve continuous_compact Continuous_const Continuous_id
 142   Continuous_plus Continuous_inv Continuous_minus Continuous_mult
 143   Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous.
 144 *)
 145
 146 (* UNEXPORTED
 147 Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
 148 *)
 149
 150 (* UNEXPORTED
 151 Section Corollaries.
 152 *)
 153
 154 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 155
 156 inline "cic:/CoRN/ftc/MoreFunctions/cI.var".
 157
 158 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 159
 160 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 161
 162 inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
 163
 164 inline "cic:/CoRN/ftc/MoreFunctions/contG.var".
 165
 166 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con".
 167
 168 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con".
 169
 170 (* UNEXPORTED
 171 End Corollaries.
 172 *)
 173
 174 (* UNEXPORTED
 175 Hint Resolve Continuous_div: continuous.
 176 *)
 177
 178 (* UNEXPORTED
 179 Section Sums.
 180 *)
 181
 182 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 183
 184 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con".
 185
 186 (*#*
 187 %\begin{convention}% Assume [f] is a sequence of continuous functions.
 188 %\end{convention}%
 189 *)
 190
 191 inline "cic:/CoRN/ftc/MoreFunctions/f.var".
 192
 193 inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
 194
 195 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con".
 196
 197 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con".
 198
 199 (* UNEXPORTED
 200 End Sums.
 201 *)
 202
 203 (* UNEXPORTED
 204 Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
 205 *)
 206
 207 (* UNEXPORTED
 208 Section Basic_Properties.
 209 *)
 210
 211 (*#* **Derivative
 212
 213 Derivative is not that much different.
 214
 215 %\begin{convention}% From this point on we assume [I] to be proper.
 216 %\end{convention}%
 217 *)
 218
 219 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 220
 221 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 222
 223 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 224
 225 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 226
 227 inline "cic:/CoRN/ftc/MoreFunctions/H.var".
 228
 229 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con".
 230
 231 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con".
 232
 233 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con".
 234
 235 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con".
 236
 237 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con".
 238
 239 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con".
 240
 241 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con".
 242
 243 (* UNEXPORTED
 244 End Basic_Properties.
 245 *)
 246
 247 (* UNEXPORTED
 248 Hint Immediate Derivative_imp_inc Derivative_imp_inc': included.
 249 *)
 250
 251 (* UNEXPORTED
 252 Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
 253   continuous.
 254 *)
 255
 256 (* UNEXPORTED
 257 Section More_Results.
 258 *)
 259
 260 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 261
 262 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 263
 264 (*#*
 265 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
 266 %\end{convention}%
 267 *)
 268
 269 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 270
 271 inline "cic:/CoRN/ftc/MoreFunctions/F'.var".
 272
 273 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 274
 275 inline "cic:/CoRN/ftc/MoreFunctions/G'.var".
 276
 277 inline "cic:/CoRN/ftc/MoreFunctions/derF.var".
 278
 279 inline "cic:/CoRN/ftc/MoreFunctions/derG.var".
 280
 281 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con".
 282
 283 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con".
 284
 285 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con".
 286
 287 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con".
 288
 289 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con".
 290
 291 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con".
 292
 293 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con".
 294
 295 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con".
 296
 297 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con".
 298
 299 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con".
 300
 301 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con".
 302
 303 (* UNEXPORTED
 304 End More_Results.
 305 *)
 306
 307 (* UNEXPORTED
 308 Section More_Corollaries.
 309 *)
 310
 311 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 312
 313 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 314
 315 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 316
 317 inline "cic:/CoRN/ftc/MoreFunctions/F'.var".
 318
 319 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 320
 321 inline "cic:/CoRN/ftc/MoreFunctions/G'.var".
 322
 323 inline "cic:/CoRN/ftc/MoreFunctions/derF.var".
 324
 325 inline "cic:/CoRN/ftc/MoreFunctions/derG.var".
 326
 327 (* begin show *)
 328
 329 inline "cic:/CoRN/ftc/MoreFunctions/Gbnd.var".
 330
 331 (* end show *)
 332
 333 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con".
 334
 335 (* UNEXPORTED
 336 End More_Corollaries.
 337 *)
 338
 339 (* UNEXPORTED
 340 Section More_Sums.
 341 *)
 342
 343 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 344
 345 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 346
 347 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con".
 348
 349 (* begin show *)
 350
 351 inline "cic:/CoRN/ftc/MoreFunctions/f.var".
 352
 353 inline "cic:/CoRN/ftc/MoreFunctions/f'.var".
 354
 355 inline "cic:/CoRN/ftc/MoreFunctions/derF.var".
 356
 357 (* end show *)
 358
 359 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con".
 360
 361 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con".
 362
 363 (* UNEXPORTED
 364 End More_Sums.
 365 *)
 366
 367 (* UNEXPORTED
 368 Section Diffble_Basic_Properties.
 369 *)
 370
 371 (*#* **Differentiability
 372
 373 Mutatis mutandis for differentiability.
 374 *)
 375
 376 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 377
 378 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 379
 380 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con".
 381
 382 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con".
 383
 384 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con".
 385
 386 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 387
 388 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 389
 390 inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
 391
 392 inline "cic:/CoRN/ftc/MoreFunctions/diffG.var".
 393
 394 (*#*
 395 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
 396 %\end{convention}%
 397 *)
 398
 399 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con".
 400
 401 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con".
 402
 403 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con".
 404
 405 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con".
 406
 407 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con".
 408
 409 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con".
 410
 411 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con".
 412
 413 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con".
 414
 415 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con".
 416
 417 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con".
 418
 419 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con".
 420
 421 (* UNEXPORTED
 422 End Diffble_Basic_Properties.
 423 *)
 424
 425 (* UNEXPORTED
 426 Hint Immediate Diffble_imp_inc: included.
 427 *)
 428
 429 (* UNEXPORTED
 430 Section Diffble_Corollaries.
 431 *)
 432
 433 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 434
 435 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 436
 437 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 438
 439 inline "cic:/CoRN/ftc/MoreFunctions/G.var".
 440
 441 inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
 442
 443 inline "cic:/CoRN/ftc/MoreFunctions/diffG.var".
 444
 445 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con".
 446
 447 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con".
 448
 449 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con".
 450
 451 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con".
 452
 453 (* UNEXPORTED
 454 End Diffble_Corollaries.
 455 *)
 456
 457 (* UNEXPORTED
 458 Section Nth_Derivative.
 459 *)
 460
 461 (*#* **Nth Derivative
 462
 463 Higher order derivatives pose more interesting problems.  It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
 464 *)
 465
 466 inline "cic:/CoRN/ftc/MoreFunctions/I.var".
 467
 468 inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
 469
 470 (* UNEXPORTED
 471 Section Definitions.
 472 *)
 473
 474 (*#*
 475 %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I].
 476 %\end{convention}%
 477 *)
 478
 479 inline "cic:/CoRN/ftc/MoreFunctions/n.var".
 480
 481 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 482
 483 inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
 484
 485 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con".
 486
 487 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
 488  (* begin hide *).con".
 489
 490 (* end hide *)
 491
 492 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con".
 493
 494 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con".
 495
 496 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con".
 497
 498 (* UNEXPORTED
 499 End Definitions.
 500 *)
 501
 502 (* UNEXPORTED
 503 Section Basic_Results.
 504 *)
 505
 506 (*#*
 507 All the usual results hold.
 508 *)
 509
 510 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con".
 511
 512 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con".
 513
 514 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con".
 515
 516 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con".
 517
 518 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con".
 519
 520 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con".
 521
 522 inline "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con".
 523
 524 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con".
 525
 526 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con".
 527
 528 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con".
 529
 530 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con".
 531
 532 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con".
 533
 534 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con".
 535
 536 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con".
 537
 538 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con".
 539
 540 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con".
 541
 542 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con".
 543
 544 (* UNEXPORTED
 545 End Basic_Results.
 546 *)
 547
 548 (* UNEXPORTED
 549 Section More_Results.
 550 *)
 551
 552 (*#*
 553 Some new results hold, too:
 554 *)
 555
 556 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con".
 557
 558 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con".
 559
 560 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con".
 561
 562 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con".
 563
 564 (*#*
 565 Some useful characterization results.
 566 *)
 567
 568 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con".
 569
 570 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con".
 571
 572 (* UNEXPORTED
 573 End More_Results.
 574 *)
 575
 576 (* UNEXPORTED
 577 Section Derivating_Diffble.
 578 *)
 579
 580 (*#*
 581 As a special case we get a differentiation operator%\ldots%#...#
 582 *)
 583
 584 inline "cic:/CoRN/ftc/MoreFunctions/F.var".
 585
 586 (* begin show *)
 587
 588 inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
 589
 590 (* end show *)
 591
 592 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con".
 593
 594 inline "cic:/CoRN/ftc/MoreFunctions/Deriv.con".
 595
 596 (* UNEXPORTED
 597 End Derivating_Diffble.
 598 *)
 599
 600 (* UNEXPORTED
 601 Section Corollaries.
 602 *)
 603
 604 (*#*
 605 %\ldots%#...# for which the expected property also holds.
 606 *)
 607
 608 inline "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con".
 609
 610 (*#*
 611 Some more interesting properties.
 612 *)
 613
 614 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con".
 615
 616 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con".
 617
 618 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con".
 619
 620 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con".
 621
 622 (* UNEXPORTED
 623 End Corollaries.
 624 *)
 625
 626 (* UNEXPORTED
 627 End Nth_Derivative.
 628 *)
 629
 630 (* UNEXPORTED
 631 Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv
 632   Derivative_minus Derivative_mult Derivative_scal Derivative_nth
 633   Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0
 634   Derivative_Sum: derivate.
 635 *)
 636
 637 (* UNEXPORTED
 638 Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc:
 639   included.
 640 *)
 641
 642 (* UNEXPORTED
 643 Hint Resolve Deriv_lemma N_Deriv_lemma: derivate.
 644 *)
 645
 646 (* UNEXPORTED
 647 Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous':
 648   continuous.
 649 *)
 650