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 x∈A. infdist x B) (SUP x∈B. 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 x∈A. 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 x∈B. 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 x∈A. infdist x B) ≤ D"
    apply (rule cSUP_least, simp add: ‹A ≠ {}›) using assms(1) by blast
  moreover have "(SUP x∈B. 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 ⟹ ∃y∈B. dist x y ≤ D"
          "⋀x. x ∈ B ⟹ ∃y∈A. 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 y∈A. 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 x∈B. infdist x A)"
proof -
  have H: "B ≠ {}" "bounded A" using assms bounded_subset by auto
  have "(SUP x∈A. infdist x B) = 0" using assms by (simp add: subset_eq)
  moreover have "(SUP x∈B. 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 x∈closure 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*)