X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FDifferentiability.ma;fp=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FDifferentiability.ma;h=812a91e02c4001d8ade0f9a90559b3db229f3dcf;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/CoRN-Decl/ftc/Differentiability.ma b/matita/contribs/CoRN-Decl/ftc/Differentiability.ma new file mode 100644 index 000000000..812a91e02 --- /dev/null +++ b/matita/contribs/CoRN-Decl/ftc/Differentiability.ma @@ -0,0 +1,275 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/CoRN-Decl/ftc/Differentiability". + +include "CoRN.ma". + +(* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *) + +include "ftc/PartInterval.ma". + +include "ftc/DerivativeOps.ma". + +(* UNEXPORTED +Section Definitions +*) + +(*#* *Differentiability + +We will now use our work on derivatives to define a notion of +differentiable function and prove its main properties. + +%\begin{convention}% Throughout this section, [a,b] will be real +numbers with [a [<] b], [I] will denote the interval [[a,b]] +and [F,G,H] will be differentiable functions. +%\end{convention}% + +Usually a function [F] is said to be differentiable in a proper +compact interval [[a,b]] if there exists another function [F'] +such that [F'] is a derivative of [F] in that interval. There is a +problem in formalizing this definition, as we pointed out earlier on, +which is that if we simply write it down as is we are not able to get +such a function [F'] from a hypothesis that [F] is differentiable. + +However, it turns out that this is not altogether the best definition +for the following reason: if we say that [F] is differentiable in +[[a,b]], we mean that there is a partial function [F'] which is +defined in [[a,b]] and satisfies a certain condition in that +interval but nothing is required of the behaviour of the function +outside [[a,b]]. Thus we can argue that, from a mathematical +point of view, the [F'] that we get eliminating a hypothesis of +differentiability should be defined exactly on that interval. If we +do this, we can quantify over the set of setoid functions in that +interval and eliminate the existencial quantifier without any +problems. +*) + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I.con". + +(* UNEXPORTED +End Definitions +*) + +(* UNEXPORTED +Implicit Arguments Diffble_I [a b]. +*) + +(* UNEXPORTED +Section Local_Properties +*) + +(*#* +From this point on, we just prove results analogous to the ones for derivability. + +A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]]. +*) + +inline "cic:/CoRN/ftc/Differentiability/included_imp_diffble.con". + +(*#* +A function differentiable in an interval is everywhere defined in that interval. +*) + +alias id "a" = "cic:/CoRN/ftc/Differentiability/Local_Properties/a.var". + +alias id "b" = "cic:/CoRN/ftc/Differentiability/Local_Properties/b.var". + +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var". + +(* begin hide *) + +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab.con" "Local_Properties__". + +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/I.con" "Local_Properties__". + +(* end hide *) + +inline "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con". + +(*#* +If a function has a derivative in an interval then it is differentiable in that interval. +*) + +inline "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con". + +(* UNEXPORTED +End Local_Properties +*) + +(* UNEXPORTED +Hint Resolve diffble_imp_inc: included. +*) + +(* UNEXPORTED +Section Operations +*) + +(*#* +All the algebraic results carry on. +*) + +alias id "a" = "cic:/CoRN/ftc/Differentiability/Operations/a.var". + +alias id "b" = "cic:/CoRN/ftc/Differentiability/Operations/b.var". + +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Operations/Hab'.var". + +(* begin hide *) + +inline "cic:/CoRN/ftc/Differentiability/Operations/Hab.con" "Operations__". + +inline "cic:/CoRN/ftc/Differentiability/Operations/I.con" "Operations__". + +(* end hide *) + +(* UNEXPORTED +Section Constants +*) + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con". + +(* UNEXPORTED +End Constants +*) + +(* UNEXPORTED +Section Well_Definedness +*) + +alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var". + +alias id "H" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var". + +alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con". + +(* UNEXPORTED +End Well_Definedness +*) + +alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/F.var". + +alias id "G" = "cic:/CoRN/ftc/Differentiability/Operations/G.var". + +alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/diffF.var". + +alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Operations/diffG.var". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con". + +(* begin show *) + +alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var". + +(* end show *) + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con". + +(* UNEXPORTED +End Operations +*) + +(* UNEXPORTED +Section Corollaries +*) + +alias id "a" = "cic:/CoRN/ftc/Differentiability/Corollaries/a.var". + +alias id "b" = "cic:/CoRN/ftc/Differentiability/Corollaries/b.var". + +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var". + +(* begin hide *) + +inline "cic:/CoRN/ftc/Differentiability/Corollaries/Hab.con" "Corollaries__". + +inline "cic:/CoRN/ftc/Differentiability/Corollaries/I.con" "Corollaries__". + +(* end hide *) + +alias id "F" = "cic:/CoRN/ftc/Differentiability/Corollaries/F.var". + +alias id "G" = "cic:/CoRN/ftc/Differentiability/Corollaries/G.var". + +alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var". + +alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con". + +alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con". + +(* UNEXPORTED +End Corollaries +*) + +(* UNEXPORTED +Section Other_Properties +*) + +(*#* +Differentiability of families of functions is proved by +induction using the constant and addition rules. +*) + +alias id "a" = "cic:/CoRN/ftc/Differentiability/Other_Properties/a.var". + +alias id "b" = "cic:/CoRN/ftc/Differentiability/Other_Properties/b.var". + +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con". + +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con". + +(* UNEXPORTED +End Other_Properties +*) + +(*#* +Finally, a differentiable function is continuous. + +%\begin{convention}% Let [F] be a partial function with derivative [F'] on [I]. +%\end{convention}% +*) + +inline "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con". + +(* UNEXPORTED +Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I + diffble_imp_contin_I: continuous. +*) + +(* UNEXPORTED +Hint Immediate included_imp_deriv: derivate. +*) +