← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Ranalysis2.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/Ranalysis2.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: Ranalysis2.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import Ranalysis1.
 
14
Open Local Scope R_scope.
 
15
 
 
16
(**********)
 
17
Lemma formule :
 
18
  forall (x h l1 l2:R) (f1 f2:R -> R),
 
19
    h <> 0 ->
 
20
    f2 x <> 0 ->
 
21
    f2 (x + h) <> 0 ->
 
22
    (f1 (x + h) / f2 (x + h) - f1 x / f2 x) / h -
 
23
    (l1 * f2 x - l2 * f1 x) / Rsqr (f2 x) =
 
24
    / f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1) +
 
25
    l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h)) -
 
26
    f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2) +
 
27
    l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x).
 
28
Proof.
 
29
  intros; unfold Rdiv, Rminus, Rsqr in |- *.
 
30
  repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
 
31
    repeat rewrite Rinv_mult_distr; try assumption.
 
32
  replace (l1 * f2 x * (/ f2 x * / f2 x)) with (l1 * / f2 x * (f2 x * / f2 x));
 
33
  [ idtac | ring ].
 
34
  replace (l1 * (/ f2 x * / f2 (x + h)) * f2 x) with
 
35
  (l1 * / f2 (x + h) * (f2 x * / f2 x)); [ idtac | ring ].
 
36
  replace (l1 * (/ f2 x * / f2 (x + h)) * - f2 (x + h)) with
 
37
  (- (l1 * / f2 x * (f2 (x + h) * / f2 (x + h)))); [ idtac | ring ].
 
38
  replace (f1 x * (/ f2 x * / f2 (x + h)) * (f2 (x + h) * / h)) with
 
39
  (f1 x * / f2 x * / h * (f2 (x + h) * / f2 (x + h))); 
 
40
  [ idtac | ring ].
 
41
  replace (f1 x * (/ f2 x * / f2 (x + h)) * (- f2 x * / h)) with
 
42
  (- (f1 x * / f2 (x + h) * / h * (f2 x * / f2 x))); 
 
43
  [ idtac | ring ].
 
44
  replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * f2 (x + h)) with
 
45
  (l2 * f1 x * / f2 x * / f2 x * (f2 (x + h) * / f2 (x + h)));
 
46
  [ idtac | ring ].
 
47
  replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * - f2 x) with
 
48
  (- (l2 * f1 x * / f2 x * / f2 (x + h) * (f2 x * / f2 x))); 
 
49
  [ idtac | ring ].
 
50
  repeat rewrite <- Rinv_r_sym; try assumption || ring.
 
51
  apply prod_neq_R0; assumption.
 
52
Qed.
 
53
 
 
54
Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y.
 
55
Proof.
 
56
  intros; unfold Rmin in |- *.
 
57
  case (Rle_dec x y); intro; assumption.
 
58
Qed.
 
59
 
 
60
Lemma maj_term1 :
 
61
  forall (x h eps l1 alp_f2:R) (eps_f2 alp_f1d:posreal) 
 
62
    (f1 f2:R -> R),
 
63
    0 < eps ->
 
64
    f2 x <> 0 ->
 
65
    f2 (x + h) <> 0 ->
 
66
    (forall h:R,
 
67
      h <> 0 ->
 
68
      Rabs h < alp_f1d ->
 
69
      Rabs ((f1 (x + h) - f1 x) / h - l1) < Rabs (eps * f2 x / 8)) ->
 
70
    (forall a:R,
 
71
      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
 
72
    h <> 0 ->
 
73
    Rabs h < alp_f1d ->
 
74
    Rabs h < Rmin eps_f2 alp_f2 ->
 
75
    Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) < eps / 4.
 
76
Proof.
 
77
  intros.
 
78
  assert (H7 := H3 h H6).
 
79
  assert (H8 := H2 h H4 H5).
 
80
  apply Rle_lt_trans with
 
81
    (2 / Rabs (f2 x) * Rabs ((f1 (x + h) - f1 x) / h - l1)).
 
82
  rewrite Rabs_mult.
 
83
  apply Rmult_le_compat_r.
 
84
  apply Rabs_pos.
 
85
  rewrite Rabs_Rinv; [ left; exact H7 | assumption ].
 
86
  apply Rlt_le_trans with (2 / Rabs (f2 x) * Rabs (eps * f2 x / 8)).
 
87
  apply Rmult_lt_compat_l.
 
88
  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
89
    [ prove_sup0 | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ].
 
90
  exact H8.
 
91
  right; unfold Rdiv in |- *.
 
92
  repeat rewrite Rabs_mult.
 
93
  rewrite Rabs_Rinv; discrR.
 
94
  replace (Rabs 8) with 8.
 
95
  replace 8 with 8; [ idtac | ring ].
 
96
  rewrite Rinv_mult_distr; [ idtac | discrR | discrR ].
 
97
  replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with
 
98
  (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x)));
 
99
  [ idtac | ring ].
 
100
  replace (Rabs eps) with eps.
 
101
  repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
 
102
  ring.
 
103
  symmetry  in |- *; apply Rabs_right; left; assumption.
 
104
  symmetry  in |- *; apply Rabs_right; left; prove_sup.
 
105
Qed.
 
106
 
 
107
Lemma maj_term2 :
 
108
  forall (x h eps l1 alp_f2 alp_f2t2:R) (eps_f2:posreal) 
 
109
    (f2:R -> R),
 
110
    0 < eps ->
 
111
    f2 x <> 0 ->
 
112
    f2 (x + h) <> 0 ->
 
113
    (forall a:R,
 
114
      Rabs a < alp_f2t2 ->
 
115
      Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))) ->
 
116
    (forall a:R,
 
117
      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
 
118
    h <> 0 ->
 
119
    Rabs h < alp_f2t2 ->
 
120
    Rabs h < Rmin eps_f2 alp_f2 ->
 
121
    l1 <> 0 -> Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) < eps / 4.
 
122
Proof.
 
123
  intros.
 
124
  assert (H8 := H3 h H6).
 
125
  assert (H9 := H2 h H5).
 
126
  apply Rle_lt_trans with
 
127
    (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))).
 
128
  rewrite Rabs_mult; apply Rmult_le_compat_l.
 
129
  apply Rabs_pos.
 
130
  rewrite <- (Rabs_Ropp (f2 x - f2 (x + h))); rewrite Ropp_minus_distr.
 
131
  left; apply H9.
 
132
  apply Rlt_le_trans with
 
133
    (Rabs (2 * (l1 / (f2 x * f2 x))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))).
 
134
  apply Rmult_lt_compat_r.
 
135
  apply Rabs_pos_lt.
 
136
  unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0;
 
137
    try assumption || discrR.
 
138
  red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H).
 
139
  apply Rinv_neq_0_compat; apply prod_neq_R0; try assumption || discrR.
 
140
  unfold Rdiv in |- *.
 
141
  repeat rewrite Rinv_mult_distr; try assumption.
 
142
  repeat rewrite Rabs_mult.
 
143
  replace (Rabs 2) with 2.
 
144
  rewrite (Rmult_comm 2).
 
145
  replace (Rabs l1 * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with
 
146
  (Rabs l1 * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); 
 
147
  [ idtac | ring ].
 
148
  repeat apply Rmult_lt_compat_l.
 
149
  apply Rabs_pos_lt; assumption.
 
150
  apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption.
 
151
  repeat rewrite Rabs_Rinv; try assumption.
 
152
  rewrite <- (Rmult_comm 2).
 
153
  unfold Rdiv in H8; exact H8.
 
154
  symmetry  in |- *; apply Rabs_right; left; prove_sup0.
 
155
  right.
 
156
  unfold Rsqr, Rdiv in |- *.
 
157
  do 1 rewrite Rinv_mult_distr; try assumption || discrR.
 
158
  do 1 rewrite Rinv_mult_distr; try assumption || discrR.
 
159
  repeat rewrite Rabs_mult.
 
160
  repeat rewrite Rabs_Rinv; try assumption || discrR.
 
161
  replace (Rabs eps) with eps.
 
162
  replace (Rabs 8) with 8.
 
163
  replace (Rabs 2) with 2.
 
164
  replace 8 with (4 * 2); [ idtac | ring ].
 
165
  rewrite Rinv_mult_distr; discrR.
 
166
  replace
 
167
  (2 * (Rabs l1 * (/ Rabs (f2 x) * / Rabs (f2 x))) *
 
168
    (eps * (Rabs (f2 x) * Rabs (f2 x)) * (/ 4 * / 2 * / Rabs l1))) with
 
169
  (eps * / 4 * (Rabs l1 * / Rabs l1) * (Rabs (f2 x) * / Rabs (f2 x)) *
 
170
    (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ].
 
171
  repeat rewrite <- Rinv_r_sym; try (apply Rabs_no_R0; assumption) || discrR.
 
172
  ring.
 
173
  symmetry  in |- *; apply Rabs_right; left; prove_sup0.
 
174
  symmetry  in |- *; apply Rabs_right; left; prove_sup.
 
175
  symmetry  in |- *; apply Rabs_right; left; assumption.
 
176
Qed.
 
177
 
 
178
Lemma maj_term3 :
 
179
  forall (x h eps l2 alp_f2:R) (eps_f2 alp_f2d:posreal) 
 
180
    (f1 f2:R -> R),
 
181
    0 < eps ->
 
182
    f2 x <> 0 ->
 
183
    f2 (x + h) <> 0 ->
 
184
    (forall h:R,
 
185
      h <> 0 ->
 
186
      Rabs h < alp_f2d ->
 
187
      Rabs ((f2 (x + h) - f2 x) / h - l2) <
 
188
      Rabs (Rsqr (f2 x) * eps / (8 * f1 x))) ->
 
189
    (forall a:R,
 
190
      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
 
191
    h <> 0 ->
 
192
    Rabs h < alp_f2d ->
 
193
    Rabs h < Rmin eps_f2 alp_f2 ->
 
194
    f1 x <> 0 ->
 
195
    Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) <
 
196
    eps / 4.
 
197
Proof.
 
198
  intros.
 
199
  assert (H8 := H2 h H4 H5).
 
200
  assert (H9 := H3 h H6).
 
201
  apply Rle_lt_trans with
 
202
    (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))).
 
203
  rewrite Rabs_mult.
 
204
  apply Rmult_le_compat_l.
 
205
  apply Rabs_pos.
 
206
  left; apply H8.
 
207
  apply Rlt_le_trans with
 
208
    (Rabs (2 * (f1 x / (f2 x * f2 x))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))).
 
209
  apply Rmult_lt_compat_r.
 
210
  apply Rabs_pos_lt.
 
211
  unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0;
 
212
    try assumption.
 
213
  red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H).
 
214
  apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption.
 
215
  unfold Rdiv in |- *.
 
216
  repeat rewrite Rinv_mult_distr; try assumption.
 
217
  repeat rewrite Rabs_mult.
 
218
  replace (Rabs 2) with 2.
 
219
  rewrite (Rmult_comm 2).
 
220
  replace (Rabs (f1 x) * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with
 
221
  (Rabs (f1 x) * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); 
 
222
  [ idtac | ring ].
 
223
  repeat apply Rmult_lt_compat_l.
 
224
  apply Rabs_pos_lt; assumption.
 
225
  apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption.
 
226
  repeat rewrite Rabs_Rinv; assumption || idtac.
 
227
  rewrite <- (Rmult_comm 2).
 
228
  unfold Rdiv in H9; exact H9.
 
229
  symmetry  in |- *; apply Rabs_right; left; prove_sup0.
 
230
  right.
 
231
  unfold Rsqr, Rdiv in |- *.
 
232
  rewrite Rinv_mult_distr; try assumption || discrR.
 
233
  rewrite Rinv_mult_distr; try assumption || discrR.
 
234
  repeat rewrite Rabs_mult.
 
235
  repeat rewrite Rabs_Rinv; try assumption || discrR.
 
236
  replace (Rabs eps) with eps.
 
237
  replace (Rabs 8) with 8.
 
238
  replace (Rabs 2) with 2.
 
239
  replace 8 with (4 * 2); [ idtac | ring ].
 
240
  rewrite Rinv_mult_distr; discrR.
 
241
  replace
 
242
  (2 * (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x))) *
 
243
    (Rabs (f2 x) * Rabs (f2 x) * eps * (/ 4 * / 2 * / Rabs (f1 x)))) with
 
244
  (eps * / 4 * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) *
 
245
    (Rabs (f1 x) * / Rabs (f1 x)) * (2 * / 2)); [ idtac | ring ].
 
246
  repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
 
247
  ring.
 
248
  symmetry  in |- *; apply Rabs_right; left; prove_sup0.
 
249
  symmetry  in |- *; apply Rabs_right; left; prove_sup.
 
250
  symmetry  in |- *; apply Rabs_right; left; assumption.
 
251
Qed.
 
252
 
 
253
Lemma maj_term4 :
 
254
  forall (x h eps l2 alp_f2 alp_f2c:R) (eps_f2:posreal) 
 
255
    (f1 f2:R -> R),
 
256
    0 < eps ->
 
257
    f2 x <> 0 ->
 
258
    f2 (x + h) <> 0 ->
 
259
    (forall a:R,
 
260
      Rabs a < alp_f2c ->
 
261
      Rabs (f2 (x + a) - f2 x) <
 
262
      Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) ->
 
263
    (forall a:R,
 
264
      Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) ->
 
265
    h <> 0 ->
 
266
    Rabs h < alp_f2c ->
 
267
    Rabs h < Rmin eps_f2 alp_f2 ->
 
268
    f1 x <> 0 ->
 
269
    l2 <> 0 ->
 
270
    Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x)) <
 
271
    eps / 4.
 
272
Proof.
 
273
  intros.
 
274
  assert (H9 := H2 h H5).
 
275
  assert (H10 := H3 h H6).
 
276
  apply Rle_lt_trans with
 
277
    (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) *
 
278
      Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
 
279
  rewrite Rabs_mult.
 
280
  apply Rmult_le_compat_l.
 
281
  apply Rabs_pos.
 
282
  left; apply H9.
 
283
  apply Rlt_le_trans with
 
284
    (Rabs (2 * l2 * (f1 x / (Rsqr (f2 x) * f2 x))) *
 
285
      Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))).
 
286
  apply Rmult_lt_compat_r.
 
287
  apply Rabs_pos_lt.
 
288
  unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0;
 
289
    assumption || idtac.
 
290
  red in |- *; intro H11; rewrite H11 in H; elim (Rlt_irrefl _ H).
 
291
  apply Rinv_neq_0_compat; apply prod_neq_R0.
 
292
  apply prod_neq_R0.
 
293
  discrR.
 
294
  assumption.
 
295
  assumption.
 
296
  unfold Rdiv in |- *.
 
297
  repeat rewrite Rinv_mult_distr;
 
298
    try assumption || (unfold Rsqr in |- *; apply prod_neq_R0; assumption).
 
299
  repeat rewrite Rabs_mult.
 
300
  replace (Rabs 2) with 2.
 
301
  replace
 
302
  (2 * Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 x)))) with
 
303
  (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * (Rabs (/ f2 x) * 2))));
 
304
  [ idtac | ring ].
 
305
  replace
 
306
  (Rabs l2 * Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h)))) with
 
307
  (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h)))));
 
308
  [ idtac | ring ].
 
309
  repeat apply Rmult_lt_compat_l.
 
310
  apply Rabs_pos_lt; assumption.
 
311
  apply Rabs_pos_lt; assumption.
 
312
  apply Rabs_pos_lt; apply Rinv_neq_0_compat; unfold Rsqr in |- *;
 
313
    apply prod_neq_R0; assumption.
 
314
  repeat rewrite Rabs_Rinv; [ idtac | assumption | assumption ].
 
315
  rewrite <- (Rmult_comm 2).
 
316
  unfold Rdiv in H10; exact H10.
 
317
  symmetry  in |- *; apply Rabs_right; left; prove_sup0.
 
318
  right; unfold Rsqr, Rdiv in |- *.
 
319
  rewrite Rinv_mult_distr; try assumption || discrR.
 
320
  rewrite Rinv_mult_distr; try assumption || discrR.
 
321
  rewrite Rinv_mult_distr; try assumption || discrR.
 
322
  rewrite Rinv_mult_distr; try assumption || discrR.
 
323
  repeat rewrite Rabs_mult.
 
324
  repeat rewrite Rabs_Rinv; try assumption || discrR.
 
325
  replace (Rabs eps) with eps.
 
326
  replace (Rabs 8) with 8.
 
327
  replace (Rabs 2) with 2.
 
328
  replace 8 with (4 * 2); [ idtac | ring ].
 
329
  rewrite Rinv_mult_distr; discrR.
 
330
  replace
 
331
  (2 * Rabs l2 *
 
332
    (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x) * / Rabs (f2 x))) *
 
333
    (Rabs (f2 x) * Rabs (f2 x) * Rabs (f2 x) * eps *
 
334
      (/ 4 * / 2 * / Rabs (f1 x) * / Rabs l2))) with
 
335
  (eps * / 4 * (Rabs l2 * / Rabs l2) * (Rabs (f1 x) * / Rabs (f1 x)) *
 
336
    (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) *
 
337
    (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ].
 
338
  repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
 
339
  ring.
 
340
  symmetry  in |- *; apply Rabs_right; left; prove_sup0.
 
341
  symmetry  in |- *; apply Rabs_right; left; prove_sup.
 
342
  symmetry  in |- *; apply Rabs_right; left; assumption.
 
343
  apply prod_neq_R0; assumption || discrR.
 
344
  apply prod_neq_R0; assumption.
 
345
Qed.
 
346
 
 
347
Lemma D_x_no_cond : forall x a:R, a <> 0 -> D_x no_cond x (x + a).
 
348
Proof.
 
349
  intros.
 
350
  unfold D_x, no_cond in |- *.
 
351
  split.
 
352
  trivial.
 
353
  apply Rminus_not_eq.
 
354
  unfold Rminus in |- *.
 
355
  rewrite Ropp_plus_distr.
 
356
  rewrite <- Rplus_assoc.
 
357
  rewrite Rplus_opp_r.
 
358
  rewrite Rplus_0_l.
 
359
  apply Ropp_neq_0_compat; assumption.
 
360
Qed.
 
361
 
 
362
Lemma Rabs_4 :
 
363
  forall a b c d:R, Rabs (a + b + c + d) <= Rabs a + Rabs b + Rabs c + Rabs d.
 
364
Proof.
 
365
  intros.
 
366
  apply Rle_trans with (Rabs (a + b) + Rabs (c + d)).
 
367
  replace (a + b + c + d) with (a + b + (c + d)); [ apply Rabs_triang | ring ].
 
368
  apply Rle_trans with (Rabs a + Rabs b + Rabs (c + d)).
 
369
  apply Rplus_le_compat_r.
 
370
  apply Rabs_triang.
 
371
  repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l.
 
372
  apply Rabs_triang.
 
373
Qed.
 
374
 
 
375
Lemma Rlt_4 :
 
376
  forall a b c d e f g h:R,
 
377
    a < b -> c < d -> e < f -> g < h -> a + c + e + g < b + d + f + h.
 
378
Proof.
 
379
  intros; apply Rlt_trans with (b + c + e + g).
 
380
  repeat apply Rplus_lt_compat_r; assumption.
 
381
  repeat rewrite Rplus_assoc; apply Rplus_lt_compat_l.
 
382
  apply Rlt_trans with (d + e + g).
 
383
  rewrite Rplus_assoc; apply Rplus_lt_compat_r; assumption.
 
384
  rewrite Rplus_assoc; apply Rplus_lt_compat_l; apply Rlt_trans with (f + g).
 
385
  apply Rplus_lt_compat_r; assumption.
 
386
  apply Rplus_lt_compat_l; assumption.
 
387
Qed.
 
388
 
 
389
Lemma Rmin_2 : forall a b c:R, a < b -> a < c -> a < Rmin b c.
 
390
Proof.
 
391
  intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption.
 
392
Qed.
 
393
 
 
394
Lemma quadruple : forall x:R, 4 * x = x + x + x + x.
 
395
Proof.
 
396
  intro; ring.
 
397
Qed.
 
398
 
 
399
Lemma quadruple_var : forall x:R, x = x / 4 + x / 4 + x / 4 + x / 4.
 
400
Proof.
 
401
  intro; rewrite <- quadruple.
 
402
  unfold Rdiv in |- *; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; discrR.
 
403
  reflexivity.
 
404
Qed.
 
405
 
 
406
(**********)
 
407
Lemma continuous_neq_0 :
 
408
  forall (f:R -> R) (x0:R),
 
409
    continuity_pt f x0 ->
 
410
    f x0 <> 0 ->
 
411
    exists eps : posreal, (forall h:R, Rabs h < eps -> f (x0 + h) <> 0).
 
412
Proof.
 
413
  intros; unfold continuity_pt in H; unfold continue_in in H;
 
414
    unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))).
 
415
  intros; elim H1; intros.
 
416
  exists (mkposreal x H2).
 
417
  intros; assert (H5 := H3 (x0 + h)).
 
418
  cut
 
419
    (dist R_met (x0 + h) x0 < x ->
 
420
      dist R_met (f (x0 + h)) (f x0) < Rabs (f x0 / 2)).
 
421
  unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
 
422
    replace (x0 + h - x0) with h.
 
423
  intros; assert (H7 := H6 H4).
 
424
  red in |- *; intro.
 
425
  rewrite H8 in H7; unfold Rminus in H7; rewrite Rplus_0_l in H7;
 
426
    rewrite Rabs_Ropp in H7; unfold Rdiv in H7; rewrite Rabs_mult in H7;
 
427
      pattern (Rabs (f x0)) at 1 in H7; rewrite <- Rmult_1_r in H7.
 
428
  cut (0 < Rabs (f x0)).
 
429
  intro; assert (H10 := Rmult_lt_reg_l _ _ _ H9 H7).
 
430
  cut (Rabs (/ 2) = / 2).
 
431
  assert (Hyp : 0 < 2).
 
432
  prove_sup0.
 
433
  intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10);
 
434
    rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; 
 
435
      [ idtac | discrR ].
 
436
  cut (IZR 1 < IZR 2).
 
437
  unfold IZR in |- *; unfold INR, nat_of_P in |- *; simpl in |- *; intro;
 
438
    elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)).
 
439
  apply IZR_lt; omega.
 
440
  unfold Rabs in |- *; case (Rcase_abs (/ 2)); intro.
 
441
  assert (Hyp : 0 < 2).
 
442
  prove_sup0.
 
443
  assert (H11 := Rmult_lt_compat_l 2 _ _ Hyp r); rewrite Rmult_0_r in H11;
 
444
    rewrite <- Rinv_r_sym in H11; [ idtac | discrR ].
 
445
  elim (Rlt_irrefl 0 (Rlt_trans _ _ _ Rlt_0_1 H11)).
 
446
  reflexivity.
 
447
  apply (Rabs_pos_lt _ H0).
 
448
  ring.
 
449
  assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro.
 
450
  intro; rewrite <- H7; unfold dist, R_met in |- *; unfold R_dist in |- *;
 
451
    unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
 
452
      apply Rabs_pos_lt.
 
453
  unfold Rdiv in |- *; apply prod_neq_R0;
 
454
    [ assumption | apply Rinv_neq_0_compat; discrR ].
 
455
  intro; apply H5.
 
456
  split.
 
457
  unfold D_x, no_cond in |- *.
 
458
  split; trivial || assumption.
 
459
  assumption.
 
460
  change (0 < Rabs (f x0 / 2)) in |- *.
 
461
  apply Rabs_pos_lt; unfold Rdiv in |- *; apply prod_neq_R0.
 
462
  assumption.
 
463
  apply Rinv_neq_0_compat; discrR.
 
464
Qed.