diff options
Diffstat (limited to 'theories/Reals/SeqProp.v')
| -rw-r--r-- | theories/Reals/SeqProp.v | 404 |
1 files changed, 202 insertions, 202 deletions
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 34f9fd72..2e851b13 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: SeqProp.v,v 1.13.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) + +(*i $Id: SeqProp.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -48,7 +48,7 @@ cut (~ (forall N:nat, Un N <= x - eps)). intro H6; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)). intro H7; apply H6; intro N; apply Rnot_lt_le; apply H7. intro H7; generalize (Un_bound_imp Un (x - eps) H7); intro H8; - unfold is_upper_bound in H8; generalize (H3 (x - eps) H8); + unfold is_upper_bound in H8; generalize (H3 (x - eps) H8); apply Rlt_not_le; apply tech_Rgt_minus; exact H1. Qed. @@ -66,12 +66,12 @@ Lemma decreasing_cv : Un_decreasing Un -> has_lb Un -> sigT (fun l:R => Un_cv Un l). intros. cut (sigT (fun l:R => Un_cv (opp_seq Un) l) -> sigT (fun l:R => Un_cv Un l)). -intro. +intro X. apply X. apply growing_cv. apply decreasing_growing; assumption. exact H0. -intro. +intro X. elim X; intros. apply existT with (- x). unfold Un_cv in p. @@ -155,14 +155,14 @@ elim H1; intros. exists (k + x1)%nat; assumption. Qed. -Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un) +Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un) (i:nat) : R := majorant (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr). -Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un) +Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un) (i:nat) : R := minorant (fun k:nat => Un (i + k)%nat) (min_ss Un i pr). Lemma Wn_decreasing : - forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr). + forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr). intros. unfold Un_decreasing in |- *. intro. @@ -289,14 +289,14 @@ Qed. (**********) Lemma Vn_Un_Wn_order : - forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) - (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n. + forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) + (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n. intros. split. unfold sequence_minorant in |- *. cut (sigT (fun l:R => is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l)). -intro. +intro X. elim X; intros. replace (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x). unfold is_lub in p. @@ -329,7 +329,7 @@ apply min_inf. apply min_ss; assumption. unfold sequence_majorant in |- *. cut (sigT (fun l:R => is_lub (EUn (fun i:nat => Un (n + i)%nat)) l)). -intro. +intro X. elim X; intros. replace (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x. unfold is_lub in p. @@ -379,7 +379,7 @@ Qed. Lemma maj_min : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un), - has_lb (sequence_majorant Un pr1). + has_lb (sequence_majorant Un pr1). intros. assert (H := Vn_Un_Wn_order Un pr1 pr2). unfold has_lb in |- *. @@ -486,7 +486,7 @@ Qed. Lemma not_Rlt : forall r1 r2:R, ~ r1 < r2 -> r1 >= r2. intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rge in |- *. tauto. -Qed. +Qed. (**********) Lemma approx_maj : @@ -628,234 +628,234 @@ assert (H2 := H1 n). apply not_Rlt; assumption. Qed. -(* Unicity of limit for convergent sequences *) +(* Unicity of limit for convergent sequences *) Lemma UL_sequence : - forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2. -intros Un l1 l2; unfold Un_cv in |- *; unfold R_dist in |- *; intros. -apply cond_eq. + forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2. +intros Un l1 l2; unfold Un_cv in |- *; unfold R_dist in |- *; intros. +apply cond_eq. intros; cut (0 < eps / 2); [ intro | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (H (eps / 2) H2); intros. -elim (H0 (eps / 2) H2); intros. -set (N := max x x0). -apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (H (eps / 2) H2); intros. +elim (H0 (eps / 2) H2); intros. +set (N := max x x0). +apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). replace (l1 - l2) with (l1 - Un N + (Un N - l2)); - [ apply Rabs_triang | ring ]. -rewrite (double_var eps); apply Rplus_lt_compat. + [ apply Rabs_triang | ring ]. +rewrite (double_var eps); apply Rplus_lt_compat. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H3; - unfold ge, N in |- *; apply le_max_l. -apply H4; unfold ge, N in |- *; apply le_max_r. + unfold ge, N in |- *; apply le_max_l. +apply H4; unfold ge, N in |- *; apply le_max_r. Qed. -(**********) +(**********) Lemma CV_plus : forall (An Bn:nat -> R) (l1 l2:R), - Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2). -unfold Un_cv in |- *; unfold R_dist in |- *; intros. + Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2). +unfold Un_cv in |- *; unfold R_dist in |- *; intros. cut (0 < eps / 2); [ intro | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (H (eps / 2) H2); intros. -elim (H0 (eps / 2) H2); intros. -set (N := max x x0). -exists N; intros. + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (H (eps / 2) H2); intros. +elim (H0 (eps / 2) H2); intros. +set (N := max x x0). +exists N; intros. replace (An n + Bn n - (l1 + l2)) with (An n - l1 + (Bn n - l2)); - [ idtac | ring ]. -apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)). -apply Rabs_triang. -rewrite (double_var eps); apply Rplus_lt_compat. + [ idtac | ring ]. +apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)). +apply Rabs_triang. +rewrite (double_var eps); apply Rplus_lt_compat. apply H3; unfold ge in |- *; apply le_trans with N; - [ unfold N in |- *; apply le_max_l | assumption ]. + [ unfold N in |- *; apply le_max_l | assumption ]. apply H4; unfold ge in |- *; apply le_trans with N; - [ unfold N in |- *; apply le_max_r | assumption ]. + [ unfold N in |- *; apply le_max_r | assumption ]. Qed. -(**********) +(**********) Lemma cv_cvabs : forall (Un:nat -> R) (l:R), - Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l). -unfold Un_cv in |- *; unfold R_dist in |- *; intros. -elim (H eps H0); intros. -exists x; intros. -apply Rle_lt_trans with (Rabs (Un n - l)). -apply Rabs_triang_inv2. -apply H1; assumption. -Qed. + Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l). +unfold Un_cv in |- *; unfold R_dist in |- *; intros. +elim (H eps H0); intros. +exists x; intros. +apply Rle_lt_trans with (Rabs (Un n - l)). +apply Rabs_triang_inv2. +apply H1; assumption. +Qed. -(**********) +(**********) Lemma CV_Cauchy : - forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un. -intros; elim X; intros. -unfold Cauchy_crit in |- *; intros. -unfold Un_cv in p; unfold R_dist in p. + forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un. +intros Un X; elim X; intros. +unfold Cauchy_crit in |- *; intros. +unfold Un_cv in p; unfold R_dist in p. cut (0 < eps / 2); [ intro | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (p (eps / 2) H0); intros. -exists x0; intros. + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (p (eps / 2) H0); intros. +exists x0; intros. unfold R_dist in |- *; - apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)). + apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)). replace (Un n - Un m) with (Un n - x + (x - Un m)); - [ apply Rabs_triang | ring ]. -rewrite (double_var eps); apply Rplus_lt_compat. -apply H1; assumption. -rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption. -Qed. + [ apply Rabs_triang | ring ]. +rewrite (double_var eps); apply Rplus_lt_compat. +apply H1; assumption. +rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption. +Qed. (**********) Lemma maj_by_pos : forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> - exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). -intros; elim X; intros. -cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). -intro. -assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). -assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). -elim H0; intros. -exists (x0 + 1). -cut (0 <= x0). -intro. -split. -apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ]. -intros. -apply Rle_trans with x0. -unfold is_upper_bound in H1. -apply H1. -exists n; reflexivity. + exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). +intros Un X; elim X; intros. +cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). +intro X0. +assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). +assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). +elim H0; intros. +exists (x0 + 1). +cut (0 <= x0). +intro. +split. +apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ]. +intros. +apply Rle_trans with x0. +unfold is_upper_bound in H1. +apply H1. +exists n; reflexivity. pattern x0 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; - apply Rlt_0_1. -apply Rle_trans with (Rabs (Un 0%nat)). -apply Rabs_pos. -unfold is_upper_bound in H1. -apply H1. -exists 0%nat; reflexivity. -apply existT with (Rabs x). -apply cv_cvabs; assumption. -Qed. - -(**********) + apply Rlt_0_1. +apply Rle_trans with (Rabs (Un 0%nat)). +apply Rabs_pos. +unfold is_upper_bound in H1. +apply H1. +exists 0%nat; reflexivity. +apply existT with (Rabs x). +apply cv_cvabs; assumption. +Qed. + +(**********) Lemma CV_mult : forall (An Bn:nat -> R) (l1 l2:R), - Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2). -intros. -cut (sigT (fun l:R => Un_cv An l)). -intro. -assert (H1 := maj_by_pos An X). -elim H1; intros M H2. -elim H2; intros. -unfold Un_cv in |- *; unfold R_dist in |- *; intros. -cut (0 < eps / (2 * M)). -intro. -case (Req_dec l2 0); intro. -unfold Un_cv in H0; unfold R_dist in H0. -elim (H0 (eps / (2 * M)) H6); intros. -exists x; intros. + Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2). +intros. +cut (sigT (fun l:R => Un_cv An l)). +intro X. +assert (H1 := maj_by_pos An X). +elim H1; intros M H2. +elim H2; intros. +unfold Un_cv in |- *; unfold R_dist in |- *; intros. +cut (0 < eps / (2 * M)). +intro. +case (Req_dec l2 0); intro. +unfold Un_cv in H0; unfold R_dist in H0. +elim (H0 (eps / (2 * M)) H6); intros. +exists x; intros. apply Rle_lt_trans with - (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). + (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). replace (An n * Bn n - l1 * l2) with (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2)); - [ apply Rabs_triang | ring ]. + [ apply Rabs_triang | ring ]. replace (Rabs (An n * Bn n - An n * l2)) with - (Rabs (An n) * Rabs (Bn n - l2)). -replace (Rabs (An n * l2 - l1 * l2)) with 0. -rewrite Rplus_0_r. -apply Rle_lt_trans with (M * Rabs (Bn n - l2)). -do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). -apply Rmult_le_compat_l. -apply Rabs_pos. -apply H4. -apply Rmult_lt_reg_l with (/ M). -apply Rinv_0_lt_compat; apply H3. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). -apply Rlt_trans with (eps / (2 * M)). -apply H8; assumption. -unfold Rdiv in |- *; rewrite Rinv_mult_distr. -apply Rmult_lt_reg_l with 2. + (Rabs (An n) * Rabs (Bn n - l2)). +replace (Rabs (An n * l2 - l1 * l2)) with 0. +rewrite Rplus_0_r. +apply Rle_lt_trans with (M * Rabs (Bn n - l2)). +do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). +apply Rmult_le_compat_l. +apply Rabs_pos. +apply H4. +apply Rmult_lt_reg_l with (/ M). +apply Rinv_0_lt_compat; apply H3. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). +apply Rlt_trans with (eps / (2 * M)). +apply H8; assumption. +unfold Rdiv in |- *; rewrite Rinv_mult_distr. +apply Rmult_lt_reg_l with 2. prove_sup0. replace (2 * (eps * (/ 2 * / M))) with (2 * / 2 * (eps * / M)); - [ idtac | ring ]. -rewrite <- Rinv_r_sym. -rewrite Rmult_1_l; rewrite double. -pattern (eps * / M) at 1 in |- *; rewrite <- Rplus_0_r. + [ idtac | ring ]. +rewrite <- Rinv_r_sym. +rewrite Rmult_1_l; rewrite double. +pattern (eps * / M) at 1 in |- *; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; assumption ]. -discrR. -discrR. -red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). -red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). + [ assumption | apply Rinv_0_lt_compat; assumption ]. +discrR. +discrR. +red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). +red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). rewrite H7; do 2 rewrite Rmult_0_r; unfold Rminus in |- *; - rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity. -replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ idtac | ring ]. -symmetry in |- *; apply Rabs_mult. -cut (0 < eps / (2 * Rabs l2)). -intro. + rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity. +replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ idtac | ring ]. +symmetry in |- *; apply Rabs_mult. +cut (0 < eps / (2 * Rabs l2)). +intro. unfold Un_cv in H; unfold R_dist in H; unfold Un_cv in H0; - unfold R_dist in H0. -elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. -elim (H0 (eps / (2 * M)) H6); intros N2 H10. -set (N := max N1 N2). -exists N; intros. + unfold R_dist in H0. +elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. +elim (H0 (eps / (2 * M)) H6); intros N2 H10. +set (N := max N1 N2). +exists N; intros. apply Rle_lt_trans with - (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). + (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). replace (An n * Bn n - l1 * l2) with (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2)); - [ apply Rabs_triang | ring ]. + [ apply Rabs_triang | ring ]. replace (Rabs (An n * Bn n - An n * l2)) with - (Rabs (An n) * Rabs (Bn n - l2)). -replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)). -rewrite (double_var eps); apply Rplus_lt_compat. -apply Rle_lt_trans with (M * Rabs (Bn n - l2)). -do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). -apply Rmult_le_compat_l. -apply Rabs_pos. -apply H4. -apply Rmult_lt_reg_l with (/ M). -apply Rinv_0_lt_compat; apply H3. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). -apply Rlt_le_trans with (eps / (2 * M)). -apply H10. -unfold ge in |- *; apply le_trans with N. -unfold N in |- *; apply le_max_r. -assumption. -unfold Rdiv in |- *; rewrite Rinv_mult_distr. -right; ring. -discrR. -red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). -red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). -apply Rmult_lt_reg_l with (/ Rabs l2). -apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)). -apply H9. -unfold ge in |- *; apply le_trans with N. -unfold N in |- *; apply le_max_l. -assumption. -unfold Rdiv in |- *; right; rewrite Rinv_mult_distr. -ring. -discrR. -apply Rabs_no_R0; assumption. -apply Rabs_no_R0; assumption. + (Rabs (An n) * Rabs (Bn n - l2)). +replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)). +rewrite (double_var eps); apply Rplus_lt_compat. +apply Rle_lt_trans with (M * Rabs (Bn n - l2)). +do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). +apply Rmult_le_compat_l. +apply Rabs_pos. +apply H4. +apply Rmult_lt_reg_l with (/ M). +apply Rinv_0_lt_compat; apply H3. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). +apply Rlt_le_trans with (eps / (2 * M)). +apply H10. +unfold ge in |- *; apply le_trans with N. +unfold N in |- *; apply le_max_r. +assumption. +unfold Rdiv in |- *; rewrite Rinv_mult_distr. +right; ring. +discrR. +red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). +red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). +apply Rmult_lt_reg_l with (/ Rabs l2). +apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)). +apply H9. +unfold ge in |- *; apply le_trans with N. +unfold N in |- *; apply le_max_l. +assumption. +unfold Rdiv in |- *; right; rewrite Rinv_mult_distr. +ring. +discrR. +apply Rabs_no_R0; assumption. +apply Rabs_no_R0; assumption. replace (An n * l2 - l1 * l2) with (l2 * (An n - l1)); - [ symmetry in |- *; apply Rabs_mult | ring ]. + [ symmetry in |- *; apply Rabs_mult | ring ]. replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); - [ symmetry in |- *; apply Rabs_mult | ring ]. -unfold Rdiv in |- *; apply Rmult_lt_0_compat. -assumption. + [ symmetry in |- *; apply Rabs_mult | ring ]. +unfold Rdiv in |- *; apply Rmult_lt_0_compat. +assumption. apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; - [ prove_sup0 | apply Rabs_pos_lt; assumption ]. + [ prove_sup0 | apply Rabs_pos_lt; assumption ]. unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; - [ prove_sup0 | assumption ] ]. -apply existT with l1; assumption. -Qed. + [ prove_sup0 | assumption ] ]. +apply existT with l1; assumption. +Qed. Lemma tech9 : forall Un:nat -> R, @@ -905,13 +905,13 @@ rewrite b; assumption. cut (forall n:nat, Un n <= x0). intro; unfold is_lub in H0; unfold is_upper_bound in H0; elim H0; intros. cut (forall y:R, EUn Un y -> y <= x0). -intro; assert (H8 := H6 _ H7). +intro; assert (H8 := H6 _ H7). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 r)). unfold EUn in |- *; intros; elim H7; intros. rewrite H8; apply H4. intro; case (Rle_dec (Un n) x0); intro. assumption. -cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0). +cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0). intro; unfold Un_cv in H3; cut (0 < Un n - x0). intro; elim (H3 (Un n - x0) H5); intros. cut (max n x1 >= x1)%nat. @@ -931,7 +931,7 @@ left; assumption. unfold ge in |- *; apply le_max_r. apply Rplus_lt_reg_r with x0. rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm x0); - rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; + rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H4; apply le_n. intros; apply Rlt_le_trans with (Un n). case (Rlt_le_dec x0 (Un n)); intro. @@ -977,7 +977,7 @@ unfold R_dist in H4; rewrite <- Rabs_Rabsolu; apply Rabs_triang. rewrite (Rabs_right k). apply Rplus_lt_reg_r with (- k); rewrite <- (Rplus_comm k); - repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; + repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; repeat rewrite Rplus_0_l; apply H4. apply Rle_ge; elim H; intros; assumption. unfold Rdiv in |- *; apply Rmult_lt_0_compat. @@ -989,7 +989,7 @@ Qed. (**********) Lemma growing_ineq : forall (Un:nat -> R) (l:R), - Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l. + Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l. intros; case (total_order_T (Un n) l); intro. elim s; intro. left; assumption. @@ -1042,14 +1042,14 @@ Qed. (**********) Lemma CV_minus : forall (An Bn:nat -> R) (l1 l2:R), - Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2). -intros. -replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i). -unfold Rminus in |- *; apply CV_plus. -assumption. -apply CV_opp; assumption. -unfold Rminus, opp_seq in |- *; reflexivity. -Qed. + Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2). +intros. +replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i). +unfold Rminus in |- *; apply CV_plus. +assumption. +apply CV_opp; assumption. +unfold Rminus, opp_seq in |- *; reflexivity. +Qed. (* Un -> +oo *) Definition cv_infty (Un:nat -> R) : Prop := @@ -1265,7 +1265,7 @@ apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro; assert (H8 := sym_eq H7); elim (fact_neq_0 _ H8). clear Un Vn; apply INR_le; simpl in |- *. induction M_nat as [| M_nat HrecM_nat]. -assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. +assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S; |