helm/software/matita/contribs/procedural/CoRN/ftc/Integral.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: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)
  20
  21 include "ftc/RefLemma.ma".
  22
  23 (*#* printing integral %\ensuremath{\int_I}% #&int;<sub>I</sub># *)
  24
  25 (*#* printing Integral %\ensuremath{\int_I}% #&int;<sub>I</sub># *)
  26
  27 (* begin hide *)
  28
  29 (* UNEXPORTED
  30 Section Lemmas
  31 *)
  32
  33 inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__" as definition.
  34
  35 inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con" as lemma.
  36
  37 (* UNEXPORTED
  38 End Lemmas
  39 *)
  40
  41 (* end hide *)
  42
  43 (* UNEXPORTED
  44 Section Integral
  45 *)
  46
  47 (*#* *Integral
  48
  49 Having proved the main properties of partitions and refinements, we
  50 will define the integral of a continuous function [F] in the interval
  51 [[a,b]] as the limit of the sequence of Sums of $F$ for even
  52 partitions of increasing number of points.
  53
  54 %\begin{convention}% All throughout, [a,b] will be real numbers, the
  55 interval [[a,b]] will be denoted by [I] and [F,G] will be
  56 continuous functions in [I].
  57 %\end{convention}%
  58 *)
  59
  60 (* UNEXPORTED
  61 cic:/CoRN/ftc/Integral/Integral/a.var
  62 *)
  63
  64 (* UNEXPORTED
  65 cic:/CoRN/ftc/Integral/Integral/b.var
  66 *)
  67
  68 (* UNEXPORTED
  69 cic:/CoRN/ftc/Integral/Integral/Hab.var
  70 *)
  71
  72 (* begin hide *)
  73
  74 inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__" as definition.
  75
  76 (* UNEXPORTED
  77 cic:/CoRN/ftc/Integral/Integral/F.var
  78 *)
  79
  80 (* UNEXPORTED
  81 cic:/CoRN/ftc/Integral/Integral/contF.var
  82 *)
  83
  84 inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__" as definition.
  85
  86 (* end hide *)
  87
  88 (* UNEXPORTED
  89 Section Darboux_Sum
  90 *)
  91
  92 inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con" as definition.
  93
  94 inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con" as lemma.
  95
  96 inline procedural "cic:/CoRN/ftc/Integral/integral.con" as definition.
  97
  98 (* UNEXPORTED
  99 End Darboux_Sum
 100 *)
 101
 102 (* UNEXPORTED
 103 Section Integral_Thm
 104 *)
 105
 106 (*#*
 107 The following shows that in fact the integral of [F] is the limit of
 108 any sequence of partitions of mesh converging to 0.
 109
 110 %\begin{convention}% Let [e] be a positive real number and [P] be a
 111 partition of [I] with [n] points and mesh smaller than the
 112 modulus of continuity of [F] for [e].  Let [fP] be a choice of points
 113 respecting [P].
 114 %\end{convention}%
 115 *)
 116
 117 (* UNEXPORTED
 118 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var
 119 *)
 120
 121 (* UNEXPORTED
 122 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var
 123 *)
 124
 125 (* UNEXPORTED
 126 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var
 127 *)
 128
 129 (* UNEXPORTED
 130 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var
 131 *)
 132
 133 (* begin hide *)
 134
 135 inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__" as definition.
 136
 137 (* end hide *)
 138
 139 (* UNEXPORTED
 140 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var
 141 *)
 142
 143 (* UNEXPORTED
 144 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var
 145 *)
 146
 147 (* UNEXPORTED
 148 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var
 149 *)
 150
 151 (* UNEXPORTED
 152 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var
 153 *)
 154
 155 (* UNEXPORTED
 156 cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var
 157 *)
 158
 159 inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con" as lemma.
 160
 161 (* UNEXPORTED
 162 End Integral_Thm
 163 *)
 164
 165 (* UNEXPORTED
 166 End Integral
 167 *)
 168
 169 (* UNEXPORTED
 170 Section Basic_Properties
 171 *)
 172
 173 (*#*
 174 The usual extensionality and strong extensionality results hold.
 175 *)
 176
 177 (* UNEXPORTED
 178 cic:/CoRN/ftc/Integral/Basic_Properties/a.var
 179 *)
 180
 181 (* UNEXPORTED
 182 cic:/CoRN/ftc/Integral/Basic_Properties/b.var
 183 *)
 184
 185 (* UNEXPORTED
 186 cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var
 187 *)
 188
 189 (* begin hide *)
 190
 191 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__" as definition.
 192
 193 (* end hide *)
 194
 195 (* NOTATION
 196 Notation Integral := (integral _ _ Hab).
 197 *)
 198
 199 (* UNEXPORTED
 200 Section Well_Definedness
 201 *)
 202
 203 (* UNEXPORTED
 204 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var
 209 *)
 210
 211 (* UNEXPORTED
 212 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var
 213 *)
 214
 215 (* UNEXPORTED
 216 cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var
 217 *)
 218
 219 inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con" as lemma.
 220
 221 inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con" as lemma.
 222
 223 inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con" as lemma.
 224
 225 inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con" as lemma.
 226
 227 (* UNEXPORTED
 228 End Well_Definedness
 229 *)
 230
 231 (* UNEXPORTED
 232 Section Linearity_and_Monotonicity
 233 *)
 234
 235 (* UNEXPORTED
 236 Opaque Even_Partition.
 237 *)
 238
 239 (*#*
 240 The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities $\int_a^bdx=b-a$#&int;<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#&int;<sub>a</sub><sup>a</sup>=0#.
 241 *)
 242
 243 inline procedural "cic:/CoRN/ftc/Integral/integral_one.con" as lemma.
 244
 245 (* UNEXPORTED
 246 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var
 247 *)
 248
 249 (* UNEXPORTED
 250 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var
 251 *)
 252
 253 (* UNEXPORTED
 254 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var
 255 *)
 256
 257 (* UNEXPORTED
 258 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var
 259 *)
 260
 261 inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con" as lemma.
 262
 263 inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con" as lemma.
 264
 265 (* UNEXPORTED
 266 Transparent Even_Partition.
 267 *)
 268
 269 inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con" as lemma.
 270
 271 (* UNEXPORTED
 272 End Linearity_and_Monotonicity
 273 *)
 274
 275 (* UNEXPORTED
 276 Section Linearity_and_Monotonicity'
 277 *)
 278
 279 (* UNEXPORTED
 280 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var
 281 *)
 282
 283 (* UNEXPORTED
 284 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var
 285 *)
 286
 287 (* UNEXPORTED
 288 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var
 289 *)
 290
 291 (* UNEXPORTED
 292 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var
 293 *)
 294
 295 (*#*
 296 %\begin{convention}% Let [alpha, beta : IR] and assume that
 297 [h := alpha{**}F{+}beta{**}G] is continuous.
 298 %\end{convention}%
 299 *)
 300
 301 (* UNEXPORTED
 302 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var
 303 *)
 304
 305 (* UNEXPORTED
 306 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var
 307 *)
 308
 309 (* begin hide *)
 310
 311 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__" as definition.
 312
 313 (* end hide *)
 314
 315 (* UNEXPORTED
 316 cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var
 317 *)
 318
 319 inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con" as lemma.
 320
 321 (* UNEXPORTED
 322 Opaque nring.
 323 *)
 324
 325 inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con" as lemma.
 326
 327 (* UNEXPORTED
 328 Transparent nring.
 329 *)
 330
 331 (* UNEXPORTED
 332 End Linearity_and_Monotonicity'
 333 *)
 334
 335 (* UNEXPORTED
 336 Section Corollaries
 337 *)
 338
 339 (* UNEXPORTED
 340 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var
 341 *)
 342
 343 (* UNEXPORTED
 344 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var
 345 *)
 346
 347 (* UNEXPORTED
 348 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var
 349 *)
 350
 351 (* UNEXPORTED
 352 cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var
 353 *)
 354
 355 (*#*
 356 As corollaries we can calculate integrals of group operations applied to functions.
 357 *)
 358
 359 inline procedural "cic:/CoRN/ftc/Integral/integral_const.con" as lemma.
 360
 361 inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con" as lemma.
 362
 363 inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con" as lemma.
 364
 365 (*#*
 366 We can also bound integrals by bounding the integrated functions.
 367 *)
 368
 369 inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con" as lemma.
 370
 371 inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con" as lemma.
 372
 373 inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con" as lemma.
 374
 375 (* UNEXPORTED
 376 End Corollaries
 377 *)
 378
 379 (* UNEXPORTED
 380 Section Integral_Sum
 381 *)
 382
 383 (*#*
 384 We now relate the sum of integrals in adjoining intervals to the
 385 integral over the union of those intervals.
 386
 387 %\begin{convention}% Let [c] be a real number such that
 388 $c\in[a,b]$#c&isin;[a,b]#.
 389 %\end{convention}%
 390 *)
 391
 392 (* UNEXPORTED
 393 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var
 394 *)
 395
 396 (* UNEXPORTED
 397 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var
 398 *)
 399
 400 (* UNEXPORTED
 401 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var
 402 *)
 403
 404 (* UNEXPORTED
 405 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var
 406 *)
 407
 408 (* UNEXPORTED
 409 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var
 410 *)
 411
 412 (* UNEXPORTED
 413 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var
 414 *)
 415
 416 (* UNEXPORTED
 417 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var
 418 *)
 419
 420 (* UNEXPORTED
 421 Section Partition_Join
 422 *)
 423
 424 (*#*
 425 We first prove that every pair of partitions, one of [[a,c]]
 426 and another of [[c,b]] defines a partition of [[a,b]] the mesh
 427 of which is less or equal to the maximum of the mesh of the original
 428 partitions (actually it is equal, but we don't need the other
 429 inequality).
 430
 431 %\begin{convention}% Let [P,Q] be partitions respectively of
 432 [[a,c]] and [[c,b]] with [n] and [m] points.
 433 %\end{convention}%
 434 *)
 435
 436 (* UNEXPORTED
 437 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var
 438 *)
 439
 440 (* UNEXPORTED
 441 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var
 442 *)
 443
 444 (* UNEXPORTED
 445 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var
 446 *)
 447
 448 (* UNEXPORTED
 449 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var
 450 *)
 451
 452 (* begin hide *)
 453
 454 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con" as lemma.
 455
 456 (* end hide *)
 457
 458 inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con" as definition.
 459
 460 (* begin hide *)
 461
 462 inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con" as lemma.
 463
 464 inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con" as lemma.
 465
 466 inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con" as lemma.
 467
 468 inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con" as lemma.
 469
 470 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con" as lemma.
 471
 472 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con" as lemma.
 473
 474 inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con" as lemma.
 475
 476 inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con" as lemma.
 477
 478 inline procedural "cic:/CoRN/ftc/Integral/partition_join.con" as definition.
 479
 480 (* end hide *)
 481
 482 (*#*
 483 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
 484 %\end{convention}%
 485 *)
 486
 487 (* UNEXPORTED
 488 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var
 489 *)
 490
 491 (* UNEXPORTED
 492 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var
 493 *)
 494
 495 (* UNEXPORTED
 496 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var
 497 *)
 498
 499 (* UNEXPORTED
 500 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var
 501 *)
 502
 503 (* UNEXPORTED
 504 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var
 505 *)
 506
 507 (* UNEXPORTED
 508 cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var
 509 *)
 510
 511 (* begin hide *)
 512
 513 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con" as lemma.
 514
 515 (* end hide *)
 516
 517 inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con" as definition.
 518
 519 (* begin hide *)
 520
 521 inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con" as lemma.
 522
 523 inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con" as lemma.
 524
 525 inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con" as lemma.
 526
 527 (* end hide *)
 528
 529 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con" as lemma.
 530
 531 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con" as lemma.
 532
 533 (* UNEXPORTED
 534 Opaque partition_join.
 535 *)
 536
 537 (* UNEXPORTED
 538 Transparent partition_join.
 539 *)
 540
 541 (* UNEXPORTED
 542 Opaque minus.
 543 *)
 544
 545 (* UNEXPORTED
 546 Transparent minus.
 547 *)
 548
 549 (* UNEXPORTED
 550 Opaque minus.
 551 *)
 552
 553 (* UNEXPORTED
 554 Transparent minus.
 555 *)
 556
 557 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con" as lemma.
 558
 559 inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con" as lemma.
 560
 561 (* UNEXPORTED
 562 End Partition_Join
 563 *)
 564
 565 (*#*
 566 With these results in mind, the following is a trivial consequence:
 567 *)
 568
 569 (* UNEXPORTED
 570 Opaque Even_Partition.
 571 *)
 572
 573 inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con" as lemma.
 574
 575 (* UNEXPORTED
 576 End Integral_Sum
 577 *)
 578
 579 (* UNEXPORTED
 580 Transparent Even_Partition.
 581 *)
 582
 583 (* UNEXPORTED
 584 End Basic_Properties
 585 *)
 586
 587 (*#*
 588 The following are simple consequences of this result and of previous ones.
 589 *)
 590
 591 inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con" as lemma.
 592
 593 (* end hide *)
 594
 595 inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con" as lemma.
 596
 597 (* end hide *)
 598
 599 (*#* remove printing Integral *)
 600