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