CoRN.metric2.ProductMetric

Require Export Metric.
Require Import Classification.
Require Import UniformContinuity.
Require Import Prelength.
Require Import Complete.
Require Import CornTac.

Product Metric

The product of two metric spaces forms a metric space

Section ProductSetoid.

Variable X Y : RSetoid.

Definition prod_st_eq (a b:X *Y) :=
st_eq (fst a) (fst b) /\ st_eq (snd a) (snd b).

Lemma prodST : Setoid_Theory _ prod_st_eq.

Definition prodS : RSetoid := Build_RSetoid prodST.
End ProductSetoid.

Section ProductMetric.
Variable X Y : MetricSpace.

Definition prod_ball e (a b:X *Y) :=
ball e (fst a) (fst b) /\ ball e (snd a) (snd b).

Lemma prod_ball_refl : forall e a, prod_ball e a a.

Lemma prod_ball_sym : forall e a b, prod_ball e a b -> prod_ball e b a.

Lemma prod_ball_triangle : forall e1 e2 a b c, prod_ball e1 a b -> prod_ball e2 b c -> prod_ball (e1 + e2) a c.

Lemma prod_ball_closed : forall e a b, (forall d, prod_ball (e + d) a b) -> prod_ball e a b.

Lemma prod_ball_eq : forall a b, (forall e, prod_ball e a b) -> prod_st_eq _ _ a b.

Lemma prod_is_MetricSpace : is_MetricSpace (prodS X Y) prod_ball.

Definition ProductMS : MetricSpace.

Product metrics preserve properties of metric spaces such as being a prelenght space, being stable, being located, and being deciable

Lemma ProductMS_prelength : PrelengthSpace X -> PrelengthSpace Y -> PrelengthSpace ProductMS.

Lemma ProductMS_stable : stableMetric X -> stableMetric Y -> stableMetric ProductMS.

Furthermore, if a product space is stable, then the components are stable (assuming the components are non-zero).

Lemma ProductMS_stableX : Y -> stableMetric ProductMS -> stableMetric X.

Lemma ProductMS_stableY : X -> stableMetric ProductMS -> stableMetric Y.

Lemma ProductMS_located : locatedMetric X -> locatedMetric Y -> locatedMetric ProductMS.

Lemma ProductMS_decidable : decidableMetric X -> decidableMetric Y -> decidableMetric ProductMS.

This defines a pairing function with types of a metric space

Definition PairMS (x:X) (y:Y) : ProductMS := (x ,y ).

End ProductMetric.
Open Local Scope uc_scope.

together forms the tensor of two functions operating between metric spaces

Lemma together_uc : forall A B C D (f:A --> C) (g:B --> D),
is_UniformlyContinuousFunction (fun (p:ProductMS A B) => (f (fst p), g (snd p)):ProductMS C D) (fun x => QposInf_min (mu f x) (mu g x)).

Definition together A B C D (f:A --> C) (g:B --> D) : (ProductMS A B --> ProductMS C D) :=
Build_UniformlyContinuousFunction (together_uc f g).

Uniformly continuous functions on the product space can be curried:

Section uc_curry.

  Context {A B C: MetricSpace} (f: ProductMS A B --> C).

  Definition uc_curry_help_prf (a: A): is_UniformlyContinuousFunction (fun b => f (a , b )) (mu f).

  Definition uc_curry_help (a: A): B --> C := Build_UniformlyContinuousFunction (uc_curry_help_prf a).

  Definition uc_curry_prf: is_UniformlyContinuousFunction uc_curry_help (mu f).

  Definition uc_curry: A --> B --> C := Build_UniformlyContinuousFunction uc_curry_prf.

End uc_curry.

Uncurry probably cannot be defined because because there is no way to construct a uniform modulus of continuity from the domain-indexed set of uni-formly continuous functions.

Hence, we can convert only one way, and so non-curried versions of binary functions are strictly more valuable than their curried representations. Consequently, it can be argued that binary functions should always be defined in non-curried form.

Completion distributes over products:

Section completion_distributes.

  Context {X Y: MetricSpace}.

  Program Definition distrib_Complete (xy: Complete (ProductMS X Y)): ProductMS (Complete X) (Complete Y) :=
   (@Build_RegularFunction _ (fun e => fst (approximate xy e)) _, @Build_RegularFunction _ (fun e => snd (approximate xy e)) _).

  Lemma distrib_Complete_uc_prf: is_UniformlyContinuousFunction distrib_Complete (fun e => e).

  Definition distrib_Complete_uc: Complete (ProductMS X Y) --> ProductMS (Complete X) (Complete Y) :=
    Build_UniformlyContinuousFunction distrib_Complete_uc_prf.

  Program Definition undistrib_Complete (xy: ProductMS (Complete X) (Complete Y)): Complete (ProductMS X Y) :=
   @Build_RegularFunction _ (fun e => (approximate (fst xy) e , approximate (snd xy) e )) _.

  Lemma undistrib_Complete_uc_prf: is_UniformlyContinuousFunction undistrib_Complete (fun e => e).

  Definition undistrib_Complete_uc: ProductMS (Complete X) (Complete Y) --> Complete (ProductMS X Y) :=
    Build_UniformlyContinuousFunction undistrib_Complete_uc_prf.

  Lemma distrib_after_undistrib_Complete xy: st_eq (distrib_Complete (undistrib_Complete xy)) xy.

  Lemma undistrib_after_distrib_Complete xy: st_eq (undistrib_Complete (distrib_Complete xy)) xy.

End completion_distributes.