diff options
Diffstat (limited to 'theories/Reals/Ranalysis4.v')
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 108 |
1 files changed, 53 insertions, 55 deletions
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index a7c5a387..00c07592 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -1,21 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(*i $Id: Ranalysis4.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. -Require Import Rtrigo. +Require Import Rtrigo1. Require Import Ranalysis1. Require Import Ranalysis3. Require Import Exp_prop. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma derivable_pt_inv : @@ -28,12 +26,12 @@ Proof. apply derivable_pt_const. assumption. assumption. - unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros; - unfold derivable_pt in |- *; exists x0; - unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; + unfold div_fct, inv_fct, fct_cte; intro X0; elim X0; intros; + unfold derivable_pt; exists x0; + unfold derivable_pt_abs; unfold derivable_pt_lim; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; intros; elim (p eps H0); intros; exists x1; intros; - unfold Rdiv in H1; unfold Rdiv in |- *; rewrite <- (Rmult_1_l (/ f x)); + unfold Rdiv in H1; unfold Rdiv; rewrite <- (Rmult_1_l (/ f x)); rewrite <- (Rmult_1_l (/ f (x + h))). apply H1; assumption. Qed. @@ -43,10 +41,10 @@ Lemma pr_nu_var : forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x), f = g -> derive_pt f x pr1 = derive_pt g x pr2. Proof. - unfold derivable_pt, derive_pt in |- *; intros. + unfold derivable_pt, derive_pt; intros. elim pr1; intros. elim pr2; intros. - simpl in |- *. + simpl. rewrite H in p. apply uniqueness_limite with g x; assumption. Qed. @@ -56,17 +54,17 @@ Lemma pr_nu_var2 : forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x), (forall h:R, f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2. Proof. - unfold derivable_pt, derive_pt in |- *; intros. + unfold derivable_pt, derive_pt; intros. elim pr1; intros. elim pr2; intros. - simpl in |- *. + simpl. assert (H0 := uniqueness_step2 _ _ _ p). assert (H1 := uniqueness_step2 _ _ _ p0). cut (limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) x1 0). intro; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2). assumption. - unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *; - simpl in |- *; unfold R_dist in |- *; unfold limit1_in in H1; + unfold limit1_in; unfold limit_in; unfold dist; + simpl; unfold R_dist; unfold limit1_in in H1; unfold limit_in in H1; unfold dist in H1; simpl in H1; unfold R_dist in H1. intros; elim (H1 eps H2); intros. @@ -82,7 +80,7 @@ Lemma derivable_inv : forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f). Proof. intros f H X. - unfold derivable in |- *; intro x. + unfold derivable; intro x. apply derivable_pt_inv. apply (H x). apply (X x). @@ -97,25 +95,25 @@ Proof. replace (derive_pt (/ f) x (derivable_pt_inv f x na pr)) with (derive_pt (fct_cte 1 / f) x (derivable_pt_div (fct_cte 1) f x (derivable_pt_const 1 x) pr na)). - rewrite derive_pt_div; rewrite derive_pt_const; unfold fct_cte in |- *; - rewrite Rmult_0_l; rewrite Rmult_1_r; unfold Rminus in |- *; + rewrite derive_pt_div; rewrite derive_pt_const; unfold fct_cte; + rewrite Rmult_0_l; rewrite Rmult_1_r; unfold Rminus; rewrite Rplus_0_l; reflexivity. apply pr_nu_var2. - intro; unfold div_fct, fct_cte, inv_fct in |- *. - unfold Rdiv in |- *; ring. + intro; unfold div_fct, fct_cte, inv_fct. + unfold Rdiv; ring. Qed. (** Rabsolu *) Lemma Rabs_derive_1 : forall x:R, 0 < x -> derivable_pt_lim Rabs x 1. Proof. intros. - unfold derivable_pt_lim in |- *; intros. + unfold derivable_pt_lim; intros. exists (mkposreal x H); intros. rewrite (Rabs_right x). rewrite (Rabs_right (x + h)). rewrite Rplus_comm. - unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_r. - rewrite Rplus_0_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym. + unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r. + rewrite Rplus_0_r; unfold Rdiv; rewrite <- Rinv_r_sym. rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. apply H1. apply Rle_ge. @@ -133,16 +131,16 @@ Qed. Lemma Rabs_derive_2 : forall x:R, x < 0 -> derivable_pt_lim Rabs x (-1). Proof. intros. - unfold derivable_pt_lim in |- *; intros. + unfold derivable_pt_lim; intros. cut (0 < - x). intro; exists (mkposreal (- x) H1); intros. rewrite (Rabs_left x). rewrite (Rabs_left (x + h)). rewrite Rplus_comm. rewrite Ropp_plus_distr. - unfold Rminus in |- *; rewrite Ropp_involutive; rewrite Rplus_assoc; + unfold Rminus; rewrite Ropp_involutive; rewrite Rplus_assoc; rewrite Rplus_opp_l. - rewrite Rplus_0_r; unfold Rdiv in |- *. + rewrite Rplus_0_r; unfold Rdiv. rewrite Ropp_mult_distr_l_reverse. rewrite <- Rinv_r_sym. rewrite Ropp_involutive; rewrite Rplus_opp_l; rewrite Rabs_R0; apply H0. @@ -165,24 +163,24 @@ Proof. intros. case (total_order_T x 0); intro. elim s; intro. - unfold derivable_pt in |- *; exists (-1). + unfold derivable_pt; exists (-1). apply (Rabs_derive_2 x a). elim H; exact b. - unfold derivable_pt in |- *; exists 1. + unfold derivable_pt; exists 1. apply (Rabs_derive_1 x r). Qed. (** Rabsolu is continuous for all x *) Lemma Rcontinuity_abs : continuity Rabs. Proof. - unfold continuity in |- *; intro. + unfold continuity; intro. case (Req_dec x 0); intro. - unfold continuity_pt in |- *; unfold continue_in in |- *; - unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; unfold R_dist in |- *; intros; exists eps; + unfold continuity_pt; unfold continue_in; + unfold limit1_in; unfold limit_in; + simpl; unfold R_dist; intros; exists eps; split. apply H0. - intros; rewrite H; rewrite Rabs_R0; unfold Rminus in |- *; rewrite Ropp_0; + intros; rewrite H; rewrite Rabs_R0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; elim H1; intros; rewrite H in H3; unfold Rminus in H3; rewrite Ropp_0 in H3; rewrite Rplus_0_r in H3; apply H3. @@ -194,11 +192,11 @@ Lemma continuity_finite_sum : forall (An:nat -> R) (N:nat), continuity (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N). Proof. - intros; unfold continuity in |- *; intro. + intros; unfold continuity; intro. induction N as [| N HrecN]. - simpl in |- *. + simpl. apply continuity_pt_const. - unfold constant in |- *; intros; reflexivity. + unfold constant; intros; reflexivity. replace (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with ((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) + (fun y:R => (An (S N) * y ^ S N)%R))%F. @@ -224,7 +222,7 @@ Proof. cut (N = 0%nat \/ (0 < N)%nat). intro; elim H0; intro. rewrite H1. - simpl in |- *. + simpl. replace (fun y:R => An 0%nat * 1 + An 1%nat * (y * 1)) with (fct_cte (An 0%nat * 1) + mult_real_fct (An 1%nat) (id * fct_cte 1))%F. replace (1 * An 1%nat * 1) with (0 + An 1%nat * (1 * fct_cte 1 x + id x * 0)). @@ -234,7 +232,7 @@ Proof. apply derivable_pt_lim_mult. apply derivable_pt_lim_id. apply derivable_pt_lim_const. - unfold fct_cte, id in |- *; ring. + unfold fct_cte, id; ring. reflexivity. replace (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with ((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) + @@ -250,7 +248,7 @@ Proof. (mult_real_fct (An (S N)) (fun y:R => y ^ S N)). apply derivable_pt_lim_scal. replace (pred (S N)) with N; [ idtac | reflexivity ]. - pattern N at 3 in |- *; replace N with (pred (S N)). + pattern N at 3; replace N with (pred (S N)). apply derivable_pt_lim_pow. reflexivity. reflexivity. @@ -261,10 +259,10 @@ Proof. rewrite <- H2. replace (pred (S N)) with N; [ idtac | reflexivity ]. ring. - simpl in |- *. + simpl. apply S_pred with 0%nat; assumption. - unfold plus_fct in |- *. - simpl in |- *; reflexivity. + unfold plus_fct. + simpl; reflexivity. inversion H. left; reflexivity. right; apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ]. @@ -280,7 +278,7 @@ Lemma derivable_pt_lim_finite_sum : Proof. intros. induction N as [| N HrecN]. - simpl in |- *. + simpl. rewrite Rmult_1_r. replace (fun _:R => An 0%nat) with (fct_cte (An 0%nat)); [ apply derivable_pt_lim_const | reflexivity ]. @@ -292,7 +290,7 @@ Lemma derivable_pt_finite_sum : derivable_pt (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x. Proof. intros. - unfold derivable_pt in |- *. + unfold derivable_pt. assert (H := derivable_pt_lim_finite_sum An x N). induction N as [| N HrecN]. exists 0; apply H. @@ -305,14 +303,14 @@ Lemma derivable_finite_sum : forall (An:nat -> R) (N:nat), derivable (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N). Proof. - intros; unfold derivable in |- *; intro; apply derivable_pt_finite_sum. + intros; unfold derivable; intro; apply derivable_pt_finite_sum. Qed. (** Regularity of hyperbolic functions *) Lemma derivable_pt_lim_cosh : forall x:R, derivable_pt_lim cosh x (sinh x). Proof. intro. - unfold cosh, sinh in |- *; unfold Rdiv in |- *. + unfold cosh, sinh; unfold Rdiv. replace (fun x0:R => (exp x0 + exp (- x0)) * / 2) with ((exp + comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ]. replace ((exp x - exp (- x)) * / 2) with @@ -326,13 +324,13 @@ Proof. apply derivable_pt_lim_id. apply derivable_pt_lim_exp. apply derivable_pt_lim_const. - unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte in |- *; ring. + unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte; ring. Qed. Lemma derivable_pt_lim_sinh : forall x:R, derivable_pt_lim sinh x (cosh x). Proof. intro. - unfold cosh, sinh in |- *; unfold Rdiv in |- *. + unfold cosh, sinh; unfold Rdiv. replace (fun x0:R => (exp x0 - exp (- x0)) * / 2) with ((exp - comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ]. replace ((exp x + exp (- x)) * / 2) with @@ -346,13 +344,13 @@ Proof. apply derivable_pt_lim_id. apply derivable_pt_lim_exp. apply derivable_pt_lim_const. - unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte in |- *; ring. + unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte; ring. Qed. Lemma derivable_pt_exp : forall x:R, derivable_pt exp x. Proof. intro. - unfold derivable_pt in |- *. + unfold derivable_pt. exists (exp x). apply derivable_pt_lim_exp. Qed. @@ -360,7 +358,7 @@ Qed. Lemma derivable_pt_cosh : forall x:R, derivable_pt cosh x. Proof. intro. - unfold derivable_pt in |- *. + unfold derivable_pt. exists (sinh x). apply derivable_pt_lim_cosh. Qed. @@ -368,24 +366,24 @@ Qed. Lemma derivable_pt_sinh : forall x:R, derivable_pt sinh x. Proof. intro. - unfold derivable_pt in |- *. + unfold derivable_pt. exists (cosh x). apply derivable_pt_lim_sinh. Qed. Lemma derivable_exp : derivable exp. Proof. - unfold derivable in |- *; apply derivable_pt_exp. + unfold derivable; apply derivable_pt_exp. Qed. Lemma derivable_cosh : derivable cosh. Proof. - unfold derivable in |- *; apply derivable_pt_cosh. + unfold derivable; apply derivable_pt_cosh. Qed. Lemma derivable_sinh : derivable sinh. Proof. - unfold derivable in |- *; apply derivable_pt_sinh. + unfold derivable; apply derivable_pt_sinh. Qed. Lemma derive_pt_exp : |