Hausdorff distance #
The Hausdorff distance on subsets of a metric (or emetric) space.
Given two subsets s
and t
of a metric space, their Hausdorff distance is the smallest d
such that any point s
is within d
of a point in t
, and conversely. This quantity
is often infinite (think of s
bounded and t
unbounded), and therefore better
expressed in the setting of emetric spaces.
Main definitions #
This files introduces:
inf_edist x s
, the infimum edistance of a pointx
to a sets
in an emetric spaceHausdorff_edist s t
, the Hausdorff edistance of two sets in an emetric space- Versions of these notions on metric spaces, called respectively
inf_dist
andHausdorff_dist
thickening δ s
, the open thickening by radiusδ
of a sets
in a pseudo emetric space.cthickening δ s
, the closed thickening by radiusδ
of a sets
in a pseudo emetric space.
Distance of a point to a set as a function into ℝ≥0∞
. #
The minimal edistance of a point to a set
Equations
- emetric.inf_edist x s = ⨅ (y : α) (H : y ∈ s), has_edist.edist x y
The edist to a union is the minimum of the edists
The edist to a singleton is the edistance to the single point of this singleton
The edist to a set is bounded above by the edist to any of its points
If a point x
belongs to s
, then its edist to s
vanishes
The edist is antitone with respect to inclusion.
The edist to a set is < r
iff there exists a point in the set at edistance < r
The edist of x
to s
is bounded by the sum of the edist of y
to s
and
the edist from x
to y
The edist to a set depends continuously on the point
The edist to a set and to its closure coincide
A point belongs to the closure of s
iff its infimum edistance to this set vanishes
Given a closed set s
, a point belongs to s
iff its infimum edistance to this set vanishes
The infimum edistance is invariant under isometries
The Hausdorff distance as a function into ℝ≥0∞
. #
The Hausdorff edistance between two sets is the smallest r
such that each set
is contained in the r
-neighborhood of the other one
Equations
- emetric.Hausdorff_edist s t = (⨆ (x : α) (H : x ∈ s), emetric.inf_edist x t) ⊔ ⨆ (y : α) (H : y ∈ t), emetric.inf_edist y s
The Hausdorff edistance of a set to itself vanishes
The Haudorff edistances of s
to t
and of t
to s
coincide
Bounding the Hausdorff edistance by bounding the edistance of any point in each set to the other set
Bounding the Hausdorff edistance by exhibiting, for any point in each set, another point in the other set at controlled distance
The distance to a set is controlled by the Hausdorff distance
If the Hausdorff distance is <r
, then any point in one of the sets has
a corresponding point at distance <r
in the other set
The distance from x
to s
or t
is controlled in terms of the Hausdorff distance
between s
and t
The Hausdorff edistance is invariant under eisometries
The Hausdorff distance is controlled by the diameter of the union
The Hausdorff distance satisfies the triangular inequality
Two sets are at zero Hausdorff edistance if and only if they have the same closure
The Hausdorff edistance between a set and its closure vanishes
Replacing a set by its closure does not change the Hausdorff edistance.
Replacing a set by its closure does not change the Hausdorff edistance.
The Hausdorff edistance between sets or their closures is the same
Two closed sets are at zero Hausdorff edistance if and only if they coincide
The Haudorff edistance to the empty set is infinite
If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty
Now, we turn to the same notions in metric spaces. To avoid the difficulties related to
Inf
and Sup
on ℝ
(which is only conditionally complete), we use the notions in ℝ≥0∞
formulated in terms of the edistance, and coerce them to ℝ
.
Then their properties follow readily from the corresponding properties in ℝ≥0∞
,
modulo some tedious rewriting of inequalities from one to the other.
Distance of a point to a set as a function into ℝ
. #
The minimal distance of a point to a set
Equations
- metric.inf_dist x s = (emetric.inf_edist x s).to_real
the minimal distance is always nonnegative
the minimal distance to the empty set is 0 (if you want to have the more reasonable
value ∞ instead, use inf_edist
, which takes values in ℝ≥0∞)
In a metric space, the minimal edistance to a nonempty set is finite
The minimal distance of a point to a set containing it vanishes
The minimal distance to a singleton is the distance to the unique point in this singleton
The minimal distance to a set is bounded by the distance to any point in this set
The minimal distance is monotonous with respect to inclusion
The minimal distance to a set is < r
iff there exists a point in this set at distance < r
The minimal distance from x
to s
is bounded by the distance from y
to s
, modulo
the distance between x
and y
The minimal distance to a set is Lipschitz in point with constant 1
The minimal distance to a set is uniformly continuous in point
The minimal distance to a set is continuous in point
The minimal distance to a set and its closure coincide
If a point belongs to the closure of s
, then its infimum distance to s
equals zero.
The converse is true provided that s
is nonempty, see mem_closure_iff_inf_dist_zero
.
A point belongs to the closure of s
iff its infimum distance to this set vanishes
Given a closed set s
, a point belongs to s
iff its infimum distance to this set vanishes
Given a closed set s
, a point belongs to s
iff its infimum distance to this set vanishes
The infimum distance is invariant under isometries
Distance of a point to a set as a function into ℝ≥0
. #
The minimal distance of a point to a set as a ℝ≥0
Equations
- metric.inf_nndist x s = (emetric.inf_edist x s).to_nnreal
The minimal distance to a set (as ℝ≥0
) is Lipschitz in point with constant 1
The minimal distance to a set (as ℝ≥0
) is uniformly continuous in point
The minimal distance to a set (as ℝ≥0
) is continuous in point
The Hausdorff distance as a function into ℝ
. #
The Hausdorff distance between two sets is the smallest nonnegative r
such that each set is
included in the r
-neighborhood of the other. If there is no such r
, it is defined to
be 0
, arbitrarily
Equations
- metric.Hausdorff_dist s t = (emetric.Hausdorff_edist s t).to_real
The Hausdorff distance is nonnegative
If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance.
The Hausdorff distance between a set and itself is zero
The Hausdorff distance from s
to t
and from t
to s
coincide
The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value ∞ instead, use Hausdorff_edist
, which takes values in ℝ≥0∞)
The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value ∞ instead, use Hausdorff_edist
, which takes values in ℝ≥0∞)
Bounding the Hausdorff distance by bounding the distance of any point in each set to the other set
Bounding the Hausdorff distance by exhibiting, for any point in each set, another point in the other set at controlled distance
The Hausdorff distance is controlled by the diameter of the union
The distance to a set is controlled by the Hausdorff distance
If the Hausdorff distance is <r
, then any point in one of the sets is at distance
<r
of a point in the other set
If the Hausdorff distance is <r
, then any point in one of the sets is at distance
<r
of a point in the other set
The infimum distance to s
and t
are the same, up to the Hausdorff distance
between s
and t
The Hausdorff distance is invariant under isometries
The Hausdorff distance satisfies the triangular inequality
The Hausdorff distance satisfies the triangular inequality
The Hausdorff distance between a set and its closure vanish
Replacing a set by its closure does not change the Hausdorff distance.
Replacing a set by its closure does not change the Hausdorff distance.
The Hausdorff distance between two sets and their closures coincide
Two sets are at zero Hausdorff distance if and only if they have the same closures
Two closed sets are at zero Hausdorff distance if and only if they coincide
The (open) δ
-thickening thickening δ E
of a subset E
in a pseudo emetric space consists
of those points that are at distance less than δ
from some point of E
.
Equations
- metric.thickening δ E = {x : α | emetric.inf_edist x E < ennreal.of_real δ}
The (open) thickening equals the preimage of an open interval under inf_edist
.
The (open) thickening is an open set.
The (open) thickening of the empty set is empty.
The (open) thickening thickening δ E
of a fixed subset E
is an increasing function of the
thickening radius δ
.
The (open) thickening thickening δ E
with a fixed thickening radius δ
is
an increasing function of the subset E
.
A point in a metric space belongs to the (open) δ
-thickening of a subset E
if and only if
it is at distance less than δ
from some point of E
.
The (open) δ
-thickening thickening δ E
of a subset E
in a metric space equals the
union of balls of radius δ
centered at points of E
.
The closed δ
-thickening cthickening δ E
of a subset E
in a pseudo emetric space consists
of those points that are at infimum distance at most δ
from E
.
Equations
- metric.cthickening δ E = {x : α | emetric.inf_edist x E ≤ ennreal.of_real δ}
The closed thickening is a closed set.
The closed thickening of the empty set is empty.
The closed thickening with radius zero is the closure of the set.
The closed thickening cthickening δ E
of a fixed subset E
is an increasing function of
the thickening radius δ
.
The closed thickening cthickening δ E
with a fixed thickening radius δ
is
an increasing function of the subset E
.
The closed thickening cthickening δ₁ E
is contained in the open thickening thickening δ₂ E
if the radius of the latter is positive and larger.
The open thickening thickening δ E
is contained in the closed thickening cthickening δ E
with the same radius.
The closed thickening of a set contains the closure of the set.
The (open) thickening of a set contains the closure of the set.
A set is contained in its own (open) thickening.
A set is contained in its own closed thickening.
The closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero.
The closure of a set equals the intersection of its closed thickenings of positive radii.
The closure of a set equals the intersection of its open thickenings of positive radii accumulating at zero.
The closure of a set equals the intersection of its (open) thickenings of positive radii.
The frontier of the (open) thickening of a set is contained in an inf_edist
level set.
The frontier of the closed thickening of a set is contained in an inf_edist
level set.
The closed ball of radius δ
centered at a point of E
is included in the closed
thickening of E
.
The closed thickening of a compact set E
is the union of the balls closed_ball x δ
over
x ∈ E
.
For the equality, see inf_edist_cthickening
.
For the equality, see inf_edist_thickening
.
For the equality, see thickening_thickening
.
For the equality, see thickening_cthickening
.
For the equality, see cthickening_thickening
.
For the equality, see cthickening_cthickening
.