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

Record UniformlyContinuousFunction : Type :=
{ucFun :> X -> Y
;mu : Qpos -> QposInf
;uc_prf : is_UniformlyContinuousFunction ucFun mu
}.

Given a uniformly continuous function with a modulus mu, it is also uniformly continuous with any smaller modulus

Lemma uc_prf_smaller : forall (f:UniformlyContinuousFunction) (mu2 : Qpos -> QposInf),
(forall e, QposInf_le (mu2 e) (mu f e)) ->
is_UniformlyContinuousFunction (ucFun f) mu2.

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.

Lemma uc_id_prf (X:MetricSpace) : is_UniformlyContinuousFunction (fun (x:X) => x) Qpos2QposInf.

Definition uc_id (X:MetricSpace) : UniformlyContinuousFunction X X :=
Build_UniformlyContinuousFunction (uc_id_prf X).

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