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