CoRN.ftc.Rolle

Require Export DiffTactics2.
Require Export MoreFunctions.

Section Rolle.

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 | ∀ Hx, AbsIR (F' x Hx) [<=] e }.
Proof.
elim Rolle_lemma9.
  exact Rolle_lemma10.
intro.
apply Rolle_lemma13.
elim (Rolle_lemma15 b0).
  left; apply Rolle_lemma11.
   assumption.
  intro.
  eapply less_wdl.
   apply a0.
  unfold fcp' in |- *; algebra.
right; apply Rolle_lemma12.
  assumption.
intro.
eapply less_wdr.
  apply b1.
unfold fcp' in |- *; algebra.
Qed.

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 : ∀ e, [0] [<] e →
{x : IR | I x | ∀ Hx, AbsIR (F b HB [-]F a HA [-]F' x Hx [*] (b [-]a )) [<=] e }.
Proof.
intros e H.
set (h := (FId {-} [-C -]a ) {*} [-C -] (F b HB [-]F a HA ) {-}F {*} [-C -] (b [-]a )) in ×.
set (h' := [-C -] (F b HB [-]F a HA ) {-}F'{*} [-C -] (b [-]a )) in ×.
cut (Derivative_I Hab' h h').
  intro H0.
  cut {x : IR | I x | ∀ Hx, AbsIR (h' x Hx) [<=] e}.
   intro H1.
   elim H1; intros x Ix Hx.
   ∃ x.
    assumption.
   intro.
   eapply leEq_wdl.
    apply (Hx (derivative_imp_inc' _ _ _ _ _ H0 x Ix)).
   apply AbsIR_wd; simpl in |- *; rational.
  unfold I, Hab in |- *; eapply Rolle with h
    (derivative_imp_inc _ _ _ _ _ H0 _ (compact_inc_lft _ _ _))
      (derivative_imp_inc _ _ _ _ _ H0 _ (compact_inc_rht _ _ _)).
    assumption.
   simpl in |- *; rational.
  assumption.
unfold h, h' in |- *; clear h h'.
New_Deriv.
  apply Feq_reflexive.
  apply included_FMinus; Included.
apply eq_imp_Feq.
   apply included_FMinus.
    apply included_FPlus; Included.
   Included.
  Included.
intros.
simpl in |- *; rational.
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' : (∀ Ha Hb, F a Ha [=] F b Hb) → ∀ e, [0] [<] e →
{x : IR | Compact Hab x | ∀ Hx, AbsIR (PartInt (ProjT1 HF) x Hx) [<=] e }.
Proof.
intros.
unfold Hab in |- ×.
apply Rolle with F (diffble_imp_inc _ _ _ _ HF _ (compact_inc_lft a b Hab))
   (diffble_imp_inc _ _ _ _ HF _ (compact_inc_rht a b Hab)).
   apply projT2.
  apply H.
assumption.
Qed.

Lemma Law_of_the_Mean'_I : ∀ HA HB e, [0] [<] e →
{x : IR | Compact Hab x | ∀ Hx,
  AbsIR (F b HB [-]F a HA [-]PartInt (ProjT1 HF) x Hx [*] (b [-]a )) [<=] e }.
Proof.
intros.
unfold Hab in |- ×.
apply Law_of_the_Mean_I.
  apply projT2.
assumption.
Qed.

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.

Variable I : interval.
Hypothesis pI : proper I.

Variables F F' : PartIR.
Hypothesis derF : Derivative I pI F F'.

Theorem Law_of_the_Mean : ∀ a b, I a → I b → ∀ e, [0] [<] e →
{x : IR | Compact (Min_leEq_Max a b) x | ∀ Ha Hb Hx,
  AbsIR (F b Hb [-]F a Ha [-]F' x Hx [*] (b [-]a )) [<=] e }.
Proof.
intros a b Ha Hb e He.
cut (included (Compact (Min_leEq_Max a b)) I). intro H.
  2: apply included_interval'; auto.
elim (less_cotransitive_unfolded _ _ _ He
   (AbsIR (F b (incF _ Hb) [-]F a (incF _ Ha) [-]F' a (incF' _ Ha) [*] (b[-]a)))); intros.
  cut (Min a b [<] Max a b). intro H0.
   cut (included (Compact (less_leEq _ _ _ H0)) I). intro H1.
    2: apply included_interval'; auto.
   elim (ap_imp_less _ _ _ (Min_less_Max_imp_ap _ _ H0)); intro.
    cut (included (Compact (less_leEq _ _ _ a1)) I). intro H2.
     2: apply included_trans with (Compact (less_leEq _ _ _ H0)); [ apply compact_map2 | apply H1 ].
    elim (Law_of_the_Mean_I _ _ a1 _ _ (included_imp_Derivative _ _ _ _ derF _ _ a1 H2) (
      incF _ Ha) (incF _ Hb) e He).
    intros x H3 H4.
    ∃ x; auto.
     apply compact_map2 with (Hab := less_leEq _ _ _ a1); auto.
    intros.
    eapply leEq_wdl.
     apply (H4 Hx).
    apply AbsIR_wd; algebra.
   cut (included (Compact (Min_leEq_Max b a)) (Compact (Min_leEq_Max a b))). intro H2.
    cut (included (Compact (less_leEq _ _ _ b0)) I). intro H3.
     2: apply included_trans with (Compact (Min_leEq_Max b a)); [ apply compact_map2
       | apply included_trans with (Compact (less_leEq _ _ _ H0)); [ apply H2 | apply H1 ] ].
    elim (Law_of_the_Mean_I _ _ b0 _ _ (included_imp_Derivative _ _ _ _ derF _ _ b0 H3) (
      incF _ Hb) (incF _ Ha) e He).
    intros x H4 H5.
    ∃ x; auto.
     apply H2; apply compact_map2 with (Hab := less_leEq _ _ _ b0); auto.
    intros.
    eapply leEq_wdl.
     apply (H5 Hx).
    eapply eq_transitive_unfolded.
     apply AbsIR_minus.
    apply AbsIR_wd; rational.
   intros x H2.
   elim H2; clear H2; intros H3 H4; split.
    eapply leEq_wdl; [ apply H3 | apply Min_comm ].
   eapply leEq_wdr; [ apply H4 | apply Max_comm ].
  apply ap_imp_Min_less_Max.
  cut (Part _ _ (incF b Hb) [-]Part _ _ (incF a Ha) [#] [0]
    or Part _ _ (incF' a Ha) [*] (b[-]a) [#] [0]).
   intro H0.
   elim H0; clear H0; intro H1.
    apply pfstrx with F (incF a Ha) (incF b Hb).
    apply ap_symmetric_unfolded; apply zero_minus_apart; auto.
   apply ap_symmetric_unfolded; apply zero_minus_apart.
   eapply cring_mult_ap_zero_op; apply H1.
  apply cg_minus_strext.
  astepr ZeroR.
  apply AbsIR_cancel_ap_zero.
  apply Greater_imp_ap; auto.
∃ a.
  apply compact_Min_lft.
intros; apply less_leEq.
eapply less_wdl.
  apply b0.
apply AbsIR_wd; algebra.
Qed.

We further generalize the mean law by writing as an explicit bound.

Theorem Law_of_the_Mean_Abs_ineq : ∀ a b, I a → I b → ∀ c,
(∀ x, Compact (Min_leEq_Max a b) x → ∀ Hx, AbsIR (F' x Hx) [<=] c) →
∀ Ha Hb, AbsIR (F b Hb [-]F a Ha) [<=] c [*]AbsIR (b [-]a).
Proof.
intros a b Ia Ib c Hc Ha Hb.
astepr (c[*]AbsIR (b[-]a) [+][0]).
apply shift_leEq_plus'.
apply approach_zero_weak.
intros e H.
elim Law_of_the_Mean with a b e; auto.
intros x H0 H1.
cut (Dom F' x). intro H2.
  eapply leEq_transitive.
   2: apply (H1 Ha Hb H2).
  eapply leEq_transitive.
   2: apply triangle_IR_minus'.
  unfold cg_minus at 1 4 in |- *; apply plus_resp_leEq_lft.
  apply inv_resp_leEq.
  stepl (AbsIR (F' x H2)[*]AbsIR(b[-]a)).
   2:apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
  apply mult_resp_leEq_rht.
   auto.
  apply AbsIR_nonneg.
apply (Derivative_imp_inc' _ _ _ _ derF).
exact (included_interval I a b Ia Ib (Min_leEq_Max a b) x H0).
Qed.

Theorem Law_of_the_Mean_ineq : ∀ a b, I a → I b → ∀ c,
(∀ x, Compact (Min_leEq_Max a b) x → ∀ Hx, AbsIR (F' x Hx) [<=] c) →
∀ Ha Hb, F b Hb [-]F a Ha [<=] c [*]AbsIR (b [-]a).
Proof.
intros.
eapply leEq_transitive.
  apply leEq_AbsIR.
apply Law_of_the_Mean_Abs_ineq; assumption.
Qed.

End Generalizations.