Complete metric space

Section RegularFunction.

Variable X:MetricSpace.

Regular functions

A regular function is one way of representing elements in a complete metric space. A regular function that take a given error e, and returns an approximation within e of the value it is representing. These approximations must be coherent and the definition belows state this property.

Definition is_RegularFunction (x:QposInf -> X) : Prop :=
 forall (e1 e2:Qpos), ball (m:=X) (e1+e2) (x e1) (x e2).

A regular function consists of an approximation function, and a proof that the approximations are coherent.
Record RegularFunction : Type :=
{approximate : Q+∞ -> X
;regFun_prf : is_RegularFunction approximate
}.
Regular functions form a metric space
Definition regFunEq (f g : RegularFunction) :=
 forall e1 e2, ball (m:=X) (e1+e2) (approximate f e1) (approximate g e2).

Lemma regFunEq_e : forall (f g : RegularFunction), (forall e, ball (m:=X) (e+e) (approximate f e) (approximate g e)) -> (regFunEq f g).

Lemma regFunEq_e_small : forall (f g : RegularFunction) (E:Qpos), (forall (e:Qpos), e <= E -> ball (m:=X) (e+e) (approximate f e) (approximate g e)) -> (regFunEq f g).

Lemma regFun_is_setoid : Setoid_Theory RegularFunction regFunEq.

Definition regFun_Setoid := Build_Setoid regFun_is_setoid.

Definition regFunBall e (f g : RegularFunction) :=
forall d1 d2, ball (m:=X) (d1+e+d2)%Qpos (approximate f d1) (approximate g d2).

Lemma regFunBall_wd : forall (e1 e2:Qpos), (QposEq e1 e2) ->
            forall (x1 x2 : regFun_Setoid), (st_eq x1 x2) ->
            forall (y1 y2 : regFun_Setoid), (st_eq y1 y2) ->
            (regFunBall e1 x1 y1 <-> regFunBall e2 x2 y2).


Lemma regFun_is_MetricSpace : is_MetricSpace regFun_Setoid regFunBall.

We define the completion of a metric space to be the space of regular functions
Definition Complete : MetricSpace :=
Build_MetricSpace regFunBall_wd regFun_is_MetricSpace.

The ball of regular functions is related to the underlying ball in ways that you would expect.
Lemma regFunBall_ball : forall (x y:Complete) (e0 e1 e2:Qpos), ball e0 (approximate x e1) (approximate y e2) -> ball (e1 + e0 + e2) x y.

Lemma regFunBall_e : forall (x y:Complete) e, (forall d, ball (d + e + d) (approximate x d) (approximate y d)) -> ball e x y.

Cunit

There is an injection from the original space to the complete space given by the constant regular function.
Lemma Cunit_fun_prf (x:X) : is_RegularFunction (fun _ => x).

Definition Cunit_fun (x:X) : Complete :=
Build_RegularFunction (Cunit_fun_prf x).

Lemma Cunit_prf : is_UniformlyContinuousFunction Cunit_fun Qpos2QposInf.

Definition Cunit : X --> Complete :=
Build_UniformlyContinuousFunction Cunit_prf.

This injection preserves the metric
Lemma ball_Cunit : forall e a b, ball e (Cunit a) (Cunit b) <-> ball e a b.

Lemma Cunit_eq : forall a b, st_eq (Cunit a) (Cunit b) <-> st_eq a b.

Lemma ball_approx_r : forall (x:Complete) e, ball e x (Cunit (approximate x e)).

Lemma ball_approx_l : forall (x:Complete) e, ball e (Cunit (approximate x e)) x.

Lemma ball_ex_approx_r : forall (x:Complete) e, ball_ex e x (Cunit (approximate x e)).

Lemma ball_ex_approx_l : forall (x:Complete) e, ball_ex e (Cunit (approximate x e)) x.

Lemma regFun_prf_ex :
 forall (r : Complete) (e1 e2 : Q+∞),
  ball_ex (e1 + e2) (approximate r e1) (approximate r e2).

End RegularFunction.


Section Faster.

Variable X : MetricSpace.
Variable x : Complete X.

A regular function is equivalent to the same function that returns a better approximation with a given error. One would not generally want to do this when doing computation; however it is quite a useful substitution to be able to make during reasoning.

Section FasterInGeneral.

Variable f : Q+ -> Q+.
Hypothesis Hf : forall x, (f x) <= x.

Lemma fasterIsRegular : is_RegularFunction (fun e => (approximate x (QposInf_bind f e))).

Definition faster : Complete X := Build_RegularFunction fasterIsRegular.

Lemma fasterIsEq : st_eq faster x.

End FasterInGeneral.

Lemma QreduceApprox_prf : forall (e:Qpos), QposRed e <= e.

Definition QreduceApprox := faster QposRed QreduceApprox_prf.

Lemma QreduceApprox_Eq : st_eq QreduceApprox x.
In particular, halving the error of the approximation is a common case.
Lemma doubleSpeed_prf : forall (e:Qpos), ((1#2)*e)%Qpos <= e.

Definition doubleSpeed := faster (Qpos_mult (1#2)) doubleSpeed_prf.

Lemma doubleSpeed_Eq : st_eq doubleSpeed x.

End Faster.

Section Cjoin.

Variable X : MetricSpace.

Cjoin

There is an injection from a twice completed space into a once completed space. This injection along with Cunit forms an isomorphism between a twice completed space and a once completed space. This proves that a complete metric space is complete.
Definition Cjoin_raw (x:Complete (Complete X)) (e:QposInf) :=
(approximate (approximate x (QposInf_mult (1#2) e)) (QposInf_mult (1#2) e))%Qpos.

Lemma Cjoin_fun_prf (x:Complete (Complete X)) : is_RegularFunction (Cjoin_raw x).

Definition Cjoin_fun (x:Complete (Complete X)) : Complete X :=
Build_RegularFunction (Cjoin_fun_prf x).

Lemma Cjoin_prf : is_UniformlyContinuousFunction Cjoin_fun Qpos2QposInf.

Definition Cjoin : (Complete (Complete X)) --> (Complete X) :=
Build_UniformlyContinuousFunction Cjoin_prf.

End Cjoin.


Section Cmap.

Variable X Y : MetricSpace.
Variable f : X --> Y.

Cmap (slow)

Uniformly continuous functions can be lifted to the completion of metric spaces. A faster version that works under some mild assumptions will be given later. But first the most generic version that we call Cmap_slow.

Definition Cmap_slow_raw (x:Complete X) (e:QposInf) :=
f (approximate x (QposInf_mult (1#2)%Qpos (QposInf_bind (mu f) e))).

Lemma Cmap_slow_raw_strongInf : forall (x:Complete X) (d:QposInf) (e:QposInf), QposInf_le d (QposInf_mult (1#2)%Qpos (QposInf_bind (mu f) e)) ->
ball_ex e (f (approximate x d)) (Cmap_slow_raw x e).

Lemma Cmap_slow_raw_strong : forall (x:Complete X) (d:QposInf) (e:Qpos), QposInf_le d (QposInf_mult (1#2)%Qpos (mu f e)) ->
ball e (f (approximate x d)) (Cmap_slow_raw x e).

Lemma Cmap_slow_fun_prf (x:Complete X) : is_RegularFunction (Cmap_slow_raw x).

Definition Cmap_slow_fun (x:Complete X) : Complete Y :=
Build_RegularFunction (Cmap_slow_fun_prf x).

Definition Cmap_slow_prf : is_UniformlyContinuousFunction Cmap_slow_fun (fun e => (QposInf_mult (1#2)(mu f e))%Qpos).

Definition Cmap_slow : (Complete X) --> (Complete Y) :=
Build_UniformlyContinuousFunction Cmap_slow_prf.

End Cmap.

Cbind can be defined in terms of map and join
Definition Cbind_slow (X Y:MetricSpace) (f:X-->Complete Y) := uc_compose Cjoin (Cmap_slow f).

The completion operation, along with the map functor from a monad in the catagory of metric spaces.
Section Monad_Laws.

Variable X Y Z : MetricSpace.

Notation "a =m b" := (st_eq a b) (at level 70, no associativity).

Lemma MonadLaw1 : forall a, Cmap_slow_fun (uc_id X) a =m a.

Lemma MonadLaw2 : forall (f:Y --> Z) (g:X --> Y) a, Cmap_slow_fun (uc_compose f g) a =m (Cmap_slow_fun f (Cmap_slow_fun g a)).

Lemma MonadLaw3 : forall (f:X --> Y) a, (Cmap_slow_fun f (Cunit_fun _ a)) =m (Cunit_fun _ (f a)).

Lemma MonadLaw4 : forall (f:X --> Y) a, (Cmap_slow_fun f (Cjoin_fun a)) =m (Cjoin_fun ((Cmap_slow_fun (Cmap_slow f)) a)).

Lemma MonadLaw5 : forall a, (Cjoin_fun (X:=X) (Cunit_fun _ a)) =m a.

Lemma MonadLaw6 : forall a, Cjoin_fun ((Cmap_slow_fun (X:=X) Cunit) a) =m a.

Lemma MonadLaw7 : forall a, Cjoin_fun ((Cmap_slow_fun (X:=Complete (Complete X)) Cjoin) a) =m Cjoin_fun (Cjoin_fun a).

This final law isn't a monad law, rather it completes the isomorphism between a twice completed metric space and a one completed metric space.
Lemma CunitCjoin : forall a, (Cunit_fun _ (Cjoin_fun (X:=X) a)) =m a.

End Monad_Laws.

The monad laws are sometimes expressed in terms of bind and unit.
Lemma BindLaw1 : forall X Y (f:X--> Complete Y) a, (st_eq (Cbind_slow f (Cunit_fun _ a)) (f a)).

Lemma BindLaw2 : forall X a, (st_eq (Cbind_slow (Cunit:X --> Complete X) a) a).

Lemma BindLaw3 : forall X Y Z (a:Complete X) (f:X --> Complete Y) (g:Y-->Complete Z), (st_eq (Cbind_slow g (Cbind_slow f a)) (Cbind_slow (uc_compose (Cbind_slow g) f) a)).

Strong Monad

The monad is a strong monad because the map function itself is a uniformly continuous function.
Section Strong_Monad.

Variable X Y : MetricSpace.
Let X_Y := UniformlyContinuousSpace X Y.
Let CX_CY := UniformlyContinuousSpace (Complete X) (Complete Y).

Lemma Cmap_strong_slow_prf : is_UniformlyContinuousFunction ((Cmap_slow (Y:=Y)):(X_Y -> CX_CY)) Qpos2QposInf.

Definition Cmap_strong_slow : (X --> Y) --> (Complete X --> Complete Y) :=
Build_UniformlyContinuousFunction Cmap_strong_slow_prf.

Using strength we can show that Complete forms an applicative functor. The ap function is useful for making multiple argument maps.
Definition Cap_slow_raw (f:Complete (X --> Y)) (x:Complete X) (e:QposInf) :=
 approximate (Cmap_slow (approximate f ((1#2)%Qpos*e)%QposInf) x) ((1#2)%Qpos*e)%QposInf.

Lemma Cap_slow_fun_prf (f:Complete (X --> Y)) (x:Complete X) : is_RegularFunction (Cap_slow_raw f x).

Definition Cap_slow_fun (f:Complete (X --> Y)) (x:Complete X) : Complete Y :=
Build_RegularFunction (Cap_slow_fun_prf f x).

Lemma Cap_slow_help (f:Complete (X --> Y)) (x:Complete X) (e:Qpos) :
 ball e (Cap_slow_fun f x) (Cmap_slow (approximate f e) x).

Definition Cap_slow_modulus (f:Complete (X --> Y)) (e:Qpos) : Q+∞ := ((1#2)%Qpos*(mu (approximate f ((1#3)*e)%Qpos) ((1#3)*e)))%QposInf.

Lemma Cap_weak_slow_prf (f:Complete (X --> Y)) : is_UniformlyContinuousFunction (Cap_slow_fun f) (Cap_slow_modulus f).

Definition Cap_weak_slow (f:Complete (X --> Y)) : Complete X --> Complete Y :=
Build_UniformlyContinuousFunction (Cap_weak_slow_prf f).

Lemma Cap_slow_prf : is_UniformlyContinuousFunction Cap_weak_slow Qpos2QposInf.

Definition Cap_slow : Complete (X --> Y) --> Complete X --> Complete Y :=
Build_UniformlyContinuousFunction Cap_slow_prf.

Lemma StrongMonadLaw1 : forall a b, st_eq (Cap_slow_fun (Cunit_fun _ a) b) (Cmap_strong_slow a b).

End Strong_Monad.


A binary version of map
Definition Cmap2_slow (X Y Z:MetricSpace) (f:X --> Y --> Z) := uc_compose (@Cap_slow Y Z) (Cmap_slow f).

Completion and Classification

The completion operations preserve stability and locatedness, but it does not preserve the decidability.
Lemma Complete_stable : forall X, stableMetric X -> stableMetric (Complete X).

Lemma Complete_located : forall X, locatedMetric X -> locatedMetric (Complete X).