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.
44 cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var
48 cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var
52 cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var
57 inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__" as definition.
59 inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__" as definition.
63 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con" as definition.
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.
72 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con" as definition.
79 Implicit Arguments Derivative_I_n [a b].
83 Implicit Arguments Diffble_I_n [a b].
92 These are the expected extensionality and uniqueness results.
96 cic:/CoRN/ftc/NthDerivative/Trivia/a.var
100 cic:/CoRN/ftc/NthDerivative/Trivia/b.var
104 cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var
109 inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__" as definition.
111 inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__" as definition.
115 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con" as lemma.
117 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con" as lemma.
119 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con" as lemma.
121 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con" as lemma.
128 Section Basic_Results
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].
140 cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var
144 cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var
148 cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var
153 inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__" as definition.
155 inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__" as definition.
160 We begin by showing that having a higher order derivative implies being differentiable.
163 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con" as lemma.
165 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con" as lemma.
168 If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n].
171 inline procedural "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con" as lemma.
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]
179 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con" as lemma.
182 As expected, an [n] times differentiable in [[a,b]] function must be
183 defined in that interval.
186 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con" as lemma.
189 Also, the notions of derivative and differentiability are related as expected.
192 inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con" as lemma.
194 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con" as lemma.
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.
201 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con" as lemma.
203 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con" as lemma.
210 First order differentiability is just a special case.
216 cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var
220 cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var
224 cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var
229 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con" as lemma.
231 inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con" as lemma.
238 As usual, nth order derivability is preserved by shrinking the interval.
241 inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con" as lemma.
243 inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con" as lemma.
246 And finally we have an addition rule for the order of the derivative.
249 inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con" as lemma.
260 cic:/CoRN/ftc/NthDerivative/More_Results/a.var
264 cic:/CoRN/ftc/NthDerivative/More_Results/b.var
268 cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var
273 inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__" as definition.
275 inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__" as definition.
279 (*#* **The Nth Derivative
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.
287 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con" as definition.
290 This operator is well defined and works as expected.
293 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con" as lemma.
295 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con" as lemma.
297 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con" as lemma.
299 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con" as lemma.
302 Some basic properties of this operation.
305 inline procedural "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con" as lemma.
307 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con" as lemma.
314 Section More_on_n_deriv
318 Some not so basic properties of this operation (needed in rather specific situations).
321 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con" as lemma.
323 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con" as lemma.
325 inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con" as lemma.