X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FNthDerivative.ma;h=0900e8703c368a9f69ab86919dc440d5a4057e89;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=7f918465b7027b92da291c86159047b602263c9d;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma index 7f918465b..0900e8703 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma @@ -16,11 +16,11 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/NthDerivative". +include "CoRN.ma". + (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *) -(* INCLUDE -Differentiability -*) +include "ftc/Differentiability.ma". (* UNEXPORTED Section Nth_Derivative. @@ -42,21 +42,21 @@ We now study higher order differentiability. We first define what we mean by the derivative of order [n] of a function. *) -inline cic:/CoRN/ftc/NthDerivative/a.var. +inline "cic:/CoRN/ftc/NthDerivative/a.var". -inline cic:/CoRN/ftc/NthDerivative/b.var. +inline "cic:/CoRN/ftc/NthDerivative/b.var". -inline cic:/CoRN/ftc/NthDerivative/Hab'.var. +inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/NthDerivative/Hab.con. +inline "cic:/CoRN/ftc/NthDerivative/Hab.con". -inline cic:/CoRN/ftc/NthDerivative/I.con. +inline "cic:/CoRN/ftc/NthDerivative/I.con". (* end hide *) -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con". (*#* Unlike first order differentiability, for our definition to be @@ -65,7 +65,7 @@ to be [n] times differentiable instead of quantifying over the [Derivative_I_n] relation. *) -inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con. +inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con". (* UNEXPORTED End Nth_Derivative. @@ -88,27 +88,27 @@ Section Trivia. These are the expected extensionality and uniqueness results. *) -inline cic:/CoRN/ftc/NthDerivative/a.var. +inline "cic:/CoRN/ftc/NthDerivative/a.var". -inline cic:/CoRN/ftc/NthDerivative/b.var. +inline "cic:/CoRN/ftc/NthDerivative/b.var". -inline cic:/CoRN/ftc/NthDerivative/Hab'.var. +inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/NthDerivative/Hab.con. +inline "cic:/CoRN/ftc/NthDerivative/Hab.con". -inline cic:/CoRN/ftc/NthDerivative/I.con. +inline "cic:/CoRN/ftc/NthDerivative/I.con". (* end hide *) -inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con. +inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con". -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con". -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con". -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con". (* UNEXPORTED End Trivia. @@ -126,17 +126,17 @@ the relation of [n] times derivative, but focus rather on the definition of [Diffble_I_n]. *) -inline cic:/CoRN/ftc/NthDerivative/a.var. +inline "cic:/CoRN/ftc/NthDerivative/a.var". -inline cic:/CoRN/ftc/NthDerivative/b.var. +inline "cic:/CoRN/ftc/NthDerivative/b.var". -inline cic:/CoRN/ftc/NthDerivative/Hab'.var. +inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/NthDerivative/Hab.con. +inline "cic:/CoRN/ftc/NthDerivative/Hab.con". -inline cic:/CoRN/ftc/NthDerivative/I.con. +inline "cic:/CoRN/ftc/NthDerivative/I.con". (* end hide *) @@ -144,15 +144,15 @@ inline cic:/CoRN/ftc/NthDerivative/I.con. We begin by showing that having a higher order derivative implies being differentiable. *) -inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con. +inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con". -inline cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con. +inline "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con". (*#* If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n]. *) -inline cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con. +inline "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con". (*#* The next result consolidates our intuition that a function is [n] @@ -160,31 +160,31 @@ times differentiable if we can build from it a chain of [n] derivatives. *) -inline cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con. +inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con". (*#* As expected, an [n] times differentiable in [[a,b]] function must be defined in that interval. *) -inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con. +inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con". (*#* Also, the notions of derivative and differentiability are related as expected. *) -inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con. +inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con". -inline cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con. +inline "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con". (*#* From this we can prove that if [F] has an nth order derivative in [[a,b]] then both [F] and its derivative are defined in that interval. *) -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con". -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con". (* UNEXPORTED Section aux. @@ -196,17 +196,17 @@ First order differentiability is just a special case. (* begin show *) -inline cic:/CoRN/ftc/NthDerivative/F.var. +inline "cic:/CoRN/ftc/NthDerivative/F.var". -inline cic:/CoRN/ftc/NthDerivative/diffF.var. +inline "cic:/CoRN/ftc/NthDerivative/diffF.var". -inline cic:/CoRN/ftc/NthDerivative/diffFn.var. +inline "cic:/CoRN/ftc/NthDerivative/diffFn.var". (* end show *) -inline cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con. +inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con". -inline cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con. +inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con". (* UNEXPORTED End aux. @@ -216,15 +216,15 @@ End aux. As usual, nth order derivability is preserved by shrinking the interval. *) -inline cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con. +inline "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con". -inline cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con. +inline "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con". (*#* And finally we have an addition rule for the order of the derivative. *) -inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con. +inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con". (* UNEXPORTED End Basic_Results. @@ -234,17 +234,17 @@ End Basic_Results. Section More_Results. *) -inline cic:/CoRN/ftc/NthDerivative/a.var. +inline "cic:/CoRN/ftc/NthDerivative/a.var". -inline cic:/CoRN/ftc/NthDerivative/b.var. +inline "cic:/CoRN/ftc/NthDerivative/b.var". -inline cic:/CoRN/ftc/NthDerivative/Hab'.var. +inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/NthDerivative/Hab.con. +inline "cic:/CoRN/ftc/NthDerivative/Hab.con". -inline cic:/CoRN/ftc/NthDerivative/I.con. +inline "cic:/CoRN/ftc/NthDerivative/I.con". (* end hide *) @@ -256,27 +256,27 @@ elimination which we would get if we had defined nth differentiability as an existential quantification of the nth derivative relation. *) -inline cic:/CoRN/ftc/NthDerivative/n_deriv_I.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con". (*#* This operator is well defined and works as expected. *) -inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con". -inline cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con". -inline cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con". -inline cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con". (*#* Some basic properties of this operation. *) -inline cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con. +inline "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con". -inline cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con". (* UNEXPORTED End More_Results. @@ -290,11 +290,11 @@ Section More_on_n_deriv. Some not so basic properties of this operation (needed in rather specific situations). *) -inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con". -inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con". -inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con. +inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con". (* UNEXPORTED End More_on_n_deriv.