Hausdorff Metric

This module defines a Hausdorff metric for an arbitrary predicate over a metric space X.

Variable X : MetricSpace.

This is the (weak) hemiMetric, which makes an asymmetric metric. We make use of the classical quantifer in this definition.

Definition hemiMetric (e:Qpos) (A B: X -> Prop) :=
forall x:X, A x ->
existsC X (fun y => B y /\ ball e x y).

This (weak) metric, makes the full symmetric metric.

Definition hausdorffBall (e:Qpos) (A B: X -> Prop) :=
hemiMetric e A B /\ hemiMetric e B A.

Lemma hemiMetric_wd1 : forall (e0 e1:Qpos) A B,
(QposEq e0 e1) -> hemiMetric e0 A B -> hemiMetric e1 A B.

Lemma hausdorffBall_wd1 : forall (e0 e1:Qpos) A B,
(QposEq e0 e1) -> hausdorffBall e0 A B -> hausdorffBall e1 A B.

Lemma hemiMetric_refl : forall e A, hemiMetric e A A.

Lemma hausdorffBall_refl : forall e A, hausdorffBall e A A.

Lemma hausdorffBall_sym : forall e A B,
hausdorffBall e A B -> hausdorffBall e B A.

Lemma hemiMetric_triangle : forall e0 e1 A B C,
hemiMetric e0 A B -> hemiMetric e1 B C -> hemiMetric (e0 + e1) A C.

Lemma hausdorffBall_triangle : forall e0 e1 A B C,
hausdorffBall e0 A B -> hausdorffBall e1 B C -> hausdorffBall (e0 + e1) A C.

Unfortunately this isn't a metric for an aribitrary predicate. More assumptions are needed to show our definition of ball is closed. See FinEnum for an example of an instance of the Hausdorff metric.

Hypothesis stableX : stableMetric X.

Lemma hemiMetric_stable :forall e A B, ~~(hemiMetric e A B) -> hemiMetric e A B.

Lemma hausdorffBall_stable :forall e A B, ~~(hausdorffBall e A B) -> hausdorffBall e A B.

Lemma hemiMetric_wd :forall (e1 e2:Qpos), (e1==e2) ->
forall A1 A2, (forall x, A1 x <-> A2 x) ->
forall B1 B2, (forall x, B1 x <-> B2 x) ->
(hemiMetric e1 A1 B1 <-> hemiMetric e2 A2 B2).

Lemma hausdorffBall_wd :forall (e1 e2:Qpos), (e1==e2) ->
forall A1 A2, (forall x, A1 x <-> A2 x) ->
forall B1 B2, (forall x, B1 x <-> B2 x) ->
(hausdorffBall e1 A1 B1 <-> hausdorffBall e2 A2 B2).

End HausdorffMetric.

Section HausdorffMetricStrong.

Variable X : MetricSpace.

Strong Hausdorff Metric

This section introduces an alternative stronger notition of Haudorff metric that uses a constructive existential.

Definition hemiMetricStrong (e:Qpos) (A B: X -> Prop) :=
forall x:X, A x ->
forall d:Qpos, {y:X | B y /\ ball (e+d) x y}.

Definition hausdorffBallStrong (e:Qpos) (A B: X -> Prop) :=
(hemiMetricStrong e A B * hemiMetricStrong e B A)%type.

Lemma hemiMetricStrong_wd1 : forall (e0 e1:Qpos) A B,
(QposEq e0 e1) -> hemiMetricStrong e0 A B -> hemiMetricStrong e1 A B.

Lemma hausdorffBallStrong_wd1 : forall (e0 e1:Qpos) A B,
(QposEq e0 e1) -> hausdorffBallStrong e0 A B -> hausdorffBallStrong e1 A B.

Lemma hemiMetricStrong_refl : forall e A, hemiMetricStrong e A A.

Lemma hausdorffBallStrong_refl : forall e A, hausdorffBallStrong e A A.

Lemma hausdorffBallStrong_sym : forall e A B,
hausdorffBallStrong e A B -> hausdorffBallStrong e B A.

Lemma hemiMetricStrong_triangle : forall e0 e1 A B C,
hemiMetricStrong e0 A B -> hemiMetricStrong e1 B C -> hemiMetricStrong (e0 + e1) A C.

Lemma hausdorffBallStrong_triangle : forall e0 e1 A B C,
hausdorffBallStrong e0 A B -> hausdorffBallStrong e1 B C -> hausdorffBallStrong (e0 + e1) A C.

Hypothesis almostDecideX : locatedMetric X.

End HausdorffMetricStrong.