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/Differentiability".
19 (* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
33 (*#* *Differentiability
35 We will now use our work on derivatives to define a notion of
36 differentiable function and prove its main properties.
38 %\begin{convention}% Throughout this section, [a,b] will be real
39 numbers with [a [<] b], [I] will denote the interval [[a,b]]
40 and [F,G,H] will be differentiable functions.
43 Usually a function [F] is said to be differentiable in a proper
44 compact interval [[a,b]] if there exists another function [F']
45 such that [F'] is a derivative of [F] in that interval. There is a
46 problem in formalizing this definition, as we pointed out earlier on,
47 which is that if we simply write it down as is we are not able to get
48 such a function [F'] from a hypothesis that [F] is differentiable.
50 However, it turns out that this is not altogether the best definition
51 for the following reason: if we say that [F] is differentiable in
52 [[a,b]], we mean that there is a partial function [F'] which is
53 defined in [[a,b]] and satisfies a certain condition in that
54 interval but nothing is required of the behaviour of the function
55 outside [[a,b]]. Thus we can argue that, from a mathematical
56 point of view, the [F'] that we get eliminating a hypothesis of
57 differentiability should be defined exactly on that interval. If we
58 do this, we can quantify over the set of setoid functions in that
59 interval and eliminate the existencial quantifier without any
63 inline cic:/CoRN/ftc/Differentiability/Diffble_I.con.
70 Implicit Arguments Diffble_I [a b].
74 Section Local_Properties.
78 From this point on, we just prove results analogous to the ones for derivability.
80 A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]].
83 inline cic:/CoRN/ftc/Differentiability/included_imp_diffble.con.
86 A function differentiable in an interval is everywhere defined in that interval.
89 inline cic:/CoRN/ftc/Differentiability/a.var.
91 inline cic:/CoRN/ftc/Differentiability/b.var.
93 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
97 inline cic:/CoRN/ftc/Differentiability/Hab.con.
99 inline cic:/CoRN/ftc/Differentiability/I.con.
103 inline cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con.
106 If a function has a derivative in an interval then it is differentiable in that interval.
109 inline cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con.
112 End Local_Properties.
116 Hint Resolve diffble_imp_inc: included.
124 All the algebraic results carry on.
127 inline cic:/CoRN/ftc/Differentiability/a.var.
129 inline cic:/CoRN/ftc/Differentiability/b.var.
131 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
135 inline cic:/CoRN/ftc/Differentiability/Hab.con.
137 inline cic:/CoRN/ftc/Differentiability/I.con.
145 inline cic:/CoRN/ftc/Differentiability/Diffble_I_const.con.
147 inline cic:/CoRN/ftc/Differentiability/Diffble_I_id.con.
154 Section Well_Definedness.
157 inline cic:/CoRN/ftc/Differentiability/F.var.
159 inline cic:/CoRN/ftc/Differentiability/H.var.
161 inline cic:/CoRN/ftc/Differentiability/diffF.var.
163 inline cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con.
166 End Well_Definedness.
169 inline cic:/CoRN/ftc/Differentiability/F.var.
171 inline cic:/CoRN/ftc/Differentiability/G.var.
173 inline cic:/CoRN/ftc/Differentiability/diffF.var.
175 inline cic:/CoRN/ftc/Differentiability/diffG.var.
177 inline cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con.
179 inline cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con.
181 inline cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con.
185 inline cic:/CoRN/ftc/Differentiability/Gbnd.var.
189 inline cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con.
199 inline cic:/CoRN/ftc/Differentiability/a.var.
201 inline cic:/CoRN/ftc/Differentiability/b.var.
203 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
207 inline cic:/CoRN/ftc/Differentiability/Hab.con.
209 inline cic:/CoRN/ftc/Differentiability/I.con.
213 inline cic:/CoRN/ftc/Differentiability/F.var.
215 inline cic:/CoRN/ftc/Differentiability/G.var.
217 inline cic:/CoRN/ftc/Differentiability/diffF.var.
219 inline cic:/CoRN/ftc/Differentiability/diffG.var.
221 inline cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con.
223 inline cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con.
225 inline cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con.
227 inline cic:/CoRN/ftc/Differentiability/Gbnd.var.
229 inline cic:/CoRN/ftc/Differentiability/Diffble_I_div.con.
236 Section Other_Properties.
240 Differentiability of families of functions is proved by
241 induction using the constant and addition rules.
244 inline cic:/CoRN/ftc/Differentiability/a.var.
246 inline cic:/CoRN/ftc/Differentiability/b.var.
248 inline cic:/CoRN/ftc/Differentiability/Hab'.var.
250 inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con.
252 inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con.
254 inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con.
257 End Other_Properties.
261 Finally, a differentiable function is continuous.
263 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
267 inline cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con.
270 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
271 diffble_imp_contin_I: continuous.
275 Hint Immediate included_imp_deriv: derivate.