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: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
21 (*#* printing Norm_Funct %\ensuremath{\|\cdot\|}% *)
23 include "reals/NRootIR.ma".
25 include "ftc/FunctSums.ma".
28 Section Definitions_and_Basic_Results
33 Constructively, continuity is the most fundamental property of any
34 function---so strongly that no example is known of a constructive
35 function that is not continuous. However, the classical definition of
36 continuity is not good for our purposes, as it is not true, for
37 example, that a function which is continuous in a compact interval is
38 uniformly continuous in that same interval (for a discussion of this
39 see Bishop 1967). Thus, our notion of continuity will be the uniform
40 one#. #%\footnote{%Similar remarks apply to convergence of sequences
41 of functions, which we will define ahead, and elsewhere; we will
42 refrain from discussing this issue at those places.%}.%
44 %\begin{convention}% Throughout this section, [a] and [b] will be real
45 numbers, [I] will denote the compact interval [[a,b]] and
46 [F, G, H] will denote arbitrary partial functions with domains
47 respectively [P, Q] and [R].
50 ** Definitions and Basic Results
52 Here we define continuity and prove some basic properties of continuous functions.
56 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var
60 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var
64 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var
69 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con" "Definitions_and_Basic_Results__" as definition.
74 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var
79 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/P.con" "Definitions_and_Basic_Results__" as definition.
83 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I.con" as definition.
86 For convenience, we distinguish the two properties of continuous functions.
89 inline procedural "cic:/CoRN/ftc/Continuity/contin_imp_inc.con" as lemma.
91 inline procedural "cic:/CoRN/ftc/Continuity/contin_prop.con" as lemma.
94 Assume [F] to be continuous in [I]. Then it has a least upper bound and a greater lower bound on [I].
98 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var
103 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hinc'.con" "Definitions_and_Basic_Results__" as definition.
107 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con" as lemma.
109 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con" as lemma.
111 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con" as lemma.
114 We now make this glb and lub into operators.
117 inline procedural "cic:/CoRN/ftc/Continuity/lub_funct.con" as definition.
119 inline procedural "cic:/CoRN/ftc/Continuity/glb_funct.con" as definition.
122 These operators have the expected properties.
125 inline procedural "cic:/CoRN/ftc/Continuity/lub_is_lub.con" as lemma.
127 inline procedural "cic:/CoRN/ftc/Continuity/glb_is_glb.con" as lemma.
129 inline procedural "cic:/CoRN/ftc/Continuity/glb_prop.con" as lemma.
131 inline procedural "cic:/CoRN/ftc/Continuity/lub_prop.con" as lemma.
134 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).
137 inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct.con" as definition.
140 The norm effectively bounds the absolute value of a function.
143 inline procedural "cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con" as lemma.
146 The following is another way of characterizing the norm:
149 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con" as lemma.
152 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.
155 inline procedural "cic:/CoRN/ftc/Continuity/positive_norm.con" as lemma.
157 inline procedural "cic:/CoRN/ftc/Continuity/norm_fun_lub.con" as lemma.
159 inline procedural "cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con" as lemma.
161 inline procedural "cic:/CoRN/ftc/Continuity/less_Norm_Funct.con" as lemma.
164 End Definitions_and_Basic_Results
168 Implicit Arguments Continuous_I [a b].
172 Implicit Arguments Norm_Funct [a b Hab F].
176 Section Local_Results
179 (*#* **Algebraic Properties
181 We now state and prove some results about continuous functions. Assume that [I] is included in the domain of both [F] and [G].
185 cic:/CoRN/ftc/Continuity/Local_Results/a.var
189 cic:/CoRN/ftc/Continuity/Local_Results/b.var
193 cic:/CoRN/ftc/Continuity/Local_Results/Hab.var
198 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results__" as definition.
203 cic:/CoRN/ftc/Continuity/Local_Results/F.var
207 cic:/CoRN/ftc/Continuity/Local_Results/G.var
212 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/P.con" "Local_Results__" as definition.
214 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results__" as definition.
219 cic:/CoRN/ftc/Continuity/Local_Results/incF.var
223 cic:/CoRN/ftc/Continuity/Local_Results/incG.var
227 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.
230 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change.con" as lemma.
232 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con" as lemma.
234 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con" as lemma.
237 Being continuous is an extensional property.
240 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_wd.con" as lemma.
243 A continuous function remains continuous if you restrict its domain.
246 inline procedural "cic:/CoRN/ftc/Continuity/included_imp_contin.con" as lemma.
249 Constant functions and identity are continuous.
252 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_const.con" as lemma.
254 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_id.con" as lemma.
257 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.
261 cic:/CoRN/ftc/Continuity/Local_Results/contF.var
265 cic:/CoRN/ftc/Continuity/Local_Results/contG.var
268 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con" as lemma.
270 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_inv.con" as lemma.
272 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_mult.con" as lemma.
279 Transparent AbsIR Max.
282 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_max.con" as lemma.
287 cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var
291 cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var
296 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_recip.con" as lemma.
303 Hint Resolve contin_imp_inc: included.
311 cic:/CoRN/ftc/Continuity/Corolaries/a.var
315 cic:/CoRN/ftc/Continuity/Corolaries/b.var
319 cic:/CoRN/ftc/Continuity/Corolaries/Hab.var
324 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__" as definition.
329 cic:/CoRN/ftc/Continuity/Corolaries/F.var
333 cic:/CoRN/ftc/Continuity/Corolaries/G.var
338 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/P.con" "Corolaries__" as definition.
340 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__" as definition.
345 cic:/CoRN/ftc/Continuity/Corolaries/contF.var
349 cic:/CoRN/ftc/Continuity/Corolaries/contG.var
353 The corresponding properties for subtraction, division and
354 multiplication by a scalar are easily proved as corollaries;
355 exponentiation is proved by induction, appealing to the results on
356 product and constant functions.
359 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_minus.con" as lemma.
361 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_scal.con" as lemma.
363 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_nth.con" as lemma.
365 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_min.con" as lemma.
367 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con" as lemma.
370 cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var
374 cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var
377 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_div.con" as lemma.
392 We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function.
396 cic:/CoRN/ftc/Continuity/Other/Sums/a.var
400 cic:/CoRN/ftc/Continuity/Other/Sums/b.var
404 cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var
408 cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var
413 inline procedural "cic:/CoRN/ftc/Continuity/Other/Sums/I.con" "Other__Sums__" as definition.
417 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con" as lemma.
419 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con" as lemma.
421 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con" as lemma.
428 For practical purposes, these characterization results are useful:
431 inline procedural "cic:/CoRN/ftc/Continuity/lub_charact.con" as lemma.
433 inline procedural "cic:/CoRN/ftc/Continuity/glb_charact.con" as lemma.
436 The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function.
439 inline procedural "cic:/CoRN/ftc/Continuity/leEq_glb.con" as lemma.
442 The norm is also an extensional property.
445 inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con" as lemma.
448 The value of the norm is covariant with the length of the interval.
451 inline procedural "cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con" as lemma.
458 Hint Resolve Continuous_I_const Continuous_I_id Continuous_I_plus
459 Continuous_I_inv Continuous_I_minus Continuous_I_mult Continuous_I_scal
460 Continuous_I_recip Continuous_I_max Continuous_I_min Continuous_I_div
461 Continuous_I_nth Continuous_I_abs: continuous.