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