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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunctions".
19 (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
21 (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *)
32 Section Basic_Results.
35 (*#* *More about Functions
37 Here we state all the main results about properties of functions that
38 we already proved for compact intervals in the more general setting of
41 %\begin{convention}% Let [I:interval] and [F,F',G,G'] be partial functions.
47 inline cic:/CoRN/ftc/MoreFunctions/I.var.
53 inline cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con.
56 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
60 inline cic:/CoRN/ftc/MoreFunctions/cI.var.
62 inline cic:/CoRN/ftc/MoreFunctions/F.var.
64 inline cic:/CoRN/ftc/MoreFunctions/contF.var.
66 inline cic:/CoRN/ftc/MoreFunctions/continuous_compact.con.
70 inline cic:/CoRN/ftc/MoreFunctions/Hinc.var.
74 inline cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con.
76 inline cic:/CoRN/ftc/MoreFunctions/FNorm.con.
78 inline cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con.
85 Hint Resolve Continuous_imp_inc: included.
89 Section Other_Results.
96 inline cic:/CoRN/ftc/MoreFunctions/I.var.
98 inline cic:/CoRN/ftc/MoreFunctions/F.var.
100 inline cic:/CoRN/ftc/MoreFunctions/G.var.
102 inline cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con.
106 inline cic:/CoRN/ftc/MoreFunctions/contF.var.
108 inline cic:/CoRN/ftc/MoreFunctions/contG.var.
112 inline cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con.
114 inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con.
116 inline cic:/CoRN/ftc/MoreFunctions/Continuous_const.con.
118 inline cic:/CoRN/ftc/MoreFunctions/Continuous_id.con.
120 inline cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con.
122 inline cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con.
124 inline cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con.
126 inline cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con.
128 inline cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con.
130 inline cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con.
132 inline cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con.
134 inline cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con.
141 Hint Resolve continuous_compact Continuous_const Continuous_id
142 Continuous_plus Continuous_inv Continuous_minus Continuous_mult
143 Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous.
147 Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
154 inline cic:/CoRN/ftc/MoreFunctions/I.var.
156 inline cic:/CoRN/ftc/MoreFunctions/cI.var.
158 inline cic:/CoRN/ftc/MoreFunctions/F.var.
160 inline cic:/CoRN/ftc/MoreFunctions/G.var.
162 inline cic:/CoRN/ftc/MoreFunctions/contF.var.
164 inline cic:/CoRN/ftc/MoreFunctions/contG.var.
166 inline cic:/CoRN/ftc/MoreFunctions/Continuous_div.con.
168 inline cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con.
175 Hint Resolve Continuous_div: continuous.
182 inline cic:/CoRN/ftc/MoreFunctions/I.var.
184 inline cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con.
187 %\begin{convention}% Assume [f] is a sequence of continuous functions.
191 inline cic:/CoRN/ftc/MoreFunctions/f.var.
193 inline cic:/CoRN/ftc/MoreFunctions/contF.var.
195 inline cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con.
197 inline cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con.
204 Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
208 Section Basic_Properties.
213 Derivative is not that much different.
215 %\begin{convention}% From this point on we assume [I] to be proper.
219 inline cic:/CoRN/ftc/MoreFunctions/I.var.
221 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
223 inline cic:/CoRN/ftc/MoreFunctions/F.var.
225 inline cic:/CoRN/ftc/MoreFunctions/G.var.
227 inline cic:/CoRN/ftc/MoreFunctions/H.var.
229 inline cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con.
231 inline cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con.
233 inline cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con.
235 inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con.
237 inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con.
239 inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con.
241 inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con.
244 End Basic_Properties.
248 Hint Immediate Derivative_imp_inc Derivative_imp_inc': included.
252 Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
257 Section More_Results.
260 inline cic:/CoRN/ftc/MoreFunctions/I.var.
262 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
265 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
269 inline cic:/CoRN/ftc/MoreFunctions/F.var.
271 inline cic:/CoRN/ftc/MoreFunctions/F'.var.
273 inline cic:/CoRN/ftc/MoreFunctions/G.var.
275 inline cic:/CoRN/ftc/MoreFunctions/G'.var.
277 inline cic:/CoRN/ftc/MoreFunctions/derF.var.
279 inline cic:/CoRN/ftc/MoreFunctions/derG.var.
281 inline cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con.
283 inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con.
285 inline cic:/CoRN/ftc/MoreFunctions/Derivative_const.con.
287 inline cic:/CoRN/ftc/MoreFunctions/Derivative_id.con.
289 inline cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con.
291 inline cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con.
293 inline cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con.
295 inline cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con.
297 inline cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con.
299 inline cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con.
301 inline cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con.
308 Section More_Corollaries.
311 inline cic:/CoRN/ftc/MoreFunctions/I.var.
313 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
315 inline cic:/CoRN/ftc/MoreFunctions/F.var.
317 inline cic:/CoRN/ftc/MoreFunctions/F'.var.
319 inline cic:/CoRN/ftc/MoreFunctions/G.var.
321 inline cic:/CoRN/ftc/MoreFunctions/G'.var.
323 inline cic:/CoRN/ftc/MoreFunctions/derF.var.
325 inline cic:/CoRN/ftc/MoreFunctions/derG.var.
329 inline cic:/CoRN/ftc/MoreFunctions/Gbnd.var.
333 inline cic:/CoRN/ftc/MoreFunctions/Derivative_div.con.
336 End More_Corollaries.
343 inline cic:/CoRN/ftc/MoreFunctions/I.var.
345 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
347 inline cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con.
351 inline cic:/CoRN/ftc/MoreFunctions/f.var.
353 inline cic:/CoRN/ftc/MoreFunctions/f'.var.
355 inline cic:/CoRN/ftc/MoreFunctions/derF.var.
359 inline cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con.
361 inline cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con.
368 Section Diffble_Basic_Properties.
371 (*#* **Differentiability
373 Mutatis mutandis for differentiability.
376 inline cic:/CoRN/ftc/MoreFunctions/I.var.
378 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
380 inline cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con.
382 inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con.
384 inline cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con.
386 inline cic:/CoRN/ftc/MoreFunctions/F.var.
388 inline cic:/CoRN/ftc/MoreFunctions/G.var.
390 inline cic:/CoRN/ftc/MoreFunctions/diffF.var.
392 inline cic:/CoRN/ftc/MoreFunctions/diffG.var.
395 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
399 inline cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con.
401 inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con.
403 inline cic:/CoRN/ftc/MoreFunctions/Diffble_const.con.
405 inline cic:/CoRN/ftc/MoreFunctions/Diffble_id.con.
407 inline cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con.
409 inline cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con.
411 inline cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con.
413 inline cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con.
415 inline cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con.
417 inline cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con.
419 inline cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con.
422 End Diffble_Basic_Properties.
426 Hint Immediate Diffble_imp_inc: included.
430 Section Diffble_Corollaries.
433 inline cic:/CoRN/ftc/MoreFunctions/I.var.
435 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
437 inline cic:/CoRN/ftc/MoreFunctions/F.var.
439 inline cic:/CoRN/ftc/MoreFunctions/G.var.
441 inline cic:/CoRN/ftc/MoreFunctions/diffF.var.
443 inline cic:/CoRN/ftc/MoreFunctions/diffG.var.
445 inline cic:/CoRN/ftc/MoreFunctions/Diffble_div.con.
447 inline cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con.
449 inline cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con.
451 inline cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con.
454 End Diffble_Corollaries.
458 Section Nth_Derivative.
461 (*#* **Nth Derivative
463 Higher order derivatives pose more interesting problems. It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
466 inline cic:/CoRN/ftc/MoreFunctions/I.var.
468 inline cic:/CoRN/ftc/MoreFunctions/pI.var.
475 %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I].
479 inline cic:/CoRN/ftc/MoreFunctions/n.var.
481 inline cic:/CoRN/ftc/MoreFunctions/F.var.
483 inline cic:/CoRN/ftc/MoreFunctions/diffF.var.
485 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con.
487 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
488 (* begin hide *).con.
492 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con.
494 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con.
496 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv.con.
503 Section Basic_Results.
507 All the usual results hold.
510 inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con.
512 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con.
514 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con.
516 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con.
518 inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con.
520 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con.
522 inline cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con.
524 inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con.
526 inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con.
528 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con.
530 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con.
532 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con.
534 inline cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con.
536 inline cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con.
538 inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con.
540 inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con.
542 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con.
549 Section More_Results.
553 Some new results hold, too:
556 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con.
558 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con.
560 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con.
562 inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con.
565 Some useful characterization results.
568 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con.
570 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con.
577 Section Derivating_Diffble.
581 As a special case we get a differentiation operator%\ldots%#...#
584 inline cic:/CoRN/ftc/MoreFunctions/F.var.
588 inline cic:/CoRN/ftc/MoreFunctions/diffF.var.
592 inline cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con.
594 inline cic:/CoRN/ftc/MoreFunctions/Deriv.con.
597 End Derivating_Diffble.
605 %\ldots%#...# for which the expected property also holds.
608 inline cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con.
611 Some more interesting properties.
614 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con.
616 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con.
618 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con.
620 inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con.
631 Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv
632 Derivative_minus Derivative_mult Derivative_scal Derivative_nth
633 Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0
634 Derivative_Sum: derivate.
638 Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc:
643 Hint Resolve Deriv_lemma N_Deriv_lemma: derivate.
647 Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous':