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 alias id "a" = "cic:/CoRN/ftc/Integral/Integral/a.var".
  63
  64 alias id "b" = "cic:/CoRN/ftc/Integral/Integral/b.var".
  65
  66 alias id "Hab" = "cic:/CoRN/ftc/Integral/Integral/Hab.var".
  67
  68 (* begin hide *)
  69
  70 inline "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__".
  71
  72 alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var".
  73
  74 alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var".
  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 alias id "n" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var".
 110
 111 alias id "P" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var".
 112
 113 alias id "e" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var".
 114
 115 alias id "He" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var".
 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 alias id "HmeshP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var".
 124
 125 alias id "fP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var".
 126
 127 alias id "HfP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var".
 128
 129 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var".
 130
 131 alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/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 alias id "a" = "cic:/CoRN/ftc/Integral/Basic_Properties/a.var".
 152
 153 alias id "b" = "cic:/CoRN/ftc/Integral/Basic_Properties/b.var".
 154
 155 alias id "Hab" = "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var".
 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 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var".
 172
 173 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var".
 174
 175 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var".
 176
 177 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var".
 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 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var".
 206
 207 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var".
 208
 209 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var".
 210
 211 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var".
 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 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var".
 232
 233 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var".
 234
 235 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var".
 236
 237 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var".
 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 alias id "alpha" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var".
 246
 247 alias id "beta" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var".
 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 alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var".
 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 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var".
 278
 279 alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var".
 280
 281 alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var".
 282
 283 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var".
 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 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var".
 323
 324 alias id "c" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var".
 325
 326 alias id "Hac" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var".
 327
 328 alias id "Hcb" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var".
 329
 330 alias id "Hab'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var".
 331
 332 alias id "Hac'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var".
 333
 334 alias id "Hcb'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var".
 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 alias id "n" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var".
 353
 354 alias id "m" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var".
 355
 356 alias id "P" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var".
 357
 358 alias id "Q" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var".
 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 alias id "fP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var".
 396
 397 alias id "HfP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var".
 398
 399 alias id "HfP'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var".
 400
 401 alias id "fQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var".
 402
 403 alias id "HfQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var".
 404
 405 alias id "HfQ'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var".
 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