(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) theory Morse_Gromov_Theorem imports "HOL-Decision_Procs.Approximation" Gromov_Hyperbolicity Hausdorff_Distance begin hide_const (open) Approximation.Min hide_const (open) Approximation.Max section ‹Quasiconvexity› text ‹In a Gromov-hyperbolic setting, convexity is not a well-defined notion as everything should be coarse. The good replacement is quasi-convexity: A set $X$ is $C$-quasi-convex if any pair of points in $X$ can be joined by a geodesic that remains within distance $C$ of $X$. One could also require this for all geodesics, up to changing $C$, as two geodesics between the same endpoints remain within uniformly bounded distance. We use the first definition to ensure that a geodesic is $0$-quasi-convex.› definition quasiconvex::"real ⇒ ('a::metric_space) set ⇒ bool" where "quasiconvex C X = (C ≥ 0 ∧ (∀x∈X. ∀y∈X. ∃G. geodesic_segment_between G x y ∧ (∀z∈G. infdist z X ≤ C)))" lemma quasiconvexD: assumes "quasiconvex C X" "x ∈ X" "y ∈ X" shows "∃G. geodesic_segment_between G x y ∧ (∀z∈G. infdist z X ≤ C)" using assms unfolding quasiconvex_def by auto lemma quasiconvexC: assumes "quasiconvex C X" shows "C ≥ 0" using assms unfolding quasiconvex_def by auto lemma quasiconvexI: assumes "C ≥ 0" "⋀x y. x ∈ X ⟹ y ∈ X ⟹ (∃G. geodesic_segment_between G x y ∧ (∀z∈G. infdist z X ≤ C))" shows "quasiconvex C X" using assms unfolding quasiconvex_def by auto lemma quasiconvex_of_geodesic: assumes "geodesic_segment G" shows "quasiconvex 0 G" proof (rule quasiconvexI, simp) fix x y assume *: "x ∈ G" "y ∈ G" obtain H where H: "H ⊆ G" "geodesic_segment_between H x y" using geodesic_subsegment_exists[OF assms(1) *] by auto have "infdist z G ≤ 0" if "z ∈ H" for z using H(1) that by auto then show "∃H. geodesic_segment_between H x y ∧ (∀z∈H. infdist z G ≤ 0)" using H(2) by auto qed lemma quasiconvex_empty: assumes "C ≥ 0" shows "quasiconvex C {}" unfolding quasiconvex_def using assms by auto lemma quasiconvex_mono: assumes "C ≤ D" "quasiconvex C G" shows "quasiconvex D G" using assms unfolding quasiconvex_def by (auto, fastforce) text ‹The $r$-neighborhood of a quasi-convex set is still quasi-convex in a hyperbolic space, for a constant that does not depend on $r$.› lemma (in Gromov_hyperbolic_space_geodesic) quasiconvex_thickening: assumes "quasiconvex C (X::'a set)" "r ≥ 0" shows "quasiconvex (C + 8 *deltaG(TYPE('a))) (⋃x∈X. cball x r)" proof (rule quasiconvexI) show "C + 8 *deltaG(TYPE('a)) ≥ 0" using quasiconvexC[OF assms(1)] by simp next fix y z assume *: "y ∈ (⋃x∈X. cball x r)" "z ∈ (⋃x∈X. cball x r)" have A: "infdist w (⋃x∈X. cball x r) ≤ C + 8 * deltaG TYPE('a)" if "w ∈ {y--z}" for w proof - obtain py where py: "py ∈ X" "y ∈ cball py r" using * by auto obtain pz where pz: "pz ∈ X" "z ∈ cball pz r" using * by auto obtain G where G: "geodesic_segment_between G py pz" "(∀p∈G. infdist p X ≤ C)" using quasiconvexD[OF assms(1) ‹py ∈ X› ‹pz ∈ X›] by auto have A: "infdist w ({y--py} ∪ G ∪ {pz--z}) ≤ 8 * deltaG(TYPE('a))" by (rule thin_quadrilaterals[OF _ G(1) _ _ ‹w ∈ {y--z}›, where ?x = y and ?t = z], auto) have "∃u ∈ {y--py} ∪ G ∪ {pz--z}. infdist w ({y--py} ∪ G ∪ {pz--z}) = dist w u" apply (rule infdist_proper_attained, auto intro!: proper_Un simp add: geodesic_segment_topology(7)) by (meson G(1) geodesic_segmentI geodesic_segment_topology(7)) then obtain u where u: "u ∈ {y--py} ∪ G ∪ {pz--z}" "infdist w ({y--py} ∪ G ∪ {pz--z}) = dist w u" by auto then consider "u ∈ {y--py}" | "u ∈ G" | "u ∈ {pz--z}" by auto then have "infdist u (⋃x∈X. cball x r) ≤ C" proof (cases) case 1 then have "dist py u ≤ dist py y" using geodesic_segment_dist_le local.some_geodesic_is_geodesic_segment(1) some_geodesic_commute some_geodesic_endpoints(1) by blast also have "... ≤ r" using py(2) by auto finally have "u ∈ cball py r" by auto then have "u ∈ (⋃x∈X. cball x r)" using py(1) by auto then have "infdist u (⋃x∈X. cball x r) = 0" by auto then show ?thesis using quasiconvexC[OF assms(1)] by auto next case 3 then have "dist pz u ≤ dist pz z" using geodesic_segment_dist_le local.some_geodesic_is_geodesic_segment(1) some_geodesic_commute some_geodesic_endpoints(1) by blast also have "... ≤ r" using pz(2) by auto finally have "u ∈ cball pz r" by auto then have "u ∈ (⋃x∈X. cball x r)" using pz(1) by auto then have "infdist u (⋃x∈X. cball x r) = 0" by auto then show ?thesis using quasiconvexC[OF assms(1)] by auto next case 2 have "infdist u (⋃x∈X. cball x r) ≤ infdist u X" apply (rule infdist_mono) using assms(2) py(1) by auto then show ?thesis using 2 G(2) by auto qed moreover have "infdist w (⋃x∈X. cball x r) ≤ infdist u (⋃x∈X. cball x r) + dist w u" by (intro mono_intros) ultimately show ?thesis using A u(2) by auto qed show "∃G. geodesic_segment_between G y z ∧ (∀w∈G. infdist w (⋃x∈X. cball x r) ≤ C + 8 * deltaG TYPE('a))" apply (rule exI[of _ "{y--z}"]) using A by auto qed text ‹If $x$ has a projection $p$ on a quasi-convex set $G$, then all segments from a point in $G$ to $x$ go close to $p$, i.e., the triangular inequality $d(x,y) \leq d(x,p) + d(p,y)$ is essentially an equality, up to an additive constant.› lemma (in Gromov_hyperbolic_space_geodesic) dist_along_quasiconvex: assumes "quasiconvex C G" "p ∈ proj_set x G" "y ∈ G" shows "dist x p + dist p y ≤ dist x y + 4 * deltaG(TYPE('a)) + 2 * C" proof - have *: "p ∈ G" using assms proj_setD by auto obtain H where H: "geodesic_segment_between H p y" "⋀q. q ∈ H ⟹ infdist q G ≤ C" using quasiconvexD[OF assms(1) * assms(3)] by auto have "∃m∈H. infdist x H = dist x m" apply (rule infdist_proper_attained[of H x]) using geodesic_segment_topology[OF geodesic_segmentI[OF H(1)]] by auto then obtain m where m: "m ∈ H" "infdist x H = dist x m" by auto then have I: "dist x m ≤ Gromov_product_at x p y + 2 * deltaG(TYPE('a))" using infdist_triangle_side[OF H(1), of x] by auto have "dist x p - dist x m - C ≤ e" if "e > 0" for e proof - have "∃r∈G. dist m r < infdist m G + e" apply (rule infdist_almost_attained) using ‹e > 0› assms(3) by auto then obtain r where r: "r ∈ G" "dist m r < infdist m G + e" by auto then have *: "dist m r ≤ C + e" using H(2)[OF ‹m ∈ H›] by auto have "dist x p ≤ dist x r" using ‹r ∈ G› assms(2) proj_set_dist_le by blast also have "... ≤ dist x m + dist m r" by (intro mono_intros) finally show ?thesis using * by (auto simp add: metric_space_class.dist_commute) qed then have "dist x p - dist x m - C ≤ 0" using dense_ge by blast then show ?thesis using I unfolding Gromov_product_at_def by (auto simp add: algebra_simps divide_simps) qed text ‹The next lemma is~\<^cite>‹‹Proposition 10.2.1› in "coornaert_delzant_papadopoulos"› with better constants. It states that the distance between the projections on a quasi-convex set is controlled by the distance of the original points, with a gain given by the distances of the points to the set.› lemma (in Gromov_hyperbolic_space_geodesic) proj_along_quasiconvex_contraction: assumes "quasiconvex C G" "px ∈ proj_set x G" "py ∈ proj_set y G" shows "dist px py ≤ max (5 * deltaG(TYPE('a)) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG(TYPE('a)) + 4 * C)" proof - have "px ∈ G" "py ∈ G" using assms proj_setD by auto have "(dist x px + dist px py - 4 * deltaG(TYPE('a)) - 2 * C) + (dist y py + dist py px - 4 *deltaG(TYPE('a)) - 2 * C) ≤ dist x py + dist y px" apply (intro mono_intros) using dist_along_quasiconvex[OF assms(1) assms(2) ‹py ∈ G›] dist_along_quasiconvex[OF assms(1) assms(3) ‹px ∈ G›] by auto also have "... ≤ max (dist x y + dist py px) (dist x px + dist py y) + 2 * deltaG(TYPE('a))" by (rule hyperb_quad_ineq) finally have *: "dist x px + dist y py + 2 * dist px py ≤ max (dist x y + dist py px) (dist x px + dist py y) + 10 * deltaG(TYPE('a)) + 4 * C" by (auto simp add: metric_space_class.dist_commute) show ?thesis proof (cases "dist x y + dist py px ≥ dist x px + dist py y") case True then have "dist x px + dist y py + 2 * dist px py ≤ dist x y + dist py px + 10 * deltaG(TYPE('a)) + 4 * C" using * by auto then show ?thesis by (auto simp add: metric_space_class.dist_commute) next case False then have "dist x px + dist y py + 2 * dist px py ≤ dist x px + dist py y + 10 * deltaG(TYPE('a)) + 4 * C" using * by auto then show ?thesis by (simp add: metric_space_class.dist_commute) qed qed text ‹The projection on a quasi-convex set is $1$-Lipschitz up to an additive error.› lemma (in Gromov_hyperbolic_space_geodesic) proj_along_quasiconvex_contraction': assumes "quasiconvex C G" "px ∈ proj_set x G" "py ∈ proj_set y G" shows "dist px py ≤ dist x y + 4 * deltaG(TYPE('a)) + 2 * C" proof (cases "dist y py ≤ dist x px") case True have "dist x px + dist px py ≤ dist x py + 4 * deltaG(TYPE('a)) + 2 * C" by (rule dist_along_quasiconvex[OF assms(1) assms(2) proj_setD(1)[OF assms(3)]]) also have "... ≤ (dist x y + dist y py) + 4 * deltaG(TYPE('a)) + 2 * C" by (intro mono_intros) finally show ?thesis using True by auto next case False have "dist y py + dist py px ≤ dist y px + 4 * deltaG(TYPE('a)) + 2 * C" by (rule dist_along_quasiconvex[OF assms(1) assms(3) proj_setD(1)[OF assms(2)]]) also have "... ≤ (dist y x + dist x px) + 4 * deltaG(TYPE('a)) + 2 * C" by (intro mono_intros) finally show ?thesis using False by (auto simp add: metric_space_class.dist_commute) qed text ‹We can in particular specialize the previous statements to geodesics, which are $0$-quasi-convex.› lemma (in Gromov_hyperbolic_space_geodesic) dist_along_geodesic: assumes "geodesic_segment G" "p ∈ proj_set x G" "y ∈ G" shows "dist x p + dist p y ≤ dist x y + 4 * deltaG(TYPE('a))" using dist_along_quasiconvex[OF quasiconvex_of_geodesic[OF assms(1)] assms(2) assms(3)] by auto lemma (in Gromov_hyperbolic_space_geodesic) proj_along_geodesic_contraction: assumes "geodesic_segment G" "px ∈ proj_set x G" "py ∈ proj_set y G" shows "dist px py ≤ max (5 * deltaG(TYPE('a))) (dist x y - dist px x - dist py y + 10 * deltaG(TYPE('a)))" using proj_along_quasiconvex_contraction[OF quasiconvex_of_geodesic[OF assms(1)] assms(2) assms(3)] by auto lemma (in Gromov_hyperbolic_space_geodesic) proj_along_geodesic_contraction': assumes "geodesic_segment G" "px ∈ proj_set x G" "py ∈ proj_set y G" shows "dist px py ≤ dist x y + 4 * deltaG(TYPE('a))" using proj_along_quasiconvex_contraction'[OF quasiconvex_of_geodesic[OF assms(1)] assms(2) assms(3)] by auto text ‹If one projects a continuous curve on a quasi-convex set, the image does not have to be connected (the projection is discontinuous), but since the projections of nearby points are within uniformly bounded distance one can find in the projection a point with almost prescribed distance to the starting point, say. For further applications, we also pick the first such point, i.e., all the previous points are also close to the starting point.› lemma (in Gromov_hyperbolic_space_geodesic) quasi_convex_projection_small_gaps: assumes "continuous_on {a..(b::real)} f" "a ≤ b" "quasiconvex C G" "⋀t. t ∈ {a..b} ⟹ p t ∈ proj_set (f t) G" "delta > deltaG(TYPE('a))" "d ∈ {4 * delta + 2 * C..dist (p a) (p b)}" shows "∃t ∈ {a..b}. (dist (p a) (p t) ∈ {d - 4 * delta - 2 * C .. d}) ∧ (∀s ∈ {a..t}. dist (p a) (p s) ≤ d)" proof - have "delta > 0" using assms(5) local.delta_nonneg by linarith moreover have "C ≥ 0" using quasiconvexC[OF assms(3)] by simp ultimately have "d ≥ 0" using assms by auto text ‹The idea is to define the desired point as the last point $u$ for which there is a projection at distance at most $d$ of the starting point. Then the projection can not be much closer to the starting point, or one could point another such point further away by almost continuity, giving a contradiction. The technical implementation requires some care, as the "last point" may not satisfy the property, for lack of continuity. If it does, then fine. Otherwise, one should go just a little bit to its left to find the desired point.› define I where "I = {t ∈ {a..b}. ∀s ∈ {a..t}. dist (p a) (p s) ≤ d}" have "a ∈ I" using ‹a ≤ b› ‹d ≥ 0› unfolding I_def by auto have "bdd_above I" unfolding I_def by auto define u where "u = Sup I" have "a ≤ u" unfolding u_def apply (rule cSup_upper) using ‹a ∈ I› ‹bdd_above I› by auto have "u ≤ b" unfolding u_def apply (rule cSup_least) using ‹a ∈ I› apply auto unfolding I_def by auto have A: "dist (p a) (p s) ≤ d" if "s < u" "a ≤ s" for s proof - have "∃t∈I. s < t" unfolding u_def apply (subst less_cSup_iff[symmetric]) using ‹a ∈ I› ‹bdd_above I› using ‹s < u› unfolding u_def by auto then obtain t where t: "t ∈ I" "s < t" by auto then have "s ∈ {a..t}" using ‹a ≤ s› by auto then show ?thesis using t(1) unfolding I_def by auto qed have "continuous (at u within {a..b}) f" using assms(1) by (simp add: ‹a ≤ u› ‹u ≤ b› continuous_on_eq_continuous_within) then have "∃i > 0. ∀s∈{a..b}. dist u s < i ⟶ dist (f u) (f s) < (delta - deltaG(TYPE('a)))" unfolding continuous_within_eps_delta using ‹deltaG(TYPE('a)) < delta› by (auto simp add: metric_space_class.dist_commute) then obtain e0 where e0: "e0 > 0" "⋀s. s ∈ {a..b} ⟹ dist u s < e0 ⟹ dist (f u) (f s) < (delta - deltaG(TYPE('a)))" by auto show ?thesis proof (cases "dist (p a) (p u) > d") text ‹First, consider the case where $u$ does not satisfy the defining property. Then the desired point $t$ is taken slightly to its left.› case True then have "u ≠ a" using ‹d ≥ 0› by auto then have "a < u" using ‹a ≤ u› by auto define e::real where "e = min (e0/2) ((u-a)/2)" then have "e > 0" using ‹a < u› ‹e0 > 0› by auto define t where "t = u - e" then have "t < u" using ‹e > 0› by auto have "u - b ≤ e" "e ≤ u - a" using ‹e > 0› ‹u ≤ b› unfolding e_def by (auto simp add: min_def) then have "t ∈ {a..b}" "t ∈ {a..t}" unfolding t_def by auto have "dist u t < e0" unfolding t_def e_def dist_real_def using ‹e0 > 0› ‹a ≤ u› by auto have *: "∀s ∈ {a..t}. dist (p a) (p s) ≤ d" using A ‹t < u› by auto have "dist (p t) (p u) ≤ dist (f t) (f u) + 4 * deltaG(TYPE('a)) + 2 * C" apply (rule proj_along_quasiconvex_contraction'[OF ‹quasiconvex C G›]) using assms (4) ‹t ∈ {a..b}› ‹a ≤ u› ‹u ≤ b› by auto also have "... ≤ (delta - deltaG(TYPE('a))) + 4 * deltaG(TYPE('a)) + 2 * C" apply (intro mono_intros) using e0(2)[OF ‹t ∈ {a..b}› ‹dist u t < e0›] by (auto simp add: metric_space_class.dist_commute) finally have I: "dist (p t) (p u) ≤ 4 * delta + 2 * C" using ‹delta > deltaG(TYPE('a))› by simp have "d ≤ dist (p a) (p u)" using True by auto also have "... ≤ dist (p a) (p t) + dist (p t) (p u)" by (intro mono_intros) also have "... ≤ dist (p a) (p t) + 4 * delta + 2 * C" using I by simp finally have **: "d - 4 * delta - 2 * C ≤ dist (p a) (p t)" by simp show ?thesis apply (rule bexI[OF _ ‹t ∈ {a..b}›]) using * ** ‹t ∈ {a..b}› by auto next text ‹Next, consider the case where $u$ satisfies the defining property. Then we will take $t = u$. The only nontrivial point to check is that the distance of $f(u)$ to the starting point is not too small. For this, we need to separate the case where $u = b$ (in which case one argues directly) and the case where $u < b$, where one can use a point slightly to the right of $u$ which has a projection at distance $ > d$ of the starting point, and use almost continuity.› case False have B: "dist (p a) (p s) ≤ d" if "s ∈ {a..u}" for s proof (cases "s = u") case True show ?thesis unfolding True using False by auto next case False then show ?thesis using that A by auto qed have C: "dist (p a) (p u) ≥ d - 4 *delta - 2 * C" proof (cases "u = b") case True have "d ≤ dist (p a) (p b)" using assms by auto also have "... ≤ dist (p a) (p u) + dist (p u) (p b)" by (intro mono_intros) also have "... ≤ dist (p a) (p u) + (dist (f u) (f b) + 4 * deltaG TYPE('a) + 2 * C)" apply (intro mono_intros proj_along_quasiconvex_contraction'[OF ‹quasiconvex C G›]) using assms ‹a ≤ u› ‹u ≤ b› by auto finally show ?thesis unfolding True using ‹deltaG(TYPE('a)) < delta› by auto next case False then have "u < b" using ‹u ≤ b› by auto define e::real where "e = min (e0/2) ((b-u)/2)" then have "e > 0" using ‹u < b› ‹e0 > 0› by auto define v where "v = u + e" then have "u < v" using ‹e > 0› by auto have "e ≤ b - u" "a - u ≤ e" using ‹e > 0› ‹a ≤ u› unfolding e_def by (auto simp add: min_def) then have "v ∈ {a..b}" unfolding v_def by auto moreover have "v ∉ I" using ‹u < v› ‹bdd_above I› cSup_upper not_le unfolding u_def by auto ultimately have "∃w ∈ {a..v}. dist (p a) (p w) > d" unfolding I_def by force then obtain w where w: "w ∈ {a..v}" "dist (p a) (p w) > d" by auto then have "w ∉ {a..u}" using B by force then have "u < w" using w(1) by auto have "w ∈ {a..b}" using w(1) ‹v ∈ {a..b}› by auto have "dist u w = w - u" unfolding dist_real_def using ‹u < w› by auto also have "... ≤ v - u" using w(1) by auto also have "... < e0" unfolding v_def e_def min_def using ‹e0 > 0› by auto finally have "dist u w < e0" by simp have "dist (p u) (p w) ≤ dist (f u) (f w) + 4 * deltaG(TYPE('a)) + 2 * C" apply (rule proj_along_quasiconvex_contraction'[OF ‹quasiconvex C G›]) using assms ‹a ≤ u› ‹u ≤ b› ‹w ∈ {a..b}› by auto also have "... ≤ (delta - deltaG(TYPE('a))) + 4 * deltaG(TYPE('a)) + 2 * C" apply (intro mono_intros) using e0(2)[OF ‹w ∈ {a..b}› ‹dist u w < e0›] by (auto simp add: metric_space_class.dist_commute) finally have I: "dist (p u) (p w) ≤ 4 * delta + 2 * C" using ‹delta > deltaG(TYPE('a))› by simp have "d ≤ dist (p a) (p u) + dist (p u) (p w)" using w(2) metric_space_class.dist_triangle[of "p a" "p w" "p u"] by auto also have "... ≤ dist (p a) (p u) + 4 * delta + 2 * C" using I by auto finally show ?thesis by simp qed show ?thesis apply (rule bexI[of _ u]) using B ‹a ≤ u› ‹u ≤ b› C by auto qed qed text ‹Same lemma, except that one exchanges the roles of the beginning and the end point.› lemma (in Gromov_hyperbolic_space_geodesic) quasi_convex_projection_small_gaps': assumes "continuous_on {a..(b::real)} f" "a ≤ b" "quasiconvex C G" "⋀x. x ∈ {a..b} ⟹ p x ∈ proj_set (f x) G" "delta > deltaG(TYPE('a))" "d ∈ {4 * delta + 2 * C..dist (p a) (p b)}" shows "∃t ∈ {a..b}. dist (p b) (p t) ∈ {d - 4 * delta - 2 * C .. d} ∧ (∀s ∈ {t..b}. dist (p b) (p s) ≤ d)" proof - have *: "continuous_on {-b..-a} (λt. f(-t))" using continuous_on_compose[of "{-b..-a}" "λt. -t" f] using assms(1) continuous_on_minus[OF continuous_on_id] by auto define q where "q = (λt. p(-t))" have "∃t ∈ {-b..-a}. (dist (q (-b)) (q t) ∈ {d - 4 * delta - 2 * C .. d}) ∧ (∀s ∈ {-b..t}. dist (q (-b)) (q s) ≤ d)" apply (rule quasi_convex_projection_small_gaps[where ?f = "λt. f(-t)" and ?G = G]) unfolding q_def using assms * by (auto simp add: metric_space_class.dist_commute) then obtain t where t: "t ∈ {-b..-a}" "dist (q (-b)) (q t) ∈ {d - 4 * delta - 2 * C .. d}" "⋀s. s ∈ {-b..t} ⟹ dist (q (-b)) (q s) ≤ d" by blast have *: "dist (p b) (p s) ≤ d" if "s ∈ {-t..b}" for s using t(3)[of "-s"] that q_def by auto show ?thesis apply (rule bexI[of _ "-t"]) using t * q_def by auto qed section ‹The Morse-Gromov Theorem› text ‹The goal of this section is to prove a central basic result in the theory of hyperbolic spaces, usually called the Morse Lemma. It is really a theorem, and we add the name Gromov the avoid the confusion with the other Morse lemma on the existence of good coordinates for $C^2$ functions with non-vanishing hessian. It states that a quasi-geodesic remains within bounded distance of a geodesic with the same endpoints, the error depending only on $\delta$ and on the parameters $(\lambda, C)$ of the quasi-geodesic, but not on its length. There are several proofs of this result. We will follow the one of Shchur~\<^cite>‹"shchur"›, which gets an optimal dependency in terms of the parameters of the quasi-isometry, contrary to all previous proofs. The price to pay is that the proof is more involved (relying in particular on the fact that the closest point projection on quasi-convex sets is exponentially contracting). We will also give afterwards for completeness the proof in~\<^cite>‹"bridson_haefliger"›, as it brings up interesting tools, although the dependency it gives is worse.› text ‹The next lemma (for $C = 0$, Lemma 2 in~\<^cite>‹"shchur"›) asserts that, if two points are not too far apart (at distance at most $10 \delta$), and far enough from a given geodesic segment, then when one moves towards this geodesic segment by a fixed amount (here $5 \delta$), then the two points become closer (the new distance is at most $5 \delta$, gaining a factor of $2$). Later, we will iterate this lemma to show that the projection on a geodesic segment is exponentially contracting. For the application, we give a more general version involving an additional constant $C$. This lemma holds for $\delta$ the hyperbolicity constant. We will want to apply it with $\delta > 0$, so to avoid problems in the case $\delta = 0$ we formulate it not using the hyperbolicity constant of the given type, but any constant which is at least the hyperbolicity constant (this is to work around the fact that one can not say or use easily in Isabelle that a type with hyperbolicity $\delta$ is also hyperbolic for any larger constant $\delta'$.› lemma (in Gromov_hyperbolic_space_geodesic) geodesic_projection_exp_contracting_aux: assumes "geodesic_segment G" "px ∈ proj_set x G" "py ∈ proj_set y G" "delta ≥ deltaG(TYPE('a))" "dist x y ≤ 10 * delta + C" "M ≥ 15/2 * delta" "dist px x ≥ M + 5 * delta + C/2" "dist py y ≥ M + 5 * delta + C/2" "C ≥ 0" shows "dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) ≤ 5 * delta" proof - have "dist px x ≤ dist py x" using proj_setD(2)[OF assms(2)] infdist_le[OF proj_setD(1)[OF assms(3)], of x] by (simp add: metric_space_class.dist_commute) have "dist py y ≤ dist px y" using proj_setD(2)[OF assms(3)] infdist_le[OF proj_setD(1)[OF assms(2)], of y] by (simp add: metric_space_class.dist_commute) have "delta ≥ 0" using assms local.delta_nonneg by linarith then have M: "M ≥ 0" "M ≤ dist px x" "M ≤ dist px y" "M ≤ dist py x" "M ≤ dist py y" using assms ‹dist px x ≤ dist py x› ‹dist py y ≤ dist px y ›by auto have "px ∈ G" "py ∈ G" using assms proj_setD by auto define x' where "x' = geodesic_segment_param {px--x} px M" define y' where "y' = geodesic_segment_param {py--y} py M" text ‹First step: the distance between $px$ and $py$ is at most $5\delta$.› have "dist px py ≤ max (5 * deltaG(TYPE('a))) (dist x y - dist px x - dist py y + 10 * deltaG(TYPE('a)))" by (rule proj_along_geodesic_contraction[OF assms(1) assms(2) assms(3)]) also have "... ≤ max (5 * deltaG(TYPE('a))) (5 * deltaG(TYPE('a)))" apply (intro mono_intros) using assms ‹delta ≥ 0› by auto finally have "dist px py ≤ 5 * delta" using ‹delta ≥ deltaG(TYPE('a))› by auto text ‹Second step: show that all the interesting Gromov products at bounded below by $M$.› have *: "x' ∈ {px--x}" unfolding x'_def by (simp add: geodesic_segment_param_in_segment) have "px ∈ proj_set x' G" by (rule proj_set_geodesic_same_basepoint[OF ‹px ∈ proj_set x G› _ *], auto) have "dist px x' = M" unfolding x'_def using M by auto have "dist px x' ≤ dist py x'" using proj_setD(2)[OF ‹px ∈ proj_set x' G›] infdist_le[OF proj_setD(1)[OF assms(3)], of x'] by (simp add: metric_space_class.dist_commute) have **: "dist px x = dist px x' + dist x' x" using geodesic_segment_dist[OF _ *, of px x] by auto have Ixx: "Gromov_product_at px x' x = M" unfolding Gromov_product_at_def ** x'_def using M by auto have "2 * M = dist px x' + dist px x - dist x' x" unfolding ** x'_def using M by auto also have "... ≤ dist py x' + dist py x - dist x' x" apply (intro mono_intros, auto) by fact+ also have "... = 2 * Gromov_product_at py x x'" unfolding Gromov_product_at_def by (auto simp add: metric_space_class.dist_commute) finally have Iyx: "Gromov_product_at py x x' ≥ M" by auto have *: "y' ∈ {py--y}" unfolding y'_def by (simp add: geodesic_segment_param_in_segment) have "py ∈ proj_set y' G" by (rule proj_set_geodesic_same_basepoint[OF ‹py ∈ proj_set y G› _ *], auto) have "dist py y' = M" unfolding y'_def using M by auto have "dist py y' ≤ dist px y'" using proj_setD(2)[OF ‹py ∈ proj_set y' G›] infdist_le[OF proj_setD(1)[OF assms(2)], of y'] by (simp add: metric_space_class.dist_commute) have **: "dist py y = dist py y' + dist y' y" using geodesic_segment_dist[OF _ *, of py y] by auto have Iyy: "Gromov_product_at py y' y = M" unfolding Gromov_product_at_def ** y'_def using M by auto have "2 * M = dist py y' + dist py y - dist y' y" unfolding ** y'_def using M by auto also have "... ≤ dist px y' + dist px y - dist y' y" apply (intro mono_intros, auto) by fact+ also have "... = 2 * Gromov_product_at px y y'" unfolding Gromov_product_at_def by (auto simp add: metric_space_class.dist_commute) finally have Ixy: "Gromov_product_at px y y' ≥ M" by auto have "2 * M ≤ dist px x + dist py y - dist x y" using assms by auto also have "... ≤ dist px x + dist px y - dist x y" by (intro mono_intros, fact) also have "... = 2 * Gromov_product_at px x y" unfolding Gromov_product_at_def by auto finally have Ix: "Gromov_product_at px x y ≥ M" by auto have "2 * M ≤ dist px x + dist py y - dist x y" using assms by auto also have "... ≤ dist py x + dist py y - dist x y" by (intro mono_intros, fact) also have "... = 2 * Gromov_product_at py x y" unfolding Gromov_product_at_def by auto finally have Iy: "Gromov_product_at py x y ≥ M" by auto text ‹Third step: prove the estimate› have "M - 2 * delta ≤ Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG(TYPE('a))" using Ixx Ixy Ix ‹delta ≥ deltaG(TYPE('a))› by auto also have "... ≤ Gromov_product_at px x' y'" by (intro mono_intros) finally have A: "M - 4 * delta + dist x' y' ≤ dist px y'" unfolding Gromov_product_at_def ‹dist px x' = M› by auto have "M - 2 * delta ≤ Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG(TYPE('a))" using Iyx Iyy Iy ‹delta ≥ deltaG(TYPE('a))› by (auto simp add: Gromov_product_commute) also have "... ≤ Gromov_product_at py x' y'" by (intro mono_intros) finally have B: "M - 4 * delta + dist x' y' ≤ dist py x'" unfolding Gromov_product_at_def ‹dist py y' = M› by auto have "dist px py ≤ 2 * M - 10 * delta" using assms ‹dist px py ≤ 5 * delta› by auto have "2 * M - 8 * delta + 2 * dist x' y' ≤ dist px y' + dist py x'" using A B by auto also have "... ≤ max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a)" by (rule hyperb_quad_ineq) also have "... ≤ max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta" using ‹deltaG(TYPE('a)) ≤ delta› by auto finally have "2 * M - 10 * delta + 2 * dist x' y' ≤ max (dist px py + dist y' x') (dist px x' + dist y' py)" by auto then have "2 * M - 10 * delta + 2 * dist x' y' ≤ dist px x' + dist py y'" apply (auto simp add: metric_space_class.dist_commute) using ‹0 ≤ delta› ‹dist px py ≤ 2 * M - 10 * delta› ‹dist px x' = M› ‹dist py y' = M› by auto then have "dist x' y' ≤ 5 * delta" unfolding ‹dist px x' = M› ‹dist py y' = M› by auto then show ?thesis unfolding x'_def y'_def by auto qed text ‹The next lemma (Lemma 10 in~\<^cite>‹"shchur"› for $C = 0$) asserts that the projection on a geodesic segment is an exponential contraction. More precisely, if a path of length $L$ is at distance at least $D$ of a geodesic segment $G$, then the projection of the path on $G$ has diameter at most $C L \exp(-c D/\delta)$, where $C$ and $c$ are universal constants. This is not completely true at one can not go below a fixed size, as always, so the correct bound is $K \max(\delta, L \exp(-c D/\delta))$. For the application, we give a slightly more general statement involving an additional constant $C$. This statement follows from the previous lemma: if one moves towards $G$ by $10 \delta$, then the distance between points is divided by $2$. Then one iterates this statement as many times as possible, gaining a factor $2$ each time and therefore an exponential factor in the end.› lemma (in Gromov_hyperbolic_space_geodesic) geodesic_projection_exp_contracting: assumes "geodesic_segment G" "⋀x y. x ∈ {a..b} ⟹ y ∈ {a..b} ⟹ dist (f x) (f y) ≤ lambda * dist x y + C" "a ≤ b" "pa ∈ proj_set (f a) G" "pb ∈ proj_set (f b) G" "⋀t. t ∈ {a..b} ⟹ infdist (f t) G ≥ D" "D ≥ 15/2 * delta + C/2" "delta > deltaG(TYPE('a))" "C ≥ 0" "lambda ≥ 0" shows "dist pa pb ≤ max (5 * deltaG(TYPE('a))) ((4 * exp(1/2 * ln 2)) * lambda * (b-a) * exp(-(D-C/2) * ln 2 / (5 * delta)))" proof - have "delta > 0" using assms using local.delta_nonneg by linarith have "exp(15/2/5 * ln 2) = exp(ln 2) * exp(1/2 * ln (2::real))" unfolding mult_exp_exp by simp also have "... = 2 * exp(1/2 * ln 2)" by auto finally have "exp(15/2/5 * ln 2) = 2 * exp(1/2 * ln (2::real))" by simp text ‹The idea of the proof is to start with a sequence of points separated by $10 \delta + C$ along the original path, and push them by a fixed distance towards $G$ to bring them at distance at most $5 \delta$, thanks to the previous lemma. Then, discard half the points, and start again. This is possible while one is far enough from $G$. In the first step of the proof, we formalize this in the case where the process can be iterated long enough that, at the end, the projections on $G$ are very close together. This is a simple induction, based on the previous lemma.› have Main: "⋀c g p. (∀i ∈ {0..2^k}. p i ∈ proj_set (g i) G) ⟹ (∀i ∈ {0..2^k}. dist (p i) (g i) ≥ 5 * delta * k + 15/2 * delta + c/2) ⟹ (∀i ∈ {0..<2^k}. dist (g i) (g (Suc i)) ≤ 10 * delta + c) ⟹ c ≥ 0 ⟹ dist (p 0) (p (2^k)) ≤ 5 * deltaG(TYPE('a))" for k proof (induction k) case 0 then have H: "p 0 ∈ proj_set (g 0) G" "p 1 ∈ proj_set (g 1) G" "dist (g 0) (g 1) ≤ 10 * delta + c" "dist (p 0) (g 0) ≥ 15/2 * delta + c/2" "dist (p 1) (g 1) ≥ 15/2 * delta + c/2" by auto have "dist (p 0) (p 1) ≤ max (5 * deltaG(TYPE('a))) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG(TYPE('a)))" by (rule proj_along_geodesic_contraction[OF ‹geodesic_segment G› ‹p 0 ∈ proj_set (g 0) G› ‹p 1 ∈ proj_set (g 1) G›]) also have "... ≤ max (5 * deltaG(TYPE('a))) (5 * deltaG(TYPE('a)))" apply (intro mono_intros) using H ‹delta > deltaG(TYPE('a))› by auto finally show "dist (p 0) (p (2^0)) ≤ 5 * deltaG(TYPE('a))" by auto next case (Suc k) have *: "5 * delta * real (k + 1) + 5 * delta = 5 * delta * real (Suc k + 1)" by (simp add: algebra_simps) define h where "h = (λi. geodesic_segment_param {p i--g i} (p i) (5 * delta * k + 15/2 * delta))" have h_dist: "dist (h i) (h (Suc i)) ≤ 5 * delta" if "i ∈ {0..<2^(Suc k)}" for i unfolding h_def apply (rule geodesic_projection_exp_contracting_aux[OF ‹geodesic_segment G› _ _ less_imp_le[OF ‹delta > deltaG(TYPE('a))›]]) unfolding * using Suc.prems that ‹delta > 0› by (auto simp add: algebra_simps divide_simps) define g' where "g' = (λi. h (2 * i))" define p' where "p' = (λi. p (2 * i))" have "dist (p' 0) (p' (2^k)) ≤ 5 * deltaG(TYPE('a))" proof (rule Suc.IH[where ?g = g' and ?c = 0]) show "∀i∈{0..2 ^ k}. p' i ∈ proj_set (g' i) G" proof fix i::nat assume "i ∈ {0..2^k}" then have *: "2 * i ∈ {0..2^(Suc k)}" by auto show "p' i ∈ proj_set (g' i) G" unfolding p'_def g'_def h_def apply (rule proj_set_geodesic_same_basepoint[of _ "g (2 * i)" _ "{p(2 * i)--g(2 * i)}"]) using Suc * by (auto simp add: geodesic_segment_param_in_segment) qed show "∀i∈{0..2 ^ k}. 5 * delta * k + 15/2 * delta + 0/2 ≤ dist (p' i) (g' i)" proof fix i::nat assume "i ∈ {0..2^k}" then have *: "2 * i ∈ {0..2^(Suc k)}" by auto have "5 * delta * k + 15/2 * delta ≤ 5 * delta * Suc k + 15/2 * delta + c/2" using ‹delta > 0› ‹c ≥ 0› by (auto simp add: algebra_simps divide_simps) also have "... ≤ dist (p (2 * i)) (g (2 * i))" using Suc * by auto finally have *: "5 * delta * k + 15/2 * delta ≤ dist (p (2 * i)) (g (2 * i))" by simp have "dist (p' i) (g' i) = 5 * delta * k + 15/2 * delta" unfolding p'_def g'_def h_def apply (rule geodesic_segment_param_in_geodesic_spaces(6)) using * ‹delta > 0› by auto then show "5 * delta * k + 15/2 * delta + 0/2 ≤ dist (p' i) (g' i)" by simp qed show "∀i∈{0..<2 ^ k}. dist (g' i) (g' (Suc i)) ≤ 10 * delta + 0" proof fix i::nat assume *: "i ∈ {0..<2 ^ k}" have "dist (g' i) (g' (Suc i)) = dist (h (2 * i)) (h (Suc (Suc (2 * i))))" unfolding g'_def by auto also have "... ≤ dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i))))" by (intro mono_intros) also have "... ≤ 5 * delta + 5 * delta" apply (intro mono_intros h_dist) using * by auto finally show "dist (g' i) (g' (Suc i)) ≤ 10 * delta + 0" by simp qed qed (simp) then show "dist (p 0) (p (2 ^ Suc k)) ≤ 5 * deltaG(TYPE('a))" unfolding p'_def by auto qed text ‹Now, we will apply the previous basic statement to points along our original path. We introduce $k$, the number of steps for which the pushing process can be done -- it only depends on the original distance $D$ to $G$. › define k where "k = nat(floor((D - C/2 - 15/2 * delta)/(5 * delta)))" have "int k = floor((D - C/2 - 15/2 * delta)/(5 * delta))" unfolding k_def apply (rule nat_0_le) using ‹D ≥ 15/2 * delta + C/2› ‹delta > 0› by auto then have "k ≤ (D - C/2 - 15/2 * delta)/(5 * delta)" "(D - C/2 - 15/2 * delta)/(5 * delta) ≤ k + 1" by linarith+ then have k: "D ≥ 5 * delta * k + 15/2 * delta + C/2" "D ≤ 5 * delta * (k+1) + 15/2 * delta + C/2" using ‹delta > 0› by (auto simp add: algebra_simps divide_simps) have "exp((D-C/2)/(5 * delta) * ln 2) * exp(-15/2/5 * ln 2) = exp(((D-C/2-15/2 * delta)/(5 * delta)) * ln 2)" unfolding mult_exp_exp using ‹delta > 0› by (simp add: algebra_simps divide_simps) also have "... ≤ exp((k+1) * ln 2)" apply (intro mono_intros) using k(2) ‹delta > 0› by (auto simp add: divide_simps algebra_simps) also have "... = 2^(k+1)" by (subst powr_realpow[symmetric], auto simp add: powr_def) also have "... = 2 * 2^k" by auto finally have k': "1/2^k ≤ 2 * exp(15/2/5 * ln 2) * exp(- ((D-C/2) * ln 2 / (5 * delta)))" by (auto simp add: algebra_simps divide_simps exp_minus) text ‹We separate the proof into two cases. If the path is not too long, then it can be covered by $2^k$ points at distance at most $10 \delta + C$. By the basic statement, it follows that the diameter of the projection is at most $5 \delta$. Otherwise, we subdivide the path into $2^N$ points at distance at most $10 \delta + C$, with $N \geq k$, and apply the basic statement to blocks of $2^k$ consecutive points. It follows that the projections of $g_0, g_{2^k}, g_{2\cdot 2^k},\dotsc$ are at distances at most $5 \delta$. Hence, the first and last projections are at distance at most $2^{N-k} \cdot 5 \delta$, which is the desired bound.› show ?thesis proof (cases "lambda * (b-a) ≤ 10 * delta * 2^k") text ‹First, treat the case where the path is rather short.› case True define g::"nat ⇒ 'a" where "g = (λi. f(a + (b-a) * i/2^k))" have "g 0 = f a" "g(2^k) = f b" unfolding g_def by auto have *: "a + (b-a) * i/2^k ∈ {a..b}" if "i ∈ {0..2^k}" for i::nat proof - have "a + (b - a) * (real i / 2 ^ k) ≤ a + (b-a) * (2^k/2^k)" apply (intro mono_intros) using that ‹a ≤ b› by auto then show ?thesis using ‹a ≤ b› by auto qed have A: "dist (g i) (g (Suc i)) ≤ 10 * delta + C" if "i ∈ {0..<2^k}" for i proof - have "dist (g i) (g (Suc i)) ≤ lambda * dist (a + (b-a) * i/2^k) (a + (b-a) * (Suc i)/2^k) + C" unfolding g_def apply (intro assms(2) *) using that by auto also have "... = lambda * (b-a)/2^k + C" unfolding dist_real_def using ‹a ≤ b› by (auto simp add: algebra_simps divide_simps) also have "... ≤ 10 * delta + C" using True by (simp add: divide_simps algebra_simps) finally show ?thesis by simp qed define p where "p = (λi. if i = 0 then pa else if i = 2^k then pb else SOME p. p ∈ proj_set (g i) G)" have B: "p i ∈ proj_set (g i) G" if "i ∈ {0..2^k}" for i proof (cases "i = 0 ∨ i = 2^k") case True then show ?thesis using ‹pa ∈ proj_set (f a) G› ‹pb ∈ proj_set (f b) G› unfolding p_def g_def by auto next case False then have "p i = (SOME p. p ∈ proj_set (g i) G)" unfolding p_def by auto moreover have "proj_set (g i) G ≠ {}" apply (rule proj_set_nonempty_of_proper) using geodesic_segment_topology[OF ‹geodesic_segment G›] by auto ultimately show ?thesis using some_in_eq by auto qed have C: "dist (p i) (g i) ≥ 5 * delta * k + 15/2 * delta + C/2" if "i ∈ {0..2^k}" for i proof - have "5 * delta * k + 15/2 * delta + C/2 ≤ D" using k(1) by simp also have "... ≤ infdist (g i) G" unfolding g_def apply (rule ‹⋀t. t ∈ {a..b} ⟹ infdist (f t) G ≥ D›) using * that by auto also have "... = dist (p i) (g i)" using that proj_setD(2)[OF B[OF that]] by (simp add: metric_space_class.dist_commute) finally show ?thesis by simp qed have "dist (p 0) (p (2^k)) ≤ 5 * deltaG(TYPE('a))" apply (rule Main[where ?g = g and ?c = C]) using A B C ‹C ≥ 0› by auto then show ?thesis unfolding p_def by auto next text ‹Now, the case where the path is long. We introduce $N$ such that it is roughly of length $2^N \cdot 10 \delta$.› case False have *: "10 * delta * 2^k ≤ lambda * (b-a)" using False by simp have "lambda * (b-a) > 0" using ‹delta > 0› False ‹0 ≤ lambda› assms(3) less_eq_real_def mult_le_0_iff by auto then have "a < b" "lambda > 0" using ‹a ≤ b› ‹lambda ≥ 0› less_eq_real_def by auto define n where "n = nat(floor(log 2 (lambda * (b-a)/(10 * delta))))" have "log 2 (lambda * (b-a)/(10 * delta)) ≥ log 2 (2^k)" apply (subst log_le_cancel_iff) using * ‹delta > 0› ‹a < b› ‹lambda > 0› by (auto simp add: divide_simps algebra_simps) moreover have "log 2 (2^k) = k" by simp ultimately have A: "log 2 (lambda * (b-a)/(10 * delta)) ≥ k" by auto have **: "int n = floor(log 2 (lambda * (b-a)/(10 * delta)))" unfolding n_def apply (rule nat_0_le) using A by auto then have "log 2 (2^n) ≤ log 2 (lambda * (b-a)/(10 * delta))" apply (subst log_nat_power, auto) by linarith then have I: "2^n ≤ lambda * (b-a)/(10 * delta)" using ‹0 < lambda * (b - a)› ‹0 < delta› by (simp add: le_log_iff powr_realpow) have "log 2 (lambda * (b-a)/(10 * delta)) ≤ log 2 (2^(n+1))" apply (subst log_nat_power, auto) using ** by linarith then have J: "lambda * (b-a)/(10 * delta) ≤ 2^(n+1)" using ‹0 < lambda * (b - a)› ‹0 < delta› by auto have K: "k ≤ n" using A ** by linarith define N where "N = n+1" have N: "k+1 ≤ N" "lambda * (b-a) / 2^N ≤ 10 *delta" "2 ^ N ≤ lambda * (b - a) / (5 * delta)" using I J K ‹delta > 0› unfolding N_def by (auto simp add: divide_simps algebra_simps) then have "2 ^ k ≠ (0::real)" "k ≤ N" by auto then have "(2^(N-k)::real) = 2^N/2^k" by (metis (no_types) add_diff_cancel_left' le_Suc_ex nonzero_mult_div_cancel_left power_add) text ‹Define $2^N$ points along the path, separated by at most $10\delta$, and their projections.› define g::"nat ⇒ 'a" where "g = (λi. f(a + (b-a) * i/2^N))" have "g 0 = f a" "g(2^N) = f b" unfolding g_def by auto have *: "a + (b-a) * i/2^N ∈ {a..b}" if "i ∈ {0..2^N}" for i::nat proof - have "a + (b - a) * (real i / 2 ^ N) ≤ a + (b-a) * (2^N/2^N)" apply (intro mono_intros) using that ‹a ≤ b› by auto then show ?thesis using ‹a ≤ b› by auto qed have A: "dist (g i) (g (Suc i)) ≤ 10 * delta + C" if "i ∈ {0..<2^N}" for i proof - have "dist (g i) (g (Suc i)) ≤ lambda * dist (a + (b-a) * i/2^N) (a + (b-a) * (Suc i)/2^N) + C" unfolding g_def apply (intro assms(2) *) using that by auto also have "... = lambda * (b-a)/2^N + C" unfolding dist_real_def using ‹a ≤ b› by (auto simp add: algebra_simps divide_simps) also have "... ≤ 10 * delta + C" using N by simp finally show ?thesis by simp qed define p where "p = (λi. if i = 0 then pa else if i = 2^N then pb else SOME p. p ∈ proj_set (g i) G)" have B: "p i ∈ proj_set (g i) G" if "i ∈ {0..2^N}" for i proof (cases "i = 0 ∨ i = 2^N") case True then show ?thesis using ‹pa ∈ proj_set (f a) G› ‹pb ∈ proj_set (f b) G› unfolding p_def g_def by auto next case False then have "p i = (SOME p. p ∈ proj_set (g i) G)" unfolding p_def by auto moreover have "proj_set (g i) G ≠ {}" apply (rule proj_set_nonempty_of_proper) using geodesic_segment_topology[OF ‹geodesic_segment G›] by auto ultimately show ?thesis using some_in_eq by auto qed have C: "dist (p i) (g i) ≥ 5 * delta * k + 15/2 * delta + C/2" if "i ∈ {0..2^N}" for i proof - have "5 * delta * k + 15/2 * delta + C/2 ≤ D" using k(1) by simp also have "... ≤ infdist (g i) G" unfolding g_def apply (rule ‹⋀t. t ∈ {a..b} ⟹ infdist (f t) G ≥ D›) using * that by auto also have "... = dist (p i) (g i)" using that proj_setD(2)[OF B[OF that]] by (simp add: metric_space_class.dist_commute) finally show ?thesis by simp qed text ‹Use the basic statement to show that, along packets of size $2^k$, the projections are within $5\delta$ of each other.› have I: "dist (p (2^k * j)) (p (2^k * (Suc j))) ≤ 5 * delta" if "j ∈ {0..<2^(N-k)}" for j proof - have I: "i + 2^k * j ∈ {0..2^N}" if "i ∈ {0..2^k}" for i proof - have "i + 2 ^ k * j ≤ 2^k + 2^k * (2^(N-k)-1)" apply (intro mono_intros) using that ‹j ∈ {0..<2^(N-k)}› by auto also have "... = 2^N" using ‹k +1 ≤ N› by (auto simp add: algebra_simps semiring_normalization_rules(26)) finally show ?thesis by auto qed have I': "i + 2^k * j ∈ {0..<2^N}" if "i ∈ {0..<2^k}" for i proof - have "i + 2 ^ k * j < 2^k + 2^k * (2^(N-k)-1)" apply (intro mono_intros) using that ‹j ∈ {0..<2^(N-k)}› by auto also have "... = 2^N" using ‹k +1 ≤ N› by (auto simp add: algebra_simps semiring_normalization_rules(26)) finally show ?thesis by auto qed define g' where "g' = (λi. g (i + 2^k * j))" define p' where "p' = (λi. p (i + 2^k * j))" have "dist (p' 0) (p' (2^k)) ≤ 5 * deltaG(TYPE('a))" apply (rule Main[where ?g = g' and ?c = C]) unfolding p'_def g'_def using A B C I I' ‹C ≥ 0› by auto also have "... ≤ 5 * delta" using ‹deltaG(TYPE('a)) < delta› by auto finally show ?thesis unfolding p'_def by auto qed text ‹Control the total distance by adding the contributions of blocks of size $2^k$.› have *: "dist (p 0) (p(2^k * j)) ≤ (∑i<j. dist (p (2^k * i)) (p (2^k * (Suc i))))" for j proof (induction j) case (Suc j) have "dist (p 0) (p(2^k * (Suc j))) ≤ dist (p 0) (p(2^k * j)) + dist (p(2^k * j)) (p(2^k * (Suc j)))" by (intro mono_intros) also have "... ≤ (∑i<j. dist (p (2^k * i)) (p (2^k * (Suc i)))) + dist (p(2^k * j)) (p(2^k * (Suc j)))" using Suc.IH by auto also have "... = (∑i<Suc j. dist (p (2^k * i)) (p (2^k * (Suc i))))" by auto finally show ?case by simp qed (auto) have "dist pa pb = dist (p 0) (p (2^N))" unfolding p_def by auto also have "... = dist (p 0) (p (2^k * 2^(N-k)))" using ‹k +1 ≤ N› by (auto simp add: semiring_normalization_rules(26)) also have "... ≤ (∑i<2^(N-k). dist (p (2^k * i)) (p (2^k * (Suc i))))" using * by auto also have "... ≤ (∑(i::nat)<2^(N-k). 5 * delta)" apply (rule sum_mono) using I by auto also have "... = 5 * delta * 2^(N-k)" by auto also have "... = 5 * delta * 2^N * (1/ 2^k)" unfolding ‹(2^(N-k)::real) = 2^N/2^k› by simp also have "... ≤ 5 * delta * (2 * lambda * (b-a)/(10 * delta)) * (2 * exp(15/2/5 * ln 2) * exp(- ((D-C/2) * ln 2 / (5 * delta))))" apply (intro mono_intros) using ‹delta > 0› ‹lambda > 0› ‹a < b› k' N by auto also have "... = (2 * exp(15/2/5 * ln 2)) * lambda * (b-a) * exp(-(D-C/2) * ln 2 / (5 * delta))" using ‹delta > 0› by (auto simp add: algebra_simps divide_simps) finally show ?thesis unfolding ‹exp(15/2/5 * ln 2) = 2 * exp(1/2 * ln (2::real))› by auto qed qed text ‹We deduce from the previous result that a projection on a quasiconvex set is also exponentially contracting. To do this, one uses the contraction of a projection on a geodesic, and one adds up the additional errors due to the quasi-convexity. In particular, the projections on the original quasiconvex set or the geodesic do not have to coincide, but they are within distance at most $C + 8 \delta$.› lemma (in Gromov_hyperbolic_space_geodesic) quasiconvex_projection_exp_contracting: assumes "quasiconvex K G" "⋀x y. x ∈ {a..b} ⟹ y ∈ {a..b} ⟹ dist (f x) (f y) ≤ lambda * dist x y + C" "a ≤ b" "pa ∈ proj_set (f a) G" "pb ∈ proj_set (f b) G" "⋀t. t ∈ {a..b} ⟹ infdist (f t) G ≥ D" "D ≥ 15/2 * delta + K + C/2" "delta > deltaG(TYPE('a))" "C ≥ 0" "lambda ≥ 0" shows "dist pa pb ≤ 2 * K + 8 * delta + max (5 * deltaG(TYPE('a))) ((4 * exp(1/2 * ln 2)) * lambda * (b-a) * exp(-(D - K - C/2) * ln 2 / (5 * delta)))" proof - obtain H where H: "geodesic_segment_between H pa pb" "⋀q. q ∈ H ⟹ infdist q G ≤ K" using quasiconvexD[OF assms(1) proj_setD(1)[OF ‹pa ∈ proj_set (f a) G›] proj_setD(1)[OF ‹pb ∈ proj_set (f b) G›]] by auto obtain qa where qa: "qa ∈ proj_set (f a) H" using proj_set_nonempty_of_proper[of H "f a"] geodesic_segment_topology[OF geodesic_segmentI[OF H(1)]] by auto obtain qb where qb: "qb ∈ proj_set (f b) H" using proj_set_nonempty_of_proper[of H "f b"] geodesic_segment_topology[OF geodesic_segmentI[OF H(1)]] by auto have I: "infdist (f t) H ≥ D - K" if "t ∈ {a..b}" for t proof - have *: "D - K ≤ dist (f t) h" if "h ∈ H" for h proof - have "D - K - dist (f t) h ≤ e" if "e > 0" for e proof - have *: "infdist h G < K + e" using H(2)[OF ‹h ∈ H›] ‹e > 0› by auto obtain g where g: "g ∈ G" "dist h g < K + e" using infdist_almost_attained[OF *] proj_setD(1)[OF ‹pa ∈ proj_set (f a) G›] by auto have "D ≤ dist (f t) g" using ‹⋀t. t ∈ {a..b} ⟹ infdist (f t) G ≥ D›[OF ‹t ∈ {a..b}›] infdist_le[OF ‹g ∈ G›, of "f t"] by auto also have "... ≤ dist (f t) h + dist h g" by (intro mono_intros) also have "... ≤ dist (f t) h + K + e" using g(2) by auto finally show ?thesis by auto qed then have *: "D - K - dist (f t) h ≤ 0" using dense_ge by blast then show ?thesis by simp qed have "D - K ≤ Inf (dist (f t) ` H)" apply (rule cInf_greatest) using * H(1) by auto then show "D - K ≤ infdist (f t) H" apply (subst infdist_notempty) using H(1) by auto qed have Q: "dist qa qb ≤ max (5 * deltaG(TYPE('a))) ((4 * exp(1/2 * ln 2)) * lambda * (b-a) * exp(-((D - K)-C/2 ) * ln 2 / (5 * delta)))" apply (rule geodesic_projection_exp_contracting[OF geodesic_segmentI[OF ‹geodesic_segment_between H pa pb›] assms(2) assms(3)]) using qa qb I assms by auto have A: "dist pa qa ≤ 4 * delta + K" proof - have "dist (f a) pa - dist (f a) qa - K ≤ e" if "e > 0" for e::real proof - have *: "infdist qa G