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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/Rolle".
19 include "CoRN_notation.ma".
21 (* $Id: Rolle.v,v 1.6 2004/04/23 10:01:01 lcf Exp $ *)
23 include "tactics/DiffTactics2.ma".
25 include "ftc/MoreFunctions.ma".
33 We now begin to work with partial functions. We begin by stating and proving Rolle's theorem in various forms and some of its corollaries.
35 %\begin{convention}% Assume that:
36 - [a,b:IR] with [a [<] b] and denote by [I] the interval [[a,b]];
37 - [F,F'] are partial functions such that [F'] is the derivative of [F] in [I];
38 - [e] is a positive real number.
45 inline "cic:/CoRN/ftc/Rolle/a.var".
47 inline "cic:/CoRN/ftc/Rolle/b.var".
49 inline "cic:/CoRN/ftc/Rolle/Hab'.var".
51 inline "cic:/CoRN/ftc/Rolle/Hab.con".
53 inline "cic:/CoRN/ftc/Rolle/I.con".
55 inline "cic:/CoRN/ftc/Rolle/F.var".
57 inline "cic:/CoRN/ftc/Rolle/F'.var".
59 inline "cic:/CoRN/ftc/Rolle/derF.var".
61 inline "cic:/CoRN/ftc/Rolle/Ha.var".
63 inline "cic:/CoRN/ftc/Rolle/Hb.var".
69 inline "cic:/CoRN/ftc/Rolle/Fab.var".
75 inline "cic:/CoRN/ftc/Rolle/e.var".
77 inline "cic:/CoRN/ftc/Rolle/He.var".
79 inline "cic:/CoRN/ftc/Rolle/contF'.con".
81 inline "cic:/CoRN/ftc/Rolle/derivF.con".
83 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma2.con".
85 inline "cic:/CoRN/ftc/Rolle/df.con".
87 inline "cic:/CoRN/ftc/Rolle/Hdf.con".
89 inline "cic:/CoRN/ftc/Rolle/Hf.con".
91 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma3.con".
93 inline "cic:/CoRN/ftc/Rolle/df'.con".
95 inline "cic:/CoRN/ftc/Rolle/Hdf'.con".
97 inline "cic:/CoRN/ftc/Rolle/Hf'.con".
99 inline "cic:/CoRN/ftc/Rolle/d.con".
101 inline "cic:/CoRN/ftc/Rolle/Hd.con".
103 inline "cic:/CoRN/ftc/Rolle/incF.con".
105 inline "cic:/CoRN/ftc/Rolle/n.con".
107 inline "cic:/CoRN/ftc/Rolle/fcp.con".
109 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma1.con".
111 inline "cic:/CoRN/ftc/Rolle/incF'.con".
113 inline "cic:/CoRN/ftc/Rolle/fcp'.con".
115 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma4.con".
117 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma5.con".
119 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma6.con".
121 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma7.con".
123 inline "cic:/CoRN/ftc/Rolle/j.con".
125 inline "cic:/CoRN/ftc/Rolle/Hj.con".
127 inline "cic:/CoRN/ftc/Rolle/Hj'.con".
129 inline "cic:/CoRN/ftc/Rolle/k.con".
131 inline "cic:/CoRN/ftc/Rolle/Hk.con".
133 inline "cic:/CoRN/ftc/Rolle/Hk'.con".
135 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma8.con".
137 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma9.con".
139 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma10.con".
141 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma11.con".
143 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma12.con".
145 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma13.con".
147 inline "cic:/CoRN/ftc/Rolle/Rolle_lemma15.con".
151 inline "cic:/CoRN/ftc/Rolle/Rolle.con".
158 Section Law_of_the_Mean.
162 The following is a simple corollary:
165 inline "cic:/CoRN/ftc/Rolle/a.var".
167 inline "cic:/CoRN/ftc/Rolle/b.var".
169 inline "cic:/CoRN/ftc/Rolle/Hab'.var".
173 inline "cic:/CoRN/ftc/Rolle/Hab.con".
175 inline "cic:/CoRN/ftc/Rolle/I.con".
179 inline "cic:/CoRN/ftc/Rolle/F.var".
181 inline "cic:/CoRN/ftc/Rolle/F'.var".
183 inline "cic:/CoRN/ftc/Rolle/HF.var".
187 inline "cic:/CoRN/ftc/Rolle/HA.var".
189 inline "cic:/CoRN/ftc/Rolle/HB.var".
193 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_I.con".
204 We can also state these theorems without expliciting the derivative of [F].
207 inline "cic:/CoRN/ftc/Rolle/a.var".
209 inline "cic:/CoRN/ftc/Rolle/b.var".
211 inline "cic:/CoRN/ftc/Rolle/Hab'.var".
215 inline "cic:/CoRN/ftc/Rolle/Hab.con".
219 inline "cic:/CoRN/ftc/Rolle/F.var".
223 inline "cic:/CoRN/ftc/Rolle/HF.var".
227 inline "cic:/CoRN/ftc/Rolle/Rolle'.con".
229 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean'_I.con".
236 Section Generalizations.
240 The mean law is more useful if we abstract [a] and [b] from the
241 context---allowing them in particular to be equal. In the case where
242 [F(a) [=] F(b)] we get Rolle's theorem again, so there is no need to
243 state it also in this form.
245 %\begin{convention}% Assume [I] is a proper interval, [F,F':PartIR].
249 inline "cic:/CoRN/ftc/Rolle/I.var".
251 inline "cic:/CoRN/ftc/Rolle/pI.var".
253 inline "cic:/CoRN/ftc/Rolle/F.var".
255 inline "cic:/CoRN/ftc/Rolle/F'.var".
259 inline "cic:/CoRN/ftc/Rolle/derF.var".
265 inline "cic:/CoRN/ftc/Rolle/incF.con".
267 inline "cic:/CoRN/ftc/Rolle/incF'.con".
271 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean.con".
274 We further generalize the mean law by writing as an explicit bound.
277 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_ineq.con".