summaryrefslogtreecommitdiff
path: root/theories/Reals
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals')
-rw-r--r--theories/Reals/PartSum.v7
-rw-r--r--theories/Reals/RIneq.v4
-rw-r--r--theories/Reals/RiemannInt.v16
3 files changed, 13 insertions, 14 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 13070bde..6087d3f2 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PartSum.v,v 1.11.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
+(*i $Id: PartSum.v,v 1.11.2.2 2005/07/13 22:28:30 herbelin Exp $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -489,8 +489,7 @@ elim s; intro.
left; apply a.
right; apply b.
cut (Un_growing (fun n:nat => sum_f_R0 An n)).
-intro; set (l1 := sum_f_R0 An N).
-fold l1 in r.
+intro; set (l1 := sum_f_R0 An N) in r.
unfold Un_cv in H; cut (0 < l1 - l).
intro; elim (H _ H2); intros.
set (N0 := max x N); cut (N0 >= x)%nat.
@@ -600,4 +599,4 @@ apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)).
do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))).
apply Rplus_le_compat_l; apply Hrecn0.
apply Rplus_le_compat_l; apply H1.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index a23f53ff..5da14193 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RIneq.v,v 1.23.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
+(*i $Id: RIneq.v,v 1.23.2.2 2005/03/29 15:35:13 herbelin Exp $ i*)
(***************************************************************************)
(** Basic lemmas for the classical reals numbers *)
@@ -1382,7 +1382,7 @@ Qed.
(**********)
Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
-intros z1 z2 H; apply Zlt_O_minus_lt.
+intros z1 z2 H; apply Zlt_0_minus_lt.
apply lt_O_IZR.
rewrite <- Z_R_minus.
exact (Rgt_minus (IZR z2) (IZR z1) H).
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 51323ac4..ce33afdb 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RiemannInt.v,v 1.18.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
+(*i $Id: RiemannInt.v,v 1.18.2.2 2005/07/13 23:18:52 herbelin Exp $ i*)
Require Import Rfunctions.
Require Import SeqSeries.
@@ -1593,13 +1593,12 @@ Lemma RiemannInt_P17 :
intro f; intros; unfold RiemannInt in |- *;
case (RiemannInt_exists pr1 RinvN RinvN_cv);
case (RiemannInt_exists pr2 RinvN RinvN_cv); intros;
- set (phi1 := phi_sequence RinvN pr1);
+ set (phi1 := phi_sequence RinvN pr1) in u0;
set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N)));
apply Rle_cv_lim with
(fun N:nat => Rabs (RiemannInt_SF (phi1 N)))
(fun N:nat => RiemannInt_SF (phi2 N)).
intro; unfold phi2 in |- *; apply StepFun_P34; assumption.
-fold phi1 in u0;
apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0);
try assumption.
apply Rcontinuity_abs.
@@ -2372,10 +2371,11 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0;
left; apply (cond_pos (RinvN n)).
exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3;
intros; unfold R_dist in |- *; unfold Rminus in |- *;
- rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n);
- fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n);
- fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n);
- fold phi2 in H1; assert (H10 : IsStepFun phi3 a b).
+ rewrite Ropp_0; rewrite Rplus_0_r;
+ set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *;
+ set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *;
+ set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *;
+ assert (H10 : IsStepFun phi3 a b).
apply StepFun_P44 with c.
apply (pre phi3).
split; assumption.
@@ -2442,7 +2442,7 @@ rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr;
replace (phi3 x + -1 * phi2 x) with (phi3 x - f x + (f x - phi2 x));
[ apply Rabs_triang | ring ].
apply Rplus_le_compat.
-fold phi3 in H1; apply H1.
+apply H1.
elim H14; intros; split.
replace (Rmin a c) with a.
apply Rle_trans with b; try assumption.