← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Cos_plus.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/Cos_plus.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: Cos_plus.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 Rtrigo_def.
 
15
Require Import Cos_rel.
 
16
Require Import Max.
 
17
Open Local Scope nat_scope.
 
18
Open Local Scope R_scope.
 
19
 
 
20
Definition Majxy (x y:R) (n:nat) : R :=
 
21
  Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S n) / INR (fact n).
 
22
 
 
23
Lemma Majxy_cv_R0 : forall x y:R, Un_cv (Majxy x y) 0.
 
24
Proof.
 
25
  intros.
 
26
  set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
 
27
  set (C0 := C ^ 4).
 
28
  cut (0 < C).
 
29
  intro.
 
30
  cut (0 < C0).
 
31
  intro.
 
32
  assert (H1 := cv_speed_pow_fact C0).
 
33
  unfold Un_cv in H1; unfold R_dist in H1.
 
34
  unfold Un_cv in |- *; unfold R_dist in |- *; intros.
 
35
  cut (0 < eps / C0);
 
36
    [ intro
 
37
      | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
38
        [ assumption | apply Rinv_0_lt_compat; assumption ] ].
 
39
  elim (H1 (eps / C0) H3); intros N0 H4.
 
40
  exists N0; intros.
 
41
  replace (Majxy x y n) with (C0 ^ S n / INR (fact n)).
 
42
  simpl in |- *.
 
43
  apply Rmult_lt_reg_l with (Rabs (/ C0)).
 
44
  apply Rabs_pos_lt.
 
45
  apply Rinv_neq_0_compat.
 
46
  red in |- *; intro; rewrite H6 in H0; elim (Rlt_irrefl _ H0).
 
47
  rewrite <- Rabs_mult.
 
48
  unfold Rminus in |- *; rewrite Rmult_plus_distr_l.
 
49
  rewrite Ropp_0; rewrite Rmult_0_r.
 
50
  unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
51
  rewrite <- Rinv_l_sym.
 
52
  rewrite Rmult_1_l.
 
53
  rewrite (Rabs_right (/ C0)).
 
54
  rewrite <- (Rmult_comm eps).
 
55
  replace (C0 ^ n * / INR (fact n) + 0) with (C0 ^ n * / INR (fact n) - 0);
 
56
    [ idtac | ring ].
 
57
  unfold Rdiv in H4; apply H4; assumption.
 
58
  apply Rle_ge; left; apply Rinv_0_lt_compat; assumption.
 
59
  red in |- *; intro; rewrite H6 in H0; elim (Rlt_irrefl _ H0).
 
60
  unfold Majxy in |- *.
 
61
  unfold C0 in |- *.
 
62
  rewrite pow_mult.
 
63
  unfold C in |- *; reflexivity.
 
64
  unfold C0 in |- *; apply pow_lt; assumption.
 
65
  apply Rlt_le_trans with 1.
 
66
  apply Rlt_0_1.
 
67
  unfold C in |- *.
 
68
  apply RmaxLess1.
 
69
Qed.
 
70
 
 
71
Lemma reste1_maj :
 
72
  forall (x y:R) (N:nat),
 
73
    (0 < N)%nat -> Rabs (Reste1 x y N) <= Majxy x y (pred N).
 
74
Proof.
 
75
  intros.
 
76
  set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
 
77
  unfold Reste1 in |- *.
 
78
  apply Rle_trans with
 
79
    (sum_f_R0
 
80
      (fun k:nat =>
 
81
        Rabs
 
82
        (sum_f_R0
 
83
          (fun l:nat =>
 
84
            (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
 
85
            x ^ (2 * S (l + k)) *
 
86
            ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
 
87
            y ^ (2 * (N - l))) (pred (N - k)))) (
 
88
              pred N)).
 
89
  apply
 
90
    (Rsum_abs
 
91
      (fun k:nat =>
 
92
        sum_f_R0
 
93
        (fun l:nat =>
 
94
          (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
 
95
          x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
 
96
          y ^ (2 * (N - l))) (pred (N - k))) (pred N)).
 
97
  apply Rle_trans with
 
98
    (sum_f_R0
 
99
      (fun k:nat =>
 
100
        sum_f_R0
 
101
        (fun l:nat =>
 
102
          Rabs
 
103
          ((-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
 
104
            x ^ (2 * S (l + k)) *
 
105
            ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
 
106
            y ^ (2 * (N - l)))) (pred (N - k))) (
 
107
              pred N)).
 
108
  apply sum_Rle.
 
109
  intros.
 
110
  apply
 
111
    (Rsum_abs
 
112
      (fun l:nat =>
 
113
        (-1) ^ S (l + n) / INR (fact (2 * S (l + n))) * x ^ (2 * S (l + n)) *
 
114
        ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) * 
 
115
        y ^ (2 * (N - l))) (pred (N - n))).
 
116
  apply Rle_trans with
 
117
    (sum_f_R0
 
118
      (fun k:nat =>
 
119
        sum_f_R0
 
120
        (fun l:nat =>
 
121
          / INR (fact (2 * S (l + k)) * fact (2 * (N - l))) *
 
122
          C ^ (2 * S (N + k))) (pred (N - k))) (pred N)).
 
123
  apply sum_Rle; intros.
 
124
  apply sum_Rle; intros.
 
125
  unfold Rdiv in |- *; repeat rewrite Rabs_mult.
 
126
  do 2 rewrite pow_1_abs.
 
127
  do 2 rewrite Rmult_1_l.
 
128
  rewrite (Rabs_right (/ INR (fact (2 * S (n0 + n))))).
 
129
  rewrite (Rabs_right (/ INR (fact (2 * (N - n0))))).
 
130
  rewrite mult_INR.
 
131
  rewrite Rinv_mult_distr.
 
132
  repeat rewrite Rmult_assoc.
 
133
  apply Rmult_le_compat_l.
 
134
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
135
  rewrite <- Rmult_assoc.
 
136
  rewrite <- (Rmult_comm (/ INR (fact (2 * (N - n0))))).
 
137
  rewrite Rmult_assoc.
 
138
  apply Rmult_le_compat_l.
 
139
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
140
  do 2 rewrite <- RPow_abs.
 
141
  apply Rle_trans with (Rabs x ^ (2 * S (n0 + n)) * C ^ (2 * (N - n0))).
 
142
  apply Rmult_le_compat_l.
 
143
  apply pow_le; apply Rabs_pos.
 
144
  apply pow_incr.
 
145
  split.
 
146
  apply Rabs_pos.
 
147
  unfold C in |- *.
 
148
  apply Rle_trans with (Rmax (Rabs x) (Rabs y)); apply RmaxLess2.
 
149
  apply Rle_trans with (C ^ (2 * S (n0 + n)) * C ^ (2 * (N - n0))).
 
150
  do 2 rewrite <- (Rmult_comm (C ^ (2 * (N - n0)))).
 
151
  apply Rmult_le_compat_l.
 
152
  apply pow_le.
 
153
  apply Rle_trans with 1.
 
154
  left; apply Rlt_0_1.
 
155
  unfold C in |- *; apply RmaxLess1.
 
156
  apply pow_incr.
 
157
  split.
 
158
  apply Rabs_pos.
 
159
  unfold C in |- *; apply Rle_trans with (Rmax (Rabs x) (Rabs y)).
 
160
  apply RmaxLess1.
 
161
  apply RmaxLess2.
 
162
  right.
 
163
  replace (2 * S (N + n))%nat with (2 * (N - n0) + 2 * S (n0 + n))%nat.
 
164
  rewrite pow_add.
 
165
  apply Rmult_comm.
 
166
  apply INR_eq; rewrite plus_INR; do 3 rewrite mult_INR.
 
167
  rewrite minus_INR.
 
168
  repeat rewrite S_INR; do 2 rewrite plus_INR; ring.
 
169
  apply le_trans with (pred (N - n)).
 
170
  exact H1.
 
171
  apply le_S_n.
 
172
  replace (S (pred (N - n))) with (N - n)%nat.
 
173
  apply le_trans with N.
 
174
  apply (fun p n m:nat => plus_le_reg_l n m p) with n.
 
175
  rewrite <- le_plus_minus.
 
176
  apply le_plus_r.
 
177
  apply le_trans with (pred N).
 
178
  assumption.
 
179
  apply le_pred_n.
 
180
  apply le_n_Sn.
 
181
  apply S_pred with 0%nat.
 
182
  apply plus_lt_reg_l with n.
 
183
  rewrite <- le_plus_minus.
 
184
  replace (n + 0)%nat with n; [ idtac | ring ].
 
185
  apply le_lt_trans with (pred N).
 
186
  assumption.
 
187
  apply lt_pred_n_n; assumption.
 
188
  apply le_trans with (pred N).
 
189
  assumption.
 
190
  apply le_pred_n.
 
191
  apply INR_fact_neq_0.
 
192
  apply INR_fact_neq_0.
 
193
  apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
194
  apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
195
  apply Rle_trans with
 
196
    (sum_f_R0
 
197
      (fun k:nat =>
 
198
        sum_f_R0
 
199
        (fun l:nat =>
 
200
          / INR (fact (2 * S (l + k)) * fact (2 * (N - l))) * C ^ (4 * N))
 
201
        (pred (N - k))) (pred N)).
 
202
  apply sum_Rle; intros.
 
203
  apply sum_Rle; intros.
 
204
  apply Rmult_le_compat_l.
 
205
  left; apply Rinv_0_lt_compat.
 
206
  rewrite mult_INR; apply Rmult_lt_0_compat; apply INR_fact_lt_0.
 
207
  apply Rle_pow.
 
208
  unfold C in |- *; apply RmaxLess1.
 
209
  replace (4 * N)%nat with (2 * (2 * N))%nat; [ idtac | ring ].
 
210
  apply (fun m n p:nat => mult_le_compat_l p n m).
 
211
  replace (2 * N)%nat with (S (N + pred N)).
 
212
  apply le_n_S.
 
213
  apply plus_le_compat_l; assumption.
 
214
  rewrite pred_of_minus.
 
215
  omega.
 
216
  apply Rle_trans with
 
217
    (sum_f_R0
 
218
      (fun k:nat =>
 
219
        sum_f_R0 (fun l:nat => C ^ (4 * N) * Rsqr (/ INR (fact (S (N + k)))))
 
220
        (pred (N - k))) (pred N)).
 
221
  apply sum_Rle; intros.
 
222
  apply sum_Rle; intros.
 
223
  rewrite <- (Rmult_comm (C ^ (4 * N))).
 
224
  apply Rmult_le_compat_l.
 
225
  apply pow_le.
 
226
  left; apply Rlt_le_trans with 1.
 
227
  apply Rlt_0_1.
 
228
  unfold C in |- *; apply RmaxLess1.
 
229
  replace (/ INR (fact (2 * S (n0 + n)) * fact (2 * (N - n0)))) with
 
230
    (Binomial.C (2 * S (N + n)) (2 * S (n0 + n)) / INR (fact (2 * S (N + n)))).
 
231
  apply Rle_trans with
 
232
    (Binomial.C (2 * S (N + n)) (S (N + n)) / INR (fact (2 * S (N + n)))).
 
233
  unfold Rdiv in |- *;
 
234
    do 2 rewrite <- (Rmult_comm (/ INR (fact (2 * S (N + n))))).
 
235
  apply Rmult_le_compat_l.
 
236
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
237
  apply C_maj.
 
238
  omega.
 
239
  right.
 
240
  unfold Rdiv in |- *; rewrite Rmult_comm.
 
241
  unfold Binomial.C in |- *.
 
242
  unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
243
  rewrite <- Rinv_l_sym.
 
244
  rewrite Rmult_1_l.
 
245
  replace (2 * S (N + n) - S (N + n))%nat with (S (N + n)).
 
246
  rewrite Rinv_mult_distr.
 
247
  unfold Rsqr in |- *; reflexivity.
 
248
  apply INR_fact_neq_0.
 
249
  apply INR_fact_neq_0.
 
250
  omega.
 
251
  apply INR_fact_neq_0.
 
252
  unfold Rdiv in |- *; rewrite Rmult_comm.
 
253
  unfold Binomial.C in |- *.
 
254
  unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
255
  rewrite <- Rinv_l_sym.
 
256
  rewrite Rmult_1_l.
 
257
  replace (2 * S (N + n) - 2 * S (n0 + n))%nat with (2 * (N - n0))%nat.
 
258
  rewrite mult_INR.
 
259
  reflexivity.
 
260
  omega.
 
261
  apply INR_fact_neq_0.
 
262
  apply Rle_trans with
 
263
    (sum_f_R0 (fun k:nat => INR N / INR (fact (S N)) * C ^ (4 * N)) (pred N)).
 
264
  apply sum_Rle; intros.
 
265
  rewrite <-
 
266
    (scal_sum (fun _:nat => C ^ (4 * N)) (pred (N - n))
 
267
      (Rsqr (/ INR (fact (S (N + n)))))).
 
268
  rewrite sum_cte.
 
269
  rewrite <- Rmult_assoc.
 
270
  do 2 rewrite <- (Rmult_comm (C ^ (4 * N))).
 
271
  rewrite Rmult_assoc.
 
272
  apply Rmult_le_compat_l.
 
273
  apply pow_le.
 
274
  left; apply Rlt_le_trans with 1.
 
275
  apply Rlt_0_1.
 
276
  unfold C in |- *; apply RmaxLess1.
 
277
  apply Rle_trans with (Rsqr (/ INR (fact (S (N + n)))) * INR N).
 
278
  apply Rmult_le_compat_l.
 
279
  apply Rle_0_sqr.
 
280
  apply le_INR.
 
281
  omega.
 
282
  rewrite Rmult_comm; unfold Rdiv in |- *; apply Rmult_le_compat_l.
 
283
  apply pos_INR.
 
284
  apply Rle_trans with (/ INR (fact (S (N + n)))).
 
285
  pattern (/ INR (fact (S (N + n)))) at 2 in |- *; rewrite <- Rmult_1_r.
 
286
  unfold Rsqr in |- *.
 
287
  apply Rmult_le_compat_l.
 
288
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
289
  apply Rmult_le_reg_l with (INR (fact (S (N + n)))).
 
290
  apply INR_fact_lt_0.
 
291
  rewrite <- Rinv_r_sym.
 
292
  rewrite Rmult_1_r.
 
293
  replace 1 with (INR 1).
 
294
  apply le_INR.
 
295
  apply lt_le_S.
 
296
  apply INR_lt; apply INR_fact_lt_0.
 
297
  reflexivity.
 
298
  apply INR_fact_neq_0.
 
299
  apply Rmult_le_reg_l with (INR (fact (S (N + n)))).
 
300
  apply INR_fact_lt_0.
 
301
  rewrite <- Rinv_r_sym.
 
302
  apply Rmult_le_reg_l with (INR (fact (S N))).
 
303
  apply INR_fact_lt_0.
 
304
  rewrite Rmult_1_r.
 
305
  rewrite (Rmult_comm (INR (fact (S N)))).
 
306
  rewrite Rmult_assoc.
 
307
  rewrite <- Rinv_l_sym.
 
308
  rewrite Rmult_1_r.
 
309
  apply le_INR.
 
310
  apply fact_le.
 
311
  apply le_n_S.
 
312
  apply le_plus_l.
 
313
  apply INR_fact_neq_0.
 
314
  apply INR_fact_neq_0.
 
315
  rewrite sum_cte.
 
316
  apply Rle_trans with (C ^ (4 * N) / INR (fact (pred N))).
 
317
  rewrite <- (Rmult_comm (C ^ (4 * N))).
 
318
  unfold Rdiv in |- *; rewrite Rmult_assoc; apply Rmult_le_compat_l.
 
319
  apply pow_le.
 
320
  left; apply Rlt_le_trans with 1.
 
321
  apply Rlt_0_1.
 
322
  unfold C in |- *; apply RmaxLess1.
 
323
  cut (S (pred N) = N).
 
324
  intro; rewrite H0.
 
325
  pattern N at 2 in |- *; rewrite <- H0.
 
326
  do 2 rewrite fact_simpl.
 
327
  rewrite H0.
 
328
  repeat rewrite mult_INR.
 
329
  repeat rewrite Rinv_mult_distr.
 
330
  rewrite (Rmult_comm (/ INR (S N))).
 
331
  repeat rewrite <- Rmult_assoc.
 
332
  rewrite <- Rinv_r_sym.
 
333
  rewrite Rmult_1_l.
 
334
  pattern (/ INR (fact (pred N))) at 2 in |- *; rewrite <- Rmult_1_r.
 
335
  rewrite Rmult_assoc.
 
336
  apply Rmult_le_compat_l.
 
337
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
338
  apply Rmult_le_reg_l with (INR (S N)).
 
339
  apply lt_INR_0; apply lt_O_Sn.
 
340
  rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
 
341
  rewrite Rmult_1_r; rewrite Rmult_1_l.
 
342
  apply le_INR; apply le_n_Sn.
 
343
  apply not_O_INR; discriminate.
 
344
  apply not_O_INR.
 
345
  red in |- *; intro; rewrite H1 in H; elim (lt_irrefl _ H).
 
346
  apply not_O_INR.
 
347
  red in |- *; intro; rewrite H1 in H; elim (lt_irrefl _ H).
 
348
  apply INR_fact_neq_0.
 
349
  apply not_O_INR; discriminate.
 
350
  apply prod_neq_R0.
 
351
  apply not_O_INR.
 
352
  red in |- *; intro; rewrite H1 in H; elim (lt_irrefl _ H).
 
353
  apply INR_fact_neq_0.
 
354
  symmetry  in |- *; apply S_pred with 0%nat; assumption.
 
355
  right.
 
356
  unfold Majxy in |- *.
 
357
  unfold C in |- *.
 
358
  replace (S (pred N)) with N.
 
359
  reflexivity.
 
360
  apply S_pred with 0%nat; assumption.
 
361
Qed.
 
362
 
 
363
Lemma reste2_maj :
 
364
  forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste2 x y N) <= Majxy x y N.
 
365
Proof.
 
366
  intros.
 
367
  set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
 
368
  unfold Reste2 in |- *.
 
369
  apply Rle_trans with
 
370
    (sum_f_R0
 
371
      (fun k:nat =>
 
372
        Rabs
 
373
        (sum_f_R0
 
374
          (fun l:nat =>
 
375
            (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
 
376
            x ^ (2 * S (l + k) + 1) *
 
377
            ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) *
 
378
            y ^ (2 * (N - l) + 1)) (pred (N - k)))) (
 
379
              pred N)).
 
380
  apply
 
381
    (Rsum_abs
 
382
      (fun k:nat =>
 
383
        sum_f_R0
 
384
        (fun l:nat =>
 
385
          (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
 
386
          x ^ (2 * S (l + k) + 1) *
 
387
          ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) *
 
388
          y ^ (2 * (N - l) + 1)) (pred (N - k))) (
 
389
            pred N)).
 
390
  apply Rle_trans with
 
391
    (sum_f_R0
 
392
      (fun k:nat =>
 
393
        sum_f_R0
 
394
        (fun l:nat =>
 
395
          Rabs
 
396
          ((-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
 
397
            x ^ (2 * S (l + k) + 1) *
 
398
            ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) *
 
399
            y ^ (2 * (N - l) + 1))) (pred (N - k))) (
 
400
              pred N)).
 
401
  apply sum_Rle.
 
402
  intros.
 
403
  apply
 
404
    (Rsum_abs
 
405
      (fun l:nat =>
 
406
        (-1) ^ S (l + n) / INR (fact (2 * S (l + n) + 1)) *
 
407
        x ^ (2 * S (l + n) + 1) *
 
408
        ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) *
 
409
        y ^ (2 * (N - l) + 1)) (pred (N - n))).
 
410
  apply Rle_trans with
 
411
    (sum_f_R0
 
412
      (fun k:nat =>
 
413
        sum_f_R0
 
414
        (fun l:nat =>
 
415
          / INR (fact (2 * S (l + k) + 1) * fact (2 * (N - l) + 1)) *
 
416
          C ^ (2 * S (S (N + k)))) (pred (N - k))) (
 
417
            pred N)).
 
418
  apply sum_Rle; intros.
 
419
  apply sum_Rle; intros.
 
420
  unfold Rdiv in |- *; repeat rewrite Rabs_mult.
 
421
  do 2 rewrite pow_1_abs.
 
422
  do 2 rewrite Rmult_1_l.
 
423
  rewrite (Rabs_right (/ INR (fact (2 * S (n0 + n) + 1)))).
 
424
  rewrite (Rabs_right (/ INR (fact (2 * (N - n0) + 1)))).
 
425
  rewrite mult_INR.
 
426
  rewrite Rinv_mult_distr.
 
427
  repeat rewrite Rmult_assoc.
 
428
  apply Rmult_le_compat_l.
 
429
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
430
  rewrite <- Rmult_assoc.
 
431
  rewrite <- (Rmult_comm (/ INR (fact (2 * (N - n0) + 1)))).
 
432
  rewrite Rmult_assoc.
 
433
  apply Rmult_le_compat_l.
 
434
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
435
  do 2 rewrite <- RPow_abs.
 
436
  apply Rle_trans with (Rabs x ^ (2 * S (n0 + n) + 1) * C ^ (2 * (N - n0) + 1)).
 
437
  apply Rmult_le_compat_l.
 
438
  apply pow_le; apply Rabs_pos.
 
439
  apply pow_incr.
 
440
  split.
 
441
  apply Rabs_pos.
 
442
  unfold C in |- *.
 
443
  apply Rle_trans with (Rmax (Rabs x) (Rabs y)); apply RmaxLess2.
 
444
  apply Rle_trans with (C ^ (2 * S (n0 + n) + 1) * C ^ (2 * (N - n0) + 1)).
 
445
  do 2 rewrite <- (Rmult_comm (C ^ (2 * (N - n0) + 1))).
 
446
  apply Rmult_le_compat_l.
 
447
  apply pow_le.
 
448
  apply Rle_trans with 1.
 
449
  left; apply Rlt_0_1.
 
450
  unfold C in |- *; apply RmaxLess1.
 
451
  apply pow_incr.
 
452
  split.
 
453
  apply Rabs_pos.
 
454
  unfold C in |- *; apply Rle_trans with (Rmax (Rabs x) (Rabs y)).
 
455
  apply RmaxLess1.
 
456
  apply RmaxLess2.
 
457
  right.
 
458
  replace (2 * S (S (N + n)))%nat with
 
459
    (2 * (N - n0) + 1 + (2 * S (n0 + n) + 1))%nat.
 
460
  repeat rewrite pow_add.
 
461
  ring.
 
462
  omega.
 
463
  apply INR_fact_neq_0.
 
464
  apply INR_fact_neq_0.
 
465
  apply Rle_ge; left; apply Rinv_0_lt_compat.
 
466
  apply INR_fact_lt_0.
 
467
  apply Rle_ge; left; apply Rinv_0_lt_compat.
 
468
  apply INR_fact_lt_0.
 
469
  apply Rle_trans with
 
470
    (sum_f_R0
 
471
      (fun k:nat =>
 
472
        sum_f_R0
 
473
        (fun l:nat =>
 
474
          / INR (fact (2 * S (l + k) + 1) * fact (2 * (N - l) + 1)) *
 
475
          C ^ (4 * S N)) (pred (N - k))) (pred N)).
 
476
  apply sum_Rle; intros.
 
477
  apply sum_Rle; intros.
 
478
  apply Rmult_le_compat_l.
 
479
  left; apply Rinv_0_lt_compat.
 
480
  rewrite mult_INR; apply Rmult_lt_0_compat; apply INR_fact_lt_0.
 
481
  apply Rle_pow.
 
482
  unfold C in |- *; apply RmaxLess1.
 
483
  replace (4 * S N)%nat with (2 * (2 * S N))%nat; [ idtac | ring ].
 
484
  apply (fun m n p:nat => mult_le_compat_l p n m).
 
485
  replace (2 * S N)%nat with (S (S (N + N))).
 
486
  repeat apply le_n_S.
 
487
  apply plus_le_compat_l.
 
488
  apply le_trans with (pred N).
 
489
  assumption.
 
490
  apply le_pred_n.
 
491
  ring.
 
492
  apply Rle_trans with
 
493
    (sum_f_R0
 
494
      (fun k:nat =>
 
495
        sum_f_R0
 
496
        (fun l:nat => C ^ (4 * S N) * Rsqr (/ INR (fact (S (S (N + k))))))
 
497
        (pred (N - k))) (pred N)).
 
498
  apply sum_Rle; intros.
 
499
  apply sum_Rle; intros.
 
500
  rewrite <- (Rmult_comm (C ^ (4 * S N))).
 
501
  apply Rmult_le_compat_l.
 
502
  apply pow_le.
 
503
  left; apply Rlt_le_trans with 1.
 
504
  apply Rlt_0_1.
 
505
  unfold C in |- *; apply RmaxLess1.
 
506
  replace (/ INR (fact (2 * S (n0 + n) + 1) * fact (2 * (N - n0) + 1))) with
 
507
    (Binomial.C (2 * S (S (N + n))) (2 * S (n0 + n) + 1) /
 
508
      INR (fact (2 * S (S (N + n))))).
 
509
  apply Rle_trans with
 
510
    (Binomial.C (2 * S (S (N + n))) (S (S (N + n))) /
 
511
      INR (fact (2 * S (S (N + n))))).
 
512
  unfold Rdiv in |- *;
 
513
    do 2 rewrite <- (Rmult_comm (/ INR (fact (2 * S (S (N + n)))))).
 
514
  apply Rmult_le_compat_l.
 
515
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
516
  apply C_maj.
 
517
  apply le_trans with (2 * S (S (n0 + n)))%nat.
 
518
  replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
 
519
  apply le_n_Sn.
 
520
  ring.
 
521
  omega.
 
522
  right.
 
523
  unfold Rdiv in |- *; rewrite Rmult_comm.
 
524
  unfold Binomial.C in |- *.
 
525
  unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
526
  rewrite <- Rinv_l_sym.
 
527
  rewrite Rmult_1_l.
 
528
  replace (2 * S (S (N + n)) - S (S (N + n)))%nat with (S (S (N + n))).
 
529
  rewrite Rinv_mult_distr.
 
530
  unfold Rsqr in |- *; reflexivity.
 
531
  apply INR_fact_neq_0.
 
532
  apply INR_fact_neq_0.
 
533
  omega.
 
534
  apply INR_fact_neq_0.
 
535
  unfold Rdiv in |- *; rewrite Rmult_comm.
 
536
  unfold Binomial.C in |- *.
 
537
  unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
538
  rewrite <- Rinv_l_sym.
 
539
  rewrite Rmult_1_l.
 
540
  replace (2 * S (S (N + n)) - (2 * S (n0 + n) + 1))%nat with
 
541
    (2 * (N - n0) + 1)%nat.
 
542
  rewrite mult_INR.
 
543
  reflexivity.
 
544
  omega.
 
545
  apply INR_fact_neq_0.
 
546
  apply Rle_trans with
 
547
    (sum_f_R0 (fun k:nat => INR N / INR (fact (S (S N))) * C ^ (4 * S N))
 
548
      (pred N)).
 
549
  apply sum_Rle; intros.
 
550
  rewrite <-
 
551
    (scal_sum (fun _:nat => C ^ (4 * S N)) (pred (N - n))
 
552
      (Rsqr (/ INR (fact (S (S (N + n))))))).
 
553
  rewrite sum_cte.
 
554
  rewrite <- Rmult_assoc.
 
555
  do 2 rewrite <- (Rmult_comm (C ^ (4 * S N))).
 
556
  rewrite Rmult_assoc.
 
557
  apply Rmult_le_compat_l.
 
558
  apply pow_le.
 
559
  left; apply Rlt_le_trans with 1.
 
560
  apply Rlt_0_1.
 
561
  unfold C in |- *; apply RmaxLess1.
 
562
  apply Rle_trans with (Rsqr (/ INR (fact (S (S (N + n))))) * INR N).
 
563
  apply Rmult_le_compat_l.
 
564
  apply Rle_0_sqr.
 
565
  replace (S (pred (N - n))) with (N - n)%nat.
 
566
  apply le_INR.
 
567
  omega.
 
568
  omega.
 
569
  rewrite Rmult_comm; unfold Rdiv in |- *; apply Rmult_le_compat_l.
 
570
  apply pos_INR.
 
571
  apply Rle_trans with (/ INR (fact (S (S (N + n))))).
 
572
  pattern (/ INR (fact (S (S (N + n))))) at 2 in |- *; rewrite <- Rmult_1_r.
 
573
  unfold Rsqr in |- *.
 
574
  apply Rmult_le_compat_l.
 
575
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
576
  apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))).
 
577
  apply INR_fact_lt_0.
 
578
  rewrite <- Rinv_r_sym.
 
579
  rewrite Rmult_1_r.
 
580
  replace 1 with (INR 1).
 
581
  apply le_INR.
 
582
  apply lt_le_S.
 
583
  apply INR_lt; apply INR_fact_lt_0.
 
584
  reflexivity.
 
585
  apply INR_fact_neq_0.
 
586
  apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))).
 
587
  apply INR_fact_lt_0.
 
588
  rewrite <- Rinv_r_sym.
 
589
  apply Rmult_le_reg_l with (INR (fact (S (S N)))).
 
590
  apply INR_fact_lt_0.
 
591
  rewrite Rmult_1_r.
 
592
  rewrite (Rmult_comm (INR (fact (S (S N))))).
 
593
  rewrite Rmult_assoc.
 
594
  rewrite <- Rinv_l_sym.
 
595
  rewrite Rmult_1_r.
 
596
  apply le_INR.
 
597
  apply fact_le.
 
598
  omega.
 
599
  apply INR_fact_neq_0.
 
600
  apply INR_fact_neq_0.
 
601
  rewrite sum_cte.
 
602
  apply Rle_trans with (C ^ (4 * S N) / INR (fact N)).
 
603
  rewrite <- (Rmult_comm (C ^ (4 * S N))).
 
604
  unfold Rdiv in |- *; rewrite Rmult_assoc; apply Rmult_le_compat_l.
 
605
  apply pow_le.
 
606
  left; apply Rlt_le_trans with 1.
 
607
  apply Rlt_0_1.
 
608
  unfold C in |- *; apply RmaxLess1.
 
609
  cut (S (pred N) = N).
 
610
  intro; rewrite H0.
 
611
  do 2 rewrite fact_simpl.
 
612
  repeat rewrite mult_INR.
 
613
  repeat rewrite Rinv_mult_distr.
 
614
  apply Rle_trans with
 
615
    (INR (S (S N)) * (/ INR (S (S N)) * (/ INR (S N) * / INR (fact N))) * INR N).
 
616
  repeat rewrite Rmult_assoc.
 
617
  rewrite (Rmult_comm (INR N)).
 
618
  rewrite (Rmult_comm (INR (S (S N)))).
 
619
  apply Rmult_le_compat_l.
 
620
  repeat apply Rmult_le_pos.
 
621
  left; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
 
622
  left; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
 
623
  left; apply Rinv_0_lt_compat.
 
624
  apply INR_fact_lt_0.
 
625
  apply pos_INR.
 
626
  apply le_INR.
 
627
  apply le_trans with (S N); apply le_n_Sn.
 
628
  repeat rewrite <- Rmult_assoc.
 
629
  rewrite <- Rinv_r_sym.
 
630
  rewrite Rmult_1_l.
 
631
  apply Rle_trans with (/ INR (S N) * / INR (fact N) * INR (S N)).
 
632
  repeat rewrite Rmult_assoc.
 
633
  repeat apply Rmult_le_compat_l.
 
634
  left; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
 
635
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
636
  apply le_INR; apply le_n_Sn.
 
637
  rewrite (Rmult_comm (/ INR (S N))).
 
638
  rewrite Rmult_assoc.
 
639
  rewrite <- Rinv_l_sym.
 
640
  rewrite Rmult_1_r; right; reflexivity.
 
641
  apply not_O_INR; discriminate.
 
642
  apply not_O_INR; discriminate.
 
643
  apply not_O_INR; discriminate.
 
644
  apply INR_fact_neq_0.
 
645
  apply not_O_INR; discriminate.
 
646
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].
 
647
  symmetry  in |- *; apply S_pred with 0%nat; assumption.
 
648
  right.
 
649
  unfold Majxy in |- *.
 
650
  unfold C in |- *.
 
651
  reflexivity.
 
652
Qed.
 
653
 
 
654
Lemma reste1_cv_R0 : forall x y:R, Un_cv (Reste1 x y) 0.
 
655
Proof.
 
656
  intros.
 
657
  assert (H := Majxy_cv_R0 x y).
 
658
  unfold Un_cv in H; unfold R_dist in H.
 
659
  unfold Un_cv in |- *; unfold R_dist in |- *; intros.
 
660
  elim (H eps H0); intros N0 H1.
 
661
  exists (S N0); intros.
 
662
  unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r.
 
663
  apply Rle_lt_trans with (Rabs (Majxy x y (pred n))).
 
664
  rewrite (Rabs_right (Majxy x y (pred n))).
 
665
  apply reste1_maj.
 
666
  apply lt_le_trans with (S N0).
 
667
  apply lt_O_Sn.
 
668
  assumption.
 
669
  apply Rle_ge.
 
670
  unfold Majxy in |- *.
 
671
  unfold Rdiv in |- *; apply Rmult_le_pos.
 
672
  apply pow_le.
 
673
  apply Rle_trans with 1.
 
674
  left; apply Rlt_0_1.
 
675
  apply RmaxLess1.
 
676
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
677
  replace (Majxy x y (pred n)) with (Majxy x y (pred n) - 0); [ idtac | ring ].
 
678
  apply H1.
 
679
  unfold ge in |- *; apply le_S_n.
 
680
  replace (S (pred n)) with n.
 
681
  assumption.
 
682
  apply S_pred with 0%nat.
 
683
  apply lt_le_trans with (S N0); [ apply lt_O_Sn | assumption ].
 
684
Qed.
 
685
 
 
686
Lemma reste2_cv_R0 : forall x y:R, Un_cv (Reste2 x y) 0.
 
687
Proof.
 
688
  intros.
 
689
  assert (H := Majxy_cv_R0 x y).
 
690
  unfold Un_cv in H; unfold R_dist in H.
 
691
  unfold Un_cv in |- *; unfold R_dist in |- *; intros.
 
692
  elim (H eps H0); intros N0 H1.
 
693
  exists (S N0); intros.
 
694
  unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r.
 
695
  apply Rle_lt_trans with (Rabs (Majxy x y n)).
 
696
  rewrite (Rabs_right (Majxy x y n)).
 
697
  apply reste2_maj.
 
698
  apply lt_le_trans with (S N0).
 
699
  apply lt_O_Sn.
 
700
  assumption.
 
701
  apply Rle_ge.
 
702
  unfold Majxy in |- *.
 
703
  unfold Rdiv in |- *; apply Rmult_le_pos.
 
704
  apply pow_le.
 
705
  apply Rle_trans with 1.
 
706
  left; apply Rlt_0_1.
 
707
  apply RmaxLess1.
 
708
  left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 
709
  replace (Majxy x y n) with (Majxy x y n - 0); [ idtac | ring ].
 
710
  apply H1.
 
711
  unfold ge in |- *; apply le_trans with (S N0).
 
712
  apply le_n_Sn.
 
713
  exact H2.
 
714
Qed.
 
715
 
 
716
Lemma reste_cv_R0 : forall x y:R, Un_cv (Reste x y) 0.
 
717
Proof.
 
718
  intros.
 
719
  unfold Reste in |- *.
 
720
  set (An := fun n:nat => Reste2 x y n).
 
721
  set (Bn := fun n:nat => Reste1 x y (S n)).
 
722
  cut
 
723
    (Un_cv (fun n:nat => An n - Bn n) (0 - 0) ->
 
724
      Un_cv (fun N:nat => Reste2 x y N - Reste1 x y (S N)) 0).
 
725
  intro.
 
726
  apply H.
 
727
  apply CV_minus.
 
728
  unfold An in |- *.
 
729
  replace (fun n:nat => Reste2 x y n) with (Reste2 x y).
 
730
  apply reste2_cv_R0.
 
731
  reflexivity.
 
732
  unfold Bn in |- *.
 
733
  assert (H0 := reste1_cv_R0 x y).
 
734
  unfold Un_cv in H0; unfold R_dist in H0.
 
735
  unfold Un_cv in |- *; unfold R_dist in |- *; intros.
 
736
  elim (H0 eps H1); intros N0 H2.
 
737
  exists N0; intros.
 
738
  apply H2.
 
739
  unfold ge in |- *; apply le_trans with (S N0).
 
740
  apply le_n_Sn.
 
741
  apply le_n_S; assumption.
 
742
  unfold An, Bn in |- *.
 
743
  intro.
 
744
  replace 0 with (0 - 0); [ idtac | ring ].
 
745
  exact H.
 
746
Qed.
 
747
 
 
748
Theorem cos_plus : forall x y:R, cos (x + y) = cos x * cos y - sin x * sin y. 
 
749
Proof.
 
750
  intros. 
 
751
  cut (Un_cv (C1 x y) (cos x * cos y - sin x * sin y)). 
 
752
  cut (Un_cv (C1 x y) (cos (x + y))). 
 
753
  intros. 
 
754
  apply UL_sequence with (C1 x y); assumption. 
 
755
  apply C1_cvg. 
 
756
  unfold Un_cv in |- *; unfold R_dist in |- *. 
 
757
  intros. 
 
758
  assert (H0 := A1_cvg x). 
 
759
  assert (H1 := A1_cvg y). 
 
760
  assert (H2 := B1_cvg x). 
 
761
  assert (H3 := B1_cvg y). 
 
762
  assert (H4 := CV_mult _ _ _ _ H0 H1). 
 
763
  assert (H5 := CV_mult _ _ _ _ H2 H3). 
 
764
  assert (H6 := reste_cv_R0 x y).
 
765
  unfold Un_cv in H4; unfold Un_cv in H5; unfold Un_cv in H6.
 
766
  unfold R_dist in H4; unfold R_dist in H5; unfold R_dist in H6. 
 
767
  cut (0 < eps / 3);
 
768
    [ intro
 
769
      | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
770
        [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. 
 
771
  elim (H4 (eps / 3) H7); intros N1 H8. 
 
772
  elim (H5 (eps / 3) H7); intros N2 H9. 
 
773
  elim (H6 (eps / 3) H7); intros N3 H10.
 
774
  set (N := S (S (max (max N1 N2) N3))). 
 
775
  exists N. 
 
776
  intros. 
 
777
  cut (n = S (pred n)). 
 
778
  intro; rewrite H12. 
 
779
  rewrite <- cos_plus_form. 
 
780
  rewrite <- H12. 
 
781
  apply Rle_lt_trans with
 
782
    (Rabs (A1 x n * A1 y n - cos x * cos y) +
 
783
      Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n))). 
 
784
  replace
 
785
    (A1 x n * A1 y n - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n) -
 
786
      (cos x * cos y - sin x * sin y)) with
 
787
    (A1 x n * A1 y n - cos x * cos y +
 
788
      (sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n)));
 
789
    [ apply Rabs_triang | ring ].
 
790
  replace eps with (eps / 3 + (eps / 3 + eps / 3)).
 
791
  apply Rplus_lt_compat. 
 
792
  apply H8. 
 
793
  unfold ge in |- *; apply le_trans with N. 
 
794
  unfold N in |- *. 
 
795
  apply le_trans with (max N1 N2). 
 
796
  apply le_max_l. 
 
797
  apply le_trans with (max (max N1 N2) N3).
 
798
  apply le_max_l.
 
799
  apply le_trans with (S (max (max N1 N2) N3)); apply le_n_Sn.
 
800
  assumption. 
 
801
  apply Rle_lt_trans with
 
802
    (Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n)) +
 
803
      Rabs (Reste x y (pred n))).
 
804
  apply Rabs_triang.
 
805
  apply Rplus_lt_compat.
 
806
  rewrite <- Rabs_Ropp. 
 
807
  rewrite Ropp_minus_distr. 
 
808
  apply H9. 
 
809
  unfold ge in |- *; apply le_trans with (max N1 N2). 
 
810
  apply le_max_r. 
 
811
  apply le_S_n. 
 
812
  rewrite <- H12. 
 
813
  apply le_trans with N.
 
814
  unfold N in |- *.
 
815
  apply le_n_S.
 
816
  apply le_trans with (max (max N1 N2) N3).
 
817
  apply le_max_l.
 
818
  apply le_n_Sn.
 
819
  assumption.
 
820
  replace (Reste x y (pred n)) with (Reste x y (pred n) - 0).
 
821
  apply H10.
 
822
  unfold ge in |- *.
 
823
  apply le_S_n.
 
824
  rewrite <- H12.
 
825
  apply le_trans with N.
 
826
  unfold N in |- *.
 
827
  apply le_n_S.
 
828
  apply le_trans with (max (max N1 N2) N3).
 
829
  apply le_max_r.
 
830
  apply le_n_Sn.
 
831
  assumption.
 
832
  ring.
 
833
  pattern eps at 4 in |- *; replace eps with (3 * (eps / 3)).
 
834
  ring.
 
835
  unfold Rdiv in |- *.
 
836
  rewrite <- Rmult_assoc.
 
837
  apply Rinv_r_simpl_m.
 
838
  discrR.
 
839
  apply lt_le_trans with (pred N).
 
840
  unfold N in |- *; simpl in |- *; apply lt_O_Sn.
 
841
  apply le_S_n.
 
842
  rewrite <- H12.
 
843
  replace (S (pred N)) with N.
 
844
  assumption.
 
845
  unfold N in |- *; simpl in |- *; reflexivity.
 
846
  cut (0 < N)%nat. 
 
847
  intro. 
 
848
  cut (0 < n)%nat. 
 
849
  intro. 
 
850
  apply S_pred with 0%nat; assumption.
 
851
  apply lt_le_trans with N; assumption. 
 
852
  unfold N in |- *; apply lt_O_Sn.
 
853
Qed.