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".
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/Rolle/a.var" "Rolle__".
47 inline "cic:/CoRN/ftc/Rolle/Rolle/b.var" "Rolle__".
49 inline "cic:/CoRN/ftc/Rolle/Rolle/Hab'.var" "Rolle__".
51 inline "cic:/CoRN/ftc/Rolle/Rolle/Hab.con" "Rolle__".
53 inline "cic:/CoRN/ftc/Rolle/Rolle/I.con" "Rolle__".
55 inline "cic:/CoRN/ftc/Rolle/Rolle/F.var" "Rolle__".
57 inline "cic:/CoRN/ftc/Rolle/Rolle/F'.var" "Rolle__".
59 inline "cic:/CoRN/ftc/Rolle/Rolle/derF.var" "Rolle__".
61 inline "cic:/CoRN/ftc/Rolle/Rolle/Ha.var" "Rolle__".
63 inline "cic:/CoRN/ftc/Rolle/Rolle/Hb.var" "Rolle__".
69 inline "cic:/CoRN/ftc/Rolle/Rolle/Fab.var" "Rolle__".
75 inline "cic:/CoRN/ftc/Rolle/Rolle/e.var" "Rolle__".
77 inline "cic:/CoRN/ftc/Rolle/Rolle/He.var" "Rolle__".
79 inline "cic:/CoRN/ftc/Rolle/Rolle/contF'.con" "Rolle__".
81 inline "cic:/CoRN/ftc/Rolle/Rolle/derivF.con" "Rolle__".
83 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma2.con" "Rolle__".
85 inline "cic:/CoRN/ftc/Rolle/Rolle/df.con" "Rolle__".
87 inline "cic:/CoRN/ftc/Rolle/Rolle/Hdf.con" "Rolle__".
89 inline "cic:/CoRN/ftc/Rolle/Rolle/Hf.con" "Rolle__".
91 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma3.con" "Rolle__".
93 inline "cic:/CoRN/ftc/Rolle/Rolle/df'.con" "Rolle__".
95 inline "cic:/CoRN/ftc/Rolle/Rolle/Hdf'.con" "Rolle__".
97 inline "cic:/CoRN/ftc/Rolle/Rolle/Hf'.con" "Rolle__".
99 inline "cic:/CoRN/ftc/Rolle/Rolle/d.con" "Rolle__".
101 inline "cic:/CoRN/ftc/Rolle/Rolle/Hd.con" "Rolle__".
103 inline "cic:/CoRN/ftc/Rolle/Rolle/incF.con" "Rolle__".
105 inline "cic:/CoRN/ftc/Rolle/Rolle/n.con" "Rolle__".
107 inline "cic:/CoRN/ftc/Rolle/Rolle/fcp.con" "Rolle__".
109 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma1.con" "Rolle__".
111 inline "cic:/CoRN/ftc/Rolle/Rolle/incF'.con" "Rolle__".
113 inline "cic:/CoRN/ftc/Rolle/Rolle/fcp'.con" "Rolle__".
116 Notation cp := (compact_part a b Hab' d Hd).
119 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma4.con" "Rolle__".
121 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma5.con" "Rolle__".
123 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma6.con" "Rolle__".
125 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma7.con" "Rolle__".
127 inline "cic:/CoRN/ftc/Rolle/Rolle/j.con" "Rolle__".
129 inline "cic:/CoRN/ftc/Rolle/Rolle/Hj.con" "Rolle__".
131 inline "cic:/CoRN/ftc/Rolle/Rolle/Hj'.con" "Rolle__".
133 inline "cic:/CoRN/ftc/Rolle/Rolle/k.con" "Rolle__".
135 inline "cic:/CoRN/ftc/Rolle/Rolle/Hk.con" "Rolle__".
137 inline "cic:/CoRN/ftc/Rolle/Rolle/Hk'.con" "Rolle__".
139 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma8.con" "Rolle__".
141 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma9.con" "Rolle__".
143 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma10.con" "Rolle__".
145 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma11.con" "Rolle__".
147 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma12.con" "Rolle__".
149 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma13.con" "Rolle__".
151 inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma15.con" "Rolle__".
155 inline "cic:/CoRN/ftc/Rolle/Rolle.con".
162 Section Law_of_the_Mean
166 The following is a simple corollary:
169 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/a.var" "Law_of_the_Mean__".
171 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/b.var" "Law_of_the_Mean__".
173 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/Hab'.var" "Law_of_the_Mean__".
177 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/Hab.con" "Law_of_the_Mean__".
179 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/I.con" "Law_of_the_Mean__".
183 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/F.var" "Law_of_the_Mean__".
185 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/F'.var" "Law_of_the_Mean__".
187 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/HF.var" "Law_of_the_Mean__".
191 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/HA.var" "Law_of_the_Mean__".
193 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/HB.var" "Law_of_the_Mean__".
197 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_I.con".
208 We can also state these theorems without expliciting the derivative of [F].
211 inline "cic:/CoRN/ftc/Rolle/Corollaries/a.var" "Corollaries__".
213 inline "cic:/CoRN/ftc/Rolle/Corollaries/b.var" "Corollaries__".
215 inline "cic:/CoRN/ftc/Rolle/Corollaries/Hab'.var" "Corollaries__".
219 inline "cic:/CoRN/ftc/Rolle/Corollaries/Hab.con" "Corollaries__".
223 inline "cic:/CoRN/ftc/Rolle/Corollaries/F.var" "Corollaries__".
227 inline "cic:/CoRN/ftc/Rolle/Corollaries/HF.var" "Corollaries__".
231 inline "cic:/CoRN/ftc/Rolle/Rolle'.con".
233 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean'_I.con".
240 Section Generalizations
244 The mean law is more useful if we abstract [a] and [b] from the
245 context---allowing them in particular to be equal. In the case where
246 [F(a) [=] F(b)] we get Rolle's theorem again, so there is no need to
247 state it also in this form.
249 %\begin{convention}% Assume [I] is a proper interval, [F,F':PartIR].
253 inline "cic:/CoRN/ftc/Rolle/Generalizations/I.var" "Generalizations__".
255 inline "cic:/CoRN/ftc/Rolle/Generalizations/pI.var" "Generalizations__".
257 inline "cic:/CoRN/ftc/Rolle/Generalizations/F.var" "Generalizations__".
259 inline "cic:/CoRN/ftc/Rolle/Generalizations/F'.var" "Generalizations__".
263 inline "cic:/CoRN/ftc/Rolle/Generalizations/derF.var" "Generalizations__".
269 inline "cic:/CoRN/ftc/Rolle/Generalizations/incF.con" "Generalizations__".
271 inline "cic:/CoRN/ftc/Rolle/Generalizations/incF'.con" "Generalizations__".
275 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean.con".
278 We further generalize the mean law by writing as an explicit bound.
281 inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_ineq.con".