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