summaryrefslogtreecommitdiff
path: root/theories/Reals/Ranalysis4.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Ranalysis4.v')
-rw-r--r--theories/Reals/Ranalysis4.v108
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 :