diff options
Diffstat (limited to 'theories/Reals/Rlimit.v')
| -rw-r--r-- | theories/Reals/Rlimit.v | 106 |
1 files changed, 53 insertions, 53 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 5c864de3..c5ee828a 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.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 *) @@ -14,7 +14,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Fourier. -Open Local Scope R_scope. +Local Open Scope R_scope. (*******************************) (** * Calculus *) @@ -31,7 +31,7 @@ Proof. intro esp. assert (H := double_var esp). unfold Rdiv in H. - symmetry in |- *; exact H. + symmetry ; exact H. Qed. (*********) @@ -39,9 +39,9 @@ Lemma eps4 : forall eps:R, eps * / (2 + 2) + eps * / (2 + 2) = eps * / 2. Proof. intro eps. replace (2 + 2) with 4. - pattern eps at 3 in |- *; rewrite double_var. + pattern eps at 3; rewrite double_var. rewrite (Rmult_plus_distr_r (eps / 2) (eps / 2) (/ 2)). - unfold Rdiv in |- *. + unfold Rdiv. repeat rewrite Rmult_assoc. rewrite <- Rinv_mult_distr. reflexivity. @@ -54,7 +54,7 @@ Qed. Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - pattern eps at 2 in |- *; rewrite <- Rmult_1_r. + pattern eps at 2; rewrite <- Rmult_1_r. repeat rewrite (Rmult_comm eps). apply Rmult_lt_compat_r. exact H. @@ -70,7 +70,7 @@ Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. replace (2 + 2) with 4. - pattern eps at 2 in |- *; rewrite <- Rmult_1_r. + pattern eps at 2; rewrite <- Rmult_1_r. repeat rewrite (Rmult_comm eps). apply Rmult_lt_compat_r. exact H. @@ -113,10 +113,10 @@ Qed. (*********) Lemma mul_factor_gt : forall eps l l':R, eps > 0 -> eps * mul_factor l l' > 0. Proof. - intros; unfold Rgt in |- *; rewrite <- (Rmult_0_r eps); + intros; unfold Rgt; rewrite <- (Rmult_0_r eps); apply Rmult_lt_compat_l. assumption. - unfold mul_factor in |- *; apply Rinv_0_lt_compat; + unfold mul_factor; apply Rinv_0_lt_compat; cut (1 <= 1 + (Rabs l + Rabs l')). cut (0 < 1). exact (Rlt_le_trans _ _ _). @@ -196,7 +196,7 @@ Proof. case (H0 (dist R_met (f x0) l)); auto. intros alpha1 [H2 H3]; apply H3; auto; split; auto. case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto. - case (dist_refl R_met (f x0) l); intros Hr1 Hr2; apply sym_eq; auto. + case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto. Qed. (*********) @@ -210,7 +210,7 @@ Qed. (*********) Lemma lim_x : forall (D:R -> Prop) (x0:R), limit1_in (fun x:R => x) D x0 x0. Proof. - 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 H0; intros; auto. Qed. @@ -221,9 +221,9 @@ Lemma limit_plus : limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:R => f x + g x) D (l + l') x0. Proof. - intros; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; + intros; unfold limit1_in; unfold limit_in; simpl; intros; elim (H (eps * / 2) (eps2_Rgt_R0 eps H1)); - elim (H0 (eps * / 2) (eps2_Rgt_R0 eps H1)); simpl in |- *; + elim (H0 (eps * / 2) (eps2_Rgt_R0 eps H1)); simpl; clear H H0; intros; elim H; elim H0; clear H H0; intros; split with (Rmin x1 x); split. exact (Rmin_Rgt_r x1 x 0 (conj H H2)). @@ -244,12 +244,12 @@ Lemma limit_Ropp : forall (f:R -> R) (D:R -> Prop) (l x0:R), limit1_in f D l x0 -> limit1_in (fun x:R => - f x) D (- l) x0. Proof. - unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; + 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; unfold R_dist in |- *; unfold Rminus in |- *; + clear H1; intro; unfold R_dist; unfold Rminus; rewrite (Ropp_involutive l); rewrite (Rplus_comm (- f x1) l); - fold (l - f x1) in |- *; fold (R_dist l (f x1)) in |- *; + fold (l - f x1); fold (R_dist l (f x1)); rewrite R_dist_sym; assumption. Qed. @@ -259,7 +259,7 @@ Lemma limit_minus : limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:R => f x - g x) D (l - l') x0. Proof. - intros; unfold Rminus in |- *; generalize (limit_Ropp g D l' x0 H0); intro; + intros; unfold Rminus; generalize (limit_Ropp g D l' x0 H0); intro; exact (limit_plus f (fun x:R => - g x) D l (- l') x0 H H1). Qed. @@ -268,9 +268,9 @@ Lemma limit_free : forall (f:R -> R) (D:R -> Prop) (x x0:R), limit1_in (fun h:R => f x) D (f x) x0. Proof. - 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 (f x) (f x)); - intros a b; rewrite (b (refl_equal (f x))); unfold Rgt in H; + intros a b; rewrite (b (eq_refl (f x))); unfold Rgt in H; assumption. Qed. @@ -280,14 +280,14 @@ Lemma limit_mul : limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:R => f x * g x) D (l * l') x0. Proof. - intros; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; + intros; unfold limit1_in; unfold limit_in; simpl; intros; elim (H (Rmin 1 (eps * mul_factor l l')) (mul_factor_gt_f eps l l' H1)); elim (H0 (eps * mul_factor l l') (mul_factor_gt eps l l' H1)); - clear H H0; simpl in |- *; intros; elim H; elim H0; + clear H H0; simpl; intros; elim H; elim H0; clear H H0; intros; split with (Rmin x1 x); split. exact (Rmin_Rgt_r x1 x 0 (conj H H2)). - intros; elim H4; clear H4; intros; unfold R_dist in |- *; + intros; elim H4; clear H4; intros; unfold R_dist; replace (f x2 * g x2 - l * l') with (f x2 * (g x2 - l') + l' * (f x2 - l)). cut (Rabs (f x2 * (g x2 - l')) + Rabs (l' * (f x2 - l)) < eps). cut @@ -309,7 +309,7 @@ Proof. apply Rmult_ge_0_gt_0_lt_compat. apply Rle_ge. exact (Rabs_pos (g x2 - l')). - rewrite (Rplus_comm 1 (Rabs l)); unfold Rgt in |- *; apply Rle_lt_0_plus_1; + rewrite (Rplus_comm 1 (Rabs l)); unfold Rgt; apply Rle_lt_0_plus_1; exact (Rabs_pos l). unfold R_dist in H9; apply (Rplus_lt_reg_r (- Rabs l) (Rabs (f x2)) (1 + Rabs l)). @@ -323,13 +323,13 @@ Proof. generalize (H3 x2 (conj H4 H6)); trivial. apply Rmult_le_compat_l. exact (Rabs_pos l'). - unfold Rle in |- *; left; assumption. + unfold Rle; left; assumption. rewrite (Rmult_comm (1 + Rabs l) (eps * mul_factor l l')); rewrite (Rmult_comm (Rabs l') (eps * mul_factor l l')); rewrite <- (Rmult_plus_distr_l (eps * mul_factor l l') (1 + Rabs l) (Rabs l')) ; rewrite (Rmult_assoc eps (mul_factor l l') (1 + Rabs l + Rabs l')); - rewrite (Rplus_assoc 1 (Rabs l) (Rabs l')); unfold mul_factor in |- *; + rewrite (Rplus_assoc 1 (Rabs l) (Rabs l')); unfold mul_factor; rewrite (Rinv_l (1 + (Rabs l + Rabs l')) (mul_factor_wd l l')); rewrite (proj1 (Rmult_ne eps)); apply Req_le; trivial. ring. @@ -344,10 +344,10 @@ Lemma single_limit : forall (f:R -> R) (D:R -> Prop) (l l' x0:R), adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'. Proof. - unfold limit1_in in |- *; unfold limit_in in |- *; intros. + unfold limit1_in; unfold limit_in; intros. cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps). - clear H0 H1; unfold dist in |- *; unfold R_met in |- *; unfold R_dist in |- *; - unfold Rabs in |- *; case (Rcase_abs (l - l')); intros. + clear H0 H1; unfold dist; unfold R_met; unfold R_dist; + unfold Rabs; case (Rcase_abs (l - l')); intros. cut (forall eps:R, eps > 0 -> - (l - l') < eps). intro; generalize (prop_eps (- (l - l')) H1); intro; generalize (Ropp_gt_lt_0_contravar (l - l') r); intro; @@ -358,10 +358,10 @@ Proof. rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro; - unfold Rgt in |- *; generalize (Rplus_lt_compat_l 1 0 1 H3); + unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3); intro; elim (Rplus_ne 1); intros a b; rewrite a in H4; clear a b; apply (Rlt_trans 0 1 2 H3 H4). - unfold Rgt in |- *; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2)); + unfold Rgt; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_0_r (/ 2)); apply (Rmult_lt_compat_l (/ 2) 0 eps); auto. apply (Rinv_0_lt_compat 2); cut (1 < 2). @@ -380,10 +380,10 @@ Proof. rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro; - unfold Rgt in |- *; generalize (Rplus_lt_compat_l 1 0 1 H3); + unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3); intro; elim (Rplus_ne 1); intros a b; rewrite a in H4; clear a b; apply (Rlt_trans 0 1 2 H3 H4). - unfold Rgt in |- *; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2)); + unfold Rgt; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_0_r (/ 2)); apply (Rmult_lt_compat_l (/ 2) 0 eps); auto. apply (Rinv_0_lt_compat 2); cut (1 < 2). @@ -393,7 +393,7 @@ Proof. (**) intros; unfold adhDa in H; elim (H0 eps H2); intros; elim (H1 eps H2); intros; clear H0 H1; elim H3; elim H4; clear H3 H4; intros; - simpl in |- *; simpl in H1, H4; generalize (Rmin_Rgt x x1 0); + simpl; simpl in H1, H4; generalize (Rmin_Rgt x x1 0); intro; elim H5; intros; clear H5; elim (H (Rmin x x1) (H7 (conj H3 H0))); intros; elim H5; intros; clear H5 H H6 H7; generalize (Rmin_Rgt x x1 (R_dist x2 x0)); intro; @@ -403,10 +403,10 @@ Proof. intros; generalize (Rplus_lt_compat (R_dist (f x2) l) eps (R_dist (f x2) l') eps H H0); - unfold R_dist in |- *; intros; rewrite (Rabs_minus_sym (f x2) l) in H1; + unfold R_dist; intros; rewrite (Rabs_minus_sym (f x2) l) in H1; rewrite (Rmult_comm 2 eps); rewrite (Rmult_plus_distr_l eps 1 1); elim (Rmult_ne eps); intros a b; rewrite a; clear a b; - generalize (R_dist_tri l l' (f x2)); unfold R_dist in |- *; + generalize (R_dist_tri l l' (f x2)); unfold R_dist; intros; apply (Rle_lt_trans (Rabs (l - l')) (Rabs (l - f x2) + Rabs (f x2 - l')) @@ -419,7 +419,7 @@ Lemma limit_comp : limit1_in f Df l x0 -> limit1_in g Dg l' l -> limit1_in (fun x:R => g (f x)) (Dgf Df Dg f) l' x0. Proof. - unfold limit1_in, limit_in, Dgf in |- *; simpl in |- *. + unfold limit1_in, limit_in, Dgf; simpl. intros f g Df Dg l l' x0 Hf Hg eps eps_pos. elim (Hg eps eps_pos). intros alpg lg. @@ -436,12 +436,12 @@ Lemma limit_inv : forall (f:R -> R) (D:R -> Prop) (l x0:R), limit1_in f D l x0 -> l <> 0 -> limit1_in (fun x:R => / f x) D (/ l) x0. Proof. - unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; - unfold R_dist in |- *; intros; elim (H (Rabs l / 2)). + unfold limit1_in; unfold limit_in; simpl; + unfold R_dist; intros; elim (H (Rabs l / 2)). intros delta1 H2; elim (H (eps * (Rsqr l / 2))). intros delta2 H3; elim H2; elim H3; intros; exists (Rmin delta1 delta2); split. - unfold Rmin in |- *; case (Rle_dec delta1 delta2); intro; assumption. + unfold Rmin; case (Rle_dec delta1 delta2); intro; assumption. intro; generalize (H5 x); clear H5; intro H5; generalize (H7 x); clear H7; intro H7; intro H10; elim H10; intros; cut (D x /\ Rabs (x - x0) < delta1). cut (D x /\ Rabs (x - x0) < delta2). @@ -455,7 +455,7 @@ Proof. (Rplus_lt_compat_l (Rabs (f x) - Rabs l / 2) (Rabs l - Rabs (f x)) (Rabs l / 2) H14); replace (Rabs (f x) - Rabs l / 2 + (Rabs l - Rabs (f x))) with (Rabs l / 2). - unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l; + unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; cut (f x <> 0). intro; replace (/ f x + - / l) with ((l - f x) * / (l * f x)). rewrite Rabs_mult; rewrite Rabs_Rinv. @@ -467,7 +467,7 @@ Proof. (/ Rabs (l * f x)) (2 / Rsqr l) (Rabs_pos (l - f x)) H18 H5 H17); replace (eps * (Rsqr l / 2) * (2 / Rsqr l)) with eps. intro; assumption. - unfold Rdiv in |- *; unfold Rsqr in |- *; rewrite Rinv_mult_distr. + unfold Rdiv; unfold Rsqr; rewrite Rinv_mult_distr. repeat rewrite Rmult_assoc. rewrite (Rmult_comm l). repeat rewrite Rmult_assoc. @@ -487,7 +487,7 @@ Proof. left; apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply prod_neq_R0; assumption. rewrite Rmult_comm; rewrite Rabs_mult; rewrite Rinv_mult_distr. - rewrite (Rsqr_abs l); unfold Rsqr in |- *; unfold Rdiv in |- *; + rewrite (Rsqr_abs l); unfold Rsqr; unfold Rdiv; rewrite Rinv_mult_distr. repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. @@ -496,7 +496,7 @@ Proof. apply Rabs_pos_lt; assumption. apply Rabs_pos_lt; assumption. apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); - [ intro H17; generalize (lt_INR_0 2 (neq_O_lt 2 H17)); unfold INR in |- *; + [ intro H17; generalize (lt_INR_0 2 (neq_O_lt 2 H17)); unfold INR; intro H18; assumption | discriminate ]. replace (Rabs (f x) * Rabs l * / 2 * / Rabs (f x)) with (Rabs l / 2). @@ -512,7 +512,7 @@ Proof. discrR. apply Rabs_no_R0. assumption. - unfold Rdiv in |- *. + unfold Rdiv. repeat rewrite Rmult_assoc. rewrite (Rmult_comm (Rabs (f x))). repeat rewrite Rmult_assoc. @@ -526,7 +526,7 @@ Proof. apply Rabs_no_R0; assumption. apply prod_neq_R0; assumption. rewrite (Rinv_mult_distr _ _ H0 H16). - unfold Rminus in |- *; rewrite Rmult_plus_distr_r. + unfold Rminus; rewrite Rmult_plus_distr_r. rewrite <- Rmult_assoc. rewrite <- Rinv_r_sym. rewrite Rmult_1_l. @@ -538,16 +538,16 @@ Proof. reflexivity. assumption. assumption. - red in |- *; intro; rewrite H16 in H15; rewrite Rabs_R0 in H15; + red; intro; rewrite H16 in H15; rewrite Rabs_R0 in H15; cut (0 < Rabs l / 2). intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (Rabs l / 2) 0 H17 H15)). - unfold Rdiv in |- *; apply Rmult_lt_0_compat. + unfold Rdiv; apply Rmult_lt_0_compat. apply Rabs_pos_lt; assumption. apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); - [ intro H17; generalize (lt_INR_0 2 (neq_O_lt 2 H17)); unfold INR in |- *; + [ intro H17; generalize (lt_INR_0 2 (neq_O_lt 2 H17)); unfold INR; intro; assumption | discriminate ]. - pattern (Rabs l) at 3 in |- *; rewrite double_var. + pattern (Rabs l) at 3; rewrite double_var. ring. split; [ assumption @@ -557,18 +557,18 @@ Proof. [ assumption | apply Rlt_le_trans with (Rmin delta1 delta2); [ assumption | apply Rmin_l ] ]. - change (0 < eps * (Rsqr l / 2)) in |- *; unfold Rdiv in |- *; + change (0 < eps * (Rsqr l / 2)); unfold Rdiv; repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat. assumption. apply Rmult_lt_0_compat. apply Rsqr_pos_lt; assumption. apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); - [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *; + [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR; intro; assumption | discriminate ]. - change (0 < Rabs l / 2) in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat; + change (0 < Rabs l / 2); unfold Rdiv; apply Rmult_lt_0_compat; [ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); - [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *; + [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR; intro; assumption | discriminate ] ]. Qed. |