# Theory Hausdorff_Distance

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

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
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]
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
next
case True
show ?thesis
proof (rule hausdorff_distanceI, auto)
fix x assume H: "x ∈ A"
have "infdist x (C ∪ D) ≤ infdist x C"
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"
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"
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"