Sup for Step Functions on Q.

Definition StepQSup : (StepQ)->Q := StepFfold (fun x => x) (fun b (x y:QS) => Qmax x y)%Q.

The Sup of the glue of two step functions.
Lemma StepQSup_glue : forall o s t, (StepQSup (glue o s t) = Qmax (StepQSup s) (StepQSup t))%Q.

The sup of the split of a step function.
Lemma StepQSupSplit : forall (o:OpenUnit) x,
 (StepQSup x == Qmax (StepQSup (SplitL x o)) (StepQSup (SplitR x o)))%Q.
How the sup interacts with various arithmetic operations on step functions.
Lemma StepQSup_resp_le : forall x y, x <= y -> (StepQSup x <= StepQSup y)%Q.

Lemma StepQSup_plus : forall x y, (StepQSup (x + y) <= StepQSup x + StepQSup y )%Q.

The Linf metric on step function over Q.
Definition LinfStepQ : MetricSpace := StepFSup Q_as_MetricSpace.

Definition LinfStepQPrelengthSpace := StepFSupPrelengthSpace QPrelengthSpace.

Sup is uniformly continuous.
Lemma sup_uc_prf : is_UniformlyContinuousFunction (StepQSup:LinfStepQ -> Q) Qpos2QposInf.


Definition StepQSup_uc : LinfStepQ --> Q_as_MetricSpace
:= Build_UniformlyContinuousFunction sup_uc_prf.

There is an injection from Linf to L1.
Lemma LinfAsL1_uc_prf : is_UniformlyContinuousFunction (fun (x:LinfStepQ) => (x:L1StepQ)) Qpos2QposInf.

Definition LinfAsL1 : LinfStepQ --> L1StepQ
:= Build_UniformlyContinuousFunction LinfAsL1_uc_prf.