diff options
Diffstat (limited to 'theories/Reals/Rderiv.v')
| -rw-r--r-- | theories/Reals/Rderiv.v | 114 |
1 files changed, 57 insertions, 57 deletions
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 105d8347..e714f5f8 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,7 @@ Require Import Rfunctions. Require Import Rlimit. Require Import Fourier. Require Import Omega. -Open Local Scope R_scope. +Local Open Scope R_scope. (*********) Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x. @@ -34,18 +34,18 @@ Lemma cont_deriv : forall (f d:R -> R) (D:R -> Prop) (x0:R), D_in f d D x0 -> continue_in f D x0. Proof. - unfold continue_in in |- *; unfold D_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; unfold Rdiv in |- *; simpl in |- *; + unfold continue_in; unfold D_in; unfold limit1_in; + unfold limit_in; unfold Rdiv; simpl; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; elim (Req_dec (d x0) 0); intro. split with (Rmin 1 x); split. elim (Rmin_Rgt 1 x 0); intros a b; apply (b (conj Rlt_0_1 H)). intros; elim H3; clear H3; intros; generalize (let (H1, H2) := Rmin_Rgt 1 x (R_dist x1 x0) in H1); - unfold Rgt in |- *; intro; elim (H5 H4); clear H5; + unfold Rgt; intro; elim (H5 H4); clear H5; intros; generalize (H1 x1 (conj H3 H6)); clear H1; intro; unfold D_x in H3; elim H3; intros. - rewrite H2 in H1; unfold R_dist in |- *; unfold R_dist in H1; + rewrite H2 in H1; unfold R_dist; unfold R_dist in H1; cut (Rabs (f x1 - f x0) < eps * Rabs (x1 - x0)). intro; unfold R_dist in H5; generalize (Rmult_lt_compat_l eps (Rabs (x1 - x0)) 1 H0 H5); @@ -68,7 +68,7 @@ Proof. intros; elim (Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) 0); intros a b; apply (b (conj H4 H3)). apply Rmult_gt_0_compat; auto. - unfold Rgt in |- *; apply Rinv_0_lt_compat; apply Rabs_pos_lt; + unfold Rgt; apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply Rmult_integral_contrapositive; split. discrR. assumption. @@ -80,17 +80,17 @@ Proof. generalize (let (H1, H2) := Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) (R_dist x1 x0) in - H1); unfold Rgt in |- *; intro; elim (H5 H4); clear H5; + H1); unfold Rgt; intro; elim (H5 H4); clear H5; intros; generalize (let (H1, H2) := Rmin_Rgt (/ 2) x (R_dist x1 x0) in H1); - unfold Rgt in |- *; intro; elim (H7 H5); clear H7; + unfold Rgt; intro; elim (H7 H5); clear H7; intros; clear H4 H5; generalize (H1 x1 (conj H3 H8)); clear H1; intro; unfold D_x in H3; elim H3; intros; - generalize (sym_not_eq H5); clear H5; intro H5; + generalize (not_eq_sym H5); clear H5; intro H5; generalize (Rminus_eq_contra x1 x0 H5); intro; generalize H1; - pattern (d x0) at 1 in |- *; + pattern (d x0) at 1; rewrite <- (let (H1, H2) := Rmult_ne (d x0) in H2); - rewrite <- (Rinv_l (x1 - x0) H9); unfold R_dist in |- *; - unfold Rminus at 1 in |- *; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))); + rewrite <- (Rinv_l (x1 - x0) H9); unfold R_dist; + unfold Rminus at 1; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))); rewrite (Rmult_comm (/ (x1 - x0) * (x1 - x0)) (d x0)); rewrite <- (Ropp_mult_distr_l_reverse (d x0) (/ (x1 - x0) * (x1 - x0))); rewrite (Rmult_comm (- d x0) (/ (x1 - x0) * (x1 - x0))); @@ -113,7 +113,7 @@ Proof. ; generalize (Rabs_triang_inv (f x1 - f x0) ((x1 - x0) * d x0)); intro; rewrite (Rmult_comm (x1 - x0) (- d x0)); rewrite (Ropp_mult_distr_l_reverse (d x0) (x1 - x0)); - fold (f x1 - f x0 - d x0 * (x1 - x0)) in |- *; + fold (f x1 - f x0 - d x0 * (x1 - x0)); rewrite (Rmult_comm (x1 - x0) (d x0)) in H10; clear H1; intro; generalize @@ -123,7 +123,7 @@ Proof. generalize (Rplus_lt_compat_l (Rabs (d x0 * (x1 - x0))) (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0))) ( - Rabs (x1 - x0) * eps) H1); unfold Rminus at 2 in |- *; + Rabs (x1 - x0) * eps) H1); unfold Rminus at 2; rewrite (Rplus_comm (Rabs (f x1 - f x0)) (- Rabs (d x0 * (x1 - x0)))); rewrite <- (Rplus_assoc (Rabs (d x0 * (x1 - x0))) (- Rabs (d x0 * (x1 - x0))) @@ -162,7 +162,7 @@ Proof. (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2) (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro; rewrite eps2 in H10; assumption. - unfold Rabs in |- *; case (Rcase_abs 2); auto. + unfold Rabs; case (Rcase_abs 2); auto. intro; cut (0 < 2). intro ; elim (Rlt_asym 0 2 H7 r). fourier. @@ -174,14 +174,14 @@ Qed. Lemma Dconst : forall (D:R -> Prop) (y x0:R), D_in (fun x:R => y) (fun x:R => 0) D x0. Proof. - unfold D_in in |- *; intros; unfold limit1_in in |- *; - unfold limit_in in |- *; unfold Rdiv in |- *; intros; - simpl in |- *; split with eps; split; auto. - intros; rewrite (Rminus_diag_eq y y (refl_equal y)); rewrite Rmult_0_l; - unfold R_dist in |- *; rewrite (Rminus_diag_eq 0 0 (refl_equal 0)); - unfold Rabs in |- *; case (Rcase_abs 0); intro. + unfold D_in; intros; unfold limit1_in; + unfold limit_in; unfold Rdiv; intros; + simpl; split with eps; split; auto. + intros; rewrite (Rminus_diag_eq y y (eq_refl y)); rewrite Rmult_0_l; + unfold R_dist; rewrite (Rminus_diag_eq 0 0 (eq_refl 0)); + unfold Rabs; case (Rcase_abs 0); intro. absurd (0 < 0); auto. - red in |- *; intro; apply (Rlt_irrefl 0 H1). + red; intro; apply (Rlt_irrefl 0 H1). unfold Rgt in H0; assumption. Qed. @@ -189,15 +189,15 @@ Qed. Lemma Dx : forall (D:R -> Prop) (x0:R), D_in (fun x:R => x) (fun x:R => 1) D x0. Proof. - unfold D_in in |- *; unfold Rdiv in |- *; intros; unfold limit1_in in |- *; - unfold limit_in in |- *; intros; simpl in |- *; split with eps; + unfold D_in; unfold Rdiv; intros; unfold limit1_in; + unfold limit_in; intros; simpl; split with eps; split; auto. intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros; - rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3))); - unfold R_dist in |- *; rewrite (Rminus_diag_eq 1 1 (refl_equal 1)); - unfold Rabs in |- *; case (Rcase_abs 0); intro. + rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (not_eq_sym H3))); + unfold R_dist; rewrite (Rminus_diag_eq 1 1 (eq_refl 1)); + unfold Rabs; case (Rcase_abs 0); intro. absurd (0 < 0); auto. - red in |- *; intro; apply (Rlt_irrefl 0 r). + red; intro; apply (Rlt_irrefl 0 r). unfold Rgt in H; assumption. Qed. @@ -208,12 +208,12 @@ Lemma Dadd : D_in g dg D x0 -> D_in (fun x:R => f x + g x) (fun x:R => df x + dg x) D x0. Proof. - unfold D_in in |- *; intros; + unfold D_in; intros; generalize (limit_plus (fun x:R => (f x - f x0) * / (x - x0)) (fun x:R => (g x - g x0) * / (x - x0)) (D_x D x0) ( - df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0); + df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in; + unfold limit_in; simpl; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; split with x; split; auto; intros; generalize (H1 x1 H2); clear H1; intro; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1; @@ -233,8 +233,8 @@ Lemma Dmult : D_in g dg D x0 -> D_in (fun x:R => f x * g x) (fun x:R => df x * g x + f x * dg x) D x0. Proof. - intros; unfold D_in in |- *; generalize H H0; intros; unfold D_in in H, H0; - generalize (cont_deriv f df D x0 H1); unfold continue_in in |- *; + intros; unfold D_in; generalize H H0; intros; unfold D_in in H, H0; + generalize (cont_deriv f df D x0 H1); unfold continue_in; intro; generalize (limit_mul (fun x:R => (g x - g x0) * / (x - x0)) ( @@ -250,8 +250,8 @@ Proof. (fun x:R => (g x - g x0) * / (x - x0) * f x) ( D_x D x0) (df x0 * g x0) (dg x0 * f x0) x0 H H4); clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H; - simpl in H; unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; intros; elim (H eps H0); clear H; intros; + simpl in H; unfold limit1_in; unfold limit_in; + simpl; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; split with x; split; auto; intros; generalize (H1 x1 H2); clear H1; intro; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1; @@ -268,9 +268,9 @@ Proof. ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1 = f x1 * g x1 - f x0 * g x0). intro; rewrite H3 in H1; assumption. ring. - unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; + unfold limit1_in; unfold limit_in; simpl; intros; split with eps; split; auto; intros; elim (R_dist_refl (g x0) (g x0)); - intros a b; rewrite (b (refl_equal (g x0))); unfold Rgt in H; + intros a b; rewrite (b (eq_refl (g x0))); unfold Rgt in H; assumption. Qed. @@ -281,7 +281,7 @@ Lemma Dmult_const : Proof. intros; generalize (Dmult D (fun _:R => 0) df (fun _:R => a) f x0 (Dconst D a x0) H); - unfold D_in in |- *; intros; rewrite (Rmult_0_l (f x0)) in H0; + unfold D_in; intros; rewrite (Rmult_0_l (f x0)) in H0; rewrite (let (H1, H2) := Rplus_ne (a * df x0) in H2) in H0; assumption. Qed. @@ -291,10 +291,10 @@ Lemma Dopp : forall (D:R -> Prop) (f df:R -> R) (x0:R), D_in f df D x0 -> D_in (fun x:R => - f x) (fun x:R => - df x) D x0. Proof. - intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in in |- *; - unfold limit1_in in |- *; unfold limit_in in |- *; + intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in; + unfold limit1_in; unfold limit_in; intros; generalize (H0 eps H1); clear H0; intro; elim H0; - clear H0; intros; elim H0; clear H0; simpl in |- *; + clear H0; intros; elim H0; clear H0; simpl; intros; split with x; split; auto. intros; generalize (H2 x1 H3); clear H2; intro; rewrite Ropp_mult_distr_l_reverse in H2; @@ -313,7 +313,7 @@ Lemma Dminus : D_in g dg D x0 -> D_in (fun x:R => f x - g x) (fun x:R => df x - dg x) D x0. Proof. - unfold Rminus in |- *; intros; generalize (Dopp D g dg x0 H0); intro; + unfold Rminus; intros; generalize (Dopp D g dg x0 H0); intro; apply (Dadd D df (fun x:R => - dg x) f (fun x:R => - g x) x0); assumption. Qed. @@ -324,14 +324,14 @@ Lemma Dx_pow_n : D_in (fun x:R => x ^ n) (fun x:R => INR n * x ^ (n - 1)) D x0. Proof. simple induction n; intros. - simpl in |- *; rewrite Rmult_0_l; apply Dconst. + simpl; rewrite Rmult_0_l; apply Dconst. intros; cut (n0 = (S n0 - 1)%nat); - [ intro a; rewrite <- a; clear a | simpl in |- *; apply minus_n_O ]. + [ intro a; rewrite <- a; clear a | simpl; apply minus_n_O ]. generalize (Dmult D (fun _:R => 1) (fun x:R => INR n0 * x ^ (n0 - 1)) ( fun x:R => x) (fun x:R => x ^ n0) x0 (Dx D x0) ( - H D x0)); unfold D_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; intros; elim (H0 eps H1); + H D x0)); unfold D_in; unfold limit1_in; + unfold limit_in; simpl; intros; elim (H0 eps H1); clear H0; intros; elim H0; clear H0; intros; split with x; split; auto. intros; generalize (H2 x1 H3); clear H2 H3; intro; @@ -340,7 +340,7 @@ Proof. rewrite (Rmult_comm (INR n0) (x0 ^ (n0 - 1))) in H2; rewrite <- (Rmult_assoc x0 (x0 ^ (n0 - 1)) (INR n0)) in H2; rewrite (tech_pow_Rmult x0 (n0 - 1)) in H2; elim (Peano_dec.eq_nat_dec n0 0) ; intros cond. - rewrite cond in H2; rewrite cond; simpl in H2; simpl in |- *; + rewrite cond in H2; rewrite cond; simpl in H2; simpl; cut (1 + x0 * 1 * 0 = 1 * 1); [ intro A; rewrite A in H2; assumption | ring ]. cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ]; @@ -355,8 +355,8 @@ Lemma Dcomp : D_in g dg Dg (f x0) -> D_in (fun x:R => g (f x)) (fun x:R => df x * dg (f x)) (Dgf Df Dg f) x0. Proof. - intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in in |- *; - unfold Rdiv in |- *; intros; + intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in; + unfold Rdiv; intros; generalize (limit_comp f (fun x:R => (g x - g (f x0)) * / (x - f x0)) ( D_x Df x0) (D_x Dg (f x0)) (f x0) (dg (f x0)) x0); @@ -376,8 +376,8 @@ Proof. (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) ( fun x:R => dg (f x0)) (D_x Df x0) (df x0) (dg (f x0)) x0 H1 (limit_free (fun x:R => dg (f x0)) (D_x Df x0) x0 x0)); - intro; unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; unfold limit1_in in H5, H7; unfold limit_in in H5, H7; + intro; unfold limit1_in; unfold limit_in; + simpl; unfold limit1_in in H5, H7; unfold limit_in in H5, H7; simpl in H5, H7; intros; elim (H5 eps H8); elim (H7 eps H8); clear H5 H7; intros; elim H5; elim H7; clear H5 H7; intros; split with (Rmin x x1); split. @@ -391,7 +391,7 @@ Proof. rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16; rewrite (Rmult_0_l (/ (x2 - x0))) in H16; rewrite (Rmult_0_l (dg (f x0))) in H16; rewrite H12; - rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (refl_equal (g (f x0)))); + rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (eq_refl (g (f x0)))); rewrite (Rmult_0_l (/ (x2 - x0))); assumption. clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros; cut @@ -405,8 +405,8 @@ Proof. in H15; rewrite (Rinv_l (f x2 - f x0) H16) in H15; rewrite (let (H1, H2) := Rmult_ne (/ (x2 - x0)) in H2) in H15; rewrite (Rmult_comm (df x0) (dg (f x0))); assumption. - clear H5 H3 H4 H2; unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; unfold limit1_in in H1; unfold limit_in in H1; + clear H5 H3 H4 H2; unfold limit1_in; unfold limit_in; + simpl; unfold limit1_in in H1; unfold limit_in in H1; simpl in H1; intros; elim (H1 eps H2); clear H1; intros; elim H1; clear H1; intros; split with x; split; auto; intros; unfold D_x, Dgf in H4, H3; elim H4; clear H4; @@ -425,8 +425,8 @@ Proof. generalize (Dcomp D D dexpr (fun x:R => INR n * x ^ (n - 1)) expr ( fun x:R => x ^ n) x0 H (Dx_pow_n n D (expr x0))); - intro; unfold D_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; intros; unfold D_in in H0; + intro; unfold D_in; unfold limit1_in; + unfold limit_in; simpl; intros; unfold D_in in H0; unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; elim (H0 eps H1); clear H0; intros; elim H0; clear H0; intros; split with x; split; intros; auto. |