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