helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.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 "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Ranalysis1.v,v 1.21.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
  34
  35 include "Reals/Rbase.ma".
  36
  37 include "Reals/Rfunctions.ma".
  38
  39 include "Reals/Rlimit.ma".
  40
  41 include "Reals/Rderiv.ma".
  42
  43 (* UNEXPORTED
  44 Open Local Scope R_scope.
  45 *)
  46
  47 (* UNEXPORTED
  48 Implicit Type f : R -> R.
  49 *)
  50
  51 (*#***************************************************)
  52
  53 (*#*           Basic operations on functions         *)
  54
  55 (*#***************************************************)
  56
  57 inline procedural "cic:/Coq/Reals/Ranalysis1/plus_fct.con" as definition.
  58
  59 inline procedural "cic:/Coq/Reals/Ranalysis1/opp_fct.con" as definition.
  60
  61 inline procedural "cic:/Coq/Reals/Ranalysis1/mult_fct.con" as definition.
  62
  63 inline procedural "cic:/Coq/Reals/Ranalysis1/mult_real_fct.con" as definition.
  64
  65 inline procedural "cic:/Coq/Reals/Ranalysis1/minus_fct.con" as definition.
  66
  67 inline procedural "cic:/Coq/Reals/Ranalysis1/div_fct.con" as definition.
  68
  69 inline procedural "cic:/Coq/Reals/Ranalysis1/div_real_fct.con" as definition.
  70
  71 inline procedural "cic:/Coq/Reals/Ranalysis1/comp.con" as definition.
  72
  73 inline procedural "cic:/Coq/Reals/Ranalysis1/inv_fct.con" as definition.
  74
  75 (* NOTATION
  76 Infix "+" := plus_fct : Rfun_scope.
  77 *)
  78
  79 (* NOTATION
  80 Notation "- x" := (opp_fct x) : Rfun_scope.
  81 *)
  82
  83 (* NOTATION
  84 Infix "*" := mult_fct : Rfun_scope.
  85 *)
  86
  87 (* NOTATION
  88 Infix "-" := minus_fct : Rfun_scope.
  89 *)
  90
  91 (* NOTATION
  92 Infix "/" := div_fct : Rfun_scope.
  93 *)
  94
  95 (* NOTATION
  96 Notation Local "f1 'o' f2" := (comp f1 f2)
  97   (at level 20, right associativity) : Rfun_scope.
  98 *)
  99
 100 (* NOTATION
 101 Notation "/ x" := (inv_fct x) : Rfun_scope.
 102 *)
 103
 104 (* UNEXPORTED
 105 Delimit Scope Rfun_scope with F.
 106 *)
 107
 108 inline procedural "cic:/Coq/Reals/Ranalysis1/fct_cte.con" as definition.
 109
 110 inline procedural "cic:/Coq/Reals/Ranalysis1/id.con" as definition.
 111
 112 (*#***************************************************)
 113
 114 (*#*            Variations of functions              *)
 115
 116 (*#***************************************************)
 117
 118 inline procedural "cic:/Coq/Reals/Ranalysis1/increasing.con" as definition.
 119
 120 inline procedural "cic:/Coq/Reals/Ranalysis1/decreasing.con" as definition.
 121
 122 inline procedural "cic:/Coq/Reals/Ranalysis1/strict_increasing.con" as definition.
 123
 124 inline procedural "cic:/Coq/Reals/Ranalysis1/strict_decreasing.con" as definition.
 125
 126 inline procedural "cic:/Coq/Reals/Ranalysis1/constant.con" as definition.
 127
 128 (*#*********)
 129
 130 inline procedural "cic:/Coq/Reals/Ranalysis1/no_cond.con" as definition.
 131
 132 (*#*********)
 133
 134 inline procedural "cic:/Coq/Reals/Ranalysis1/constant_D_eq.con" as definition.
 135
 136 (*#**************************************************)
 137
 138 (*#*      Definition of continuity as a limit       *)
 139
 140 (*#**************************************************)
 141
 142 (*#*********)
 143
 144 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt.con" as definition.
 145
 146 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity.con" as definition.
 147
 148 (* UNEXPORTED
 149 Arguments Scope continuity_pt [Rfun_scope R_scope].
 150 *)
 151
 152 (* UNEXPORTED
 153 Arguments Scope continuity [Rfun_scope].
 154 *)
 155
 156 (*#*********)
 157
 158 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_plus.con" as lemma.
 159
 160 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_opp.con" as lemma.
 161
 162 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_minus.con" as lemma.
 163
 164 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_mult.con" as lemma.
 165
 166 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_const.con" as lemma.
 167
 168 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_scal.con" as lemma.
 169
 170 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_inv.con" as lemma.
 171
 172 inline procedural "cic:/Coq/Reals/Ranalysis1/div_eq_inv.con" as lemma.
 173
 174 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_div.con" as lemma.
 175
 176 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_comp.con" as lemma.
 177
 178 (*#*********)
 179
 180 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_plus.con" as lemma.
 181
 182 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_opp.con" as lemma.
 183
 184 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_minus.con" as lemma.
 185
 186 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_mult.con" as lemma.
 187
 188 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_const.con" as lemma.
 189
 190 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_scal.con" as lemma.
 191
 192 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_inv.con" as lemma.
 193
 194 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_div.con" as lemma.
 195
 196 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_comp.con" as lemma.
 197
 198 (*#****************************************************)
 199
 200 (*#*  Derivative's definition using Landau's kernel   *)
 201
 202 (*#****************************************************)
 203
 204 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim.con" as definition.
 205
 206 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_abs.con" as definition.
 207
 208 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt.con" as definition.
 209
 210 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable.con" as definition.
 211
 212 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt.con" as definition.
 213
 214 inline procedural "cic:/Coq/Reals/Ranalysis1/derive.con" as definition.
 215
 216 (* UNEXPORTED
 217 Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
 218 *)
 219
 220 (* UNEXPORTED
 221 Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope].
 222 *)
 223
 224 (* UNEXPORTED
 225 Arguments Scope derivable_pt [Rfun_scope R_scope].
 226 *)
 227
 228 (* UNEXPORTED
 229 Arguments Scope derivable [Rfun_scope].
 230 *)
 231
 232 (* UNEXPORTED
 233 Arguments Scope derive_pt [Rfun_scope R_scope _].
 234 *)
 235
 236 (* UNEXPORTED
 237 Arguments Scope derive [Rfun_scope _].
 238 *)
 239
 240 inline procedural "cic:/Coq/Reals/Ranalysis1/antiderivative.con" as definition.
 241
 242 (*#***********************************)
 243
 244 (*#* Class of differential functions *)
 245
 246 (*#***********************************)
 247
 248 inline procedural "cic:/Coq/Reals/Ranalysis1/Differential.ind".
 249
 250 inline procedural "cic:/Coq/Reals/Ranalysis1/Differential_D2.ind".
 251
 252 (*#*********)
 253
 254 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step1.con" as lemma.
 255
 256 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step2.con" as lemma.
 257
 258 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step3.con" as lemma.
 259
 260 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_limite.con" as lemma.
 261
 262 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq.con" as lemma.
 263
 264 (*#*********)
 265
 266 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq_0.con" as lemma.
 267
 268 (*#*********)
 269
 270 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq_1.con" as lemma.
 271
 272 (*#*******************************************************************)
 273
 274 (*#* Equivalence of this definition with the one using limit concept *)
 275
 276 (*#*******************************************************************)
 277
 278 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_D_in.con" as lemma.
 279
 280 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_D_in.con" as lemma.
 281
 282 (*#**********************************)
 283
 284 (*#*   derivability -> continuity   *)
 285
 286 (*#**********************************)
 287
 288 (*#*********)
 289
 290 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_derive.con" as lemma.
 291
 292 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_continuous_pt.con" as theorem.
 293
 294 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_continuous.con" as theorem.
 295
 296 (*#***************************************************************)
 297
 298 (*#*                      Main rules                             *)
 299
 300 (*#***************************************************************)
 301
 302 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_plus.con" as lemma.
 303
 304 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_opp.con" as lemma.
 305
 306 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_minus.con" as lemma.
 307
 308 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_mult.con" as lemma.
 309
 310 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_const.con" as lemma.
 311
 312 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_scal.con" as lemma.
 313
 314 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_id.con" as lemma.
 315
 316 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_Rsqr.con" as lemma.
 317
 318 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_comp.con" as lemma.
 319
 320 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_plus.con" as lemma.
 321
 322 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_opp.con" as lemma.
 323
 324 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_minus.con" as lemma.
 325
 326 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_mult.con" as lemma.
 327
 328 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_const.con" as lemma.
 329
 330 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_scal.con" as lemma.
 331
 332 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_id.con" as lemma.
 333
 334 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_Rsqr.con" as lemma.
 335
 336 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_comp.con" as lemma.
 337
 338 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_plus.con" as lemma.
 339
 340 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_opp.con" as lemma.
 341
 342 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_minus.con" as lemma.
 343
 344 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_mult.con" as lemma.
 345
 346 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_const.con" as lemma.
 347
 348 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_scal.con" as lemma.
 349
 350 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_id.con" as lemma.
 351
 352 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_Rsqr.con" as lemma.
 353
 354 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_comp.con" as lemma.
 355
 356 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_plus.con" as lemma.
 357
 358 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_opp.con" as lemma.
 359
 360 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_minus.con" as lemma.
 361
 362 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_mult.con" as lemma.
 363
 364 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_const.con" as lemma.
 365
 366 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_scal.con" as lemma.
 367
 368 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_id.con" as lemma.
 369
 370 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_Rsqr.con" as lemma.
 371
 372 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_comp.con" as lemma.
 373
 374 (* Pow *)
 375
 376 inline procedural "cic:/Coq/Reals/Ranalysis1/pow_fct.con" as definition.
 377
 378 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_pow_pos.con" as lemma.
 379
 380 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_pow.con" as lemma.
 381
 382 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_pow.con" as lemma.
 383
 384 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pow.con" as lemma.
 385
 386 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_pow.con" as lemma.
 387
 388 inline procedural "cic:/Coq/Reals/Ranalysis1/pr_nu.con" as lemma.
 389
 390 (*#***********************************************************)
 391
 392 (*#*             Local extremum's condition                  *)
 393
 394 (*#***********************************************************)
 395
 396 inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_maximum.con" as theorem.
 397
 398 inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_minimum.con" as theorem.
 399
 400 inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_constant2.con" as theorem.
 401
 402 (*#*********)
 403
 404 inline procedural "cic:/Coq/Reals/Ranalysis1/nonneg_derivative_0.con" as lemma.
 405