matita/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