# 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
Furthermore, if a product space is stable, then the components are stable (assuming the components are non-zero).
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:
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: