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: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
21 include "ftc/PartInterval.ma".
23 include "ftc/DerivativeOps.ma".
29 (*#* *Differentiability
31 We will now use our work on derivatives to define a notion of
32 differentiable function and prove its main properties.
34 %\begin{convention}% Throughout this section, [a,b] will be real
35 numbers with [a [<] b], [I] will denote the interval [[a,b]]
36 and [F,G,H] will be differentiable functions.
39 Usually a function [F] is said to be differentiable in a proper
40 compact interval [[a,b]] if there exists another function [F']
41 such that [F'] is a derivative of [F] in that interval. There is a
42 problem in formalizing this definition, as we pointed out earlier on,
43 which is that if we simply write it down as is we are not able to get
44 such a function [F'] from a hypothesis that [F] is differentiable.
46 However, it turns out that this is not altogether the best definition
47 for the following reason: if we say that [F] is differentiable in
48 [[a,b]], we mean that there is a partial function [F'] which is
49 defined in [[a,b]] and satisfies a certain condition in that
50 interval but nothing is required of the behaviour of the function
51 outside [[a,b]]. Thus we can argue that, from a mathematical
52 point of view, the [F'] that we get eliminating a hypothesis of
53 differentiability should be defined exactly on that interval. If we
54 do this, we can quantify over the set of setoid functions in that
55 interval and eliminate the existencial quantifier without any
59 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I.con" as definition.
66 Implicit Arguments Diffble_I [a b].
70 Section Local_Properties
74 From this point on, we just prove results analogous to the ones for derivability.
76 A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]].
79 inline procedural "cic:/CoRN/ftc/Differentiability/included_imp_diffble.con" as lemma.
82 A function differentiable in an interval is everywhere defined in that interval.
86 cic:/CoRN/ftc/Differentiability/Local_Properties/a.var
90 cic:/CoRN/ftc/Differentiability/Local_Properties/b.var
94 cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var
99 inline procedural "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab.con" "Local_Properties__" as definition.
101 inline procedural "cic:/CoRN/ftc/Differentiability/Local_Properties/I.con" "Local_Properties__" as definition.
105 inline procedural "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con" as lemma.
108 If a function has a derivative in an interval then it is differentiable in that interval.
111 inline procedural "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con" as lemma.
118 Hint Resolve diffble_imp_inc: included.
126 All the algebraic results carry on.
130 cic:/CoRN/ftc/Differentiability/Operations/a.var
134 cic:/CoRN/ftc/Differentiability/Operations/b.var
138 cic:/CoRN/ftc/Differentiability/Operations/Hab'.var
143 inline procedural "cic:/CoRN/ftc/Differentiability/Operations/Hab.con" "Operations__" as definition.
145 inline procedural "cic:/CoRN/ftc/Differentiability/Operations/I.con" "Operations__" as definition.
153 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con" as lemma.
155 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con" as lemma.
162 Section Well_Definedness
166 cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var
170 cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var
174 cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var
177 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con" as lemma.
184 cic:/CoRN/ftc/Differentiability/Operations/F.var
188 cic:/CoRN/ftc/Differentiability/Operations/G.var
192 cic:/CoRN/ftc/Differentiability/Operations/diffF.var
196 cic:/CoRN/ftc/Differentiability/Operations/diffG.var
199 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con" as lemma.
201 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con" as lemma.
203 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con" as lemma.
208 cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var
213 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con" as lemma.
224 cic:/CoRN/ftc/Differentiability/Corollaries/a.var
228 cic:/CoRN/ftc/Differentiability/Corollaries/b.var
232 cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var
237 inline procedural "cic:/CoRN/ftc/Differentiability/Corollaries/Hab.con" "Corollaries__" as definition.
239 inline procedural "cic:/CoRN/ftc/Differentiability/Corollaries/I.con" "Corollaries__" as definition.
244 cic:/CoRN/ftc/Differentiability/Corollaries/F.var
248 cic:/CoRN/ftc/Differentiability/Corollaries/G.var
252 cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var
256 cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var
259 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con" as lemma.
261 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con" as lemma.
263 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con" as lemma.
266 cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var
269 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con" as lemma.
276 Section Other_Properties
280 Differentiability of families of functions is proved by
281 induction using the constant and addition rules.
285 cic:/CoRN/ftc/Differentiability/Other_Properties/a.var
289 cic:/CoRN/ftc/Differentiability/Other_Properties/b.var
293 cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var
296 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con" as lemma.
298 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con" as lemma.
300 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con" as lemma.
307 Finally, a differentiable function is continuous.
309 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
313 inline procedural "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con" as lemma.
316 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
317 diffble_imp_contin_I: continuous.
321 Hint Immediate included_imp_deriv: derivate.