Rolle's Theorem
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.
Assume that:
- a,b:IR with a < b and denote by I the interval [a,b];
- F,F' are partial functions such that F' is the derivative of F in I;
- e is a positive real number.
Hypothesis Fab : F a Ha [=] F b Hb.
Theorem Rolle : {x : IR | I x | forall Hx, AbsIR (F' x Hx) [<=] e}.
End Rolle.
Section Law_of_the_Mean.
The following is a simple corollary:
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Variables F F' : PartIR.
Hypothesis HF : Derivative_I Hab' F F'.
Hypothesis HA : Dom F a.
Hypothesis HB : Dom F b.
Lemma Law_of_the_Mean_I : forall e, 0 [<] e ->
{x : IR | I x | forall Hx, AbsIR (F b HB[-]F a HA[-]F' x Hx[*] (b[-]a)) [<=] e}.
Included.
Included.
Qed.
End Law_of_the_Mean.
Section Corollaries.
We can also state these theorems without expliciting the derivative of F.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Variable F : PartIR.
Hypothesis HF : Diffble_I Hab' F.
Theorem Rolle' : (forall Ha Hb, F a Ha [=] F b Hb) -> forall e, 0 [<] e ->
{x : IR | Compact Hab x | forall Hx, AbsIR (PartInt (ProjT1 HF) x Hx) [<=] e}.
Lemma Law_of_the_Mean'_I : forall HA HB e, 0 [<] e ->
{x : IR | Compact Hab x | forall Hx,
AbsIR (F b HB[-]F a HA[-]PartInt (ProjT1 HF) x Hx[*] (b[-]a)) [<=] e}.
End Corollaries.
Section Generalizations.
The mean law is more useful if we abstract a and b from the
context---allowing them in particular to be equal. In the case where
F(a) = F(b) we get Rolle's theorem again, so there is no need to
state it also in this form.
Assume I is a proper interval, F,F':PartIR.
Assume I is a proper interval, F,F':PartIR.
Variable I : interval.
Hypothesis pI : proper I.
Variables F F' : PartIR.
Hypothesis derF : Derivative I pI F F'.
Theorem Law_of_the_Mean : forall a b, I a -> I b -> forall e, 0 [<] e ->
{x : IR | Compact (Min_leEq_Max a b) x | forall Ha Hb Hx,
AbsIR (F b Hb[-]F a Ha[-]F' x Hx[*] (b[-]a)) [<=] e}.
We further generalize the mean law by writing as an explicit bound.
Theorem Law_of_the_Mean_Abs_ineq : forall a b, I a -> I b -> forall c,
(forall x, Compact (Min_leEq_Max a b) x -> forall Hx, AbsIR (F' x Hx) [<=] c) ->
forall Ha Hb, AbsIR (F b Hb[-]F a Ha) [<=] c[*]AbsIR (b[-]a).
Theorem Law_of_the_Mean_ineq : forall a b, I a -> I b -> forall c,
(forall x, Compact (Min_leEq_Max a b) x -> forall Hx, AbsIR (F' x Hx) [<=] c) ->
forall Ha Hb, F b Hb[-]F a Ha [<=] c[*]AbsIR (b[-]a).
End Generalizations.