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
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Ranalysis4.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo.
Require Import Ranalysis1.
Require Import Ranalysis3.
Require Import Exp_prop.
Open Local Scope R_scope.
(**********)
Lemma derivable_pt_inv :
forall (f:R -> R) (x:R),
f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x.
Proof.
intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x).
intro X0; apply X0.
apply derivable_pt_div.
apply derivable_pt_const.
assumption.
assumption.
unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros;
unfold derivable_pt in |- *; exists x0;
unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *;
unfold derivable_pt_abs in p; unfold derivable_pt_lim in p;
intros; elim (p eps H0); intros; exists x1; intros;
unfold Rdiv in H1; unfold Rdiv in |- *; rewrite <- (Rmult_1_l (/ f x));
rewrite <- (Rmult_1_l (/ f (x + h))).
apply H1; assumption.
Qed.
(**********)
Lemma pr_nu_var :
forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
f = g -> derive_pt f x pr1 = derive_pt g x pr2.
Proof.
unfold derivable_pt, derive_pt in |- *; intros.
elim pr1; intros.
elim pr2; intros.
simpl in |- *.
rewrite H in p.
apply uniqueness_limite with g x; assumption.
Qed.
(**********)
Lemma pr_nu_var2 :
forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
(forall h:R, f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.
Proof.
unfold derivable_pt, derive_pt in |- *; intros.
elim pr1; intros.
elim pr2; intros.
simpl in |- *.
assert (H0 := uniqueness_step2 _ _ _ p).
assert (H1 := uniqueness_step2 _ _ _ p0).
cut (limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) x1 0).
intro; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2).
assumption.
unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
simpl in |- *; unfold R_dist in |- *; unfold limit1_in in H1;
unfold limit_in in H1; unfold dist in H1; simpl in H1;
unfold R_dist in H1.
intros; elim (H1 eps H2); intros.
elim H3; intros.
exists x2.
split.
assumption.
intros; do 2 rewrite H; apply H5; assumption.
Qed.
(**********)
Lemma derivable_inv :
forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f).
Proof.
intros f H X.
unfold derivable in |- *; intro x.
apply derivable_pt_inv.
apply (H x).
apply (X x).
Qed.
Lemma derive_pt_inv :
forall (f:R -> R) (x:R) (pr:derivable_pt f x) (na:f x <> 0),
derive_pt (/ f) x (derivable_pt_inv f x na pr) =
- derive_pt f x pr / Rsqr (f x).
Proof.
intros;
replace (derive_pt (/ f) x (derivable_pt_inv f x na pr)) with
(derive_pt (fct_cte 1 / f) x
(derivable_pt_div (fct_cte 1) f x (derivable_pt_const 1 x) pr na)).
rewrite derive_pt_div; rewrite derive_pt_const; unfold fct_cte in |- *;
rewrite Rmult_0_l; rewrite Rmult_1_r; unfold Rminus in |- *;
rewrite Rplus_0_l; reflexivity.
apply pr_nu_var2.
intro; unfold div_fct, fct_cte, inv_fct in |- *.
unfold Rdiv in |- *; ring.
Qed.
(** Rabsolu *)
Lemma Rabs_derive_1 : forall x:R, 0 < x -> derivable_pt_lim Rabs x 1.
Proof.
intros.
unfold derivable_pt_lim in |- *; intros.
exists (mkposreal x H); intros.
rewrite (Rabs_right x).
rewrite (Rabs_right (x + h)).
rewrite Rplus_comm.
unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_r.
rewrite Rplus_0_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym.
rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0.
apply H1.
apply Rle_ge.
case (Rcase_abs h); intro.
rewrite (Rabs_left h r) in H2.
left; rewrite Rplus_comm; apply Rplus_lt_reg_r with (- h); rewrite Rplus_0_r;
rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
apply H2.
apply Rplus_le_le_0_compat.
left; apply H.
apply Rge_le; apply r.
left; apply H.
Qed.
Lemma Rabs_derive_2 : forall x:R, x < 0 -> derivable_pt_lim Rabs x (-1).
Proof.
intros.
unfold derivable_pt_lim in |- *; intros.
cut (0 < - x).
intro; exists (mkposreal (- x) H1); intros.
rewrite (Rabs_left x).
rewrite (Rabs_left (x + h)).
rewrite Rplus_comm.
rewrite Ropp_plus_distr.
unfold Rminus in |- *; rewrite Ropp_involutive; rewrite Rplus_assoc;
rewrite Rplus_opp_l.
rewrite Rplus_0_r; unfold Rdiv in |- *.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- Rinv_r_sym.
rewrite Ropp_involutive; rewrite Rplus_opp_l; rewrite Rabs_R0; apply H0.
apply H2.
case (Rcase_abs h); intro.
apply Ropp_lt_cancel.
rewrite Ropp_0; rewrite Ropp_plus_distr; apply Rplus_lt_0_compat.
apply H1.
apply Ropp_0_gt_lt_contravar; apply r.
rewrite (Rabs_right h r) in H3.
apply Rplus_lt_reg_r with (- x); rewrite Rplus_0_r; rewrite <- Rplus_assoc;
rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H3.
apply H.
apply Ropp_0_gt_lt_contravar; apply H.
Qed.
(** Rabsolu is derivable for all x <> 0 *)
Lemma Rderivable_pt_abs : forall x:R, x <> 0 -> derivable_pt Rabs x.
Proof.
intros.
case (total_order_T x 0); intro.
elim s; intro.
unfold derivable_pt in |- *; exists (-1).
apply (Rabs_derive_2 x a).
elim H; exact b.
unfold derivable_pt in |- *; exists 1.
apply (Rabs_derive_1 x r).
Qed.
(** Rabsolu is continuous for all x *)
Lemma Rcontinuity_abs : continuity Rabs.
Proof.
unfold continuity in |- *; intro.
case (Req_dec x 0); intro.
unfold continuity_pt in |- *; unfold continue_in in |- *;
unfold limit1_in in |- *; unfold limit_in in |- *;
simpl in |- *; unfold R_dist in |- *; intros; exists eps;
split.
apply H0.
intros; rewrite H; rewrite Rabs_R0; unfold Rminus in |- *; rewrite Ropp_0;
rewrite Rplus_0_r; rewrite Rabs_Rabsolu; elim H1;
intros; rewrite H in H3; unfold Rminus in H3; rewrite Ropp_0 in H3;
rewrite Rplus_0_r in H3; apply H3.
apply derivable_continuous_pt; apply (Rderivable_pt_abs x H).
Qed.
(** Finite sums : Sum a_k x^k *)
Lemma continuity_finite_sum :
forall (An:nat -> R) (N:nat),
continuity (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).
Proof.
intros; unfold continuity in |- *; intro.
induction N as [| N HrecN].
simpl in |- *.
apply continuity_pt_const.
unfold constant in |- *; intros; reflexivity.
replace (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with
((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) +
(fun y:R => (An (S N) * y ^ S N)%R))%F.
apply continuity_pt_plus.
apply HrecN.
replace (fun y:R => An (S N) * y ^ S N) with
(mult_real_fct (An (S N)) (fun y:R => y ^ S N)).
apply continuity_pt_scal.
apply derivable_continuous_pt.
apply derivable_pt_pow.
reflexivity.
reflexivity.
Qed.
Lemma derivable_pt_lim_fs :
forall (An:nat -> R) (x:R) (N:nat),
(0 < N)%nat ->
derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x
(sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)).
Proof.
intros; induction N as [| N HrecN].
elim (lt_irrefl _ H).
cut (N = 0%nat \/ (0 < N)%nat).
intro; elim H0; intro.
rewrite H1.
simpl in |- *.
replace (fun y:R => An 0%nat * 1 + An 1%nat * (y * 1)) with
(fct_cte (An 0%nat * 1) + mult_real_fct (An 1%nat) (id * fct_cte 1))%F.
replace (1 * An 1%nat * 1) with (0 + An 1%nat * (1 * fct_cte 1 x + id x * 0)).
apply derivable_pt_lim_plus.
apply derivable_pt_lim_const.
apply derivable_pt_lim_scal.
apply derivable_pt_lim_mult.
apply derivable_pt_lim_id.
apply derivable_pt_lim_const.
unfold fct_cte, id in |- *; ring.
reflexivity.
replace (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with
((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) +
(fun y:R => (An (S N) * y ^ S N)%R))%F.
replace (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N)))
with
(sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N) +
An (S N) * (INR (S (pred (S N))) * x ^ pred (S N))).
apply derivable_pt_lim_plus.
apply HrecN.
assumption.
replace (fun y:R => An (S N) * y ^ S N) with
(mult_real_fct (An (S N)) (fun y:R => y ^ S N)).
apply derivable_pt_lim_scal.
replace (pred (S N)) with N; [ idtac | reflexivity ].
pattern N at 3 in |- *; replace N with (pred (S N)).
apply derivable_pt_lim_pow.
reflexivity.
reflexivity.
cut (pred (S N) = S (pred N)).
intro; rewrite H2.
rewrite tech5.
apply Rplus_eq_compat_l.
rewrite <- H2.
replace (pred (S N)) with N; [ idtac | reflexivity ].
ring.
simpl in |- *.
apply S_pred with 0%nat; assumption.
unfold plus_fct in |- *.
simpl in |- *; reflexivity.
inversion H.
left; reflexivity.
right; apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
Qed.
Lemma derivable_pt_lim_finite_sum :
forall (An:nat -> R) (x:R) (N:nat),
derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x
match N with
| O => 0
| _ => sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)
end.
Proof.
intros.
induction N as [| N HrecN].
simpl in |- *.
rewrite Rmult_1_r.
replace (fun _:R => An 0%nat) with (fct_cte (An 0%nat));
[ apply derivable_pt_lim_const | reflexivity ].
apply derivable_pt_lim_fs; apply lt_O_Sn.
Qed.
Lemma derivable_pt_finite_sum :
forall (An:nat -> R) (N:nat) (x:R),
derivable_pt (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x.
Proof.
intros.
unfold derivable_pt in |- *.
assert (H := derivable_pt_lim_finite_sum An x N).
induction N as [| N HrecN].
exists 0; apply H.
exists
(sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N)));
apply H.
Qed.
Lemma derivable_finite_sum :
forall (An:nat -> R) (N:nat),
derivable (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).
Proof.
intros; unfold derivable in |- *; intro; apply derivable_pt_finite_sum.
Qed.
(** Regularity of hyperbolic functions *)
Lemma derivable_pt_lim_cosh : forall x:R, derivable_pt_lim cosh x (sinh x).
Proof.
intro.
unfold cosh, sinh in |- *; unfold Rdiv in |- *.
replace (fun x0:R => (exp x0 + exp (- x0)) * / 2) with
((exp + comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ].
replace ((exp x - exp (- x)) * / 2) with
((exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0).
apply derivable_pt_lim_mult.
apply derivable_pt_lim_plus.
apply derivable_pt_lim_exp.
apply derivable_pt_lim_comp.
apply derivable_pt_lim_opp.
apply derivable_pt_lim_id.
apply derivable_pt_lim_exp.
apply derivable_pt_lim_const.
unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte in |- *; ring.
Qed.
Lemma derivable_pt_lim_sinh : forall x:R, derivable_pt_lim sinh x (cosh x).
Proof.
intro.
unfold cosh, sinh in |- *; unfold Rdiv in |- *.
replace (fun x0:R => (exp x0 - exp (- x0)) * / 2) with
((exp - comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ].
replace ((exp x + exp (- x)) * / 2) with
((exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0).
apply derivable_pt_lim_mult.
apply derivable_pt_lim_minus.
apply derivable_pt_lim_exp.
apply derivable_pt_lim_comp.
apply derivable_pt_lim_opp.
apply derivable_pt_lim_id.
apply derivable_pt_lim_exp.
apply derivable_pt_lim_const.
unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte in |- *; ring.
Qed.
Lemma derivable_pt_exp : forall x:R, derivable_pt exp x.
Proof.
intro.
unfold derivable_pt in |- *.
exists (exp x).
apply derivable_pt_lim_exp.
Qed.
Lemma derivable_pt_cosh : forall x:R, derivable_pt cosh x.
Proof.
intro.
unfold derivable_pt in |- *.
exists (sinh x).
apply derivable_pt_lim_cosh.
Qed.
Lemma derivable_pt_sinh : forall x:R, derivable_pt sinh x.
Proof.
intro.
unfold derivable_pt in |- *.
exists (cosh x).
apply derivable_pt_lim_sinh.
Qed.
Lemma derivable_exp : derivable exp.
Proof.
unfold derivable in |- *; apply derivable_pt_exp.
Qed.
Lemma derivable_cosh : derivable cosh.
Proof.
unfold derivable in |- *; apply derivable_pt_cosh.
Qed.
Lemma derivable_sinh : derivable sinh.
Proof.
unfold derivable in |- *; apply derivable_pt_sinh.
Qed.
Lemma derive_pt_exp :
forall x:R, derive_pt exp x (derivable_pt_exp x) = exp x.
Proof.
intro; apply derive_pt_eq_0.
apply derivable_pt_lim_exp.
Qed.
Lemma derive_pt_cosh :
forall x:R, derive_pt cosh x (derivable_pt_cosh x) = sinh x.
Proof.
intro; apply derive_pt_eq_0.
apply derivable_pt_lim_cosh.
Qed.
Lemma derive_pt_sinh :
forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x.
Proof.
intro; apply derive_pt_eq_0.
apply derivable_pt_lim_sinh.
Qed.
|
