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