diff options
Diffstat (limited to 'theories7/Reals/Rcomplete.v')
| -rw-r--r-- | theories7/Reals/Rcomplete.v | 175 |
1 files changed, 175 insertions, 0 deletions
diff --git a/theories7/Reals/Rcomplete.v b/theories7/Reals/Rcomplete.v new file mode 100644 index 00000000..5985a382 --- /dev/null +++ b/theories7/Reals/Rcomplete.v @@ -0,0 +1,175 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Rcomplete.v,v 1.1.2.1 2004/07/16 19:31:34 herbelin Exp $ i*) + +Require Rbase. +Require Rfunctions. +Require Rseries. +Require SeqProp. +Require Max. +V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. +Open Local Scope R_scope. + +(****************************************************) +(* R is complete : *) +(* Each sequence which satisfies *) +(* the Cauchy's criterion converges *) +(* *) +(* Proof with adjacent sequences (Vn and Wn) *) +(****************************************************) + +Theorem R_complete : (Un:nat->R) (Cauchy_crit Un) -> (sigTT R [l:R](Un_cv Un l)). +Intros. +Pose Vn := (sequence_minorant Un (cauchy_min Un H)). +Pose Wn := (sequence_majorant Un (cauchy_maj Un H)). +Assert H0 := (maj_cv Un H). +Fold Wn in H0. +Assert H1 := (min_cv Un H). +Fold Vn in H1. +Elim H0; Intros. +Elim H1; Intros. +Cut x==x0. +Intros. +Apply existTT with x. +Rewrite <- H2 in p0. +Unfold Un_cv. +Intros. +Unfold Un_cv in p; Unfold Un_cv in p0. +Cut ``0<eps/3``. +Intro. +Elim (p ``eps/3`` H4); Intros. +Elim (p0 ``eps/3`` H4); Intros. +Exists (max x1 x2). +Intros. +Unfold R_dist. +Apply Rle_lt_trans with ``(Rabsolu ((Un n)-(Vn n)))+(Rabsolu ((Vn n)-x))``. +Replace ``(Un n)-x`` with ``((Un n)-(Vn n))+((Vn n)-x)``; [Apply Rabsolu_triang | Ring]. +Apply Rle_lt_trans with ``(Rabsolu ((Wn n)-(Vn n)))+(Rabsolu ((Vn n)-x))``. +Do 2 Rewrite <- (Rplus_sym ``(Rabsolu ((Vn n)-x))``). +Apply Rle_compatibility. +Repeat Rewrite Rabsolu_right. +Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-(Vn n)``); Apply Rle_compatibility. +Assert H8 := (Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). +Fold Vn Wn in H8. +Elim (H8 n); Intros. +Assumption. +Apply Rle_sym1. +Unfold Rminus; Apply Rle_anti_compatibility with (Vn n). +Rewrite Rplus_Or. +Replace ``(Vn n)+((Wn n)+ -(Vn n))`` with (Wn n); [Idtac | Ring]. +Assert H8 := (Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). +Fold Vn Wn in H8. +Elim (H8 n); Intros. +Apply Rle_trans with (Un n); Assumption. +Apply Rle_sym1. +Unfold Rminus; Apply Rle_anti_compatibility with (Vn n). +Rewrite Rplus_Or. +Replace ``(Vn n)+((Un n)+ -(Vn n))`` with (Un n); [Idtac | Ring]. +Assert H8 := (Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). +Fold Vn Wn in H8. +Elim (H8 n); Intros. +Assumption. +Apply Rle_lt_trans with ``(Rabsolu ((Wn n)-x))+(Rabsolu (x-(Vn n)))+(Rabsolu ((Vn n)-x))``. +Do 2 Rewrite <- (Rplus_sym ``(Rabsolu ((Vn n)-x))``). +Apply Rle_compatibility. +Replace ``(Wn n)-(Vn n)`` with ``((Wn n)-x)+(x-(Vn n))``; [Apply Rabsolu_triang | Ring]. +Apply Rlt_le_trans with ``eps/3+eps/3+eps/3``. +Repeat Apply Rplus_lt. +Unfold R_dist in H5. +Apply H5. +Unfold ge; Apply le_trans with (max x1 x2). +Apply le_max_l. +Assumption. +Rewrite <- Rabsolu_Ropp. +Replace ``-(x-(Vn n))`` with ``(Vn n)-x``; [Idtac | Ring]. +Unfold R_dist in H6. +Apply H6. +Unfold ge; Apply le_trans with (max x1 x2). +Apply le_max_r. +Assumption. +Unfold R_dist in H6. +Apply H6. +Unfold ge; Apply le_trans with (max x1 x2). +Apply le_max_r. +Assumption. +Right. +Pattern 4 eps; Replace ``eps`` with ``3*eps/3``. +Ring. +Unfold Rdiv; Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; DiscrR. +Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. +Apply cond_eq. +Intros. +Cut ``0<eps/5``. +Intro. +Unfold Un_cv in p; Unfold Un_cv in p0. +Unfold R_dist in p; Unfold R_dist in p0. +Elim (p ``eps/5`` H3); Intros N1 H4. +Elim (p0 ``eps/5`` H3); Intros N2 H5. +Unfold Cauchy_crit in H. +Unfold R_dist in H. +Elim (H ``eps/5`` H3); Intros N3 H6. +Pose N := (max (max N1 N2) N3). +Apply Rle_lt_trans with ``(Rabsolu (x-(Wn N)))+(Rabsolu ((Wn N)-x0))``. +Replace ``x-x0`` with ``(x-(Wn N))+((Wn N)-x0)``; [Apply Rabsolu_triang | Ring]. +Apply Rle_lt_trans with ``(Rabsolu (x-(Wn N)))+(Rabsolu ((Wn N)-(Vn N)))+(Rabsolu (((Vn N)-x0)))``. +Rewrite Rplus_assoc. +Apply Rle_compatibility. +Replace ``(Wn N)-x0`` with ``((Wn N)-(Vn N))+((Vn N)-x0)``; [Apply Rabsolu_triang | Ring]. +Replace ``eps`` with ``eps/5+3*eps/5+eps/5``. +Repeat Apply Rplus_lt. +Rewrite <- Rabsolu_Ropp. +Replace ``-(x-(Wn N))`` with ``(Wn N)-x``; [Apply H4 | Ring]. +Unfold ge N. +Apply le_trans with (max N1 N2); Apply le_max_l. +Unfold Wn Vn. +Unfold sequence_majorant sequence_minorant. +Assert H7 := (approx_maj [k:nat](Un (plus N k)) (maj_ss Un N (cauchy_maj Un H))). +Assert H8 := (approx_min [k:nat](Un (plus N k)) (min_ss Un N (cauchy_min Un H))). +Cut (Wn N)==(majorant ([k:nat](Un (plus N k))) (maj_ss Un N (cauchy_maj Un H))). +Cut (Vn N)==(minorant ([k:nat](Un (plus N k))) (min_ss Un N (cauchy_min Un H))). +Intros. +Rewrite <- H9; Rewrite <- H10. +Rewrite <- H9 in H8. +Rewrite <- H10 in H7. +Elim (H7 ``eps/5`` H3); Intros k2 H11. +Elim (H8 ``eps/5`` H3); Intros k1 H12. +Apply Rle_lt_trans with ``(Rabsolu ((Wn N)-(Un (plus N k2))))+(Rabsolu ((Un (plus N k2))-(Vn N)))``. +Replace ``(Wn N)-(Vn N)`` with ``((Wn N)-(Un (plus N k2)))+((Un (plus N k2))-(Vn N))``; [Apply Rabsolu_triang | Ring]. +Apply Rle_lt_trans with ``(Rabsolu ((Wn N)-(Un (plus N k2))))+(Rabsolu ((Un (plus N k2))-(Un (plus N k1))))+(Rabsolu ((Un (plus N k1))-(Vn N)))``. +Rewrite Rplus_assoc. +Apply Rle_compatibility. +Replace ``(Un (plus N k2))-(Vn N)`` with ``((Un (plus N k2))-(Un (plus N k1)))+((Un (plus N k1))-(Vn N))``; [Apply Rabsolu_triang | Ring]. +Replace ``3*eps/5`` with ``eps/5+eps/5+eps/5``; [Repeat Apply Rplus_lt | Ring]. +Assumption. +Apply H6. +Unfold ge. +Apply le_trans with N. +Unfold N; Apply le_max_r. +Apply le_plus_l. +Unfold ge. +Apply le_trans with N. +Unfold N; Apply le_max_r. +Apply le_plus_l. +Rewrite <- Rabsolu_Ropp. +Replace ``-((Un (plus N k1))-(Vn N))`` with ``(Vn N)-(Un (plus N k1))``; [Assumption | Ring]. +Reflexivity. +Reflexivity. +Apply H5. +Unfold ge; Apply le_trans with (max N1 N2). +Apply le_max_r. +Unfold N; Apply le_max_l. +Pattern 4 eps; Replace ``eps`` with ``5*eps/5``. +Ring. +Unfold Rdiv; Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m. +DiscrR. +Unfold Rdiv; Apply Rmult_lt_pos. +Assumption. +Apply Rlt_Rinv. +Sup0; Try Apply lt_O_Sn. +Qed. |