CoRN.metric2.UniformContinuity

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

Set Implicit Arguments.

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 : ∀ (X:MetricSpace) (e d:QposInf) (a b:X), QposInf_le e d → ball_ex e a b → ball_ex d a b.
Proof.
intros X e d a b Hed Hab.
destruct d as [d|]; destruct e as [e|].
    eapply (ball_weak_le X).
     apply Hed.
    assumption.
   elim Hed.
  constructor.
assumption.
Qed.

Lemma ball_ex_dec : ∀ (X:MetricSpace), (∀ e (a b:X), {ball e a b }+{¬ball e a b }) → ∀ e (a b:X), {ball_ex e a b }+{¬ball_ex e a b }.
Proof.
intros X ball_dec e a b.
destruct e as [e|].
  apply (ball_dec e a b).
simpl.
auto.
Defined.

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) :=
∀ 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 : ∀ (f1 f2:X → Y) (mu1 mu2: Qpos → QposInf),
(∀ x, st_eq (f1 x) (f2 x)) →
(∀ x, QposInf_le (mu2 x) (mu1 x)) →
(is_UniformlyContinuousFunction f1 mu1) →
(is_UniformlyContinuousFunction f2 mu2).
Proof.
intros f1 f2 mu1 mu2 Hf Hmu H e a b Hab.
do 2 rewrite <- Hf.
apply H.
eapply ball_ex_weak_le.
apply Hmu.
assumption.
Qed.

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 : ∀ (f:UniformlyContinuousFunction) (mu2 : Qpos → QposInf),
(∀ e, QposInf_le (mu2 e) (mu f e)) →
is_UniformlyContinuousFunction (ucFun f) mu2.
Proof.
intros f my2 H.
eapply is_UniformlyContinuousFunction_wd.
intros; reflexivity.
apply H.
apply uc_prf.
Qed.

The metric space of uniformly continuous functions

The space of uniformly continuous functions from a metric space

Definition ucEq (f g : UniformlyContinuousFunction) :=
∀ x, st_eq (f x) (g x).

Lemma uc_setoid : Setoid_Theory UniformlyContinuousFunction ucEq.
Proof.
constructor.
   intros x a.
   reflexivity.
  intros x y H a.
  symmetry.
  apply H.
intros x y z H1 H2 a.
transitivity (y a).
  apply H1.
apply H2.
Qed.

Definition uc_Setoid : RSetoid := (Build_RSetoid uc_setoid).

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

Lemma uc_is_MetricSpace : is_MetricSpace uc_Setoid ucBall.
Proof.
constructor.
     firstorder using ball_refl.
    firstorder using ball_sym.
   intros e1 e2 f g h H1 H2 a.
   apply ball_triangle with (g a); auto.
  intros e f g H a.
  apply ball_closed.
  firstorder.
intros f g H a.
apply ball_eq.
firstorder.
Qed.

Lemma ucBall_wd : ∀ (e1 e2:Qpos), (QposEq e1 e2) →
            ∀ (x1 x2 : uc_Setoid), (st_eq x1 x2) →
            ∀ (y1 y2 : uc_Setoid), (st_eq y1 y2) →
            (ucBall e1 x1 y1 ↔ ucBall e2 x2 y2).
Proof.
intros.
unfold ucEq in ×.
unfold ucBall in ×.
simpl in H0, H1.
unfold ucEq in H0, H1.
split.
  intros.
  rewrite <- H.
  rewrite <- H0.
  rewrite <- H1.
  auto.
intros.
rewrite → H.
rewrite → H0.
rewrite → H1.
auto.
Qed.

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).
Proof with auto.
intros.
destruct e...
simpl in ×.
apply uc_prf.
assumption.
Qed.

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.
Proof.
intros e a b Hab.
assumption.
Qed.

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)).
Proof.
revert g f.
intros [g mu_g Hg] [f mu_f Hf] e a b Hab.
unfold is_UniformlyContinuousFunction in ×.
simpl in ×.
apply Hg.
clear Hg.
destruct (mu_g e) as [mge|]; firstorder.
Qed.

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 : ∀ X Y Z (f:Y -->Z),
is_UniformlyContinuousFunction (@uc_compose X Y Z f) (mu f).
Proof.
intros X Y Z f e x y Hxy z.
simpl.
simpl in Hxy.
apply uc_prf.
destruct (mu f e); auto.
apply Hxy.
Qed.

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 : ∀ X Y Z,
is_UniformlyContinuousFunction (@uc_compose_uc0 X Y Z) Qpos2QposInf.
Proof.
intros X Y Z e x y Hxy z z0.
simpl.
apply Hxy.
Qed.

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