(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Isometries› theory Isometries imports Library_Complements Hausdorff_Distance begin text ‹Isometries, i.e., functions that preserve distances, show up very often in mathematics. We introduce a dedicated definition, and show its basic properties.› definition isometry_on::"('a::metric_space) set ⇒ ('a ⇒ ('b::metric_space)) ⇒ bool" where "isometry_on X f = (∀x ∈ X. ∀y ∈ X. dist (f x) (f y) = dist x y)" definition isometry :: "('a::metric_space ⇒ 'b::metric_space) ⇒ bool" where "isometry f ≡ isometry_on UNIV f ∧ range f = UNIV" lemma isometry_on_subset: assumes "isometry_on X f" "Y ⊆ X" shows "isometry_on Y f" using assms unfolding isometry_on_def by auto lemma isometry_onI [intro?]: assumes "⋀x y. x ∈ X ⟹ y ∈ X ⟹ dist (f x) (f y) = dist x y" shows "isometry_on X f" using assms unfolding isometry_on_def by auto lemma isometry_onD: assumes "isometry_on X f" "x ∈ X" "y ∈ X" shows "dist (f x) (f y) = dist x y" using assms unfolding isometry_on_def by auto lemma isometryI [intro?]: assumes "⋀x y. dist (f x) (f y) = dist x y" "range f = UNIV" shows "isometry f" unfolding isometry_def isometry_on_def using assms by auto lemma assumes "isometry_on X f" shows isometry_on_lipschitz: "1-lipschitz_on X f" and isometry_on_uniformly_continuous: "uniformly_continuous_on X f" and isometry_on_continuous: "continuous_on X f" proof - show "1-lipschitz_on X f" apply (rule lipschitz_onI) using isometry_onD[OF assms] by auto then show "uniformly_continuous_on X f" "continuous_on X f" using lipschitz_on_uniformly_continuous lipschitz_on_continuous_on by auto qed lemma isometryD: assumes "isometry f" shows "isometry_on UNIV f" "dist (f x) (f y) = dist x y" "range f = UNIV" "1-lipschitz_on UNIV f" "uniformly_continuous_on UNIV f" "continuous_on UNIV f" using assms unfolding isometry_def isometry_on_def apply auto using isometry_on_lipschitz isometry_on_uniformly_continuous isometry_on_continuous assms unfolding isometry_def by blast+ lemma isometry_on_injective: assumes "isometry_on X f" shows "inj_on f X" using assms inj_on_def isometry_on_def by force lemma isometry_on_compose: assumes "isometry_on X f" "isometry_on (f`X) g" shows "isometry_on X (λx. g(f x))" using assms unfolding isometry_on_def by auto lemma isometry_on_cong: assumes "isometry_on X f" "⋀x. x ∈ X ⟹ g x = f x" shows "isometry_on X g" using assms unfolding isometry_on_def by auto lemma isometry_on_inverse: assumes "isometry_on X f" shows "isometry_on (f`X) (inv_into X f)" "⋀x. x ∈ X ⟹ (inv_into X f) (f x) = x" "⋀y. y ∈ f`X ⟹ f (inv_into X f y) = y" "bij_betw f X (f`X)" proof - show *: "bij_betw f X (f`X)" using assms unfolding bij_betw_def inj_on_def isometry_on_def by force show "isometry_on (f`X) (inv_into X f)" using assms unfolding isometry_on_def by (auto) (metis (mono_tags, lifting) dist_eq_0_iff inj_on_def inv_into_f_f) fix x assume "x ∈ X" then show "(inv_into X f) (f x) = x" using * by (simp add: bij_betw_def) next fix y assume "y ∈ f`X" then show "f (inv_into X f y) = y" by (simp add: f_inv_into_f) qed lemma isometry_inverse: assumes "isometry f" shows "isometry (inv f)" "bij f" using isometry_on_inverse[OF isometryD(1)[OF assms]] isometryD(3)[OF assms] unfolding isometry_def by (auto simp add: bij_imp_bij_inv bij_is_surj) lemma isometry_on_homeomorphism: assumes "isometry_on X f" shows "homeomorphism X (f`X) f (inv_into X f)" "homeomorphism_on X f" "X homeomorphic f`X" proof - show *: "homeomorphism X (f`X) f (inv_into X f)" apply (rule homeomorphismI) using uniformly_continuous_imp_continuous[OF isometry_on_uniformly_continuous] isometry_on_inverse[OF assms] assms by auto then show "X homeomorphic f`X" unfolding homeomorphic_def by auto show "homeomorphism_on X f" unfolding homeomorphism_on_def using * by auto qed lemma isometry_homeomorphism: fixes f::"('a::metric_space) ⇒ ('b::metric_space)" assumes "isometry f" shows "homeomorphism UNIV UNIV f (inv f)" "(UNIV::'a set) homeomorphic (UNIV::'b set)" using isometry_on_homeomorphism[OF isometryD(1)[OF assms]] isometryD(3)[OF assms] by auto lemma isometry_on_closure: assumes "isometry_on X f" "continuous_on (closure X) f" shows "isometry_on (closure X) f" proof (rule isometry_onI) fix x y assume "x ∈ closure X" "y ∈ closure X" obtain u v::"nat ⇒ 'a" where *: "⋀n. u n ∈ X" "u ⇢ x" "⋀n. v n ∈ X" "v ⇢ y" using ‹x ∈ closure X› ‹y ∈ closure X› unfolding closure_sequential by blast have "(λn. f (u n)) ⇢ f x" using *(1) *(2) ‹x ∈ closure X› ‹continuous_on (closure X) f› unfolding comp_def continuous_on_closure_sequentially[of X f] by auto moreover have "(λn. f (v n)) ⇢ f y" using *(3) *(4) ‹y ∈ closure X› ‹continuous_on (closure X) f› unfolding comp_def continuous_on_closure_sequentially[of X f] by auto ultimately have "(λn. dist (f (u n)) (f (v n))) ⇢ dist (f x) (f y)" by (simp add: tendsto_dist) then have "(λn. dist (u n) (v n)) ⇢ dist (f x) (f y)" using assms(1) *(1) *(3) unfolding isometry_on_def by auto moreover have "(λn. dist (u n) (v n)) ⇢ dist x y" using *(2) *(4) by (simp add: tendsto_dist) ultimately show "dist (f x) (f y) = dist x y" using LIMSEQ_unique by auto qed lemma isometry_extend_closure: fixes f::"('a::metric_space) ⇒ ('b::complete_space)" assumes "isometry_on X f" shows "∃g. isometry_on (closure X) g ∧ (∀x∈X. g x = f x)" proof - obtain g where g: "⋀x. x ∈ X ⟹ g x = f x" "uniformly_continuous_on (closure X) g" using uniformly_continuous_on_extension_on_closure[OF isometry_on_uniformly_continuous[OF assms]] by metis have "isometry_on (closure X) g" apply (rule isometry_on_closure, rule isometry_on_cong[OF assms]) using g uniformly_continuous_imp_continuous[OF g(2)] by auto then show ?thesis using g(1) by auto qed lemma isometry_on_complete_image: assumes "isometry_on X f" "complete X" shows "complete (f`X)" proof (rule completeI) fix u :: "nat ⇒ 'b" assume u: "∀n. u n ∈ f`X" "Cauchy u" define v where "v = (λn. inv_into X f (u n))" have "v n ∈ X" for n unfolding v_def by (simp add: inv_into_into u(1)) have "dist (v n) (v m) = dist (u n) (u m)" for m n using u(1) isometry_on_inverse[OF ‹isometry_on X f›] unfolding isometry_on_def v_def by (auto simp add: inv_into_into) then have "Cauchy v" using u(2) unfolding Cauchy_def by auto obtain l where "l ∈ X" "v ⇢ l" apply (rule completeE[OF ‹complete X› _ ‹Cauchy v›]) using ‹⋀n. v n ∈ X› by auto have "(λn. f (v n)) ⇢ f l" apply (rule continuous_on_tendsto_compose[OF isometry_on_continuous[OF ‹isometry_on X f›]]) using ‹⋀n. v n ∈ X› ‹l ∈ X› ‹v ⇢ l› by auto moreover have "f(v n) = u n" for n unfolding v_def by (simp add: f_inv_into_f u(1)) ultimately have "u ⇢ f l" by auto then show "∃m ∈ f`X. u ⇢ m" using ‹l ∈ X› by auto qed lemma isometry_on_id [simp]: "isometry_on A (λx. x)" "isometry_on A id" unfolding isometry_on_def by auto lemma isometry_on_add [simp]: "isometry_on A (λx. x + (t::'a::real_normed_vector))" unfolding isometry_on_def by auto lemma isometry_on_minus [simp]: "isometry_on A (λ(x::'a::real_normed_vector). -x)" unfolding isometry_on_def by (auto simp add: dist_minus) lemma isometry_on_diff [simp]: "isometry_on A (λx. (t::'a::real_normed_vector) - x)" unfolding isometry_on_def by (auto, metis add_uminus_conv_diff dist_add_cancel dist_minus) lemma isometry_preserves_bounded: assumes "isometry_on X f" "A ⊆ X" shows "bounded (f`A) ⟷ bounded A" unfolding bounded_two_points using assms(2) isometry_onD[OF assms(1)] by auto (metis assms(2) rev_subsetD)+ lemma isometry_preserves_infdist: "infdist (f x) (f`A) = infdist x A" if "isometry_on X f" "A ⊆ X" "x ∈ X" using that by (simp add: infdist_def image_comp isometry_on_def subset_iff) lemma isometry_preserves_hausdorff_distance: "hausdorff_distance (f`A) (f`B) = hausdorff_distance A B" if "isometry_on X f" "A ⊆ X" "B ⊆ X" using that isometry_preserves_infdist [OF that(1) that(2)] isometry_preserves_infdist [OF that(1) that(3)] isometry_preserves_bounded [OF that(1) that(2)] isometry_preserves_bounded [OF that(1) that(3)] by (simp add: hausdorff_distance_def image_comp subset_eq) lemma isometry_on_UNIV_iterates: fixes f::"('a::metric_space) ⇒ 'a" assumes "isometry_on UNIV f" shows "isometry_on UNIV (f^^n)" by (induction n, auto, rule isometry_on_compose[of _ _ f], auto intro: isometry_on_subset[OF assms]) lemma isometry_iterates: fixes f::"('a::metric_space) ⇒ 'a" assumes "isometry f" shows "isometry (f^^n)" using isometry_on_UNIV_iterates[OF isometryD(1)[OF assms], of n] bij_fn[OF isometry_inverse(2)[OF assms], of n] unfolding isometry_def by (simp add: bij_is_surj) section ‹Geodesic spaces› text ‹A geodesic space is a metric space in which any pair of points can be joined by a geodesic segment, i.e., an isometrically embedded copy of a segment in the real line. Most spaces in geometry are geodesic. We introduce in this section the corresponding class of metric spaces. First, we study properties of general geodesic segments in metric spaces.› subsection ‹Geodesic segments in general metric spaces› definition geodesic_segment_between::"('a::metric_space) set ⇒ 'a ⇒ 'a ⇒ bool" where "geodesic_segment_between G x y = (∃g::(real ⇒ 'a). g 0 = x ∧ g (dist x y) = y ∧ isometry_on {0..dist x y} g ∧ G = g`{0..dist x y})" definition geodesic_segment::"('a::metric_space) set ⇒ bool" where "geodesic_segment G = (∃x y. geodesic_segment_between G x y)" text ‹We also introduce the parametrization of a geodesic segment. It is convenient to use the following definition, which guarantees that the point is on $G$ even without checking that $G$ is a geodesic segment or that the parameter is in the reasonable range: this shortens some arguments below.› definition geodesic_segment_param::"('a::metric_space) set ⇒ 'a ⇒ real ⇒ 'a" where "geodesic_segment_param G x t = (if ∃w. w ∈ G ∧ dist x w = t then SOME w. w ∈ G ∧ dist x w = t else SOME w. w ∈ G)" lemma geodesic_segment_betweenI: assumes "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" shows "geodesic_segment_between G x y" unfolding geodesic_segment_between_def apply (rule exI[of _ g]) using assms by auto lemma geodesic_segmentI [intro, simp]: assumes "geodesic_segment_between G x y" shows "geodesic_segment G" unfolding geodesic_segment_def using assms by auto lemma geodesic_segmentI2 [intro]: assumes "isometry_on {a..b} g" "a ≤ (b::real)" shows "geodesic_segment_between (g`{a..b}) (g a) (g b)" "geodesic_segment (g`{a..b})" proof - define h where "h = (λt. g (t+a))" have *: "isometry_on {0..b-a} h" apply (rule isometry_onI) using ‹isometry_on {a..b} g› ‹a ≤ b› by (auto simp add: isometry_on_def h_def) have **: "dist (h 0) (h (b-a)) = b-a" using isometry_onD[OF ‹isometry_on {0..b-a} h›, of 0 "b-a"] ‹a ≤ b› unfolding dist_real_def by auto have "geodesic_segment_between (h`{0..b-a}) (h 0) (h (b-a))" unfolding geodesic_segment_between_def apply (rule exI[of _ h]) unfolding ** using * by auto moreover have "g`{a..b} = h`{0..b-a}" unfolding h_def apply (auto simp add: image_iff) by (metis add.commute atLeastAtMost_iff diff_ge_0_iff_ge diff_right_mono le_add_diff_inverse) moreover have "h 0 = g a" "h (b-a) = g b" unfolding h_def by auto ultimately show "geodesic_segment_between (g`{a..b}) (g a) (g b)" by auto then show "geodesic_segment (g`{a..b})" unfolding geodesic_segment_def by auto qed lemma geodesic_segmentD: assumes "geodesic_segment_between G x y" shows "∃g::(real ⇒ _). (g t = x ∧ g (t + dist x y) = y ∧ isometry_on {t..t+dist x y} g ∧ G = g`{t..t+dist x y})" proof - obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "G = h`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) have * [simp]: "(λx. x - t) ` {t..t + dist x y} = {0..dist x y}" by auto define g where "g = (λs. h (s - t))" have "g t = x" "g (t + dist x y) = y" using h assms(1) unfolding g_def by auto moreover have "isometry_on {t..t+dist x y} g" unfolding g_def apply (rule isometry_on_compose[of _ _ h]) by (simp add: dist_real_def isometry_on_def, simp add: h(3)) moreover have "g` {t..t + dist x y} = G" unfolding g_def h(4) using * by (metis image_image) ultimately show ?thesis by auto qed lemma geodesic_segment_endpoints [simp]: assumes "geodesic_segment_between G x y" shows "x ∈ G" "y ∈ G" "G ≠ {}" using assms unfolding geodesic_segment_between_def by (auto, metis atLeastAtMost_iff image_eqI less_eq_real_def zero_le_dist) lemma geodesic_segment_commute: assumes "geodesic_segment_between G x y" shows "geodesic_segment_between G y x" proof - obtain g::"real⇒'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) define h::"real⇒'a" where "h = (λt. g(dist x y-t))" have "(λt. dist x y -t)`{0..dist x y} = {0..dist x y}" by auto then have "h`{0..dist x y} = G" unfolding g(4) h_def by (metis image_image) moreover have "h 0 = y" "h (dist x y) = x" unfolding h_def using g by auto moreover have "isometry_on {0..dist x y} h" unfolding h_def apply (rule isometry_on_compose[of _ _ g]) using g(3) by auto ultimately show ?thesis unfolding geodesic_segment_between_def by (auto simp add: dist_commute) qed lemma geodesic_segment_dist: assumes "geodesic_segment_between G x y" "a ∈ G" shows "dist x a + dist a y = dist x y" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain t where t: "t ∈ {0..dist x y}" "a = g t" using g(4) assms by auto have "dist x a = t" using isometry_onD[OF g(3) _ t(1), of 0] unfolding g(1) dist_real_def t(2) using t(1) by auto moreover have "dist a y = dist x y - t" using isometry_onD[OF g(3) _ t(1), of "dist x y"] unfolding g(2) dist_real_def t(2) using t(1) by (auto simp add: dist_commute) ultimately show ?thesis by auto qed lemma geodesic_segment_dist_unique: assumes "geodesic_segment_between G x y" "a ∈ G" "b ∈ G" "dist x a = dist x b" shows "a = b" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain ta where ta: "ta ∈ {0..dist x y}" "a = g ta" using g(4) assms by auto have *: "dist x a = ta" unfolding g(1)[symmetric] ta(2) using isometry_onD[OF g(3), of 0 ta] unfolding dist_real_def using ta(1) by auto obtain tb where tb: "tb ∈ {0..dist x y}" "b = g tb" using g(4) assms by auto have "dist x b = tb" unfolding g(1)[symmetric] tb(2) using isometry_onD[OF g(3), of 0 tb] unfolding dist_real_def using tb(1) by auto then have "ta = tb" using * ‹dist x a = dist x b› by auto then show "a = b" using ta(2) tb(2) by auto qed lemma geodesic_segment_union: assumes "dist x z = dist x y + dist y z" "geodesic_segment_between G x y" "geodesic_segment_between H y z" shows "geodesic_segment_between (G ∪ H) x z" "G ∩ H = {y}" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain h where h: "h (dist x y) = y" "h (dist x z) = z" "isometry_on {dist x y..dist x z} h" "H = h`{dist x y..dist x z}" unfolding ‹dist x z = dist x y + dist y z› using geodesic_segmentD[OF ‹geodesic_segment_between H y z›, of "dist x y"] by auto define f where "f = (λt. if t ≤ dist x y then g t else h t)" have fg: "f t = g t" if "t ≤ dist x y" for t unfolding f_def using that by auto have fh: "f t = h t" if "t ≥ dist x y" for t unfolding f_def apply (cases "t > dist x y") using that g(2) h(1) by auto have "f 0 = x" "f (dist x z) = z" using fg fh g(1) h(2) assms(1) by auto have "f`{0..dist x z} = f`{0..dist x y} ∪ f`{dist x y..dist x z}" unfolding assms(1) image_Un[symmetric] by (simp add: ivl_disj_un_two_touch(4)) moreover have "f`{0..dist x y} = G" unfolding g(4) using fg image_cong by force moreover have "f`{dist x y..dist x z} = H" unfolding h(4) using fh image_cong by force ultimately have "f`{0..dist x z} = G ∪ H" by simp have Ifg: "dist (f s) (f t) = s-t" if "0 ≤ t" "t ≤ s" "s ≤ dist x y" for s t using that fg[of s] fg[of t] isometry_onD[OF g(3), of s t] unfolding dist_real_def by auto have Ifh: "dist (f s) (f t) = s-t" if "dist x y ≤ t" "t ≤ s" "s ≤ dist x z" for s t using that fh[of s] fh[of t] isometry_onD[OF h(3), of s t] unfolding dist_real_def by auto have I: "dist (f s) (f t) = s-t" if "0 ≤ t" "t ≤ s" "s ≤ dist x z" for s t proof - consider "t ≤ dist x y ∧ s ≥ dist x y" | "s ≤ dist x y" | "t ≥ dist x y" by fastforce then show ?thesis proof (cases) case 1 have "dist (f t) (f s) ≤ dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)" using dist_triangle by auto also have "... ≤ (dist x y - t) + (s - dist x y)" using that 1 Ifg[of t "dist x y"] Ifh[of "dist x y" s] by (auto simp add: dist_commute intro: mono_intros) finally have *: "dist (f t) (f s) ≤ s - t" by simp have "dist x z ≤ dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))" unfolding ‹f 0 = x› ‹f (dist x z) = z› using dist_triangle4 by auto also have "... ≤ t + dist (f t) (f s) + (dist x z - s)" using that 1 Ifg[of 0 t] Ifh[of s "dist x z"] by (auto simp add: dist_commute intro: mono_intros) finally have "s - t ≤ dist (f t) (f s)" by auto then show "dist (f s) (f t) = s-t" using * dist_commute by auto next case 2 then show ?thesis using Ifg that by auto next case 3 then show ?thesis using Ifh that by auto qed qed have "isometry_on {0..dist x z} f" unfolding isometry_on_def dist_real_def using I by (auto, metis abs_of_nonneg dist_commute dist_real_def le_cases zero_le_dist) then show "geodesic_segment_between (G ∪ H) x z" unfolding geodesic_segment_between_def using ‹f 0 = x› ‹f (dist x z) = z› ‹f`{0..dist x z} = G ∪ H› by auto have "G ∩ H ⊆ {y}" proof (auto) fix a assume a: "a ∈ G" "a ∈ H" obtain s where s: "s ∈ {0..dist x y}" "a = g s" using a g(4) by auto obtain t where t: "t ∈ {dist x y..dist x z}" "a = h t" using a h(4) by auto have "a = f s" using fg s by auto moreover have "a = f t" using fh t by auto ultimately have "s = t" using isometry_onD[OF ‹isometry_on {0..dist x z} f›, of s t] s(1) t(1) by auto then have "s = dist x y" using s t by auto then show "a = y" using s(2) g by auto qed then show "G ∩ H = {y}" using assms by auto qed lemma geodesic_segment_dist_le: assumes "geodesic_segment_between G x y" "a ∈ G" "b ∈ G" shows "dist a b ≤ dist x y" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain s t where st: "s ∈ {0..dist x y}" "t ∈ {0..dist x y}" "a = g s" "b = g t" using g(4) assms by auto have "dist a b = abs(s-t)" using isometry_onD[OF g(3) st(1) st(2)] unfolding st(3) st(4) dist_real_def by simp then show "dist a b ≤ dist x y" using st(1) st(2) unfolding dist_real_def by auto qed lemma geodesic_segment_param [simp]: assumes "geodesic_segment_between G x y" shows "geodesic_segment_param G x 0 = x" "geodesic_segment_param G x (dist x y) = y" "t ∈ {0..dist x y} ⟹ geodesic_segment_param G x t ∈ G" "isometry_on {0..dist x y} (geodesic_segment_param G x)" "(geodesic_segment_param G x)`{0..dist x y} = G" "t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param G x t) = t" "s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)" "z ∈ G ⟹ z = geodesic_segment_param G x (dist x z)" proof - obtain g::"real⇒'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) have *: "g t ∈ G ∧ dist x (g t) = t" if "t ∈ {0..dist x y}" for t using isometry_onD[OF g(3), of 0 t] that g(1) g(4) unfolding dist_real_def by auto have G: "geodesic_segment_param G x t = g t" if "t ∈ {0..dist x y}" for t proof - have A: "geodesic_segment_param G x t ∈ G ∧ dist x (geodesic_segment_param G x t) = t" using *[OF that] unfolding geodesic_segment_param_def apply auto using *[OF that] by (metis (mono_tags, lifting) someI)+ obtain s where s: "geodesic_segment_param G x t = g s" "s ∈ {0..dist x y}" using A g(4) by auto have "s = t" using *[OF ‹s ∈ {0..dist x y}›] A unfolding s(1) by auto then show ?thesis using s by auto qed show "geodesic_segment_param G x 0 = x" "geodesic_segment_param G x (dist x y) = y" "t ∈ {0..dist x y} ⟹ geodesic_segment_param G x t ∈ G" "isometry_on {0..dist x y} (geodesic_segment_param G x)" "(geodesic_segment_param G x)`{0..dist x y} = G" "t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param G x t) = t" "s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)" "z ∈ G ⟹ z = geodesic_segment_param G x (dist x z)" using G g apply (auto simp add: rev_image_eqI) using G isometry_on_cong * atLeastAtMost_iff apply blast using G isometry_on_cong * atLeastAtMost_iff apply blast by (auto simp add: * dist_real_def isometry_onD) qed lemma geodesic_segment_param_in_segment: assumes "G ≠ {}" shows "geodesic_segment_param G x t ∈ G" unfolding geodesic_segment_param_def apply (auto, metis (mono_tags, lifting) someI) using assms some_in_eq by fastforce lemma geodesic_segment_reverse_param: assumes "geodesic_segment_between G x y" "t ∈ {0..dist x y}" shows "geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t" proof - have * [simp]: "geodesic_segment_between G y x" using geodesic_segment_commute[OF assms(1)] by simp have "geodesic_segment_param G y (dist x y - t) ∈ G" apply (rule geodesic_segment_param(3)[of _ _ x]) using assms(2) by (auto simp add: dist_commute) moreover have "dist (geodesic_segment_param G y (dist x y - t)) x = t" using geodesic_segment_param(2)[OF *] geodesic_segment_param(7)[OF *, of "dist x y -t" "dist x y"] assms(2) by (auto simp add: dist_commute) moreover have "geodesic_segment_param G x t ∈ G" apply (rule geodesic_segment_param(3)[OF assms(1)]) using assms(2) by auto moreover have "dist (geodesic_segment_param G x t) x = t" using geodesic_segment_param(6)[OF assms] by (simp add: dist_commute) ultimately show ?thesis using geodesic_segment_dist_unique[OF assms(1)] by (simp add: dist_commute) qed lemma dist_along_geodesic_wrt_endpoint: assumes "geodesic_segment_between G x y" "u ∈ G" "v ∈ G" shows "dist u v = abs(dist u x - dist v x)" proof - have *: "u = geodesic_segment_param G x (dist x u)" "v = geodesic_segment_param G x (dist x v)" using assms by auto have "dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))" using * by auto also have "... = abs(dist x u - dist x v)" apply (rule geodesic_segment_param(7)[OF assms(1)]) using assms apply auto using geodesic_segment_dist_le geodesic_segment_endpoints(1) by blast+ finally show ?thesis by (simp add: dist_commute) qed text ‹One often needs to restrict a geodesic segment to a subsegment. We introduce the tools to express this conveniently.› definition geodesic_subsegment::"('a::metric_space) set ⇒ 'a ⇒ real ⇒ real ⇒ 'a set" where "geodesic_subsegment G x s t = G ∩ {z. dist x z ≥ s ∧ dist x z ≤ t}" text ‹A subsegment is always contained in the original segment.› lemma geodesic_subsegment_subset: "geodesic_subsegment G x s t ⊆ G" unfolding geodesic_subsegment_def by simp text ‹A subsegment is indeed a geodesic segment, and its endpoints and parametrization can be expressed in terms of the original segment.› lemma geodesic_subsegment: assumes "geodesic_segment_between G x y" "0 ≤ s" "s ≤ t" "t ≤ dist x y" shows "geodesic_subsegment G x s t = (geodesic_segment_param G x)`{s..t}" "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)" "⋀u. s ≤ u ⟹ u ≤ t ⟹ geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u" proof - show A: "geodesic_subsegment G x s t = (geodesic_segment_param G x)`{s..t}" proof (auto) fix y assume y: "y ∈ geodesic_subsegment G x s t" have "y = geodesic_segment_param G x (dist x y)" apply (rule geodesic_segment_param(8)[OF assms(1)]) using y geodesic_subsegment_subset by force moreover have "dist x y ≥ s ∧ dist x y ≤ t" using y unfolding geodesic_subsegment_def by auto ultimately show "y ∈ geodesic_segment_param G x ` {s..t}" by auto next fix u assume H: "s ≤ u" "u ≤ t" have *: "dist x (geodesic_segment_param G x u) = u" apply (rule geodesic_segment_param(6)[OF assms(1)]) using H assms by auto show "geodesic_segment_param G x u ∈ geodesic_subsegment G x s t" unfolding geodesic_subsegment_def using geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF assms(1)]] by (auto simp add: * H) qed have *: "isometry_on {s..t} (geodesic_segment_param G x)" by (rule isometry_on_subset[of "{0..dist x y}"]) (auto simp add: assms) show B: "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)" unfolding A apply (rule geodesic_segmentI2) using * assms by auto fix u assume u: "s ≤ u" "u ≤ t" show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u" proof (rule geodesic_segment_dist_unique[OF B]) show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) ∈ geodesic_subsegment G x s t" by (rule geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF B]]) show "geodesic_segment_param G x u ∈ geodesic_subsegment G x s t" unfolding A using u by auto have "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s" using B assms u by auto moreover have "dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u -s" using assms u by auto ultimately show "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)" by simp qed qed text ‹The parameterizations of a segment and a subsegment sharing an endpoint coincide where defined.› lemma geodesic_segment_subparam: assumes "geodesic_segment_between G x z" "geodesic_segment_between H x y" "H ⊆ G" "t ∈ {0..dist x y}" shows "geodesic_segment_param G x t = geodesic_segment_param H x t" proof - have "geodesic_segment_param H x t ∈ G" using assms(3) geodesic_segment_param(3)[OF assms(2) assms(4)] by auto then have "geodesic_segment_param H x t = geodesic_segment_param G x (dist x (geodesic_segment_param H x t))" using geodesic_segment_param(8)[OF assms(1)] by auto then show ?thesis using geodesic_segment_param(6)[OF assms(2) assms(4)] by auto qed text ‹A segment contains a subsegment between any of its points› lemma geodesic_subsegment_exists: assumes "geodesic_segment G" "x ∈ G" "y ∈ G" shows "∃H. H ⊆ G ∧ geodesic_segment_between H x y" proof - obtain a0 b0 where Ga0b0: "geodesic_segment_between G a0 b0" using assms(1) unfolding geodesic_segment_def by auto text ‹Permuting the endpoints if necessary, we can ensure that the first endpoint $a$ is closer to $x$ than $y$.› have "∃ a b. geodesic_segment_between G a b ∧ dist x a ≤ dist y a" proof (cases "dist x a0 ≤ dist y a0") case True show ?thesis apply (rule exI[of _ a0], rule exI[of _ b0]) using True Ga0b0 by auto next case False show ?thesis apply (rule exI[of _ b0], rule exI[of _ a0]) using Ga0b0 geodesic_segment_commute geodesic_segment_dist[OF Ga0b0 ‹x ∈ G›] geodesic_segment_dist[OF Ga0b0 ‹y ∈ G›] False by (auto simp add: dist_commute) qed then obtain a b where Gab: "geodesic_segment_between G a b" "dist x a ≤ dist y a" by auto have *: "0 ≤ dist x a" "dist x a ≤ dist y a" "dist y a ≤ dist a b" using Gab assms by (meson geodesic_segment_dist_le geodesic_segment_endpoints(1) zero_le_dist)+ have **: "x = geodesic_segment_param G a (dist x a)" "y = geodesic_segment_param G a (dist y a)" using Gab ‹x ∈ G› ‹y ∈ G› by (metis dist_commute geodesic_segment_param(8))+ define H where "H = geodesic_subsegment G a (dist x a) (dist y a)" have "H ⊆ G" unfolding H_def by (rule geodesic_subsegment_subset) moreover have "geodesic_segment_between H x y" unfolding H_def using geodesic_subsegment(2)[OF Gab(1) *] ** by auto ultimately show ?thesis by auto qed text ‹A geodesic segment is homeomorphic to an interval.› lemma geodesic_segment_homeo_interval: assumes "geodesic_segment_between G x y" shows "{0..dist x y} homeomorphic G" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) show ?thesis using isometry_on_homeomorphism(3)[OF g(3)] unfolding g(4) by simp qed text ‹Just like an interval, a geodesic segment is compact, connected, path connected, bounded, closed, nonempty, and proper.› lemma geodesic_segment_topology: assumes "geodesic_segment G" shows "compact G" "connected G" "path_connected G" "bounded G" "closed G" "G ≠ {}" "proper G" proof - show "compact G" using assms geodesic_segment_homeo_interval homeomorphic_compactness unfolding geodesic_segment_def by force show "path_connected G" using assms is_interval_path_connected geodesic_segment_homeo_interval homeomorphic_path_connectedness unfolding geodesic_segment_def by (metis is_interval_cc) then show "connected G" using path_connected_imp_connected by auto show "bounded G" by (rule compact_imp_bounded, fact) show "closed G" by (rule compact_imp_closed, fact) show "G ≠ {}" using assms geodesic_segment_def geodesic_segment_endpoints(3) by auto show "proper G" using proper_of_compact ‹compact G› by auto qed lemma geodesic_segment_between_x_x [simp]: "geodesic_segment_between {x} x x" "geodesic_segment {x}" "geodesic_segment_between G x x ⟷ G = {x}" proof - show *: "geodesic_segment_between {x} x x" unfolding geodesic_segment_between_def apply (rule exI[of _ "λ_. x"]) unfolding isometry_on_def by auto then show "geodesic_segment {x}" by auto show "geodesic_segment_between G x x ⟷ G = {x}" using geodesic_segment_dist_le geodesic_segment_endpoints(2) * by fastforce qed lemma geodesic_segment_disconnection: assumes "geodesic_segment_between G x y" "z ∈ G" shows "(connected (G - {z})) = (z = x ∨ z = y)" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain t where t: "t ∈ {0..dist x y}" "z = g t" using ‹z ∈ G› g(4) by auto have "({0..dist x y} - {t}) homeomorphic (G - {g t})" proof - have *: "isometry_on ({0..dist x y} - {t}) g" apply (rule isometry_on_subset[OF g(3)]) by auto have "({0..dist x y} - {t}) homeomorphic g`({0..dist x y} - {t})" by (rule isometry_on_homeomorphism(3)[OF *]) moreover have "g`({0..dist x y} - {t}) = G - {g t}" unfolding g(4) using isometry_on_injective[OF g(3)] t by (auto simp add: inj_onD) ultimately show ?thesis by auto qed moreover have "connected({0..dist x y} - {t}) = (t = 0 ∨ t = dist x y)" using t(1) by (auto simp add: connected_iff_interval, fastforce) ultimately have "connected (G - {z}) = (t = 0 ∨ t = dist x y)" unfolding ‹z = g t›[symmetric]using homeomorphic_connectedness by blast moreover have "(t = 0 ∨ t = dist x y) = (z = x ∨ z = y)" using t g apply auto by (metis atLeastAtMost_iff isometry_on_inverse(2) order_refl zero_le_dist)+ ultimately show ?thesis by auto qed lemma geodesic_segment_unique_endpoints: assumes "geodesic_segment_between G x y" "geodesic_segment_between G a b" shows "{x, y} = {a, b}" by (metis geodesic_segment_disconnection assms(1) assms(2) doubleton_eq_iff geodesic_segment_endpoints(1) geodesic_segment_endpoints(2)) lemma geodesic_segment_subsegment: assumes "geodesic_segment G" "H ⊆ G" "compact H" "connected H" "H ≠ {}" shows "geodesic_segment H" proof - obtain x y where "geodesic_segment_between G x y" using assms unfolding geodesic_segment_def by auto obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) define L where "L = (inv_into {0..dist x y} g)`H" have "L ⊆ {0..dist x y}" unfolding L_def using isometry_on_inverse[OF ‹isometry_on {0..dist x y} g›] assms(2) g(4) by auto have "isometry_on G (inv_into {0..dist x y} g)" using isometry_on_inverse[OF ‹isometry_on {0..dist x y} g›] g(4) by auto then have "isometry_on H (inv_into {0..dist x y} g)" using ‹H ⊆ G› isometry_on_subset by auto then have "H homeomorphic L" unfolding L_def using isometry_on_homeomorphism(3) by auto then have "compact L ∧ connected L" using assms homeomorphic_compactness homeomorphic_connectedness by blast then obtain a b where "L = {a..b}" using connected_compact_interval_1[of L] by auto have "a ≤ b" using ‹H ≠ {}› ‹L = {a..b}› unfolding L_def by auto then have "0 ≤ a" "b ≤ dist x y" using ‹L ⊆ {0..dist x y}› ‹L = {a..b}› by auto have *: "H = g`{a..b}" by (metis L_def ‹L = {a..b}› assms(2) g(4) image_inv_into_cancel) show "geodesic_segment H" unfolding * apply (rule geodesic_segmentI2[OF _ ‹a ≤ b›]) apply (rule isometry_on_subset[OF g(3)]) using ‹0 ≤ a› ‹b ≤ dist x y› by auto qed text ‹The image under an isometry of a geodesic segment is still obviously a geodesic segment.› lemma isometry_preserves_geodesic_segment_between: assumes "isometry_on X f" "G ⊆ X" "geodesic_segment_between G x y" shows "geodesic_segment_between (f`G) (f x) (f y)" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) then have *: "f`G = (f o g) `{0..dist x y}" "f x = (f o g) 0" "f y = (f o g) (dist x y)" by auto show ?thesis unfolding * apply (intro geodesic_segmentI2(1)) unfolding comp_def apply (rule isometry_on_compose[of _ g]) using g(3) g(4) assms by (auto intro: isometry_on_subset) qed text ‹The sum of distances $d(w, x) + d(w, y)$ can be controlled using the distance from $w$ to a geodesic segment between $x$ and $y$.› lemma geodesic_segment_distance: assumes "geodesic_segment_between G x y" shows "dist w x + dist w y ≤ dist x y + 2 * infdist w G" proof - have "∃z ∈ G. infdist w G = dist w z" apply (rule infdist_proper_attained) using assms by (auto simp add: geodesic_segment_topology) then obtain z where z: "z ∈ G" "infdist w G = dist w z" by auto have "dist w x + dist w y ≤ (dist w z + dist z x) + (dist w z + dist z y)" by (intro mono_intros) also have "... = dist x z + dist z y + 2 * dist w z" by (auto simp add: dist_commute) also have "... = dist x y + 2 * infdist w G" using z(1) assms geodesic_segment_dist unfolding z(2) by auto finally show ?thesis by auto qed text ‹If a point $y$ is on a geodesic segment between $x$ and its closest projection $p$ on a set $A$, then $p$ is also a closest projection of $y$, and the closest projection set of $y$ is contained in that of $x$.› lemma proj_set_geodesic_same_basepoint: assumes "p ∈ proj_set x A" "geodesic_segment_between G p x" "y ∈ G" shows "p ∈ proj_set y A" proof (rule proj_setI) show "p ∈ A" using assms proj_setD by auto have *: "dist y p ≤ dist y q" if "q ∈ A" for q proof - have "dist p y + dist y x = dist p x" using assms geodesic_segment_dist by blast also have "... ≤ dist q x" using proj_set_dist_le[OF ‹q ∈ A› assms(1)] by (simp add: dist_commute) also have "... ≤ dist q y + dist y x" by (intro mono_intros) finally show ?thesis by (simp add: dist_commute) qed have "dist y p ≤ Inf (dist y ` A)" apply (rule cINF_greatest) using ‹p ∈ A› * by auto then show "dist y p ≤ infdist y A" unfolding infdist_def using ‹p ∈ A› by auto qed lemma proj_set_subset: assumes "p ∈ proj_set x A" "geodesic_segment_between G p x" "y ∈ G" shows "proj_set y A ⊆ proj_set x A" proof - have "z ∈ proj_set x A" if "z ∈ proj_set y A" for z proof (rule proj_setI) show "z ∈ A" using that proj_setD by auto have "dist x z ≤ dist x y + dist y z" by (intro mono_intros) also have "... ≤ dist x y + dist y p" using proj_set_dist_le[OF proj_setD(1)[OF ‹p ∈ proj_set x A›] that] by auto also have "... = dist x p" using assms geodesic_segment_commute geodesic_segment_dist by blast also have "... = infdist x A" using proj_setD(2)[OF assms(1)] by simp finally show "dist x z ≤ infdist x A" by simp qed then show ?thesis by auto qed lemma proj_set_thickening: assumes "p ∈ proj_set x Z" "0 ≤ D" "D ≤ dist p x" "geodesic_segment_between G p x" shows "geodesic_segment_param G p D ∈ proj_set x (⋃z∈Z. cball z D)" proof (rule proj_setI') have "dist p (geodesic_segment_param G p D) = D" using geodesic_segment_param(7)[OF assms(4), of 0 D] unfolding geodesic_segment_param(1)[OF assms(4)] using assms by simp then show "geodesic_segment_param G p D ∈ (⋃z∈Z. cball z D)" using proj_setD(1)[OF ‹p ∈ proj_set x Z›] by force show "dist x (geodesic_segment_param G p D) ≤ dist x y" if "y ∈ (⋃z∈Z. cball z D)" for y proof - obtain z where y: "y ∈ cball z D" "z ∈ Z" using ‹y ∈ (⋃z∈Z. cball z D)› by auto have "dist (geodesic_segment_param G p D) x + D = dist p x" using geodesic_segment_param(7)[OF assms(4), of D "dist p x"] unfolding geodesic_segment_param(2)[OF assms(4)] using assms by simp also have "... ≤ dist z x" using proj_setD(2)[OF ‹p ∈ proj_set x Z›] infdist_le[OF ‹z ∈ Z›, of x] by (simp add: dist_commute) also have "... ≤ dist z y + dist y x" by (intro mono_intros) also have "... ≤ D + dist y x" using y by simp finally show ?thesis by (simp add: dist_commute) qed qed lemma proj_set_thickening': assumes "p ∈ proj_set x Z" "0 ≤ D" "D ≤ E" "E ≤ dist p x" "geodesic_segment_between G p x" shows "geodesic_segment_param G p D ∈ proj_set (geodesic_segment_param G p E) (⋃z∈Z. cball z D)" proof - define H where "H = geodesic_subsegment G p D (dist p x)" have H1: "geodesic_segment_between H (geodesic_segment_param G p D) x" apply (subst geodesic_segment_param(2)[OF ‹geodesic_segment_between G p x›, symmetric]) unfolding H_def apply (rule geodesic_subsegment(2)) using assms by auto have H2: "geodesic_segment_param G p E ∈ H" unfolding H_def using assms geodesic_subsegment(1) by force have "geodesic_segment_param G p D ∈ proj_set x (⋃z∈Z. cball z D)" apply (rule proj_set_thickening) using assms by auto then show ?thesis by (rule proj_set_geodesic_same_basepoint[OF _ H1 H2]) qed text ‹It is often convenient to use \emph{one} geodesic between $x$ and $y$, even if it is not unique. We introduce a notation for such a choice of a geodesic, denoted \verb+{x--S--y}+ for such a geodesic that moreover remains in the set $S$. We also enforce the condition \verb+{x--S--y} = {y--S--x}+. When there is no such geodesic, we simply take \verb+{x--S--y} = {x, y}+ for definiteness. It would be even better to enforce that, if $a$ is on \verb+{x--S--y}+, then \verb+{x--S--y}+ is the union of \verb+{x--S--a}+ and \verb+{a--S--y}+, but I do not know if such a choice is always possible -- such a choice of geodesics is called a geodesic bicombing. We also write \verb+{x--y}+ for \verb+{x--UNIV--y}+.› definition some_geodesic_segment_between::"'a::metric_space ⇒ 'a set ⇒ 'a ⇒ 'a set" ("(1{_--_--_})") where "some_geodesic_segment_between = (SOME f. ∀ x y S. f x S y = f y S x ∧ (if (∃G. geodesic_segment_between G x y ∧ G ⊆ S) then (geodesic_segment_between (f x S y) x y ∧ (f x S y ⊆ S)) else f x S y = {x, y}))" abbreviation some_geodesic_segment_between_UNIV::"'a::metric_space ⇒ 'a ⇒ 'a set" ("(1{_--_})") where "some_geodesic_segment_between_UNIV x y ≡ {x--UNIV--y}" text ‹We prove that there is such a choice of geodesics, compatible with direction reversal. What we do is choose arbitrarily a geodesic between $x$ and $y$ if it exists, and then use the geodesic between $\min(x, y)$ and $\max(x,y)$, for any total order on the space, to ensure that we get the same result from $x$ to $y$ or from $y$ to $x$.› lemma some_geodesic_segment_between_exists: "∃f. ∀ x y S. f x S y = f y S x ∧ (if (∃G. geodesic_segment_between G x y ∧ G ⊆ S) then (geodesic_segment_between (f x S y) x y ∧ (f x S y ⊆ S)) else f x S y = {x, y})" proof - define g::"'a ⇒ 'a set ⇒ 'a ⇒ 'a set" where "g = (λx S y. if (∃G. geodesic_segment_between G x y ∧ G ⊆ S) then (SOME G. geodesic_segment_between G x y ∧ G ⊆ S) else {x, y})" have g1: "geodesic_segment_between (g x S y) x y ∧ (g x S y ⊆ S)" if "∃G. geodesic_segment_between G x y ∧ G ⊆ S" for x y S unfolding g_def using someI_ex[OF that] by auto have g2: "g x S y = {x, y}" if "¬(∃G. geodesic_segment_between G x y ∧ G ⊆ S)" for x y S unfolding g_def using that by auto obtain r::"'a rel" where r: "well_order_on UNIV r" using well_order_on by auto have A: "x = y" if "(x, y) ∈ r" "(y, x) ∈ r" for x y using r that unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def by auto have B: "(x, y) ∈ r ∨ (y, x) ∈ r" for x y using r unfolding well_order_on_def linear_order_on_def total_on_def partial_order_on_def preorder_on_def refl_on_def by force define f where "f = (λx S y. if (x, y) ∈ r then g x S y else g y S x)" have "f x S y = f y S x" for x y S unfolding f_def using r A B by auto moreover have "geodesic_segment_between (f x S y) x y ∧ (f x S y ⊆ S)" if "∃G. geodesic_segment_between G x y ∧ G ⊆ S" for x y S unfolding f_def using g1 geodesic_segment_commute that by smt moreover have "f x S y = {x, y}" if "¬(∃G. geodesic_segment_between G x y ∧ G ⊆ S)" for x y S unfolding f_def using g2 that geodesic_segment_commute doubleton_eq_iff by metis ultimately show ?thesis by metis qed lemma some_geodesic_commute: "{x--S--y} = {y--S--x}" unfolding some_geodesic_segment_between_def by (auto simp add: someI_ex[OF some_geodesic_segment_between_exists]) lemma some_geodesic_segment_description: "(∃G. geodesic_segment_between G x y ∧ G ⊆ S) ⟹ geodesic_segment_between {x--S--y} x y" "(¬(∃G. geodesic_segment_between G x y ∧ G ⊆ S)) ⟹ {x--S--y} = {x, y}" unfolding some_geodesic_segment_between_def by (simp add: someI_ex[OF some_geodesic_segment_between_exists])+ text ‹Basic topological properties of our chosen set of geodesics.› lemma some_geodesic_compact [simp]: "compact {x--S--y}" apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using some_geodesic_segment_description[of x y] geodesic_segment_topology[of "{x--S--y}"] geodesic_segment_def apply auto by blast lemma some_geodesic_closed [simp]: "closed {x--S--y}" by (rule compact_imp_closed[OF some_geodesic_compact[of x S y]]) lemma some_geodesic_bounded [simp]: "bounded {x--S--y}" by (rule compact_imp_bounded[OF some_geodesic_compact[of x S y]]) lemma some_geodesic_endpoints [simp]: "x ∈ {x--S--y}" "y ∈ {x--S--y}" "{x--S--y} ≠ {}" apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using some_geodesic_segment_description[of x y S] apply auto apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using some_geodesic_segment_description[of x y S] apply auto apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using geodesic_segment_endpoints(3) by (auto, blast) lemma some_geodesic_subsegment: assumes "H ⊆ {x--S--y}" "compact H" "connected H" "H ≠ {}" shows "geodesic_segment H" apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using some_geodesic_segment_description[of x y] geodesic_segment_subsegment[OF _ assms] geodesic_segment_def apply auto[1] using some_geodesic_segment_description[of x y] assms by (metis connected_finite_iff_sing finite.emptyI finite.insertI finite_subset geodesic_segment_between_x_x(2)) lemma some_geodesic_in_subset: assumes "x ∈ S" "y ∈ S" shows "{x--S--y} ⊆ S" apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") unfolding some_geodesic_segment_between_def by (simp add: assms someI_ex[OF some_geodesic_segment_between_exists])+ lemma some_geodesic_same_endpoints [simp]: "{x--S--x} = {x}" apply (cases "∃G. geodesic_segment_between G x x ∧ G ⊆ S") apply (meson geodesic_segment_between_x_x(3) some_geodesic_segment_description(1)) by (simp add: some_geodesic_segment_description(2)) subsection ‹Geodesic subsets› text ‹A subset is \emph{geodesic} if any two of its points can be joined by a geodesic segment. We prove basic properties of such a subset in this paragraph -- notably connectedness. A basic example is given by convex subsets of vector spaces, as closed segments are geodesic.› definition geodesic_subset::"('a::metric_space) set ⇒ bool" where "geodesic_subset S = (∀x∈S. ∀y∈S. ∃G. geodesic_segment_between G x y ∧ G ⊆ S)" lemma geodesic_subsetD: assumes "geodesic_subset S" "x ∈ S" "y ∈ S" shows "geodesic_segment_between {x--S--y} x y" using assms some_geodesic_segment_description(1) unfolding geodesic_subset_def by blast lemma geodesic_subsetI: assumes "⋀x y. x ∈ S ⟹ y ∈ S ⟹ ∃G. geodesic_segment_between G x y ∧ G ⊆ S" shows "geodesic_subset S" using assms unfolding geodesic_subset_def by auto lemma geodesic_subset_empty: "geodesic_subset {}" using geodesic_subsetI by auto lemma geodesic_subset_singleton: "geodesic_subset {x}" by (auto intro!: geodesic_subsetI geodesic_segment_between_x_x(1)) lemma geodesic_subset_path_connected: assumes "geodesic_subset S" shows "path_connected S" proof - have "∃g. path g ∧ path_image g ⊆ S ∧ pathstart g = x ∧ pathfinish g = y" if "x ∈ S" "y ∈ S" for x y proof - define G where "G = {x--S--y}" have *: "geodesic_segment_between G x y" "G ⊆ S" "x ∈ G" "y ∈ G" using assms that by (auto simp add: G_def geodesic_subsetD some_geodesic_in_subset that(1) that(2)) then have "path_connected G" using geodesic_segment_topology(3) unfolding geodesic_segment_def by auto then have "∃g. path g ∧ path_image g ⊆ G ∧ pathstart g = x ∧ pathfinish g = y" using * unfolding path_connected_def by auto then show ?thesis using ‹G ⊆ S› by auto qed then show ?thesis unfolding path_connected_def by auto qed text ‹To show that a segment in a normed vector space is geodesic, we will need to use its length parametrization, which is given in the next lemma.› lemma closed_segment_as_isometric_image: "((λt. x + (t/dist x y) *⇩_{R}(y - x))`{0..dist x y}) = closed_segment x y" proof (auto simp add: closed_segment_def image_iff) fix t assume H: "0 ≤ t" "t ≤ dist x y" show "∃u. x + (t / dist x y) *⇩_{R}(y - x) = (1 - u) *⇩_{R}x + u *⇩_{R}y ∧ 0 ≤ u ∧ u ≤ 1" apply (rule exI[of _ "t/dist x y"]) using H apply (auto simp add: algebra_simps divide_simps) apply (metis add_diff_cancel_left' add_diff_eq add_divide_distrib dist_eq_0_iff scaleR_add_left vector_fraction_eq_iff) done next fix u::real assume H: "0 ≤ u" "u ≤ 1" show "∃t∈{0..dist x y}. (1 - u) *⇩_{R}x + u *⇩_{R}y = x + (t / dist x y) *⇩_{R}(y - x)" apply (rule bexI[of _ "u * dist x y"]) using H by (auto simp add: algebra_simps mult_left_le_one_le) qed proposition closed_segment_is_geodesic: fixes x y::"'a::real_normed_vector" shows "isometry_on {0..dist x y} (λt. x + (t/dist x y) *⇩_{R}(y - x))" "geodesic_segment_between (closed_segment x y) x y" "geodesic_segment (closed_segment x y)" proof - show *: "isometry_on {0..dist x y} (λt. x + (t/dist x y) *⇩_{R}(y - x))" unfolding isometry_on_def dist_norm apply (cases "x = y") by (auto simp add: scaleR_diff_left[symmetric] diff_divide_distrib[symmetric] norm_minus_commute) show "geodesic_segment_between (closed_segment x y) x y" unfolding closed_segment_as_isometric_image[symmetric] apply (rule geodesic_segment_betweenI[OF _ _ *]) by auto then show "geodesic_segment (closed_segment x y)" by auto qed text ‹We deduce that a convex set is geodesic.› proposition convex_is_geodesic: assumes "convex (S::'a::real_normed_vector set)" shows "geodesic_subset S" proof (rule geodesic_subsetI) fix x y assume H: "x ∈ S" "y ∈ S" show "∃G. geodesic_segment_between G x y ∧ G ⊆ S" apply (rule exI[of _ "closed_segment x y"]) apply (auto simp add: closed_segment_is_geodesic) using H assms convex_contains_segment by blast qed subsection ‹Geodesic spaces› text ‹In this subsection, we define geodesic spaces (metric spaces in which there is a geodesic segment joining any pair of points). We specialize the previous statements on geodesic segments to these situations.› class geodesic_space = metric_space + assumes geodesic: "geodesic_subset (UNIV::('a::metric_space) set)" text ‹The simplest example of a geodesic space is a real normed vector space. Significant examples also include graphs (with the graph distance), Riemannian manifolds, and $CAT(\kappa)$ spaces.› instance real_normed_vector ⊆ geodesic_space by (standard, simp add: convex_is_geodesic) lemma (in geodesic_space) some_geodesic_is_geodesic_segment [simp]: "geodesic_segment_between {x--y} x (y::'a)" "geodesic_segment {x--y}" using some_geodesic_segment_description(1)[of x y] geodesic_subsetD[OF geodesic] by (auto, blast) lemma (in geodesic_space) some_geodesic_connected [simp]: "connected {x--y}" "path_connected {x--y}" by (auto intro!: geodesic_segment_topology) text ‹In geodesic spaces, we restate as simp rules all properties of the geodesic segment parametrizations.› lemma (in geodesic_space) geodesic_segment_param_in_geodesic_spaces [simp]: "geodesic_segment_param {x--y} x 0 = x" "geodesic_segment_param {x--y} x (dist x y) = y" "t ∈ {0..dist x y} ⟹ geodesic_segment_param {x--y} x t ∈ {x--y}" "isometry_on {0..dist x y} (geodesic_segment_param {x--y} x)" "(geodesic_segment_param {x--y} x)`{0..dist x y} = {x--y}" "t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param {x--y} x t) = t" "s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param {x--y} x s) (geodesic_segment_param {x--y} x t) = abs(s-t)" "z ∈ {x--y} ⟹ z = geodesic_segment_param {x--y} x (dist x z)" using geodesic_segment_param[OF some_geodesic_is_geodesic_segment(1)[of x y]] by auto subsection ‹Uniquely geodesic spaces› text ‹In this subsection, we define uniquely geodesic spaces, i.e., geodesic spaces in which, additionally, there is a unique geodesic between any pair of points.› class uniquely_geodesic_space = geodesic_space + assumes uniquely_geodesic: "⋀x y G H. geodesic_segment_between G x y ⟹ geodesic_segment_between H x y ⟹ G = H" text ‹To prove that a geodesic space is uniquely geodesic, it suffices to show that there is no loop, i.e., if two geodesic segments intersect only at their endpoints, then they coincide. Indeed, assume this holds, and consider two geodesics with the same endpoints. If they differ at some time $t$, then consider the last time $a$ before $t$ where they coincide, and the first time $b$ after $t$ where they coincide. Then the restrictions of the two geodesics to $[a,b]$ give a loop, and a contradiction.› lemma (in geodesic_space) uniquely_geodesic_spaceI: assumes "⋀G H x (y::'a). geodesic_segment_between G x y ⟹ geodesic_segment_between H x y ⟹ G ∩ H = {x, y} ⟹ x = y" "geodesic_segment_between G x y" "geodesic_segment_between H x (y::'a)" shows "G = H" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "H = h`{0..dist x y}" by (meson ‹geodesic_segment_between H x y› geodesic_segment_between_def) have "g t = h t" if "t ∈ {0..dist x y}" for t proof (rule ccontr) assume "g t ≠ h t" define Z where "Z = {s ∈ {0..dist x y}. g s = h s}" have "0 ∈ Z" "dist x y ∈ Z" unfolding Z_def using g h by auto have "t ∉ Z" unfolding Z_def using ‹g t ≠ h t› by