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 (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
  20
  21 (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *)
  22
  23 (* INCLUDE
  24 MoreIntervals
  25 *)
  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