X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreFunctions.ma;fp=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreFunctions.ma;h=4d7622ba2318fe4ae14baa440efc243b20854a5c;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma b/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma new file mode 100644 index 000000000..4d7622ba2 --- /dev/null +++ b/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma @@ -0,0 +1,650 @@ +(**************************************************************************) +(* ___ *) +(* ||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/MoreFunctions". + +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 +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var". + +(*#* +Trivial stuff. +*) + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con". + +(*#* +%\begin{convention}% Assume that [I] is compact and [F] is continuous in [I]. +%\end{convention}% +*) + +alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var". + +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var". + +inline "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con". + +(* begin show *) + +alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var". + +(* end show *) + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con". + +inline "cic:/CoRN/ftc/MoreFunctions/FNorm.con". + +inline "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con". + +(* UNEXPORTED +End Basic_Results +*) + +(* UNEXPORTED +Hint Resolve Continuous_imp_inc: included. +*) + +(* UNEXPORTED +Section Other_Results +*) + +(*#* +The usual stuff. +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con". + +(* begin show *) + +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var". + +alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var". + +(* end show *) + +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con". + +(* 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 +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var". + +alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var". + +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var". + +alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con". + +inline "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con". + +(* UNEXPORTED +End Corollaries +*) + +(* UNEXPORTED +Hint Resolve Continuous_div: continuous. +*) + +(* UNEXPORTED +Section Sums +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con". + +(*#* +%\begin{convention}% Assume [f] is a sequence of continuous functions. +%\end{convention}% +*) + +alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var". + +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con". + +(* 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}% +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var". + +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var". + +alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con". + +(* 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 +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var". + +alias id "pI" = "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}% +*) + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var". + +alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var". + +alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var". + +alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var". + +alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var". + +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con". + +(* UNEXPORTED +End More_Results +*) + +(* UNEXPORTED +Section More_Corollaries +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var". + +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var". + +alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var". + +alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var". + +alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var". + +alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var". + +(* begin show *) + +alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var". + +(* end show *) + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con". + +(* UNEXPORTED +End More_Corollaries +*) + +(* UNEXPORTED +Section More_Sums +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var". + +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con". + +(* begin show *) + +alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var". + +alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var". + +alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var". + +(* end show *) + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con". + +(* UNEXPORTED +End More_Sums +*) + +(* UNEXPORTED +Section Diffble_Basic_Properties +*) + +(*#* **Differentiability + +Mutatis mutandis for differentiability. +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var". + +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var". + +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var". + +alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var". + +(*#* +%\begin{convention}% Assume [F] and [G] are differentiable in [I]. +%\end{convention}% +*) + +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con". + +(* UNEXPORTED +End Diffble_Basic_Properties +*) + +(* UNEXPORTED +Hint Immediate Diffble_imp_inc: included. +*) + +(* UNEXPORTED +Section Diffble_Corollaries +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var". + +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var". + +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var". + +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var". + +alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con". + +(* 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. +*) + +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var". + +alias id "pI" = "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}% +*) + +alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var". + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var". + +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char + (* begin hide *).con". + +(* end hide *) + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con". + +(* UNEXPORTED +End Definitions +*) + +(* UNEXPORTED +Section Basic_Results +*) + +(*#* +All the usual results hold. +*) + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con". + +inline "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con". + +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con". + +(* UNEXPORTED +End Basic_Results +*) + +(* UNEXPORTED +Section More_Results +*) + +(*#* +Some new results hold, too: +*) + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con". + +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con". + +(*#* +Some useful characterization results. +*) + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con". + +(* UNEXPORTED +End More_Results +*) + +(* UNEXPORTED +Section Derivating_Diffble +*) + +(*#* +As a special case we get a differentiation operator%\ldots%#...# +*) + +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var". + +(* begin show *) + +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var". + +(* end show *) + +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Deriv.con". + +(* UNEXPORTED +End Derivating_Diffble +*) + +(* UNEXPORTED +Section Corollaries +*) + +(*#* +%\ldots%#...# for which the expected property also holds. +*) + +inline "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con". + +(*#* +Some more interesting properties. +*) + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con". + +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con". + +(* 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. +*) +