(* 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*)