Section Prelength_Space.

Prelength space

In a length space the "internal" metric of a metric space corresponds to the given external metric. The internal metric of a space measures the distance between two point by the length of curves connecting them.

Because the notion of curves really only makes sense in a complete metric space, here we use a weaker notion of a prelength space. In this case the internal metric says that two points are within e of each other if you can get between the two points making arbitarily short hops while covering a distance arbitrarily close to e.
Variable X:MetricSpace.

The notion of a prelength space is neatly characterized by the following simple definition.
Definition PrelengthSpace :=
forall (a b:X) (e d1 d2:Qpos), e < d1+d2 -> ball e a b ->
exists2 c:X, ball d1 a c & ball d2 c b.

There is some evidence that we should be using the classical existential in the above definition. For now we take the middle road and use the Prop based existential. This show that the exists statement is not used in computations, but still every occurance is constructive.

Hypothesis prelength : PrelengthSpace.

This proves that you can construct a trail of points between a and b that is arbitarily close to e and with arbitrarily short hops.
Lemma trail : forall dl e (a b:X),
 ball e a b ->
 e < QposSum dl ->
 let n := length dl in
 (exists2 f : N -> X, f 0 = a /\ f n = b
               & forall i z, i < n -> ball (nth i dl z) (f i) (f (S i)))%nat.

Variable Y:MetricSpace.

The major applicaiton of prelength spaces is that it allows one to reduce the problem of ball (e1 + e2) (f a) (f b) to ball (mu f e1 + mu f e2) a b instead of reduceing it to ball (mu f (e1 + e2)) a b. This new reduction allows one to continue reasoning by making use of the triangle law.

Below we show a more general lemma allowing for arbitarily many terms in the sum.
Lemma mu_sum : forall e0 (es : list Q+) (f:UniformlyContinuousFunction X Y) a b,
ball_ex (fold_right QposInf_plus (mu f e0) (map (mu f) es)) a b ->
ball (fold_right Qpos_plus e0 es) (f a) (f b).

End Prelength_Space.

Section Map.

Variable X Y : MetricSpace.
Hypothesis plX : PrelengthSpace X.
Variable f : X --> Y.

A more effictient Cmap and Cbind

The main application of prelength spaces is to allow one to use a more natural and more efficent map function for complete metric spaces. Since this map function is more widely used in practice, it gets the name Cmap while the original map function is stuck with the name Cmap_slow as a reminder to try to use the function defined here if possible.

Definition Cmap_raw (x:Complete X) (e:QposInf) :=
f (approximate x (QposInf_bind (mu f) e)).

Lemma Cmap_fun_prf (x:Complete X) : is_RegularFunction (fun e => f (approximate x (QposInf_bind (mu f) e))).

Definition Cmap_fun (x:Complete X) : Complete Y :=
Build_RegularFunction (Cmap_fun_prf x).

Lemma Cmap_prf : is_UniformlyContinuousFunction Cmap_fun (mu f).

Definition Cmap : (Complete X) --> (Complete Y) :=
Build_UniformlyContinuousFunction Cmap_prf.

Cmap is equivalent to the original Cmap_slow
Lemma Cmap_correct : st_eq Cmap (Cmap_slow f).

Lemma Cmap_fun_correct : forall x, st_eq (Cmap_fun x) (Cmap_slow_fun f x).

End Map.


Similarly we define a new Cbind
Definition Cbind X Y plX (f:X-->Complete Y) := uc_compose Cjoin (Cmap plX f).

Lemma Cbind_correct : forall X Y plX (f:X-->Complete Y), st_eq (Cbind plX f) (Cbind_slow f).

Lemma Cbind_fun_correct : forall X Y plX (f:X-->Complete Y) x, st_eq (Cbind plX f x) (Cbind_slow f x).

Similarly we define a new Cmap_strong
Lemma Cmap_strong_prf : forall (X Y:MetricSpace) (plX:PrelengthSpace X),
 is_UniformlyContinuousFunction (@Cmap X Y plX) Qpos2QposInf.

Definition Cmap_strong X Y plX : (X --> Y) --> (Complete X --> Complete Y) :=
Build_UniformlyContinuousFunction (@Cmap_strong_prf X Y plX).

Lemma Cmap_strong_correct : forall X Y plX, st_eq (@Cmap_strong X Y plX) (@Cmap_strong_slow X Y).

Similarly we define a new Cap
Definition Cap_raw X Y plX (f:Complete (X --> Y)) (x:Complete X) (e:QposInf) :=
 approximate (Cmap plX (approximate f ((1#2)%Qpos*e)%QposInf) x) ((1#2)%Qpos*e)%QposInf.

Lemma Cap_fun_prf X Y plX (f:Complete (X --> Y)) (x:Complete X) : is_RegularFunction (Cap_raw plX f x).

Definition Cap_fun X Y plX (f:Complete (X --> Y)) (x:Complete X) : Complete Y :=
Build_RegularFunction (Cap_fun_prf plX f x).

Lemma Cap_fun_correct : forall X Y plX (f:Complete (X --> Y)) x, st_eq (Cap_fun plX f x) (Cap_slow_fun f x).

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

Lemma Cap_weak_prf X Y plX (f:Complete (X --> Y)) : is_UniformlyContinuousFunction (Cap_fun plX f) (Cap_modulus f).

Definition Cap_weak X Y plX (f:Complete (X --> Y)) : Complete X --> Complete Y :=
Build_UniformlyContinuousFunction (Cap_weak_prf plX f).

Lemma Cap_weak_correct : forall X Y plX (f:Complete (X --> Y)), st_eq (Cap_weak plX f) (Cap_weak_slow f).

Lemma Cap_prf X Y plX : is_UniformlyContinuousFunction (@Cap_weak X Y plX) Qpos2QposInf.

Definition Cap X Y plX : Complete (X --> Y) --> Complete X --> Complete Y :=
Build_UniformlyContinuousFunction (Cap_prf plX).

Lemma Cap_correct : forall X Y plX, st_eq (Cap Y plX) (Cap_slow X Y).


Similarly we define a new Cmap2.
Definition Cmap2 (X Y Z:MetricSpace) (Xpl : PrelengthSpace X) (Ypl : PrelengthSpace Y) f := uc_compose (@Cap Y Z Ypl) (Cmap Xpl f).

Completion of a metric space preserves the prelength property. In fact the completion of a prelenght space is a length space, but we have not formalized the notion of a length space yet.
Lemma CompletePL : forall X, PrelengthSpace X -> PrelengthSpace (Complete X).