Theory Hausdorff_Distance

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section ‹Hausdorff distance›

theory Hausdorff_Distance
  imports Library_Complements
begin

subsection ‹Preliminaries›



subsection ‹Hausdorff distance›

text ‹The Hausdorff distance between two subsets of a metric space is the minimal $M$ such that
each set is included in the $M$-neighborhood of the other. For nonempty bounded sets, it
satisfies the triangular inequality, it is symmetric, but it vanishes on sets that have the same
closure. In particular, it defines a distance on closed bounded nonempty sets. We establish
all these properties below.›

definition hausdorff_distance::"('a::metric_space) set  'a set  real"
  where "hausdorff_distance A B = (if A = {}  B = {}  (¬(bounded A))  (¬(bounded B)) then 0
                                   else max (SUP xA. infdist x B) (SUP xB. infdist x A))"

lemma hausdorff_distance_self [simp]:
  "hausdorff_distance A A = 0"
unfolding hausdorff_distance_def by auto

lemma hausdorff_distance_sym:
  "hausdorff_distance A B = hausdorff_distance B A"
unfolding hausdorff_distance_def by auto

lemma hausdorff_distance_points [simp]:
  "hausdorff_distance {x} {y} = dist x y"
unfolding hausdorff_distance_def by (auto, metis dist_commute max.idem)

text ‹The Hausdorff distance is expressed in terms of a supremum. To use it, one needs again
and again to show that this is the supremum of a set which is bounded from above.›

lemma bdd_above_infdist_aux:
  assumes "bounded A" "bounded B"
  shows "bdd_above ((λx. infdist x B)`A)"
proof (cases "B = {}")
  case True
  then show ?thesis unfolding infdist_def by auto
next
  case False
  then obtain y where "y  B" by auto
  then have "infdist x B  dist x y" if "x  A" for x
    by (simp add: infdist_le)
  then show ?thesis unfolding bdd_above_def
    by (auto, metis assms(1) bounded_any_center dist_commute order_trans)
qed

lemma hausdorff_distance_nonneg [simp, mono_intros]:
  "hausdorff_distance A B  0"
proof (cases "A = {}  B = {}  (¬(bounded A))  (¬(bounded B))")
  case True
  then show ?thesis unfolding hausdorff_distance_def by auto
next
  case False
  then have "A  {}" "B  {}" "bounded A" "bounded B" by auto
  have "(SUP xA. infdist x B)  0"
    using bdd_above_infdist_aux[OF bounded A bounded B] infdist_nonneg
    by (metis A  {} all_not_in_conv cSUP_upper2)
  moreover have "(SUP xB. infdist x A)  0"
    using bdd_above_infdist_aux[OF bounded B bounded A] infdist_nonneg
    by (metis B  {} all_not_in_conv cSUP_upper2)
  ultimately show ?thesis unfolding hausdorff_distance_def by auto
qed

lemma hausdorff_distanceI:
  assumes "x. x  A  infdist x B  D"
          "x. x  B  infdist x A  D"
          "D  0"
  shows "hausdorff_distance A B  D"
proof (cases "A = {}  B = {}  (¬(bounded A))  (¬(bounded B))")
  case True
  then show ?thesis unfolding hausdorff_distance_def using D  0 by auto
next
  case False
  then have "A  {}" "B  {}" "bounded A" "bounded B" by auto
  have "(SUP xA. infdist x B)  D"
    apply (rule cSUP_least, simp add: A  {}) using assms(1) by blast
  moreover have "(SUP xB. infdist x A)  D"
    apply (rule cSUP_least, simp add: B  {}) using assms(2) by blast
  ultimately show ?thesis unfolding hausdorff_distance_def using False by auto
qed

lemma hausdorff_distanceI2:
  assumes "x. x  A  yB. dist x y  D"
          "x. x  B  yA. dist x y  D"
          "D  0"
  shows "hausdorff_distance A B  D"
proof (rule hausdorff_distanceI[OF _ _ D  0])
  fix x assume "x  A" show "infdist x B  D" using assms(1)[OF x  A] infdist_le2 by fastforce
next
  fix x assume "x  B" show "infdist x A  D" using assms(2)[OF x  B] infdist_le2 by fastforce
qed

lemma infdist_le_hausdorff_distance [mono_intros]:
  assumes "x  A" "bounded A" "bounded B"
  shows "infdist x B  hausdorff_distance A B"
proof (cases "B = {}")
  case True
  then have "infdist x B = 0" unfolding infdist_def by auto
  then show ?thesis using hausdorff_distance_nonneg by auto
next
  case False
  have "infdist x B  (SUP yA. infdist y B)"
    using bdd_above_infdist_aux[OF bounded A bounded B] by (meson assms(1) cSUP_upper)
  then show ?thesis unfolding hausdorff_distance_def using assms False by auto
qed

lemma hausdorff_distance_infdist_triangle [mono_intros]:
  assumes "B  {}" "bounded B" "bounded C"
  shows "infdist x C  infdist x B + hausdorff_distance B C"
proof (cases "C = {}")
  case True
  then have "infdist x C = 0" unfolding infdist_def by auto
  then show ?thesis using infdist_nonneg[of x B] hausdorff_distance_nonneg[of B C] by auto
next
  case False
  have "infdist x C - hausdorff_distance B C  dist x b" if "b  B" for b
  proof -
    have "infdist x C  infdist b C + dist x b" by (rule infdist_triangle)
    also have "...  dist x b + hausdorff_distance B C"
      using infdist_le_hausdorff_distance[OF b  B bounded B bounded C] by auto
    finally show ?thesis by auto
  qed
  then have "infdist x C - hausdorff_distance B C  infdist x B"
    unfolding infdist_def using B  {} by (simp add: le_cINF_iff)
  then show ?thesis by auto
qed

lemma hausdorff_distance_triangle [mono_intros]:
  assumes "B  {}" "bounded B"
  shows "hausdorff_distance A C  hausdorff_distance A B + hausdorff_distance B C"
proof (cases "A = {}  C = {}  (¬(bounded A))  (¬(bounded C))")
  case True
  then have "hausdorff_distance A C = 0" unfolding hausdorff_distance_def by auto
  then show ?thesis
    using hausdorff_distance_nonneg[of A B] hausdorff_distance_nonneg[of B C] by auto
next
  case False
  then have *: "A  {}" "C  {}" "bounded A" "bounded C" by auto
  define M where "M = hausdorff_distance A B + hausdorff_distance B C"
  have "infdist x C  M" if "x  A" for x
    using hausdorff_distance_infdist_triangle[OF B  {} bounded B bounded C, of x]
          infdist_le_hausdorff_distance[OF x  A bounded A bounded B] by (auto simp add: M_def)
  moreover have "infdist x A  M" if "x  C" for x
    using hausdorff_distance_infdist_triangle[OF B  {} bounded B bounded A, of x]
          infdist_le_hausdorff_distance[OF x  C bounded C bounded B]
    by (auto simp add: hausdorff_distance_sym M_def)
  ultimately have "hausdorff_distance A C  M"
    unfolding hausdorff_distance_def using * bdd_above_infdist_aux by (auto simp add: cSUP_least)
  then show ?thesis unfolding M_def by auto
qed

lemma hausdorff_distance_subset:
  assumes "A  B" "A  {}" "bounded B"
  shows "hausdorff_distance A B = (SUP xB. infdist x A)"
proof -
  have H: "B  {}" "bounded A" using assms bounded_subset by auto
  have "(SUP xA. infdist x B) = 0" using assms by (simp add: subset_eq)
  moreover have "(SUP xB. infdist x A)  0"
    using bdd_above_infdist_aux[OF bounded B bounded A] infdist_nonneg[of _ A]
    by (meson H(1) cSUP_upper2 ex_in_conv)
  ultimately show ?thesis unfolding hausdorff_distance_def using assms H by auto
qed

lemma hausdorff_distance_closure [simp]:
  "hausdorff_distance A (closure A) = 0"
proof (cases "A = {}  (¬(bounded A))")
  case True
  then show ?thesis unfolding hausdorff_distance_def by auto
next
  case False
  then have "A  {}" "bounded A" by auto
  then have "closure A  {}" "bounded (closure A)" "A  closure A"
    using closure_subset by auto
  have "infdist x A = 0" if "x  closure A" for x
    using in_closure_iff_infdist_zero[OF A  {}] that by auto
  then have "(SUP xclosure A. infdist x A) = 0"
    using closure A  {} by auto
  then show ?thesis
    unfolding hausdorff_distance_subset[OF A  closure A A  {} bounded (closure A)] by simp
qed

lemma hausdorff_distance_closures [simp]:
  "hausdorff_distance (closure A) (closure B) = hausdorff_distance A B"
proof (cases "A = {}  B = {}  (¬(bounded A))  (¬(bounded B))")
  case True
  then have *: "hausdorff_distance A B = 0" unfolding hausdorff_distance_def by auto
  have "closure A = {}  (¬(bounded (closure A)))  closure B = {}  (¬(bounded (closure B)))"
    using True bounded_subset closure_subset by auto
  then have "hausdorff_distance (closure A) (closure B) = 0"
    unfolding hausdorff_distance_def by auto
  then show ?thesis using * by simp
next
  case False
  then have H: "A  {}" "B  {}" "bounded A" "bounded B" by auto
  then have H2: "closure A  {}" "closure B  {}" "bounded (closure A)" "bounded (closure B)"
    by auto
  have "hausdorff_distance A B  hausdorff_distance A (closure A) + hausdorff_distance (closure A) B"
    apply (rule hausdorff_distance_triangle) using H H2 by auto
  also have "... = hausdorff_distance (closure A) B"
    using hausdorff_distance_closure by auto
  also have "...  hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B"
    apply (rule hausdorff_distance_triangle) using H H2 by auto
  also have "... = hausdorff_distance (closure A) (closure B)"
    using hausdorff_distance_closure by (auto simp add: hausdorff_distance_sym)
  finally have *: "hausdorff_distance A B  hausdorff_distance (closure A) (closure B)" by simp

  have "hausdorff_distance (closure A) (closure B)  hausdorff_distance (closure A) A + hausdorff_distance A (closure B)"
    apply (rule hausdorff_distance_triangle) using H H2 by auto
  also have "... = hausdorff_distance A (closure B)"
    using hausdorff_distance_closure by (auto simp add: hausdorff_distance_sym)
  also have "...  hausdorff_distance A B + hausdorff_distance B (closure B)"
    apply (rule hausdorff_distance_triangle) using H H2 by auto
  also have "... = hausdorff_distance A B"
    using hausdorff_distance_closure by (auto simp add: hausdorff_distance_sym)
  finally have "hausdorff_distance (closure A) (closure B)  hausdorff_distance A B" by simp
  then show ?thesis using * by auto
qed

lemma hausdorff_distance_zero:
  assumes "A  {}" "bounded A" "B  {}" "bounded B"
  shows "hausdorff_distance A B = 0  closure A = closure B"
proof
  assume H: "hausdorff_distance A B = 0"
  have "A  closure B"
  proof
    fix x assume "x  A"
    have "infdist x B = 0"
      using infdist_le_hausdorff_distance[OF x  A bounded A bounded B] H infdist_nonneg[of x B] by auto
    then show "x  closure B" using in_closure_iff_infdist_zero[OF B  {}] by auto
  qed
  then have A: "closure A  closure B" by (simp add: closure_minimal)

  have "B  closure A"
  proof
    fix x assume "x  B"
    have "infdist x A = 0"
      using infdist_le_hausdorff_distance[OF x  B bounded B bounded A] H infdist_nonneg[of x A]
      by (auto simp add: hausdorff_distance_sym)
    then show "x  closure A" using in_closure_iff_infdist_zero[OF A  {}] by auto
  qed
  then have "closure B  closure A" by (simp add: closure_minimal)
  then show "closure A = closure B" using A by auto
next
  assume "closure A = closure B"
  then show "hausdorff_distance A B = 0"
    using hausdorff_distance_closures[of A B] by auto
qed

lemma hausdorff_distance_vimage:
  assumes "x. x  A  dist (f x) (g x)  C"
          "C  0"
  shows "hausdorff_distance (f`A) (g`A)  C"
apply (rule hausdorff_distanceI2[OF _ _ C  0]) using assms by (auto simp add: dist_commute, auto)

lemma hausdorff_distance_union [mono_intros]:
  assumes "A  {}" "B  {}" "C  {}" "D  {}"
  shows "hausdorff_distance (A  B) (C  D)  max (hausdorff_distance A C) (hausdorff_distance B D)"
proof (cases "bounded A  bounded B  bounded C  bounded D")
  case False
  then have "hausdorff_distance (A  B) (C  D) = 0"
    unfolding hausdorff_distance_def by auto
  then show ?thesis
    by (simp add: hausdorff_distance_nonneg le_max_iff_disj)
next
  case True
  show ?thesis
  proof (rule hausdorff_distanceI, auto)
    fix x assume H: "x  A"
    have "infdist x (C  D)  infdist x C"
      by (simp add: assms infdist_union_min)
    also have "...  hausdorff_distance A C"
      apply (rule infdist_le_hausdorff_distance) using H True by auto
    also have "...  max (hausdorff_distance A C) (hausdorff_distance B D)"
      by auto
    finally show "infdist x (C  D)  max (hausdorff_distance A C) (hausdorff_distance B D)"
      by simp
  next
    fix x assume H: "x  B"
    have "infdist x (C  D)  infdist x D"
      by (simp add: assms infdist_union_min)
    also have "...  hausdorff_distance B D"
      apply (rule infdist_le_hausdorff_distance) using H True by auto
    also have "...  max (hausdorff_distance A C) (hausdorff_distance B D)"
      by auto
    finally show "infdist x (C  D)  max (hausdorff_distance A C) (hausdorff_distance B D)"
      by simp
  next
    fix x assume H: "x  C"
    have "infdist x (A  B)  infdist x A"
      by (simp add: assms infdist_union_min)
    also have "...  hausdorff_distance C A"
      apply (rule infdist_le_hausdorff_distance) using H True by auto
    also have "...  max (hausdorff_distance A C) (hausdorff_distance B D)"
      using hausdorff_distance_sym[of A C] by auto
    finally show "infdist x (A  B)  max (hausdorff_distance A C) (hausdorff_distance B D)"
      by simp
  next
    fix x assume H: "x  D"
    have "infdist x (A  B)  infdist x B"
      by (simp add: assms infdist_union_min)
    also have "...  hausdorff_distance D B"
      apply (rule infdist_le_hausdorff_distance) using H True by auto
    also have "...  max (hausdorff_distance A C) (hausdorff_distance B D)"
      using hausdorff_distance_sym[of B D] by auto
    finally show "infdist x (A  B)  max (hausdorff_distance A C) (hausdorff_distance B D)"
      by simp
  qed (simp add: le_max_iff_disj)
qed

end (*of theory Hausdorff_Distance*)