Linf metric for Step Functions

The Linf metric for StepF X is obtained by lifting the ball predicate on X

Section StepFSupBall.

Variable X:MetricSpace.

A setoid verion of the ball predicate
Definition ballS0 (m : MetricSpace): Q+ -> m -> m --> iffSetoid.

Defined.

Definition ballS (m : MetricSpace): Q+ -> m --> m --> iffSetoid.

Defined.

The definition of the usp metric
Definition StepFSupBall(e:Qpos)(f:StepF X)(g:StepF X):=
StepFfoldProp ((@ballS X e)^@> f <@> g).

Lemma StepFSupBallGlueGlue : forall e o fl fr gl gr,
StepFSupBall e (glue o fl fr) (glue o gl gr) <->
StepFSupBall e fl gl /\ StepFSupBall e fr gr.

End StepFSupBall.


Add Parametric Morphism X : (@StepFSupBall X)
  with signature QposEq ==> (@StepF_eq _) ==> (@StepF_eq _) ==> iff
 as StepFSupBall_wd.
Qed.

Section SupMetric.
The StepFSupBall satifies the requirements of a metric.
Variable X : MetricSpace.

Lemma StepFSupBall_refl : forall e (x:StepF X), (StepFSupBall e x x).

Lemma StepFSupBall_sym : forall e (x y:StepF X), (StepFSupBall e x y) -> (StepFSupBall e y x).


Lemma StepFSupBall_triangle : forall e d (x y z:StepF X),
 (StepFSupBall e x y) -> (StepFSupBall d y z) -> (StepFSupBall (e+d) x z).


Lemma StepFSupBall_closed : forall e (x y:StepF X), (forall d, (StepFSupBall (e+d) x y)) -> (StepFSupBall e x y).












Lemma StepFSupBall_eq : forall (x y : StepF X),
(forall e : Q+, StepFSupBall e x y) -> StepF_eq x y.









Example of a Metric Space <Step, StepFSupBall>

Lemma StepFSupBall_is_MetricSpace :
 (is_MetricSpace (@StepFS X) (@StepFSupBall X)).

Definition StepFSup : MetricSpace :=
@Build_MetricSpace (StepFS X) _ (@StepFSupBall_wd X) StepFSupBall_is_MetricSpace.

The StepFSup is is a prelength space.
Lemma StepFSupPrelengthSpace : PrelengthSpace X -> PrelengthSpace StepFSup.

End SupMetric.


Lemma StepFSupBallBind(X:MetricSpace): ((forall (e : Q+) (a b : StepF (StepFS X)) ,
forall f:(StepFS X) -->(StepFS X),
(forall c d, (StepFSupBall e c d) -> (StepFSupBall e (f c) (f d)))->
StepFSupBall (X:=StepFSup X) e a b ->
StepFSupBall (X:=X) e (StFBind00 a f) (StFBind00 b f))).





































Section UniformlyContinuousFunctions.

Variable X Y : MetricSpace.

Various functions with step functions are uniformly continuous with this metric.
Definition StFJoinSup :(StepFSup (StepFSup X)) --> (StepFSup X).

Defined.

Definition StFReturn_uc : X --> (StepFSup X).

Defined.

Lemma uc_stdFun(X Y:MetricSpace):
(UniformlyContinuousFunction X Y) ->(extSetoid X Y).



Definition Map_uc (f:X-->Y):(StepFSup X)-->(StepFSup Y).









Defined.

Definition glue_uc0 (o:OpenUnit):
 StepFSup X -> StepFSup X --> StepFSup X.
Defined.

Definition glue_uc (o:OpenUnit):
 StepFSup X --> StepFSup X --> StepFSup X.
Defined.

There is an injection from X to StepFSup X.
Lemma constStepF_uc_prf : is_UniformlyContinuousFunction
 (@constStepF X:X -> StepFSup X) Qpos2QposInf.

Definition constStepF_uc : X --> StepFSup X
:= Build_UniformlyContinuousFunction (constStepF_uc_prf).

End UniformlyContinuousFunctions.