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