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 include "CoRN_notation.ma".
21 (* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
23 include "ftc/PartInterval.ma".
25 include "ftc/DerivativeOps.ma".
31 (*#* *Differentiability
33 We will now use our work on derivatives to define a notion of
34 differentiable function and prove its main properties.
36 %\begin{convention}% Throughout this section, [a,b] will be real
37 numbers with [a [<] b], [I] will denote the interval [[a,b]]
38 and [F,G,H] will be differentiable functions.
41 Usually a function [F] is said to be differentiable in a proper
42 compact interval [[a,b]] if there exists another function [F']
43 such that [F'] is a derivative of [F] in that interval. There is a
44 problem in formalizing this definition, as we pointed out earlier on,
45 which is that if we simply write it down as is we are not able to get
46 such a function [F'] from a hypothesis that [F] is differentiable.
48 However, it turns out that this is not altogether the best definition
49 for the following reason: if we say that [F] is differentiable in
50 [[a,b]], we mean that there is a partial function [F'] which is
51 defined in [[a,b]] and satisfies a certain condition in that
52 interval but nothing is required of the behaviour of the function
53 outside [[a,b]]. Thus we can argue that, from a mathematical
54 point of view, the [F'] that we get eliminating a hypothesis of
55 differentiability should be defined exactly on that interval. If we
56 do this, we can quantify over the set of setoid functions in that
57 interval and eliminate the existencial quantifier without any
61 inline "cic:/CoRN/ftc/Differentiability/Diffble_I.con".
68 Implicit Arguments Diffble_I [a b].
72 Section Local_Properties.
76 From this point on, we just prove results analogous to the ones for derivability.
78 A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]].
81 inline "cic:/CoRN/ftc/Differentiability/included_imp_diffble.con".
84 A function differentiable in an interval is everywhere defined in that interval.
87 inline "cic:/CoRN/ftc/Differentiability/a.var".
89 inline "cic:/CoRN/ftc/Differentiability/b.var".
91 inline "cic:/CoRN/ftc/Differentiability/Hab'.var".
95 inline "cic:/CoRN/ftc/Differentiability/Hab.con".
97 inline "cic:/CoRN/ftc/Differentiability/I.con".
101 inline "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con".
104 If a function has a derivative in an interval then it is differentiable in that interval.
107 inline "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con".
110 End Local_Properties.
114 Hint Resolve diffble_imp_inc: included.
122 All the algebraic results carry on.
125 inline "cic:/CoRN/ftc/Differentiability/a.var".
127 inline "cic:/CoRN/ftc/Differentiability/b.var".
129 inline "cic:/CoRN/ftc/Differentiability/Hab'.var".
133 inline "cic:/CoRN/ftc/Differentiability/Hab.con".
135 inline "cic:/CoRN/ftc/Differentiability/I.con".
143 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con".
145 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con".
152 Section Well_Definedness.
155 inline "cic:/CoRN/ftc/Differentiability/F.var".
157 inline "cic:/CoRN/ftc/Differentiability/H.var".
159 inline "cic:/CoRN/ftc/Differentiability/diffF.var".
161 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con".
164 End Well_Definedness.
167 inline "cic:/CoRN/ftc/Differentiability/F.var".
169 inline "cic:/CoRN/ftc/Differentiability/G.var".
171 inline "cic:/CoRN/ftc/Differentiability/diffF.var".
173 inline "cic:/CoRN/ftc/Differentiability/diffG.var".
175 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con".
177 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con".
179 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con".
183 inline "cic:/CoRN/ftc/Differentiability/Gbnd.var".
187 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con".
197 inline "cic:/CoRN/ftc/Differentiability/a.var".
199 inline "cic:/CoRN/ftc/Differentiability/b.var".
201 inline "cic:/CoRN/ftc/Differentiability/Hab'.var".
205 inline "cic:/CoRN/ftc/Differentiability/Hab.con".
207 inline "cic:/CoRN/ftc/Differentiability/I.con".
211 inline "cic:/CoRN/ftc/Differentiability/F.var".
213 inline "cic:/CoRN/ftc/Differentiability/G.var".
215 inline "cic:/CoRN/ftc/Differentiability/diffF.var".
217 inline "cic:/CoRN/ftc/Differentiability/diffG.var".
219 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con".
221 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con".
223 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con".
225 inline "cic:/CoRN/ftc/Differentiability/Gbnd.var".
227 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con".
234 Section Other_Properties.
238 Differentiability of families of functions is proved by
239 induction using the constant and addition rules.
242 inline "cic:/CoRN/ftc/Differentiability/a.var".
244 inline "cic:/CoRN/ftc/Differentiability/b.var".
246 inline "cic:/CoRN/ftc/Differentiability/Hab'.var".
248 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con".
250 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con".
252 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con".
255 End Other_Properties.
259 Finally, a differentiable function is continuous.
261 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
265 inline "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con".
268 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
269 diffble_imp_contin_I: continuous.
273 Hint Immediate included_imp_deriv: derivate.