Documentation

Mathlib.Topology.MetricSpace.HausdorffDistance

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:

Main results #

Tags #

metric space, Hausdorff distance

Distance of a point to a set as a function into ℝ≥0∞. #

def EMetric.infEdist {α : Type u} [PseudoEMetricSpace α] (x : α) (s : Set α) :

The minimal edistance of a point to a set

Equations
Instances For
    theorem EMetric.le_infEdist {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {d : ENNReal} :
    d EMetric.infEdist x s ys, d edist x y
    @[simp]
    theorem EMetric.infEdist_union {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {t : Set α} :

    The edist to a union is the minimum of the edists

    @[simp]
    theorem EMetric.infEdist_iUnion {ι : Sort u_1} {α : Type u} [PseudoEMetricSpace α] (f : ιSet α) (x : α) :
    EMetric.infEdist x (⋃ (i : ι), f i) = ⨅ (i : ι), EMetric.infEdist x (f i)
    theorem EMetric.infEdist_biUnion {α : Type u} [PseudoEMetricSpace α] {ι : Type u_2} (f : ιSet α) (I : Set ι) (x : α) :
    EMetric.infEdist x (iI, f i) = iI, EMetric.infEdist x (f i)
    @[simp]
    theorem EMetric.infEdist_singleton {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} :

    The edist to a singleton is the edistance to the single point of this singleton

    theorem EMetric.infEdist_le_edist_of_mem {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {s : Set α} (h : y s) :

    The edist to a set is bounded above by the edist to any of its points

    theorem EMetric.infEdist_zero_of_mem {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} (h : x s) :

    If a point x belongs to s, then its edist to s vanishes

    theorem EMetric.infEdist_anti {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {t : Set α} (h : s t) :

    The edist is antitone with respect to inclusion.

    theorem EMetric.infEdist_lt_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal} :
    EMetric.infEdist x s < r ys, edist x y < r

    The edist to a set is < r iff there exists a point in the set at edistance < r

    theorem EMetric.infEdist_le_infEdist_add_edist {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {s : Set α} :

    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

    theorem EMetric.edist_le_infEdist_add_ediam {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {s : Set α} (hy : y s) :
    theorem EMetric.continuous_infEdist {α : Type u} [PseudoEMetricSpace α] {s : Set α} :
    Continuous fun (x : α) => EMetric.infEdist x s

    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

    theorem EMetric.mem_iff_infEdist_zero_of_closed {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} (h : IsClosed s) :

    Given a closed set s, a point belongs to s iff its infimum edistance to this set vanishes

    theorem EMetric.infEdist_pos_iff_not_mem_closure {α : Type u} [PseudoEMetricSpace α] {x : α} {E : Set α} :

    The infimum edistance of a point to a set is positive if and only if the point is not in the closure of the set.

    theorem EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure {α : Type u} [PseudoEMetricSpace α] {x : α} {E : Set α} (h : xclosure E) :
    ∃ (ε : ), 0 < ε ENNReal.ofReal ε < EMetric.infEdist x E
    theorem EMetric.infEdist_image {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {x : α} {t : Set α} {Φ : αβ} (hΦ : Isometry Φ) :

    The infimum edistance is invariant under isometries

    @[simp]
    theorem EMetric.infEdist_vadd {α : Type u} [PseudoEMetricSpace α] {M : Type u_2} [VAdd M α] [IsometricVAdd M α] (c : M) (x : α) (s : Set α) :
    @[simp]
    theorem EMetric.infEdist_smul {α : Type u} [PseudoEMetricSpace α] {M : Type u_2} [SMul M α] [IsometricSMul M α] (c : M) (x : α) (s : Set α) :
    theorem IsOpen.exists_iUnion_isClosed {α : Type u} [PseudoEMetricSpace α] {U : Set α} (hU : IsOpen U) :
    ∃ (F : Set α), (∀ (n : ), IsClosed (F n)) (∀ (n : ), F n U) ⋃ (n : ), F n = U Monotone F
    theorem IsCompact.exists_infEdist_eq_edist {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : IsCompact s) (hne : s.Nonempty) (x : α) :
    ys, EMetric.infEdist x s = edist x y
    theorem EMetric.exists_pos_forall_lt_edist {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :
    ∃ (r : NNReal), 0 < r xs, yt, r < edist x y

    The Hausdorff distance as a function into ℝ≥0∞. #

    theorem EMetric.hausdorffEdist_def {α : Type u_2} [PseudoEMetricSpace α] (s : Set α) (t : Set α) :
    EMetric.hausdorffEdist s t = (xs, EMetric.infEdist x t) yt, EMetric.infEdist y s
    @[irreducible]
    def EMetric.hausdorffEdist {α : Type u_2} [PseudoEMetricSpace α] (s : Set α) (t : Set α) :

    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
    Instances For
      @[simp]

      The Hausdorff edistance of a set to itself vanishes.

      The Haudorff edistances of s to t and of t to s coincide.

      theorem EMetric.hausdorffEdist_le_of_infEdist {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} {r : ENNReal} (H1 : xs, EMetric.infEdist x t r) (H2 : xt, EMetric.infEdist x s r) :

      Bounding the Hausdorff edistance by bounding the edistance of any point in each set to the other set

      theorem EMetric.hausdorffEdist_le_of_mem_edist {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} {r : ENNReal} (H1 : xs, yt, edist x y r) (H2 : xt, ys, edist x y r) :

      Bounding the Hausdorff edistance by exhibiting, for any point in each set, another point in the other set at controlled distance

      theorem EMetric.infEdist_le_hausdorffEdist_of_mem {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {t : Set α} (h : x s) :

      The distance to a set is controlled by the Hausdorff distance.

      theorem EMetric.exists_edist_lt_of_hausdorffEdist_lt {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {t : Set α} {r : ENNReal} (h : x s) (H : EMetric.hausdorffEdist s t < r) :
      yt, edist x y < r

      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.

      theorem EMetric.hausdorffEdist_image {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {t : Set α} {Φ : αβ} (h : Isometry Φ) :

      The Hausdorff edistance is invariant under isometries.

      theorem EMetric.hausdorffEdist_le_ediam {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) :

      The Hausdorff distance is controlled by the diameter of the union.

      The Hausdorff distance satisfies the triangle inequality.

      Two sets are at zero Hausdorff edistance if and only if they have the same closure.

      @[simp]

      The Hausdorff edistance between a set and its closure vanishes.

      @[simp]

      Replacing a set by its closure does not change the Hausdorff edistance.

      @[simp]

      Replacing a set by its closure does not change the Hausdorff edistance.

      The Hausdorff edistance between sets or their closures is the same.

      theorem EMetric.hausdorffEdist_zero_iff_eq_of_closed {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : IsClosed s) (ht : IsClosed t) :

      Two closed sets are at zero Hausdorff edistance if and only if they coincide.

      theorem EMetric.hausdorffEdist_empty {α : Type u} [PseudoEMetricSpace α] {s : Set α} (ne : s.Nonempty) :

      The Haudorff edistance to the empty set is infinite.

      theorem EMetric.nonempty_of_hausdorffEdist_ne_top {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : s.Nonempty) (fin : EMetric.hausdorffEdist s t ) :
      t.Nonempty

      If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty.

      theorem EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (fin : EMetric.hausdorffEdist s t ) :
      s = t = s.Nonempty t.Nonempty

      Now, we turn to the same notions in metric spaces. To avoid the difficulties related to sInf and sSup 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 . #

      def Metric.infDist {α : Type u} [PseudoMetricSpace α] (x : α) (s : Set α) :

      The minimal distance of a point to a set

      Equations
      Instances For
        theorem Metric.infDist_eq_iInf {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} :
        Metric.infDist x s = ⨅ (y : s), dist x y
        theorem Metric.infDist_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} :

        The minimal distance is always nonnegative

        @[simp]
        theorem Metric.infDist_empty {α : Type u} [PseudoMetricSpace α] {x : α} :

        The minimal distance to the empty set is 0 (if you want to have the more reasonable value instead, use EMetric.infEdist, which takes values in ℝ≥0∞)

        theorem Metric.infEdist_ne_top {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : s.Nonempty) :

        In a metric space, the minimal edistance to a nonempty set is finite.

        theorem Metric.infEdist_eq_top_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} :
        theorem Metric.infDist_zero_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : x s) :

        The minimal distance of a point to a set containing it vanishes.

        @[simp]
        theorem Metric.infDist_singleton {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :

        The minimal distance to a singleton is the distance to the unique point in this singleton.

        theorem Metric.infDist_le_dist_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : y s) :

        The minimal distance to a set is bounded by the distance to any point in this set.

        theorem Metric.infDist_le_infDist_of_subset {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {x : α} (h : s t) (hs : s.Nonempty) :

        The minimal distance is monotone with respect to inclusion.

        theorem Metric.infDist_lt_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : } (hs : s.Nonempty) :
        Metric.infDist x s < r ys, dist x y < r

        The minimal distance to a set s is < r iff there exists a point in s at distance < r.

        theorem Metric.infDist_le_infDist_add_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} :

        The minimal distance from x to s is bounded by the distance from y to s, modulo the distance between x and y.

        theorem Metric.not_mem_of_dist_lt_infDist {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : dist x y < Metric.infDist x s) :
        ys
        theorem Metric.dist_le_infDist_add_diam {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (hs : Bornology.IsBounded s) (hy : y s) :
        theorem Metric.lipschitz_infDist_pt {α : Type u} [PseudoMetricSpace α] (s : Set α) :
        LipschitzWith 1 fun (x : α) => Metric.infDist x s

        The minimal distance to a set is Lipschitz in point with constant 1

        The minimal distance to a set is uniformly continuous in point

        theorem Metric.continuous_infDist_pt {α : Type u} [PseudoMetricSpace α] (s : Set α) :
        Continuous fun (x : α) => Metric.infDist x s

        The minimal distance to a set is continuous in point

        theorem Metric.infDist_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} :

        The minimal distances to a set and its closure coincide.

        theorem Metric.infDist_zero_of_mem_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (hx : x closure s) :

        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 Metric.mem_closure_iff_infDist_zero.

        theorem Metric.mem_closure_iff_infDist_zero {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : s.Nonempty) :

        A point belongs to the closure of s iff its infimum distance to this set vanishes.

        theorem IsClosed.mem_iff_infDist_zero {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : IsClosed s) (hs : s.Nonempty) :

        Given a closed set s, a point belongs to s iff its infimum distance to this set vanishes

        theorem IsClosed.not_mem_iff_infDist_pos {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : IsClosed s) (hs : s.Nonempty) :
        xs 0 < Metric.infDist x s

        Given a closed set s, a point belongs to s iff its infimum distance to this set vanishes.

        theorem Metric.continuousAt_inv_infDist_pt {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : xclosure s) :
        ContinuousAt (fun (x : α) => (Metric.infDist x s)⁻¹) x
        theorem Metric.infDist_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {t : Set α} {x : α} {Φ : αβ} (hΦ : Isometry Φ) :
        Metric.infDist (Φ x) (Φ '' t) = Metric.infDist x t

        The infimum distance is invariant under isometries.

        theorem Metric.infDist_inter_closedBall_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : y s) :
        theorem IsCompact.exists_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : IsCompact s) (hne : s.Nonempty) (x : α) :
        ys, Metric.infDist x s = dist x y
        theorem IsClosed.exists_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (h : IsClosed s) (hne : s.Nonempty) (x : α) :
        ys, Metric.infDist x s = dist x y
        theorem Metric.exists_mem_closure_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (hne : s.Nonempty) (x : α) :
        yclosure s, Metric.infDist x s = dist x y

        Distance of a point to a set as a function into ℝ≥0. #

        def Metric.infNndist {α : Type u} [PseudoMetricSpace α] (x : α) (s : Set α) :

        The minimal distance of a point to a set as a ℝ≥0

        Equations
        Instances For
          @[simp]
          theorem Metric.coe_infNndist {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} :
          theorem Metric.lipschitz_infNndist_pt {α : Type u} [PseudoMetricSpace α] (s : Set α) :
          LipschitzWith 1 fun (x : α) => Metric.infNndist x s

          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

          theorem Metric.continuous_infNndist_pt {α : Type u} [PseudoMetricSpace α] (s : Set α) :
          Continuous fun (x : α) => Metric.infNndist x s

          The minimal distance to a set (as ℝ≥0) is continuous in point

          The Hausdorff distance as a function into . #

          def Metric.hausdorffDist {α : Type u} [PseudoMetricSpace α] (s : Set α) (t : Set α) :

          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
          Instances For
            theorem Metric.hausdorffDist_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} :

            The Hausdorff distance is nonnegative.

            theorem Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) (bs : Bornology.IsBounded s) (bt : Bornology.IsBounded t) :

            If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance.

            @[simp]

            The Hausdorff distance between a set and itself is zero.

            The Hausdorff distances from s to t and from t to s coincide.

            @[simp]

            The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value instead, use EMetric.hausdorffEdist, which takes values in ℝ≥0∞).

            @[simp]

            The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value instead, use EMetric.hausdorffEdist, which takes values in ℝ≥0∞).

            theorem Metric.hausdorffDist_le_of_infDist {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {r : } (hr : 0 r) (H1 : xs, Metric.infDist x t r) (H2 : xt, Metric.infDist x s r) :

            Bounding the Hausdorff distance by bounding the distance of any point in each set to the other set

            theorem Metric.hausdorffDist_le_of_mem_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {r : } (hr : 0 r) (H1 : xs, yt, dist x y r) (H2 : xt, ys, dist x y r) :

            Bounding the Hausdorff distance by exhibiting, for any point in each set, another point in the other set at controlled distance

            theorem Metric.hausdorffDist_le_diam {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (hs : s.Nonempty) (bs : Bornology.IsBounded s) (ht : t.Nonempty) (bt : Bornology.IsBounded t) :

            The Hausdorff distance is controlled by the diameter of the union.

            theorem Metric.infDist_le_hausdorffDist_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {x : α} (hx : x s) (fin : EMetric.hausdorffEdist s t ) :

            The distance to a set is controlled by the Hausdorff distance.

            theorem Metric.exists_dist_lt_of_hausdorffDist_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {x : α} {r : } (h : x s) (H : Metric.hausdorffDist s t < r) (fin : EMetric.hausdorffEdist s t ) :
            yt, dist x y < r

            If the Hausdorff distance is < r, any point in one of the sets is at distance < r of a point in the other set.

            theorem Metric.exists_dist_lt_of_hausdorffDist_lt' {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {y : α} {r : } (h : y t) (H : Metric.hausdorffDist s t < r) (fin : EMetric.hausdorffEdist s t ) :
            xs, dist x y < r

            If the Hausdorff distance is < r, 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

            theorem Metric.hausdorffDist_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {t : Set α} {Φ : αβ} (h : Isometry Φ) :

            The Hausdorff distance is invariant under isometries.

            The Hausdorff distance satisfies the triangle inequality.

            The Hausdorff distance satisfies the triangle inequality.

            @[simp]

            The Hausdorff distance between a set and its closure vanishes.

            @[simp]

            Replacing a set by its closure does not change the Hausdorff distance.

            @[simp]

            Replacing a set by its closure does not change the Hausdorff distance.

            The Hausdorff distances between two sets and their closures coincide.

            Two sets are at zero Hausdorff distance if and only if they have the same closures.

            theorem IsClosed.hausdorffDist_zero_iff_eq {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (hs : IsClosed s) (ht : IsClosed t) (fin : EMetric.hausdorffEdist s t ) :

            Two closed sets are at zero Hausdorff distance if and only if they coincide.