helm/software/matita/contribs/procedural/CoRN/ftc/Derivative.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: Derivative.v,v 1.7 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 include "ftc/Continuity.ma".
  22
  23 (* UNEXPORTED
  24 Section Definitions
  25 *)
  26
  27 (*#* *Derivatives
  28
  29 We will now proceed toward the development of differential calculus.
  30 To begin with, the main notion is that of derivative.
  31
  32 At this stage we will not define a notion of differentiable function,
  33 mainly because the natural definition (that of being a function which
  34 has some derivative) poses some technical problems; thus, we will
  35 postpone that part of our work to a subsequent stage.
  36
  37 Derivative is a binary relation in the type of partial functions,
  38 dependent (once again) on a compact interval with distinct
  39 endpoints#. #%\footnote{%As before, we do not define pointwise
  40 differentiability, mainly for coherence reasons.  See Bishop [1967]
  41 for a discussion on the relative little interest of that concept.%}.%
  42 The reason for requiring the endpoints to be apart is mainly to be
  43 able to derive the usual properties of the derivative
  44 relation---namely, that any two derivatives of the same function must
  45 coincide.
  46
  47 %\begin{convention}% Let [a,b:IR] with [a [<] b] and denote by [I] the
  48 interval [[a,b]].  Throughout this chapter, [F, F', G, G'] and [H]
  49 will be partial functions with domains respectively [P, P', Q, Q'] and
  50 [R].
  51 %\end{convention}%
  52 *)
  53
  54 (* UNEXPORTED
  55 cic:/CoRN/ftc/Derivative/Definitions/a.var
  56 *)
  57
  58 (* UNEXPORTED
  59 cic:/CoRN/ftc/Derivative/Definitions/b.var
  60 *)
  61
  62 (* UNEXPORTED
  63 cic:/CoRN/ftc/Derivative/Definitions/Hab'.var
  64 *)
  65
  66 (* begin hide *)
  67
  68 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/Hab.con" "Definitions__" as definition.
  69
  70 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/I.con" "Definitions__" as definition.
  71
  72 (* end hide *)
  73
  74 (* UNEXPORTED
  75 cic:/CoRN/ftc/Derivative/Definitions/F.var
  76 *)
  77
  78 (* begin hide *)
  79
  80 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/P.con" "Definitions__" as definition.
  81
  82 (* end hide *)
  83
  84 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I.con" as definition.
  85
  86 (* UNEXPORTED
  87 End Definitions
  88 *)
  89
  90 (* UNEXPORTED
  91 Implicit Arguments Derivative_I [a b].
  92 *)
  93
  94 (* UNEXPORTED
  95 Section Basic_Properties
  96 *)
  97
  98 (*#* **Basic Properties
  99 *)
 100
 101 (* UNEXPORTED
 102 cic:/CoRN/ftc/Derivative/Basic_Properties/a.var
 103 *)
 104
 105 (* UNEXPORTED
 106 cic:/CoRN/ftc/Derivative/Basic_Properties/b.var
 107 *)
 108
 109 (* UNEXPORTED
 110 cic:/CoRN/ftc/Derivative/Basic_Properties/Hab'.var
 111 *)
 112
 113 (* begin hide *)
 114
 115 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab.con" "Basic_Properties__" as definition.
 116
 117 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/I.con" "Basic_Properties__" as definition.
 118
 119 (* end hide *)
 120
 121 (*#*
 122 Like we did for equality, we begin by stating a lemma that makes proofs of derivation easier in practice.
 123 *)
 124
 125 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_char.con" as lemma.
 126
 127 (* end hide *)
 128
 129 (*#*
 130 Derivative is a well defined relation; we will make this explicit for both arguments:
 131 *)
 132
 133 (* UNEXPORTED
 134 cic:/CoRN/ftc/Derivative/Basic_Properties/F.var
 135 *)
 136
 137 (* UNEXPORTED
 138 cic:/CoRN/ftc/Derivative/Basic_Properties/G.var
 139 *)
 140
 141 (* UNEXPORTED
 142 cic:/CoRN/ftc/Derivative/Basic_Properties/H.var
 143 *)
 144
 145 (* begin hide *)
 146
 147 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/P.con" "Basic_Properties__" as definition.
 148
 149 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Q.con" "Basic_Properties__" as definition.
 150
 151 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/R.con" "Basic_Properties__" as definition.
 152
 153 (* end hide *)
 154
 155 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_wdl.con" as lemma.
 156
 157 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_wdr.con" as lemma.
 158
 159 (* begin hide *)
 160
 161 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Derivative_I_unique_lemma.con" "Basic_Properties__" as definition.
 162
 163 (* end hide *)
 164
 165 (*#*
 166 Derivative is unique.
 167 *)
 168
 169 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_unique.con" as lemma.
 170
 171 (*#*
 172 Finally, the set where we are considering the relation is included in the domain of both functions.
 173 *)
 174
 175 inline procedural "cic:/CoRN/ftc/Derivative/derivative_imp_inc.con" as lemma.
 176
 177 inline procedural "cic:/CoRN/ftc/Derivative/derivative_imp_inc'.con" as lemma.
 178
 179 (*#*
 180 Any function that is or has a derivative is continuous.
 181 *)
 182
 183 (* UNEXPORTED
 184 cic:/CoRN/ftc/Derivative/Basic_Properties/Hab''.var
 185 *)
 186
 187 inline procedural "cic:/CoRN/ftc/Derivative/deriv_imp_contin'_I.con" as lemma.
 188
 189 inline procedural "cic:/CoRN/ftc/Derivative/deriv_imp_contin_I.con" as lemma.
 190
 191 (* UNEXPORTED
 192 End Basic_Properties
 193 *)
 194
 195 (*#*
 196 If [G] is the derivative of [F] in a given interval, then [G] is also the derivative of [F] in any smaller interval.
 197 *)
 198
 199 inline procedural "cic:/CoRN/ftc/Derivative/included_imp_deriv.con" as lemma.
 200