1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
21 include "ftc/Differentiability.ma".
24 Section Nth_Derivative
29 We now study higher order differentiability.
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.
40 We first define what we mean by the derivative of order [n] of a function.
43 alias id "a" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var".
45 alias id "b" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var".
47 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var".
51 inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__" as definition.
53 inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__" as definition.
57 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con" as definition.
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.
66 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con" as definition.
73 Implicit Arguments Derivative_I_n [a b].
77 Implicit Arguments Diffble_I_n [a b].
86 These are the expected extensionality and uniqueness results.
89 alias id "a" = "cic:/CoRN/ftc/NthDerivative/Trivia/a.var".
91 alias id "b" = "cic:/CoRN/ftc/NthDerivative/Trivia/b.var".
93 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var".
97 inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__" as definition.
99 inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__" as definition.
103 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con" as lemma.
105 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con" as lemma.
107 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con" as lemma.
109 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con" as lemma.
116 Section Basic_Results
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].
127 alias id "a" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var".
129 alias id "b" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var".
131 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var".
135 inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__" as definition.
137 inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__" as definition.
142 We begin by showing that having a higher order derivative implies being differentiable.
145 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con" as lemma.
147 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con" as lemma.
150 If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n].
153 inline procedural "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con" as lemma.
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]
161 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con" as lemma.
164 As expected, an [n] times differentiable in [[a,b]] function must be
165 defined in that interval.
168 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con" as lemma.
171 Also, the notions of derivative and differentiability are related as expected.
174 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con" as lemma.
176 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con" as lemma.
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.
183 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con" as lemma.
185 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con" as lemma.
192 First order differentiability is just a special case.
197 alias id "F" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var".
199 alias id "diffF" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var".
201 alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var".
205 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con" as lemma.
207 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con" as lemma.
214 As usual, nth order derivability is preserved by shrinking the interval.
217 inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con" as lemma.
219 inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con" as lemma.
222 And finally we have an addition rule for the order of the derivative.
225 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con" as lemma.
235 alias id "a" = "cic:/CoRN/ftc/NthDerivative/More_Results/a.var".
237 alias id "b" = "cic:/CoRN/ftc/NthDerivative/More_Results/b.var".
239 alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var".
243 inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__" as definition.
245 inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__" as definition.
249 (*#* **The Nth Derivative
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.
257 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con" as definition.
260 This operator is well defined and works as expected.
263 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con" as lemma.
265 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con" as lemma.
267 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con" as lemma.
269 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con" as lemma.
272 Some basic properties of this operation.
275 inline procedural "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con" as lemma.
277 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con" as lemma.
284 Section More_on_n_deriv
288 Some not so basic properties of this operation (needed in rather specific situations).
291 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con" as lemma.
293 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con" as lemma.
295 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con" as lemma.