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: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
21 (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *)
23 include "ftc/MoreIntervals.ma".
33 (*#* *More about Functions
35 Here we state all the main results about properties of functions that
36 we already proved for compact intervals in the more general setting of
39 %\begin{convention}% Let [I:interval] and [F,F',G,G'] be partial functions.
46 cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var
53 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con" as lemma.
56 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
61 cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var
65 cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var
69 cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var
72 inline procedural "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con" as lemma.
77 cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var
82 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con" as lemma.
84 inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm.con" as definition.
86 inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con" as lemma.
93 Hint Resolve Continuous_imp_inc: included.
105 cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var
109 cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var
113 cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var
116 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con" as lemma.
121 cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var
125 cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var
130 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con" as lemma.
132 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con" as lemma.
134 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con" as lemma.
136 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con" as lemma.
138 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con" as lemma.
140 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con" as lemma.
142 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con" as lemma.
144 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con" as lemma.
146 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con" as lemma.
148 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con" as lemma.
150 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con" as lemma.
152 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con" as lemma.
159 Hint Resolve continuous_compact Continuous_const Continuous_id
160 Continuous_plus Continuous_inv Continuous_minus Continuous_mult
161 Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous.
165 Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
173 cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var
177 cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var
181 cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var
185 cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var
189 cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var
193 cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var
196 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con" as lemma.
198 inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con" as lemma.
205 Hint Resolve Continuous_div: continuous.
213 cic:/CoRN/ftc/MoreFunctions/Sums/I.var
216 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con" as lemma.
219 %\begin{convention}% Assume [f] is a sequence of continuous functions.
224 cic:/CoRN/ftc/MoreFunctions/Sums/f.var
228 cic:/CoRN/ftc/MoreFunctions/Sums/contF.var
231 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con" as lemma.
233 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con" as lemma.
240 Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
244 Section Basic_Properties
249 Derivative is not that much different.
251 %\begin{convention}% From this point on we assume [I] to be proper.
256 cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var
260 cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var
264 cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var
268 cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var
272 cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var
275 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con" as lemma.
277 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con" as lemma.
279 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con" as lemma.
281 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con" as lemma.
283 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con" as lemma.
285 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con" as lemma.
287 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con" as lemma.
294 Hint Immediate Derivative_imp_inc Derivative_imp_inc': included.
298 Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
307 cic:/CoRN/ftc/MoreFunctions/More_Results/I.var
311 cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var
315 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
320 cic:/CoRN/ftc/MoreFunctions/More_Results/F.var
324 cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var
328 cic:/CoRN/ftc/MoreFunctions/More_Results/G.var
332 cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var
336 cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var
340 cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var
343 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con" as lemma.
345 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con" as lemma.
347 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con" as lemma.
349 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con" as lemma.
351 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con" as lemma.
353 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con" as lemma.
355 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con" as lemma.
357 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con" as lemma.
359 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con" as lemma.
361 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con" as lemma.
363 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con" as lemma.
370 Section More_Corollaries
374 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var
378 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var
382 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var
386 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var
390 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var
394 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var
398 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var
402 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var
408 cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var
413 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con" as lemma.
424 cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var
428 cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var
431 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con" as lemma.
436 cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var
440 cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var
444 cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var
449 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con" as lemma.
451 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con" as lemma.
458 Section Diffble_Basic_Properties
461 (*#* **Differentiability
463 Mutatis mutandis for differentiability.
467 cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var
471 cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var
474 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con" as lemma.
476 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con" as lemma.
478 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con" as lemma.
481 cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var
485 cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var
489 cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var
493 cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var
497 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
501 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con" as lemma.
503 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con" as lemma.
505 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con" as lemma.
507 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con" as lemma.
509 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con" as lemma.
511 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con" as lemma.
513 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con" as lemma.
515 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con" as lemma.
517 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con" as lemma.
519 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con" as lemma.
521 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con" as lemma.
524 End Diffble_Basic_Properties
528 Hint Immediate Diffble_imp_inc: included.
532 Section Diffble_Corollaries
536 cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var
540 cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var
544 cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var
548 cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var
552 cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var
556 cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var
559 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con" as lemma.
561 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con" as lemma.
563 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con" as lemma.
565 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con" as lemma.
568 End Diffble_Corollaries
572 Section Nth_Derivative
575 (*#* **Nth Derivative
577 Higher order derivatives pose more interesting problems. It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
581 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var
585 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var
593 %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I].
598 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var
602 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var
606 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var
609 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con" as definition.
611 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
612 (* begin hide *).con" as lemma.
616 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con" as lemma.
618 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con" as lemma.
620 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con" as definition.
627 Section Basic_Results
631 All the usual results hold.
634 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con" as lemma.
636 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con" as lemma.
638 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con" as lemma.
640 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con" as lemma.
642 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con" as lemma.
644 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con" as lemma.
646 inline procedural "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con" as lemma.
648 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con" as lemma.
650 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con" as lemma.
652 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con" as lemma.
654 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con" as lemma.
656 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con" as lemma.
658 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con" as lemma.
660 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con" as lemma.
662 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con" as lemma.
664 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con" as lemma.
666 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con" as lemma.
677 Some new results hold, too:
680 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con" as lemma.
682 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con" as lemma.
684 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con" as lemma.
686 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con" as lemma.
689 Some useful characterization results.
692 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con" as lemma.
694 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con" as lemma.
701 Section Derivating_Diffble
705 As a special case we get a differentiation operator%\ldots%#...#
709 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var
715 cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var
720 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con" as lemma.
722 inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv.con" as definition.
725 End Derivating_Diffble
733 %\ldots%#...# for which the expected property also holds.
736 inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con" as lemma.
739 Some more interesting properties.
742 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con" as lemma.
744 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con" as lemma.
746 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con" as lemma.
748 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con" as lemma.
759 Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv
760 Derivative_minus Derivative_mult Derivative_scal Derivative_nth
761 Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0
762 Derivative_Sum: derivate.
766 Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc:
771 Hint Resolve Deriv_lemma N_Deriv_lemma: derivate.
775 Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous':