CoRN.metric2.Metric

Require Export RSetoid.
Require Import Relation_Definitions.
Require Export Qpossec.
Require Import COrdFields2.
Require Import Qordfield.
Require Import QMinMax.
Require Import List.
Require Import CornTac.
Require Import stdlib_omissions.Q.

Require QnnInf.
Import QnnInf.notations.

Open Local Scope Q_scope.

Metric Space

In this version, a metric space over a setoid X is characterized by a ball relation B where B e x y is intended to mean that the two points x and y are within e of each other ( d(x,y)<=e ). This is characterized by the axioms given in the record structure below.

Record is_MetricSpace (X : RSetoid) (B: Qpos -> relation X) : Prop :=
{ msp_refl: forall e, Reflexive (B e)
; msp_sym: forall e, Symmetric (B e)
; msp_triangle: forall e1 e2 a b c, B e1 a b -> B e2 b c -> B (e1 + e2)%Qpos a c
; msp_closed: forall e a b, (forall d, B (e +d)%Qpos a b) -> B e a b
; msp_eq: forall a b, (forall e, B e a b) -> st_eq a b
}.

Record MetricSpace : Type :=
{ msp_is_setoid :> RSetoid
; ball : Qpos -> msp_is_setoid -> msp_is_setoid -> Prop
; ball_wd : forall (e1 e2:Qpos), (QposEq e1 e2) ->
            forall x1 x2, (st_eq x1 x2) ->
            forall y1 y2, (st_eq y1 y2) ->
            (ball e1 x1 y1 <-> ball e2 x2 y2)
; msp : is_MetricSpace msp_is_setoid ball
}.

Section Metric_Space.

Variable X : MetricSpace.

These lemmas give direct access to the ball axioms of a metric space

Lemma ball_refl : forall e (a:X), ball e a a.

Lemma ball_sym : forall e (a b:X), ball e a b -> ball e b a.

Lemma ball_triangle : forall e1 e2 (a b c:X), ball e1 a b -> ball e2 b c -> ball (e1 +e2) a c.

Lemma ball_closed : forall e (a b:X), (forall d, ball (e +d) a b) -> ball e a b.

Lemma ball_eq : forall (a b:X), (forall e, ball e a b) -> st_eq a b.

Lemma ball_eq_iff : forall (a b:X), (forall e, ball e a b ) <-> st_eq a b.

The ball constraint on a and b can always be weakened. Here are two forms of the weakening lemma.

Lemma ball_weak : forall e d (a b:X), ball e a b -> ball (e +d) a b.

Hint Resolve ball_refl ball_triangle ball_weak : metric.

Lemma ball_weak_le : forall (e d:Qpos) (a b:X), e <=d -> ball e a b -> ball d a b.

End Metric_Space.

We can easily generalize ball to take the ratio from Q or QnnInf:

Section gball.

  Context {m: MetricSpace}.

  Definition gball (q: Q) (x y: m): Prop :=
    match Qdec_sign q with
    | inl (inl _) => False
    | inl (inr p) => ball (exist (Qlt 0) q p) x y
    | inr _ => x [=]y
    end.

  Definition gball_ex (e: QnnInf): relation m :=
    match e with
    | QnnInf.Finite e' => gball (proj1_sig e')
    | QnnInf.Infinite => fun _ _ => True
    end.

  Lemma ball_gball (q: Qpos) (x y: m): gball q x y <-> ball q x y.

  Global Instance gball_Proper: Proper (Qeq ==> @st_eq m ==> @st_eq m ==> iff) gball.

  Global Instance gball_ex_Proper: Proper (QnnInf.eq ==> @st_eq m ==> @st_eq m ==> iff) gball_ex.

  Global Instance gball_refl (e: Q): 0 <= e -> Reflexive (gball e).

  Global Instance gball_ex_refl (e: QnnInf): Reflexive (gball_ex e).

  Global Instance gball_sym (e: Q): Symmetric (gball e).

  Lemma gball_ex_sym (e: QnnInf): Symmetric (gball_ex e).

  Lemma gball_triangle (e1 e2: Q) (a b c: m):
    gball e1 a b -> gball e2 b c -> gball (e1 + e2) a c.

  Lemma gball_ex_triangle (e1 e2: QnnInf) (a b c: m):
    gball_ex e1 a b -> gball_ex e2 b c -> gball_ex (e1 + e2)%QnnInf a c.

  Lemma gball_0 (x y: m): gball 0 x y <-> x [=] y.

  Lemma gball_weak_le (q q': Q): q <= q' -> forall x y, gball q x y -> gball q' x y.

End gball.