helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.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/Differentiability".
  18
  19 (* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
  20
  21 (* INCLUDE
  22 PartInterval
  23 *)
  24
  25 (* INCLUDE
  26 DerivativeOps
  27 *)
  28
  29 (* UNEXPORTED
  30 Section Definitions.
  31 *)
  32
  33 (*#* *Differentiability
  34
  35 We will now use our work on derivatives to define a notion of
  36 differentiable function and prove its main properties.
  37
  38 %\begin{convention}% Throughout this section, [a,b] will be real
  39 numbers with [a [<] b], [I] will denote the interval [[a,b]]
  40 and [F,G,H] will be differentiable functions.
  41 %\end{convention}%
  42
  43 Usually a function [F] is said to be differentiable in a proper
  44 compact interval [[a,b]] if there exists another function [F']
  45 such that [F'] is a derivative of [F] in that interval.  There is a
  46 problem in formalizing this definition, as we pointed out earlier on,
  47 which is that if we simply write it down as is we are not able to get
  48 such a function [F'] from a hypothesis that [F] is differentiable.
  49
  50 However, it turns out that this is not altogether the best definition
  51 for the following reason: if we say that [F] is differentiable in
  52 [[a,b]], we mean that there is a partial function [F'] which is
  53 defined in [[a,b]] and satisfies a certain condition in that
  54 interval but nothing is required of the behaviour of the function
  55 outside [[a,b]].  Thus we can argue that, from a mathematical
  56 point of view, the [F'] that we get eliminating a hypothesis of
  57 differentiability should be defined exactly on that interval.  If we
  58 do this, we can quantify over the set of setoid functions in that
  59 interval and eliminate the existencial quantifier without any
  60 problems.
  61 *)
  62
  63 inline cic:/CoRN/ftc/Differentiability/Diffble_I.con.
  64
  65 (* UNEXPORTED
  66 End Definitions.
  67 *)
  68
  69 (* UNEXPORTED
  70 Implicit Arguments Diffble_I [a b].
  71 *)
  72
  73 (* UNEXPORTED
  74 Section Local_Properties.
  75 *)
  76
  77 (*#*
  78 From this point on, we just prove results analogous to the ones for derivability.
  79
  80 A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]].
  81 *)
  82
  83 inline cic:/CoRN/ftc/Differentiability/included_imp_diffble.con.
  84
  85 (*#*
  86 A function differentiable in an interval is everywhere defined in that interval.
  87 *)
  88
  89 inline cic:/CoRN/ftc/Differentiability/a.var.
  90
  91 inline cic:/CoRN/ftc/Differentiability/b.var.
  92
  93 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
  94
  95 (* begin hide *)
  96
  97 inline cic:/CoRN/ftc/Differentiability/Hab.con.
  98
  99 inline cic:/CoRN/ftc/Differentiability/I.con.
 100
 101 (* end hide *)
 102
 103 inline cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con.
 104
 105 (*#*
 106 If a function has a derivative in an interval then it is differentiable in that interval.
 107 *)
 108
 109 inline cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con.
 110
 111 (* UNEXPORTED
 112 End Local_Properties.
 113 *)
 114
 115 (* UNEXPORTED
 116 Hint Resolve diffble_imp_inc: included.
 117 *)
 118
 119 (* UNEXPORTED
 120 Section Operations.
 121 *)
 122
 123 (*#*
 124 All the algebraic results carry on.
 125 *)
 126
 127 inline cic:/CoRN/ftc/Differentiability/a.var.
 128
 129 inline cic:/CoRN/ftc/Differentiability/b.var.
 130
 131 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
 132
 133 (* begin hide *)
 134
 135 inline cic:/CoRN/ftc/Differentiability/Hab.con.
 136
 137 inline cic:/CoRN/ftc/Differentiability/I.con.
 138
 139 (* end hide *)
 140
 141 (* UNEXPORTED
 142 Section Constants.
 143 *)
 144
 145 inline cic:/CoRN/ftc/Differentiability/Diffble_I_const.con.
 146
 147 inline cic:/CoRN/ftc/Differentiability/Diffble_I_id.con.
 148
 149 (* UNEXPORTED
 150 End Constants.
 151 *)
 152
 153 (* UNEXPORTED
 154 Section Well_Definedness.
 155 *)
 156
 157 inline cic:/CoRN/ftc/Differentiability/F.var.
 158
 159 inline cic:/CoRN/ftc/Differentiability/H.var.
 160
 161 inline cic:/CoRN/ftc/Differentiability/diffF.var.
 162
 163 inline cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con.
 164
 165 (* UNEXPORTED
 166 End Well_Definedness.
 167 *)
 168
 169 inline cic:/CoRN/ftc/Differentiability/F.var.
 170
 171 inline cic:/CoRN/ftc/Differentiability/G.var.
 172
 173 inline cic:/CoRN/ftc/Differentiability/diffF.var.
 174
 175 inline cic:/CoRN/ftc/Differentiability/diffG.var.
 176
 177 inline cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con.
 178
 179 inline cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con.
 180
 181 inline cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con.
 182
 183 (* begin show *)
 184
 185 inline cic:/CoRN/ftc/Differentiability/Gbnd.var.
 186
 187 (* end show *)
 188
 189 inline cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con.
 190
 191 (* UNEXPORTED
 192 End Operations.
 193 *)
 194
 195 (* UNEXPORTED
 196 Section Corollaries.
 197 *)
 198
 199 inline cic:/CoRN/ftc/Differentiability/a.var.
 200
 201 inline cic:/CoRN/ftc/Differentiability/b.var.
 202
 203 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
 204
 205 (* begin hide *)
 206
 207 inline cic:/CoRN/ftc/Differentiability/Hab.con.
 208
 209 inline cic:/CoRN/ftc/Differentiability/I.con.
 210
 211 (* end hide *)
 212
 213 inline cic:/CoRN/ftc/Differentiability/F.var.
 214
 215 inline cic:/CoRN/ftc/Differentiability/G.var.
 216
 217 inline cic:/CoRN/ftc/Differentiability/diffF.var.
 218
 219 inline cic:/CoRN/ftc/Differentiability/diffG.var.
 220
 221 inline cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con.
 222
 223 inline cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con.
 224
 225 inline cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con.
 226
 227 inline cic:/CoRN/ftc/Differentiability/Gbnd.var.
 228
 229 inline cic:/CoRN/ftc/Differentiability/Diffble_I_div.con.
 230
 231 (* UNEXPORTED
 232 End Corollaries.
 233 *)
 234
 235 (* UNEXPORTED
 236 Section Other_Properties.
 237 *)
 238
 239 (*#*
 240 Differentiability of families of functions is proved by
 241 induction using the constant and addition rules.
 242 *)
 243
 244 inline cic:/CoRN/ftc/Differentiability/a.var.
 245
 246 inline cic:/CoRN/ftc/Differentiability/b.var.
 247
 248 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
 249
 250 inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con.
 251
 252 inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con.
 253
 254 inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con.
 255
 256 (* UNEXPORTED
 257 End Other_Properties.
 258 *)
 259
 260 (*#*
 261 Finally, a differentiable function is continuous.
 262
 263 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
 264 %\end{convention}%
 265 *)
 266
 267 inline cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con.
 268
 269 (* UNEXPORTED
 270 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
 271   diffble_imp_contin_I: continuous.
 272 *)
 273
 274 (* UNEXPORTED
 275 Hint Immediate included_imp_deriv: derivate.
 276 *)
 277