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".
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".
82 A function differentiable in an interval is everywhere defined in that interval.
85 alias id "a" = "cic:/CoRN/ftc/Differentiability/Local_Properties/a.var".
87 alias id "b" = "cic:/CoRN/ftc/Differentiability/Local_Properties/b.var".
89 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var".
93 inline procedural "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab.con" "Local_Properties__".
95 inline procedural "cic:/CoRN/ftc/Differentiability/Local_Properties/I.con" "Local_Properties__".
99 inline procedural "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con".
102 If a function has a derivative in an interval then it is differentiable in that interval.
105 inline procedural "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con".
112 Hint Resolve diffble_imp_inc: included.
120 All the algebraic results carry on.
123 alias id "a" = "cic:/CoRN/ftc/Differentiability/Operations/a.var".
125 alias id "b" = "cic:/CoRN/ftc/Differentiability/Operations/b.var".
127 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Operations/Hab'.var".
131 inline procedural "cic:/CoRN/ftc/Differentiability/Operations/Hab.con" "Operations__".
133 inline procedural "cic:/CoRN/ftc/Differentiability/Operations/I.con" "Operations__".
141 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con".
143 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con".
150 Section Well_Definedness
153 alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var".
155 alias id "H" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var".
157 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var".
159 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con".
165 alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/F.var".
167 alias id "G" = "cic:/CoRN/ftc/Differentiability/Operations/G.var".
169 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/diffF.var".
171 alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Operations/diffG.var".
173 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con".
175 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con".
177 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con".
181 alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var".
185 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con".
195 alias id "a" = "cic:/CoRN/ftc/Differentiability/Corollaries/a.var".
197 alias id "b" = "cic:/CoRN/ftc/Differentiability/Corollaries/b.var".
199 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var".
203 inline procedural "cic:/CoRN/ftc/Differentiability/Corollaries/Hab.con" "Corollaries__".
205 inline procedural "cic:/CoRN/ftc/Differentiability/Corollaries/I.con" "Corollaries__".
209 alias id "F" = "cic:/CoRN/ftc/Differentiability/Corollaries/F.var".
211 alias id "G" = "cic:/CoRN/ftc/Differentiability/Corollaries/G.var".
213 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var".
215 alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var".
217 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con".
219 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con".
221 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con".
223 alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var".
225 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con".
232 Section Other_Properties
236 Differentiability of families of functions is proved by
237 induction using the constant and addition rules.
240 alias id "a" = "cic:/CoRN/ftc/Differentiability/Other_Properties/a.var".
242 alias id "b" = "cic:/CoRN/ftc/Differentiability/Other_Properties/b.var".
244 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var".
246 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con".
248 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con".
250 inline procedural "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con".
257 Finally, a differentiable function is continuous.
259 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
263 inline procedural "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con".
266 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
267 diffble_imp_contin_I: continuous.
271 Hint Immediate included_imp_deriv: derivate.