helm/software/matita/contribs/procedural/CoRN/ftc/FTC.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: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 (*#* printing [-S-] %\ensuremath{\int}% #&int;# *)
  22
  23 include "ftc/MoreIntegrals.ma".
  24
  25 include "ftc/CalculusTheorems.ma".
  26
  27 (* UNEXPORTED
  28 Opaque Min.
  29 *)
  30
  31 (* UNEXPORTED
  32 Section Indefinite_Integral
  33 *)
  34
  35 (*#* *The Fundamental Theorem of Calculus
  36
  37 Finally we can prove the fundamental theorem of calculus and its most
  38 important corollaries, which are the main tools to formalize most of
  39 real analysis.
  40
  41 **Indefinite Integrals
  42
  43 We define the indefinite integral of a function in a proper interval
  44 in the obvious way; we just need to state a first lemma so that the
  45 continuity proofs become unnecessary.
  46
  47 %\begin{convention}% Let [I : interval], [F : PartIR] be continuous in [I]
  48 and [a] be a point in [I].
  49 %\end{convention}%
  50 *)
  51
  52 (* UNEXPORTED
  53 cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var
  54 *)
  55
  56 (* UNEXPORTED
  57 cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var
  58 *)
  59
  60 (* UNEXPORTED
  61 cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var
  62 *)
  63
  64 (* UNEXPORTED
  65 cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var
  66 *)
  67
  68 (* UNEXPORTED
  69 cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var
  70 *)
  71
  72 inline procedural "cic:/CoRN/ftc/FTC/prim_lemma.con" as lemma.
  73
  74 inline procedural "cic:/CoRN/ftc/FTC/Fprim_strext.con" as lemma.
  75
  76 inline procedural "cic:/CoRN/ftc/FTC/Fprim.con" as definition.
  77
  78 (* UNEXPORTED
  79 End Indefinite_Integral
  80 *)
  81
  82 (* UNEXPORTED
  83 Implicit Arguments Fprim [I F].
  84 *)
  85
  86 (* NOTATION
  87 Notation "[-S-] F" := (Fprim F) (at level 20).
  88 *)
  89
  90 (* UNEXPORTED
  91 Section FTC
  92 *)
  93
  94 (*#* **The FTC
  95
  96 We can now prove our main theorem.  We begin by remarking that the
  97 primitive function is always continuous.
  98
  99 %\begin{convention}% Assume that [J : interval], [F : PartIR] is
 100 continuous in [J] and [x0] is a point in [J].  Denote by [G] the
 101 indefinite integral of [F] from [x0].
 102 %\end{convention}%
 103 *)
 104
 105 (* UNEXPORTED
 106 cic:/CoRN/ftc/FTC/FTC/J.var
 107 *)
 108
 109 (* UNEXPORTED
 110 cic:/CoRN/ftc/FTC/FTC/F.var
 111 *)
 112
 113 (* UNEXPORTED
 114 cic:/CoRN/ftc/FTC/FTC/contF.var
 115 *)
 116
 117 (* UNEXPORTED
 118 cic:/CoRN/ftc/FTC/FTC/x0.var
 119 *)
 120
 121 (* UNEXPORTED
 122 cic:/CoRN/ftc/FTC/FTC/Hx0.var
 123 *)
 124
 125 (* begin hide *)
 126
 127 inline procedural "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__" as definition.
 128
 129 (* end hide *)
 130
 131 inline procedural "cic:/CoRN/ftc/FTC/Continuous_prim.con" as lemma.
 132
 133 (*#*
 134 The derivative of [G] is simply [F].
 135 *)
 136
 137 (* UNEXPORTED
 138 cic:/CoRN/ftc/FTC/FTC/pJ.var
 139 *)
 140
 141 inline procedural "cic:/CoRN/ftc/FTC/FTC1.con" as theorem.
 142
 143 (*#*
 144 Any other function [G0] with derivative [F] must differ from [G] by a constant.
 145 *)
 146
 147 (* UNEXPORTED
 148 cic:/CoRN/ftc/FTC/FTC/G0.var
 149 *)
 150
 151 (* UNEXPORTED
 152 cic:/CoRN/ftc/FTC/FTC/derG0.var
 153 *)
 154
 155 inline procedural "cic:/CoRN/ftc/FTC/FTC2.con" as theorem.
 156
 157 (*#*
 158 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
 159 *)
 160
 161 (* begin hide *)
 162
 163 inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__" as definition.
 164
 165 (* end hide *)
 166
 167 (* UNEXPORTED
 168 Opaque G.
 169 *)
 170
 171 inline procedural "cic:/CoRN/ftc/FTC/Barrow.con" as theorem.
 172
 173 (* end hide *)
 174
 175 (* UNEXPORTED
 176 End FTC
 177 *)
 178
 179 (* UNEXPORTED
 180 Hint Resolve Continuous_prim: continuous.
 181 *)
 182
 183 (* UNEXPORTED
 184 Hint Resolve FTC1: derivate.
 185 *)
 186
 187 (* UNEXPORTED
 188 Section Limit_of_Integral_Seq
 189 *)
 190
 191 (*#* **Corollaries
 192
 193 With these tools in our hand, we can prove several useful results.
 194
 195 %\begin{convention}% From this point onwards:
 196  - [J : interval];
 197  - [f : nat->PartIR] is a sequence of continuous functions (in [J]);
 198  - [F : PartIR] is continuous in [J].
 199
 200 %\end{convention}%
 201
 202 In the first place, if a sequence of continuous functions converges
 203 then the sequence of their primitives also converges, and the limit
 204 commutes with the indefinite integral.
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var
 209 *)
 210
 211 (* UNEXPORTED
 212 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var
 213 *)
 214
 215 (* UNEXPORTED
 216 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var
 217 *)
 218
 219 (* UNEXPORTED
 220 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var
 221 *)
 222
 223 (* UNEXPORTED
 224 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var
 225 *)
 226
 227 (* UNEXPORTED
 228 Section Compact
 229 *)
 230
 231 (*#*
 232 We need to prove this result first for compact intervals.
 233
 234 %\begin{convention}% Assume that [a, b, x0 : IR] with [(f n)] and [F]
 235 continuous in [[a,b]], $x0\in[a,b]$#x0&isin;[a,b]#; denote by
 236 [(g n)] and [G] the indefinite integrals respectively of [(f n)] and
 237 [F] with origin [x0].
 238 %\end{convention}%
 239 *)
 240
 241 (* UNEXPORTED
 242 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var
 243 *)
 244
 245 (* UNEXPORTED
 246 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var
 247 *)
 248
 249 (* UNEXPORTED
 250 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var
 251 *)
 252
 253 (* UNEXPORTED
 254 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var
 255 *)
 256
 257 (* UNEXPORTED
 258 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var
 259 *)
 260
 261 (* begin show *)
 262
 263 (* UNEXPORTED
 264 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var
 265 *)
 266
 267 (* end show *)
 268
 269 (* UNEXPORTED
 270 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var
 271 *)
 272
 273 (* UNEXPORTED
 274 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var
 275 *)
 276
 277 (* UNEXPORTED
 278 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var
 279 *)
 280
 281 (* begin hide *)
 282
 283 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__" as definition.
 284
 285 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__" as definition.
 286
 287 (* end hide *)
 288
 289 (* begin show *)
 290
 291 (* UNEXPORTED
 292 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var
 293 *)
 294
 295 (* UNEXPORTED
 296 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var
 297 *)
 298
 299 (* end show *)
 300
 301 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con" as lemma.
 302
 303 (* UNEXPORTED
 304 End Compact
 305 *)
 306
 307 (*#*
 308 And now we can generalize it step by step.
 309 *)
 310
 311 inline procedural "cic:/CoRN/ftc/FTC/limit_of_integral.con" as lemma.
 312
 313 inline procedural "cic:/CoRN/ftc/FTC/limit_of_Integral.con" as lemma.
 314
 315 (* UNEXPORTED
 316 Section General
 317 *)
 318
 319 (*#*
 320 Finally, with [x0, g, G] as before,
 321 *)
 322
 323 (* begin show *)
 324
 325 (* UNEXPORTED
 326 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var
 327 *)
 328
 329 (* end show *)
 330
 331 (* UNEXPORTED
 332 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var
 333 *)
 334
 335 (* UNEXPORTED
 336 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var
 337 *)
 338
 339 (* begin hide *)
 340
 341 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__" as definition.
 342
 343 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__" as definition.
 344
 345 (* end hide *)
 346
 347 (* UNEXPORTED
 348 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var
 349 *)
 350
 351 (* UNEXPORTED
 352 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var
 353 *)
 354
 355 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con" as lemma.
 356
 357 (* UNEXPORTED
 358 End General
 359 *)
 360
 361 (* UNEXPORTED
 362 End Limit_of_Integral_Seq
 363 *)
 364
 365 (* UNEXPORTED
 366 Section Limit_of_Derivative_Seq
 367 *)
 368
 369 (*#*
 370 Similar results hold for the sequence of derivatives of a converging sequence; this time the proof is easier, as we can do it directly for any kind of interval.
 371
 372 %\begin{convention}% Let [g] be the sequence of derivatives of [f] and [G] be the derivative of [F].
 373 %\end{convention}%
 374 *)
 375
 376 (* UNEXPORTED
 377 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var
 378 *)
 379
 380 (* UNEXPORTED
 381 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var
 382 *)
 383
 384 (* UNEXPORTED
 385 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var
 386 *)
 387
 388 (* UNEXPORTED
 389 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var
 390 *)
 391
 392 (* UNEXPORTED
 393 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var
 394 *)
 395
 396 (* UNEXPORTED
 397 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var
 398 *)
 399
 400 (* UNEXPORTED
 401 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var
 402 *)
 403
 404 (* UNEXPORTED
 405 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var
 406 *)
 407
 408 (* UNEXPORTED
 409 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var
 410 *)
 411
 412 (* UNEXPORTED
 413 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var
 414 *)
 415
 416 (* UNEXPORTED
 417 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var
 418 *)
 419
 420 (* UNEXPORTED
 421 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var
 422 *)
 423
 424 (* UNEXPORTED
 425 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var
 426 *)
 427
 428 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con" as lemma.
 429
 430 (* UNEXPORTED
 431 End Limit_of_Derivative_Seq
 432 *)
 433
 434 (* UNEXPORTED
 435 Section Derivative_Series
 436 *)
 437
 438 (*#*
 439 As a very important case of this result, we get a rule for deriving series.
 440 *)
 441
 442 (* UNEXPORTED
 443 cic:/CoRN/ftc/FTC/Derivative_Series/J.var
 444 *)
 445
 446 (* UNEXPORTED
 447 cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var
 448 *)
 449
 450 (* UNEXPORTED
 451 cic:/CoRN/ftc/FTC/Derivative_Series/f.var
 452 *)
 453
 454 (* UNEXPORTED
 455 cic:/CoRN/ftc/FTC/Derivative_Series/g.var
 456 *)
 457
 458 (* begin show *)
 459
 460 (* UNEXPORTED
 461 cic:/CoRN/ftc/FTC/Derivative_Series/convF.var
 462 *)
 463
 464 (* UNEXPORTED
 465 cic:/CoRN/ftc/FTC/Derivative_Series/convG.var
 466 *)
 467
 468 (* end show *)
 469
 470 (* UNEXPORTED
 471 cic:/CoRN/ftc/FTC/Derivative_Series/derF.var
 472 *)
 473
 474 inline procedural "cic:/CoRN/ftc/FTC/Derivative_FSeries.con" as lemma.
 475
 476 (* UNEXPORTED
 477 End Derivative_Series
 478 *)
 479