diff options
Diffstat (limited to 'theories/Reals/SeqSeries.v')
| -rw-r--r-- | theories/Reals/SeqSeries.v | 98 |
1 files changed, 49 insertions, 49 deletions
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 0d876be5..5140c29c 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.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 *) @@ -19,7 +19,7 @@ Require Export Rsigma. Require Export Rprod. Require Export Cauchy_prod. Require Export Alembert. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma sum_maj1 : @@ -41,21 +41,21 @@ Proof. intro; rewrite H4; rewrite H5. apply sum_cv_maj with (fun l:nat => An (S N + l)%nat) (fun (l:nat) (x:R) => fn (S N + l)%nat x) x. - unfold SP in |- *; apply H2. + unfold SP; apply H2. apply H3. intros; apply H1. - symmetry in |- *; eapply UL_sequence. + symmetry ; eapply UL_sequence. apply H3. - unfold Un_cv in H0; unfold Un_cv in |- *; intros; elim (H0 eps H5); + unfold Un_cv in H0; unfold Un_cv; intros; elim (H0 eps H5); intros N0 H6. unfold R_dist in H6; exists N0; intros. - unfold R_dist in |- *; + unfold R_dist; replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N)) with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2); [ idtac | ring ]. replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n) with (sum_f_R0 An (S (N + n))). - apply H6; unfold ge in |- *; apply le_trans with n. + apply H6; unfold ge; apply le_trans with n. apply H7. apply le_trans with (N + n)%nat. apply le_plus_r. @@ -80,12 +80,12 @@ Proof. reflexivity. apply le_lt_n_Sm; apply le_plus_l. apply le_O_n. - symmetry in |- *; eapply UL_sequence. + symmetry ; eapply UL_sequence. apply H2. - unfold Un_cv in H; unfold Un_cv in |- *; intros. + unfold Un_cv in H; unfold Un_cv; intros. elim (H eps H4); intros N0 H5. unfold R_dist in H5; exists N0; intros. - unfold R_dist, SP in |- *; + unfold R_dist, SP; replace (sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - (l1 - sum_f_R0 (fun k:nat => fn k x) N)) with @@ -96,7 +96,7 @@ Proof. (sum_f_R0 (fun k:nat => fn k x) N + sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) with (sum_f_R0 (fun k:nat => fn k x) (S (N + n))). - unfold SP in H5; apply H5; unfold ge in |- *; apply le_trans with n. + unfold SP in H5; apply H5; unfold ge; apply le_trans with n. apply H6. apply le_trans with (N + n)%nat. apply le_plus_r. @@ -124,16 +124,16 @@ Proof. apply le_plus_l. apply le_O_n. exists (l2 - sum_f_R0 An N). - unfold Un_cv in H0; unfold Un_cv in |- *; intros. + unfold Un_cv in H0; unfold Un_cv; intros. elim (H0 eps H2); intros N0 H3. unfold R_dist in H3; exists N0; intros. - unfold R_dist in |- *; + unfold R_dist; replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N)) with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2); [ idtac | ring ]. replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n) with (sum_f_R0 An (S (N + n))). - apply H3; unfold ge in |- *; apply le_trans with n. + apply H3; unfold ge; apply le_trans with n. apply H4. apply le_trans with (N + n)%nat. apply le_plus_r. @@ -160,10 +160,10 @@ Proof. apply le_plus_l. apply le_O_n. exists (l1 - SP fn N x). - unfold Un_cv in H; unfold Un_cv in |- *; intros. + unfold Un_cv in H; unfold Un_cv; intros. elim (H eps H2); intros N0 H3. unfold R_dist in H3; exists N0; intros. - unfold R_dist, SP in |- *. + unfold R_dist, SP. replace (sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - (l1 - sum_f_R0 (fun k:nat => fn k x) N)) with @@ -175,7 +175,7 @@ Proof. sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) with (sum_f_R0 (fun k:nat => fn k x) (S (N + n))). unfold SP in H3; apply H3. - unfold ge in |- *; apply le_trans with n. + unfold ge; apply le_trans with n. apply H4. apply le_trans with (N + n)%nat. apply le_plus_r. @@ -213,7 +213,7 @@ Lemma Rseries_CV_comp : Proof. intros An Bn H X; apply cv_cauchy_2. assert (H0 := cv_cauchy_1 _ X). - unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *. + unfold Cauchy_crit_series; unfold Cauchy_crit. intros; elim (H0 eps H1); intros. exists x; intros. cut @@ -227,7 +227,7 @@ Proof. elim a; intro. rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 Bn n m); [ idtac | assumption ]. - unfold R_dist in |- *; unfold Rminus in |- *; do 2 rewrite Ropp_plus_distr; + unfold R_dist; unfold Rminus; do 2 rewrite Ropp_plus_distr; do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r; do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right. apply sum_Rle; intros. @@ -238,12 +238,12 @@ Proof. apply Rle_trans with (An (S n + n0)%nat); assumption. apply Rle_ge; apply cond_pos_sum; intro. elim (H (S n + n0)%nat); intros; assumption. - rewrite b; unfold R_dist in |- *; unfold Rminus in |- *; + rewrite b; unfold R_dist; unfold Rminus; do 2 rewrite Rplus_opp_r; rewrite Rabs_R0; right; reflexivity. rewrite (tech2 An m n); [ idtac | assumption ]. rewrite (tech2 Bn m n); [ idtac | assumption ]. - unfold R_dist in |- *; unfold Rminus in |- *; do 2 rewrite Rplus_assoc; + unfold R_dist; unfold Rminus; do 2 rewrite Rplus_assoc; rewrite (Rplus_comm (sum_f_R0 An m)); rewrite (Rplus_comm (sum_f_R0 Bn m)); do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l; do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right. @@ -266,13 +266,13 @@ Lemma Cesaro : Un_cv (fun n:nat => sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n) l. Proof with trivial. - unfold Un_cv in |- *; intros; assert (H3 : forall n:nat, 0 < sum_f_R0 An n)... + unfold Un_cv; intros; assert (H3 : forall n:nat, 0 < sum_f_R0 An n)... intro; apply tech1... assert (H4 : forall n:nat, sum_f_R0 An n <> 0)... - intro; red in |- *; intro; assert (H5 := H3 n); rewrite H4 in H5; + intro; red; intro; assert (H5 := H3 n); rewrite H4 in H5; elim (Rlt_irrefl _ H5)... assert (H5 := cv_infty_cv_R0 _ H4 H1); assert (H6 : 0 < eps / 2)... - unfold Rdiv in |- *; apply Rmult_lt_0_compat... + unfold Rdiv; apply Rmult_lt_0_compat... apply Rinv_0_lt_compat; prove_sup... elim (H _ H6); clear H; intros N1 H; set (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); @@ -282,10 +282,10 @@ Proof with trivial. (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2))... case (Req_dec C 0); intro... exists 0%nat; intros... - rewrite H7; unfold Rdiv in |- *; rewrite Rmult_0_l; apply Rmult_lt_0_compat... + rewrite H7; unfold Rdiv; rewrite Rmult_0_l; apply Rmult_lt_0_compat... apply Rinv_0_lt_compat; prove_sup... assert (H8 : 0 < eps / (2 * Rabs C))... - unfold Rdiv in |- *; apply Rmult_lt_0_compat... + unfold Rdiv; apply Rmult_lt_0_compat... apply Rinv_0_lt_compat; apply Rmult_lt_0_compat... prove_sup... apply Rabs_pos_lt... @@ -294,23 +294,23 @@ Proof with trivial. rewrite Rplus_0_r in H11... apply Rle_lt_trans with (Rabs (C / sum_f_R0 An n))... apply RRle_abs... - unfold Rdiv in |- *; rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs C)... + unfold Rdiv; rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs C)... apply Rinv_0_lt_compat; apply Rabs_pos_lt... rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_l; replace (/ Rabs C * (eps * / 2)) with (eps / (2 * Rabs C))... - unfold Rdiv in |- *; rewrite Rinv_mult_distr... + unfold Rdiv; rewrite Rinv_mult_distr... ring... discrR... apply Rabs_no_R0... apply Rabs_no_R0... elim H7; clear H7; intros N2 H7; set (N := max N1 N2); exists (S N); intros; - unfold R_dist in |- *; + unfold R_dist; replace (sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n - l) with (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n / sum_f_R0 An n)... assert (H9 : (N1 < n)%nat)... apply lt_le_trans with (S N)... - apply le_lt_n_Sm; unfold N in |- *; apply le_max_l... - rewrite (tech2 (fun k:nat => An k * (Bn k - l)) _ _ H9); unfold Rdiv in |- *; + apply le_lt_n_Sm; unfold N; apply le_max_l... + rewrite (tech2 (fun k:nat => An k * (Bn k - l)) _ _ H9); unfold Rdiv; rewrite Rmult_plus_distr_r; apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1 / sum_f_R0 An n) + @@ -319,12 +319,12 @@ Proof with trivial. (n - S N1) / sum_f_R0 An n))... apply Rabs_triang... rewrite (double_var eps); apply Rplus_lt_compat... - unfold Rdiv in |- *; rewrite Rabs_mult; fold C in |- *; rewrite Rabs_right... + unfold Rdiv; rewrite Rabs_mult; fold C; rewrite Rabs_right... apply (H7 n); apply le_trans with (S N)... - apply le_trans with N; [ unfold N in |- *; apply le_max_r | apply le_n_Sn ]... + apply le_trans with N; [ unfold N; apply le_max_r | apply le_n_Sn ]... apply Rle_ge; left; apply Rinv_0_lt_compat... - unfold R_dist in H; unfold Rdiv in |- *; rewrite Rabs_mult; + unfold R_dist in H; unfold Rdiv; rewrite Rabs_mult; rewrite (Rabs_right (/ sum_f_R0 An n))... apply Rle_lt_trans with (sum_f_R0 (fun i:nat => Rabs (An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l))) @@ -340,22 +340,22 @@ Proof with trivial. do 2 rewrite <- (Rmult_comm (/ sum_f_R0 An n)); apply Rmult_le_compat_l... left; apply Rinv_0_lt_compat... apply sum_Rle; intros; rewrite Rabs_mult; - pattern (An (S N1 + n0)%nat) at 2 in |- *; + pattern (An (S N1 + n0)%nat) at 2; rewrite <- (Rabs_right (An (S N1 + n0)%nat))... apply Rmult_le_compat_l... apply Rabs_pos... - left; apply H; unfold ge in |- *; apply le_trans with (S N1); + left; apply H; unfold ge; apply le_trans with (S N1); [ apply le_n_Sn | apply le_plus_l ]... apply Rle_ge; left... rewrite <- (scal_sum (fun i:nat => An (S N1 + i)%nat) (n - S N1) (eps / 2)); - unfold Rdiv in |- *; repeat rewrite Rmult_assoc; apply Rmult_lt_compat_l... - pattern (/ 2) at 2 in |- *; rewrite <- Rmult_1_r; apply Rmult_lt_compat_l... + unfold Rdiv; repeat rewrite Rmult_assoc; apply Rmult_lt_compat_l... + pattern (/ 2) at 2; rewrite <- Rmult_1_r; apply Rmult_lt_compat_l... apply Rinv_0_lt_compat; prove_sup... rewrite Rmult_comm; apply Rmult_lt_reg_l with (sum_f_R0 An n)... rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym... rewrite Rmult_1_l; rewrite Rmult_1_r; rewrite (tech2 An N1 n)... rewrite Rplus_comm; - pattern (sum_f_R0 (fun i:nat => An (S N1 + i)%nat) (n - S N1)) at 1 in |- *; + pattern (sum_f_R0 (fun i:nat => An (S N1 + i)%nat) (n - S N1)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l... apply Rle_ge; left; apply Rinv_0_lt_compat... replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with @@ -371,41 +371,41 @@ Lemma Cesaro_1 : Proof with trivial. intros Bn l H; set (An := fun _:nat => 1)... assert (H0 : forall n:nat, 0 < An n)... - intro; unfold An in |- *; apply Rlt_0_1... + intro; unfold An; apply Rlt_0_1... assert (H1 : forall n:nat, 0 < sum_f_R0 An n)... intro; apply tech1... assert (H2 : cv_infty (fun n:nat => sum_f_R0 An n))... - unfold cv_infty in |- *; intro; case (Rle_dec M 0); intro... + unfold cv_infty; intro; case (Rle_dec M 0); intro... exists 0%nat; intros; apply Rle_lt_trans with 0... assert (H2 : 0 < M)... auto with real... clear n; set (m := up M); elim (archimed M); intros; assert (H5 : (0 <= m)%Z)... - apply le_IZR; unfold m in |- *; simpl in |- *; left; apply Rlt_trans with M... - elim (IZN _ H5); intros; exists x; intros; unfold An in |- *; rewrite sum_cte; + apply le_IZR; unfold m; simpl; left; apply Rlt_trans with M... + elim (IZN _ H5); intros; exists x; intros; unfold An; rewrite sum_cte; rewrite Rmult_1_l; apply Rlt_trans with (IZR (up M))... apply Rle_lt_trans with (INR x)... - rewrite INR_IZR_INZ; fold m in |- *; rewrite <- H6; right... + rewrite INR_IZR_INZ; fold m; rewrite <- H6; right... apply lt_INR; apply le_lt_n_Sm... assert (H3 := Cesaro _ _ _ H H0 H2)... - unfold Un_cv in |- *; unfold Un_cv in H3; intros; elim (H3 _ H4); intros; - exists (S x); intros; unfold R_dist in |- *; unfold R_dist in H5; + unfold Un_cv; unfold Un_cv in H3; intros; elim (H3 _ H4); intros; + exists (S x); intros; unfold R_dist; unfold R_dist in H5; apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => An k * Bn k) (pred n) / sum_f_R0 An (pred n) - l))... right; replace (sum_f_R0 Bn (pred n) / INR n - l) with (sum_f_R0 (fun k:nat => An k * Bn k) (pred n) / sum_f_R0 An (pred n) - l)... - unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- l)); + unfold Rminus; do 2 rewrite <- (Rplus_comm (- l)); apply Rplus_eq_compat_l... - unfold An in |- *; + unfold An; replace (sum_f_R0 (fun k:nat => 1 * Bn k) (pred n)) with (sum_f_R0 Bn (pred n))... rewrite sum_cte; rewrite Rmult_1_l; replace (S (pred n)) with n... apply S_pred with 0%nat; apply lt_le_trans with (S x)... apply lt_O_Sn... apply sum_eq; intros; ring... - apply H5; unfold ge in |- *; apply le_S_n; replace (S (pred n)) with n... + apply H5; unfold ge; apply le_S_n; replace (S (pred n)) with n... apply S_pred with 0%nat; apply lt_le_trans with (S x)... apply lt_O_Sn... Qed. |