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 include "CoRN.ma".
  20
  21 (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
  22
  23 include "ftc/Differentiability.ma".
  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 alias id "a" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var".
  46
  47 alias id "b" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var".
  48
  49 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var".
  50
  51 (* begin hide *)
  52
  53 inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__".
  54
  55 inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__".
  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 alias id "a" = "cic:/CoRN/ftc/NthDerivative/Trivia/a.var".
  92
  93 alias id "b" = "cic:/CoRN/ftc/NthDerivative/Trivia/b.var".
  94
  95 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var".
  96
  97 (* begin hide *)
  98
  99 inline "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__".
 100
 101 inline "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__".
 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 alias id "a" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var".
 130
 131 alias id "b" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var".
 132
 133 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var".
 134
 135 (* begin hide *)
 136
 137 inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__".
 138
 139 inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__".
 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 alias id "F" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var".
 200
 201 alias id "diffF" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var".
 202
 203 alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/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 alias id "a" = "cic:/CoRN/ftc/NthDerivative/More_Results/a.var".
 238
 239 alias id "b" = "cic:/CoRN/ftc/NthDerivative/More_Results/b.var".
 240
 241 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var".
 242
 243 (* begin hide *)
 244
 245 inline "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__".
 246
 247 inline "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__".
 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