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