]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/ftc/Differentiability.ma
made executable again
[helm.git] / matita / matita / contribs / CoRN-Decl / ftc / Differentiability.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/Differentiability".
18
19 include "CoRN.ma".
20
21 (* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
22
23 include "ftc/PartInterval.ma".
24
25 include "ftc/DerivativeOps.ma".
26
27 (* UNEXPORTED
28 Section Definitions
29 *)
30
31 (*#* *Differentiability
32
33 We will now use our work on derivatives to define a notion of
34 differentiable function and prove its main properties.
35
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.
39 %\end{convention}%
40
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.
47
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
58 problems.
59 *)
60
61 inline "cic:/CoRN/ftc/Differentiability/Diffble_I.con".
62
63 (* UNEXPORTED
64 End Definitions
65 *)
66
67 (* UNEXPORTED
68 Implicit Arguments Diffble_I [a b].
69 *)
70
71 (* UNEXPORTED
72 Section Local_Properties
73 *)
74
75 (*#*
76 From this point on, we just prove results analogous to the ones for derivability.
77
78 A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]].
79 *)
80
81 inline "cic:/CoRN/ftc/Differentiability/included_imp_diffble.con".
82
83 (*#*
84 A function differentiable in an interval is everywhere defined in that interval.
85 *)
86
87 alias id "a" = "cic:/CoRN/ftc/Differentiability/Local_Properties/a.var".
88
89 alias id "b" = "cic:/CoRN/ftc/Differentiability/Local_Properties/b.var".
90
91 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var".
92
93 (* begin hide *)
94
95 inline "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab.con" "Local_Properties__".
96
97 inline "cic:/CoRN/ftc/Differentiability/Local_Properties/I.con" "Local_Properties__".
98
99 (* end hide *)
100
101 inline "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con".
102
103 (*#*
104 If a function has a derivative in an interval then it is differentiable in that interval.
105 *)
106
107 inline "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con".
108
109 (* UNEXPORTED
110 End Local_Properties
111 *)
112
113 (* UNEXPORTED
114 Hint Resolve diffble_imp_inc: included.
115 *)
116
117 (* UNEXPORTED
118 Section Operations
119 *)
120
121 (*#*
122 All the algebraic results carry on.
123 *)
124
125 alias id "a" = "cic:/CoRN/ftc/Differentiability/Operations/a.var".
126
127 alias id "b" = "cic:/CoRN/ftc/Differentiability/Operations/b.var".
128
129 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Operations/Hab'.var".
130
131 (* begin hide *)
132
133 inline "cic:/CoRN/ftc/Differentiability/Operations/Hab.con" "Operations__".
134
135 inline "cic:/CoRN/ftc/Differentiability/Operations/I.con" "Operations__".
136
137 (* end hide *)
138
139 (* UNEXPORTED
140 Section Constants
141 *)
142
143 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con".
144
145 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con".
146
147 (* UNEXPORTED
148 End Constants
149 *)
150
151 (* UNEXPORTED
152 Section Well_Definedness
153 *)
154
155 alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var".
156
157 alias id "H" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var".
158
159 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var".
160
161 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con".
162
163 (* UNEXPORTED
164 End Well_Definedness
165 *)
166
167 alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/F.var".
168
169 alias id "G" = "cic:/CoRN/ftc/Differentiability/Operations/G.var".
170
171 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/diffF.var".
172
173 alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Operations/diffG.var".
174
175 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con".
176
177 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con".
178
179 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con".
180
181 (* begin show *)
182
183 alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var".
184
185 (* end show *)
186
187 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con".
188
189 (* UNEXPORTED
190 End Operations
191 *)
192
193 (* UNEXPORTED
194 Section Corollaries
195 *)
196
197 alias id "a" = "cic:/CoRN/ftc/Differentiability/Corollaries/a.var".
198
199 alias id "b" = "cic:/CoRN/ftc/Differentiability/Corollaries/b.var".
200
201 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var".
202
203 (* begin hide *)
204
205 inline "cic:/CoRN/ftc/Differentiability/Corollaries/Hab.con" "Corollaries__".
206
207 inline "cic:/CoRN/ftc/Differentiability/Corollaries/I.con" "Corollaries__".
208
209 (* end hide *)
210
211 alias id "F" = "cic:/CoRN/ftc/Differentiability/Corollaries/F.var".
212
213 alias id "G" = "cic:/CoRN/ftc/Differentiability/Corollaries/G.var".
214
215 alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var".
216
217 alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var".
218
219 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con".
220
221 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con".
222
223 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con".
224
225 alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var".
226
227 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con".
228
229 (* UNEXPORTED
230 End Corollaries
231 *)
232
233 (* UNEXPORTED
234 Section Other_Properties
235 *)
236
237 (*#*
238 Differentiability of families of functions is proved by
239 induction using the constant and addition rules.
240 *)
241
242 alias id "a" = "cic:/CoRN/ftc/Differentiability/Other_Properties/a.var".
243
244 alias id "b" = "cic:/CoRN/ftc/Differentiability/Other_Properties/b.var".
245
246 alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var".
247
248 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con".
249
250 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con".
251
252 inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con".
253
254 (* UNEXPORTED
255 End Other_Properties
256 *)
257
258 (*#*
259 Finally, a differentiable function is continuous.
260
261 %\begin{convention}% Let [F] be a partial function with derivative [F'] on [I].
262 %\end{convention}%
263 *)
264
265 inline "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con".
266
267 (* UNEXPORTED
268 Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I
269   diffble_imp_contin_I: continuous.
270 *)
271
272 (* UNEXPORTED
273 Hint Immediate included_imp_deriv: derivate.
274 *)
275