1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
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.
|
