Theory Morse_Gromov_Theorem

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

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))"
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"
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
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
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)"
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'"
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)"
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›
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"

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 `