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: Ranalysis1.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
12
Require Import Rfunctions.
13
Require Export Rlimit.
14
Require Export Rderiv.
15
Open Local Scope R_scope.
16
Implicit Type f : R -> R.
18
(****************************************************)
19
(** * Basic operations on functions *)
20
(****************************************************)
21
Definition plus_fct f1 f2 (x:R) : R := f1 x + f2 x.
22
Definition opp_fct f (x:R) : R := - f x.
23
Definition mult_fct f1 f2 (x:R) : R := f1 x * f2 x.
24
Definition mult_real_fct (a:R) f (x:R) : R := a * f x.
25
Definition minus_fct f1 f2 (x:R) : R := f1 x - f2 x.
26
Definition div_fct f1 f2 (x:R) : R := f1 x / f2 x.
27
Definition div_real_fct (a:R) f (x:R) : R := a / f x.
28
Definition comp f1 f2 (x:R) : R := f1 (f2 x).
29
Definition inv_fct f (x:R) : R := / f x.
31
Delimit Scope Rfun_scope with F.
33
Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope].
34
Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope].
35
Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope].
36
Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope].
37
Arguments Scope inv_fct [Rfun_scope R_scope].
38
Arguments Scope opp_fct [Rfun_scope R_scope].
39
Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope].
40
Arguments Scope div_real_fct [R_scope Rfun_scope R_scope].
41
Arguments Scope comp [Rfun_scope Rfun_scope R_scope].
43
Infix "+" := plus_fct : Rfun_scope.
44
Notation "- x" := (opp_fct x) : Rfun_scope.
45
Infix "*" := mult_fct : Rfun_scope.
46
Infix "-" := minus_fct : Rfun_scope.
47
Infix "/" := div_fct : Rfun_scope.
48
Notation Local "f1 'o' f2" := (comp f1 f2)
49
(at level 20, right associativity) : Rfun_scope.
50
Notation "/ x" := (inv_fct x) : Rfun_scope.
52
Definition fct_cte (a x:R) : R := a.
53
Definition id (x:R) := x.
55
(****************************************************)
56
(** * Variations of functions *)
57
(****************************************************)
58
Definition increasing f : Prop := forall x y:R, x <= y -> f x <= f y.
59
Definition decreasing f : Prop := forall x y:R, x <= y -> f y <= f x.
60
Definition strict_increasing f : Prop := forall x y:R, x < y -> f x < f y.
61
Definition strict_decreasing f : Prop := forall x y:R, x < y -> f y < f x.
62
Definition constant f : Prop := forall x y:R, f x = f y.
65
Definition no_cond (x:R) : Prop := True.
68
Definition constant_D_eq f (D:R -> Prop) (c:R) : Prop :=
69
forall x:R, D x -> f x = c.
71
(***************************************************)
72
(** * Definition of continuity as a limit *)
73
(***************************************************)
76
Definition continuity_pt f (x0:R) : Prop := continue_in f no_cond x0.
77
Definition continuity f : Prop := forall x:R, continuity_pt f x.
79
Arguments Scope continuity_pt [Rfun_scope R_scope].
80
Arguments Scope continuity [Rfun_scope].
83
Lemma continuity_pt_plus :
85
continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 + f2) x0.
87
unfold continuity_pt, plus_fct in |- *; unfold continue_in in |- *; intros;
88
apply limit_plus; assumption.
91
Lemma continuity_pt_opp :
92
forall f (x0:R), continuity_pt f x0 -> continuity_pt (- f) x0.
94
unfold continuity_pt, opp_fct in |- *; unfold continue_in in |- *; intros;
95
apply limit_Ropp; assumption.
98
Lemma continuity_pt_minus :
100
continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 - f2) x0.
102
unfold continuity_pt, minus_fct in |- *; unfold continue_in in |- *; intros;
103
apply limit_minus; assumption.
106
Lemma continuity_pt_mult :
108
continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 * f2) x0.
110
unfold continuity_pt, mult_fct in |- *; unfold continue_in in |- *; intros;
111
apply limit_mul; assumption.
114
Lemma continuity_pt_const : forall f (x0:R), constant f -> continuity_pt f x0.
116
unfold constant, continuity_pt in |- *; unfold continue_in in |- *;
117
unfold limit1_in in |- *; unfold limit_in in |- *;
118
intros; exists 1; split;
120
| intros; generalize (H x x0); intro; rewrite H2; simpl in |- *;
121
rewrite R_dist_eq; assumption ].
124
Lemma continuity_pt_scal :
126
continuity_pt f x0 -> continuity_pt (mult_real_fct a f) x0.
128
unfold continuity_pt, mult_real_fct in |- *; unfold continue_in in |- *;
129
intros; apply (limit_mul (fun x:R => a) f (D_x no_cond x0) a (f x0) x0).
130
unfold limit1_in in |- *; unfold limit_in in |- *; intros; exists 1; split.
132
intros; rewrite R_dist_eq; assumption.
136
Lemma continuity_pt_inv :
137
forall f (x0:R), continuity_pt f x0 -> f x0 <> 0 -> continuity_pt (/ f) x0.
140
replace (/ f)%F with (fun x:R => / f x).
141
unfold continuity_pt in |- *; unfold continue_in in |- *; intros;
142
apply limit_inv; assumption.
143
unfold inv_fct in |- *; reflexivity.
146
Lemma div_eq_inv : forall f1 f2, (f1 / f2)%F = (f1 * / f2)%F.
151
Lemma continuity_pt_div :
153
continuity_pt f1 x0 ->
154
continuity_pt f2 x0 -> f2 x0 <> 0 -> continuity_pt (f1 / f2) x0.
156
intros; rewrite (div_eq_inv f1 f2); apply continuity_pt_mult;
157
[ assumption | apply continuity_pt_inv; assumption ].
160
Lemma continuity_pt_comp :
162
continuity_pt f1 x -> continuity_pt f2 (f1 x) -> continuity_pt (f2 o f1) x.
164
unfold continuity_pt in |- *; unfold continue_in in |- *; intros;
167
(limit1_in (fun x0:R => f2 (f1 x0))
168
(Dgf (D_x no_cond x) (D_x no_cond (f1 x)) f1) (
170
limit1_in (fun x0:R => f2 (f1 x0)) (D_x no_cond x) (f2 (f1 x)) x).
175
unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
176
simpl in |- *; unfold R_dist in |- *; intros.
177
assert (H3 := H1 eps H2).
181
elim H4; intros; assumption.
182
intros; case (Req_dec (f1 x) (f1 x1)); intro.
183
rewrite H6; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
185
elim H4; intros; apply H8.
187
unfold Dgf, D_x, no_cond in |- *.
191
elim H5; unfold D_x, no_cond in |- *; intros.
192
elim H9; intros; assumption.
196
elim H5; intros; assumption.
200
Lemma continuity_plus :
201
forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 + f2).
203
unfold continuity in |- *; intros;
204
apply (continuity_pt_plus f1 f2 x (H x) (H0 x)).
207
Lemma continuity_opp : forall f, continuity f -> continuity (- f).
209
unfold continuity in |- *; intros; apply (continuity_pt_opp f x (H x)).
212
Lemma continuity_minus :
213
forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 - f2).
215
unfold continuity in |- *; intros;
216
apply (continuity_pt_minus f1 f2 x (H x) (H0 x)).
219
Lemma continuity_mult :
220
forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 * f2).
222
unfold continuity in |- *; intros;
223
apply (continuity_pt_mult f1 f2 x (H x) (H0 x)).
226
Lemma continuity_const : forall f, constant f -> continuity f.
228
unfold continuity in |- *; intros; apply (continuity_pt_const f x H).
231
Lemma continuity_scal :
232
forall f (a:R), continuity f -> continuity (mult_real_fct a f).
234
unfold continuity in |- *; intros; apply (continuity_pt_scal f a x (H x)).
237
Lemma continuity_inv :
238
forall f, continuity f -> (forall x:R, f x <> 0) -> continuity (/ f).
240
unfold continuity in |- *; intros; apply (continuity_pt_inv f x (H x) (H0 x)).
243
Lemma continuity_div :
246
continuity f2 -> (forall x:R, f2 x <> 0) -> continuity (f1 / f2).
248
unfold continuity in |- *; intros;
249
apply (continuity_pt_div f1 f2 x (H x) (H0 x) (H1 x)).
252
Lemma continuity_comp :
253
forall f1 f2, continuity f1 -> continuity f2 -> continuity (f2 o f1).
255
unfold continuity in |- *; intros.
256
apply (continuity_pt_comp f1 f2 x (H x) (H0 (f1 x))).
260
(*****************************************************)
261
(** * Derivative's definition using Landau's kernel *)
262
(*****************************************************)
264
Definition derivable_pt_lim f (x l:R) : Prop :=
267
exists delta : posreal,
269
h <> 0 -> Rabs h < delta -> Rabs ((f (x + h) - f x) / h - l) < eps).
271
Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l.
273
Definition derivable_pt f (x:R) := { l:R | derivable_pt_abs f x l }.
274
Definition derivable f := forall x:R, derivable_pt f x.
276
Definition derive_pt f (x:R) (pr:derivable_pt f x) := proj1_sig pr.
277
Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x).
279
Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
280
Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope].
281
Arguments Scope derivable_pt [Rfun_scope R_scope].
282
Arguments Scope derivable [Rfun_scope].
283
Arguments Scope derive_pt [Rfun_scope R_scope _].
284
Arguments Scope derive [Rfun_scope _].
286
Definition antiderivative f (g:R -> R) (a b:R) : Prop :=
288
a <= x <= b -> exists pr : derivable_pt g x, f x = derive_pt g x pr) /\
290
(**************************************)
291
(** * Class of differential functions *)
292
(**************************************)
293
Record Differential : Type := mkDifferential
294
{d1 :> R -> R; cond_diff : derivable d1}.
296
Record Differential_D2 : Type := mkDifferential_D2
298
cond_D1 : derivable d2;
299
cond_D2 : derivable (derive d2 cond_D1)}.
302
Lemma uniqueness_step1 :
303
forall f (x l1 l2:R),
304
limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l1 0 ->
305
limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l2 0 ->
310
(single_limit (fun h:R => (f (x + h) - f x) / h) (
311
fun h:R => h <> 0) l1 l2 0); try assumption.
312
unfold adhDa in |- *; intros; exists (alp / 2).
314
unfold Rdiv in |- *; apply prod_neq_R0.
315
red in |- *; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1).
316
apply Rinv_neq_0_compat; discrR.
317
unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0;
318
rewrite Rplus_0_r; unfold Rdiv in |- *; rewrite Rabs_mult.
319
replace (Rabs (/ 2)) with (/ 2).
320
replace (Rabs alp) with alp.
321
apply Rmult_lt_reg_l with 2.
323
rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym;
324
[ idtac | discrR ]; rewrite Rmult_1_r; rewrite double;
325
pattern alp at 1 in |- *; replace alp with (alp + 0);
326
[ idtac | ring ]; apply Rplus_lt_compat_l; assumption.
327
symmetry in |- *; apply Rabs_right; left; assumption.
328
symmetry in |- *; apply Rabs_right; left; change (0 < / 2) in |- *;
329
apply Rinv_0_lt_compat; prove_sup0.
332
Lemma uniqueness_step2 :
334
derivable_pt_lim f x l ->
335
limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0.
337
unfold derivable_pt_lim in |- *; intros; unfold limit1_in in |- *;
338
unfold limit_in in |- *; intros.
339
assert (H1 := H eps H0).
344
simpl in |- *; unfold R_dist in |- *; intros.
348
| unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5;
352
Lemma uniqueness_step3 :
354
limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0 ->
355
derivable_pt_lim f x l.
357
unfold limit1_in, derivable_pt_lim in |- *; unfold limit_in in |- *;
358
unfold dist in |- *; simpl in |- *; intros.
360
intros; elim H1; intros.
361
exists (mkposreal x0 H2).
362
simpl in |- *; intros; unfold R_dist in H3; apply (H3 h).
365
| unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; assumption ].
368
Lemma uniqueness_limite :
369
forall f (x l1 l2:R),
370
derivable_pt_lim f x l1 -> derivable_pt_lim f x l2 -> l1 = l2.
373
assert (H1 := uniqueness_step2 _ _ _ H).
374
assert (H2 := uniqueness_step2 _ _ _ H0).
375
assert (H3 := uniqueness_step1 _ _ _ _ H1 H2).
380
forall f (x l:R) (pr:derivable_pt f x),
381
derive_pt f x pr = l <-> derivable_pt_lim f x l.
384
intro; assert (H1 := proj2_sig pr); unfold derive_pt in H; rewrite H in H1;
386
intro; assert (H1 := proj2_sig pr); unfold derivable_pt_abs in H1.
387
assert (H2 := uniqueness_limite _ _ _ _ H H1).
388
unfold derive_pt in |- *; unfold derivable_pt_abs in |- *.
389
symmetry in |- *; assumption.
393
Lemma derive_pt_eq_0 :
394
forall f (x l:R) (pr:derivable_pt f x),
395
derivable_pt_lim f x l -> derive_pt f x pr = l.
397
intros; elim (derive_pt_eq f x l pr); intros.
402
Lemma derive_pt_eq_1 :
403
forall f (x l:R) (pr:derivable_pt f x),
404
derive_pt f x pr = l -> derivable_pt_lim f x l.
406
intros; elim (derive_pt_eq f x l pr); intros.
411
(**********************************************************************)
412
(** * Equivalence of this definition with the one using limit concept *)
413
(**********************************************************************)
414
Lemma derive_pt_D_in :
415
forall f (df:R -> R) (x:R) (pr:derivable_pt f x),
416
D_in f df no_cond x <-> derive_pt f x pr = df x.
419
unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
420
simpl in |- *; unfold R_dist in |- *; intros.
421
apply derive_pt_eq_0.
422
unfold derivable_pt_lim in |- *.
423
intros; elim (H eps H0); intros alpha H1; elim H1; intros;
424
exists (mkposreal alpha H2); intros; generalize (H3 (x + h));
425
intro; cut (x + h - x = h);
426
[ intro; cut (D_x no_cond x (x + h) /\ Rabs (x + h - x) < alpha);
427
[ intro; generalize (H6 H8); rewrite H7; intro; assumption
429
[ unfold D_x in |- *; split;
430
[ unfold no_cond in |- *; trivial
431
| apply Rminus_not_eq_right; rewrite H7; assumption ]
432
| rewrite H7; assumption ] ]
435
assert (H0 := derive_pt_eq_1 f x (df x) pr H).
436
unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
437
unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
439
elim (H0 eps H1); intros alpha H2; exists (pos alpha); split.
440
apply (cond_pos alpha).
441
intros; elim H3; intros; unfold D_x in H4; elim H4; intros; cut (x0 - x <> 0).
442
intro; generalize (H2 (x0 - x) H8 H5); replace (x + (x0 - x)) with x0.
448
Lemma derivable_pt_lim_D_in :
449
forall f (df:R -> R) (x:R),
450
D_in f df no_cond x <-> derivable_pt_lim f x (df x).
453
unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
454
simpl in |- *; unfold R_dist in |- *; intros.
455
unfold derivable_pt_lim in |- *.
456
intros; elim (H eps H0); intros alpha H1; elim H1; intros;
457
exists (mkposreal alpha H2); intros; generalize (H3 (x + h));
458
intro; cut (x + h - x = h);
459
[ intro; cut (D_x no_cond x (x + h) /\ Rabs (x + h - x) < alpha);
460
[ intro; generalize (H6 H8); rewrite H7; intro; assumption
462
[ unfold D_x in |- *; split;
463
[ unfold no_cond in |- *; trivial
464
| apply Rminus_not_eq_right; rewrite H7; assumption ]
465
| rewrite H7; assumption ] ]
468
unfold derivable_pt_lim in H.
469
unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
470
unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
472
elim (H eps H0); intros alpha H2; exists (pos alpha); split.
473
apply (cond_pos alpha).
475
elim H1; intros; unfold D_x in H3; elim H3; intros; cut (x0 - x <> 0).
476
intro; generalize (H2 (x0 - x) H7 H4); replace (x + (x0 - x)) with x0.
483
(***********************************)
484
(** * derivability -> continuity *)
485
(***********************************)
487
Lemma derivable_derive :
488
forall f (x:R) (pr:derivable_pt f x), exists l : R, derive_pt f x pr = l.
490
intros; exists (proj1_sig pr).
491
unfold derive_pt in |- *; reflexivity.
494
Theorem derivable_continuous_pt :
495
forall f (x:R), derivable_pt f x -> continuity_pt f x.
498
generalize (derivable_derive f x X); intro.
500
cut (l = fct_cte l x).
503
generalize (derive_pt_D_in f (fct_cte l) x); intro.
505
generalize (H4 H1); intro.
506
unfold continuity_pt in |- *.
507
apply (cont_deriv f (fct_cte l) no_cond x H5).
508
unfold fct_cte in |- *; reflexivity.
511
Theorem derivable_continuous : forall f, derivable f -> continuity f.
513
unfold derivable, continuity in |- *; intros f X x.
514
apply (derivable_continuous_pt f x (X x)).
517
(****************************************************************)
519
(****************************************************************)
521
Lemma derivable_pt_lim_plus :
522
forall f1 f2 (x l1 l2:R),
523
derivable_pt_lim f1 x l1 ->
524
derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 + f2) x (l1 + l2).
526
apply uniqueness_step3.
527
assert (H1 := uniqueness_step2 _ _ _ H).
528
assert (H2 := uniqueness_step2 _ _ _ H0).
529
unfold plus_fct in |- *.
532
(f1 (x + h) + f2 (x + h) - (f1 x + f2 x)) / h =
533
(f1 (x + h) - f1 x) / h + (f2 (x + h) - f2 x) / h).
536
(limit_plus (fun h':R => (f1 (x + h') - f1 x) / h')
537
(fun h':R => (f2 (x + h') - f2 x) / h') (fun h:R => h <> 0) l1 l2 0 H1 H2).
538
unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
539
simpl in |- *; unfold R_dist in |- *; intros.
540
elim (H4 eps H5); intros.
545
intros; rewrite H3; apply H8; assumption.
546
intro; unfold Rdiv in |- *; ring.
549
Lemma derivable_pt_lim_opp :
550
forall f (x l:R), derivable_pt_lim f x l -> derivable_pt_lim (- f) x (- l).
553
apply uniqueness_step3.
554
assert (H1 := uniqueness_step2 _ _ _ H).
555
unfold opp_fct in |- *.
556
cut (forall h:R, (- f (x + h) - - f x) / h = - ((f (x + h) - f x) / h)).
559
(limit_Ropp (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0 H1).
560
unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
561
simpl in |- *; unfold R_dist in |- *; intros.
562
elim (H2 eps H3); intros.
567
intros; rewrite H0; apply H6; assumption.
568
intro; unfold Rdiv in |- *; ring.
571
Lemma derivable_pt_lim_minus :
572
forall f1 f2 (x l1 l2:R),
573
derivable_pt_lim f1 x l1 ->
574
derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 - f2) x (l1 - l2).
577
apply uniqueness_step3.
578
assert (H1 := uniqueness_step2 _ _ _ H).
579
assert (H2 := uniqueness_step2 _ _ _ H0).
580
unfold minus_fct in |- *.
583
(f1 (x + h) - f1 x) / h - (f2 (x + h) - f2 x) / h =
584
(f1 (x + h) - f2 (x + h) - (f1 x - f2 x)) / h).
587
(limit_minus (fun h':R => (f1 (x + h') - f1 x) / h')
588
(fun h':R => (f2 (x + h') - f2 x) / h') (fun h:R => h <> 0) l1 l2 0 H1 H2).
589
unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
590
simpl in |- *; unfold R_dist in |- *; intros.
591
elim (H4 eps H5); intros.
596
intros; rewrite <- H3; apply H8; assumption.
597
intro; unfold Rdiv in |- *; ring.
600
Lemma derivable_pt_lim_mult :
601
forall f1 f2 (x l1 l2:R),
602
derivable_pt_lim f1 x l1 ->
603
derivable_pt_lim f2 x l2 ->
604
derivable_pt_lim (f1 * f2) x (l1 * f2 x + f1 x * l2).
607
assert (H1 := derivable_pt_lim_D_in f1 (fun y:R => l1) x).
610
assert (H5 := derivable_pt_lim_D_in f2 (fun y:R => l2) x).
612
assert (H8 := H7 H0).
613
clear H1 H2 H3 H5 H6 H7.
616
derivable_pt_lim_D_in (f1 * f2)%F (fun y:R => l1 * f2 x + f1 x * l2) x).
620
unfold mult_fct in |- *.
621
apply (Dmult no_cond (fun y:R => l1) (fun y:R => l2) f1 f2 x); assumption.
624
Lemma derivable_pt_lim_const : forall a x:R, derivable_pt_lim (fct_cte a) x 0.
626
intros; unfold fct_cte, derivable_pt_lim in |- *.
627
intros; exists (mkposreal 1 Rlt_0_1); intros; unfold Rminus in |- *;
628
rewrite Rplus_opp_r; unfold Rdiv in |- *; rewrite Rmult_0_l;
629
rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
632
Lemma derivable_pt_lim_scal :
634
derivable_pt_lim f x l -> derivable_pt_lim (mult_real_fct a f) x (a * l).
637
assert (H0 := derivable_pt_lim_const a x).
638
replace (mult_real_fct a f) with (fct_cte a * f)%F.
639
replace (a * l) with (0 * f x + a * l); [ idtac | ring ].
640
apply (derivable_pt_lim_mult (fct_cte a) f x 0 l); assumption.
641
unfold mult_real_fct, mult_fct, fct_cte in |- *; reflexivity.
644
Lemma derivable_pt_lim_id : forall x:R, derivable_pt_lim id x 1.
646
intro; unfold derivable_pt_lim in |- *.
647
intros eps Heps; exists (mkposreal eps Heps); intros h H1 H2;
648
unfold id in |- *; replace ((x + h - x) / h - 1) with 0.
649
rewrite Rabs_R0; apply Rle_lt_trans with (Rabs h).
652
unfold Rminus in |- *; rewrite Rplus_assoc; rewrite (Rplus_comm x);
654
rewrite Rplus_opp_l; rewrite Rplus_0_r; unfold Rdiv in |- *;
655
rewrite <- Rinv_r_sym.
656
symmetry in |- *; apply Rplus_opp_r.
660
Lemma derivable_pt_lim_Rsqr : forall x:R, derivable_pt_lim Rsqr x (2 * x).
662
intro; unfold derivable_pt_lim in |- *.
663
unfold Rsqr in |- *; intros eps Heps; exists (mkposreal eps Heps);
664
intros h H1 H2; replace (((x + h) * (x + h) - x * x) / h - 2 * x) with h.
666
replace ((x + h) * (x + h) - x * x) with (2 * x * h + h * h);
668
unfold Rdiv in |- *; rewrite Rmult_plus_distr_r.
669
repeat rewrite Rmult_assoc.
670
repeat rewrite <- Rinv_r_sym; [ idtac | assumption ].
674
Lemma derivable_pt_lim_comp :
675
forall f1 f2 (x l1 l2:R),
676
derivable_pt_lim f1 x l1 ->
677
derivable_pt_lim f2 (f1 x) l2 -> derivable_pt_lim (f2 o f1) x (l2 * l1).
679
intros; assert (H1 := derivable_pt_lim_D_in f1 (fun y:R => l1) x).
682
assert (H5 := derivable_pt_lim_D_in f2 (fun y:R => l2) (f1 x)).
684
assert (H8 := H7 H0).
685
clear H1 H2 H3 H5 H6 H7.
686
assert (H1 := derivable_pt_lim_D_in (f2 o f1)%F (fun y:R => l2 * l1) x).
688
clear H1 H3; apply H2.
691
(D_in (fun x0:R => f2 (f1 x0)) (fun y:R => l2 * l1)
692
(Dgf no_cond no_cond f1) x ->
693
D_in (fun x0:R => f2 (f1 x0)) (fun y:R => l2 * l1) no_cond x).
696
apply (Dcomp no_cond no_cond (fun y:R => l1) (fun y:R => l2) f1 f2 x);
698
unfold Dgf, D_in, no_cond in |- *; unfold limit1_in in |- *;
699
unfold limit_in in |- *; unfold dist in |- *; simpl in |- *;
700
unfold R_dist in |- *; intros.
701
elim (H1 eps H3); intros.
702
exists x0; intros; split.
703
elim H5; intros; assumption.
704
intros; elim H5; intros; apply H9; split.
705
unfold D_x in |- *; split.
707
elim H6; intros; unfold D_x in H10; elim H10; intros; assumption.
708
elim H6; intros; assumption.
711
Lemma derivable_pt_plus :
713
derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 + f2) x.
715
unfold derivable_pt in |- *; intros f1 f2 x X X0.
719
apply derivable_pt_lim_plus; assumption.
722
Lemma derivable_pt_opp :
723
forall f (x:R), derivable_pt f x -> derivable_pt (- f) x.
725
unfold derivable_pt in |- *; intros f x X.
728
apply derivable_pt_lim_opp; assumption.
731
Lemma derivable_pt_minus :
733
derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 - f2) x.
735
unfold derivable_pt in |- *; intros f1 f2 x X X0.
739
apply derivable_pt_lim_minus; assumption.
742
Lemma derivable_pt_mult :
744
derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 * f2) x.
746
unfold derivable_pt in |- *; intros f1 f2 x X X0.
749
exists (x0 * f2 x + f1 x * x1).
750
apply derivable_pt_lim_mult; assumption.
753
Lemma derivable_pt_const : forall a x:R, derivable_pt (fct_cte a) x.
755
intros; unfold derivable_pt in |- *.
757
apply derivable_pt_lim_const.
760
Lemma derivable_pt_scal :
761
forall f (a x:R), derivable_pt f x -> derivable_pt (mult_real_fct a f) x.
763
unfold derivable_pt in |- *; intros f1 a x X.
766
apply derivable_pt_lim_scal; assumption.
769
Lemma derivable_pt_id : forall x:R, derivable_pt id x.
771
unfold derivable_pt in |- *; intro.
773
apply derivable_pt_lim_id.
776
Lemma derivable_pt_Rsqr : forall x:R, derivable_pt Rsqr x.
778
unfold derivable_pt in |- *; intro; exists (2 * x).
779
apply derivable_pt_lim_Rsqr.
782
Lemma derivable_pt_comp :
784
derivable_pt f1 x -> derivable_pt f2 (f1 x) -> derivable_pt (f2 o f1) x.
786
unfold derivable_pt in |- *; intros f1 f2 x X X0.
790
apply derivable_pt_lim_comp; assumption.
793
Lemma derivable_plus :
794
forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 + f2).
796
unfold derivable in |- *; intros f1 f2 X X0 x.
797
apply (derivable_pt_plus _ _ x (X _) (X0 _)).
800
Lemma derivable_opp : forall f, derivable f -> derivable (- f).
802
unfold derivable in |- *; intros f X x.
803
apply (derivable_pt_opp _ x (X _)).
806
Lemma derivable_minus :
807
forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 - f2).
809
unfold derivable in |- *; intros f1 f2 X X0 x.
810
apply (derivable_pt_minus _ _ x (X _) (X0 _)).
813
Lemma derivable_mult :
814
forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 * f2).
816
unfold derivable in |- *; intros f1 f2 X X0 x.
817
apply (derivable_pt_mult _ _ x (X _) (X0 _)).
820
Lemma derivable_const : forall a:R, derivable (fct_cte a).
822
unfold derivable in |- *; intros.
823
apply derivable_pt_const.
826
Lemma derivable_scal :
827
forall f (a:R), derivable f -> derivable (mult_real_fct a f).
829
unfold derivable in |- *; intros f a X x.
830
apply (derivable_pt_scal _ a x (X _)).
833
Lemma derivable_id : derivable id.
835
unfold derivable in |- *; intro; apply derivable_pt_id.
838
Lemma derivable_Rsqr : derivable Rsqr.
840
unfold derivable in |- *; intro; apply derivable_pt_Rsqr.
843
Lemma derivable_comp :
844
forall f1 f2, derivable f1 -> derivable f2 -> derivable (f2 o f1).
846
unfold derivable in |- *; intros f1 f2 X X0 x.
847
apply (derivable_pt_comp _ _ x (X _) (X0 _)).
850
Lemma derive_pt_plus :
851
forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
852
derive_pt (f1 + f2) x (derivable_pt_plus _ _ _ pr1 pr2) =
853
derive_pt f1 x pr1 + derive_pt f2 x pr2.
856
assert (H := derivable_derive f1 x pr1).
857
assert (H0 := derivable_derive f2 x pr2).
859
(H1 := derivable_derive (f1 + f2)%F x (derivable_pt_plus _ _ _ pr1 pr2)).
860
elim H; clear H; intros l1 H.
861
elim H0; clear H0; intros l2 H0.
862
elim H1; clear H1; intros l H1.
863
rewrite H; rewrite H0; apply derive_pt_eq_0.
864
assert (H3 := proj2_sig pr1).
865
unfold derive_pt in H; rewrite H in H3.
866
assert (H4 := proj2_sig pr2).
867
unfold derive_pt in H0; rewrite H0 in H4.
868
apply derivable_pt_lim_plus; assumption.
871
Lemma derive_pt_opp :
872
forall f (x:R) (pr1:derivable_pt f x),
873
derive_pt (- f) x (derivable_pt_opp _ _ pr1) = - derive_pt f x pr1.
876
assert (H := derivable_derive f x pr1).
877
assert (H0 := derivable_derive (- f)%F x (derivable_pt_opp _ _ pr1)).
878
elim H; clear H; intros l1 H.
879
elim H0; clear H0; intros l2 H0.
880
rewrite H; apply derive_pt_eq_0.
881
assert (H3 := proj2_sig pr1).
882
unfold derive_pt in H; rewrite H in H3.
883
apply derivable_pt_lim_opp; assumption.
886
Lemma derive_pt_minus :
887
forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
888
derive_pt (f1 - f2) x (derivable_pt_minus _ _ _ pr1 pr2) =
889
derive_pt f1 x pr1 - derive_pt f2 x pr2.
892
assert (H := derivable_derive f1 x pr1).
893
assert (H0 := derivable_derive f2 x pr2).
895
(H1 := derivable_derive (f1 - f2)%F x (derivable_pt_minus _ _ _ pr1 pr2)).
896
elim H; clear H; intros l1 H.
897
elim H0; clear H0; intros l2 H0.
898
elim H1; clear H1; intros l H1.
899
rewrite H; rewrite H0; apply derive_pt_eq_0.
900
assert (H3 := proj2_sig pr1).
901
unfold derive_pt in H; rewrite H in H3.
902
assert (H4 := proj2_sig pr2).
903
unfold derive_pt in H0; rewrite H0 in H4.
904
apply derivable_pt_lim_minus; assumption.
907
Lemma derive_pt_mult :
908
forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
909
derive_pt (f1 * f2) x (derivable_pt_mult _ _ _ pr1 pr2) =
910
derive_pt f1 x pr1 * f2 x + f1 x * derive_pt f2 x pr2.
913
assert (H := derivable_derive f1 x pr1).
914
assert (H0 := derivable_derive f2 x pr2).
916
(H1 := derivable_derive (f1 * f2)%F x (derivable_pt_mult _ _ _ pr1 pr2)).
917
elim H; clear H; intros l1 H.
918
elim H0; clear H0; intros l2 H0.
919
elim H1; clear H1; intros l H1.
920
rewrite H; rewrite H0; apply derive_pt_eq_0.
921
assert (H3 := proj2_sig pr1).
922
unfold derive_pt in H; rewrite H in H3.
923
assert (H4 := proj2_sig pr2).
924
unfold derive_pt in H0; rewrite H0 in H4.
925
apply derivable_pt_lim_mult; assumption.
928
Lemma derive_pt_const :
929
forall a x:R, derive_pt (fct_cte a) x (derivable_pt_const a x) = 0.
932
apply derive_pt_eq_0.
933
apply derivable_pt_lim_const.
936
Lemma derive_pt_scal :
937
forall f (a x:R) (pr:derivable_pt f x),
938
derive_pt (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr) =
939
a * derive_pt f x pr.
942
assert (H := derivable_derive f x pr).
944
(H0 := derivable_derive (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr)).
945
elim H; clear H; intros l1 H.
946
elim H0; clear H0; intros l2 H0.
947
rewrite H; apply derive_pt_eq_0.
948
assert (H3 := proj2_sig pr).
949
unfold derive_pt in H; rewrite H in H3.
950
apply derivable_pt_lim_scal; assumption.
953
Lemma derive_pt_id : forall x:R, derive_pt id x (derivable_pt_id _) = 1.
956
apply derive_pt_eq_0.
957
apply derivable_pt_lim_id.
960
Lemma derive_pt_Rsqr :
961
forall x:R, derive_pt Rsqr x (derivable_pt_Rsqr _) = 2 * x.
964
apply derive_pt_eq_0.
965
apply derivable_pt_lim_Rsqr.
968
Lemma derive_pt_comp :
969
forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 (f1 x)),
970
derive_pt (f2 o f1) x (derivable_pt_comp _ _ _ pr1 pr2) =
971
derive_pt f2 (f1 x) pr2 * derive_pt f1 x pr1.
974
assert (H := derivable_derive f1 x pr1).
975
assert (H0 := derivable_derive f2 (f1 x) pr2).
977
(H1 := derivable_derive (f2 o f1)%F x (derivable_pt_comp _ _ _ pr1 pr2)).
978
elim H; clear H; intros l1 H.
979
elim H0; clear H0; intros l2 H0.
980
elim H1; clear H1; intros l H1.
981
rewrite H; rewrite H0; apply derive_pt_eq_0.
982
assert (H3 := proj2_sig pr1).
983
unfold derive_pt in H; rewrite H in H3.
984
assert (H4 := proj2_sig pr2).
985
unfold derive_pt in H0; rewrite H0 in H4.
986
apply derivable_pt_lim_comp; assumption.
990
Definition pow_fct (n:nat) (y:R) : R := y ^ n.
992
Lemma derivable_pt_lim_pow_pos :
993
forall (x:R) (n:nat),
994
(0 < n)%nat -> derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).
997
induction n as [| n Hrecn].
998
elim (lt_irrefl _ H).
999
cut (n = 0%nat \/ (0 < n)%nat).
1000
intro; elim H0; intro.
1001
rewrite H1; simpl in |- *.
1002
replace (fun y:R => y * 1) with (id * fct_cte 1)%F.
1003
replace (1 * 1) with (1 * fct_cte 1 x + id x * 0).
1004
apply derivable_pt_lim_mult.
1005
apply derivable_pt_lim_id.
1006
apply derivable_pt_lim_const.
1007
unfold fct_cte, id in |- *; ring.
1009
replace (fun y:R => y ^ S n) with (fun y:R => y * y ^ n).
1010
replace (pred (S n)) with n; [ idtac | reflexivity ].
1011
replace (fun y:R => y * y ^ n) with (id * (fun y:R => y ^ n))%F.
1012
set (f := fun y:R => y ^ n).
1013
replace (INR (S n) * x ^ n) with (1 * f x + id x * (INR n * x ^ pred n)).
1014
apply derivable_pt_lim_mult.
1015
apply derivable_pt_lim_id.
1016
unfold f in |- *; apply Hrecn; assumption.
1018
pattern n at 1 5 in |- *; replace n with (S (pred n)).
1019
unfold id in |- *; rewrite S_INR; simpl in |- *.
1021
symmetry in |- *; apply S_pred with 0%nat; assumption.
1022
unfold mult_fct, id in |- *; reflexivity.
1027
apply lt_le_trans with 1%nat.
1032
Lemma derivable_pt_lim_pow :
1033
forall (x:R) (n:nat),
1034
derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).
1037
induction n as [| n Hrecn].
1040
replace (fun _:R => 1) with (fct_cte 1);
1041
[ apply derivable_pt_lim_const | reflexivity ].
1042
apply derivable_pt_lim_pow_pos.
1046
Lemma derivable_pt_pow :
1047
forall (n:nat) (x:R), derivable_pt (fun y:R => y ^ n) x.
1049
intros; unfold derivable_pt in |- *.
1050
exists (INR n * x ^ pred n).
1051
apply derivable_pt_lim_pow.
1054
Lemma derivable_pow : forall n:nat, derivable (fun y:R => y ^ n).
1056
intro; unfold derivable in |- *; intro; apply derivable_pt_pow.
1059
Lemma derive_pt_pow :
1060
forall (n:nat) (x:R),
1061
derive_pt (fun y:R => y ^ n) x (derivable_pt_pow n x) = INR n * x ^ pred n.
1063
intros; apply derive_pt_eq_0.
1064
apply derivable_pt_lim_pow.
1068
forall f (x:R) (pr1 pr2:derivable_pt f x),
1069
derive_pt f x pr1 = derive_pt f x pr2.
1072
unfold derivable_pt in pr1.
1073
unfold derivable_pt in pr2.
1076
unfold derivable_pt_abs in p.
1077
unfold derivable_pt_abs in p0.
1079
apply (uniqueness_limite f x x0 x1 p p0).
1083
(************************************************************)
1084
(** * Local extremum's condition *)
1085
(************************************************************)
1087
Theorem deriv_maximum :
1088
forall f (a b c:R) (pr:derivable_pt f c),
1091
(forall x:R, a < x -> x < b -> f x <= f c) -> derive_pt f c pr = 0.
1093
intros; case (Rtotal_order 0 (derive_pt f c pr)); intro.
1094
assert (H3 := derivable_derive f c pr).
1095
elim H3; intros l H4; rewrite H4 in H2.
1096
assert (H5 := derive_pt_eq_1 f c l pr H4).
1099
| unfold Rdiv in |- *; apply Rmult_lt_0_compat;
1100
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
1101
elim (H5 (l / 2) H6); intros delta H7.
1102
cut (0 < (b - c) / 2).
1103
intro; cut (Rmin (delta / 2) ((b - c) / 2) <> 0).
1104
intro; cut (Rabs (Rmin (delta / 2) ((b - c) / 2)) < delta).
1106
assert (H11 := H7 (Rmin (delta / 2) ((b - c) / 2)) H9 H10).
1107
cut (0 < Rmin (delta / 2) ((b - c) / 2)).
1108
intro; cut (a < c + Rmin (delta / 2) ((b - c) / 2)).
1109
intro; cut (c + Rmin (delta / 2) ((b - c) / 2) < b).
1110
intro; assert (H15 := H1 (c + Rmin (delta / 2) ((b - c) / 2)) H13 H14).
1112
((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) /
1113
Rmin (delta / 2) ((b - c) / 2) <= 0).
1114
intro; cut (- l < 0).
1115
intro; unfold Rminus in H11.
1117
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1118
Rmin (delta / 2) ((b + - c) / 2) + - l < 0).
1122
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1123
Rmin (delta / 2) ((b + - c) / 2) + - l) < l / 2).
1124
unfold Rabs in |- *;
1127
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1128
Rmin (delta / 2) ((b + - c) / 2) + - l)); intro.
1131
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1132
Rmin (delta / 2) ((b + - c) / 2) + - l)) with
1135
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1136
Rmin (delta / 2) ((b + - c) / 2))).
1139
(Rplus_lt_compat_l (- l)
1142
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1143
Rmin (delta / 2) ((b + - c) / 2))) (l / 2) H19);
1144
repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
1145
rewrite Rplus_0_l; replace (- l + l / 2) with (- (l / 2)).
1148
(Ropp_lt_gt_contravar
1150
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1151
Rmin (delta / 2) ((b + - c) / 2))) (- (l / 2)) H20);
1152
repeat rewrite Ropp_involutive; intro;
1154
(Rlt_trans 0 (l / 2)
1155
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1156
Rmin (delta / 2) ((b + - c) / 2)) H6 H21); intro;
1160
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1161
Rmin (delta / 2) ((b + - c) / 2)) 0 H22 H16)).
1162
pattern l at 2 in |- *; rewrite double_var.
1169
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1170
Rmin (delta / 2) ((b + - c) / 2) + - l) 0 r).
1171
elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H20 H18)).
1175
((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
1176
Rmin (delta / 2) ((b + - c) / 2) + - l) with
1180
((f (c + Rmin (delta / 2) ((b + - c) / 2)) - f c) /
1181
Rmin (delta / 2) ((b + - c) / 2)))).
1182
apply Ropp_gt_lt_contravar;
1187
((f (c + Rmin (delta / 2) ((b + - c) / 2)) - f c) /
1188
Rmin (delta / 2) ((b + - c) / 2))) in |- *; apply Rplus_lt_le_0_compat;
1190
| rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption ].
1191
unfold Rminus; ring.
1192
rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
1194
((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) /
1195
Rmin (delta / 2) ((b - c) / 2)) with
1197
((f c - f (c + Rmin (delta / 2) ((b - c) / 2))) /
1198
Rmin (delta / 2) ((b - c) / 2))).
1199
rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge;
1200
unfold Rdiv in |- *; apply Rmult_le_pos;
1202
(Rplus_le_compat_r (- f (c + Rmin (delta * / 2) ((b - c) * / 2)))
1203
(f (c + Rmin (delta * / 2) ((b - c) * / 2))) (
1204
f c) H15); rewrite Rplus_opp_r; intro; assumption
1205
| left; apply Rinv_0_lt_compat; assumption ].
1206
unfold Rdiv in |- *.
1207
rewrite <- Ropp_mult_distr_l_reverse.
1208
repeat rewrite <- (Rmult_comm (/ Rmin (delta * / 2) ((b - c) * / 2))).
1209
apply Rmult_eq_reg_l with (Rmin (delta * / 2) ((b - c) * / 2)).
1210
repeat rewrite <- Rmult_assoc.
1211
rewrite <- Rinv_r_sym.
1212
repeat rewrite Rmult_1_l.
1215
unfold Rdiv in H12; rewrite H16 in H12; elim (Rlt_irrefl 0 H12).
1217
unfold Rdiv in H12; rewrite H16 in H12; elim (Rlt_irrefl 0 H12).
1218
assert (H14 := Rmin_r (delta / 2) ((b - c) / 2)).
1221
Rplus_le_compat_l c (Rmin (delta / 2) ((b - c) / 2)) ((b - c) / 2) H14).
1222
apply Rle_lt_trans with (c + (b - c) / 2).
1224
apply Rmult_lt_reg_l with 2.
1226
replace (2 * (c + (b - c) / 2)) with (c + b).
1227
replace (2 * b) with (b + b).
1228
apply Rplus_lt_compat_r; assumption.
1230
unfold Rdiv in |- *; rewrite Rmult_plus_distr_l.
1231
repeat rewrite (Rmult_comm 2).
1232
rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
1236
apply Rlt_trans with c.
1238
pattern c at 1 in |- *; rewrite <- (Rplus_0_r c); apply Rplus_lt_compat_l;
1240
cut (0 < delta / 2).
1243
(Rmin_stable_in_posreal (mkposreal (delta / 2) H12)
1244
(mkposreal ((b - c) / 2) H8)).
1245
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
1246
[ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
1247
unfold Rabs in |- *; case (Rcase_abs (Rmin (delta / 2) ((b - c) / 2))).
1249
cut (0 < delta / 2).
1252
(Rmin_stable_in_posreal (mkposreal (delta / 2) H10)
1253
(mkposreal ((b - c) / 2) H8)); simpl in |- *; intro;
1254
elim (Rlt_irrefl 0 (Rlt_trans 0 (Rmin (delta / 2) ((b - c) / 2)) 0 H11 r)).
1255
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
1256
[ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
1257
intro; apply Rle_lt_trans with (delta / 2).
1259
unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2.
1261
rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
1263
replace (2 * delta) with (delta + delta).
1264
pattern delta at 2 in |- *; rewrite <- (Rplus_0_r delta);
1265
apply Rplus_lt_compat_l.
1266
rewrite Rplus_0_r; apply (cond_pos delta).
1267
symmetry in |- *; apply double.
1269
cut (0 < delta / 2).
1272
(Rmin_stable_in_posreal (mkposreal (delta / 2) H9)
1273
(mkposreal ((b - c) / 2) H8)); simpl in |- *;
1274
intro; red in |- *; intro; rewrite H11 in H10; elim (Rlt_irrefl 0 H10).
1275
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
1276
[ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
1277
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
1278
generalize (Rplus_lt_compat_r (- c) c b H0); rewrite Rplus_opp_r; intro;
1280
apply Rinv_0_lt_compat; prove_sup0.
1282
symmetry in |- *; assumption.
1283
generalize (derivable_derive f c pr); intro; elim H4; intros l H5.
1284
rewrite H5 in H3; generalize (derive_pt_eq_1 f c l pr H5); intro;
1285
cut (0 < - (l / 2)).
1286
intro; elim (H6 (- (l / 2)) H7); intros delta H9.
1287
cut (0 < (c - a) / 2).
1288
intro; cut (Rmax (- (delta / 2)) ((a - c) / 2) < 0).
1289
intro; cut (Rmax (- (delta / 2)) ((a - c) / 2) <> 0).
1290
intro; cut (Rabs (Rmax (- (delta / 2)) ((a - c) / 2)) < delta).
1291
intro; generalize (H9 (Rmax (- (delta / 2)) ((a - c) / 2)) H11 H12); intro;
1292
cut (a < c + Rmax (- (delta / 2)) ((a - c) / 2)).
1293
cut (c + Rmax (- (delta / 2)) ((a - c) / 2) < b).
1294
intros; generalize (H1 (c + Rmax (- (delta / 2)) ((a - c) / 2)) H15 H14);
1298
(f (c + Rmax (- (delta / 2)) ((a - c) / 2)) - f c) /
1299
Rmax (- (delta / 2)) ((a - c) / 2)).
1300
intro; cut (0 < - l).
1301
intro; unfold Rminus in H13;
1304
(f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
1305
Rmax (- (delta / 2)) ((a + - c) / 2) + - l).
1309
((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
1310
Rmax (- (delta / 2)) ((a + - c) / 2) + - l) <
1312
unfold Rabs in |- *;
1315
((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
1316
Rmax (- (delta / 2)) ((a + - c) / 2) + - l)).
1321
((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
1322
Rmax (- (delta / 2)) ((a + - c) / 2) + - l) 0 H19 r)).
1325
(Rplus_lt_compat_r l
1326
((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
1327
Rmax (- (delta / 2)) ((a + - c) / 2) + - l) (
1328
- (l / 2)) H20); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l;
1329
rewrite Rplus_0_r; replace (- (l / 2) + l) with (l / 2).
1334
((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
1335
Rmax (- (delta / 2)) ((a + - c) / 2)) (l / 2) 0 H22 H21);
1340
((f (c + Rmax (- (delta / 2)) ((a - c) / 2)) - f c) /
1341
Rmax (- (delta / 2)) ((a - c) / 2)) 0 H17 H23)).
1342
rewrite <- (Ropp_involutive (l / 2)); rewrite <- Ropp_0;
1343
apply Ropp_lt_gt_contravar; assumption.
1344
pattern l at 3 in |- *; rewrite double_var.
1347
apply Rplus_le_lt_0_compat; assumption.
1348
rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
1349
unfold Rdiv in |- *;
1351
((f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c) *
1352
/ Rmax (- (delta * / 2)) ((a - c) * / 2)) with
1353
(- (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c) *
1354
/ - Rmax (- (delta * / 2)) ((a - c) * / 2)).
1357
(Rplus_le_compat_l (- f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)))
1358
(f (c + Rmax (- (delta * / 2)) ((a - c) * / 2))) (
1359
f c) H16); rewrite Rplus_opp_l;
1360
replace (- (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c)) with
1361
(- f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) + f c).
1364
left; apply Rinv_0_lt_compat; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar;
1366
unfold Rdiv in |- *.
1367
rewrite <- Ropp_inv_permute.
1368
rewrite Rmult_opp_opp.
1370
unfold Rdiv in H11; assumption.
1371
generalize (Rplus_lt_compat_l c (Rmax (- (delta / 2)) ((a - c) / 2)) 0 H10);
1372
rewrite Rplus_0_r; intro; apply Rlt_trans with c;
1374
generalize (RmaxLess2 (- (delta / 2)) ((a - c) / 2)); intro;
1376
(Rplus_le_compat_l c ((a - c) / 2) (Rmax (- (delta / 2)) ((a - c) / 2)) H14);
1377
intro; apply Rlt_le_trans with (c + (a - c) / 2).
1378
apply Rmult_lt_reg_l with 2.
1380
replace (2 * (c + (a - c) / 2)) with (a + c).
1382
apply Rplus_lt_compat_l; assumption.
1385
unfold Rabs in |- *; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))).
1386
intro; generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro;
1388
(Ropp_le_ge_contravar (- (delta / 2)) (Rmax (- (delta / 2)) ((a - c) / 2))
1389
H12); rewrite Ropp_involutive; intro;
1390
generalize (Rge_le (delta / 2) (- Rmax (- (delta / 2)) ((a - c) / 2)) H13);
1391
intro; apply Rle_lt_trans with (delta / 2).
1393
apply Rmult_lt_reg_l with 2.
1395
unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
1396
rewrite <- Rinv_r_sym.
1397
rewrite Rmult_1_l; rewrite double.
1398
pattern delta at 2 in |- *; rewrite <- (Rplus_0_r delta);
1399
apply Rplus_lt_compat_l; rewrite Rplus_0_r; apply (cond_pos delta).
1401
cut (- (delta / 2) < 0).
1402
cut ((a - c) / 2 < 0).
1405
(Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H13)
1406
(mknegreal ((a - c) / 2) H12)); simpl in |- *;
1407
intro; generalize (Rge_le (Rmax (- (delta / 2)) ((a - c) / 2)) 0 r);
1411
(Rle_lt_trans 0 (Rmax (- (delta / 2)) ((a - c) / 2)) 0 H15 H14)).
1412
rewrite <- Ropp_0; rewrite <- (Ropp_involutive ((a - c) / 2));
1413
apply Ropp_lt_gt_contravar; replace (- ((a - c) / 2)) with ((c - a) / 2).
1415
unfold Rdiv in |- *.
1416
rewrite <- Ropp_mult_distr_l_reverse.
1417
rewrite (Ropp_minus_distr a c).
1419
rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold Rdiv in |- *;
1420
apply Rmult_lt_0_compat;
1421
[ apply (cond_pos delta)
1422
| assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ].
1423
red in |- *; intro; rewrite H11 in H10; elim (Rlt_irrefl 0 H10).
1424
cut ((a - c) / 2 < 0).
1425
intro; cut (- (delta / 2) < 0).
1428
(Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H11)
1429
(mknegreal ((a - c) / 2) H10)).
1430
rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold Rdiv in |- *;
1431
apply Rmult_lt_0_compat;
1432
[ apply (cond_pos delta)
1433
| assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ].
1434
rewrite <- Ropp_0; rewrite <- (Ropp_involutive ((a - c) / 2));
1435
apply Ropp_lt_gt_contravar; replace (- ((a - c) / 2)) with ((c - a) / 2).
1437
unfold Rdiv in |- *.
1438
rewrite <- Ropp_mult_distr_l_reverse.
1439
rewrite (Ropp_minus_distr a c).
1441
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
1442
[ generalize (Rplus_lt_compat_r (- a) a c H); rewrite Rplus_opp_r; intro;
1444
| assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ].
1445
replace (- (l / 2)) with (- l / 2).
1446
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
1447
rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
1448
assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ].
1449
unfold Rdiv in |- *; apply Ropp_mult_distr_l_reverse.
1452
Theorem deriv_minimum :
1453
forall f (a b c:R) (pr:derivable_pt f c),
1456
(forall x:R, a < x -> x < b -> f c <= f x) -> derive_pt f c pr = 0.
1459
rewrite <- (Ropp_involutive (derive_pt f c pr)).
1460
apply Ropp_eq_0_compat.
1461
rewrite <- (derive_pt_opp f c pr).
1462
cut (forall x:R, a < x -> x < b -> (- f)%F x <= (- f)%F c).
1464
apply (deriv_maximum (- f)%F a b c (derivable_pt_opp _ _ pr) H H0 H2).
1465
intros; unfold opp_fct in |- *; apply Ropp_ge_le_contravar; apply Rle_ge.
1469
Theorem deriv_constant2 :
1470
forall f (a b c:R) (pr:derivable_pt f c),
1472
c < b -> (forall x:R, a < x -> x < b -> f x = f c) -> derive_pt f c pr = 0.
1475
eapply deriv_maximum with a b; try assumption.
1476
intros; right; apply (H1 x H2 H3).
1480
Lemma nonneg_derivative_0 :
1481
forall f (pr:derivable f),
1482
increasing f -> forall x:R, 0 <= derive_pt f x (pr x).
1484
intros; unfold increasing in H.
1485
assert (H0 := derivable_derive f x (pr x)).
1486
elim H0; intros l H1.
1487
rewrite H1; case (Rtotal_order 0 l); intro.
1491
assert (H4 := derive_pt_eq_1 f x l (pr x) H1).
1492
cut (0 < - (l / 2)).
1493
intro; elim (H4 (- (l / 2)) H5); intros delta H6.
1494
cut (delta / 2 <> 0 /\ 0 < delta / 2 /\ Rabs (delta / 2) < delta).
1495
intro; decompose [and] H7; intros; generalize (H6 (delta / 2) H8 H11);
1496
cut (0 <= (f (x + delta / 2) - f x) / (delta / 2)).
1497
intro; cut (0 <= (f (x + delta / 2) - f x) / (delta / 2) - l).
1498
intro; unfold Rabs in |- *;
1499
case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)).
1503
(Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 H12 r)).
1506
(Rplus_lt_compat_r l ((f (x + delta / 2) - f x) / (delta / 2) - l)
1507
(- (l / 2)) H13); unfold Rminus in |- *;
1508
replace (- (l / 2) + l) with (l / 2).
1509
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro;
1511
(Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2)) (l / 2) H9 H14);
1512
intro; cut (l / 2 < 0).
1513
intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (l / 2) 0 H15 H16)).
1514
rewrite <- Ropp_0 in H5;
1515
generalize (Ropp_lt_gt_contravar (-0) (- (l / 2)) H5);
1516
repeat rewrite Ropp_involutive; intro; assumption.
1517
pattern l at 3 in |- *; rewrite double_var.
1519
unfold Rminus in |- *; apply Rplus_le_le_0_compat.
1520
unfold Rdiv in |- *; apply Rmult_le_pos.
1521
cut (x <= x + delta * / 2).
1522
intro; generalize (H x (x + delta * / 2) H12); intro;
1523
generalize (Rplus_le_compat_l (- f x) (f x) (f (x + delta * / 2)) H13);
1524
rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption.
1525
pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
1527
left; apply Rinv_0_lt_compat; assumption.
1528
left; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
1529
unfold Rdiv in |- *; apply Rmult_le_pos.
1530
cut (x <= x + delta * / 2).
1531
intro; generalize (H x (x + delta * / 2) H9); intro;
1532
generalize (Rplus_le_compat_l (- f x) (f x) (f (x + delta * / 2)) H12);
1533
rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption.
1534
pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
1536
left; apply Rinv_0_lt_compat; assumption.
1538
unfold Rdiv in |- *; apply prod_neq_R0.
1539
generalize (cond_pos delta); intro; red in |- *; intro H9; rewrite H9 in H7;
1540
elim (Rlt_irrefl 0 H7).
1541
apply Rinv_neq_0_compat; discrR.
1543
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
1544
[ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
1545
replace (Rabs (delta / 2)) with (delta / 2).
1546
unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2.
1548
rewrite (Rmult_comm 2).
1549
rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
1552
pattern (pos delta) at 1 in |- *; rewrite <- Rplus_0_r.
1553
apply Rplus_lt_compat_l; apply (cond_pos delta).
1554
symmetry in |- *; apply Rabs_right.
1555
left; change (0 < delta / 2) in |- *; unfold Rdiv in |- *;
1556
apply Rmult_lt_0_compat;
1557
[ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
1558
unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse;
1559
apply Rmult_lt_0_compat.
1560
apply Rplus_lt_reg_r with l.
1561
unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption.
1562
apply Rinv_0_lt_compat; prove_sup0.
added
removed
theories/Reals/Ranalysis1.v
