# CoRN.metric2.UniformContinuity

Require Export Metric.
Require Export QposInf.
Require Import List.
Require Import CornTac.

This extended notition of ball operates over QposInf, allowing one to say, ball Infinity a b, holds for all a and b.

Definition ball_ex (X: MetricSpace) (e: QposInf): X -> X -> Prop :=
match e with
| Qpos2QposInf e' => ball e'
| QposInfinity => fun a b => True
end.
Lemma ball_ex_weak_le : forall (X:MetricSpace) (e d:QposInf) (a b:X), QposInf_le e d -> ball_ex e a b -> ball_ex d a b.

Lemma ball_ex_dec : forall (X:MetricSpace), (forall e (a b:X), {ball e a b}+{~ball e a b}) -> forall e (a b:X), {ball_ex e a b}+{~ball_ex e a b}.

Section UniformlyContinuousFunction.

## Uniform Continuity

Variable X Y : MetricSpace.

This is the traditional definitition of uniform continuity with an explicitly given modulus of continuity
Definition is_UniformlyContinuousFunction
(f: X -> Y) (mu: Qpos -> QposInf) :=
forall e a b, ball_ex (mu e) a b -> ball e (f a) (f b).

Every uniformly continuous function is automatically well defined
Lemma is_UniformlyContinuousFunction_wd : forall (f1 f2:X -> Y) (mu1 mu2: Qpos -> QposInf),
(forall x, st_eq (f1 x) (f2 x)) ->
(forall x, QposInf_le (mu2 x) (mu1 x)) ->
(is_UniformlyContinuousFunction f1 mu1) ->
(is_UniformlyContinuousFunction f2 mu2).

A uniformly continuous function consists of a function, a modulus of continuity, and a proof that the function is uniformly continuous with that modulus
Given a uniformly continuous function with a modulus mu, it is also uniformly continuous with any smaller modulus

### The metric space of uniformly continuous functions

The space of uniformly continuous functions from a metric space
Definition ucEq (f g : UniformlyContinuousFunction) :=
forall x, st_eq (f x) (g x).

Lemma uc_setoid : Setoid_Theory UniformlyContinuousFunction ucEq.

Definition uc_Setoid : RSetoid := (Build_RSetoid uc_setoid).

Definition ucBall e (f g : UniformlyContinuousFunction) := forall a, ball e (f a) (g a).

Lemma uc_is_MetricSpace : is_MetricSpace uc_Setoid ucBall.

Lemma ucBall_wd : forall (e1 e2:Qpos), (QposEq e1 e2) ->
forall (x1 x2 : uc_Setoid), (st_eq x1 x2) ->
forall (y1 y2 : uc_Setoid), (st_eq y1 y2) ->
(ucBall e1 x1 y1 <-> ucBall e2 x2 y2).

mu_ex generalizes mu analogous to how ball_ex generalizes ball:

Definition mu_ex (f: UniformlyContinuousFunction) (e: QposInf): QposInf :=
match e with
| Qpos2QposInf e' => mu f e'
| QposInfinity => QposInfinity
end.

Lemma uc_ex_prf (u: UniformlyContinuousFunction) (e: QposInf) (a b: X):
ball_ex (mu_ex u e) a b -> ball_ex e (ucFun u a) (ucFun u b).

End UniformlyContinuousFunction.

Definition UniformlyContinuousSpace (X Y:MetricSpace) : MetricSpace :=
Build_MetricSpace (@ucBall_wd X Y) (@uc_is_MetricSpace X Y).

Notation "x --> y" := (UniformlyContinuousSpace x y) (at level 55, right associativity) : uc_scope.

Open Local Scope uc_scope.

### The category of metric spaces.

Metric spaces with uniformly continuous functions form a category.
The identity function is uniformly continuous.
The composition of two uniformly continuous functions is uniformly continuous
Lemma uc_compose_prf (X Y Z:MetricSpace) (g: Y --> Z) (f:X --> Y) :
is_UniformlyContinuousFunction (fun x => g (f x)) (fun e => QposInf_bind (mu f) (mu g e)).

Definition uc_compose (X Y Z:MetricSpace) (g: Y --> Z) (f:X --> Y) : X --> Z :=
Build_UniformlyContinuousFunction (uc_compose_prf g f).

Notation "f ∘ g" := (uc_compose f g) (at level 40, left associativity) : uc_scope.

Lemma is_uc_uc_compose0 : forall X Y Z (f:Y-->Z),
is_UniformlyContinuousFunction (@uc_compose X Y Z f) (mu f).

Definition uc_compose_uc0 X Y Z (f:Y-->Z) : (X-->Y) --> X --> Z :=
Build_UniformlyContinuousFunction (is_uc_uc_compose0 f).

Lemma is_uc_uc_compose : forall X Y Z,
is_UniformlyContinuousFunction (@uc_compose_uc0 X Y Z) Qpos2QposInf.

Definition uc_compose_uc X Y Z : (Y-->Z)-->(X-->Y)-->X-->Z :=
Build_UniformlyContinuousFunction (@is_uc_uc_compose X Y Z).