diff options
| -rw-r--r-- | theories/Reals/PartSum.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Rcomplete.v | 9 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt.v | 2 | ||||
| -rw-r--r-- | theories/Reals/SeqSeries.v | 2 |
4 files changed, 9 insertions, 8 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index cddcf54c16..737520552a 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -11,7 +11,7 @@ Require Rbase. Require Rfunctions. Require Rseries. -Require Rcomplet. +Require Rcomplete. Require Max. Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``. @@ -362,7 +362,7 @@ Qed. Lemma cv_cauchy_2 : (An:nat->R) (Cauchy_crit_series An) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). Intros. -Apply R_complet. +Apply R_complete. Unfold Cauchy_crit_series in H. Exact H. Qed. diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 80516e3075..8a653d1aaf 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -15,13 +15,14 @@ Require SeqProp. Require Max. (****************************************************) -(* R est complet : *) -(* Toute suite de Cauchy de (R,| |) converge *) +(* R is complete : *) +(* Each sequence which satisfies *) +(* the Cauchy's criterion converges *) (* *) -(* Preuve a l'aide des suites adjacentes Vn et Wn *) +(* Proof with adjacent sequences (Vn and Wn) *) (****************************************************) -Theorem R_complet : (Un:nat->R) (Cauchy_crit Un) -> (sigTT R [l:R](Un_cv Un l)). +Theorem R_complete : (Un:nat->R) (Cauchy_crit Un) -> (sigTT R [l:R](Un_cv Un l)). Intros. Pose Vn := (suite_minorant Un (cauchy_min Un H)). Pose Wn := (suite_majorant Un (cauchy_maj Un H)). diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 5ea7268f24..8a4379a834 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -42,7 +42,7 @@ Apply H1. Qed. Lemma RiemannInt_P2 : (f:R->R;a,b:R;un:nat->posreal;vn,wn:nat->(StepFun a b)) (Un_cv un R0) -> ``a<=b`` -> ((n:nat)((t:R)``(Rmin a b)<=t<=(Rmax a b)``->``(Rabsolu ((f t)-(vn n t)))<=(wn n t)``)/\``(Rabsolu (RiemannInt_SF (wn n)))<(un n)``) -> (sigTT ? [l:R](Un_cv [N:nat](RiemannInt_SF (vn N)) l)). -Intros; Apply R_complet; Unfold Un_cv in H; Unfold Cauchy_crit; Intros; Assert H3 : ``0<eps/2``. +Intros; Apply R_complete; Unfold Un_cv in H; Unfold Cauchy_crit; Intros; Assert H3 : ``0<eps/2``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. Elim (H ? H3); Intros N0 H4; Exists N0; Intros; Unfold R_dist; Unfold R_dist in H4; Elim (H1 n); Elim (H1 m); Intros; Replace ``(RiemannInt_SF (vn n))-(RiemannInt_SF (vn m))`` with ``(RiemannInt_SF (vn n))+(-1)*(RiemannInt_SF (vn m))``; [Idtac | Ring]; Rewrite <- StepFun_P30; Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 ``-1`` (vn n) (vn m)))))). Apply StepFun_P34; Assumption. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index bd80fb9bc0..421d6576e5 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Export Rseries. Require Export SeqProp. -Require Export Rcomplet. +Require Export Rcomplete. Require Export PartSum. Require Export AltSeries. Require Export Binomial. |