diff options
Diffstat (limited to 'theories/Reals/MVT.v')
| -rw-r--r-- | theories/Reals/MVT.v | 1210 |
1 files changed, 616 insertions, 594 deletions
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 241313a0..8bb9298a 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: MVT.v 8670 2006-03-28 22:16:14Z herbelin $ i*) + +(*i $Id: MVT.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -15,685 +15,707 @@ Require Import Rtopology. Open Local Scope R_scope. (* The Mean Value Theorem *) Theorem MVT : - forall (f g:R -> R) (a b:R) (pr1:forall c:R, a < c < b -> derivable_pt f c) - (pr2:forall c:R, a < c < b -> derivable_pt g c), - a < b -> - (forall c:R, a <= c <= b -> continuity_pt f c) -> - (forall c:R, a <= c <= b -> continuity_pt g c) -> + forall (f g:R -> R) (a b:R) (pr1:forall c:R, a < c < b -> derivable_pt f c) + (pr2:forall c:R, a < c < b -> derivable_pt g c), + a < b -> + (forall c:R, a <= c <= b -> continuity_pt f c) -> + (forall c:R, a <= c <= b -> continuity_pt g c) -> exists c : R, - (exists P : a < c < b, + (exists P : a < c < b, (g b - g a) * derive_pt f c (pr1 c P) = (f b - f a) * derive_pt g c (pr2 c P)). -intros; assert (H2 := Rlt_le _ _ H). -set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). -cut (forall c:R, a < c < b -> derivable_pt h c). -intro X; cut (forall c:R, a <= c <= b -> continuity_pt h c). -intro; assert (H4 := continuity_ab_maj h a b H2 H3). -assert (H5 := continuity_ab_min h a b H2 H3). -elim H4; intros Mx H6. -elim H5; intros mx H7. -cut (h a = h b). -intro; set (M := h Mx); set (m := h mx). -cut - (forall (c:R) (P:a < c < b), - derive_pt h c (X c P) = - (g b - g a) * derive_pt f c (pr1 c P) - - (f b - f a) * derive_pt g c (pr2 c P)). -intro; case (Req_dec (h a) M); intro. -case (Req_dec (h a) m); intro. -cut (forall c:R, a <= c <= b -> h c = M). -intro; cut (a < (a + b) / 2 < b). +Proof. + intros; assert (H2 := Rlt_le _ _ H). + set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). + cut (forall c:R, a < c < b -> derivable_pt h c). + intro X; cut (forall c:R, a <= c <= b -> continuity_pt h c). + intro; assert (H4 := continuity_ab_maj h a b H2 H3). + assert (H5 := continuity_ab_min h a b H2 H3). + elim H4; intros Mx H6. + elim H5; intros mx H7. + cut (h a = h b). + intro; set (M := h Mx); set (m := h mx). + cut + (forall (c:R) (P:a < c < b), + derive_pt h c (X c P) = + (g b - g a) * derive_pt f c (pr1 c P) - + (f b - f a) * derive_pt g c (pr2 c P)). + intro; case (Req_dec (h a) M); intro. + case (Req_dec (h a) m); intro. + cut (forall c:R, a <= c <= b -> h c = M). + intro; cut (a < (a + b) / 2 < b). (*** h constant ***) -intro; exists ((a + b) / 2). -exists H13. -apply Rminus_diag_uniq; rewrite <- H9; apply deriv_constant2 with a b. -elim H13; intros; assumption. -elim H13; intros; assumption. -intros; rewrite (H12 ((a + b) / 2)). -apply H12; split; left; assumption. -elim H13; intros; split; left; assumption. -split. -apply Rmult_lt_reg_l with 2. -prove_sup0. -unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; - rewrite <- Rinv_r_sym. -rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H. -discrR. -apply Rmult_lt_reg_l with 2. -prove_sup0. -unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; - rewrite <- Rinv_r_sym. -rewrite Rmult_1_l; rewrite Rplus_comm; rewrite double; - apply Rplus_lt_compat_l; apply H. -discrR. -intros; elim H6; intros H13 _. -elim H7; intros H14 _. -apply Rle_antisym. -apply H13; apply H12. -rewrite H10 in H11; rewrite H11; apply H14; apply H12. -cut (a < mx < b). + intro; exists ((a + b) / 2). + exists H13. + apply Rminus_diag_uniq; rewrite <- H9; apply deriv_constant2 with a b. + elim H13; intros; assumption. + elim H13; intros; assumption. + intros; rewrite (H12 ((a + b) / 2)). + apply H12; split; left; assumption. + elim H13; intros; split; left; assumption. + split. + apply Rmult_lt_reg_l with 2. + prove_sup0. + unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + rewrite <- Rinv_r_sym. + rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H. + discrR. + apply Rmult_lt_reg_l with 2. + prove_sup0. + unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + rewrite <- Rinv_r_sym. + rewrite Rmult_1_l; rewrite Rplus_comm; rewrite double; + apply Rplus_lt_compat_l; apply H. + discrR. + intros; elim H6; intros H13 _. + elim H7; intros H14 _. + apply Rle_antisym. + apply H13; apply H12. + rewrite H10 in H11; rewrite H11; apply H14; apply H12. + cut (a < mx < b). (*** h admet un minimum global sur [a,b] ***) -intro; exists mx. -exists H12. -apply Rminus_diag_uniq; rewrite <- H9; apply deriv_minimum with a b. -elim H12; intros; assumption. -elim H12; intros; assumption. -intros; elim H7; intros. -apply H15; split; left; assumption. -elim H7; intros _ H12; elim H12; intros; split. -inversion H13. -apply H15. -rewrite H15 in H11; elim H11; reflexivity. -inversion H14. -apply H15. -rewrite H8 in H11; rewrite <- H15 in H11; elim H11; reflexivity. -cut (a < Mx < b). + intro; exists mx. + exists H12. + apply Rminus_diag_uniq; rewrite <- H9; apply deriv_minimum with a b. + elim H12; intros; assumption. + elim H12; intros; assumption. + intros; elim H7; intros. + apply H15; split; left; assumption. + elim H7; intros _ H12; elim H12; intros; split. + inversion H13. + apply H15. + rewrite H15 in H11; elim H11; reflexivity. + inversion H14. + apply H15. + rewrite H8 in H11; rewrite <- H15 in H11; elim H11; reflexivity. + cut (a < Mx < b). (*** h admet un maximum global sur [a,b] ***) -intro; exists Mx. -exists H11. -apply Rminus_diag_uniq; rewrite <- H9; apply deriv_maximum with a b. -elim H11; intros; assumption. -elim H11; intros; assumption. -intros; elim H6; intros; apply H14. -split; left; assumption. -elim H6; intros _ H11; elim H11; intros; split. -inversion H12. -apply H14. -rewrite H14 in H10; elim H10; reflexivity. -inversion H13. -apply H14. -rewrite H8 in H10; rewrite <- H14 in H10; elim H10; reflexivity. -intros; unfold h in |- *; - replace - (derive_pt (fun y:R => (g b - g a) * f y - (f b - f a) * g y) c (X c P)) - with - (derive_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) c - (derivable_pt_minus _ _ _ - (derivable_pt_mult _ _ _ (derivable_pt_const (g b - g a) c) (pr1 c P)) - (derivable_pt_mult _ _ _ (derivable_pt_const (f b - f a) c) (pr2 c P)))); - [ idtac | apply pr_nu ]. -rewrite derive_pt_minus; do 2 rewrite derive_pt_mult; - do 2 rewrite derive_pt_const; do 2 rewrite Rmult_0_l; - do 2 rewrite Rplus_0_l; reflexivity. -unfold h in |- *; ring. -intros; unfold h in |- *; - change - (continuity_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) - c) in |- *. -apply continuity_pt_minus; apply continuity_pt_mult. -apply derivable_continuous_pt; apply derivable_const. -apply H0; apply H3. -apply derivable_continuous_pt; apply derivable_const. -apply H1; apply H3. -intros; - change - (derivable_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) - c) in |- *. -apply derivable_pt_minus; apply derivable_pt_mult. -apply derivable_pt_const. -apply (pr1 _ H3). -apply derivable_pt_const. -apply (pr2 _ H3). + intro; exists Mx. + exists H11. + apply Rminus_diag_uniq; rewrite <- H9; apply deriv_maximum with a b. + elim H11; intros; assumption. + elim H11; intros; assumption. + intros; elim H6; intros; apply H14. + split; left; assumption. + elim H6; intros _ H11; elim H11; intros; split. + inversion H12. + apply H14. + rewrite H14 in H10; elim H10; reflexivity. + inversion H13. + apply H14. + rewrite H8 in H10; rewrite <- H14 in H10; elim H10; reflexivity. + intros; unfold h in |- *; + replace + (derive_pt (fun y:R => (g b - g a) * f y - (f b - f a) * g y) c (X c P)) + with + (derive_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) c + (derivable_pt_minus _ _ _ + (derivable_pt_mult _ _ _ (derivable_pt_const (g b - g a) c) (pr1 c P)) + (derivable_pt_mult _ _ _ (derivable_pt_const (f b - f a) c) (pr2 c P)))); + [ idtac | apply pr_nu ]. + rewrite derive_pt_minus; do 2 rewrite derive_pt_mult; + do 2 rewrite derive_pt_const; do 2 rewrite Rmult_0_l; + do 2 rewrite Rplus_0_l; reflexivity. + unfold h in |- *; ring. + intros; unfold h in |- *; + change + (continuity_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) + c) in |- *. + apply continuity_pt_minus; apply continuity_pt_mult. + apply derivable_continuous_pt; apply derivable_const. + apply H0; apply H3. + apply derivable_continuous_pt; apply derivable_const. + apply H1; apply H3. + intros; + change + (derivable_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) + c) in |- *. + apply derivable_pt_minus; apply derivable_pt_mult. + apply derivable_pt_const. + apply (pr1 _ H3). + apply derivable_pt_const. + apply (pr2 _ H3). Qed. (* Corollaries ... *) Lemma MVT_cor1 : - forall (f:R -> R) (a b:R) (pr:derivable f), - a < b -> + forall (f:R -> R) (a b:R) (pr:derivable f), + a < b -> exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b. -intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c); - [ intro X | intros; apply pr ]. -cut (forall c:R, a < c < b -> derivable_pt id c); - [ intro X0 | intros; apply derivable_pt_id ]. -cut (forall c:R, a <= c <= b -> continuity_pt f c); - [ intro | intros; apply derivable_continuous_pt; apply pr ]. -cut (forall c:R, a <= c <= b -> continuity_pt id c); - [ intro | intros; apply derivable_continuous_pt; apply derivable_id ]. -assert (H2 := MVT f id a b X X0 H H0 H1). -elim H2; intros c H3; elim H3; intros. -exists c; split. -cut (derive_pt id c (X0 c x) = derive_pt id c (derivable_pt_id c)); - [ intro | apply pr_nu ]. -rewrite H5 in H4; rewrite (derive_pt_id c) in H4; rewrite Rmult_1_r in H4; - rewrite <- H4; replace (derive_pt f c (X c x)) with (derive_pt f c (pr c)); - [ idtac | apply pr_nu ]; apply Rmult_comm. -apply x. +Proof. + intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c); + [ intro X | intros; apply pr ]. + cut (forall c:R, a < c < b -> derivable_pt id c); + [ intro X0 | intros; apply derivable_pt_id ]. + cut (forall c:R, a <= c <= b -> continuity_pt f c); + [ intro | intros; apply derivable_continuous_pt; apply pr ]. + cut (forall c:R, a <= c <= b -> continuity_pt id c); + [ intro | intros; apply derivable_continuous_pt; apply derivable_id ]. + assert (H2 := MVT f id a b X X0 H H0 H1). + elim H2; intros c H3; elim H3; intros. + exists c; split. + cut (derive_pt id c (X0 c x) = derive_pt id c (derivable_pt_id c)); + [ intro | apply pr_nu ]. + rewrite H5 in H4; rewrite (derive_pt_id c) in H4; rewrite Rmult_1_r in H4; + rewrite <- H4; replace (derive_pt f c (X c x)) with (derive_pt f c (pr c)); + [ idtac | apply pr_nu ]; apply Rmult_comm. + apply x. Qed. Theorem MVT_cor2 : - forall (f f':R -> R) (a b:R), - a < b -> - (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) -> + forall (f f':R -> R) (a b:R), + a < b -> + (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) -> exists c : R, f b - f a = f' c * (b - a) /\ a < c < b. -intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c). -intro X; cut (forall c:R, a < c < b -> derivable_pt f c). -intro X0; cut (forall c:R, a <= c <= b -> continuity_pt f c). -intro; cut (forall c:R, a <= c <= b -> derivable_pt id c). -intro X1; cut (forall c:R, a < c < b -> derivable_pt id c). -intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c). -intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros; - exists x; split. -cut (derive_pt id x (X2 x x0) = 1). -cut (derive_pt f x (X0 x x0) = f' x). -intros; rewrite H4 in H3; rewrite H5 in H3; unfold id in H3; - rewrite Rmult_1_r in H3; rewrite Rmult_comm; symmetry in |- *; - assumption. -apply derive_pt_eq_0; apply H0; elim x0; intros; split; left; assumption. -apply derive_pt_eq_0; apply derivable_pt_lim_id. -assumption. -intros; apply derivable_continuous_pt; apply X1; assumption. -intros; apply derivable_pt_id. -intros; apply derivable_pt_id. -intros; apply derivable_continuous_pt; apply X; assumption. -intros; elim H1; intros; apply X; split; left; assumption. -intros; unfold derivable_pt in |- *; apply existT with (f' c); apply H0; - apply H1. +Proof. + intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c). + intro X; cut (forall c:R, a < c < b -> derivable_pt f c). + intro X0; cut (forall c:R, a <= c <= b -> continuity_pt f c). + intro; cut (forall c:R, a <= c <= b -> derivable_pt id c). + intro X1; cut (forall c:R, a < c < b -> derivable_pt id c). + intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c). + intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros; + exists x; split. + cut (derive_pt id x (X2 x x0) = 1). + cut (derive_pt f x (X0 x x0) = f' x). + intros; rewrite H4 in H3; rewrite H5 in H3; unfold id in H3; + rewrite Rmult_1_r in H3; rewrite Rmult_comm; symmetry in |- *; + assumption. + apply derive_pt_eq_0; apply H0; elim x0; intros; split; left; assumption. + apply derive_pt_eq_0; apply derivable_pt_lim_id. + assumption. + intros; apply derivable_continuous_pt; apply X1; assumption. + intros; apply derivable_pt_id. + intros; apply derivable_pt_id. + intros; apply derivable_continuous_pt; apply X; assumption. + intros; elim H1; intros; apply X; split; left; assumption. + intros; unfold derivable_pt in |- *; apply existT with (f' c); apply H0; + apply H1. Qed. Lemma MVT_cor3 : - forall (f f':R -> R) (a b:R), - a < b -> - (forall x:R, a <= x -> x <= b -> derivable_pt_lim f x (f' x)) -> + forall (f f':R -> R) (a b:R), + a < b -> + (forall x:R, a <= x -> x <= b -> derivable_pt_lim f x (f' x)) -> exists c : R, a <= c /\ c <= b /\ f b = f a + f' c * (b - a). -intros f f' a b H H0; - assert (H1 : exists c : R, f b - f a = f' c * (b - a) /\ a < c < b); - [ apply MVT_cor2; [ apply H | intros; elim H1; intros; apply (H0 _ H2 H3) ] - | elim H1; intros; exists x; elim H2; intros; elim H4; intros; split; - [ left; assumption | split; [ left; assumption | rewrite <- H3; ring ] ] ]. +Proof. + intros f f' a b H H0; + assert (H1 : exists c : R, f b - f a = f' c * (b - a) /\ a < c < b); + [ apply MVT_cor2; [ apply H | intros; elim H1; intros; apply (H0 _ H2 H3) ] + | elim H1; intros; exists x; elim H2; intros; elim H4; intros; split; + [ left; assumption | split; [ left; assumption | rewrite <- H3; ring ] ] ]. Qed. Lemma Rolle : - forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x), - (forall x:R, a <= x <= b -> continuity_pt f x) -> - a < b -> - f a = f b -> + forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x), + (forall x:R, a <= x <= b -> continuity_pt f x) -> + a < b -> + f a = f b -> exists c : R, (exists P : a < c < b, derive_pt f c (pr c P) = 0). -intros; assert (H2 : forall x:R, a < x < b -> derivable_pt id x). -intros; apply derivable_pt_id. -assert (H3 := MVT f id a b pr H2 H0 H); - assert (H4 : forall x:R, a <= x <= b -> continuity_pt id x). -intros; apply derivable_continuous; apply derivable_id. -elim (H3 H4); intros; elim H5; intros; exists x; exists x0; rewrite H1 in H6; - unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6; - rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a); - [ rewrite Rmult_0_r; apply H6 - | apply Rminus_eq_contra; red in |- *; intro; rewrite H7 in H0; - elim (Rlt_irrefl _ H0) ]. +Proof. + intros; assert (H2 : forall x:R, a < x < b -> derivable_pt id x). + intros; apply derivable_pt_id. + assert (H3 := MVT f id a b pr H2 H0 H); + assert (H4 : forall x:R, a <= x <= b -> continuity_pt id x). + intros; apply derivable_continuous; apply derivable_id. + elim (H3 H4); intros; elim H5; intros; exists x; exists x0; rewrite H1 in H6; + unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6; + rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a); + [ rewrite Rmult_0_r; apply H6 + | apply Rminus_eq_contra; red in |- *; intro; rewrite H7 in H0; + elim (Rlt_irrefl _ H0) ]. Qed. (**********) Lemma nonneg_derivative_1 : - forall (f:R -> R) (pr:derivable f), - (forall x:R, 0 <= derive_pt f x (pr x)) -> increasing f. -intros. -unfold increasing in |- *. -intros. -case (total_order_T x y); intro. -elim s; intro. -apply Rplus_le_reg_l with (- f x). -rewrite Rplus_opp_l; rewrite Rplus_comm. -assert (H1 := MVT_cor1 f _ _ pr a). -elim H1; intros. -elim H2; intros. -unfold Rminus in H3. -rewrite H3. -apply Rmult_le_pos. -apply H. -apply Rplus_le_reg_l with x. -rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. -rewrite b; right; reflexivity. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r)). + forall (f:R -> R) (pr:derivable f), + (forall x:R, 0 <= derive_pt f x (pr x)) -> increasing f. +Proof. + intros. + unfold increasing in |- *. + intros. + case (total_order_T x y); intro. + elim s; intro. + apply Rplus_le_reg_l with (- f x). + rewrite Rplus_opp_l; rewrite Rplus_comm. + assert (H1 := MVT_cor1 f _ _ pr a). + elim H1; intros. + elim H2; intros. + unfold Rminus in H3. + rewrite H3. + apply Rmult_le_pos. + apply H. + apply Rplus_le_reg_l with x. + rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. + rewrite b; right; reflexivity. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r)). Qed. - + (**********) Lemma nonpos_derivative_0 : - forall (f:R -> R) (pr:derivable f), - decreasing f -> forall x:R, derive_pt f x (pr x) <= 0. -intros f pr H x; assert (H0 := H); unfold decreasing in H0; - generalize (derivable_derive f x (pr x)); intro; elim H1; - intros l H2. -rewrite H2; case (Rtotal_order l 0); intro. -left; assumption. -elim H3; intro. -right; assumption. -generalize (derive_pt_eq_1 f x l (pr x) H2); intros; cut (0 < l / 2). -intro; elim (H5 (l / 2) H6); intros delta H7; - cut (delta / 2 <> 0 /\ 0 < delta / 2 /\ Rabs (delta / 2) < delta). -intro; decompose [and] H8; intros; generalize (H7 (delta / 2) H9 H12); - cut ((f (x + delta / 2) - f x) / (delta / 2) <= 0). -intro; cut (0 < - ((f (x + delta / 2) - f x) / (delta / 2) - l)). -intro; unfold Rabs in |- *; - case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)). -intros; - generalize - (Rplus_lt_compat_r (- l) (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) - (l / 2) H14); unfold Rminus in |- *. -replace (l / 2 + - l) with (- (l / 2)). -replace (- ((f (x + delta / 2) + - f x) / (delta / 2) + - l) + - l) with - (- ((f (x + delta / 2) + - f x) / (delta / 2))). -intro. -generalize - (Ropp_lt_gt_contravar (- ((f (x + delta / 2) + - f x) / (delta / 2))) - (- (l / 2)) H15). -repeat rewrite Ropp_involutive. -intro. -generalize - (Rlt_trans 0 (l / 2) ((f (x + delta / 2) - f x) / (delta / 2)) H6 H16); - intro. -elim - (Rlt_irrefl 0 - (Rlt_le_trans 0 ((f (x + delta / 2) - f x) / (delta / 2)) 0 H17 H10)). -ring. -pattern l at 3 in |- *; rewrite double_var. -ring. -intros. -generalize - (Ropp_ge_le_contravar ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 r). -rewrite Ropp_0. -intro. -elim - (Rlt_irrefl 0 - (Rlt_le_trans 0 (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) 0 H13 - H15)). -replace (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) with - ((f x - f (x + delta / 2)) / (delta / 2) + l). -unfold Rminus in |- *. -apply Rplus_le_lt_0_compat. -unfold Rdiv in |- *; apply Rmult_le_pos. -cut (x <= x + delta * / 2). -intro; generalize (H0 x (x + delta * / 2) H13); intro; - generalize - (Rplus_le_compat_l (- f (x + delta / 2)) (f (x + delta / 2)) (f x) H14); - rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption. -pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - left; assumption. -left; apply Rinv_0_lt_compat; assumption. -assumption. -rewrite Ropp_minus_distr. -unfold Rminus in |- *. -rewrite (Rplus_comm l). -unfold Rdiv in |- *. -rewrite <- Ropp_mult_distr_l_reverse. -rewrite Ropp_plus_distr. -rewrite Ropp_involutive. -rewrite (Rplus_comm (f x)). -reflexivity. -replace ((f (x + delta / 2) - f x) / (delta / 2)) with - (- ((f x - f (x + delta / 2)) / (delta / 2))). -rewrite <- Ropp_0. -apply Ropp_ge_le_contravar. -apply Rle_ge. -unfold Rdiv in |- *; apply Rmult_le_pos. -cut (x <= x + delta * / 2). -intro; generalize (H0 x (x + delta * / 2) H10); intro. -generalize - (Rplus_le_compat_l (- f (x + delta / 2)) (f (x + delta / 2)) (f x) H13); - rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption. -pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - left; assumption. -left; apply Rinv_0_lt_compat; assumption. -unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse. -rewrite Ropp_minus_distr. -reflexivity. -split. -unfold Rdiv in |- *; apply prod_neq_R0. -generalize (cond_pos delta); intro; red in |- *; intro H9; rewrite H9 in H8; - elim (Rlt_irrefl 0 H8). -apply Rinv_neq_0_compat; discrR. -split. -unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. -rewrite Rabs_right. -unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2. -prove_sup0. -rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. -rewrite Rmult_1_l; rewrite double; pattern (pos delta) at 1 in |- *; - rewrite <- Rplus_0_r. -apply Rplus_lt_compat_l; apply (cond_pos delta). -discrR. -apply Rle_ge; unfold Rdiv in |- *; left; apply Rmult_lt_0_compat. -apply (cond_pos delta). -apply Rinv_0_lt_compat; prove_sup0. -unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply H4 | apply Rinv_0_lt_compat; prove_sup0 ]. + forall (f:R -> R) (pr:derivable f), + decreasing f -> forall x:R, derive_pt f x (pr x) <= 0. +Proof. + intros f pr H x; assert (H0 := H); unfold decreasing in H0; + generalize (derivable_derive f x (pr x)); intro; elim H1; + intros l H2. + rewrite H2; case (Rtotal_order l 0); intro. + left; assumption. + elim H3; intro. + right; assumption. + generalize (derive_pt_eq_1 f x l (pr x) H2); intros; cut (0 < l / 2). + intro; elim (H5 (l / 2) H6); intros delta H7; + cut (delta / 2 <> 0 /\ 0 < delta / 2 /\ Rabs (delta / 2) < delta). + intro; decompose [and] H8; intros; generalize (H7 (delta / 2) H9 H12); + cut ((f (x + delta / 2) - f x) / (delta / 2) <= 0). + intro; cut (0 < - ((f (x + delta / 2) - f x) / (delta / 2) - l)). + intro; unfold Rabs in |- *; + case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)). + intros; + generalize + (Rplus_lt_compat_r (- l) (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) + (l / 2) H14); unfold Rminus in |- *. + replace (l / 2 + - l) with (- (l / 2)). + replace (- ((f (x + delta / 2) + - f x) / (delta / 2) + - l) + - l) with + (- ((f (x + delta / 2) + - f x) / (delta / 2))). + intro. + generalize + (Ropp_lt_gt_contravar (- ((f (x + delta / 2) + - f x) / (delta / 2))) + (- (l / 2)) H15). + repeat rewrite Ropp_involutive. + intro. + generalize + (Rlt_trans 0 (l / 2) ((f (x + delta / 2) - f x) / (delta / 2)) H6 H16); + intro. + elim + (Rlt_irrefl 0 + (Rlt_le_trans 0 ((f (x + delta / 2) - f x) / (delta / 2)) 0 H17 H10)). + ring. + pattern l at 3 in |- *; rewrite double_var. + ring. + intros. + generalize + (Ropp_ge_le_contravar ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 r). + rewrite Ropp_0. + intro. + elim + (Rlt_irrefl 0 + (Rlt_le_trans 0 (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) 0 H13 + H15)). + replace (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) with + ((f x - f (x + delta / 2)) / (delta / 2) + l). + unfold Rminus in |- *. + apply Rplus_le_lt_0_compat. + unfold Rdiv in |- *; apply Rmult_le_pos. + cut (x <= x + delta * / 2). + intro; generalize (H0 x (x + delta * / 2) H13); intro; + generalize + (Rplus_le_compat_l (- f (x + delta / 2)) (f (x + delta / 2)) (f x) H14); + rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption. + pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + left; assumption. + left; apply Rinv_0_lt_compat; assumption. + assumption. + rewrite Ropp_minus_distr. + unfold Rminus in |- *. + rewrite (Rplus_comm l). + unfold Rdiv in |- *. + rewrite <- Ropp_mult_distr_l_reverse. + rewrite Ropp_plus_distr. + rewrite Ropp_involutive. + rewrite (Rplus_comm (f x)). + reflexivity. + replace ((f (x + delta / 2) - f x) / (delta / 2)) with + (- ((f x - f (x + delta / 2)) / (delta / 2))). + rewrite <- Ropp_0. + apply Ropp_ge_le_contravar. + apply Rle_ge. + unfold Rdiv in |- *; apply Rmult_le_pos. + cut (x <= x + delta * / 2). + intro; generalize (H0 x (x + delta * / 2) H10); intro. + generalize + (Rplus_le_compat_l (- f (x + delta / 2)) (f (x + delta / 2)) (f x) H13); + rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption. + pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + left; assumption. + left; apply Rinv_0_lt_compat; assumption. + unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse. + rewrite Ropp_minus_distr. + reflexivity. + split. + unfold Rdiv in |- *; apply prod_neq_R0. + generalize (cond_pos delta); intro; red in |- *; intro H9; rewrite H9 in H8; + elim (Rlt_irrefl 0 H8). + apply Rinv_neq_0_compat; discrR. + split. + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. + rewrite Rabs_right. + unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2. + prove_sup0. + rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. + rewrite Rmult_1_l; rewrite double; pattern (pos delta) at 1 in |- *; + rewrite <- Rplus_0_r. + apply Rplus_lt_compat_l; apply (cond_pos delta). + discrR. + apply Rle_ge; unfold Rdiv in |- *; left; apply Rmult_lt_0_compat. + apply (cond_pos delta). + apply Rinv_0_lt_compat; prove_sup0. + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply H4 | apply Rinv_0_lt_compat; prove_sup0 ]. Qed. (**********) Lemma increasing_decreasing_opp : - forall f:R -> R, increasing f -> decreasing (- f)%F. -unfold increasing, decreasing, opp_fct in |- *; intros; generalize (H x y H0); - intro; apply Ropp_ge_le_contravar; apply Rle_ge; assumption. + forall f:R -> R, increasing f -> decreasing (- f)%F. +Proof. + unfold increasing, decreasing, opp_fct in |- *; intros; generalize (H x y H0); + intro; apply Ropp_ge_le_contravar; apply Rle_ge; assumption. Qed. (**********) Lemma nonpos_derivative_1 : - forall (f:R -> R) (pr:derivable f), - (forall x:R, derive_pt f x (pr x) <= 0) -> decreasing f. -intros. -cut (forall h:R, - - f h = f h). -intro. -generalize (increasing_decreasing_opp (- f)%F). -unfold decreasing in |- *. -unfold opp_fct in |- *. -intros. -rewrite <- (H0 x); rewrite <- (H0 y). -apply H1. -cut (forall x:R, 0 <= derive_pt (- f) x (derivable_opp f pr x)). -intros. -replace (fun x:R => - f x) with (- f)%F; [ idtac | reflexivity ]. -apply (nonneg_derivative_1 (- f)%F (derivable_opp f pr) H3). -intro. -assert (H3 := derive_pt_opp f x0 (pr x0)). -cut - (derive_pt (- f) x0 (derivable_pt_opp f x0 (pr x0)) = - derive_pt (- f) x0 (derivable_opp f pr x0)). -intro. -rewrite <- H4. -rewrite H3. -rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; apply (H x0). -apply pr_nu. -assumption. -intro; ring. + forall (f:R -> R) (pr:derivable f), + (forall x:R, derive_pt f x (pr x) <= 0) -> decreasing f. +Proof. + intros. + cut (forall h:R, - - f h = f h). + intro. + generalize (increasing_decreasing_opp (- f)%F). + unfold decreasing in |- *. + unfold opp_fct in |- *. + intros. + rewrite <- (H0 x); rewrite <- (H0 y). + apply H1. + cut (forall x:R, 0 <= derive_pt (- f) x (derivable_opp f pr x)). + intros. + replace (fun x:R => - f x) with (- f)%F; [ idtac | reflexivity ]. + apply (nonneg_derivative_1 (- f)%F (derivable_opp f pr) H3). + intro. + assert (H3 := derive_pt_opp f x0 (pr x0)). + cut + (derive_pt (- f) x0 (derivable_pt_opp f x0 (pr x0)) = + derive_pt (- f) x0 (derivable_opp f pr x0)). + intro. + rewrite <- H4. + rewrite H3. + rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; apply (H x0). + apply pr_nu. + assumption. + intro; ring. Qed. - + (**********) Lemma positive_derivative : - forall (f:R -> R) (pr:derivable f), - (forall x:R, 0 < derive_pt f x (pr x)) -> strict_increasing f. -intros. -unfold strict_increasing in |- *. -intros. -apply Rplus_lt_reg_r with (- f x). -rewrite Rplus_opp_l; rewrite Rplus_comm. -assert (H1 := MVT_cor1 f _ _ pr H0). -elim H1; intros. -elim H2; intros. -unfold Rminus in H3. -rewrite H3. -apply Rmult_lt_0_compat. -apply H. -apply Rplus_lt_reg_r with x. -rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. + forall (f:R -> R) (pr:derivable f), + (forall x:R, 0 < derive_pt f x (pr x)) -> strict_increasing f. +Proof. + intros. + unfold strict_increasing in |- *. + intros. + apply Rplus_lt_reg_r with (- f x). + rewrite Rplus_opp_l; rewrite Rplus_comm. + assert (H1 := MVT_cor1 f _ _ pr H0). + elim H1; intros. + elim H2; intros. + unfold Rminus in H3. + rewrite H3. + apply Rmult_lt_0_compat. + apply H. + apply Rplus_lt_reg_r with x. + rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. Qed. (**********) Lemma strictincreasing_strictdecreasing_opp : - forall f:R -> R, strict_increasing f -> strict_decreasing (- f)%F. -unfold strict_increasing, strict_decreasing, opp_fct in |- *; intros; - generalize (H x y H0); intro; apply Ropp_lt_gt_contravar; - assumption. + forall f:R -> R, strict_increasing f -> strict_decreasing (- f)%F. +Proof. + unfold strict_increasing, strict_decreasing, opp_fct in |- *; intros; + generalize (H x y H0); intro; apply Ropp_lt_gt_contravar; + assumption. Qed. - + (**********) Lemma negative_derivative : - forall (f:R -> R) (pr:derivable f), - (forall x:R, derive_pt f x (pr x) < 0) -> strict_decreasing f. -intros. -cut (forall h:R, - - f h = f h). -intros. -generalize (strictincreasing_strictdecreasing_opp (- f)%F). -unfold strict_decreasing, opp_fct in |- *. -intros. -rewrite <- (H0 x). -rewrite <- (H0 y). -apply H1; [ idtac | assumption ]. -cut (forall x:R, 0 < derive_pt (- f) x (derivable_opp f pr x)). -intros; eapply positive_derivative; apply H3. -intro. -assert (H3 := derive_pt_opp f x0 (pr x0)). -cut - (derive_pt (- f) x0 (derivable_pt_opp f x0 (pr x0)) = - derive_pt (- f) x0 (derivable_opp f pr x0)). -intro. -rewrite <- H4; rewrite H3. -rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply (H x0). -apply pr_nu. -intro; ring. + forall (f:R -> R) (pr:derivable f), + (forall x:R, derive_pt f x (pr x) < 0) -> strict_decreasing f. +Proof. + intros. + cut (forall h:R, - - f h = f h). + intros. + generalize (strictincreasing_strictdecreasing_opp (- f)%F). + unfold strict_decreasing, opp_fct in |- *. + intros. + rewrite <- (H0 x). + rewrite <- (H0 y). + apply H1; [ idtac | assumption ]. + cut (forall x:R, 0 < derive_pt (- f) x (derivable_opp f pr x)). + intros; eapply positive_derivative; apply H3. + intro. + assert (H3 := derive_pt_opp f x0 (pr x0)). + cut + (derive_pt (- f) x0 (derivable_pt_opp f x0 (pr x0)) = + derive_pt (- f) x0 (derivable_opp f pr x0)). + intro. + rewrite <- H4; rewrite H3. + rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply (H x0). + apply pr_nu. + intro; ring. Qed. - + (**********) Lemma null_derivative_0 : - forall (f:R -> R) (pr:derivable f), - constant f -> forall x:R, derive_pt f x (pr x) = 0. -intros. -unfold constant in H. -apply derive_pt_eq_0. -intros; exists (mkposreal 1 Rlt_0_1); simpl in |- *; intros. -rewrite (H x (x + h)); unfold Rminus in |- *; unfold Rdiv in |- *; - rewrite Rplus_opp_r; rewrite Rmult_0_l; rewrite Rplus_opp_r; - rewrite Rabs_R0; assumption. + forall (f:R -> R) (pr:derivable f), + constant f -> forall x:R, derive_pt f x (pr x) = 0. +Proof. + intros. + unfold constant in H. + apply derive_pt_eq_0. + intros; exists (mkposreal 1 Rlt_0_1); simpl in |- *; intros. + rewrite (H x (x + h)); unfold Rminus in |- *; unfold Rdiv in |- *; + rewrite Rplus_opp_r; rewrite Rmult_0_l; rewrite Rplus_opp_r; + rewrite Rabs_R0; assumption. Qed. (**********) Lemma increasing_decreasing : - forall f:R -> R, increasing f -> decreasing f -> constant f. -unfold increasing, decreasing, constant in |- *; intros; - case (Rtotal_order x y); intro. -generalize (Rlt_le x y H1); intro; - apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)). -elim H1; intro. -rewrite H2; reflexivity. -generalize (Rlt_le y x H2); intro; symmetry in |- *; - apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)). + forall f:R -> R, increasing f -> decreasing f -> constant f. +Proof. + unfold increasing, decreasing, constant in |- *; intros; + case (Rtotal_order x y); intro. + generalize (Rlt_le x y H1); intro; + apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)). + elim H1; intro. + rewrite H2; reflexivity. + generalize (Rlt_le y x H2); intro; symmetry in |- *; + apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)). Qed. (**********) Lemma null_derivative_1 : - forall (f:R -> R) (pr:derivable f), - (forall x:R, derive_pt f x (pr x) = 0) -> constant f. -intros. -cut (forall x:R, derive_pt f x (pr x) <= 0). -cut (forall x:R, 0 <= derive_pt f x (pr x)). -intros. -assert (H2 := nonneg_derivative_1 f pr H0). -assert (H3 := nonpos_derivative_1 f pr H1). -apply increasing_decreasing; assumption. -intro; right; symmetry in |- *; apply (H x). -intro; right; apply (H x). + forall (f:R -> R) (pr:derivable f), + (forall x:R, derive_pt f x (pr x) = 0) -> constant f. +Proof. + intros. + cut (forall x:R, derive_pt f x (pr x) <= 0). + cut (forall x:R, 0 <= derive_pt f x (pr x)). + intros. + assert (H2 := nonneg_derivative_1 f pr H0). + assert (H3 := nonpos_derivative_1 f pr H1). + apply increasing_decreasing; assumption. + intro; right; symmetry in |- *; apply (H x). + intro; right; apply (H x). Qed. (**********) Lemma derive_increasing_interv_ax : - forall (a b:R) (f:R -> R) (pr:derivable f), - a < b -> - ((forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) -> - forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y) /\ - ((forall t:R, a < t < b -> 0 <= derive_pt f t (pr t)) -> - forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x <= f y). -intros. -split; intros. -apply Rplus_lt_reg_r with (- f x). -rewrite Rplus_opp_l; rewrite Rplus_comm. -assert (H4 := MVT_cor1 f _ _ pr H3). -elim H4; intros. -elim H5; intros. -unfold Rminus in H6. -rewrite H6. -apply Rmult_lt_0_compat. -apply H0. -elim H7; intros. -split. -elim H1; intros. -apply Rle_lt_trans with x; assumption. -elim H2; intros. -apply Rlt_le_trans with y; assumption. -apply Rplus_lt_reg_r with x. -rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. -apply Rplus_le_reg_l with (- f x). -rewrite Rplus_opp_l; rewrite Rplus_comm. -assert (H4 := MVT_cor1 f _ _ pr H3). -elim H4; intros. -elim H5; intros. -unfold Rminus in H6. -rewrite H6. -apply Rmult_le_pos. -apply H0. -elim H7; intros. -split. -elim H1; intros. -apply Rle_lt_trans with x; assumption. -elim H2; intros. -apply Rlt_le_trans with y; assumption. -apply Rplus_le_reg_l with x. -rewrite Rplus_0_r; replace (x + (y + - x)) with y; - [ left; assumption | ring ]. + forall (a b:R) (f:R -> R) (pr:derivable f), + a < b -> + ((forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) -> + forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y) /\ + ((forall t:R, a < t < b -> 0 <= derive_pt f t (pr t)) -> + forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x <= f y). +Proof. + intros. + split; intros. + apply Rplus_lt_reg_r with (- f x). + rewrite Rplus_opp_l; rewrite Rplus_comm. + assert (H4 := MVT_cor1 f _ _ pr H3). + elim H4; intros. + elim H5; intros. + unfold Rminus in H6. + rewrite H6. + apply Rmult_lt_0_compat. + apply H0. + elim H7; intros. + split. + elim H1; intros. + apply Rle_lt_trans with x; assumption. + elim H2; intros. + apply Rlt_le_trans with y; assumption. + apply Rplus_lt_reg_r with x. + rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. + apply Rplus_le_reg_l with (- f x). + rewrite Rplus_opp_l; rewrite Rplus_comm. + assert (H4 := MVT_cor1 f _ _ pr H3). + elim H4; intros. + elim H5; intros. + unfold Rminus in H6. + rewrite H6. + apply Rmult_le_pos. + apply H0. + elim H7; intros. + split. + elim H1; intros. + apply Rle_lt_trans with x; assumption. + elim H2; intros. + apply Rlt_le_trans with y; assumption. + apply Rplus_le_reg_l with x. + rewrite Rplus_0_r; replace (x + (y + - x)) with y; + [ left; assumption | ring ]. Qed. (**********) Lemma derive_increasing_interv : - forall (a b:R) (f:R -> R) (pr:derivable f), - a < b -> - (forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) -> - forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y. -intros. -generalize (derive_increasing_interv_ax a b f pr H); intro. -elim H4; intros H5 _; apply (H5 H0 x y H1 H2 H3). + forall (a b:R) (f:R -> R) (pr:derivable f), + a < b -> + (forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) -> + forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y. +Proof. + intros. + generalize (derive_increasing_interv_ax a b f pr H); intro. + elim H4; intros H5 _; apply (H5 H0 x y H1 H2 H3). Qed. (**********) Lemma derive_increasing_interv_var : - forall (a b:R) (f:R -> R) (pr:derivable f), - a < b -> - (forall t:R, a < t < b -> 0 <= derive_pt f t (pr t)) -> - forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x <= f y. -intros a b f pr H H0 x y H1 H2 H3; - generalize (derive_increasing_interv_ax a b f pr H); - intro; elim H4; intros _ H5; apply (H5 H0 x y H1 H2 H3). + forall (a b:R) (f:R -> R) (pr:derivable f), + a < b -> + (forall t:R, a < t < b -> 0 <= derive_pt f t (pr t)) -> + forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x <= f y. +Proof. + intros a b f pr H H0 x y H1 H2 H3; + generalize (derive_increasing_interv_ax a b f pr H); + intro; elim H4; intros _ H5; apply (H5 H0 x y H1 H2 H3). Qed. (**********) (**********) Theorem IAF : - forall (f:R -> R) (a b k:R) (pr:derivable f), - a <= b -> - (forall c:R, a <= c <= b -> derive_pt f c (pr c) <= k) -> - f b - f a <= k * (b - a). -intros. -case (total_order_T a b); intro. -elim s; intro. -assert (H1 := MVT_cor1 f _ _ pr a0). -elim H1; intros. -elim H2; intros. -rewrite H3. -do 2 rewrite <- (Rmult_comm (b - a)). -apply Rmult_le_compat_l. -apply Rplus_le_reg_l with a; rewrite Rplus_0_r. -replace (a + (b - a)) with b; [ assumption | ring ]. -apply H0. -elim H4; intros. -split; left; assumption. -rewrite b0. -unfold Rminus in |- *; do 2 rewrite Rplus_opp_r. -rewrite Rmult_0_r; right; reflexivity. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). + forall (f:R -> R) (a b k:R) (pr:derivable f), + a <= b -> + (forall c:R, a <= c <= b -> derive_pt f c (pr c) <= k) -> + f b - f a <= k * (b - a). +Proof. + intros. + case (total_order_T a b); intro. + elim s; intro. + assert (H1 := MVT_cor1 f _ _ pr a0). + elim H1; intros. + elim H2; intros. + rewrite H3. + do 2 rewrite <- (Rmult_comm (b - a)). + apply Rmult_le_compat_l. + apply Rplus_le_reg_l with a; rewrite Rplus_0_r. + replace (a + (b - a)) with b; [ assumption | ring ]. + apply H0. + elim H4; intros. + split; left; assumption. + rewrite b0. + unfold Rminus in |- *; do 2 rewrite Rplus_opp_r. + rewrite Rmult_0_r; right; reflexivity. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). Qed. Lemma IAF_var : - forall (f g:R -> R) (a b:R) (pr1:derivable f) (pr2:derivable g), - a <= b -> - (forall c:R, a <= c <= b -> derive_pt g c (pr2 c) <= derive_pt f c (pr1 c)) -> - g b - g a <= f b - f a. -intros. -cut (derivable (g - f)). -intro X. -cut (forall c:R, a <= c <= b -> derive_pt (g - f) c (X c) <= 0). -intro. -assert (H2 := IAF (g - f)%F a b 0 X H H1). -rewrite Rmult_0_l in H2; unfold minus_fct in H2. -apply Rplus_le_reg_l with (- f b + f a). -replace (- f b + f a + (f b - f a)) with 0; [ idtac | ring ]. -replace (- f b + f a + (g b - g a)) with (g b - f b - (g a - f a)); - [ apply H2 | ring ]. -intros. -cut - (derive_pt (g - f) c (X c) = - derive_pt (g - f) c (derivable_pt_minus _ _ _ (pr2 c) (pr1 c))). -intro. -rewrite H2. -rewrite derive_pt_minus. -apply Rplus_le_reg_l with (derive_pt f c (pr1 c)). -rewrite Rplus_0_r. -replace - (derive_pt f c (pr1 c) + (derive_pt g c (pr2 c) - derive_pt f c (pr1 c))) - with (derive_pt g c (pr2 c)); [ idtac | ring ]. -apply H0; assumption. -apply pr_nu. -apply derivable_minus; assumption. + forall (f g:R -> R) (a b:R) (pr1:derivable f) (pr2:derivable g), + a <= b -> + (forall c:R, a <= c <= b -> derive_pt g c (pr2 c) <= derive_pt f c (pr1 c)) -> + g b - g a <= f b - f a. +Proof. + intros. + cut (derivable (g - f)). + intro X. + cut (forall c:R, a <= c <= b -> derive_pt (g - f) c (X c) <= 0). + intro. + assert (H2 := IAF (g - f)%F a b 0 X H H1). + rewrite Rmult_0_l in H2; unfold minus_fct in H2. + apply Rplus_le_reg_l with (- f b + f a). + replace (- f b + f a + (f b - f a)) with 0; [ idtac | ring ]. + replace (- f b + f a + (g b - g a)) with (g b - f b - (g a - f a)); + [ apply H2 | ring ]. + intros. + cut + (derive_pt (g - f) c (X c) = + derive_pt (g - f) c (derivable_pt_minus _ _ _ (pr2 c) (pr1 c))). + intro. + rewrite H2. + rewrite derive_pt_minus. + apply Rplus_le_reg_l with (derive_pt f c (pr1 c)). + rewrite Rplus_0_r. + replace + (derive_pt f c (pr1 c) + (derive_pt g c (pr2 c) - derive_pt f c (pr1 c))) + with (derive_pt g c (pr2 c)); [ idtac | ring ]. + apply H0; assumption. + apply pr_nu. + apply derivable_minus; assumption. Qed. (* If f has a null derivative in ]a,b[ and is continue in [a,b], *) (* then f is constant on [a,b] *) Lemma null_derivative_loc : - forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x), - (forall x:R, a <= x <= b -> continuity_pt f x) -> - (forall (x:R) (P:a < x < b), derive_pt f x (pr x P) = 0) -> - constant_D_eq f (fun x:R => a <= x <= b) (f a). -intros; unfold constant_D_eq in |- *; intros; case (total_order_T a b); intro. -elim s; intro. -assert (H2 : forall y:R, a < y < x -> derivable_pt id y). -intros; apply derivable_pt_id. -assert (H3 : forall y:R, a <= y <= x -> continuity_pt id y). -intros; apply derivable_continuous; apply derivable_id. -assert (H4 : forall y:R, a < y < x -> derivable_pt f y). -intros; apply pr; elim H4; intros; split. -assumption. -elim H1; intros; apply Rlt_le_trans with x; assumption. -assert (H5 : forall y:R, a <= y <= x -> continuity_pt f y). -intros; apply H; elim H5; intros; split. -assumption. -elim H1; intros; apply Rle_trans with x; assumption. -elim H1; clear H1; intros; elim H1; clear H1; intro. -assert (H7 := MVT f id a x H4 H2 H1 H5 H3). -elim H7; intros; elim H8; intros; assert (H10 : a < x0 < b). -elim x1; intros; split. -assumption. -apply Rlt_le_trans with x; assumption. -assert (H11 : derive_pt f x0 (H4 x0 x1) = 0). -replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10)); - [ apply H0 | apply pr_nu ]. -assert (H12 : derive_pt id x0 (H2 x0 x1) = 1). -apply derive_pt_eq_0; apply derivable_pt_lim_id. -rewrite H11 in H9; rewrite H12 in H9; rewrite Rmult_0_r in H9; - rewrite Rmult_1_r in H9; apply Rminus_diag_uniq; symmetry in |- *; - assumption. -rewrite H1; reflexivity. -assert (H2 : x = a). -rewrite <- b0 in H1; elim H1; intros; apply Rle_antisym; assumption. -rewrite H2; reflexivity. -elim H1; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H2 H3) r)). + forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x), + (forall x:R, a <= x <= b -> continuity_pt f x) -> + (forall (x:R) (P:a < x < b), derive_pt f x (pr x P) = 0) -> + constant_D_eq f (fun x:R => a <= x <= b) (f a). +Proof. + intros; unfold constant_D_eq in |- *; intros; case (total_order_T a b); intro. + elim s; intro. + assert (H2 : forall y:R, a < y < x -> derivable_pt id y). + intros; apply derivable_pt_id. + assert (H3 : forall y:R, a <= y <= x -> continuity_pt id y). + intros; apply derivable_continuous; apply derivable_id. + assert (H4 : forall y:R, a < y < x -> derivable_pt f y). + intros; apply pr; elim H4; intros; split. + assumption. + elim H1; intros; apply Rlt_le_trans with x; assumption. + assert (H5 : forall y:R, a <= y <= x -> continuity_pt f y). + intros; apply H; elim H5; intros; split. + assumption. + elim H1; intros; apply Rle_trans with x; assumption. + elim H1; clear H1; intros; elim H1; clear H1; intro. + assert (H7 := MVT f id a x H4 H2 H1 H5 H3). + elim H7; intros; elim H8; intros; assert (H10 : a < x0 < b). + elim x1; intros; split. + assumption. + apply Rlt_le_trans with x; assumption. + assert (H11 : derive_pt f x0 (H4 x0 x1) = 0). + replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10)); + [ apply H0 | apply pr_nu ]. + assert (H12 : derive_pt id x0 (H2 x0 x1) = 1). + apply derive_pt_eq_0; apply derivable_pt_lim_id. + rewrite H11 in H9; rewrite H12 in H9; rewrite Rmult_0_r in H9; + rewrite Rmult_1_r in H9; apply Rminus_diag_uniq; symmetry in |- *; + assumption. + rewrite H1; reflexivity. + assert (H2 : x = a). + rewrite <- b0 in H1; elim H1; intros; apply Rle_antisym; assumption. + rewrite H2; reflexivity. + elim H1; intros; + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H2 H3) r)). Qed. (* Unicity of the antiderivative *) Lemma antiderivative_Ucte : - forall (f g1 g2:R -> R) (a b:R), - antiderivative f g1 a b -> - antiderivative f g2 a b -> + forall (f g1 g2:R -> R) (a b:R), + antiderivative f g1 a b -> + antiderivative f g2 a b -> exists c : R, (forall x:R, a <= x <= b -> g1 x = g2 x + c). -unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0; - clear H0; intros H0 _; exists (g1 a - g2 a); intros; - assert (H3 : forall x:R, a <= x <= b -> derivable_pt g1 x). -intros; unfold derivable_pt in |- *; apply existT with (f x0); elim (H x0 H3); - intros; eapply derive_pt_eq_1; symmetry in |- *; - apply H4. -assert (H4 : forall x:R, a <= x <= b -> derivable_pt g2 x). -intros; unfold derivable_pt in |- *; apply existT with (f x0); - elim (H0 x0 H4); intros; eapply derive_pt_eq_1; symmetry in |- *; - apply H5. -assert (H5 : forall x:R, a < x < b -> derivable_pt (g1 - g2) x). -intros; elim H5; intros; apply derivable_pt_minus; - [ apply H3; split; left; assumption | apply H4; split; left; assumption ]. -assert (H6 : forall x:R, a <= x <= b -> continuity_pt (g1 - g2) x). -intros; apply derivable_continuous_pt; apply derivable_pt_minus; - [ apply H3 | apply H4 ]; assumption. -assert (H7 : forall (x:R) (P:a < x < b), derive_pt (g1 - g2) x (H5 x P) = 0). -intros; elim P; intros; apply derive_pt_eq_0; replace 0 with (f x0 - f x0); - [ idtac | ring ]. -assert (H9 : a <= x0 <= b). -split; left; assumption. -apply derivable_pt_lim_minus; [ elim (H _ H9) | elim (H0 _ H9) ]; intros; - eapply derive_pt_eq_1; symmetry in |- *; apply H10. -assert (H8 := null_derivative_loc (g1 - g2)%F a b H5 H6 H7); - unfold constant_D_eq in H8; assert (H9 := H8 _ H2); - unfold minus_fct in H9; rewrite <- H9; ring. +Proof. + unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0; + clear H0; intros H0 _; exists (g1 a - g2 a); intros; + assert (H3 : forall x:R, a <= x <= b -> derivable_pt g1 x). + intros; unfold derivable_pt in |- *; apply existT with (f x0); elim (H x0 H3); + intros; eapply derive_pt_eq_1; symmetry in |- *; + apply H4. + assert (H4 : forall x:R, a <= x <= b -> derivable_pt g2 x). + intros; unfold derivable_pt in |- *; apply existT with (f x0); + elim (H0 x0 H4); intros; eapply derive_pt_eq_1; symmetry in |- *; + apply H5. + assert (H5 : forall x:R, a < x < b -> derivable_pt (g1 - g2) x). + intros; elim H5; intros; apply derivable_pt_minus; + [ apply H3; split; left; assumption | apply H4; split; left; assumption ]. + assert (H6 : forall x:R, a <= x <= b -> continuity_pt (g1 - g2) x). + intros; apply derivable_continuous_pt; apply derivable_pt_minus; + [ apply H3 | apply H4 ]; assumption. + assert (H7 : forall (x:R) (P:a < x < b), derive_pt (g1 - g2) x (H5 x P) = 0). + intros; elim P; intros; apply derive_pt_eq_0; replace 0 with (f x0 - f x0); + [ idtac | ring ]. + assert (H9 : a <= x0 <= b). + split; left; assumption. + apply derivable_pt_lim_minus; [ elim (H _ H9) | elim (H0 _ H9) ]; intros; + eapply derive_pt_eq_1; symmetry in |- *; apply H10. + assert (H8 := null_derivative_loc (g1 - g2)%F a b H5 H6 H7); + unfold constant_D_eq in H8; assert (H9 := H8 _ H2); + unfold minus_fct in H9; rewrite <- H9; ring. Qed. |