diff options
Diffstat (limited to 'theories/Reals/SeqSeries.v')
| -rw-r--r-- | theories/Reals/SeqSeries.v | 68 |
1 files changed, 33 insertions, 35 deletions
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 5f2173c7..25fe4848 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -222,39 +222,37 @@ Proof. intro; apply Rle_lt_trans with (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m)). assumption. apply H2; assumption. - assert (H5 := lt_eq_lt_dec n m). - elim H5; intro. - elim a; intro. - rewrite (tech2 An n m); [ idtac | assumption ]. - rewrite (tech2 Bn n m); [ idtac | assumption ]. - 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. - elim (H (S n + n0)%nat); intros. - apply H8. - apply Rle_ge; apply cond_pos_sum; intro. - elim (H (S n + n0)%nat); intros. - 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; unfold Rminus; + destruct (lt_eq_lt_dec n m) as [[| -> ]|]. + - rewrite (tech2 An n m); [ idtac | assumption ]. + rewrite (tech2 Bn n m); [ idtac | assumption ]. + 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. + elim (H (S n + n0)%nat); intros H7 H8. + apply H8. + apply Rle_ge; apply cond_pos_sum; intro. + elim (H (S n + n0)%nat); intros. + 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. + - 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; 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. - apply sum_Rle; intros. - elim (H (S m + n0)%nat); intros; apply H8. - apply Rle_ge; apply cond_pos_sum; intro. - elim (H (S m + n0)%nat); intros. - apply Rle_trans with (An (S m + n0)%nat); assumption. - apply Rle_ge. - apply cond_pos_sum; intro. - elim (H (S m + n0)%nat); intros; assumption. + - rewrite (tech2 An m n); [ idtac | assumption ]. + rewrite (tech2 Bn m n); [ idtac | assumption ]. + 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. + apply sum_Rle; intros. + elim (H (S m + n0)%nat); intros H7 H8; apply H8. + apply Rle_ge; apply cond_pos_sum; intro. + elim (H (S m + n0)%nat); intros. + apply Rle_trans with (An (S m + n0)%nat); assumption. + apply Rle_ge. + apply cond_pos_sum; intro. + elim (H (S m + n0)%nat); intros; assumption. Qed. (** Cesaro's theorem *) @@ -361,7 +359,7 @@ Proof with trivial. replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with (sum_f_R0 (fun k:nat => An k * Bn k) n + sum_f_R0 (fun k:nat => An k * - l) n)... - rewrite <- (scal_sum An n (- l)); field... + rewrite <- (scal_sum An n (- l)); field... rewrite <- plus_sum; apply sum_eq; intros; ring... Qed. @@ -375,11 +373,11 @@ Proof with trivial. 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; intro; case (Rle_dec M 0); intro... + unfold cv_infty; intro; destruct (Rle_dec M 0) as [Hle|Hnle]... 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; + clear Hnle; set (m := up M); elim (archimed M); intros; assert (H5 : (0 <= m)%Z)... apply le_IZR; unfold m; simpl; left; apply Rlt_trans with M... elim (IZN _ H5); intros; exists x; intros; unfold An; rewrite sum_cte; |