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
(************************************************************************)
9
(*i $Id: Rtrigo_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
12
Require Import Rfunctions.
13
Require Import SeqSeries.
14
Require Import Rtrigo.
15
Require Import Ranalysis1.
16
Require Import PSeries_reg.
17
Open Local Scope nat_scope.
18
Open Local Scope R_scope.
21
forall fn:nat -> R -> R,
22
fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)) ->
25
unfold CVN_R in |- *; intros.
27
intro hyp_r; unfold CVN_r in |- *.
28
exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)).
33
sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k)))
35
intro X; elim X; intros.
39
intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult.
40
rewrite pow_1_abs; rewrite Rmult_1_l.
41
cut (0 < / INR (fact (2 * n))).
42
intro; rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))).
43
apply Rmult_le_compat_l.
45
rewrite <- RPow_abs; apply pow_maj_Rabs.
47
unfold Boule in H0; rewrite Rminus_0_r in H0.
49
apply Rinv_0_lt_compat; apply INR_fact_lt_0.
51
intro; apply Rabs_no_R0.
53
apply Rinv_neq_0_compat.
55
apply pow_nonzero; assumption.
56
assert (H0 := Alembert_cos).
57
unfold cos_n in H0; unfold Un_cv in H0; unfold Un_cv in |- *; intros.
58
cut (0 < eps / Rsqr r).
59
intro; elim (H0 _ H2); intros N0 H3.
61
unfold R_dist in |- *; assert (H5 := H3 _ H4).
65
(Rabs (/ INR (fact (2 * S n)) * r ^ (2 * S n)) /
66
Rabs (/ INR (fact (2 * n)) * r ^ (2 * n)))) with
68
Rabs ((-1) ^ S n / INR (fact (2 * S n)) / ((-1) ^ n / INR (fact (2 * n))))).
69
apply Rmult_lt_reg_l with (/ Rsqr r).
70
apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
71
pattern (/ Rsqr r) at 1 in |- *; replace (/ Rsqr r) with (Rabs (/ Rsqr r)).
72
rewrite <- Rabs_mult; rewrite Rmult_minus_distr_l; rewrite Rmult_0_r;
73
rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
74
rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); apply H5.
75
unfold Rsqr in |- *; apply prod_neq_R0; assumption.
79
apply Rle_ge; apply Rle_0_sqr.
80
unfold Rsqr in |- *; apply prod_neq_R0; assumption.
81
rewrite (Rmult_comm (Rsqr r)); unfold Rdiv in |- *; repeat rewrite Rabs_mult;
82
rewrite Rabs_Rabsolu; rewrite pow_1_abs; rewrite Rmult_1_l;
83
repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l.
85
rewrite Rabs_mult; rewrite (pow_1_abs n); rewrite Rmult_1_l;
87
rewrite Rinv_involutive.
88
rewrite Rinv_mult_distr.
90
rewrite Rinv_involutive.
91
rewrite (Rmult_comm (Rabs (Rabs (r ^ (2 * S n))))); rewrite Rabs_mult;
92
rewrite Rabs_Rabsolu; rewrite Rmult_assoc; apply Rmult_eq_compat_l.
94
do 2 rewrite Rabs_Rabsolu; repeat rewrite Rabs_right.
95
replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r).
96
repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
97
unfold Rsqr in |- *; ring.
98
apply pow_nonzero; assumption.
99
replace (2 * S n)%nat with (S (S (2 * n))).
102
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
103
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
104
apply Rabs_no_R0; apply pow_nonzero; assumption.
105
apply Rabs_no_R0; apply INR_fact_neq_0.
106
apply INR_fact_neq_0.
107
apply Rabs_no_R0; apply Rinv_neq_0_compat; apply INR_fact_neq_0.
108
apply Rabs_no_R0; apply pow_nonzero; assumption.
109
apply INR_fact_neq_0.
110
apply Rinv_neq_0_compat; apply INR_fact_neq_0.
112
apply pow_nonzero; discrR.
113
apply Rinv_neq_0_compat; apply INR_fact_neq_0.
114
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
116
apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
117
assert (H0 := cond_pos r); red in |- *; intro; rewrite H1 in H0;
118
elim (Rlt_irrefl _ H0).
122
Lemma continuity_cos : continuity cos.
124
set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)).
126
intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
127
intro cv; cut (forall n:nat, continuity (fn n)).
128
intro; cut (forall x:R, cos x = SFL fn cv x).
129
intro; cut (continuity (SFL fn cv) -> continuity cos).
131
apply SFL_continuity; assumption.
132
unfold continuity in |- *; unfold continuity_pt in |- *;
133
unfold continue_in in |- *; unfold limit1_in in |- *;
134
unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *;
136
elim (H1 x _ H2); intros.
141
intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6.
142
intro; unfold cos, SFL in |- *.
143
case (cv x); case (exist_cos (Rsqr x)); intros.
144
symmetry in |- *; eapply UL_sequence.
146
unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros.
147
elim (c _ H0); intros N0 H1.
149
unfold R_dist in H1; unfold R_dist, SP in |- *.
150
replace (sum_f_R0 (fun k:nat => fn k x) n) with
151
(sum_f_R0 (fun i:nat => cos_n i * Rsqr x ^ i) n).
152
apply H1; assumption.
153
apply sum_eq; intros.
154
unfold cos_n, fn in |- *; apply Rmult_eq_compat_l.
155
unfold Rsqr in |- *; rewrite pow_sqr; reflexivity.
156
intro; unfold fn in |- *;
157
replace (fun x:R => (-1) ^ n / INR (fact (2 * n)) * x ^ (2 * n)) with
158
(fct_cte ((-1) ^ n / INR (fact (2 * n))) * pow_fct (2 * n))%F;
159
[ idtac | reflexivity ].
160
apply continuity_mult.
161
apply derivable_continuous; apply derivable_const.
162
apply derivable_continuous; apply (derivable_pow (2 * n)).
163
apply CVN_R_CVS; apply X.
164
apply CVN_R_cos; unfold fn in |- *; reflexivity.
168
Lemma continuity_sin : continuity sin.
170
unfold continuity in |- *; intro.
171
assert (H0 := continuity_cos (PI / 2 - x)).
172
unfold continuity_pt in H0; unfold continue_in in H0; unfold limit1_in in H0;
173
unfold limit_in in H0; simpl in H0; unfold R_dist in H0;
174
unfold continuity_pt in |- *; unfold continue_in in |- *;
175
unfold limit1_in in |- *; unfold limit_in in |- *;
176
simpl in |- *; unfold R_dist in |- *; intros.
177
elim (H0 _ H); intros.
182
intros; rewrite <- (cos_shift x); rewrite <- (cos_shift x1); apply H3.
185
unfold D_x, no_cond in |- *; split.
187
red in |- *; intro; unfold D_x, no_cond in H5; elim H5; intros _ H8; elim H8;
188
rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive x1);
189
apply Ropp_eq_compat; apply Rplus_eq_reg_l with (PI / 2);
191
replace (PI / 2 - x1 - (PI / 2 - x)) with (x - x1); [ idtac | ring ];
192
rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr'; apply H6.
196
forall fn:nat -> R -> R,
198
(fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)) ->
201
unfold CVN_R in |- *; unfold CVN_r in |- *; intros fn H r.
202
exists (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)).
208
(fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n)
210
intro X; elim X; intros.
214
intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult;
215
rewrite pow_1_abs; rewrite Rmult_1_l.
216
cut (0 < / INR (fact (2 * n + 1))).
217
intro; rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))).
218
apply Rmult_le_compat_l.
220
rewrite <- RPow_abs; apply pow_maj_Rabs.
221
rewrite Rabs_Rabsolu; unfold Boule in H0; rewrite Rminus_0_r in H0; left;
223
apply Rinv_0_lt_compat; apply INR_fact_lt_0.
225
intro; apply Alembert_C2.
226
intro; apply Rabs_no_R0.
228
apply Rinv_neq_0_compat; apply INR_fact_neq_0.
229
apply pow_nonzero; assumption.
230
assert (H1 := Alembert_sin).
231
unfold sin_n in H1; unfold Un_cv in H1; unfold Un_cv in |- *; intros.
232
cut (0 < eps / Rsqr r).
233
intro; elim (H1 _ H3); intros N0 H4.
235
unfold R_dist in |- *; assert (H6 := H4 _ H5).
239
(Rabs (/ INR (fact (2 * S n + 1)) * r ^ (2 * S n)) /
240
Rabs (/ INR (fact (2 * n + 1)) * r ^ (2 * n)))) with
243
((-1) ^ S n / INR (fact (2 * S n + 1)) /
244
((-1) ^ n / INR (fact (2 * n + 1))))).
245
apply Rmult_lt_reg_l with (/ Rsqr r).
246
apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
247
pattern (/ Rsqr r) at 1 in |- *; rewrite <- (Rabs_right (/ Rsqr r)).
248
rewrite <- Rabs_mult.
249
rewrite Rmult_minus_distr_l.
250
rewrite Rmult_0_r; rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
251
rewrite Rmult_1_l; rewrite <- (Rmult_comm eps).
253
unfold Rsqr in |- *; apply prod_neq_R0; assumption.
254
apply Rle_ge; left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
255
unfold Rdiv in |- *; rewrite (Rmult_comm (Rsqr r)); repeat rewrite Rabs_mult;
256
rewrite Rabs_Rabsolu; rewrite pow_1_abs.
258
repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l.
259
rewrite Rinv_mult_distr.
260
rewrite Rinv_involutive.
263
rewrite pow_1_abs; rewrite Rinv_1; rewrite Rmult_1_l.
264
rewrite Rinv_mult_distr.
265
rewrite <- Rabs_Rinv.
266
rewrite Rinv_involutive.
268
do 2 rewrite Rabs_Rabsolu.
269
rewrite (Rmult_comm (Rabs (r ^ (2 * S n)))).
270
rewrite Rmult_assoc; apply Rmult_eq_compat_l.
272
rewrite Rabs_Rabsolu.
273
repeat rewrite Rabs_right.
274
replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r).
275
do 2 rewrite <- Rmult_assoc.
276
rewrite <- Rinv_l_sym.
277
unfold Rsqr in |- *; ring.
278
apply pow_nonzero; assumption.
279
replace (2 * S n)%nat with (S (S (2 * n))).
282
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
283
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
284
apply Rabs_no_R0; apply pow_nonzero; assumption.
285
apply INR_fact_neq_0.
286
apply Rinv_neq_0_compat; apply INR_fact_neq_0.
287
apply Rabs_no_R0; apply Rinv_neq_0_compat; apply INR_fact_neq_0.
288
apply Rabs_no_R0; apply pow_nonzero; assumption.
289
apply pow_nonzero; discrR.
290
apply INR_fact_neq_0.
291
apply pow_nonzero; discrR.
292
apply Rinv_neq_0_compat; apply INR_fact_neq_0.
293
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
294
[ assumption | apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption ].
295
assert (H0 := cond_pos r); red in |- *; intro; rewrite H1 in H0;
296
elim (Rlt_irrefl _ H0).
299
(** (sin h)/h -> 1 when h -> 0 *)
300
Lemma derivable_pt_lim_sin_0 : derivable_pt_lim sin 0 1.
302
unfold derivable_pt_lim in |- *; intros.
304
(fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)).
306
intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
308
set (r := mkposreal _ Rlt_0_1).
310
intro; cut (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y).
311
intro; cut (Boule 0 r 0).
312
intro; assert (H2 := SFL_continuity_pt _ cv _ X0 H0 _ H1).
313
unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2;
314
unfold limit_in in H2; simpl in H2; unfold R_dist in H2.
315
elim (H2 _ H); intros alp H3.
317
exists (mkposreal _ H4).
318
simpl in |- *; intros.
319
rewrite sin_0; rewrite Rplus_0_l; unfold Rminus in |- *; rewrite Ropp_0;
321
cut (Rabs (SFL fn cv h - SFL fn cv 0) < eps).
322
intro; cut (SFL fn cv 0 = 1).
323
intro; cut (SFL fn cv h = sin h / h).
324
intro; rewrite H9 in H8; rewrite H10 in H8.
326
unfold SFL, sin in |- *.
328
case (exist_sin (Rsqr h)); intros.
329
unfold Rdiv in |- *; rewrite (Rinv_r_simpl_m h x0 H6).
332
unfold sin_in in s; unfold sin_n, infinite_sum in s;
333
unfold SP, fn, Un_cv in |- *; intros.
334
elim (s _ H10); intros N0 H11.
336
unfold R_dist in |- *; unfold R_dist in H11.
338
(sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * h ^ (2 * k)) n)
340
(sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * Rsqr h ^ i) n).
341
apply H11; assumption.
342
apply sum_eq; intros; apply Rmult_eq_compat_l; unfold Rsqr in |- *;
343
rewrite pow_sqr; reflexivity.
344
unfold SFL, sin in |- *.
348
unfold SP, fn in |- *; unfold Un_cv in |- *; intros; exists 1%nat; intros.
349
unfold R_dist in |- *;
351
(sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * 0 ^ (2 * k)) n)
353
unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
355
simpl in |- *; rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite Rinv_1;
356
rewrite Rmult_1_r; pattern 1 at 1 in |- *; rewrite <- Rplus_0_r;
357
apply Rplus_eq_compat_l.
358
symmetry in |- *; apply sum_eq_R0; intros.
359
rewrite Rmult_0_l; rewrite Rmult_0_r; reflexivity.
360
unfold ge in H10; apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H10 ].
363
unfold D_x, no_cond in |- *; split.
365
apply (sym_not_eq (A:=R)); apply H6.
366
unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; apply H7.
367
unfold Boule in |- *; unfold Rminus in |- *; rewrite Ropp_0;
368
rewrite Rplus_0_r; rewrite Rabs_R0; apply (cond_pos r).
369
intros; unfold fn in |- *;
370
replace (fun x:R => (-1) ^ n / INR (fact (2 * n + 1)) * x ^ (2 * n)) with
371
(fct_cte ((-1) ^ n / INR (fact (2 * n + 1))) * pow_fct (2 * n))%F;
372
[ idtac | reflexivity ].
373
apply continuity_pt_mult.
374
apply derivable_continuous_pt.
375
apply derivable_pt_const.
376
apply derivable_continuous_pt.
377
apply (derivable_pt_pow (2 * n) y).
379
apply (CVN_R_CVS _ X).
380
apply CVN_R_sin; unfold fn in |- *; reflexivity.
383
(** ((cos h)-1)/h -> 0 when h -> 0 *)
384
Lemma derivable_pt_lim_cos_0 : derivable_pt_lim cos 0 0.
386
unfold derivable_pt_lim in |- *; intros.
387
assert (H0 := derivable_pt_lim_sin_0).
388
unfold derivable_pt_lim in H0.
390
intro; elim (H0 _ H1); intros del H2.
391
cut (continuity_pt sin 0).
392
intro; unfold continuity_pt in H3; unfold continue_in in H3;
393
unfold limit1_in in H3; unfold limit_in in H3; simpl in H3;
395
cut (0 < eps / 2); [ intro | assumption ].
396
elim (H3 _ H4); intros del_c H5.
397
cut (0 < Rmin del del_c).
398
intro; set (delta := mkposreal _ H6).
399
exists delta; intros.
400
rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))).
401
unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r.
402
unfold Rdiv in |- *; do 2 rewrite Ropp_mult_distr_l_reverse.
404
replace (2 * Rsqr (sin (h * / 2)) * / h) with
405
(sin (h / 2) * (sin (h / 2) / (h / 2) - 1) + sin (h / 2)).
406
apply Rle_lt_trans with
407
(Rabs (sin (h / 2) * (sin (h / 2) / (h / 2) - 1)) + Rabs (sin (h / 2))).
409
rewrite (double_var eps); apply Rplus_lt_compat.
410
apply Rle_lt_trans with (Rabs (sin (h / 2) / (h / 2) - 1)).
411
rewrite Rabs_mult; rewrite Rmult_comm;
412
pattern (Rabs (sin (h / 2) / (h / 2) - 1)) at 2 in |- *;
413
rewrite <- Rmult_1_r; apply Rmult_le_compat_l.
415
assert (H9 := SIN_bound (h / 2)).
416
unfold Rabs in |- *; case (Rcase_abs (sin (h / 2))); intro.
417
pattern 1 at 3 in |- *; rewrite <- (Ropp_involutive 1).
418
apply Ropp_le_contravar.
419
elim H9; intros; assumption.
420
elim H9; intros; assumption.
421
cut (Rabs (h / 2) < del).
422
intro; cut (h / 2 <> 0).
423
intro; assert (H11 := H2 _ H10 H9).
424
rewrite Rplus_0_l in H11; rewrite sin_0 in H11.
425
rewrite Rminus_0_r in H11; apply H11.
426
unfold Rdiv in |- *; apply prod_neq_R0.
428
apply Rinv_neq_0_compat; discrR.
429
apply Rlt_trans with (del / 2).
430
unfold Rdiv in |- *; rewrite Rabs_mult.
431
rewrite (Rabs_right (/ 2)).
432
do 2 rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l.
433
apply Rinv_0_lt_compat; prove_sup0.
434
apply Rlt_le_trans with (pos delta).
436
unfold delta in |- *; simpl in |- *; apply Rmin_l.
437
apply Rle_ge; left; apply Rinv_0_lt_compat; prove_sup0.
438
rewrite <- (Rplus_0_r (del / 2)); pattern del at 1 in |- *;
439
rewrite (double_var del); apply Rplus_lt_compat_l;
440
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
441
apply (cond_pos del).
442
apply Rinv_0_lt_compat; prove_sup0.
443
elim H5; intros; assert (H11 := H10 (h / 2)).
444
rewrite sin_0 in H11; do 2 rewrite Rminus_0_r in H11.
447
unfold D_x, no_cond in |- *; split.
449
apply (sym_not_eq (A:=R)); unfold Rdiv in |- *; apply prod_neq_R0.
451
apply Rinv_neq_0_compat; discrR.
452
apply Rlt_trans with (del_c / 2).
453
unfold Rdiv in |- *; rewrite Rabs_mult.
454
rewrite (Rabs_right (/ 2)).
455
do 2 rewrite <- (Rmult_comm (/ 2)).
456
apply Rmult_lt_compat_l.
457
apply Rinv_0_lt_compat; prove_sup0.
458
apply Rlt_le_trans with (pos delta).
460
unfold delta in |- *; simpl in |- *; apply Rmin_r.
461
apply Rle_ge; left; apply Rinv_0_lt_compat; prove_sup0.
462
rewrite <- (Rplus_0_r (del_c / 2)); pattern del_c at 2 in |- *;
463
rewrite (double_var del_c); apply Rplus_lt_compat_l.
464
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
466
apply Rinv_0_lt_compat; prove_sup0.
467
rewrite Rmult_minus_distr_l; rewrite Rmult_1_r; unfold Rminus in |- *;
468
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
469
rewrite (Rmult_comm 2); unfold Rdiv, Rsqr in |- *.
470
repeat rewrite Rmult_assoc.
471
repeat apply Rmult_eq_compat_l.
472
rewrite Rinv_mult_distr.
473
rewrite Rinv_involutive.
477
apply Rinv_neq_0_compat; discrR.
478
pattern h at 2 in |- *; replace h with (2 * (h / 2)).
479
rewrite (cos_2a_sin (h / 2)).
480
rewrite cos_0; unfold Rsqr in |- *; ring.
481
unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
483
unfold Rmin in |- *; case (Rle_dec del del_c); intro.
484
apply (cond_pos del).
485
elim H5; intros; assumption.
486
apply continuity_sin.
487
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
488
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
492
Theorem derivable_pt_lim_sin : forall x:R, derivable_pt_lim sin x (cos x).
494
intro; assert (H0 := derivable_pt_lim_sin_0).
495
assert (H := derivable_pt_lim_cos_0).
496
unfold derivable_pt_lim in H0, H.
497
unfold derivable_pt_lim in |- *; intros.
500
| unfold Rdiv in |- *; apply Rmult_lt_0_compat;
501
[ apply H1 | apply Rinv_0_lt_compat; prove_sup0 ] ].
502
elim (H0 _ H2); intros alp1 H3.
503
elim (H _ H2); intros alp2 H4.
504
set (alp := Rmin alp1 alp2).
506
intro; exists (mkposreal _ H5); intros.
507
replace ((sin (x + h) - sin x) / h - cos x) with
508
(sin x * ((cos h - 1) / h) + cos x * (sin h / h - 1)).
509
apply Rle_lt_trans with
510
(Rabs (sin x * ((cos h - 1) / h)) + Rabs (cos x * (sin h / h - 1))).
512
rewrite (double_var eps); apply Rplus_lt_compat.
513
apply Rle_lt_trans with (Rabs ((cos h - 1) / h)).
514
rewrite Rabs_mult; rewrite Rmult_comm;
515
pattern (Rabs ((cos h - 1) / h)) at 2 in |- *; rewrite <- Rmult_1_r;
516
apply Rmult_le_compat_l.
518
assert (H8 := SIN_bound x); elim H8; intros.
519
unfold Rabs in |- *; case (Rcase_abs (sin x)); intro.
520
rewrite <- (Ropp_involutive 1).
521
apply Ropp_le_contravar; assumption.
524
intro; assert (H9 := H4 _ H6 H8).
525
rewrite cos_0 in H9; rewrite Rplus_0_l in H9; rewrite Rminus_0_r in H9;
527
apply Rlt_le_trans with alp.
529
unfold alp in |- *; apply Rmin_r.
530
apply Rle_lt_trans with (Rabs (sin h / h - 1)).
531
rewrite Rabs_mult; rewrite Rmult_comm;
532
pattern (Rabs (sin h / h - 1)) at 2 in |- *; rewrite <- Rmult_1_r;
533
apply Rmult_le_compat_l.
535
assert (H8 := COS_bound x); elim H8; intros.
536
unfold Rabs in |- *; case (Rcase_abs (cos x)); intro.
537
rewrite <- (Ropp_involutive 1); apply Ropp_le_contravar; assumption.
540
intro; assert (H9 := H3 _ H6 H8).
541
rewrite sin_0 in H9; rewrite Rplus_0_l in H9; rewrite Rminus_0_r in H9;
543
apply Rlt_le_trans with alp.
545
unfold alp in |- *; apply Rmin_l.
546
rewrite sin_plus; unfold Rminus, Rdiv in |- *;
547
repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
548
repeat rewrite Rmult_assoc; repeat rewrite Rplus_assoc;
549
apply Rplus_eq_compat_l.
550
rewrite (Rplus_comm (sin x * (-1 * / h))); repeat rewrite Rplus_assoc;
551
apply Rplus_eq_compat_l.
552
rewrite Ropp_mult_distr_r_reverse; rewrite Ropp_mult_distr_l_reverse;
553
rewrite Rmult_1_r; rewrite Rmult_1_l; rewrite Ropp_mult_distr_r_reverse;
554
rewrite <- Ropp_mult_distr_l_reverse; apply Rplus_comm.
555
unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec alp1 alp2); intro.
556
apply (cond_pos alp1).
557
apply (cond_pos alp2).
560
Lemma derivable_pt_lim_cos : forall x:R, derivable_pt_lim cos x (- sin x).
562
intro; cut (forall h:R, sin (h + PI / 2) = cos h).
563
intro; replace (- sin x) with (cos (x + PI / 2) * (1 + 0)).
564
generalize (derivable_pt_lim_comp (id + fct_cte (PI / 2))%F sin); intros.
565
cut (derivable_pt_lim (id + fct_cte (PI / 2)) x (1 + 0)).
566
cut (derivable_pt_lim sin ((id + fct_cte (PI / 2))%F x) (cos (x + PI / 2))).
567
intros; generalize (H0 _ _ _ H2 H1);
568
replace (comp sin (id + fct_cte (PI / 2))%F) with
569
(fun x:R => sin (x + PI / 2)); [ idtac | reflexivity ].
570
unfold derivable_pt_lim in |- *; intros.
571
elim (H3 eps H4); intros.
573
intros; rewrite <- (H (x + h)); rewrite <- (H x); apply H5; assumption.
574
apply derivable_pt_lim_sin.
575
apply derivable_pt_lim_plus.
576
apply derivable_pt_lim_id.
577
apply derivable_pt_lim_const.
578
rewrite sin_cos; rewrite <- (Rplus_comm x); ring.
579
intro; rewrite cos_sin; rewrite Rplus_comm; reflexivity.
582
Lemma derivable_pt_sin : forall x:R, derivable_pt sin x.
584
unfold derivable_pt in |- *; intro.
586
apply derivable_pt_lim_sin.
589
Lemma derivable_pt_cos : forall x:R, derivable_pt cos x.
591
unfold derivable_pt in |- *; intro.
593
apply derivable_pt_lim_cos.
596
Lemma derivable_sin : derivable sin.
598
unfold derivable in |- *; intro; apply derivable_pt_sin.
601
Lemma derivable_cos : derivable cos.
603
unfold derivable in |- *; intro; apply derivable_pt_cos.
606
Lemma derive_pt_sin :
607
forall x:R, derive_pt sin x (derivable_pt_sin _) = cos x.
609
intros; apply derive_pt_eq_0.
610
apply derivable_pt_lim_sin.
613
Lemma derive_pt_cos :
614
forall x:R, derive_pt cos x (derivable_pt_cos _) = - sin x.
616
intros; apply derive_pt_eq_0.
617
apply derivable_pt_lim_cos.
added
removed
theories/Reals/Rtrigo_reg.v
