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