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
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
|
(************************************************************************)
(* 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: Rseries.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Import Rbase.
Require Import Rfunctions.
Require Import Classical.
Require Import Compare.
Open Local Scope R_scope.
Implicit Type r : R.
(* classical is needed for [Un_cv_crit] *)
(*********************************************************)
(** * Definition of sequence and properties *)
(* *)
(*********************************************************)
Section sequence.
(*********)
Variable Un : nat -> R.
(*********)
Boxed Fixpoint Rmax_N (N:nat) : R :=
match N with
| O => Un 0
| S n => Rmax (Un (S n)) (Rmax_N n)
end.
(*********)
Definition EUn r : Prop := exists i : nat, r = Un i.
(*********)
Definition Un_cv (l:R) : Prop :=
forall eps:R,
eps > 0 ->
exists N : nat, (forall n:nat, (n >= N)%nat -> R_dist (Un n) l < eps).
(*********)
Definition Cauchy_crit : Prop :=
forall eps:R,
eps > 0 ->
exists N : nat,
(forall n m:nat,
(n >= N)%nat -> (m >= N)%nat -> R_dist (Un n) (Un m) < eps).
(*********)
Definition Un_growing : Prop := forall n:nat, Un n <= Un (S n).
(*********)
Lemma EUn_noempty : exists r : R, EUn r.
Proof.
unfold EUn in |- *; split with (Un 0); split with 0%nat; trivial.
Qed.
(*********)
Lemma Un_in_EUn : forall n:nat, EUn (Un n).
Proof.
intro; unfold EUn in |- *; split with n; trivial.
Qed.
(*********)
Lemma Un_bound_imp :
forall x:R, (forall n:nat, Un n <= x) -> is_upper_bound EUn x.
Proof.
intros; unfold is_upper_bound in |- *; intros; unfold EUn in H0; elim H0;
clear H0; intros; generalize (H x1); intro; rewrite <- H0 in H1;
trivial.
Qed.
(*********)
Lemma growing_prop :
forall n m:nat, Un_growing -> (n >= m)%nat -> Un n >= Un m.
Proof.
double induction n m; intros.
unfold Rge in |- *; right; trivial.
elimtype False; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
cut (n0 >= 0)%nat.
generalize H0; intros; unfold Un_growing in H0;
apply
(Rge_trans (Un (S n0)) (Un n0) (Un 0) (Rle_ge (Un n0) (Un (S n0)) (H0 n0))
(H 0%nat H2 H3)).
elim n0; auto.
elim (lt_eq_lt_dec n1 n0); intro y.
elim y; clear y; intro y.
unfold ge in H2; generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2)); intro;
elimtype False; auto.
rewrite y; unfold Rge in |- *; right; trivial.
unfold ge in H0; generalize (H0 (S n0) H1 (lt_le_S n0 n1 y)); intro;
unfold Un_growing in H1;
apply
(Rge_trans (Un (S n1)) (Un n1) (Un (S n0))
(Rle_ge (Un n1) (Un (S n1)) (H1 n1)) H3).
Qed.
(** classical is needed: [not_all_not_ex] *)
(*********)
Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l.
Proof.
unfold Un_growing, Un_cv in |- *; intros;
generalize (completeness_weak EUn H0 EUn_noempty);
intro; elim H1; clear H1; intros; split with x; intros;
unfold is_lub in H1; unfold bound in H0; unfold is_upper_bound in H0, H1;
elim H0; clear H0; intros; elim H1; clear H1; intros;
generalize (H3 x0 H0); intro; cut (forall n:nat, Un n <= x);
intro.
cut (exists N : nat, x - eps < Un N).
intro; elim H6; clear H6; intros; split with x1.
intros; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps).
unfold Rgt in H2;
apply (Rle_lt_trans (Un n - x) 0 eps (Rle_minus (Un n) x (H5 n)) H2).
fold Un_growing in H; generalize (growing_prop n x1 H H7); intro;
generalize
(Rlt_le_trans (x - eps) (Un x1) (Un n) H6 (Rge_le (Un n) (Un x1) H8));
intro; generalize (Rplus_lt_compat_l (- x) (x - eps) (Un n) H9);
unfold Rminus in |- *; rewrite <- (Rplus_assoc (- x) x (- eps));
rewrite (Rplus_comm (- x) (Un n)); fold (Un n - x) in |- *;
rewrite Rplus_opp_l; rewrite (let (H1, H2) := Rplus_ne (- eps) in H2);
trivial.
cut (~ (forall N:nat, x - eps >= Un N)).
intro; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)); red in |- *;
intro; red in H6; elim H6; clear H6; intro;
apply (Rnot_lt_ge (x - eps) (Un N) (H7 N)).
red in |- *; intro; cut (forall N:nat, Un N <= x - eps).
intro; generalize (Un_bound_imp (x - eps) H7); intro;
unfold is_upper_bound in H8; generalize (H3 (x - eps) H8);
intro; generalize (Rle_minus x (x - eps) H9); unfold Rminus in |- *;
rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; rewrite Rplus_opp_r;
rewrite (let (H1, H2) := Rplus_ne (- - eps) in H2);
rewrite Ropp_involutive; intro; unfold Rgt in H2;
generalize (Rgt_not_le eps 0 H2); intro; auto.
intro; elim (H6 N); intro; unfold Rle in |- *.
left; unfold Rgt in H7; assumption.
right; auto.
apply (H1 (Un n) (Un_in_EUn n)).
Qed.
(*********)
Lemma finite_greater :
forall N:nat, exists M : R, (forall n:nat, (n <= N)%nat -> Un n <= M).
Proof.
intro; induction N as [| N HrecN].
split with (Un 0); intros; rewrite (le_n_O_eq n H);
apply (Req_le (Un n) (Un n) (refl_equal (Un n))).
elim HrecN; clear HrecN; intros; split with (Rmax (Un (S N)) x); intros;
elim (Rmax_Rle (Un (S N)) x (Un n)); intros; clear H1;
inversion H0.
rewrite <- H1; rewrite <- H1 in H2;
apply
(H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (refl_equal (Un n))))).
apply (H2 (or_intror (Un n <= Un (S N)) (H n H3))).
Qed.
(*********)
Lemma cauchy_bound : Cauchy_crit -> bound EUn.
Proof.
unfold Cauchy_crit, bound in |- *; intros; unfold is_upper_bound in |- *;
unfold Rgt in H; elim (H 1 Rlt_0_1); clear H; intros;
generalize (H x); intro; generalize (le_dec x); intro;
elim (finite_greater x); intros; split with (Rmax x0 (Un x + 1));
clear H; intros; unfold EUn in H; elim H; clear H;
intros; elim (H1 x2); clear H1; intro y.
unfold ge in H0; generalize (H0 x2 (le_n x) y); clear H0; intro;
rewrite <- H in H0; unfold R_dist in H0; elim (Rabs_def2 (Un x - x1) 1 H0);
clear H0; intros; elim (Rmax_Rle x0 (Un x + 1) x1);
intros; apply H4; clear H3 H4; right; clear H H0 y;
apply (Rlt_le x1 (Un x + 1)); generalize (Rlt_minus (-1) (Un x - x1) H1);
clear H1; intro; apply (Rminus_lt x1 (Un x + 1));
cut (-1 - (Un x - x1) = x1 - (Un x + 1));
[ intro; rewrite H0 in H; assumption | ring ].
generalize (H2 x2 y); clear H2 H0; intro; rewrite <- H in H0;
elim (Rmax_Rle x0 (Un x + 1) x1); intros; clear H1;
apply H2; left; assumption.
Qed.
End sequence.
(*****************************************************************)
(** * Definition of Power Series and properties *)
(* *)
(*****************************************************************)
Section Isequence.
(*********)
Variable An : nat -> R.
(*********)
Definition Pser (x l:R) : Prop := infinit_sum (fun n:nat => An n * x ^ n) l.
End Isequence.
Lemma GP_infinite :
forall x:R, Rabs x < 1 -> Pser (fun n:nat => 1) x (/ (1 - x)).
Proof.
intros; unfold Pser in |- *; unfold infinit_sum in |- *; intros;
elim (Req_dec x 0).
intros; exists 0%nat; intros; rewrite H1; rewrite Rminus_0_r; rewrite Rinv_1;
cut (sum_f_R0 (fun n0:nat => 1 * 0 ^ n0) n = 1).
intros; rewrite H3; rewrite R_dist_eq; auto.
elim n; simpl in |- *.
ring.
intros; rewrite H3; ring.
intro; cut (0 < eps * (Rabs (1 - x) * Rabs (/ x))).
intro; elim (pow_lt_1_zero x H (eps * (Rabs (1 - x) * Rabs (/ x))) H2);
intro N; intros; exists N; intros;
cut
(sum_f_R0 (fun n0:nat => 1 * x ^ n0) n = sum_f_R0 (fun n0:nat => x ^ n0) n).
intros; rewrite H5;
apply
(Rmult_lt_reg_l (Rabs (1 - x))
(R_dist (sum_f_R0 (fun n0:nat => x ^ n0) n) (/ (1 - x))) eps).
apply Rabs_pos_lt.
apply Rminus_eq_contra.
apply Rlt_dichotomy_converse.
right; unfold Rgt in |- *.
apply (Rle_lt_trans x (Rabs x) 1).
apply RRle_abs.
assumption.
unfold R_dist in |- *; rewrite <- Rabs_mult.
rewrite Rmult_minus_distr_l.
cut
((1 - x) * sum_f_R0 (fun n0:nat => x ^ n0) n =
- (sum_f_R0 (fun n0:nat => x ^ n0) n * (x - 1))).
intro; rewrite H6.
rewrite GP_finite.
rewrite Rinv_r.
cut (- (x ^ (n + 1) - 1) - 1 = - x ^ (n + 1)).
intro; rewrite H7.
rewrite Rabs_Ropp; cut ((n + 1)%nat = S n); auto.
intro H8; rewrite H8; simpl in |- *; rewrite Rabs_mult;
apply
(Rlt_le_trans (Rabs x * Rabs (x ^ n))
(Rabs x * (eps * (Rabs (1 - x) * Rabs (/ x)))) (
Rabs (1 - x) * eps)).
apply Rmult_lt_compat_l.
apply Rabs_pos_lt.
assumption.
auto.
cut
(Rabs x * (eps * (Rabs (1 - x) * Rabs (/ x))) =
Rabs x * Rabs (/ x) * (eps * Rabs (1 - x))).
clear H8; intros; rewrite H8; rewrite <- Rabs_mult; rewrite Rinv_r.
rewrite Rabs_R1; cut (1 * (eps * Rabs (1 - x)) = Rabs (1 - x) * eps).
intros; rewrite H9; unfold Rle in |- *; right; reflexivity.
ring.
assumption.
ring.
ring.
ring.
apply Rminus_eq_contra.
apply Rlt_dichotomy_converse.
right; unfold Rgt in |- *.
apply (Rle_lt_trans x (Rabs x) 1).
apply RRle_abs.
assumption.
ring; ring.
elim n; simpl in |- *.
ring.
intros; rewrite H5.
ring.
apply Rmult_lt_0_compat.
auto.
apply Rmult_lt_0_compat.
apply Rabs_pos_lt.
apply Rminus_eq_contra.
apply Rlt_dichotomy_converse.
right; unfold Rgt in |- *.
apply (Rle_lt_trans x (Rabs x) 1).
apply RRle_abs.
assumption.
apply Rabs_pos_lt.
apply Rinv_neq_0_compat.
assumption.
Qed.
|
