]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/CoRN-Decl/ftc/Continuity.ma
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
[helm.git] / matitaB / matita / contribs / CoRN-Decl / ftc / Continuity.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/Continuity".
18
19 include "CoRN.ma".
20
21 (* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
22
23 (*#* printing Norm_Funct %\ensuremath{\|\cdot\|}% *)
24
25 include "reals/NRootIR.ma".
26
27 include "ftc/FunctSums.ma".
28
29 (* UNEXPORTED
30 Section Definitions_and_Basic_Results
31 *)
32
33 (*#* *Continuity
34
35 Constructively, continuity is the most fundamental property of any
36 function---so strongly that no example is known of a constructive
37 function that is not continuous.  However, the classical definition of
38 continuity is not good for our purposes, as it is not true, for
39 example, that a function which is continuous in a compact interval is
40 uniformly continuous in that same interval (for a discussion of this
41 see Bishop 1967).  Thus, our notion of continuity will be the uniform
42 one#. #%\footnote{%Similar remarks apply to convergence of sequences
43 of functions, which we will define ahead, and elsewhere; we will
44 refrain from discussing this issue at those places.%}.%
45
46 %\begin{convention}% Throughout this section, [a] and [b] will be real
47 numbers, [I] will denote the compact interval [[a,b]] and
48 [F, G, H] will denote arbitrary partial functions with domains
49 respectively [P, Q] and [R].
50 %\end{convention}%
51
52 ** Definitions and Basic Results
53
54 Here we define continuity and prove some basic properties of continuous functions.
55 *)
56
57 alias id "a" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var".
58
59 alias id "b" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var".
60
61 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var".
62
63 (* begin hide *)
64
65 inline "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con" "Definitions_and_Basic_Results__".
66
67 (* end hide *)
68
69 alias id "F" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var".
70
71 (* begin hide *)
72
73 inline "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/P.con" "Definitions_and_Basic_Results__".
74
75 (* end hide *)
76
77 inline "cic:/CoRN/ftc/Continuity/Continuous_I.con".
78
79 (*#*
80 For convenience, we distinguish the two properties of continuous functions.
81 *)
82
83 inline "cic:/CoRN/ftc/Continuity/contin_imp_inc.con".
84
85 inline "cic:/CoRN/ftc/Continuity/contin_prop.con".
86
87 (*#*
88 Assume [F] to be continuous in [I].  Then it has a least upper bound and a greater lower bound on [I].
89 *)
90
91 alias id "contF" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var".
92
93 (* begin hide *)
94
95 inline "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hinc'.con" "Definitions_and_Basic_Results__".
96
97 (* end hide *)
98
99 inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con".
100
101 inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con".
102
103 inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con".
104
105 (*#*
106 We now make this glb and lub into operators.
107 *)
108
109 inline "cic:/CoRN/ftc/Continuity/lub_funct.con".
110
111 inline "cic:/CoRN/ftc/Continuity/glb_funct.con".
112
113 (*#*
114 These operators have the expected properties.
115 *)
116
117 inline "cic:/CoRN/ftc/Continuity/lub_is_lub.con".
118
119 inline "cic:/CoRN/ftc/Continuity/glb_is_glb.con".
120
121 inline "cic:/CoRN/ftc/Continuity/glb_prop.con".
122
123 inline "cic:/CoRN/ftc/Continuity/lub_prop.con".
124
125 (*#*
126 The norm of a function is defined as being the supremum of its absolute value; that is equivalent to the following definition (which is often more convenient to use).
127 *)
128
129 inline "cic:/CoRN/ftc/Continuity/Norm_Funct.con".
130
131 (*#*
132 The norm effectively bounds the absolute value of a function.
133 *)
134
135 inline "cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con".
136
137 (*#*
138 The following is another way of characterizing the norm:
139 *)
140
141 inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con".
142
143 (*#*
144 We now prove some basic properties of the norm---namely that it is positive, and that it provides a least upper bound for the absolute value of its argument.
145 *)
146
147 inline "cic:/CoRN/ftc/Continuity/positive_norm.con".
148
149 inline "cic:/CoRN/ftc/Continuity/norm_fun_lub.con".
150
151 inline "cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con".
152
153 inline "cic:/CoRN/ftc/Continuity/less_Norm_Funct.con".
154
155 (* UNEXPORTED
156 End Definitions_and_Basic_Results
157 *)
158
159 (* UNEXPORTED
160 Implicit Arguments Continuous_I [a b].
161 *)
162
163 (* UNEXPORTED
164 Implicit Arguments Norm_Funct [a b Hab F].
165 *)
166
167 (* UNEXPORTED
168 Section Local_Results
169 *)
170
171 (*#* **Algebraic Properties
172
173 We now state and prove some results about continuous functions.  Assume that [I] is included in the domain of both [F] and [G].
174 *)
175
176 alias id "a" = "cic:/CoRN/ftc/Continuity/Local_Results/a.var".
177
178 alias id "b" = "cic:/CoRN/ftc/Continuity/Local_Results/b.var".
179
180 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Local_Results/Hab.var".
181
182 (* begin hide *)
183
184 inline "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results__".
185
186 (* end hide *)
187
188 alias id "F" = "cic:/CoRN/ftc/Continuity/Local_Results/F.var".
189
190 alias id "G" = "cic:/CoRN/ftc/Continuity/Local_Results/G.var".
191
192 (* begin hide *)
193
194 inline "cic:/CoRN/ftc/Continuity/Local_Results/P.con" "Local_Results__".
195
196 inline "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results__".
197
198 (* end hide *)
199
200 alias id "incF" = "cic:/CoRN/ftc/Continuity/Local_Results/incF.var".
201
202 alias id "incG" = "cic:/CoRN/ftc/Continuity/Local_Results/incG.var".
203
204 (*#*
205 The first result does not require the function to be continuous; however, its preconditions are easily verified by continuous functions, which justifies its inclusion in this section.
206 *)
207
208 inline "cic:/CoRN/ftc/Continuity/cont_no_sign_change.con".
209
210 inline "cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con".
211
212 inline "cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con".
213
214 (*#*
215 Being continuous is an extensional property.
216 *)
217
218 inline "cic:/CoRN/ftc/Continuity/Continuous_I_wd.con".
219
220 (*#*
221 A continuous function remains continuous if you restrict its domain.
222 *)
223
224 inline "cic:/CoRN/ftc/Continuity/included_imp_contin.con".
225
226 (*#*
227 Constant functions and identity are continuous.
228 *)
229
230 inline "cic:/CoRN/ftc/Continuity/Continuous_I_const.con".
231
232 inline "cic:/CoRN/ftc/Continuity/Continuous_I_id.con".
233
234 (*#*
235 Assume [F] and [G] are continuous in [I].  Then functions derived from these through algebraic operations are also continuous, provided (in the case of reciprocal and division) some extra conditions are met.
236 *)
237
238 alias id "contF" = "cic:/CoRN/ftc/Continuity/Local_Results/contF.var".
239
240 alias id "contG" = "cic:/CoRN/ftc/Continuity/Local_Results/contG.var".
241
242 inline "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con".
243
244 inline "cic:/CoRN/ftc/Continuity/Continuous_I_inv.con".
245
246 inline "cic:/CoRN/ftc/Continuity/Continuous_I_mult.con".
247
248 (* UNEXPORTED
249 Opaque AbsIR Max.
250 *)
251
252 (* UNEXPORTED
253 Transparent AbsIR Max.
254 *)
255
256 inline "cic:/CoRN/ftc/Continuity/Continuous_I_max.con".
257
258 (* begin show *)
259
260 alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var".
261
262 alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var".
263
264 (* end show *)
265
266 inline "cic:/CoRN/ftc/Continuity/Continuous_I_recip.con".
267
268 (* UNEXPORTED
269 End Local_Results
270 *)
271
272 (* UNEXPORTED
273 Hint Resolve contin_imp_inc: included.
274 *)
275
276 (* UNEXPORTED
277 Section Corolaries
278 *)
279
280 alias id "a" = "cic:/CoRN/ftc/Continuity/Corolaries/a.var".
281
282 alias id "b" = "cic:/CoRN/ftc/Continuity/Corolaries/b.var".
283
284 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Corolaries/Hab.var".
285
286 (* begin hide *)
287
288 inline "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__".
289
290 (* end hide *)
291
292 alias id "F" = "cic:/CoRN/ftc/Continuity/Corolaries/F.var".
293
294 alias id "G" = "cic:/CoRN/ftc/Continuity/Corolaries/G.var".
295
296 (* begin hide *)
297
298 inline "cic:/CoRN/ftc/Continuity/Corolaries/P.con" "Corolaries__".
299
300 inline "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__".
301
302 (* end hide *)
303
304 alias id "contF" = "cic:/CoRN/ftc/Continuity/Corolaries/contF.var".
305
306 alias id "contG" = "cic:/CoRN/ftc/Continuity/Corolaries/contG.var".
307
308 (*#*
309 The corresponding properties for subtraction, division and
310 multiplication by a scalar are easily proved as corollaries;
311 exponentiation is proved by induction, appealing to the results on
312 product and constant functions.
313 *)
314
315 inline "cic:/CoRN/ftc/Continuity/Continuous_I_minus.con".
316
317 inline "cic:/CoRN/ftc/Continuity/Continuous_I_scal.con".
318
319 inline "cic:/CoRN/ftc/Continuity/Continuous_I_nth.con".
320
321 inline "cic:/CoRN/ftc/Continuity/Continuous_I_min.con".
322
323 inline "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con".
324
325 alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var".
326
327 alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var".
328
329 inline "cic:/CoRN/ftc/Continuity/Continuous_I_div.con".
330
331 (* UNEXPORTED
332 End Corolaries
333 *)
334
335 (* UNEXPORTED
336 Section Other
337 *)
338
339 (* UNEXPORTED
340 Section Sums
341 *)
342
343 (*#*
344 We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function.
345 *)
346
347 alias id "a" = "cic:/CoRN/ftc/Continuity/Other/Sums/a.var".
348
349 alias id "b" = "cic:/CoRN/ftc/Continuity/Other/Sums/b.var".
350
351 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var".
352
353 alias id "Hab'" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var".
354
355 (* begin hide *)
356
357 inline "cic:/CoRN/ftc/Continuity/Other/Sums/I.con" "Other__Sums__".
358
359 (* end hide *)
360
361 inline "cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con".
362
363 inline "cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con".
364
365 inline "cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con".
366
367 (* UNEXPORTED
368 End Sums
369 *)
370
371 (*#*
372 For practical purposes, these characterization results are useful:
373 *)
374
375 inline "cic:/CoRN/ftc/Continuity/lub_charact.con".
376
377 inline "cic:/CoRN/ftc/Continuity/glb_charact.con".
378
379 (*#*
380 The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function.
381 *)
382
383 inline "cic:/CoRN/ftc/Continuity/leEq_glb.con".
384
385 (*#*
386 The norm is also an extensional property.
387 *)
388
389 inline "cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con".
390
391 (*#*
392 The value of the norm is covariant with the length of the interval.
393 *)
394
395 inline "cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con".
396
397 (* UNEXPORTED
398 End Other
399 *)
400
401 (* UNEXPORTED
402 Hint Resolve Continuous_I_const Continuous_I_id Continuous_I_plus
403   Continuous_I_inv Continuous_I_minus Continuous_I_mult Continuous_I_scal
404   Continuous_I_recip Continuous_I_max Continuous_I_min Continuous_I_div
405   Continuous_I_nth Continuous_I_abs: continuous.
406 *)
407