summaryrefslogtreecommitdiff
path: root/theories/Reals/PSeries_reg.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/Reals/PSeries_reg.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Reals/PSeries_reg.v')
-rw-r--r--theories/Reals/PSeries_reg.v29
1 files changed, 13 insertions, 16 deletions
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 64b8e0af..e122a26a 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -6,14 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PSeries_reg.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PSeries_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Require Import Max.
-Require Import Even. Open Local Scope R_scope.
+Require Import Even.
+Open Local Scope R_scope.
Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.
@@ -28,25 +29,21 @@ Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
(** Normal convergence *)
Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type :=
- sigT
- (fun An:nat -> R =>
- sigT
- (fun l:R =>
+ { An:nat -> R &
+ { l:R |
Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\
- (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n))).
+ (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n) } }.
Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r.
Definition SFL (fn:nat -> R -> R)
- (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
- (y:R) : R := match cv y with
- | existT a b => a
- end.
+ (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l })
+ (y:R) : R := let (a,_) := cv y in a.
(** In a complete space, normal convergence implies uniform convergence *)
Lemma CVN_CVU :
forall (fn:nat -> R -> R)
- (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
+ (cv:forall x:R, {l:R | Un_cv (fun N:nat => SP fn N x) l })
(r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.
Proof.
intros; unfold CVU in |- *; intros.
@@ -193,7 +190,7 @@ Qed.
(** Continuity and normal convergence *)
Lemma SFL_continuity_pt :
forall (fn:nat -> R -> R)
- (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
+ (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l })
(r:posreal),
CVN_r fn r ->
(forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y) ->
@@ -210,7 +207,7 @@ Qed.
Lemma SFL_continuity :
forall (fn:nat -> R -> R)
- (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)),
+ (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }),
CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv).
Proof.
intros; unfold continuity in |- *; intro.
@@ -229,7 +226,7 @@ Qed.
(** As R is complete, normal convergence implies that (fn) is simply-uniformly convergent *)
Lemma CVN_R_CVS :
forall fn:nat -> R -> R,
- CVN_R fn -> forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l).
+ CVN_R fn -> forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }.
Proof.
intros; apply R_complete.
unfold SP in |- *; set (An := fun N:nat => fn N x).
@@ -248,7 +245,7 @@ Proof.
rewrite Rminus_0_r.
pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
apply Rlt_0_1.
- apply existT with l.
+ exists l.
cut (forall n:nat, 0 <= Bn n).
intro; unfold Un_cv in H3; unfold Un_cv in |- *; intros.
elim (H3 _ H6); intros.