helm/software/matita/contribs/procedural/CoRN/ftc/CalculusTheorems.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: CalculusTheorems.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
  20
  21 include "ftc/Rolle.ma".
  22
  23 include "tactics/DiffTactics3.ma".
  24
  25 (* UNEXPORTED
  26 Opaque Min Max.
  27 *)
  28
  29 (* UNEXPORTED
  30 Section Various_Theorems
  31 *)
  32
  33 (*#* *Calculus Theorems
  34
  35 This file is intended to present a collection of miscellaneous, mostly
  36 technical results in differential calculus that are interesting or
  37 useful in future work.
  38
  39 We begin with some properties of continuous functions.  Every
  40 continuous function commutes with the limit of a numerical sequence
  41 (sometimes called Heine continuity).
  42 *)
  43
  44 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_comm_Lim.con" as lemma.
  45
  46 (*#*
  47 This is a tricky result: if [F] is continuous and positive in both [[a,b]]
  48 and [(b,c]], then it is positive in [[a,c]].
  49 *)
  50
  51 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_pos.con" as lemma.
  52
  53 (*#*
  54 Similar results for increasing functions:
  55 *)
  56
  57 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues.con" as lemma.
  58
  59 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues'.con" as lemma.
  60
  61 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues.con" as lemma.
  62
  63 inline procedural "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues'.con" as lemma.
  64
  65 (*#* More on glueing intervals. *)
  66
  67 inline procedural "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clor_nonneg.con" as lemma.
  68
  69 inline procedural "cic:/CoRN/ftc/CalculusTheorems/olor_pos_olcr_nonneg.con" as lemma.
  70
  71 inline procedural "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clcr_nonneg.con" as lemma.
  72
  73 (*#*
  74 Any function that has the null function as its derivative must be constant.
  75 *)
  76
  77 inline procedural "cic:/CoRN/ftc/CalculusTheorems/FConst_prop.con" as lemma.
  78
  79 (*#* As a corollary, two functions with the same derivative must differ
  80 by a constant.
  81 *)
  82
  83 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Feq_crit_with_const.con" as lemma.
  84
  85 (*#* This yields the following known result: any differential equation
  86 of the form [f'=g] with initial condition [f(a) [=] b] has a unique solution.
  87 *)
  88
  89 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Feq_criterium.con" as lemma.
  90
  91 (*#*
  92 Finally, a well known result: any function with a (strictly) positive
  93 derivative is (strictly) increasing.  Although the two lemmas look
  94 quite similar the proofs are completely different, both from the
  95 formalization and from the mathematical point of view.
  96 *)
  97
  98 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_leEq.con" as lemma.
 101
 102 inline procedural "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less'.con" as lemma.
 103
 104 (*#* From these results we can finally prove that exponentiation to a
 105 real power preserves the less or equal than relation!
 106 *)
 107
 108 (* UNEXPORTED
 109 Opaque nring.
 110 *)
 111
 112 (* UNEXPORTED
 113 Transparent nring.
 114 *)
 115
 116 inline procedural "cic:/CoRN/ftc/CalculusTheorems/nexp_resp_leEq_odd.con" as lemma.
 117
 118 (* UNEXPORTED
 119 End Various_Theorems
 120 *)
 121