(**************************************************************************) (* ___ *) (* ||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 *********************) include "CoRN.ma". (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *) (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *) include "ftc/MoreIntervals.ma". (* UNEXPORTED Opaque Min Max. *) (* UNEXPORTED Section Basic_Results *) (*#* *More about Functions Here we state all the main results about properties of functions that we already proved for compact intervals in the more general setting of arbitrary intervals. %\begin{convention}% Let [I:interval] and [F,F',G,G'] be partial functions. %\end{convention}% **Continuity *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var *) (*#* Trivial stuff. *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con" as lemma. (*#* %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con" as lemma. (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var *) (* end show *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm.con" as definition. inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con" as lemma. (* UNEXPORTED End Basic_Results *) (* UNEXPORTED Hint Resolve Continuous_imp_inc: included. *) (* UNEXPORTED Section Other_Results *) (*#* The usual stuff. *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con" as lemma. (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var *) (* end show *) inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con" as lemma. (* UNEXPORTED End Other_Results *) (* UNEXPORTED Hint Resolve continuous_compact Continuous_const Continuous_id Continuous_plus Continuous_inv Continuous_minus Continuous_mult Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous. *) (* UNEXPORTED Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous. *) (* UNEXPORTED Section Corollaries *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con" as lemma. (* UNEXPORTED End Corollaries *) (* UNEXPORTED Hint Resolve Continuous_div: continuous. *) (* UNEXPORTED Section Sums *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Sums/I.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con" as lemma. (*#* %\begin{convention}% Assume [f] is a sequence of continuous functions. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Sums/f.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Sums/contF.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con" as lemma. (* UNEXPORTED End Sums *) (* UNEXPORTED Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous. *) (* UNEXPORTED Section Basic_Properties *) (*#* **Derivative Derivative is not that much different. %\begin{convention}% From this point on we assume [I] to be proper. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con" as lemma. (* UNEXPORTED End Basic_Properties *) (* UNEXPORTED Hint Immediate Derivative_imp_inc Derivative_imp_inc': included. *) (* UNEXPORTED Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous': continuous. *) (* UNEXPORTED Section More_Results *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var *) (*#* %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/G.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con" as lemma. (* UNEXPORTED End More_Results *) (* UNEXPORTED Section More_Corollaries *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var *) (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var *) (* end show *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con" as lemma. (* UNEXPORTED End More_Corollaries *) (* UNEXPORTED Section More_Sums *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con" as lemma. (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var *) (* end show *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con" as lemma. (* UNEXPORTED End More_Sums *) (* UNEXPORTED Section Diffble_Basic_Properties *) (*#* **Differentiability Mutatis mutandis for differentiability. *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con" as lemma. (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var *) (*#* %\begin{convention}% Assume [F] and [G] are differentiable in [I]. %\end{convention}% *) inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con" as lemma. (* UNEXPORTED End Diffble_Basic_Properties *) (* UNEXPORTED Hint Immediate Diffble_imp_inc: included. *) (* UNEXPORTED Section Diffble_Corollaries *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con" as lemma. (* UNEXPORTED End Diffble_Corollaries *) (* UNEXPORTED Section Nth_Derivative *) (*#* **Nth Derivative Higher order derivatives pose more interesting problems. It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval. *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var *) (* UNEXPORTED Section Definitions *) (*#* %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var *) inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con" as definition. inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char (* begin hide *).con" as lemma. (* end hide *) inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con" as definition. (* UNEXPORTED End Definitions *) (* UNEXPORTED Section Basic_Results *) (*#* All the usual results hold. *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con" as lemma. (* UNEXPORTED End Basic_Results *) (* UNEXPORTED Section More_Results *) (*#* Some new results hold, too: *) inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con" as lemma. (*#* Some useful characterization results. *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con" as lemma. (* UNEXPORTED End More_Results *) (* UNEXPORTED Section Derivating_Diffble *) (*#* As a special case we get a differentiation operator%\ldots%#...# *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var *) (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var *) (* end show *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv.con" as definition. (* UNEXPORTED End Derivating_Diffble *) (* UNEXPORTED Section Corollaries *) (*#* %\ldots%#...# for which the expected property also holds. *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con" as lemma. (*#* Some more interesting properties. *) inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con" as lemma. inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con" as lemma. (* UNEXPORTED End Corollaries *) (* UNEXPORTED End Nth_Derivative *) (* UNEXPORTED Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv Derivative_minus Derivative_mult Derivative_scal Derivative_nth Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0 Derivative_Sum: derivate. *) (* UNEXPORTED Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc: included. *) (* UNEXPORTED Hint Resolve Deriv_lemma N_Deriv_lemma: derivate. *) (* UNEXPORTED Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous': continuous. *)