helm/software/matita/contribs/CoRN-Procedural/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".
  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".
  80
  81 (*#*
  82 A function differentiable in an interval is everywhere defined in that interval.
  83 *)
  84
  85 alias id "a" = "cic:/CoRN/ftc/Differentiability/Local_Properties/a.var".
  86
  87 alias id "b" = "cic:/CoRN/ftc/Differentiability/Local_Properties/b.var".
  88
  89 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var".
  90
  91 (* begin hide *)
  92
  93 inline procedural "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab.con" "Local_Properties__".
  94
  95 inline procedural "cic:/CoRN/ftc/Differentiability/Local_Properties/I.con" "Local_Properties__".
  96
  97 (* end hide *)
  98
  99 inline procedural "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con".
 100
 101 (*#*
 102 If a function has a derivative in an interval then it is differentiable in that interval.
 103 *)
 104
 105 inline procedural "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con".
 106
 107 (* UNEXPORTED
 108 End Local_Properties
 109 *)
 110
 111 (* UNEXPORTED
 112 Hint Resolve diffble_imp_inc: included.
 113 *)
 114
 115 (* UNEXPORTED
 116 Section Operations
 117 *)
 118
 119 (*#*
 120 All the algebraic results carry on.
 121 *)
 122
 123 alias id "a" = "cic:/CoRN/ftc/Differentiability/Operations/a.var".
 124
 125 alias id "b" = "cic:/CoRN/ftc/Differentiability/Operations/b.var".
 126
 127 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Operations/Hab'.var".
 128
 129 (* begin hide *)
 130
 131 inline procedural "cic:/CoRN/ftc/Differentiability/Operations/Hab.con" "Operations__".
 132
 133 inline procedural "cic:/CoRN/ftc/Differentiability/Operations/I.con" "Operations__".
 134
 135 (* end hide *)
 136
 137 (* UNEXPORTED
 138 Section Constants
 139 *)
 140
 141 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con".
 142
 143 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con".
 144
 145 (* UNEXPORTED
 146 End Constants
 147 *)
 148
 149 (* UNEXPORTED
 150 Section Well_Definedness
 151 *)
 152
 153 alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var".
 154
 155 alias id "H" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var".
 156
 157 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var".
 158
 159 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con".
 160
 161 (* UNEXPORTED
 162 End Well_Definedness
 163 *)
 164
 165 alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/F.var".
 166
 167 alias id "G" = "cic:/CoRN/ftc/Differentiability/Operations/G.var".
 168
 169 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/diffF.var".
 170
 171 alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Operations/diffG.var".
 172
 173 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con".
 174
 175 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con".
 176
 177 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con".
 178
 179 (* begin show *)
 180
 181 alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var".
 182
 183 (* end show *)
 184
 185 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con".
 186
 187 (* UNEXPORTED
 188 End Operations
 189 *)
 190
 191 (* UNEXPORTED
 192 Section Corollaries
 193 *)
 194
 195 alias id "a" = "cic:/CoRN/ftc/Differentiability/Corollaries/a.var".
 196
 197 alias id "b" = "cic:/CoRN/ftc/Differentiability/Corollaries/b.var".
 198
 199 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var".
 200
 201 (* begin hide *)
 202
 203 inline procedural "cic:/CoRN/ftc/Differentiability/Corollaries/Hab.con" "Corollaries__".
 204
 205 inline procedural "cic:/CoRN/ftc/Differentiability/Corollaries/I.con" "Corollaries__".
 206
 207 (* end hide *)
 208
 209 alias id "F" = "cic:/CoRN/ftc/Differentiability/Corollaries/F.var".
 210
 211 alias id "G" = "cic:/CoRN/ftc/Differentiability/Corollaries/G.var".
 212
 213 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var".
 214
 215 alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var".
 216
 217 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con".
 218
 219 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con".
 220
 221 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con".
 222
 223 alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var".
 224
 225 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con".
 226
 227 (* UNEXPORTED
 228 End Corollaries
 229 *)
 230
 231 (* UNEXPORTED
 232 Section Other_Properties
 233 *)
 234
 235 (*#*
 236 Differentiability of families of functions is proved by
 237 induction using the constant and addition rules.
 238 *)
 239
 240 alias id "a" = "cic:/CoRN/ftc/Differentiability/Other_Properties/a.var".
 241
 242 alias id "b" = "cic:/CoRN/ftc/Differentiability/Other_Properties/b.var".
 243
 244 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var".
 245
 246 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con".
 247
 248 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con".
 249
 250 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con".
 251
 252 (* UNEXPORTED
 253 End Other_Properties
 254 *)
 255
 256 (*#*
 257 Finally, a differentiable function is continuous.
 258
 259 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
 260 %\end{convention}%
 261 *)
 262
 263 inline procedural "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con".
 264
 265 (* UNEXPORTED
 266 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
 267   diffble_imp_contin_I: continuous.
 268 *)
 269
 270 (* UNEXPORTED
 271 Hint Immediate included_imp_deriv: derivate.
 272 *)
 273