blob: 77cb560ccbecbf6b2679a21eaaf2314374bed723 (
plain)
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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import SeqProp.
Require Import Max.
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 :
forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .
Proof.
intros.
set (Vn := sequence_minorant Un (cauchy_min Un H)).
set (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.
exists x.
rewrite <- H2 in p0.
unfold Un_cv in |- *.
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 in |- *.
apply Rle_lt_trans with (Rabs (Un n - Vn n) + Rabs (Vn n - x)).
replace (Un n - x) with (Un n - Vn n + (Vn n - x));
[ apply Rabs_triang | ring ].
apply Rle_lt_trans with (Rabs (Wn n - Vn n) + Rabs (Vn n - x)).
do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
apply Rplus_le_compat_l.
repeat rewrite Rabs_right.
unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- Vn n));
apply Rplus_le_compat_l.
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_ge.
unfold Rminus in |- *; apply Rplus_le_reg_l with (Vn n).
rewrite Rplus_0_r.
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_ge.
unfold Rminus in |- *; apply Rplus_le_reg_l with (Vn n).
rewrite Rplus_0_r.
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 (Rabs (Wn n - x) + Rabs (x - Vn n) + Rabs (Vn n - x)).
do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
apply Rplus_le_compat_l.
replace (Wn n - Vn n) with (Wn n - x + (x - Vn n));
[ apply Rabs_triang | ring ].
apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3).
repeat apply Rplus_lt_compat.
unfold R_dist in H5.
apply H5.
unfold ge in |- *; apply le_trans with (max x1 x2).
apply le_max_l.
assumption.
rewrite <- Rabs_Ropp.
replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ].
unfold R_dist in H6.
apply H6.
unfold ge in |- *; apply le_trans with (max x1 x2).
apply le_max_r.
assumption.
unfold R_dist in H6.
apply H6.
unfold ge in |- *; apply le_trans with (max x1 x2).
apply le_max_r.
assumption.
right.
pattern eps at 4 in |- *; replace eps with (3 * (eps / 3)).
ring.
unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR.
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_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.
set (N := max (max N1 N2) N3).
apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)).
replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ].
apply Rle_lt_trans with
(Rabs (x - Wn N) + Rabs (Wn N - Vn N) + Rabs (Vn N - x0)).
rewrite Rplus_assoc.
apply Rplus_le_compat_l.
replace (Wn N - x0) with (Wn N - Vn N + (Vn N - x0));
[ apply Rabs_triang | ring ].
replace eps with (eps / 5 + 3 * (eps / 5) + eps / 5).
repeat apply Rplus_lt_compat.
rewrite <- Rabs_Ropp.
replace (- (x - Wn N)) with (Wn N - x); [ apply H4 | ring ].
unfold ge, N in |- *.
apply le_trans with (max N1 N2); apply le_max_l.
unfold Wn, Vn in |- *.
unfold sequence_majorant, sequence_minorant in |- *.
assert
(H7 :=
approx_maj (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
assert
(H8 :=
approx_min (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
cut
(Wn N =
majorant (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
cut
(Vn N =
minorant (fun k:nat => Un (N + k)%nat) (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
(Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)).
replace (Wn N - Vn N) with
(Wn N - Un (N + k2)%nat + (Un (N + k2)%nat - Vn N));
[ apply Rabs_triang | ring ].
apply Rle_lt_trans with
(Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Un (N + k1)%nat) +
Rabs (Un (N + k1)%nat - Vn N)).
rewrite Rplus_assoc.
apply Rplus_le_compat_l.
replace (Un (N + k2)%nat - Vn N) with
(Un (N + k2)%nat - Un (N + k1)%nat + (Un (N + k1)%nat - Vn N));
[ apply Rabs_triang | ring ].
replace (3 * (eps / 5)) with (eps / 5 + eps / 5 + eps / 5);
[ repeat apply Rplus_lt_compat | ring ].
assumption.
apply H6.
unfold ge in |- *.
apply le_trans with N.
unfold N in |- *; apply le_max_r.
apply le_plus_l.
unfold ge in |- *.
apply le_trans with N.
unfold N in |- *; apply le_max_r.
apply le_plus_l.
rewrite <- Rabs_Ropp.
replace (- (Un (N + k1)%nat - Vn N)) with (Vn N - Un (N + k1)%nat);
[ assumption | ring ].
reflexivity.
reflexivity.
apply H5.
unfold ge in |- *; apply le_trans with (max N1 N2).
apply le_max_r.
unfold N in |- *; apply le_max_l.
pattern eps at 4 in |- *; replace eps with (5 * (eps / 5)).
ring.
unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
discrR.
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
assumption.
apply Rinv_0_lt_compat.
prove_sup0; try apply lt_O_Sn.
Qed.
|
