← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Reals/PSeries_reg.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Reals/PSeries_reg.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: PSeries_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import SeqSeries.
 
14
Require Import Ranalysis1.
 
15
Require Import Max.
 
16
Require Import Even.
 
17
Open Local Scope R_scope.
 
18
 
 
19
Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.
 
20
 
 
21
(** Uniform convergence *)
 
22
Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R) 
 
23
  (r:posreal) : Prop :=
 
24
  forall eps:R,
 
25
    0 < eps ->
 
26
    exists N : nat,
 
27
      (forall (n:nat) (y:R),
 
28
        (N <= n)%nat -> Boule x r y -> Rabs (f y - fn n y) < eps). 
 
29
 
 
30
(** Normal convergence *)
 
31
Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type :=
 
32
  { An:nat -> R &
 
33
    { l:R |
 
34
      Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\
 
35
      (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n) } }.
 
36
 
 
37
Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r.
 
38
 
 
39
Definition SFL (fn:nat -> R -> R)
 
40
  (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) 
 
41
  (y:R) : R := let (a,_) := cv y in a.
 
42
 
 
43
(** In a complete space, normal convergence implies uniform convergence *)
 
44
Lemma CVN_CVU :
 
45
  forall (fn:nat -> R -> R)
 
46
    (cv:forall x:R, {l:R | Un_cv (fun N:nat => SP fn N x) l })
 
47
    (r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.
 
48
Proof.
 
49
  intros; unfold CVU in |- *; intros.
 
50
  unfold CVN_r in X.
 
51
  elim X; intros An X0.
 
52
  elim X0; intros s H0.
 
53
  elim H0; intros.
 
54
  cut (Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n - s) 0).
 
55
  intro; unfold Un_cv in H3.
 
56
  elim (H3 eps H); intros N0 H4.
 
57
  exists N0; intros.
 
58
  apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => Rabs (An k)) n - s)).
 
59
  rewrite <- (Rabs_Ropp (sum_f_R0 (fun k:nat => Rabs (An k)) n - s));
 
60
    rewrite Ropp_minus_distr';
 
61
      rewrite (Rabs_right (s - sum_f_R0 (fun k:nat => Rabs (An k)) n)).
 
62
  eapply sum_maj1.
 
63
  unfold SFL in |- *; case (cv y); intro.
 
64
  trivial.
 
65
  apply H1.
 
66
  intro; elim H0; intros.
 
67
  rewrite (Rabs_right (An n0)).
 
68
  apply H8; apply H6.
 
69
  apply Rle_ge; apply Rle_trans with (Rabs (fn n0 y)).
 
70
  apply Rabs_pos.
 
71
  apply H8; apply H6.
 
72
  apply Rle_ge;
 
73
    apply Rplus_le_reg_l with (sum_f_R0 (fun k:nat => Rabs (An k)) n).
 
74
  rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm s);
 
75
    rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l;
 
76
      apply sum_incr.
 
77
  apply H1.
 
78
  intro; apply Rabs_pos.
 
79
  unfold R_dist in H4; unfold Rminus in H4; rewrite Ropp_0 in H4.
 
80
  assert (H7 := H4 n H5).
 
81
  rewrite Rplus_0_r in H7; apply H7.
 
82
  unfold Un_cv in H1; unfold Un_cv in |- *; intros.
 
83
  elim (H1 _ H3); intros.
 
84
  exists x; intros.
 
85
  unfold R_dist in |- *; unfold R_dist in H4.
 
86
  rewrite Rminus_0_r; apply H4; assumption.
 
87
Qed.
 
88
 
 
89
(** Each limit of a sequence of functions which converges uniformly is continue *)
 
90
Lemma CVU_continuity :
 
91
  forall (fn:nat -> R -> R) (f:R -> R) (x:R) (r:posreal),
 
92
    CVU fn f x r ->
 
93
    (forall (n:nat) (y:R), Boule x r y -> continuity_pt (fn n) y) ->
 
94
    forall y:R, Boule x r y -> continuity_pt f y.
 
95
Proof.
 
96
  intros; unfold continuity_pt in |- *; unfold continue_in in |- *;
 
97
    unfold limit1_in in |- *; unfold limit_in in |- *; 
 
98
      simpl in |- *; unfold R_dist in |- *; intros.
 
99
  unfold CVU in H.
 
100
  cut (0 < eps / 3);
 
101
    [ intro
 
102
      | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
103
        [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
 
104
  elim (H _ H3); intros N0 H4.
 
105
  assert (H5 := H0 N0 y H1).
 
106
  cut (exists del : posreal, (forall h:R, Rabs h < del -> Boule x r (y + h))).
 
107
  intro.
 
108
  elim H6; intros del1 H7.
 
109
  unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5;
 
110
    unfold limit_in in H5; simpl in H5; unfold R_dist in H5.
 
111
  elim (H5 _ H3); intros del2 H8.
 
112
  set (del := Rmin del1 del2).
 
113
  exists del; intros.
 
114
  split.
 
115
  unfold del in |- *; unfold Rmin in |- *; case (Rle_dec del1 del2); intro.
 
116
  apply (cond_pos del1).
 
117
  elim H8; intros; assumption.
 
118
  intros;
 
119
    apply Rle_lt_trans with (Rabs (f x0 - fn N0 x0) + Rabs (fn N0 x0 - f y)).
 
120
  replace (f x0 - f y) with (f x0 - fn N0 x0 + (fn N0 x0 - f y));
 
121
  [ apply Rabs_triang | ring ].
 
122
  apply Rle_lt_trans with
 
123
    (Rabs (f x0 - fn N0 x0) + Rabs (fn N0 x0 - fn N0 y) + Rabs (fn N0 y - f y)).
 
124
  rewrite Rplus_assoc; apply Rplus_le_compat_l.
 
125
  replace (fn N0 x0 - f y) with (fn N0 x0 - fn N0 y + (fn N0 y - f y));
 
126
  [ apply Rabs_triang | ring ].
 
127
  replace eps with (eps / 3 + eps / 3 + eps / 3).
 
128
  repeat apply Rplus_lt_compat.
 
129
  apply H4.
 
130
  apply le_n.
 
131
  replace x0 with (y + (x0 - y)); [ idtac | ring ]; apply H7.
 
132
  elim H9; intros.
 
133
  apply Rlt_le_trans with del.
 
134
  assumption.
 
135
  unfold del in |- *; apply Rmin_l.
 
136
  elim H8; intros.
 
137
  apply H11.
 
138
  split.
 
139
  elim H9; intros; assumption.
 
140
  elim H9; intros; apply Rlt_le_trans with del.
 
141
  assumption.
 
142
  unfold del in |- *; apply Rmin_r.
 
143
  rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr'; apply H4.
 
144
  apply le_n.
 
145
  assumption.
 
146
  apply Rmult_eq_reg_l with 3.
 
147
  do 2 rewrite Rmult_plus_distr_l; unfold Rdiv in |- *; rewrite <- Rmult_assoc;
 
148
    rewrite Rinv_r_simpl_m.
 
149
  ring.
 
150
  discrR.
 
151
  discrR.
 
152
  cut (0 < r - Rabs (x - y)).
 
153
  intro; exists (mkposreal _ H6).
 
154
  simpl in |- *; intros.
 
155
  unfold Boule in |- *; replace (y + h - x) with (h + (y - x));
 
156
    [ idtac | ring ]; apply Rle_lt_trans with (Rabs h + Rabs (y - x)).
 
157
  apply Rabs_triang.
 
158
  apply Rplus_lt_reg_r with (- Rabs (x - y)).
 
159
  rewrite <- (Rabs_Ropp (y - x)); rewrite Ropp_minus_distr'.
 
160
  replace (- Rabs (x - y) + r) with (r - Rabs (x - y)).
 
161
  replace (- Rabs (x - y) + (Rabs h + Rabs (x - y))) with (Rabs h).
 
162
  apply H7.
 
163
  ring.
 
164
  ring.
 
165
  unfold Boule in H1; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr';
 
166
    apply Rplus_lt_reg_r with (Rabs (y - x)).
 
167
  rewrite Rplus_0_r; replace (Rabs (y - x) + (r - Rabs (y - x))) with (pos r);
 
168
    [ apply H1 | ring ].
 
169
Qed.
 
170
 
 
171
(**********)
 
172
Lemma continuity_pt_finite_SF :
 
173
  forall (fn:nat -> R -> R) (N:nat) (x:R),
 
174
    (forall n:nat, (n <= N)%nat -> continuity_pt (fn n) x) ->
 
175
    continuity_pt (fun y:R => sum_f_R0 (fun k:nat => fn k y) N) x.
 
176
Proof.
 
177
  intros; induction  N as [| N HrecN].
 
178
  simpl in |- *; apply (H 0%nat); apply le_n.
 
179
  simpl in |- *;
 
180
    replace (fun y:R => sum_f_R0 (fun k:nat => fn k y) N + fn (S N) y) with
 
181
    ((fun y:R => sum_f_R0 (fun k:nat => fn k y) N) + (fun y:R => fn (S N) y))%F;
 
182
    [ idtac | reflexivity ].
 
183
  apply continuity_pt_plus.
 
184
  apply HrecN.
 
185
  intros; apply H.
 
186
  apply le_trans with N; [ assumption | apply le_n_Sn ].
 
187
  apply (H (S N)); apply le_n.
 
188
Qed.
 
189
 
 
190
(** Continuity and normal convergence *)
 
191
Lemma SFL_continuity_pt :
 
192
  forall (fn:nat -> R -> R)
 
193
    (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l })
 
194
    (r:posreal),
 
195
    CVN_r fn r ->
 
196
    (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y) ->
 
197
    forall y:R, Boule 0 r y -> continuity_pt (SFL fn cv) y.
 
198
Proof.
 
199
  intros; eapply CVU_continuity.
 
200
  apply CVN_CVU.
 
201
  apply X.
 
202
  intros; unfold SP in |- *; apply continuity_pt_finite_SF.
 
203
  intros; apply H.
 
204
  apply H1.
 
205
  apply H0.
 
206
Qed.
 
207
 
 
208
Lemma SFL_continuity :
 
209
  forall (fn:nat -> R -> R)
 
210
    (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }),
 
211
    CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv).
 
212
Proof.
 
213
  intros; unfold continuity in |- *; intro.
 
214
  cut (0 < Rabs x + 1);
 
215
    [ intro | apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ] ].
 
216
  cut (Boule 0 (mkposreal _ H0) x).
 
217
  intro; eapply SFL_continuity_pt with (mkposreal _ H0).
 
218
  apply X.
 
219
  intros; apply (H n y).
 
220
  apply H1.
 
221
  unfold Boule in |- *; simpl in |- *; rewrite Rminus_0_r;
 
222
    pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; 
 
223
      apply Rplus_lt_compat_l; apply Rlt_0_1.
 
224
Qed.
 
225
 
 
226
(** As R is complete, normal convergence implies that (fn) is simply-uniformly convergent *) 
 
227
Lemma CVN_R_CVS :
 
228
  forall fn:nat -> R -> R,
 
229
    CVN_R fn -> forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }.
 
230
Proof.
 
231
  intros; apply R_complete.
 
232
  unfold SP in |- *; set (An := fun N:nat => fn N x).
 
233
  change (Cauchy_crit_series An) in |- *.
 
234
  apply cauchy_abs.
 
235
  unfold Cauchy_crit_series in |- *; apply CV_Cauchy.
 
236
  unfold CVN_R in X; cut (0 < Rabs x + 1).
 
237
  intro; assert (H0 := X (mkposreal _ H)).
 
238
  unfold CVN_r in H0; elim H0; intros Bn H1.
 
239
  elim H1; intros l H2.
 
240
  elim H2; intros.
 
241
  apply Rseries_CV_comp with Bn.
 
242
  intro; split.
 
243
  apply Rabs_pos.
 
244
  unfold An in |- *; apply H4; unfold Boule in |- *; simpl in |- *;
 
245
    rewrite Rminus_0_r.
 
246
  pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
 
247
    apply Rlt_0_1.
 
248
  exists l.
 
249
  cut (forall n:nat, 0 <= Bn n).
 
250
  intro; unfold Un_cv in H3; unfold Un_cv in |- *; intros.
 
251
  elim (H3 _ H6); intros.
 
252
  exists x0; intros.
 
253
  replace (sum_f_R0 Bn n) with (sum_f_R0 (fun k:nat => Rabs (Bn k)) n).
 
254
  apply H7; assumption.
 
255
  apply sum_eq; intros; apply Rabs_right; apply Rle_ge; apply H5.
 
256
  intro; apply Rle_trans with (Rabs (An n)).
 
257
  apply Rabs_pos.
 
258
  unfold An in |- *; apply H4; unfold Boule in |- *; simpl in |- *;
 
259
    rewrite Rminus_0_r; pattern (Rabs x) at 1 in |- *; 
 
260
      rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1.
 
261
  apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ].
 
262
Qed.