helm/software/matita/contribs/CoRN-Procedural/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 alias id "I" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var".
  53
  54 alias id "F" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var".
  55
  56 alias id "contF" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var".
  57
  58 alias id "a" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var".
  59
  60 alias id "Ha" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var".
  61
  62 inline procedural "cic:/CoRN/ftc/FTC/prim_lemma.con".
  63
  64 inline procedural "cic:/CoRN/ftc/FTC/Fprim_strext.con".
  65
  66 inline procedural "cic:/CoRN/ftc/FTC/Fprim.con".
  67
  68 (* UNEXPORTED
  69 End Indefinite_Integral
  70 *)
  71
  72 (* UNEXPORTED
  73 Implicit Arguments Fprim [I F].
  74 *)
  75
  76 (* NOTATION
  77 Notation "[-S-] F" := (Fprim F) (at level 20).
  78 *)
  79
  80 (* UNEXPORTED
  81 Section FTC
  82 *)
  83
  84 (*#* **The FTC
  85
  86 We can now prove our main theorem.  We begin by remarking that the
  87 primitive function is always continuous.
  88
  89 %\begin{convention}% Assume that [J : interval], [F : PartIR] is
  90 continuous in [J] and [x0] is a point in [J].  Denote by [G] the
  91 indefinite integral of [F] from [x0].
  92 %\end{convention}%
  93 *)
  94
  95 alias id "J" = "cic:/CoRN/ftc/FTC/FTC/J.var".
  96
  97 alias id "F" = "cic:/CoRN/ftc/FTC/FTC/F.var".
  98
  99 alias id "contF" = "cic:/CoRN/ftc/FTC/FTC/contF.var".
 100
 101 alias id "x0" = "cic:/CoRN/ftc/FTC/FTC/x0.var".
 102
 103 alias id "Hx0" = "cic:/CoRN/ftc/FTC/FTC/Hx0.var".
 104
 105 (* begin hide *)
 106
 107 inline procedural "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__".
 108
 109 (* end hide *)
 110
 111 inline procedural "cic:/CoRN/ftc/FTC/Continuous_prim.con".
 112
 113 (*#*
 114 The derivative of [G] is simply [F].
 115 *)
 116
 117 alias id "pJ" = "cic:/CoRN/ftc/FTC/FTC/pJ.var".
 118
 119 inline procedural "cic:/CoRN/ftc/FTC/FTC1.con".
 120
 121 (*#*
 122 Any other function [G0] with derivative [F] must differ from [G] by a constant.
 123 *)
 124
 125 alias id "G0" = "cic:/CoRN/ftc/FTC/FTC/G0.var".
 126
 127 alias id "derG0" = "cic:/CoRN/ftc/FTC/FTC/derG0.var".
 128
 129 inline procedural "cic:/CoRN/ftc/FTC/FTC2.con".
 130
 131 (*#*
 132 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
 133 *)
 134
 135 (* begin hide *)
 136
 137 inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__".
 138
 139 (* end hide *)
 140
 141 (* UNEXPORTED
 142 Opaque G.
 143 *)
 144
 145 inline procedural "cic:/CoRN/ftc/FTC/Barrow.con".
 146
 147 (* end hide *)
 148
 149 (* UNEXPORTED
 150 End FTC
 151 *)
 152
 153 (* UNEXPORTED
 154 Hint Resolve Continuous_prim: continuous.
 155 *)
 156
 157 (* UNEXPORTED
 158 Hint Resolve FTC1: derivate.
 159 *)
 160
 161 (* UNEXPORTED
 162 Section Limit_of_Integral_Seq
 163 *)
 164
 165 (*#* **Corollaries
 166
 167 With these tools in our hand, we can prove several useful results.
 168
 169 %\begin{convention}% From this point onwards:
 170  - [J : interval];
 171  - [f : nat->PartIR] is a sequence of continuous functions (in [J]);
 172  - [F : PartIR] is continuous in [J].
 173
 174 %\end{convention}%
 175
 176 In the first place, if a sequence of continuous functions converges
 177 then the sequence of their primitives also converges, and the limit
 178 commutes with the indefinite integral.
 179 *)
 180
 181 alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var".
 182
 183 alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var".
 184
 185 alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var".
 186
 187 alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var".
 188
 189 alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var".
 190
 191 (* UNEXPORTED
 192 Section Compact
 193 *)
 194
 195 (*#*
 196 We need to prove this result first for compact intervals.
 197
 198 %\begin{convention}% Assume that [a, b, x0 : IR] with [(f n)] and [F]
 199 continuous in [[a,b]], $x0\in[a,b]$#x0&isin;[a,b]#; denote by
 200 [(g n)] and [G] the indefinite integrals respectively of [(f n)] and
 201 [F] with origin [x0].
 202 %\end{convention}%
 203 *)
 204
 205 alias id "a" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var".
 206
 207 alias id "b" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var".
 208
 209 alias id "Hab" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var".
 210
 211 alias id "contIf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var".
 212
 213 alias id "contIF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var".
 214
 215 (* begin show *)
 216
 217 alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var".
 218
 219 (* end show *)
 220
 221 alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var".
 222
 223 alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var".
 224
 225 alias id "Hx0'" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var".
 226
 227 (* begin hide *)
 228
 229 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__".
 230
 231 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__".
 232
 233 (* end hide *)
 234
 235 (* begin show *)
 236
 237 alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var".
 238
 239 alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var".
 240
 241 (* end show *)
 242
 243 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con".
 244
 245 (* UNEXPORTED
 246 End Compact
 247 *)
 248
 249 (*#*
 250 And now we can generalize it step by step.
 251 *)
 252
 253 inline procedural "cic:/CoRN/ftc/FTC/limit_of_integral.con".
 254
 255 inline procedural "cic:/CoRN/ftc/FTC/limit_of_Integral.con".
 256
 257 (* UNEXPORTED
 258 Section General
 259 *)
 260
 261 (*#*
 262 Finally, with [x0, g, G] as before,
 263 *)
 264
 265 (* begin show *)
 266
 267 alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var".
 268
 269 (* end show *)
 270
 271 alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var".
 272
 273 alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var".
 274
 275 (* begin hide *)
 276
 277 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__".
 278
 279 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__".
 280
 281 (* end hide *)
 282
 283 alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var".
 284
 285 alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var".
 286
 287 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con".
 288
 289 (* UNEXPORTED
 290 End General
 291 *)
 292
 293 (* UNEXPORTED
 294 End Limit_of_Integral_Seq
 295 *)
 296
 297 (* UNEXPORTED
 298 Section Limit_of_Derivative_Seq
 299 *)
 300
 301 (*#*
 302 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.
 303
 304 %\begin{convention}% Let [g] be the sequence of derivatives of [f] and [G] be the derivative of [F].
 305 %\end{convention}%
 306 *)
 307
 308 alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var".
 309
 310 alias id "pJ" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var".
 311
 312 alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var".
 313
 314 alias id "g" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var".
 315
 316 alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var".
 317
 318 alias id "G" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var".
 319
 320 alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var".
 321
 322 alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var".
 323
 324 alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var".
 325
 326 alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var".
 327
 328 alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var".
 329
 330 alias id "convG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var".
 331
 332 alias id "derf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var".
 333
 334 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con".
 335
 336 (* UNEXPORTED
 337 End Limit_of_Derivative_Seq
 338 *)
 339
 340 (* UNEXPORTED
 341 Section Derivative_Series
 342 *)
 343
 344 (*#*
 345 As a very important case of this result, we get a rule for deriving series.
 346 *)
 347
 348 alias id "J" = "cic:/CoRN/ftc/FTC/Derivative_Series/J.var".
 349
 350 alias id "pJ" = "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var".
 351
 352 alias id "f" = "cic:/CoRN/ftc/FTC/Derivative_Series/f.var".
 353
 354 alias id "g" = "cic:/CoRN/ftc/FTC/Derivative_Series/g.var".
 355
 356 (* begin show *)
 357
 358 alias id "convF" = "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var".
 359
 360 alias id "convG" = "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var".
 361
 362 (* end show *)
 363
 364 alias id "derF" = "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var".
 365
 366 inline procedural "cic:/CoRN/ftc/FTC/Derivative_FSeries.con".
 367
 368 (* UNEXPORTED
 369 End Derivative_Series
 370 *)
 371