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