helm/software/matita/contribs/CoRN-Procedural/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__".
  34
  35 inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con".
  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 alias id "a" = "cic:/CoRN/ftc/Integral/Integral/a.var".
  61
  62 alias id "b" = "cic:/CoRN/ftc/Integral/Integral/b.var".
  63
  64 alias id "Hab" = "cic:/CoRN/ftc/Integral/Integral/Hab.var".
  65
  66 (* begin hide *)
  67
  68 inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__".
  69
  70 alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var".
  71
  72 alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var".
  73
  74 inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__".
  75
  76 (* end hide *)
  77
  78 (* UNEXPORTED
  79 Section Darboux_Sum
  80 *)
  81
  82 inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con".
  83
  84 inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con".
  85
  86 inline procedural "cic:/CoRN/ftc/Integral/integral.con".
  87
  88 (* UNEXPORTED
  89 End Darboux_Sum
  90 *)
  91
  92 (* UNEXPORTED
  93 Section Integral_Thm
  94 *)
  95
  96 (*#*
  97 The following shows that in fact the integral of [F] is the limit of
  98 any sequence of partitions of mesh converging to 0.
  99
 100 %\begin{convention}% Let [e] be a positive real number and [P] be a
 101 partition of [I] with [n] points and mesh smaller than the
 102 modulus of continuity of [F] for [e].  Let [fP] be a choice of points
 103 respecting [P].
 104 %\end{convention}%
 105 *)
 106
 107 alias id "n" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var".
 108
 109 alias id "P" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var".
 110
 111 alias id "e" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var".
 112
 113 alias id "He" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var".
 114
 115 (* begin hide *)
 116
 117 inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__".
 118
 119 (* end hide *)
 120
 121 alias id "HmeshP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var".
 122
 123 alias id "fP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var".
 124
 125 alias id "HfP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var".
 126
 127 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var".
 128
 129 alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var".
 130
 131 inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con".
 132
 133 (* UNEXPORTED
 134 End Integral_Thm
 135 *)
 136
 137 (* UNEXPORTED
 138 End Integral
 139 *)
 140
 141 (* UNEXPORTED
 142 Section Basic_Properties
 143 *)
 144
 145 (*#*
 146 The usual extensionality and strong extensionality results hold.
 147 *)
 148
 149 alias id "a" = "cic:/CoRN/ftc/Integral/Basic_Properties/a.var".
 150
 151 alias id "b" = "cic:/CoRN/ftc/Integral/Basic_Properties/b.var".
 152
 153 alias id "Hab" = "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var".
 154
 155 (* begin hide *)
 156
 157 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__".
 158
 159 (* end hide *)
 160
 161 (* NOTATION
 162 Notation Integral := (integral _ _ Hab).
 163 *)
 164
 165 (* UNEXPORTED
 166 Section Well_Definedness
 167 *)
 168
 169 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var".
 170
 171 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var".
 172
 173 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var".
 174
 175 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var".
 176
 177 inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con".
 178
 179 inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con".
 180
 181 inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con".
 182
 183 inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con".
 184
 185 (* UNEXPORTED
 186 End Well_Definedness
 187 *)
 188
 189 (* UNEXPORTED
 190 Section Linearity_and_Monotonicity
 191 *)
 192
 193 (* UNEXPORTED
 194 Opaque Even_Partition.
 195 *)
 196
 197 (*#*
 198 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#.
 199 *)
 200
 201 inline procedural "cic:/CoRN/ftc/Integral/integral_one.con".
 202
 203 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var".
 204
 205 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var".
 206
 207 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var".
 208
 209 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var".
 210
 211 inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
 212
 213 inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con".
 214
 215 (* UNEXPORTED
 216 Transparent Even_Partition.
 217 *)
 218
 219 inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con".
 220
 221 (* UNEXPORTED
 222 End Linearity_and_Monotonicity
 223 *)
 224
 225 (* UNEXPORTED
 226 Section Linearity_and_Monotonicity'
 227 *)
 228
 229 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var".
 230
 231 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var".
 232
 233 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var".
 234
 235 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var".
 236
 237 (*#*
 238 %\begin{convention}% Let [alpha, beta : IR] and assume that
 239 [h := alpha{**}F{+}beta{**}G] is continuous.
 240 %\end{convention}%
 241 *)
 242
 243 alias id "alpha" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var".
 244
 245 alias id "beta" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var".
 246
 247 (* begin hide *)
 248
 249 inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__".
 250
 251 (* end hide *)
 252
 253 alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var".
 254
 255 inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con".
 256
 257 (* UNEXPORTED
 258 Opaque nring.
 259 *)
 260
 261 inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con".
 262
 263 (* UNEXPORTED
 264 Transparent nring.
 265 *)
 266
 267 (* UNEXPORTED
 268 End Linearity_and_Monotonicity'
 269 *)
 270
 271 (* UNEXPORTED
 272 Section Corollaries
 273 *)
 274
 275 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var".
 276
 277 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var".
 278
 279 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var".
 280
 281 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var".
 282
 283 (*#*
 284 As corollaries we can calculate integrals of group operations applied to functions.
 285 *)
 286
 287 inline procedural "cic:/CoRN/ftc/Integral/integral_const.con".
 288
 289 inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con".
 290
 291 inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con".
 292
 293 (*#*
 294 We can also bound integrals by bounding the integrated functions.
 295 *)
 296
 297 inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con".
 298
 299 inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con".
 300
 301 inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
 302
 303 (* UNEXPORTED
 304 End Corollaries
 305 *)
 306
 307 (* UNEXPORTED
 308 Section Integral_Sum
 309 *)
 310
 311 (*#*
 312 We now relate the sum of integrals in adjoining intervals to the
 313 integral over the union of those intervals.
 314
 315 %\begin{convention}% Let [c] be a real number such that
 316 $c\in[a,b]$#c&isin;[a,b]#.
 317 %\end{convention}%
 318 *)
 319
 320 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var".
 321
 322 alias id "c" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var".
 323
 324 alias id "Hac" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var".
 325
 326 alias id "Hcb" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var".
 327
 328 alias id "Hab'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var".
 329
 330 alias id "Hac'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var".
 331
 332 alias id "Hcb'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var".
 333
 334 (* UNEXPORTED
 335 Section Partition_Join
 336 *)
 337
 338 (*#*
 339 We first prove that every pair of partitions, one of [[a,c]]
 340 and another of [[c,b]] defines a partition of [[a,b]] the mesh
 341 of which is less or equal to the maximum of the mesh of the original
 342 partitions (actually it is equal, but we don't need the other
 343 inequality).
 344
 345 %\begin{convention}% Let [P,Q] be partitions respectively of
 346 [[a,c]] and [[c,b]] with [n] and [m] points.
 347 %\end{convention}%
 348 *)
 349
 350 alias id "n" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var".
 351
 352 alias id "m" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var".
 353
 354 alias id "P" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var".
 355
 356 alias id "Q" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var".
 357
 358 (* begin hide *)
 359
 360 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con".
 361
 362 (* end hide *)
 363
 364 inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con".
 365
 366 (* begin hide *)
 367
 368 inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con".
 369
 370 inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con".
 371
 372 inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con".
 373
 374 inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con".
 375
 376 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
 377
 378 inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
 379
 380 inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con".
 381
 382 inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con".
 383
 384 inline procedural "cic:/CoRN/ftc/Integral/partition_join.con".
 385
 386 (* end hide *)
 387
 388 (*#*
 389 %\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
 390 %\end{convention}%
 391 *)
 392
 393 alias id "fP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var".
 394
 395 alias id "HfP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var".
 396
 397 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var".
 398
 399 alias id "fQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var".
 400
 401 alias id "HfQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var".
 402
 403 alias id "HfQ'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var".
 404
 405 (* begin hide *)
 406
 407 inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
 408
 409 (* end hide *)
 410
 411 inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con".
 412
 413 (* begin hide *)
 414
 415 inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con".
 416
 417 inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con".
 418
 419 inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con".
 420
 421 (* end hide *)
 422
 423 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
 424
 425 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
 426
 427 (* UNEXPORTED
 428 Opaque partition_join.
 429 *)
 430
 431 (* UNEXPORTED
 432 Transparent partition_join.
 433 *)
 434
 435 (* UNEXPORTED
 436 Opaque minus.
 437 *)
 438
 439 (* UNEXPORTED
 440 Transparent minus.
 441 *)
 442
 443 (* UNEXPORTED
 444 Opaque minus.
 445 *)
 446
 447 (* UNEXPORTED
 448 Transparent minus.
 449 *)
 450
 451 inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
 452
 453 inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
 454
 455 (* UNEXPORTED
 456 End Partition_Join
 457 *)
 458
 459 (*#*
 460 With these results in mind, the following is a trivial consequence:
 461 *)
 462
 463 (* UNEXPORTED
 464 Opaque Even_Partition.
 465 *)
 466
 467 inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
 468
 469 (* UNEXPORTED
 470 End Integral_Sum
 471 *)
 472
 473 (* UNEXPORTED
 474 Transparent Even_Partition.
 475 *)
 476
 477 (* UNEXPORTED
 478 End Basic_Properties
 479 *)
 480
 481 (*#*
 482 The following are simple consequences of this result and of previous ones.
 483 *)
 484
 485 inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con".
 486
 487 (* end hide *)
 488
 489 inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
 490
 491 (* end hide *)
 492
 493 (*#* remove printing Integral *)
 494