matita/contribs/CoRN-Decl/ftc/NthDerivative.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/NthDerivative".
  18
  19 (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
  20
  21 (* INCLUDE
  22 Differentiability
  23 *)
  24
  25 (* UNEXPORTED
  26 Section Nth_Derivative.
  27 *)
  28
  29 (*#* *Nth Derivative
  30
  31 We now study higher order differentiability.
  32
  33 %\begin{convention}% Throughout this section:
  34  - [a, b] will be real numbers with [a [<] b];
  35  - [I] will denote the compact interval [[a,b]];
  36  - [F, G, H] will denote partial functions.
  37
  38 %\end{convention}%
  39
  40 **Definitions
  41
  42 We first define what we mean by the derivative of order [n] of a function.
  43 *)
  44
  45 inline cic:/CoRN/ftc/NthDerivative/a.var.
  46
  47 inline cic:/CoRN/ftc/NthDerivative/b.var.
  48
  49 inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
  50
  51 (* begin hide *)
  52
  53 inline cic:/CoRN/ftc/NthDerivative/Hab.con.
  54
  55 inline cic:/CoRN/ftc/NthDerivative/I.con.
  56
  57 (* end hide *)
  58
  59 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con.
  60
  61 (*#*
  62 Unlike first order differentiability, for our definition to be
  63 workable it is better to define directly what it means for a function
  64 to be [n] times differentiable instead of quantifying over the
  65 [Derivative_I_n] relation.
  66 *)
  67
  68 inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con.
  69
  70 (* UNEXPORTED
  71 End Nth_Derivative.
  72 *)
  73
  74 (* UNEXPORTED
  75 Implicit Arguments Derivative_I_n [a b].
  76 *)
  77
  78 (* UNEXPORTED
  79 Implicit Arguments Diffble_I_n [a b].
  80 *)
  81
  82 (* UNEXPORTED
  83 Section Trivia.
  84 *)
  85
  86 (*#* **Trivia
  87
  88 These are the expected extensionality and uniqueness results.
  89 *)
  90
  91 inline cic:/CoRN/ftc/NthDerivative/a.var.
  92
  93 inline cic:/CoRN/ftc/NthDerivative/b.var.
  94
  95 inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
  96
  97 (* begin hide *)
  98
  99 inline cic:/CoRN/ftc/NthDerivative/Hab.con.
 100
 101 inline cic:/CoRN/ftc/NthDerivative/I.con.
 102
 103 (* end hide *)
 104
 105 inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con.
 106
 107 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con.
 108
 109 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con.
 110
 111 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con.
 112
 113 (* UNEXPORTED
 114 End Trivia.
 115 *)
 116
 117 (* UNEXPORTED
 118 Section Basic_Results.
 119 *)
 120
 121 (*#* **Basic Results
 122
 123 We now explore the concept of [n] times differentiability.  Notice
 124 that, unlike the first order case, we do not pay so much attention to
 125 the relation of [n] times derivative, but focus rather on the
 126 definition of [Diffble_I_n].
 127 *)
 128
 129 inline cic:/CoRN/ftc/NthDerivative/a.var.
 130
 131 inline cic:/CoRN/ftc/NthDerivative/b.var.
 132
 133 inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
 134
 135 (* begin hide *)
 136
 137 inline cic:/CoRN/ftc/NthDerivative/Hab.con.
 138
 139 inline cic:/CoRN/ftc/NthDerivative/I.con.
 140
 141 (* end hide *)
 142
 143 (*#*
 144 We begin by showing that having a higher order derivative implies being differentiable.
 145 *)
 146
 147 inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con.
 148
 149 inline cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con.
 150
 151 (*#*
 152 If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n].
 153 *)
 154
 155 inline cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con.
 156
 157 (*#*
 158 The next result consolidates our intuition that a function is [n]
 159 times differentiable if we can build from it a chain of [n]
 160 derivatives.
 161 *)
 162
 163 inline cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con.
 164
 165 (*#*
 166 As expected, an [n] times differentiable in [[a,b]] function must be
 167 defined in that interval.
 168 *)
 169
 170 inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con.
 171
 172 (*#*
 173 Also, the notions of derivative and differentiability are related as expected.
 174 *)
 175
 176 inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con.
 177
 178 inline cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con.
 179
 180 (*#*
 181 From this we can prove that if [F] has an nth order derivative in
 182 [[a,b]] then both [F] and its derivative are defined in that interval.
 183 *)
 184
 185 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con.
 186
 187 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con.
 188
 189 (* UNEXPORTED
 190 Section aux.
 191 *)
 192
 193 (*#*
 194 First order differentiability is just a special case.
 195 *)
 196
 197 (* begin show *)
 198
 199 inline cic:/CoRN/ftc/NthDerivative/F.var.
 200
 201 inline cic:/CoRN/ftc/NthDerivative/diffF.var.
 202
 203 inline cic:/CoRN/ftc/NthDerivative/diffFn.var.
 204
 205 (* end show *)
 206
 207 inline cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con.
 208
 209 inline cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con.
 210
 211 (* UNEXPORTED
 212 End aux.
 213 *)
 214
 215 (*#*
 216 As usual, nth order derivability is preserved by shrinking the interval.
 217 *)
 218
 219 inline cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con.
 220
 221 inline cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con.
 222
 223 (*#*
 224 And finally we have an addition rule for the order of the derivative.
 225 *)
 226
 227 inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con.
 228
 229 (* UNEXPORTED
 230 End Basic_Results.
 231 *)
 232
 233 (* UNEXPORTED
 234 Section More_Results.
 235 *)
 236
 237 inline cic:/CoRN/ftc/NthDerivative/a.var.
 238
 239 inline cic:/CoRN/ftc/NthDerivative/b.var.
 240
 241 inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
 242
 243 (* begin hide *)
 244
 245 inline cic:/CoRN/ftc/NthDerivative/Hab.con.
 246
 247 inline cic:/CoRN/ftc/NthDerivative/I.con.
 248
 249 (* end hide *)
 250
 251 (*#* **The Nth Derivative
 252
 253 We now define an operator that returns an nth order derivative of an
 254 n-times differentiable function.  This is analogous to the quantifier
 255 elimination which we would get if we had defined nth differentiability
 256 as an existential quantification of the nth derivative relation.
 257 *)
 258
 259 inline cic:/CoRN/ftc/NthDerivative/n_deriv_I.con.
 260
 261 (*#*
 262 This operator is well defined and works as expected.
 263 *)
 264
 265 inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con.
 266
 267 inline cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con.
 268
 269 inline cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con.
 270
 271 inline cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con.
 272
 273 (*#*
 274 Some basic properties of this operation.
 275 *)
 276
 277 inline cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con.
 278
 279 inline cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con.
 280
 281 (* UNEXPORTED
 282 End More_Results.
 283 *)
 284
 285 (* UNEXPORTED
 286 Section More_on_n_deriv.
 287 *)
 288
 289 (*#*
 290 Some not so basic properties of this operation (needed in rather specific situations).
 291 *)
 292
 293 inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con.
 294
 295 inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con.
 296
 297 inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con.
 298
 299 (* UNEXPORTED
 300 End More_on_n_deriv.
 301 *)
 302