CoRN.metric2.Prelength

Require Export Metric.
Require Import UniformContinuity.
Require Import Complete.
Require Import COrdFields2.
Require Import Qordfield.
Require Import QMinMax.
Require Import QposMinMax.
Require Import List.
Require Import CornTac.
Require Import Qauto.

Open Local Scope Q_scope.

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 : nat -> 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 Qpos) (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.

Open Local Scope uc_scope.
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.

Section fast_Monad_Laws.
Open Local Scope uc_scope.

Variable X Y Z : MetricSpace.
Hypothesis plX : PrelengthSpace X.
Hypothesis plY : PrelengthSpace Y.

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

Lemma fast_MonadLaw1 a : Cmap plX (uc_id X) a =m a.

Lemma fast_MonadLaw2 (f:Y --> Z) (g:X --> Y) a : Cmap plX (uc_compose f g) a =m (Cmap plY f (Cmap plX g a)).

Lemma fast_MonadLaw3 (f:X --> Y) a : Cmap plX f (Cunit a) =m Cunit (f a).

End fast_Monad_Laws.

Open Local Scope uc_scope.

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) : QposInf := (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).