Theory Morse_Gromov_Theorem

(*  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  (xX. yX. G. geodesic_segment_between G x y  (zG. infdist z X  C)))"

lemma quasiconvexD:
  assumes "quasiconvex C X" "x  X" "y  X"
  shows "G. geodesic_segment_between G x y  (zG. 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  (zG. 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  (zH. 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))) (xX. 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  (xX. cball x r)" "z  (xX. cball x r)"
  have A: "infdist w (xX. 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" "(pG. 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 (xX. 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  (xX. cball x r)"
        using py(1) by auto
      then have "infdist u (xX. 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  (xX. cball x r)"
        using pz(1) by auto
      then have "infdist u (xX. cball x r) = 0"
        by auto
      then show ?thesis
        using quasiconvexC[OF assms(1)] by auto
    next
      case 2
      have "infdist u (xX. 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 (xX. cball x r)  infdist u (xX. 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  (wG. infdist w (xX. 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 "mH. 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 "rG. 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 "tI. 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 yby 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