L1 metric for Step Functions

The L1 metric is measured by the integral of the absolute value of the difference between step functions.

Integeral for Step Functions.

Definition IntegralQ:(StepQ)->Q:=(StepFfold (fun x => x) (fun b (x y:QS) => (Qred (affineCombo b x y:QS))))%Q.
Definition L1Norm(f:StepF QS):Q:=(IntegralQ (StepQabs f)).
Definition L1Distance(f g:StepF QS):Q:=(L1Norm (f - g)).
Definition L1Ball (e:Qpos)(f g:StepF QS):Prop:=((L1Distance f g)<=e)%Q.


Lemma L1ball_dec : forall e a b, {L1Ball e a b}+{~L1Ball e a b}.



The integral of the glue of two step functions.
Lemma Integral_glue : forall o s t, (IntegralQ (glue o s t) == o*(IntegralQ s) + (1-o)*(IntegralQ t))%Q.

The integral of the split of a step function.
Lemma IntegralSplit : forall (o:OpenUnit) x,
 (IntegralQ x ==
 affineCombo o (IntegralQ (SplitL x o)) (IntegralQ (SplitR x o)))%Q.




How the intergral intreacts with arithemetic functions on step functions.
Lemma Integral_plus:forall s t,
  ((IntegralQ s)+(IntegralQ t)==(IntegralQ (s + t)))%Q.

Lemma Integral_opp:forall s,
  (-(IntegralQ s)==(IntegralQ (- s)))%Q.

Lemma Integral_minus:forall s t,
  ((IntegralQ s)-(IntegralQ t)==(IntegralQ (s - t)))%Q.

Lemma Integral_scale :forall q x,
 (q*(IntegralQ x) == (IntegralQ (QscaleS q^@>x)))%Q.

Lemma Abs_Integral : forall x,
 (Qabs (IntegralQ x) <= IntegralQ (QabsS ^@> x))%Q.

Lemma Abs_Integral_Norm : forall x,
 (Qabs (IntegralQ x) <= L1Norm x)%Q.

The integral of a nonnegative function is nonnegative.
Lemma Integral_resp_nonneg :forall x,
 (constStepF (0:QS)) <= x -> (0 <= (IntegralQ x))%Q.

Lemma Integral_resp_le :forall x y,
 x <= y -> (IntegralQ x <= IntegralQ y)%Q.

Properties of the L1 norm.
Lemma L1Norm_glue : forall o s t, (L1Norm (glue o s t) == o*L1Norm s + (1-o)*L1Norm t)%Q.

Lemma L1Norm_nonneg : forall x, (0 <= (L1Norm x))%Q.

Lemma L1Norm_Zero : forall s,
 (L1Norm s <= 0)%Q -> s == (constStepF (0:QS)).

Lemma L1Norm_scale : forall q s,
 (L1Norm (QscaleS q ^@> s) == Qabs q * L1Norm s)%Q.

L1 ball has all the required properties.
Lemma L1ball_refl : forall e x, (L1Ball e x x).

Lemma L1ball_sym : forall e x y, (L1Ball e x y) -> (L1Ball e y x).

Lemma L1ball_triangle : forall e d x y z, (L1Ball e x y) -> (L1Ball d y z) -> (L1Ball (e+d) x z).

Lemma L1ball_closed : forall e x y, (forall d, (L1Ball (e+d) x y)) -> (L1Ball e x y).







Lemma L1ball_eq : forall x y, (forall e : Q+, L1Ball e x y) -> StepF_eq x y.

Definition L1S : Setoid := Build_Setoid (StepF_Sth QS).

Example of a Metric Space <StepQ, L1Ball>

Lemma L1_is_MetricSpace :
 (is_MetricSpace L1S L1Ball).
Definition L1StepQ : MetricSpace :=
@Build_MetricSpace L1S _ L1Ball_wd L1_is_MetricSpace.
The L1 metric is a prelength space.
Lemma L1StepQPrelengthSpace : PrelengthSpace L1StepQ.

Integration is uniformly continuous.
Lemma integral_uc_prf : is_UniformlyContinuousFunction IntegralQ Qpos2QposInf.


Definition IntegralQ_uc : L1StepQ --> Q_as_MetricSpace
:= Build_UniformlyContinuousFunction integral_uc_prf.