summaryrefslogtreecommitdiff
path: root/theories/Reals/PartSum.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/PartSum.v')
-rw-r--r--theories/Reals/PartSum.v65
1 files changed, 28 insertions, 37 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 364d72cb..b710c75c 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.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 *)
@@ -180,12 +180,9 @@ Proof.
replace (S (S (pred N))) with (S N).
rewrite (HrecN H1); ring.
rewrite H2; simpl; reflexivity.
- assert (H2 := O_or_S N).
- elim H2; intros.
- elim a; intros.
- rewrite <- p.
+ destruct (O_or_S N) as [(m,<-)|<-].
simpl; reflexivity.
- rewrite <- b in H1; elim (lt_irrefl _ H1).
+ elim (lt_irrefl _ H1).
rewrite H1; simpl; reflexivity.
inversion H.
right; reflexivity.
@@ -395,9 +392,7 @@ Proof.
(sum_f_R0 (fun i:nat => Rabs (An i)) m)).
assumption.
apply H1; assumption.
- assert (H4 := lt_eq_lt_dec n m).
- elim H4; intro.
- elim a; intro.
+ destruct (lt_eq_lt_dec n m) as [[ | -> ]|].
rewrite (tech2 An n m); [ idtac | assumption ].
rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ].
unfold R_dist.
@@ -418,7 +413,6 @@ Proof.
apply Rle_ge.
apply cond_pos_sum.
intro; apply Rabs_pos.
- rewrite b.
unfold R_dist.
unfold Rminus; do 2 rewrite Rplus_opp_r.
rewrite Rabs_R0; right; reflexivity.
@@ -451,8 +445,7 @@ Lemma cv_cauchy_1 :
{ l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } ->
Cauchy_crit_series An.
Proof.
- intros An X.
- elim X; intros.
+ intros An (x,p).
unfold Un_cv in p.
unfold Cauchy_crit_series; unfold Cauchy_crit.
intros.
@@ -508,12 +501,11 @@ Lemma sum_incr :
Un_cv (fun n:nat => sum_f_R0 An n) l ->
(forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l.
Proof.
- intros; case (total_order_T (sum_f_R0 An N) l); intro.
- elim s; intro.
- left; apply a.
- right; apply b.
+ intros; destruct (total_order_T (sum_f_R0 An N) l) as [[Hlt|Heq]|Hgt].
+ left; apply Hlt.
+ right; apply Heq.
cut (Un_growing (fun n:nat => sum_f_R0 An n)).
- intro; set (l1 := sum_f_R0 An N) in r.
+ intro; set (l1 := sum_f_R0 An N) in Hgt.
unfold Un_cv in H; cut (0 < l1 - l).
intro; elim (H _ H2); intros.
set (N0 := max x N); cut (N0 >= x)%nat.
@@ -522,21 +514,21 @@ Proof.
intro; unfold R_dist in H5; rewrite Rabs_right in H5.
cut (sum_f_R0 An N0 < l1).
intro; elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H7 H6)).
- apply Rplus_lt_reg_r with (- l).
+ apply Rplus_lt_reg_l with (- l).
do 2 rewrite (Rplus_comm (- l)).
apply H5.
apply Rle_ge; apply Rplus_le_reg_l with l.
rewrite Rplus_0_r; replace (l + (sum_f_R0 An N0 - l)) with (sum_f_R0 An N0);
[ idtac | ring ]; apply Rle_trans with l1.
- left; apply r.
+ left; apply Hgt.
apply H6.
unfold l1; apply Rge_le;
apply (growing_prop (fun k:nat => sum_f_R0 An k)).
apply H1.
unfold ge, N0; apply le_max_r.
unfold ge, N0; apply le_max_l.
- apply Rplus_lt_reg_r with l; rewrite Rplus_0_r;
- replace (l + (l1 - l)) with l1; [ apply r | ring ].
+ apply Rplus_lt_reg_l with l; rewrite Rplus_0_r;
+ replace (l + (l1 - l)) with l1; [ apply Hgt | ring ].
unfold Un_growing; intro; simpl;
pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r;
apply Rplus_le_compat_l; apply H0.
@@ -549,10 +541,9 @@ Lemma sum_cv_maj :
Un_cv (fun n:nat => sum_f_R0 An n) l2 ->
(forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2.
Proof.
- intros; case (total_order_T (Rabs l1) l2); intro.
- elim s; intro.
- left; apply a.
- right; apply b.
+ intros; destruct (total_order_T (Rabs l1) l2) as [[Hlt|Heq]|Hgt].
+ left; apply Hlt.
+ right; apply Heq.
cut (forall n0:nat, Rabs (SP fn n0 x) <= sum_f_R0 An n0).
intro; cut (0 < (Rabs l1 - l2) / 2).
intro; unfold Un_cv in H, H0.
@@ -568,17 +559,17 @@ Proof.
intro; assert (H11 := H2 N).
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H10)).
apply Rlt_trans with ((Rabs l1 + l2) / 2); assumption.
- case (Rcase_abs (Rabs l1 - Rabs (SP fn N x))); intro.
+ destruct (Rcase_abs (Rabs l1 - Rabs (SP fn N x))) as [Hlt|Hge].
apply Rlt_trans with (Rabs l1).
apply Rmult_lt_reg_l with 2.
prove_sup0.
unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc;
rewrite <- Rinv_l_sym.
- rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply r.
+ rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply Hgt.
discrR.
- apply (Rminus_lt _ _ r0).
- rewrite (Rabs_right _ r0) in H7.
- apply Rplus_lt_reg_r with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)).
+ apply (Rminus_lt _ _ Hlt).
+ rewrite (Rabs_right _ Hge) in H7.
+ apply Rplus_lt_reg_l with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)).
replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with
(Rabs l1 - Rabs (SP fn N x)).
unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
@@ -586,18 +577,18 @@ Proof.
unfold Rdiv; rewrite Rmult_plus_distr_r;
rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l;
repeat rewrite (Rmult_comm (/ 2)); pattern (Rabs l1) at 1;
- rewrite double_var; unfold Rdiv; ring.
- case (Rcase_abs (sum_f_R0 An N - l2)); intro.
+ rewrite double_var; unfold Rdiv in |- *; ring.
+ destruct (Rcase_abs (sum_f_R0 An N - l2)) as [Hlt|Hge].
apply Rlt_trans with l2.
- apply (Rminus_lt _ _ r0).
+ apply (Rminus_lt _ _ Hlt).
apply Rmult_lt_reg_l with 2.
prove_sup0.
rewrite (double l2); unfold Rdiv; rewrite (Rmult_comm 2);
rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l;
- apply r.
+ apply Hgt.
discrR.
- rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_r with (- l2).
+ rewrite (Rabs_right _ Hge) in H6; apply Rplus_lt_reg_l with (- l2).
replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2).
rewrite Rplus_comm; apply H6.
unfold Rdiv; rewrite <- (Rmult_comm (/ 2));
@@ -610,9 +601,9 @@ Proof.
apply H4; unfold ge, N; apply le_max_l.
apply H5; unfold ge, N; apply le_max_r.
unfold Rdiv; apply Rmult_lt_0_compat.
- apply Rplus_lt_reg_r with l2.
+ apply Rplus_lt_reg_l with l2.
rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1);
- [ apply r | ring ].
+ [ apply Hgt | ring ].
apply Rinv_0_lt_compat; prove_sup0.
intros; induction n0 as [| n0 Hrecn0].
unfold SP; simpl; apply H1.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:59:25 +0000