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 (* $Id: Derivative.v,v 1.7 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 Continuity
  23 *)
  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 inline cic:/CoRN/ftc/Derivative/a.var.
  57
  58 inline cic:/CoRN/ftc/Derivative/b.var.
  59
  60 inline cic:/CoRN/ftc/Derivative/Hab'.var.
  61
  62 (* begin hide *)
  63
  64 inline cic:/CoRN/ftc/Derivative/Hab.con.
  65
  66 inline cic:/CoRN/ftc/Derivative/I.con.
  67
  68 (* end hide *)
  69
  70 inline cic:/CoRN/ftc/Derivative/F.var.
  71
  72 (* begin hide *)
  73
  74 inline cic:/CoRN/ftc/Derivative/P.con.
  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 inline cic:/CoRN/ftc/Derivative/a.var.
  96
  97 inline cic:/CoRN/ftc/Derivative/b.var.
  98
  99 inline cic:/CoRN/ftc/Derivative/Hab'.var.
 100
 101 (* begin hide *)
 102
 103 inline cic:/CoRN/ftc/Derivative/Hab.con.
 104
 105 inline cic:/CoRN/ftc/Derivative/I.con.
 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 inline cic:/CoRN/ftc/Derivative/F.var.
 122
 123 inline cic:/CoRN/ftc/Derivative/G.var.
 124
 125 inline cic:/CoRN/ftc/Derivative/H.var.
 126
 127 (* begin hide *)
 128
 129 inline cic:/CoRN/ftc/Derivative/P.con.
 130
 131 inline cic:/CoRN/ftc/Derivative/Q.con.
 132
 133 inline cic:/CoRN/ftc/Derivative/R.con.
 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/Derivative_I_unique_lemma.con.
 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 inline cic:/CoRN/ftc/Derivative/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