# Library Coq.Reals.Rlimit

Definition of the limit
Require Import Rbase.
Require Import Rfunctions.
Require Import Classical_Prop.
Require Import Fourier.
Open Local Scope R_scope.

# Calculus

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.

# Metric space

Record Metric_Space : Type :=
{Base : Type;
dist : Base -> Base -> R;
dist_pos : forall x y:Base, dist x y >= 0;
dist_sym : forall x y:Base, dist x y = dist y x;
dist_refl : forall x y:Base, dist x y = 0 <-> x = y;
dist_tri : forall x y z:Base, dist x y <= dist x z + dist z y}.

## Limit in Metric space

Definition limit_in (X X':Metric_Space) (f:Base X -> Base X')
(D:Base X -> Prop) (x0:Base X) (l:Base X') :=
forall eps:R,
eps > 0 ->
exists alp : R,
alp > 0 /\
(forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps).

## R is a metric space

Definition R_met : Metric_Space :=
Build_Metric_Space R R_dist R_dist_pos R_dist_sym R_dist_refl R_dist_tri.

# Limit 1 arg

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.