helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var".
  56
  57 alias id "b" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var".
  58
  59 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var".
  60
  61 (* begin hide *)
  62
  63 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con" "Definitions_and_Basic_Results__".
  64
  65 (* end hide *)
  66
  67 alias id "F" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var".
  68
  69 (* begin hide *)
  70
  71 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/P.con" "Definitions_and_Basic_Results__".
  72
  73 (* end hide *)
  74
  75 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I.con".
  76
  77 (*#*
  78 For convenience, we distinguish the two properties of continuous functions.
  79 *)
  80
  81 inline procedural "cic:/CoRN/ftc/Continuity/contin_imp_inc.con".
  82
  83 inline procedural "cic:/CoRN/ftc/Continuity/contin_prop.con".
  84
  85 (*#*
  86 Assume [F] to be continuous in [I].  Then it has a least upper bound and a greater lower bound on [I].
  87 *)
  88
  89 alias id "contF" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var".
  90
  91 (* begin hide *)
  92
  93 inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hinc'.con" "Definitions_and_Basic_Results__".
  94
  95 (* end hide *)
  96
  97 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con".
  98
  99 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con".
 100
 101 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con".
 102
 103 (*#*
 104 We now make this glb and lub into operators.
 105 *)
 106
 107 inline procedural "cic:/CoRN/ftc/Continuity/lub_funct.con".
 108
 109 inline procedural "cic:/CoRN/ftc/Continuity/glb_funct.con".
 110
 111 (*#*
 112 These operators have the expected properties.
 113 *)
 114
 115 inline procedural "cic:/CoRN/ftc/Continuity/lub_is_lub.con".
 116
 117 inline procedural "cic:/CoRN/ftc/Continuity/glb_is_glb.con".
 118
 119 inline procedural "cic:/CoRN/ftc/Continuity/glb_prop.con".
 120
 121 inline procedural "cic:/CoRN/ftc/Continuity/lub_prop.con".
 122
 123 (*#*
 124 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).
 125 *)
 126
 127 inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct.con".
 128
 129 (*#*
 130 The norm effectively bounds the absolute value of a function.
 131 *)
 132
 133 inline procedural "cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con".
 134
 135 (*#*
 136 The following is another way of characterizing the norm:
 137 *)
 138
 139 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con".
 140
 141 (*#*
 142 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.
 143 *)
 144
 145 inline procedural "cic:/CoRN/ftc/Continuity/positive_norm.con".
 146
 147 inline procedural "cic:/CoRN/ftc/Continuity/norm_fun_lub.con".
 148
 149 inline procedural "cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con".
 150
 151 inline procedural "cic:/CoRN/ftc/Continuity/less_Norm_Funct.con".
 152
 153 (* UNEXPORTED
 154 End Definitions_and_Basic_Results
 155 *)
 156
 157 (* UNEXPORTED
 158 Implicit Arguments Continuous_I [a b].
 159 *)
 160
 161 (* UNEXPORTED
 162 Implicit Arguments Norm_Funct [a b Hab F].
 163 *)
 164
 165 (* UNEXPORTED
 166 Section Local_Results
 167 *)
 168
 169 (*#* **Algebraic Properties
 170
 171 We now state and prove some results about continuous functions.  Assume that [I] is included in the domain of both [F] and [G].
 172 *)
 173
 174 alias id "a" = "cic:/CoRN/ftc/Continuity/Local_Results/a.var".
 175
 176 alias id "b" = "cic:/CoRN/ftc/Continuity/Local_Results/b.var".
 177
 178 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Local_Results/Hab.var".
 179
 180 (* begin hide *)
 181
 182 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results__".
 183
 184 (* end hide *)
 185
 186 alias id "F" = "cic:/CoRN/ftc/Continuity/Local_Results/F.var".
 187
 188 alias id "G" = "cic:/CoRN/ftc/Continuity/Local_Results/G.var".
 189
 190 (* begin hide *)
 191
 192 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/P.con" "Local_Results__".
 193
 194 inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results__".
 195
 196 (* end hide *)
 197
 198 alias id "incF" = "cic:/CoRN/ftc/Continuity/Local_Results/incF.var".
 199
 200 alias id "incG" = "cic:/CoRN/ftc/Continuity/Local_Results/incG.var".
 201
 202 (*#*
 203 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.
 204 *)
 205
 206 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change.con".
 207
 208 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con".
 209
 210 inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con".
 211
 212 (*#*
 213 Being continuous is an extensional property.
 214 *)
 215
 216 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_wd.con".
 217
 218 (*#*
 219 A continuous function remains continuous if you restrict its domain.
 220 *)
 221
 222 inline procedural "cic:/CoRN/ftc/Continuity/included_imp_contin.con".
 223
 224 (*#*
 225 Constant functions and identity are continuous.
 226 *)
 227
 228 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_const.con".
 229
 230 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_id.con".
 231
 232 (*#*
 233 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.
 234 *)
 235
 236 alias id "contF" = "cic:/CoRN/ftc/Continuity/Local_Results/contF.var".
 237
 238 alias id "contG" = "cic:/CoRN/ftc/Continuity/Local_Results/contG.var".
 239
 240 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con".
 241
 242 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_inv.con".
 243
 244 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_mult.con".
 245
 246 (* UNEXPORTED
 247 Opaque AbsIR Max.
 248 *)
 249
 250 (* UNEXPORTED
 251 Transparent AbsIR Max.
 252 *)
 253
 254 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_max.con".
 255
 256 (* begin show *)
 257
 258 alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var".
 259
 260 alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var".
 261
 262 (* end show *)
 263
 264 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_recip.con".
 265
 266 (* UNEXPORTED
 267 End Local_Results
 268 *)
 269
 270 (* UNEXPORTED
 271 Hint Resolve contin_imp_inc: included.
 272 *)
 273
 274 (* UNEXPORTED
 275 Section Corolaries
 276 *)
 277
 278 alias id "a" = "cic:/CoRN/ftc/Continuity/Corolaries/a.var".
 279
 280 alias id "b" = "cic:/CoRN/ftc/Continuity/Corolaries/b.var".
 281
 282 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Corolaries/Hab.var".
 283
 284 (* begin hide *)
 285
 286 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__".
 287
 288 (* end hide *)
 289
 290 alias id "F" = "cic:/CoRN/ftc/Continuity/Corolaries/F.var".
 291
 292 alias id "G" = "cic:/CoRN/ftc/Continuity/Corolaries/G.var".
 293
 294 (* begin hide *)
 295
 296 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/P.con" "Corolaries__".
 297
 298 inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__".
 299
 300 (* end hide *)
 301
 302 alias id "contF" = "cic:/CoRN/ftc/Continuity/Corolaries/contF.var".
 303
 304 alias id "contG" = "cic:/CoRN/ftc/Continuity/Corolaries/contG.var".
 305
 306 (*#*
 307 The corresponding properties for subtraction, division and
 308 multiplication by a scalar are easily proved as corollaries;
 309 exponentiation is proved by induction, appealing to the results on
 310 product and constant functions.
 311 *)
 312
 313 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_minus.con".
 314
 315 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_scal.con".
 316
 317 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_nth.con".
 318
 319 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_min.con".
 320
 321 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con".
 322
 323 alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var".
 324
 325 alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var".
 326
 327 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_div.con".
 328
 329 (* UNEXPORTED
 330 End Corolaries
 331 *)
 332
 333 (* UNEXPORTED
 334 Section Other
 335 *)
 336
 337 (* UNEXPORTED
 338 Section Sums
 339 *)
 340
 341 (*#*
 342 We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function.
 343 *)
 344
 345 alias id "a" = "cic:/CoRN/ftc/Continuity/Other/Sums/a.var".
 346
 347 alias id "b" = "cic:/CoRN/ftc/Continuity/Other/Sums/b.var".
 348
 349 alias id "Hab" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var".
 350
 351 alias id "Hab'" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var".
 352
 353 (* begin hide *)
 354
 355 inline procedural "cic:/CoRN/ftc/Continuity/Other/Sums/I.con" "Other__Sums__".
 356
 357 (* end hide *)
 358
 359 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con".
 360
 361 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con".
 362
 363 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con".
 364
 365 (* UNEXPORTED
 366 End Sums
 367 *)
 368
 369 (*#*
 370 For practical purposes, these characterization results are useful:
 371 *)
 372
 373 inline procedural "cic:/CoRN/ftc/Continuity/lub_charact.con".
 374
 375 inline procedural "cic:/CoRN/ftc/Continuity/glb_charact.con".
 376
 377 (*#*
 378 The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function.
 379 *)
 380
 381 inline procedural "cic:/CoRN/ftc/Continuity/leEq_glb.con".
 382
 383 (*#*
 384 The norm is also an extensional property.
 385 *)
 386
 387 inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con".
 388
 389 (*#*
 390 The value of the norm is covariant with the length of the interval.
 391 *)
 392
 393 inline procedural "cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con".
 394
 395 (* UNEXPORTED
 396 End Other
 397 *)
 398
 399 (* UNEXPORTED
 400 Hint Resolve Continuous_I_const Continuous_I_id Continuous_I_plus
 401   Continuous_I_inv Continuous_I_minus Continuous_I_mult Continuous_I_scal
 402   Continuous_I_recip Continuous_I_max Continuous_I_min Continuous_I_div
 403   Continuous_I_nth Continuous_I_abs: continuous.
 404 *)
 405