helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/ftc/Derivative/Definitions/a.var".
  55
  56 alias id "b" = "cic:/CoRN/ftc/Derivative/Definitions/b.var".
  57
  58 alias id "Hab'" = "cic:/CoRN/ftc/Derivative/Definitions/Hab'.var".
  59
  60 (* begin hide *)
  61
  62 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/Hab.con" "Definitions__".
  63
  64 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/I.con" "Definitions__".
  65
  66 (* end hide *)
  67
  68 alias id "F" = "cic:/CoRN/ftc/Derivative/Definitions/F.var".
  69
  70 (* begin hide *)
  71
  72 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/P.con" "Definitions__".
  73
  74 (* end hide *)
  75
  76 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I.con".
  77
  78 (* UNEXPORTED
  79 End Definitions
  80 *)
  81
  82 (* UNEXPORTED
  83 Implicit Arguments Derivative_I [a b].
  84 *)
  85
  86 (* UNEXPORTED
  87 Section Basic_Properties
  88 *)
  89
  90 (*#* **Basic Properties
  91 *)
  92
  93 alias id "a" = "cic:/CoRN/ftc/Derivative/Basic_Properties/a.var".
  94
  95 alias id "b" = "cic:/CoRN/ftc/Derivative/Basic_Properties/b.var".
  96
  97 alias id "Hab'" = "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab'.var".
  98
  99 (* begin hide *)
 100
 101 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab.con" "Basic_Properties__".
 102
 103 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/I.con" "Basic_Properties__".
 104
 105 (* end hide *)
 106
 107 (*#*
 108 Like we did for equality, we begin by stating a lemma that makes proofs of derivation easier in practice.
 109 *)
 110
 111 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_char.con".
 112
 113 (* end hide *)
 114
 115 (*#*
 116 Derivative is a well defined relation; we will make this explicit for both arguments:
 117 *)
 118
 119 alias id "F" = "cic:/CoRN/ftc/Derivative/Basic_Properties/F.var".
 120
 121 alias id "G" = "cic:/CoRN/ftc/Derivative/Basic_Properties/G.var".
 122
 123 alias id "H" = "cic:/CoRN/ftc/Derivative/Basic_Properties/H.var".
 124
 125 (* begin hide *)
 126
 127 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/P.con" "Basic_Properties__".
 128
 129 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Q.con" "Basic_Properties__".
 130
 131 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/R.con" "Basic_Properties__".
 132
 133 (* end hide *)
 134
 135 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_wdl.con".
 136
 137 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_wdr.con".
 138
 139 (* begin hide *)
 140
 141 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Derivative_I_unique_lemma.con" "Basic_Properties__".
 142
 143 (* end hide *)
 144
 145 (*#*
 146 Derivative is unique.
 147 *)
 148
 149 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_unique.con".
 150
 151 (*#*
 152 Finally, the set where we are considering the relation is included in the domain of both functions.
 153 *)
 154
 155 inline procedural "cic:/CoRN/ftc/Derivative/derivative_imp_inc.con".
 156
 157 inline procedural "cic:/CoRN/ftc/Derivative/derivative_imp_inc'.con".
 158
 159 (*#*
 160 Any function that is or has a derivative is continuous.
 161 *)
 162
 163 alias id "Hab''" = "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab''.var".
 164
 165 inline procedural "cic:/CoRN/ftc/Derivative/deriv_imp_contin'_I.con".
 166
 167 inline procedural "cic:/CoRN/ftc/Derivative/deriv_imp_contin_I.con".
 168
 169 (* UNEXPORTED
 170 End Basic_Properties
 171 *)
 172
 173 (*#*
 174 If [G] is the derivative of [F] in a given interval, then [G] is also the derivative of [F] in any smaller interval.
 175 *)
 176
 177 inline procedural "cic:/CoRN/ftc/Derivative/included_imp_deriv.con".
 178