1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Ranalysis1.v,v 1.21.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
35 include "Reals/Rbase.ma".
37 include "Reals/Rfunctions.ma".
39 include "Reals/Rlimit.ma".
41 include "Reals/Rderiv.ma".
44 Open Local Scope R_scope.
48 Implicit Type f : R -> R.
51 (*#***************************************************)
53 (*#* Basic operations on functions *)
55 (*#***************************************************)
57 inline procedural "cic:/Coq/Reals/Ranalysis1/plus_fct.con" as definition.
59 inline procedural "cic:/Coq/Reals/Ranalysis1/opp_fct.con" as definition.
61 inline procedural "cic:/Coq/Reals/Ranalysis1/mult_fct.con" as definition.
63 inline procedural "cic:/Coq/Reals/Ranalysis1/mult_real_fct.con" as definition.
65 inline procedural "cic:/Coq/Reals/Ranalysis1/minus_fct.con" as definition.
67 inline procedural "cic:/Coq/Reals/Ranalysis1/div_fct.con" as definition.
69 inline procedural "cic:/Coq/Reals/Ranalysis1/div_real_fct.con" as definition.
71 inline procedural "cic:/Coq/Reals/Ranalysis1/comp.con" as definition.
73 inline procedural "cic:/Coq/Reals/Ranalysis1/inv_fct.con" as definition.
76 Infix "+" := plus_fct : Rfun_scope.
80 Notation "- x" := (opp_fct x) : Rfun_scope.
84 Infix "*" := mult_fct : Rfun_scope.
88 Infix "-" := minus_fct : Rfun_scope.
92 Infix "/" := div_fct : Rfun_scope.
96 Notation Local "f1 'o' f2" := (comp f1 f2)
97 (at level 20, right associativity) : Rfun_scope.
101 Notation "/ x" := (inv_fct x) : Rfun_scope.
105 Delimit Scope Rfun_scope with F.
108 inline procedural "cic:/Coq/Reals/Ranalysis1/fct_cte.con" as definition.
110 inline procedural "cic:/Coq/Reals/Ranalysis1/id.con" as definition.
112 (*#***************************************************)
114 (*#* Variations of functions *)
116 (*#***************************************************)
118 inline procedural "cic:/Coq/Reals/Ranalysis1/increasing.con" as definition.
120 inline procedural "cic:/Coq/Reals/Ranalysis1/decreasing.con" as definition.
122 inline procedural "cic:/Coq/Reals/Ranalysis1/strict_increasing.con" as definition.
124 inline procedural "cic:/Coq/Reals/Ranalysis1/strict_decreasing.con" as definition.
126 inline procedural "cic:/Coq/Reals/Ranalysis1/constant.con" as definition.
130 inline procedural "cic:/Coq/Reals/Ranalysis1/no_cond.con" as definition.
134 inline procedural "cic:/Coq/Reals/Ranalysis1/constant_D_eq.con" as definition.
136 (*#**************************************************)
138 (*#* Definition of continuity as a limit *)
140 (*#**************************************************)
144 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt.con" as definition.
146 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity.con" as definition.
149 Arguments Scope continuity_pt [Rfun_scope R_scope].
153 Arguments Scope continuity [Rfun_scope].
158 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_plus.con" as lemma.
160 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_opp.con" as lemma.
162 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_minus.con" as lemma.
164 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_mult.con" as lemma.
166 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_const.con" as lemma.
168 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_scal.con" as lemma.
170 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_inv.con" as lemma.
172 inline procedural "cic:/Coq/Reals/Ranalysis1/div_eq_inv.con" as lemma.
174 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_div.con" as lemma.
176 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_comp.con" as lemma.
180 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_plus.con" as lemma.
182 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_opp.con" as lemma.
184 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_minus.con" as lemma.
186 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_mult.con" as lemma.
188 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_const.con" as lemma.
190 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_scal.con" as lemma.
192 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_inv.con" as lemma.
194 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_div.con" as lemma.
196 inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_comp.con" as lemma.
198 (*#****************************************************)
200 (*#* Derivative's definition using Landau's kernel *)
202 (*#****************************************************)
204 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim.con" as definition.
206 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_abs.con" as definition.
208 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt.con" as definition.
210 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable.con" as definition.
212 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt.con" as definition.
214 inline procedural "cic:/Coq/Reals/Ranalysis1/derive.con" as definition.
217 Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
221 Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope].
225 Arguments Scope derivable_pt [Rfun_scope R_scope].
229 Arguments Scope derivable [Rfun_scope].
233 Arguments Scope derive_pt [Rfun_scope R_scope _].
237 Arguments Scope derive [Rfun_scope _].
240 inline procedural "cic:/Coq/Reals/Ranalysis1/antiderivative.con" as definition.
242 (*#***********************************)
244 (*#* Class of differential functions *)
246 (*#***********************************)
248 inline procedural "cic:/Coq/Reals/Ranalysis1/Differential.ind".
250 inline procedural "cic:/Coq/Reals/Ranalysis1/Differential_D2.ind".
254 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step1.con" as lemma.
256 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step2.con" as lemma.
258 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step3.con" as lemma.
260 inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_limite.con" as lemma.
262 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq.con" as lemma.
266 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq_0.con" as lemma.
270 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq_1.con" as lemma.
272 (*#*******************************************************************)
274 (*#* Equivalence of this definition with the one using limit concept *)
276 (*#*******************************************************************)
278 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_D_in.con" as lemma.
280 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_D_in.con" as lemma.
282 (*#**********************************)
284 (*#* derivability -> continuity *)
286 (*#**********************************)
290 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_derive.con" as lemma.
292 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_continuous_pt.con" as theorem.
294 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_continuous.con" as theorem.
296 (*#***************************************************************)
300 (*#***************************************************************)
302 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_plus.con" as lemma.
304 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_opp.con" as lemma.
306 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_minus.con" as lemma.
308 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_mult.con" as lemma.
310 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_const.con" as lemma.
312 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_scal.con" as lemma.
314 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_id.con" as lemma.
316 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_Rsqr.con" as lemma.
318 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_comp.con" as lemma.
320 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_plus.con" as lemma.
322 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_opp.con" as lemma.
324 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_minus.con" as lemma.
326 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_mult.con" as lemma.
328 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_const.con" as lemma.
330 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_scal.con" as lemma.
332 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_id.con" as lemma.
334 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_Rsqr.con" as lemma.
336 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_comp.con" as lemma.
338 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_plus.con" as lemma.
340 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_opp.con" as lemma.
342 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_minus.con" as lemma.
344 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_mult.con" as lemma.
346 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_const.con" as lemma.
348 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_scal.con" as lemma.
350 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_id.con" as lemma.
352 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_Rsqr.con" as lemma.
354 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_comp.con" as lemma.
356 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_plus.con" as lemma.
358 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_opp.con" as lemma.
360 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_minus.con" as lemma.
362 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_mult.con" as lemma.
364 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_const.con" as lemma.
366 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_scal.con" as lemma.
368 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_id.con" as lemma.
370 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_Rsqr.con" as lemma.
372 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_comp.con" as lemma.
376 inline procedural "cic:/Coq/Reals/Ranalysis1/pow_fct.con" as definition.
378 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_pow_pos.con" as lemma.
380 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_pow.con" as lemma.
382 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_pow.con" as lemma.
384 inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pow.con" as lemma.
386 inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_pow.con" as lemma.
388 inline procedural "cic:/Coq/Reals/Ranalysis1/pr_nu.con" as lemma.
390 (*#***********************************************************)
392 (*#* Local extremum's condition *)
394 (*#***********************************************************)
396 inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_maximum.con" as theorem.
398 inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_minimum.con" as theorem.
400 inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_constant2.con" as theorem.
404 inline procedural "cic:/Coq/Reals/Ranalysis1/nonneg_derivative_0.con" as lemma.