Library Coq.Reals.Rlimit
Definition of the limit
Require Import Rbase.
Require Import Rfunctions.
Require Import Lra.
Local Open Scope R_scope.
Lemma eps2_Rgt_R0 :
forall eps:
R,
eps > 0
-> eps * / 2
> 0.
Lemma eps2 :
forall eps:
R,
eps * / 2
+ eps * / 2
= eps.
Lemma eps4 :
forall eps:
R,
eps * / (2
+ 2
) + eps * / (2
+ 2
) = eps * / 2.
Lemma Rlt_eps2_eps :
forall eps:
R,
eps > 0
-> eps * / 2
< eps.
Lemma Rlt_eps4_eps :
forall eps:
R,
eps > 0
-> eps * / (2
+ 2
) < eps.
Lemma prop_eps :
forall r:
R,
(forall eps:
R,
eps > 0
-> r < eps) -> r <= 0.
Definition mul_factor (
l l':
R) :=
/ (1
+ (Rabs l + Rabs l')).
Lemma mul_factor_wd :
forall l l':
R, 1
+ (Rabs l + Rabs l') <> 0.
Lemma mul_factor_gt :
forall eps l l':
R,
eps > 0
-> eps * mul_factor l l' > 0.
Lemma mul_factor_gt_f :
forall eps l l':
R,
eps > 0
-> Rmin 1 (
eps * mul_factor l l')
> 0.
Definition Dgf (
Df Dg:
R -> Prop) (
f:
R -> R) (
x:
R) :=
Df x /\ Dg (
f x).
Definition limit1_in (
f:
R -> R) (
D:
R -> Prop) (
l x0:
R) :
Prop :=
limit_in R_met R_met f D x0 l.
Lemma tech_limit :
forall (
f:
R -> R) (
D:
R -> Prop) (
l x0:
R),
D x0 -> limit1_in f D l x0 -> l = f x0.
Lemma tech_limit_contr :
forall (
f:
R -> R) (
D:
R -> Prop) (
l x0:
R),
D x0 -> l <> f x0 -> ~ limit1_in f D l x0.
Lemma lim_x :
forall (
D:
R -> Prop) (
x0:
R),
limit1_in (
fun x:
R =>
x)
D x0 x0.
Lemma limit_plus :
forall (
f g:
R -> R) (
D:
R -> Prop) (
l l' x0:
R),
limit1_in f D l x0 ->
limit1_in g D l' x0 -> limit1_in (
fun x:
R =>
f x + g x)
D (
l + l')
x0.
Lemma limit_Ropp :
forall (
f:
R -> R) (
D:
R -> Prop) (
l x0:
R),
limit1_in f D l x0 -> limit1_in (
fun x:
R =>
- f x)
D (
- l)
x0.
Lemma limit_minus :
forall (
f g:
R -> R) (
D:
R -> Prop) (
l l' x0:
R),
limit1_in f D l x0 ->
limit1_in g D l' x0 -> limit1_in (
fun x:
R =>
f x - g x)
D (
l - l')
x0.
Lemma limit_free :
forall (
f:
R -> R) (
D:
R -> Prop) (
x x0:
R),
limit1_in (
fun h:
R =>
f x)
D (
f x)
x0.
Lemma limit_mul :
forall (
f g:
R -> R) (
D:
R -> Prop) (
l l' x0:
R),
limit1_in f D l x0 ->
limit1_in g D l' x0 -> limit1_in (
fun x:
R =>
f x * g x)
D (
l * l')
x0.
Definition adhDa (
D:
R -> Prop) (
a:
R) :
Prop :=
forall alp:
R,
alp > 0
-> exists x :
R, D x /\ R_dist x a < alp.
Lemma single_limit :
forall (
f:
R -> R) (
D:
R -> Prop) (
l l' x0:
R),
adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'.
Lemma limit_comp :
forall (
f g:
R -> R) (
Df Dg:
R -> Prop) (
l l' x0:
R),
limit1_in f Df l x0 ->
limit1_in g Dg l' l -> limit1_in (
fun x:
R =>
g (
f x)) (
Dgf Df Dg f)
l' x0.
Lemma limit_inv :
forall (
f:
R -> R) (
D:
R -> Prop) (
l x0:
R),
limit1_in f D l x0 -> l <> 0
-> limit1_in (
fun x:
R =>
/ f x)
D (
/ l)
x0.