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.

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}.

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 /\ X.(dist) x x0 < alp -> X'.(dist) (f x) l < eps).

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

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.