helm/software/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 (* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 (*#* printing [-S-] %\ensuremath{\int}% #&int;# *)
  22
  23 (* INCLUDE
  24 MoreIntegrals
  25 *)
  26
  27 (* INCLUDE
  28 CalculusTheorems
  29 *)
  30
  31 (* UNEXPORTED
  32 Opaque Min.
  33 *)
  34
  35 (* UNEXPORTED
  36 Section Indefinite_Integral.
  37 *)
  38
  39 (*#* *The Fundamental Theorem of Calculus
  40
  41 Finally we can prove the fundamental theorem of calculus and its most
  42 important corollaries, which are the main tools to formalize most of
  43 real analysis.
  44
  45 **Indefinite Integrals
  46
  47 We define the indefinite integral of a function in a proper interval
  48 in the obvious way; we just need to state a first lemma so that the
  49 continuity proofs become unnecessary.
  50
  51 %\begin{convention}% Let [I : interval], [F : PartIR] be continuous in [I]
  52 and [a] be a point in [I].
  53 %\end{convention}%
  54 *)
  55
  56 inline cic:/CoRN/ftc/FTC/I.var.
  57
  58 inline cic:/CoRN/ftc/FTC/F.var.
  59
  60 inline cic:/CoRN/ftc/FTC/contF.var.
  61
  62 inline cic:/CoRN/ftc/FTC/a.var.
  63
  64 inline cic:/CoRN/ftc/FTC/Ha.var.
  65
  66 inline cic:/CoRN/ftc/FTC/prim_lemma.con.
  67
  68 inline cic:/CoRN/ftc/FTC/Fprim_strext.con.
  69
  70 inline cic:/CoRN/ftc/FTC/Fprim.con.
  71
  72 (* UNEXPORTED
  73 End Indefinite_Integral.
  74 *)
  75
  76 (* UNEXPORTED
  77 Implicit Arguments Fprim [I F].
  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 inline cic:/CoRN/ftc/FTC/J.var.
  96
  97 inline cic:/CoRN/ftc/FTC/F.var.
  98
  99 inline cic:/CoRN/ftc/FTC/contF.var.
 100
 101 inline cic:/CoRN/ftc/FTC/x0.var.
 102
 103 inline cic:/CoRN/ftc/FTC/Hx0.var.
 104
 105 (* begin hide *)
 106
 107 inline cic:/CoRN/ftc/FTC/G.con.
 108
 109 (* end hide *)
 110
 111 inline cic:/CoRN/ftc/FTC/Continuous_prim.con.
 112
 113 (*#*
 114 The derivative of [G] is simply [F].
 115 *)
 116
 117 inline cic:/CoRN/ftc/FTC/pJ.var.
 118
 119 inline 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 inline cic:/CoRN/ftc/FTC/G0.var.
 126
 127 inline cic:/CoRN/ftc/FTC/derG0.var.
 128
 129 inline 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 cic:/CoRN/ftc/FTC/G0_inc.con.
 138
 139 (* end hide *)
 140
 141 (* UNEXPORTED
 142 Opaque G.
 143 *)
 144
 145 inline 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 inline cic:/CoRN/ftc/FTC/J.var.
 182
 183 inline cic:/CoRN/ftc/FTC/f.var.
 184
 185 inline cic:/CoRN/ftc/FTC/F.var.
 186
 187 inline cic:/CoRN/ftc/FTC/contf.var.
 188
 189 inline cic:/CoRN/ftc/FTC/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 inline cic:/CoRN/ftc/FTC/a.var.
 206
 207 inline cic:/CoRN/ftc/FTC/b.var.
 208
 209 inline cic:/CoRN/ftc/FTC/Hab.var.
 210
 211 inline cic:/CoRN/ftc/FTC/contIf.var.
 212
 213 inline cic:/CoRN/ftc/FTC/contIF.var.
 214
 215 (* begin show *)
 216
 217 inline cic:/CoRN/ftc/FTC/convF.var.
 218
 219 (* end show *)
 220
 221 inline cic:/CoRN/ftc/FTC/x0.var.
 222
 223 inline cic:/CoRN/ftc/FTC/Hx0.var.
 224
 225 inline cic:/CoRN/ftc/FTC/Hx0'.var.
 226
 227 (* begin hide *)
 228
 229 inline cic:/CoRN/ftc/FTC/g.con.
 230
 231 inline cic:/CoRN/ftc/FTC/G.con.
 232
 233 (* end hide *)
 234
 235 (* begin show *)
 236
 237 inline cic:/CoRN/ftc/FTC/contg.var.
 238
 239 inline cic:/CoRN/ftc/FTC/contG.var.
 240
 241 (* end show *)
 242
 243 inline 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 cic:/CoRN/ftc/FTC/limit_of_integral.con.
 254
 255 inline 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 inline cic:/CoRN/ftc/FTC/convF.var.
 268
 269 (* end show *)
 270
 271 inline cic:/CoRN/ftc/FTC/x0.var.
 272
 273 inline cic:/CoRN/ftc/FTC/Hx0.var.
 274
 275 (* begin hide *)
 276
 277 inline cic:/CoRN/ftc/FTC/g.con.
 278
 279 inline cic:/CoRN/ftc/FTC/G.con.
 280
 281 (* end hide *)
 282
 283 inline cic:/CoRN/ftc/FTC/contg.var.
 284
 285 inline cic:/CoRN/ftc/FTC/contG.var.
 286
 287 inline 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 inline cic:/CoRN/ftc/FTC/J.var.
 309
 310 inline cic:/CoRN/ftc/FTC/pJ.var.
 311
 312 inline cic:/CoRN/ftc/FTC/f.var.
 313
 314 inline cic:/CoRN/ftc/FTC/g.var.
 315
 316 inline cic:/CoRN/ftc/FTC/F.var.
 317
 318 inline cic:/CoRN/ftc/FTC/G.var.
 319
 320 inline cic:/CoRN/ftc/FTC/contf.var.
 321
 322 inline cic:/CoRN/ftc/FTC/contF.var.
 323
 324 inline cic:/CoRN/ftc/FTC/convF.var.
 325
 326 inline cic:/CoRN/ftc/FTC/contg.var.
 327
 328 inline cic:/CoRN/ftc/FTC/contG.var.
 329
 330 inline cic:/CoRN/ftc/FTC/convG.var.
 331
 332 inline cic:/CoRN/ftc/FTC/derf.var.
 333
 334 inline 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 inline cic:/CoRN/ftc/FTC/J.var.
 349
 350 inline cic:/CoRN/ftc/FTC/pJ.var.
 351
 352 inline cic:/CoRN/ftc/FTC/f.var.
 353
 354 inline cic:/CoRN/ftc/FTC/g.var.
 355
 356 (* begin show *)
 357
 358 inline cic:/CoRN/ftc/FTC/convF.var.
 359
 360 inline cic:/CoRN/ftc/FTC/convG.var.
 361
 362 (* end show *)
 363
 364 inline cic:/CoRN/ftc/FTC/derF.var.
 365
 366 inline cic:/CoRN/ftc/FTC/Derivative_FSeries.con.
 367
 368 (* UNEXPORTED
 369 End Derivative_Series.
 370 *)
 371