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: Rlimit.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
11
(*********************************************************)
12
(** Definition of the limit *)
14
(*********************************************************)
17
Require Import Rfunctions.
18
Require Import Classical_Prop.
19
Require Import Fourier.
20
Open Local Scope R_scope.
22
(*******************************)
24
(*******************************)
26
Lemma eps2_Rgt_R0 : forall eps:R, eps > 0 -> eps * / 2 > 0.
32
Lemma eps2 : forall eps:R, eps * / 2 + eps * / 2 = eps.
35
assert (H := double_var esp).
37
symmetry in |- *; exact H.
41
Lemma eps4 : forall eps:R, eps * / (2 + 2) + eps * / (2 + 2) = eps * / 2.
44
replace (2 + 2) with 4.
45
pattern eps at 3 in |- *; rewrite double_var.
46
rewrite (Rmult_plus_distr_r (eps / 2) (eps / 2) (/ 2)).
48
repeat rewrite Rmult_assoc.
49
rewrite <- Rinv_mult_distr.
57
Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps.
60
pattern eps at 2 in |- *; rewrite <- Rmult_1_r.
61
repeat rewrite (Rmult_comm eps).
62
apply Rmult_lt_compat_r.
64
apply Rmult_lt_reg_l with 2.
66
rewrite Rmult_1_r; rewrite <- Rinv_r_sym.
72
Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps.
75
replace (2 + 2) with 4.
76
pattern eps at 2 in |- *; rewrite <- Rmult_1_r.
77
repeat rewrite (Rmult_comm eps).
78
apply Rmult_lt_compat_r.
80
apply Rmult_lt_reg_l with 4.
82
apply Rmult_lt_0_compat; fourier.
84
rewrite Rmult_1_r; rewrite <- Rinv_r_sym.
91
Lemma prop_eps : forall r:R, (forall eps:R, eps > 0 -> r < eps) -> r <= 0.
93
intros; elim (Rtotal_order r 0); intro.
94
apply Rlt_le; assumption.
96
apply Req_le; assumption.
97
clear H0; generalize (H r H1); intro; generalize (Rlt_irrefl r); intro;
102
Definition mul_factor (l l':R) := / (1 + (Rabs l + Rabs l')).
105
Lemma mul_factor_wd : forall l l':R, 1 + (Rabs l + Rabs l') <> 0.
107
intros; rewrite (Rplus_comm 1 (Rabs l + Rabs l')); apply tech_Rplus.
108
cut (Rabs (l + l') <= Rabs l + Rabs l').
109
cut (0 <= Rabs (l + l')).
110
exact (Rle_trans _ _ _).
111
exact (Rabs_pos (l + l')).
112
exact (Rabs_triang _ _).
117
Lemma mul_factor_gt : forall eps l l':R, eps > 0 -> eps * mul_factor l l' > 0.
119
intros; unfold Rgt in |- *; rewrite <- (Rmult_0_r eps);
120
apply Rmult_lt_compat_l.
122
unfold mul_factor in |- *; apply Rinv_0_lt_compat;
123
cut (1 <= 1 + (Rabs l + Rabs l')).
125
exact (Rlt_le_trans _ _ _).
127
replace (1 <= 1 + (Rabs l + Rabs l')) with (1 + 0 <= 1 + (Rabs l + Rabs l')).
128
apply Rplus_le_compat_l.
129
cut (Rabs (l + l') <= Rabs l + Rabs l').
130
cut (0 <= Rabs (l + l')).
131
exact (Rle_trans _ _ _).
133
exact (Rabs_triang _ _).
134
rewrite (proj1 (Rplus_ne 1)); trivial.
138
Lemma mul_factor_gt_f :
139
forall eps l l':R, eps > 0 -> Rmin 1 (eps * mul_factor l l') > 0.
140
intros; apply Rmin_Rgt_r; split.
142
exact (mul_factor_gt eps l l' H).
146
(*******************************)
147
(** * Metric space *)
148
(*******************************)
151
Record Metric_Space : Type :=
153
dist : Base -> Base -> R;
154
dist_pos : forall x y:Base, dist x y >= 0;
155
dist_sym : forall x y:Base, dist x y = dist y x;
156
dist_refl : forall x y:Base, dist x y = 0 <-> x = y;
157
dist_tri : forall x y z:Base, dist x y <= dist x z + dist z y}.
159
(*******************************)
160
(** ** Limit in Metric space *)
161
(*******************************)
164
Definition limit_in (X X':Metric_Space) (f:Base X -> Base X')
165
(D:Base X -> Prop) (x0:Base X) (l:Base X') :=
170
(forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps).
172
(*******************************)
173
(** ** R is a metric space *)
174
(*******************************)
177
Definition R_met : Metric_Space :=
178
Build_Metric_Space R R_dist R_dist_pos R_dist_sym R_dist_refl R_dist_tri.
180
(*******************************)
182
(*******************************)
184
Definition Dgf (Df Dg:R -> Prop) (f:R -> R) (x:R) := Df x /\ Dg (f x).
187
Definition limit1_in (f:R -> R) (D:R -> Prop) (l x0:R) : Prop :=
188
limit_in R_met R_met f D x0 l.
192
forall (f:R -> R) (D:R -> Prop) (l x0:R),
193
D x0 -> limit1_in f D l x0 -> l = f x0.
195
intros f D l x0 H H0.
196
case (Rabs_pos (f x0 - l)); intros H1.
197
absurd (dist R_met (f x0) l < dist R_met (f x0) l).
199
case (H0 (dist R_met (f x0) l)); auto.
200
intros alpha1 [H2 H3]; apply H3; auto; split; auto.
201
case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto.
202
case (dist_refl R_met (f x0) l); intros Hr1 Hr2; apply sym_eq; auto.
206
Lemma tech_limit_contr :
207
forall (f:R -> R) (D:R -> Prop) (l x0:R),
208
D x0 -> l <> f x0 -> ~ limit1_in f D l x0.
210
intros; generalize (tech_limit f D l x0); tauto.
214
Lemma lim_x : forall (D:R -> Prop) (x0:R), limit1_in (fun x:R => x) D x0 x0.
216
unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
217
split with eps; split; auto; intros; elim H0; intros;
223
forall (f g:R -> R) (D:R -> Prop) (l l' x0:R),
224
limit1_in f D l x0 ->
225
limit1_in g D l' x0 -> limit1_in (fun x:R => f x + g x) D (l + l') x0.
227
intros; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *;
228
intros; elim (H (eps * / 2) (eps2_Rgt_R0 eps H1));
229
elim (H0 (eps * / 2) (eps2_Rgt_R0 eps H1)); simpl in |- *;
230
clear H H0; intros; elim H; elim H0; clear H H0; intros;
231
split with (Rmin x1 x); split.
232
exact (Rmin_Rgt_r x1 x 0 (conj H H2)).
233
intros; elim H4; clear H4; intros;
234
cut (R_dist (f x2) l + R_dist (g x2) l' < eps).
235
cut (R_dist (f x2 + g x2) (l + l') <= R_dist (f x2) l + R_dist (g x2) l').
236
exact (Rle_lt_trans _ _ _).
237
exact (R_dist_plus _ _ _ _).
238
elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); clear H5; intros.
239
generalize (H3 x2 (conj H4 H6)); generalize (H0 x2 (conj H4 H5)); intros;
240
replace eps with (eps * / 2 + eps * / 2).
241
exact (Rplus_lt_compat _ _ _ _ H7 H8).
247
forall (f:R -> R) (D:R -> Prop) (l x0:R),
248
limit1_in f D l x0 -> limit1_in (fun x:R => - f x) D (- l) x0.
250
unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
251
elim (H eps H0); clear H; intros; elim H; clear H;
252
intros; split with x; split; auto; intros; generalize (H1 x1 H2);
253
clear H1; intro; unfold R_dist in |- *; unfold Rminus in |- *;
254
rewrite (Ropp_involutive l); rewrite (Rplus_comm (- f x1) l);
255
fold (l - f x1) in |- *; fold (R_dist l (f x1)) in |- *;
256
rewrite R_dist_sym; assumption.
261
forall (f g:R -> R) (D:R -> Prop) (l l' x0:R),
262
limit1_in f D l x0 ->
263
limit1_in g D l' x0 -> limit1_in (fun x:R => f x - g x) D (l - l') x0.
265
intros; unfold Rminus in |- *; generalize (limit_Ropp g D l' x0 H0); intro;
266
exact (limit_plus f (fun x:R => - g x) D l (- l') x0 H H1).
271
forall (f:R -> R) (D:R -> Prop) (x x0:R),
272
limit1_in (fun h:R => f x) D (f x) x0.
274
unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
275
split with eps; split; auto; intros; elim (R_dist_refl (f x) (f x));
276
intros a b; rewrite (b (refl_equal (f x))); unfold Rgt in H;
282
forall (f g:R -> R) (D:R -> Prop) (l l' x0:R),
283
limit1_in f D l x0 ->
284
limit1_in g D l' x0 -> limit1_in (fun x:R => f x * g x) D (l * l') x0.
286
intros; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *;
288
elim (H (Rmin 1 (eps * mul_factor l l')) (mul_factor_gt_f eps l l' H1));
289
elim (H0 (eps * mul_factor l l') (mul_factor_gt eps l l' H1));
290
clear H H0; simpl in |- *; intros; elim H; elim H0;
291
clear H H0; intros; split with (Rmin x1 x); split.
292
exact (Rmin_Rgt_r x1 x 0 (conj H H2)).
293
intros; elim H4; clear H4; intros; unfold R_dist in |- *;
294
replace (f x2 * g x2 - l * l') with (f x2 * (g x2 - l') + l' * (f x2 - l)).
295
cut (Rabs (f x2 * (g x2 - l')) + Rabs (l' * (f x2 - l)) < eps).
297
(Rabs (f x2 * (g x2 - l') + l' * (f x2 - l)) <=
298
Rabs (f x2 * (g x2 - l')) + Rabs (l' * (f x2 - l))).
299
exact (Rle_lt_trans _ _ _).
300
exact (Rabs_triang _ _).
301
rewrite (Rabs_mult (f x2) (g x2 - l')); rewrite (Rabs_mult l' (f x2 - l));
303
((1 + Rabs l) * (eps * mul_factor l l') + Rabs l' * (eps * mul_factor l l') <=
306
(Rabs (f x2) * Rabs (g x2 - l') + Rabs l' * Rabs (f x2 - l) <
307
(1 + Rabs l) * (eps * mul_factor l l') + Rabs l' * (eps * mul_factor l l')).
308
exact (Rlt_le_trans _ _ _).
309
elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); clear H5; intros;
310
generalize (H0 x2 (conj H4 H5)); intro; generalize (Rmin_Rgt_l _ _ _ H7);
311
intro; elim H8; intros; clear H0 H8; apply Rplus_lt_le_compat.
312
apply Rmult_ge_0_gt_0_lt_compat.
314
exact (Rabs_pos (g x2 - l')).
315
rewrite (Rplus_comm 1 (Rabs l)); unfold Rgt in |- *; apply Rle_lt_0_plus_1;
318
apply (Rplus_lt_reg_r (- Rabs l) (Rabs (f x2)) (1 + Rabs l)).
319
rewrite <- (Rplus_assoc (- Rabs l) 1 (Rabs l));
320
rewrite (Rplus_comm (- Rabs l) 1);
321
rewrite (Rplus_assoc 1 (- Rabs l) (Rabs l)); rewrite (Rplus_opp_l (Rabs l));
322
rewrite (proj1 (Rplus_ne 1)); rewrite (Rplus_comm (- Rabs l) (Rabs (f x2)));
323
generalize H9; cut (Rabs (f x2) - Rabs l <= Rabs (f x2 - l)).
324
exact (Rle_lt_trans _ _ _).
325
exact (Rabs_triang_inv _ _).
326
generalize (H3 x2 (conj H4 H6)); trivial.
327
apply Rmult_le_compat_l.
329
unfold Rle in |- *; left; assumption.
330
rewrite (Rmult_comm (1 + Rabs l) (eps * mul_factor l l'));
331
rewrite (Rmult_comm (Rabs l') (eps * mul_factor l l'));
333
(Rmult_plus_distr_l (eps * mul_factor l l') (1 + Rabs l) (Rabs l'))
334
; rewrite (Rmult_assoc eps (mul_factor l l') (1 + Rabs l + Rabs l'));
335
rewrite (Rplus_assoc 1 (Rabs l) (Rabs l')); unfold mul_factor in |- *;
336
rewrite (Rinv_l (1 + (Rabs l + Rabs l')) (mul_factor_wd l l'));
337
rewrite (proj1 (Rmult_ne eps)); apply Req_le; trivial.
342
Definition adhDa (D:R -> Prop) (a:R) : Prop :=
343
forall alp:R, alp > 0 -> exists x : R, D x /\ R_dist x a < alp.
347
forall (f:R -> R) (D:R -> Prop) (l l' x0:R),
348
adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'.
350
unfold limit1_in in |- *; unfold limit_in in |- *; intros.
351
cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps).
352
clear H0 H1; unfold dist in |- *; unfold R_met in |- *; unfold R_dist in |- *;
353
unfold Rabs in |- *; case (Rcase_abs (l - l')); intros.
354
cut (forall eps:R, eps > 0 -> - (l - l') < eps).
355
intro; generalize (prop_eps (- (l - l')) H1); intro;
356
generalize (Ropp_gt_lt_0_contravar (l - l') r); intro;
357
unfold Rgt in H3; generalize (Rgt_not_le (- (l - l')) 0 H3);
358
intro; elimtype False; auto.
359
intros; cut (eps * / 2 > 0).
360
intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2));
361
rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2).
362
elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial.
363
apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro;
364
unfold Rgt in |- *; generalize (Rplus_lt_compat_l 1 0 1 H3);
365
intro; elim (Rplus_ne 1); intros a b; rewrite a in H4;
366
clear a b; apply (Rlt_trans 0 1 2 H3 H4).
367
unfold Rgt in |- *; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2));
368
rewrite <- (Rmult_0_r (/ 2)); apply (Rmult_lt_compat_l (/ 2) 0 eps);
370
apply (Rinv_0_lt_compat 2); cut (1 < 2).
371
intro; apply (Rlt_trans 0 1 2 Rlt_0_1 H2).
372
generalize (Rplus_lt_compat_l 1 0 1 Rlt_0_1); elim (Rplus_ne 1); intros a b;
373
rewrite a; clear a b; trivial.
375
cut (forall eps:R, eps > 0 -> l - l' < eps).
376
intro; generalize (prop_eps (l - l') H1); intro; elim (Rle_le_eq (l - l') 0);
377
intros a b; clear b; apply (Rminus_diag_uniq l l');
380
apply (Rge_le (l - l') 0 r).
381
intros; cut (eps * / 2 > 0).
382
intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2));
383
rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2).
384
elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial.
385
apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro;
386
unfold Rgt in |- *; generalize (Rplus_lt_compat_l 1 0 1 H3);
387
intro; elim (Rplus_ne 1); intros a b; rewrite a in H4;
388
clear a b; apply (Rlt_trans 0 1 2 H3 H4).
389
unfold Rgt in |- *; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2));
390
rewrite <- (Rmult_0_r (/ 2)); apply (Rmult_lt_compat_l (/ 2) 0 eps);
392
apply (Rinv_0_lt_compat 2); cut (1 < 2).
393
intro; apply (Rlt_trans 0 1 2 Rlt_0_1 H2).
394
generalize (Rplus_lt_compat_l 1 0 1 Rlt_0_1); elim (Rplus_ne 1); intros a b;
395
rewrite a; clear a b; trivial.
397
intros; unfold adhDa in H; elim (H0 eps H2); intros; elim (H1 eps H2); intros;
398
clear H0 H1; elim H3; elim H4; clear H3 H4; intros;
399
simpl in |- *; simpl in H1, H4; generalize (Rmin_Rgt x x1 0);
400
intro; elim H5; intros; clear H5; elim (H (Rmin x x1) (H7 (conj H3 H0)));
401
intros; elim H5; intros; clear H5 H H6 H7;
402
generalize (Rmin_Rgt x x1 (R_dist x2 x0)); intro;
403
elim H; intros; clear H H6; unfold Rgt in H5; elim (H5 H9);
404
intros; clear H5 H9; generalize (H1 x2 (conj H8 H6));
405
generalize (H4 x2 (conj H8 H)); clear H8 H H6 H1 H4 H0 H3;
408
(Rplus_lt_compat (R_dist (f x2) l) eps (R_dist (f x2) l') eps H H0);
409
unfold R_dist in |- *; intros; rewrite (Rabs_minus_sym (f x2) l) in H1;
410
rewrite (Rmult_comm 2 eps); rewrite (Rmult_plus_distr_l eps 1 1);
411
elim (Rmult_ne eps); intros a b; rewrite a; clear a b;
412
generalize (R_dist_tri l l' (f x2)); unfold R_dist in |- *;
415
(Rle_lt_trans (Rabs (l - l')) (Rabs (l - f x2) + Rabs (f x2 - l'))
421
forall (f g:R -> R) (Df Dg:R -> Prop) (l l' x0:R),
422
limit1_in f Df l x0 ->
423
limit1_in g Dg l' l -> limit1_in (fun x:R => g (f x)) (Dgf Df Dg f) l' x0.
425
unfold limit1_in, limit_in, Dgf in |- *; simpl in |- *.
426
intros f g Df Dg l l' x0 Hf Hg eps eps_pos.
427
elim (Hg eps eps_pos).
439
forall (f:R -> R) (D:R -> Prop) (l x0:R),
440
limit1_in f D l x0 -> l <> 0 -> limit1_in (fun x:R => / f x) D (/ l) x0.
442
unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *;
443
unfold R_dist in |- *; intros; elim (H (Rabs l / 2)).
444
intros delta1 H2; elim (H (eps * (Rsqr l / 2))).
445
intros delta2 H3; elim H2; elim H3; intros; exists (Rmin delta1 delta2);
447
unfold Rmin in |- *; case (Rle_dec delta1 delta2); intro; assumption.
448
intro; generalize (H5 x); clear H5; intro H5; generalize (H7 x); clear H7;
449
intro H7; intro H10; elim H10; intros; cut (D x /\ Rabs (x - x0) < delta1).
450
cut (D x /\ Rabs (x - x0) < delta2).
451
intros; generalize (H5 H11); clear H5; intro H5; generalize (H7 H12);
452
clear H7; intro H7; generalize (Rabs_triang_inv l (f x));
453
intro; rewrite Rabs_minus_sym in H7;
455
(Rle_lt_trans (Rabs l - Rabs (f x)) (Rabs (l - f x)) (Rabs l / 2) H13 H7);
458
(Rplus_lt_compat_l (Rabs (f x) - Rabs l / 2) (Rabs l - Rabs (f x))
460
replace (Rabs (f x) - Rabs l / 2 + (Rabs l - Rabs (f x))) with (Rabs l / 2).
461
unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l;
462
rewrite Rplus_0_r; intro; cut (f x <> 0).
463
intro; replace (/ f x + - / l) with ((l - f x) * / (l * f x)).
464
rewrite Rabs_mult; rewrite Rabs_Rinv.
465
cut (/ Rabs (l * f x) < 2 / Rsqr l).
466
intro; rewrite Rabs_minus_sym in H5; cut (0 <= / Rabs (l * f x)).
469
(Rmult_le_0_lt_compat (Rabs (l - f x)) (eps * (Rsqr l / 2))
470
(/ Rabs (l * f x)) (2 / Rsqr l) (Rabs_pos (l - f x)) H18 H5 H17);
471
replace (eps * (Rsqr l / 2) * (2 / Rsqr l)) with eps.
473
unfold Rdiv in |- *; unfold Rsqr in |- *; rewrite Rinv_mult_distr.
474
repeat rewrite Rmult_assoc.
475
rewrite (Rmult_comm l).
476
repeat rewrite Rmult_assoc.
477
rewrite <- Rinv_l_sym.
479
rewrite (Rmult_comm l).
480
repeat rewrite Rmult_assoc.
481
rewrite <- Rinv_l_sym.
483
rewrite <- Rinv_l_sym.
484
rewrite Rmult_1_r; reflexivity.
490
left; apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply prod_neq_R0;
492
rewrite Rmult_comm; rewrite Rabs_mult; rewrite Rinv_mult_distr.
493
rewrite (Rsqr_abs l); unfold Rsqr in |- *; unfold Rdiv in |- *;
494
rewrite Rinv_mult_distr.
495
repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r.
496
apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption.
497
apply Rmult_lt_reg_l with (Rabs (f x) * Rabs l * / 2).
498
repeat apply Rmult_lt_0_compat.
499
apply Rabs_pos_lt; assumption.
500
apply Rabs_pos_lt; assumption.
501
apply Rinv_0_lt_compat; cut (0%nat <> 2%nat);
502
[ intro H17; generalize (lt_INR_0 2 (neq_O_lt 2 H17)); unfold INR in |- *;
503
intro H18; assumption
505
replace (Rabs (f x) * Rabs l * / 2 * / Rabs (f x)) with (Rabs l / 2).
506
replace (Rabs (f x) * Rabs l * / 2 * (2 * / Rabs l)) with (Rabs (f x)).
508
repeat rewrite Rmult_assoc.
509
rewrite (Rmult_comm (Rabs l)).
510
repeat rewrite Rmult_assoc.
511
rewrite <- Rinv_l_sym.
513
rewrite <- Rinv_l_sym.
514
rewrite Rmult_1_r; reflexivity.
519
repeat rewrite Rmult_assoc.
520
rewrite (Rmult_comm (Rabs (f x))).
521
repeat rewrite Rmult_assoc.
522
rewrite <- Rinv_l_sym.
525
apply Rabs_no_R0; assumption.
526
apply Rabs_no_R0; assumption.
527
apply Rabs_no_R0; assumption.
528
apply Rabs_no_R0; assumption.
529
apply Rabs_no_R0; assumption.
530
apply prod_neq_R0; assumption.
531
rewrite (Rinv_mult_distr _ _ H0 H16).
532
unfold Rminus in |- *; rewrite Rmult_plus_distr_r.
533
rewrite <- Rmult_assoc.
534
rewrite <- Rinv_r_sym.
536
rewrite Ropp_mult_distr_l_reverse.
537
rewrite (Rmult_comm (f x)).
539
rewrite <- Rinv_l_sym.
544
red in |- *; intro; rewrite H16 in H15; rewrite Rabs_R0 in H15;
545
cut (0 < Rabs l / 2).
546
intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (Rabs l / 2) 0 H17 H15)).
547
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
548
apply Rabs_pos_lt; assumption.
549
apply Rinv_0_lt_compat; cut (0%nat <> 2%nat);
550
[ intro H17; generalize (lt_INR_0 2 (neq_O_lt 2 H17)); unfold INR in |- *;
553
pattern (Rabs l) at 3 in |- *; rewrite double_var.
557
| apply Rlt_le_trans with (Rmin delta1 delta2);
558
[ assumption | apply Rmin_r ] ].
561
| apply Rlt_le_trans with (Rmin delta1 delta2);
562
[ assumption | apply Rmin_l ] ].
563
change (0 < eps * (Rsqr l / 2)) in |- *; unfold Rdiv in |- *;
564
repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat.
566
apply Rmult_lt_0_compat. apply Rsqr_pos_lt; assumption.
567
apply Rinv_0_lt_compat; cut (0%nat <> 2%nat);
568
[ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *;
571
change (0 < Rabs l / 2) in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat;
572
[ apply Rabs_pos_lt; assumption
573
| apply Rinv_0_lt_compat; cut (0%nat <> 2%nat);
574
[ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *;
added
removed
theories/Reals/Rlimit.v
