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 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 inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var" "Indefinite_Integral__".
  55
  56 inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var" "Indefinite_Integral__".
  57
  58 inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var" "Indefinite_Integral__".
  59
  60 inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var" "Indefinite_Integral__".
  61
  62 inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var" "Indefinite_Integral__".
  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 inline "cic:/CoRN/ftc/FTC/FTC/J.var" "FTC__".
  98
  99 inline "cic:/CoRN/ftc/FTC/FTC/F.var" "FTC__".
 100
 101 inline "cic:/CoRN/ftc/FTC/FTC/contF.var" "FTC__".
 102
 103 inline "cic:/CoRN/ftc/FTC/FTC/x0.var" "FTC__".
 104
 105 inline "cic:/CoRN/ftc/FTC/FTC/Hx0.var" "FTC__".
 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 inline "cic:/CoRN/ftc/FTC/FTC/pJ.var" "FTC__".
 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 inline "cic:/CoRN/ftc/FTC/FTC/G0.var" "FTC__".
 128
 129 inline "cic:/CoRN/ftc/FTC/FTC/derG0.var" "FTC__".
 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 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var" "Limit_of_Integral_Seq__".
 184
 185 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var" "Limit_of_Integral_Seq__".
 186
 187 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var" "Limit_of_Integral_Seq__".
 188
 189 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var" "Limit_of_Integral_Seq__".
 190
 191 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var" "Limit_of_Integral_Seq__".
 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 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var" "Limit_of_Integral_Seq__Compact__".
 208
 209 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var" "Limit_of_Integral_Seq__Compact__".
 210
 211 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var" "Limit_of_Integral_Seq__Compact__".
 212
 213 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var" "Limit_of_Integral_Seq__Compact__".
 214
 215 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var" "Limit_of_Integral_Seq__Compact__".
 216
 217 (* begin show *)
 218
 219 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var" "Limit_of_Integral_Seq__Compact__".
 220
 221 (* end show *)
 222
 223 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var" "Limit_of_Integral_Seq__Compact__".
 224
 225 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var" "Limit_of_Integral_Seq__Compact__".
 226
 227 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var" "Limit_of_Integral_Seq__Compact__".
 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 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var" "Limit_of_Integral_Seq__Compact__".
 240
 241 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var" "Limit_of_Integral_Seq__Compact__".
 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 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var" "Limit_of_Integral_Seq__General__".
 270
 271 (* end show *)
 272
 273 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var" "Limit_of_Integral_Seq__General__".
 274
 275 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var" "Limit_of_Integral_Seq__General__".
 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 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var" "Limit_of_Integral_Seq__General__".
 286
 287 inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var" "Limit_of_Integral_Seq__General__".
 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 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var" "Limit_of_Derivative_Seq__".
 311
 312 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var" "Limit_of_Derivative_Seq__".
 313
 314 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var" "Limit_of_Derivative_Seq__".
 315
 316 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var" "Limit_of_Derivative_Seq__".
 317
 318 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var" "Limit_of_Derivative_Seq__".
 319
 320 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var" "Limit_of_Derivative_Seq__".
 321
 322 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var" "Limit_of_Derivative_Seq__".
 323
 324 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var" "Limit_of_Derivative_Seq__".
 325
 326 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var" "Limit_of_Derivative_Seq__".
 327
 328 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var" "Limit_of_Derivative_Seq__".
 329
 330 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var" "Limit_of_Derivative_Seq__".
 331
 332 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var" "Limit_of_Derivative_Seq__".
 333
 334 inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var" "Limit_of_Derivative_Seq__".
 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 inline "cic:/CoRN/ftc/FTC/Derivative_Series/J.var" "Derivative_Series__".
 351
 352 inline "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var" "Derivative_Series__".
 353
 354 inline "cic:/CoRN/ftc/FTC/Derivative_Series/f.var" "Derivative_Series__".
 355
 356 inline "cic:/CoRN/ftc/FTC/Derivative_Series/g.var" "Derivative_Series__".
 357
 358 (* begin show *)
 359
 360 inline "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var" "Derivative_Series__".
 361
 362 inline "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var" "Derivative_Series__".
 363
 364 (* end show *)
 365
 366 inline "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var" "Derivative_Series__".
 367
 368 inline "cic:/CoRN/ftc/FTC/Derivative_FSeries.con".
 369
 370 (* UNEXPORTED
 371 End Derivative_Series
 372 *)
 373