diff options
Diffstat (limited to 'theories/Reals/MVT.v')
| -rw-r--r-- | theories/Reals/MVT.v | 699 |
1 files changed, 699 insertions, 0 deletions
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v new file mode 100644 index 00000000..baa61304 --- /dev/null +++ b/theories/Reals/MVT.v @@ -0,0 +1,699 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: MVT.v,v 1.10.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) + +Require Import Rbase. +Require Import Rfunctions. +Require Import Ranalysis1. +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) -> + exists c : R, + (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; 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). +(*** 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). +(*** 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). +Qed. + +(* Corollaries ... *) +Lemma MVT_cor1 : + 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 | intros; apply pr ]. +cut (forall c:R, a < c < b -> derivable_pt id c); + [ intro | 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)) -> + 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; cut (forall c:R, a < c < b -> derivable_pt f c). +intro; cut (forall c:R, a <= c <= b -> continuity_pt f c). +intro; cut (forall c:R, a <= c <= b -> derivable_pt id c). +intro; cut (forall c:R, a < c < b -> derivable_pt id c). +intro; 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)) -> + 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 ] ] ]. +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 -> + 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) ]. +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)). +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 ]. +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. +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. +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 ]. +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. +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. +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. +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)). +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). +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 ]. +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). +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). +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)). +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. +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)). +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 -> + 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. +Qed. |