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