← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Rderiv.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/Rderiv.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: Rderiv.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
(*********************************************************)
 
12
(**     Definition of the derivative,continuity          *)
 
13
(*                                                       *)
 
14
(*********************************************************)
 
15
 
 
16
Require Import Rbase.
 
17
Require Import Rfunctions.
 
18
Require Import Rlimit.
 
19
Require Import Fourier.
 
20
Require Import Classical_Prop.
 
21
Require Import Classical_Pred_Type.
 
22
Require Import Omega.
 
23
Open Local Scope R_scope.
 
24
 
 
25
(*********)
 
26
Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x.
 
27
 
 
28
(*********)
 
29
Definition continue_in (f:R -> R) (D:R -> Prop) (x0:R) : Prop :=
 
30
  limit1_in f (D_x D x0) (f x0) x0.
 
31
 
 
32
(*********)
 
33
Definition D_in (f d:R -> R) (D:R -> Prop) (x0:R) : Prop :=
 
34
  limit1_in (fun x:R => (f x - f x0) / (x - x0)) (D_x D x0) (d x0) x0.
 
35
 
 
36
(*********)
 
37
Lemma cont_deriv :
 
38
  forall (f d:R -> R) (D:R -> Prop) (x0:R),
 
39
    D_in f d D x0 -> continue_in f D x0.
 
40
Proof.
 
41
  unfold continue_in in |- *; unfold D_in in |- *; unfold limit1_in in |- *;
 
42
    unfold limit_in in |- *; unfold Rdiv in |- *; simpl in |- *; 
 
43
      intros; elim (H eps H0); clear H; intros; elim H; 
 
44
        clear H; intros; elim (Req_dec (d x0) 0); intro.
 
45
  split with (Rmin 1 x); split.
 
46
  elim (Rmin_Rgt 1 x 0); intros a b; apply (b (conj Rlt_0_1 H)).
 
47
  intros; elim H3; clear H3; intros;
 
48
    generalize (let (H1, H2) := Rmin_Rgt 1 x (R_dist x1 x0) in H1);
 
49
      unfold Rgt in |- *; intro; elim (H5 H4); clear H5; 
 
50
        intros; generalize (H1 x1 (conj H3 H6)); clear H1; 
 
51
          intro; unfold D_x in H3; elim H3; intros.
 
52
  rewrite H2 in H1; unfold R_dist in |- *; unfold R_dist in H1;
 
53
    cut (Rabs (f x1 - f x0) < eps * Rabs (x1 - x0)).
 
54
  intro; unfold R_dist in H5;
 
55
    generalize (Rmult_lt_compat_l eps (Rabs (x1 - x0)) 1 H0 H5);
 
56
      rewrite Rmult_1_r; intro; apply Rlt_trans with (r2 := eps * Rabs (x1 - x0));
 
57
        assumption.
 
58
  rewrite (Rminus_0_r ((f x1 - f x0) * / (x1 - x0))) in H1;
 
59
    rewrite Rabs_mult in H1; cut (x1 - x0 <> 0).
 
60
  intro; rewrite (Rabs_Rinv (x1 - x0) H9) in H1;
 
61
    generalize
 
62
      (Rmult_lt_compat_l (Rabs (x1 - x0)) (Rabs (f x1 - f x0) * / Rabs (x1 - x0))
 
63
        eps (Rabs_pos_lt (x1 - x0) H9) H1); intro; rewrite Rmult_comm in H10;
 
64
      rewrite Rmult_assoc in H10; rewrite Rinv_l in H10.
 
65
  rewrite Rmult_1_r in H10; rewrite Rmult_comm; assumption.
 
66
  apply Rabs_no_R0; auto.
 
67
  apply Rminus_eq_contra; auto.
 
68
(**)
 
69
  split with (Rmin (Rmin (/ 2) x) (eps * / Rabs (2 * d x0))); split.
 
70
  cut (Rmin (/ 2) x > 0).
 
71
  cut (eps * / Rabs (2 * d x0) > 0).
 
72
  intros; elim (Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) 0);
 
73
    intros a b; apply (b (conj H4 H3)).
 
74
  apply Rmult_gt_0_compat; auto.
 
75
  unfold Rgt in |- *; apply Rinv_0_lt_compat; apply Rabs_pos_lt;
 
76
    apply Rmult_integral_contrapositive; split.
 
77
  discrR.
 
78
  assumption.
 
79
  elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2).
 
80
  intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4;
 
81
    apply (b (conj H4 H)).
 
82
  fourier.
 
83
  intros; elim H3; clear H3; intros;
 
84
    generalize
 
85
      (let (H1, H2) :=
 
86
        Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) (R_dist x1 x0) in
 
87
        H1); unfold Rgt in |- *; intro; elim (H5 H4); clear H5; 
 
88
      intros; generalize (let (H1, H2) := Rmin_Rgt (/ 2) x (R_dist x1 x0) in H1);
 
89
        unfold Rgt in |- *; intro; elim (H7 H5); clear H7; 
 
90
          intros; clear H4 H5; generalize (H1 x1 (conj H3 H8)); 
 
91
            clear H1; intro; unfold D_x in H3; elim H3; intros;
 
92
              generalize (sym_not_eq H5); clear H5; intro H5;
 
93
                generalize (Rminus_eq_contra x1 x0 H5); intro; generalize H1;
 
94
                  pattern (d x0) at 1 in |- *;
 
95
                    rewrite <- (let (H1, H2) := Rmult_ne (d x0) in H2);
 
96
                      rewrite <- (Rinv_l (x1 - x0) H9); unfold R_dist in |- *;
 
97
                        unfold Rminus at 1 in |- *; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0)));
 
98
                          rewrite (Rmult_comm (/ (x1 - x0) * (x1 - x0)) (d x0));
 
99
                            rewrite <- (Ropp_mult_distr_l_reverse (d x0) (/ (x1 - x0) * (x1 - x0)));
 
100
                              rewrite (Rmult_comm (- d x0) (/ (x1 - x0) * (x1 - x0)));
 
101
                                rewrite (Rmult_assoc (/ (x1 - x0)) (x1 - x0) (- d x0));
 
102
                                  rewrite <-
 
103
                                    (Rmult_plus_distr_l (/ (x1 - x0)) (f x1 - f x0) ((x1 - x0) * - d x0))
 
104
                                    ; rewrite (Rabs_mult (/ (x1 - x0)) (f x1 - f x0 + (x1 - x0) * - d x0));
 
105
                                      clear H1; intro;
 
106
                                        generalize
 
107
                                          (Rmult_lt_compat_l (Rabs (x1 - x0))
 
108
                                            (Rabs (/ (x1 - x0)) * Rabs (f x1 - f x0 + (x1 - x0) * - d x0)) eps
 
109
                                            (Rabs_pos_lt (x1 - x0) H9) H1);
 
110
                                          rewrite <-
 
111
                                            (Rmult_assoc (Rabs (x1 - x0)) (Rabs (/ (x1 - x0)))
 
112
                                              (Rabs (f x1 - f x0 + (x1 - x0) * - d x0)));
 
113
                                            rewrite (Rabs_Rinv (x1 - x0) H9);
 
114
                                              rewrite (Rinv_r (Rabs (x1 - x0)) (Rabs_no_R0 (x1 - x0) H9));
 
115
                                                rewrite
 
116
                                                  (let (H1, H2) := Rmult_ne (Rabs (f x1 - f x0 + (x1 - x0) * - d x0)) in H2)
 
117
                                                  ; generalize (Rabs_triang_inv (f x1 - f x0) ((x1 - x0) * d x0)); 
 
118
                                                    intro; rewrite (Rmult_comm (x1 - x0) (- d x0));
 
119
                                                      rewrite (Ropp_mult_distr_l_reverse (d x0) (x1 - x0));
 
120
                                                        fold (f x1 - f x0 - d x0 * (x1 - x0)) in |- *;
 
121
                                                          rewrite (Rmult_comm (x1 - x0) (d x0)) in H10; clear H1; 
 
122
                                                            intro;
 
123
                                                              generalize
 
124
                                                                (Rle_lt_trans (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0)))
 
125
                                                                  (Rabs (f x1 - f x0 - d x0 * (x1 - x0))) (Rabs (x1 - x0) * eps) H10 H1);
 
126
                                                                clear H1; intro;
 
127
                                                                  generalize
 
128
                                                                    (Rplus_lt_compat_l (Rabs (d x0 * (x1 - x0)))
 
129
                                                                      (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0))) (
 
130
                                                                        Rabs (x1 - x0) * eps) H1); unfold Rminus at 2 in |- *;
 
131
                                                                    rewrite (Rplus_comm (Rabs (f x1 - f x0)) (- Rabs (d x0 * (x1 - x0))));
 
132
                                                                      rewrite <-
 
133
                                                                        (Rplus_assoc (Rabs (d x0 * (x1 - x0))) (- Rabs (d x0 * (x1 - x0)))
 
134
                                                                          (Rabs (f x1 - f x0))); rewrite (Rplus_opp_r (Rabs (d x0 * (x1 - x0))));
 
135
                                                                        rewrite (let (H1, H2) := Rplus_ne (Rabs (f x1 - f x0)) in H2); 
 
136
                                                                          clear H1; intro; cut (Rabs (d x0 * (x1 - x0)) + Rabs (x1 - x0) * eps < eps).
 
137
  intro;
 
138
    apply
 
139
      (Rlt_trans (Rabs (f x1 - f x0))
 
140
        (Rabs (d x0 * (x1 - x0)) + Rabs (x1 - x0) * eps) eps H1 H11). 
 
141
  clear H1 H5 H3 H10; generalize (Rabs_pos_lt (d x0) H2); intro;
 
142
    unfold Rgt in H0;
 
143
      generalize (Rmult_lt_compat_l eps (R_dist x1 x0) (/ 2) H0 H7); 
 
144
        clear H7; intro;
 
145
          generalize
 
146
            (Rmult_lt_compat_l (Rabs (d x0)) (R_dist x1 x0) (
 
147
              eps * / Rabs (2 * d x0)) H1 H6); clear H6; intro;
 
148
            rewrite (Rmult_comm eps (R_dist x1 x0)) in H3; unfold R_dist in H3, H5;
 
149
              rewrite <- (Rabs_mult (d x0) (x1 - x0)) in H5;
 
150
                rewrite (Rabs_mult 2 (d x0)) in H5; cut (Rabs 2 <> 0).
 
151
  intro; fold (Rabs (d x0) > 0) in H1;
 
152
    rewrite
 
153
      (Rinv_mult_distr (Rabs 2) (Rabs (d x0)) H6
 
154
        (Rlt_dichotomy_converse (Rabs (d x0)) 0 (or_intror (Rabs (d x0) < 0) H1)))
 
155
      in H5;
 
156
      rewrite (Rmult_comm (Rabs (d x0)) (eps * (/ Rabs 2 * / Rabs (d x0)))) in H5;
 
157
        rewrite <- (Rmult_assoc eps (/ Rabs 2) (/ Rabs (d x0))) in H5;
 
158
          rewrite (Rmult_assoc (eps * / Rabs 2) (/ Rabs (d x0)) (Rabs (d x0))) in H5;
 
159
            rewrite
 
160
              (Rinv_l (Rabs (d x0))
 
161
                (Rlt_dichotomy_converse (Rabs (d x0)) 0 (or_intror (Rabs (d x0) < 0) H1)))
 
162
              in H5; rewrite (let (H1, H2) := Rmult_ne (eps * / Rabs 2) in H1) in H5;
 
163
                cut (Rabs 2 = 2).
 
164
  intro; rewrite H7 in H5;
 
165
    generalize
 
166
      (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2)
 
167
        (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro; 
 
168
      rewrite eps2 in H10; assumption.
 
169
  unfold Rabs in |- *; case (Rcase_abs 2); auto.
 
170
  intro; cut (0 < 2).
 
171
  intro; generalize (Rlt_asym 0 2 H7); intro; elimtype False; auto.
 
172
  fourier.
 
173
  apply Rabs_no_R0.
 
174
  discrR.
 
175
Qed.
 
176
 
 
177
 
 
178
(*********)
 
179
Lemma Dconst :
 
180
  forall (D:R -> Prop) (y x0:R), D_in (fun x:R => y) (fun x:R => 0) D x0.
 
181
Proof.
 
182
  unfold D_in in |- *; intros; unfold limit1_in in |- *;
 
183
    unfold limit_in in |- *; unfold Rdiv in |- *; intros; 
 
184
      simpl in |- *; split with eps; split; auto.
 
185
  intros; rewrite (Rminus_diag_eq y y (refl_equal y)); rewrite Rmult_0_l;
 
186
    unfold R_dist in |- *; rewrite (Rminus_diag_eq 0 0 (refl_equal 0));
 
187
      unfold Rabs in |- *; case (Rcase_abs 0); intro.
 
188
  absurd (0 < 0); auto.
 
189
  red in |- *; intro; apply (Rlt_irrefl 0 H1).
 
190
  unfold Rgt in H0; assumption.
 
191
Qed.
 
192
 
 
193
(*********)
 
194
Lemma Dx :
 
195
  forall (D:R -> Prop) (x0:R), D_in (fun x:R => x) (fun x:R => 1) D x0.
 
196
Proof.
 
197
  unfold D_in in |- *; unfold Rdiv in |- *; intros; unfold limit1_in in |- *;
 
198
    unfold limit_in in |- *; intros; simpl in |- *; split with eps; 
 
199
      split; auto.
 
200
  intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros;
 
201
    rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3)));
 
202
      unfold R_dist in |- *; rewrite (Rminus_diag_eq 1 1 (refl_equal 1));
 
203
        unfold Rabs in |- *; case (Rcase_abs 0); intro.
 
204
  absurd (0 < 0); auto.
 
205
  red in |- *; intro; apply (Rlt_irrefl 0 r).
 
206
  unfold Rgt in H; assumption.
 
207
Qed. 
 
208
 
 
209
(*********)
 
210
Lemma Dadd :
 
211
  forall (D:R -> Prop) (df dg f g:R -> R) (x0:R),
 
212
    D_in f df D x0 ->
 
213
    D_in g dg D x0 ->
 
214
    D_in (fun x:R => f x + g x) (fun x:R => df x + dg x) D x0.
 
215
Proof.
 
216
  unfold D_in in |- *; intros;
 
217
    generalize
 
218
      (limit_plus (fun x:R => (f x - f x0) * / (x - x0))
 
219
        (fun x:R => (g x - g x0) * / (x - x0)) (D_x D x0) (
 
220
          df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in in |- *;
 
221
      unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0); 
 
222
        clear H; intros; elim H; clear H; intros; split with x; 
 
223
          split; auto; intros; generalize (H1 x1 H2); clear H1; 
 
224
            intro; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1;
 
225
              rewrite (Rmult_comm (g x1 - g x0) (/ (x1 - x0))) in H1;
 
226
                rewrite <- (Rmult_plus_distr_l (/ (x1 - x0)) (f x1 - f x0) (g x1 - g x0))
 
227
                  in H1;
 
228
                  rewrite (Rmult_comm (/ (x1 - x0)) (f x1 - f x0 + (g x1 - g x0))) in H1;
 
229
                    cut (f x1 - f x0 + (g x1 - g x0) = f x1 + g x1 - (f x0 + g x0)).
 
230
  intro; rewrite H3 in H1; assumption.
 
231
  ring.
 
232
Qed.
 
233
 
 
234
(*********)
 
235
Lemma Dmult :
 
236
  forall (D:R -> Prop) (df dg f g:R -> R) (x0:R),
 
237
    D_in f df D x0 ->
 
238
    D_in g dg D x0 ->
 
239
    D_in (fun x:R => f x * g x) (fun x:R => df x * g x + f x * dg x) D x0.
 
240
Proof.
 
241
  intros; unfold D_in in |- *; generalize H H0; intros; unfold D_in in H, H0;
 
242
    generalize (cont_deriv f df D x0 H1); unfold continue_in in |- *; 
 
243
      intro;
 
244
        generalize
 
245
          (limit_mul (fun x:R => (g x - g x0) * / (x - x0)) (
 
246
            fun x:R => f x) (D_x D x0) (dg x0) (f x0) x0 H0 H3); 
 
247
          intro; cut (limit1_in (fun x:R => g x0) (D_x D x0) (g x0) x0).
 
248
  intro;
 
249
    generalize
 
250
      (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) (
 
251
        fun _:R => g x0) (D_x D x0) (df x0) (g x0) x0 H H5);
 
252
      clear H H0 H1 H2 H3 H5; intro;
 
253
        generalize
 
254
          (limit_plus (fun x:R => (f x - f x0) * / (x - x0) * g x0)
 
255
            (fun x:R => (g x - g x0) * / (x - x0) * f x) (
 
256
              D_x D x0) (df x0 * g x0) (dg x0 * f x0) x0 H H4); 
 
257
          clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H; 
 
258
            simpl in H; unfold limit1_in in |- *; unfold limit_in in |- *; 
 
259
              simpl in |- *; intros; elim (H eps H0); clear H; intros; 
 
260
                elim H; clear H; intros; split with x; split; auto; 
 
261
                  intros; generalize (H1 x1 H2); clear H1; intro;
 
262
                    rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1;
 
263
                      rewrite (Rmult_comm (g x1 - g x0) (/ (x1 - x0))) in H1;
 
264
                        rewrite (Rmult_assoc (/ (x1 - x0)) (f x1 - f x0) (g x0)) in H1;
 
265
                          rewrite (Rmult_assoc (/ (x1 - x0)) (g x1 - g x0) (f x1)) in H1;
 
266
                            rewrite <-
 
267
                              (Rmult_plus_distr_l (/ (x1 - x0)) ((f x1 - f x0) * g x0)
 
268
                                ((g x1 - g x0) * f x1)) in H1;
 
269
                              rewrite
 
270
                                (Rmult_comm (/ (x1 - x0)) ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1))
 
271
                                in H1; rewrite (Rmult_comm (dg x0) (f x0)) in H1;
 
272
                                  cut
 
273
                                    ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1 = f x1 * g x1 - f x0 * g x0).
 
274
  intro; rewrite H3 in H1; assumption.
 
275
  ring.
 
276
  unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
 
277
    split with eps; split; auto; intros; elim (R_dist_refl (g x0) (g x0));
 
278
      intros a b; rewrite (b (refl_equal (g x0))); unfold Rgt in H; 
 
279
        assumption.
 
280
Qed.
 
281
 
 
282
(*********)
 
283
Lemma Dmult_const :
 
284
  forall (D:R -> Prop) (f df:R -> R) (x0 a:R),
 
285
    D_in f df D x0 -> D_in (fun x:R => a * f x) (fun x:R => a * df x) D x0.
 
286
Proof.
 
287
  intros;
 
288
    generalize (Dmult D (fun _:R => 0) df (fun _:R => a) f x0 (Dconst D a x0) H);
 
289
      unfold D_in in |- *; intros; rewrite (Rmult_0_l (f x0)) in H0;
 
290
        rewrite (let (H1, H2) := Rplus_ne (a * df x0) in H2) in H0; 
 
291
          assumption.
 
292
Qed.
 
293
 
 
294
(*********)
 
295
Lemma Dopp :
 
296
  forall (D:R -> Prop) (f df:R -> R) (x0:R),
 
297
    D_in f df D x0 -> D_in (fun x:R => - f x) (fun x:R => - df x) D x0.
 
298
Proof.
 
299
  intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in in |- *;
 
300
    unfold limit1_in in |- *; unfold limit_in in |- *; 
 
301
      intros; generalize (H0 eps H1); clear H0; intro; elim H0; 
 
302
        clear H0; intros; elim H0; clear H0; simpl in |- *; 
 
303
          intros; split with x; split; auto.
 
304
  intros; generalize (H2 x1 H3); clear H2; intro;
 
305
    rewrite Ropp_mult_distr_l_reverse in H2;
 
306
      rewrite Ropp_mult_distr_l_reverse in H2;
 
307
        rewrite Ropp_mult_distr_l_reverse in H2;
 
308
          rewrite (let (H1, H2) := Rmult_ne (f x1) in H2) in H2;
 
309
            rewrite (let (H1, H2) := Rmult_ne (f x0) in H2) in H2;
 
310
              rewrite (let (H1, H2) := Rmult_ne (df x0) in H2) in H2; 
 
311
                assumption.
 
312
Qed.
 
313
 
 
314
(*********)
 
315
Lemma Dminus :
 
316
  forall (D:R -> Prop) (df dg f g:R -> R) (x0:R),
 
317
    D_in f df D x0 ->
 
318
    D_in g dg D x0 ->
 
319
    D_in (fun x:R => f x - g x) (fun x:R => df x - dg x) D x0.
 
320
Proof.
 
321
  unfold Rminus in |- *; intros; generalize (Dopp D g dg x0 H0); intro;
 
322
    apply (Dadd D df (fun x:R => - dg x) f (fun x:R => - g x) x0); 
 
323
      assumption. 
 
324
Qed.
 
325
 
 
326
(*********)
 
327
Lemma Dx_pow_n :
 
328
  forall (n:nat) (D:R -> Prop) (x0:R),
 
329
    D_in (fun x:R => x ^ n) (fun x:R => INR n * x ^ (n - 1)) D x0.
 
330
Proof.
 
331
  simple induction n; intros.
 
332
  simpl in |- *; rewrite Rmult_0_l; apply Dconst.
 
333
  intros; cut (n0 = (S n0 - 1)%nat);
 
334
    [ intro a; rewrite <- a; clear a | simpl in |- *; apply minus_n_O ].
 
335
  generalize
 
336
    (Dmult D (fun _:R => 1) (fun x:R => INR n0 * x ^ (n0 - 1)) (
 
337
      fun x:R => x) (fun x:R => x ^ n0) x0 (Dx D x0) (
 
338
        H D x0)); unfold D_in in |- *; unfold limit1_in in |- *;
 
339
    unfold limit_in in |- *; simpl in |- *; intros; elim (H0 eps H1); 
 
340
      clear H0; intros; elim H0; clear H0; intros; split with x; 
 
341
        split; auto.
 
342
  intros; generalize (H2 x1 H3); clear H2 H3; intro;
 
343
    rewrite (let (H1, H2) := Rmult_ne (x0 ^ n0) in H2) in H2;
 
344
      rewrite (tech_pow_Rmult x1 n0) in H2; rewrite (tech_pow_Rmult x0 n0) in H2;
 
345
        rewrite (Rmult_comm (INR n0) (x0 ^ (n0 - 1))) in H2;
 
346
          rewrite <- (Rmult_assoc x0 (x0 ^ (n0 - 1)) (INR n0)) in H2;
 
347
            rewrite (tech_pow_Rmult x0 (n0 - 1)) in H2; elim (classic (n0 = 0%nat));
 
348
              intro cond.
 
349
  rewrite cond in H2; rewrite cond; simpl in H2; simpl in |- *;
 
350
    cut (1 + x0 * 1 * 0 = 1 * 1);
 
351
      [ intro A; rewrite A in H2; assumption | ring ].
 
352
  cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ];
 
353
    rewrite (H3 cond) in H2; rewrite (Rmult_comm (x0 ^ n0) (INR n0)) in H2;
 
354
      rewrite (tech_pow_Rplus x0 n0 n0) in H2; assumption.
 
355
Qed.
 
356
 
 
357
(*********)
 
358
Lemma Dcomp :
 
359
  forall (Df Dg:R -> Prop) (df dg f g:R -> R) (x0:R),
 
360
    D_in f df Df x0 ->
 
361
    D_in g dg Dg (f x0) ->
 
362
    D_in (fun x:R => g (f x)) (fun x:R => df x * dg (f x)) (Dgf Df Dg f) x0.
 
363
Proof.
 
364
  intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in in |- *;
 
365
    unfold Rdiv in |- *; intros;
 
366
      generalize
 
367
        (limit_comp f (fun x:R => (g x - g (f x0)) * / (x - f x0)) (
 
368
          D_x Df x0) (D_x Dg (f x0)) (f x0) (dg (f x0)) x0); 
 
369
        intro; generalize (cont_deriv f df Df x0 H); intro; 
 
370
          unfold continue_in in H4; generalize (H3 H4 H2); clear H3; 
 
371
            intro;
 
372
              generalize
 
373
                (limit_mul (fun x:R => (g (f x) - g (f x0)) * / (f x - f x0))
 
374
                  (fun x:R => (f x - f x0) * / (x - x0))
 
375
                  (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (dg (f x0)) (
 
376
                    df x0) x0 H3); intro;
 
377
                cut
 
378
                  (limit1_in (fun x:R => (f x - f x0) * / (x - x0))
 
379
                    (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (df x0) x0).
 
380
  intro; generalize (H5 H6); clear H5; intro;
 
381
    generalize
 
382
      (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) (
 
383
        fun x:R => dg (f x0)) (D_x Df x0) (df x0) (dg (f x0)) x0 H1
 
384
      (limit_free (fun x:R => dg (f x0)) (D_x Df x0) x0 x0)); 
 
385
      intro; unfold limit1_in in |- *; unfold limit_in in |- *; 
 
386
        simpl in |- *; unfold limit1_in in H5, H7; unfold limit_in in H5, H7;
 
387
          simpl in H5, H7; intros; elim (H5 eps H8); elim (H7 eps H8); 
 
388
            clear H5 H7; intros; elim H5; elim H7; clear H5 H7; 
 
389
              intros; split with (Rmin x x1); split.
 
390
  elim (Rmin_Rgt x x1 0); intros a b; apply (b (conj H9 H5)); clear a b.
 
391
  intros; elim H11; clear H11; intros; elim (Rmin_Rgt x x1 (R_dist x2 x0));
 
392
    intros a b; clear b; unfold Rgt in a; elim (a H12); 
 
393
      clear H5 a; intros; unfold D_x, Dgf in H11, H7, H10; 
 
394
        clear H12; elim (classic (f x2 = f x0)); intro.
 
395
  elim H11; clear H11; intros; elim H11; clear H11; intros;
 
396
    generalize (H10 x2 (conj (conj H11 H14) H5)); intro;
 
397
      rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16;
 
398
        rewrite (Rmult_0_l (/ (x2 - x0))) in H16;
 
399
          rewrite (Rmult_0_l (dg (f x0))) in H16; rewrite H12;
 
400
            rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (refl_equal (g (f x0))));
 
401
              rewrite (Rmult_0_l (/ (x2 - x0))); assumption.
 
402
  clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros;
 
403
    cut
 
404
      (((Df x2 /\ x0 <> x2) /\ Dg (f x2) /\ f x0 <> f x2) /\ R_dist x2 x0 < x1);
 
405
      auto; intro; generalize (H7 x2 H14); intro;
 
406
        generalize (Rminus_eq_contra (f x2) (f x0) H12); intro;
 
407
          rewrite
 
408
            (Rmult_assoc (g (f x2) - g (f x0)) (/ (f x2 - f x0))
 
409
              ((f x2 - f x0) * / (x2 - x0))) in H15;
 
410
            rewrite <- (Rmult_assoc (/ (f x2 - f x0)) (f x2 - f x0) (/ (x2 - x0)))
 
411
              in H15; rewrite (Rinv_l (f x2 - f x0) H16) in H15;
 
412
                rewrite (let (H1, H2) := Rmult_ne (/ (x2 - x0)) in H2) in H15;
 
413
                  rewrite (Rmult_comm (df x0) (dg (f x0))); assumption.
 
414
  clear H5 H3 H4 H2; unfold limit1_in in |- *; unfold limit_in in |- *;
 
415
    simpl in |- *; unfold limit1_in in H1; unfold limit_in in H1; 
 
416
      simpl in H1; intros; elim (H1 eps H2); clear H1; intros; 
 
417
        elim H1; clear H1; intros; split with x; split; auto; 
 
418
          intros; unfold D_x, Dgf in H4, H3; elim H4; clear H4; 
 
419
            intros; elim H4; clear H4; intros; exact (H3 x1 (conj H4 H5)).
 
420
Qed.   
 
421
 
 
422
(*********)
 
423
Lemma D_pow_n :
 
424
  forall (n:nat) (D:R -> Prop) (x0:R) (expr dexpr:R -> R),
 
425
    D_in expr dexpr D x0 ->
 
426
    D_in (fun x:R => expr x ^ n)
 
427
    (fun x:R => INR n * expr x ^ (n - 1) * dexpr x) (
 
428
      Dgf D D expr) x0.
 
429
Proof.
 
430
  intros n D x0 expr dexpr H;
 
431
    generalize
 
432
      (Dcomp D D dexpr (fun x:R => INR n * x ^ (n - 1)) expr (
 
433
        fun x:R => x ^ n) x0 H (Dx_pow_n n D (expr x0))); 
 
434
      intro; unfold D_in in |- *; unfold limit1_in in |- *;
 
435
        unfold limit_in in |- *; simpl in |- *; intros; unfold D_in in H0;
 
436
          unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; 
 
437
            elim (H0 eps H1); clear H0; intros; elim H0; clear H0; 
 
438
              intros; split with x; split; intros; auto.
 
439
  cut
 
440
    (dexpr x0 * (INR n * expr x0 ^ (n - 1)) =
 
441
      INR n * expr x0 ^ (n - 1) * dexpr x0);
 
442
    [ intro Rew; rewrite <- Rew; exact (H2 x1 H3) | ring ].
 
443
Qed.