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.
45 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var".
51 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con" as lemma.
54 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
58 alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var".
60 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var".
62 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var".
64 inline procedural "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con" as lemma.
68 alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var".
72 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con" as lemma.
74 inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm.con" as definition.
76 inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con" as lemma.
83 Hint Resolve Continuous_imp_inc: included.
94 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var".
96 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var".
98 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var".
100 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con" as lemma.
104 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var".
106 alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var".
110 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con" as lemma.
112 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con" as lemma.
114 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con" as lemma.
116 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con" as lemma.
118 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con" as lemma.
120 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con" as lemma.
122 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con" as lemma.
124 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con" as lemma.
126 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con" as lemma.
128 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con" as lemma.
130 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con" as lemma.
132 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con" as lemma.
139 Hint Resolve continuous_compact Continuous_const Continuous_id
140 Continuous_plus Continuous_inv Continuous_minus Continuous_mult
141 Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous.
145 Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
152 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var".
154 alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var".
156 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var".
158 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var".
160 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var".
162 alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var".
164 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con" as lemma.
166 inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con" as lemma.
173 Hint Resolve Continuous_div: continuous.
180 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var".
182 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con" as lemma.
185 %\begin{convention}% Assume [f] is a sequence of continuous functions.
189 alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var".
191 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var".
193 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con" as lemma.
195 inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con" as lemma.
202 Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
206 Section Basic_Properties
211 Derivative is not that much different.
213 %\begin{convention}% From this point on we assume [I] to be proper.
217 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var".
219 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var".
221 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var".
223 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var".
225 alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var".
227 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con" as lemma.
229 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con" as lemma.
231 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con" as lemma.
233 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con" as lemma.
235 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con" as lemma.
237 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con" as lemma.
239 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con" as lemma.
246 Hint Immediate Derivative_imp_inc Derivative_imp_inc': included.
250 Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
258 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var".
260 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var".
263 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
267 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var".
269 alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var".
271 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var".
273 alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var".
275 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var".
277 alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var".
279 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con" as lemma.
281 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con" as lemma.
283 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con" as lemma.
285 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con" as lemma.
287 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con" as lemma.
289 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con" as lemma.
291 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con" as lemma.
293 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con" as lemma.
295 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con" as lemma.
297 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con" as lemma.
299 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con" as lemma.
306 Section More_Corollaries
309 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var".
311 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var".
313 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var".
315 alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var".
317 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var".
319 alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var".
321 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var".
323 alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var".
327 alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var".
331 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con" as lemma.
341 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var".
343 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var".
345 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con" as lemma.
349 alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var".
351 alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var".
353 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var".
357 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con" as lemma.
359 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con" as lemma.
366 Section Diffble_Basic_Properties
369 (*#* **Differentiability
371 Mutatis mutandis for differentiability.
374 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var".
376 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var".
378 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con" as lemma.
380 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con" as lemma.
382 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con" as lemma.
384 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var".
386 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var".
388 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var".
390 alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var".
393 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
397 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con" as lemma.
399 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con" as lemma.
401 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con" as lemma.
403 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con" as lemma.
405 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con" as lemma.
407 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con" as lemma.
409 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con" as lemma.
411 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con" as lemma.
413 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con" as lemma.
415 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con" as lemma.
417 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con" as lemma.
420 End Diffble_Basic_Properties
424 Hint Immediate Diffble_imp_inc: included.
428 Section Diffble_Corollaries
431 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var".
433 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var".
435 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var".
437 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var".
439 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var".
441 alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var".
443 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con" as lemma.
445 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con" as lemma.
447 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con" as lemma.
449 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con" as lemma.
452 End Diffble_Corollaries
456 Section Nth_Derivative
459 (*#* **Nth Derivative
461 Higher order derivatives pose more interesting problems. It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
464 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var".
466 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var".
473 %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I].
477 alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var".
479 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var".
481 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var".
483 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con" as definition.
485 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
486 (* begin hide *).con" as lemma.
490 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con" as lemma.
492 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con" as lemma.
494 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con" as definition.
501 Section Basic_Results
505 All the usual results hold.
508 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con" as lemma.
510 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con" as lemma.
512 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con" as lemma.
514 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con" as lemma.
516 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con" as lemma.
518 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con" as lemma.
520 inline procedural "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con" as lemma.
522 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con" as lemma.
524 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con" as lemma.
526 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con" as lemma.
528 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con" as lemma.
530 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con" as lemma.
532 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con" as lemma.
534 inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con" as lemma.
536 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con" as lemma.
538 inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con" as lemma.
540 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con" as lemma.
551 Some new results hold, too:
554 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con" as lemma.
556 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con" as lemma.
558 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con" as lemma.
560 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con" as lemma.
563 Some useful characterization results.
566 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con" as lemma.
568 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con" as lemma.
575 Section Derivating_Diffble
579 As a special case we get a differentiation operator%\ldots%#...#
582 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var".
586 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var".
590 inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con" as lemma.
592 inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv.con" as definition.
595 End Derivating_Diffble
603 %\ldots%#...# for which the expected property also holds.
606 inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con" as lemma.
609 Some more interesting properties.
612 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con" as lemma.
614 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con" as lemma.
616 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con" as lemma.
618 inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con" as lemma.
629 Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv
630 Derivative_minus Derivative_mult Derivative_scal Derivative_nth
631 Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0
632 Derivative_Sum: derivate.
636 Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc:
641 Hint Resolve Deriv_lemma N_Deriv_lemma: derivate.
645 Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous':