helm/software/matita/contribs/procedural/CoRN/ftc/Continuity.mma

   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 include "CoRN.ma".
  18
  19 (* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 (*#* printing Norm_Funct %\ensuremath{\|\cdot\|}% *)
  22
  23 include "reals/NRootIR.ma".
  24
  25 include "ftc/FunctSums.ma".
  26
  27 (* UNEXPORTED
  28 Section Definitions_and_Basic_Results
  29 *)
  30
  31 (*#* *Continuity
  32
  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.%}.%
  43
  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].
  48 %\end{convention}%
  49
  50 ** Definitions and Basic Results
  51
  52 Here we define continuity and prove some basic properties of continuous functions.
  53 *)
  54
  55 (* UNEXPORTED
  56 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var
  57 *)
  58
  59 (* UNEXPORTED
  60 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var
  61 *)
  62
  63 (* UNEXPORTED
  64 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var
  65 *)
  66
  67 (* begin hide *)
  68
  69 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con" "Definitions_and_Basic_Results__" as definition.
  70
  71 (* end hide *)
  72
  73 (* UNEXPORTED
  74 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var
  75 *)
  76
  77 (* begin hide *)
  78
  79 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/P.con" "Definitions_and_Basic_Results__" as definition.
  80
  81 (* end hide *)
  82
  83 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I.con" as definition.
  84
  85 (*#*
  86 For convenience, we distinguish the two properties of continuous functions.
  87 *)
  88
  89 inline procedural "cic:/CoRN/ftc/Continuity/contin_imp_inc.con" as lemma.
  90
  91 inline procedural "cic:/CoRN/ftc/Continuity/contin_prop.con" as lemma.
  92
  93 (*#*
  94 Assume [F] to be continuous in [I].  Then it has a least upper bound and a greater lower bound on [I].
  95 *)
  96
  97 (* UNEXPORTED
  98 cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var
  99 *)
 100
 101 (* begin hide *)
 102
 103 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hinc'.con" "Definitions_and_Basic_Results__" as definition.
 104
 105 (* end hide *)
 106
 107 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con" as lemma.
 108
 109 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con" as lemma.
 110
 111 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con" as lemma.
 112
 113 (*#*
 114 We now make this glb and lub into operators.
 115 *)
 116
 117 inline procedural "cic:/CoRN/ftc/Continuity/lub_funct.con" as definition.
 118
 119 inline procedural "cic:/CoRN/ftc/Continuity/glb_funct.con" as definition.
 120
 121 (*#*
 122 These operators have the expected properties.
 123 *)
 124
 125 inline procedural "cic:/CoRN/ftc/Continuity/lub_is_lub.con" as lemma.
 126
 127 inline procedural "cic:/CoRN/ftc/Continuity/glb_is_glb.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/ftc/Continuity/glb_prop.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/ftc/Continuity/lub_prop.con" as lemma.
 132
 133 (*#*
 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).
 135 *)
 136
 137 inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct.con" as definition.
 138
 139 (*#*
 140 The norm effectively bounds the absolute value of a function.
 141 *)
 142
 143 inline procedural "cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con" as lemma.
 144
 145 (*#*
 146 The following is another way of characterizing the norm:
 147 *)
 148
 149 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con" as lemma.
 150
 151 (*#*
 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.
 153 *)
 154
 155 inline procedural "cic:/CoRN/ftc/Continuity/positive_norm.con" as lemma.
 156
 157 inline procedural "cic:/CoRN/ftc/Continuity/norm_fun_lub.con" as lemma.
 158
 159 inline procedural "cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con" as lemma.
 160
 161 inline procedural "cic:/CoRN/ftc/Continuity/less_Norm_Funct.con" as lemma.
 162
 163 (* UNEXPORTED
 164 End Definitions_and_Basic_Results
 165 *)
 166
 167 (* UNEXPORTED
 168 Implicit Arguments Continuous_I [a b].
 169 *)
 170
 171 (* UNEXPORTED
 172 Implicit Arguments Norm_Funct [a b Hab F].
 173 *)
 174
 175 (* UNEXPORTED
 176 Section Local_Results
 177 *)
 178
 179 (*#* **Algebraic Properties
 180
 181 We now state and prove some results about continuous functions.  Assume that [I] is included in the domain of both [F] and [G].
 182 *)
 183
 184 (* UNEXPORTED
 185 cic:/CoRN/ftc/Continuity/Local_Results/a.var
 186 *)
 187
 188 (* UNEXPORTED
 189 cic:/CoRN/ftc/Continuity/Local_Results/b.var
 190 *)
 191
 192 (* UNEXPORTED
 193 cic:/CoRN/ftc/Continuity/Local_Results/Hab.var
 194 *)
 195
 196 (* begin hide *)
 197
 198 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results__" as definition.
 199
 200 (* end hide *)
 201
 202 (* UNEXPORTED
 203 cic:/CoRN/ftc/Continuity/Local_Results/F.var
 204 *)
 205
 206 (* UNEXPORTED
 207 cic:/CoRN/ftc/Continuity/Local_Results/G.var
 208 *)
 209
 210 (* begin hide *)
 211
 212 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/P.con" "Local_Results__" as definition.
 213
 214 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results__" as definition.
 215
 216 (* end hide *)
 217
 218 (* UNEXPORTED
 219 cic:/CoRN/ftc/Continuity/Local_Results/incF.var
 220 *)
 221
 222 (* UNEXPORTED
 223 cic:/CoRN/ftc/Continuity/Local_Results/incG.var
 224 *)
 225
 226 (*#*
 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.
 228 *)
 229
 230 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change.con" as lemma.
 231
 232 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con" as lemma.
 233
 234 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con" as lemma.
 235
 236 (*#*
 237 Being continuous is an extensional property.
 238 *)
 239
 240 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_wd.con" as lemma.
 241
 242 (*#*
 243 A continuous function remains continuous if you restrict its domain.
 244 *)
 245
 246 inline procedural "cic:/CoRN/ftc/Continuity/included_imp_contin.con" as lemma.
 247
 248 (*#*
 249 Constant functions and identity are continuous.
 250 *)
 251
 252 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_const.con" as lemma.
 253
 254 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_id.con" as lemma.
 255
 256 (*#*
 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.
 258 *)
 259
 260 (* UNEXPORTED
 261 cic:/CoRN/ftc/Continuity/Local_Results/contF.var
 262 *)
 263
 264 (* UNEXPORTED
 265 cic:/CoRN/ftc/Continuity/Local_Results/contG.var
 266 *)
 267
 268 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con" as lemma.
 269
 270 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_inv.con" as lemma.
 271
 272 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_mult.con" as lemma.
 273
 274 (* UNEXPORTED
 275 Opaque AbsIR Max.
 276 *)
 277
 278 (* UNEXPORTED
 279 Transparent AbsIR Max.
 280 *)
 281
 282 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_max.con" as lemma.
 283
 284 (* begin show *)
 285
 286 (* UNEXPORTED
 287 cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var
 288 *)
 289
 290 (* UNEXPORTED
 291 cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var
 292 *)
 293
 294 (* end show *)
 295
 296 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_recip.con" as lemma.
 297
 298 (* UNEXPORTED
 299 End Local_Results
 300 *)
 301
 302 (* UNEXPORTED
 303 Hint Resolve contin_imp_inc: included.
 304 *)
 305
 306 (* UNEXPORTED
 307 Section Corolaries
 308 *)
 309
 310 (* UNEXPORTED
 311 cic:/CoRN/ftc/Continuity/Corolaries/a.var
 312 *)
 313
 314 (* UNEXPORTED
 315 cic:/CoRN/ftc/Continuity/Corolaries/b.var
 316 *)
 317
 318 (* UNEXPORTED
 319 cic:/CoRN/ftc/Continuity/Corolaries/Hab.var
 320 *)
 321
 322 (* begin hide *)
 323
 324 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__" as definition.
 325
 326 (* end hide *)
 327
 328 (* UNEXPORTED
 329 cic:/CoRN/ftc/Continuity/Corolaries/F.var
 330 *)
 331
 332 (* UNEXPORTED
 333 cic:/CoRN/ftc/Continuity/Corolaries/G.var
 334 *)
 335
 336 (* begin hide *)
 337
 338 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/P.con" "Corolaries__" as definition.
 339
 340 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__" as definition.
 341
 342 (* end hide *)
 343
 344 (* UNEXPORTED
 345 cic:/CoRN/ftc/Continuity/Corolaries/contF.var
 346 *)
 347
 348 (* UNEXPORTED
 349 cic:/CoRN/ftc/Continuity/Corolaries/contG.var
 350 *)
 351
 352 (*#*
 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.
 357 *)
 358
 359 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_minus.con" as lemma.
 360
 361 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_scal.con" as lemma.
 362
 363 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_nth.con" as lemma.
 364
 365 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_min.con" as lemma.
 366
 367 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con" as lemma.
 368
 369 (* UNEXPORTED
 370 cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var
 371 *)
 372
 373 (* UNEXPORTED
 374 cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var
 375 *)
 376
 377 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_div.con" as lemma.
 378
 379 (* UNEXPORTED
 380 End Corolaries
 381 *)
 382
 383 (* UNEXPORTED
 384 Section Other
 385 *)
 386
 387 (* UNEXPORTED
 388 Section Sums
 389 *)
 390
 391 (*#*
 392 We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function.
 393 *)
 394
 395 (* UNEXPORTED
 396 cic:/CoRN/ftc/Continuity/Other/Sums/a.var
 397 *)
 398
 399 (* UNEXPORTED
 400 cic:/CoRN/ftc/Continuity/Other/Sums/b.var
 401 *)
 402
 403 (* UNEXPORTED
 404 cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var
 405 *)
 406
 407 (* UNEXPORTED
 408 cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var
 409 *)
 410
 411 (* begin hide *)
 412
 413 inline procedural "cic:/CoRN/ftc/Continuity/Other/Sums/I.con" "Other__Sums__" as definition.
 414
 415 (* end hide *)
 416
 417 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con" as lemma.
 418
 419 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con" as lemma.
 420
 421 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con" as lemma.
 422
 423 (* UNEXPORTED
 424 End Sums
 425 *)
 426
 427 (*#*
 428 For practical purposes, these characterization results are useful:
 429 *)
 430
 431 inline procedural "cic:/CoRN/ftc/Continuity/lub_charact.con" as lemma.
 432
 433 inline procedural "cic:/CoRN/ftc/Continuity/glb_charact.con" as lemma.
 434
 435 (*#*
 436 The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function.
 437 *)
 438
 439 inline procedural "cic:/CoRN/ftc/Continuity/leEq_glb.con" as lemma.
 440
 441 (*#*
 442 The norm is also an extensional property.
 443 *)
 444
 445 inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con" as lemma.
 446
 447 (*#*
 448 The value of the norm is covariant with the length of the interval.
 449 *)
 450
 451 inline procedural "cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con" as lemma.
 452
 453 (* UNEXPORTED
 454 End Other
 455 *)
 456
 457 (* UNEXPORTED
 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.
 462 *)
 463