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