Theory Gromov_Boundary

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

theory Gromov_Boundary
  imports Gromov_Hyperbolicity Eexp_Eln
begin

section ‹Constructing a distance from a quasi-distance›

text ‹Below, we will construct a distance on the Gromov completion of a hyperbolic space. The
geometrical object that arises naturally is almost a distance, but it does not satisfy the triangular
inequality. There is a general process to turn such a quasi-distance into a genuine distance, as
follows: define the new distance $\tilde d(x,y)$ to be the infimum of $d(x, u_1) + d(u_1,u_2) +
\dotsb + d(u_{n-1},x)$ over all sequences of points (of any length) connecting $x$ to $y$.
It is clear that it satisfies the triangular inequality, is symmetric, and $\tilde d(x,y) \leq
d(x,y)$. What is not clear, however, is if $\tilde d(x,y)$ can be zero if $x \neq y$, or more
generally how one can bound $\tilde d$ from below. The main point of this contruction is that,
if $d$ satisfies the inequality $d(x,z) \leq \sqrt{2} \max(d(x,y), d(y,z))$, then one
has $\tilde d(x,y) \geq d(x,y)/2$ (and in particular $\tilde d$ defines the same topology, the
same set of Lipschitz functions, and so on, as $d$).

This statement can be found in [Bourbaki, topologie generale, chapitre 10] or in
[Ghys-de la Harpe] for instance. We follow their proof.
›

definition turn_into_distance::"('a  'a  real)  ('a  'a  real)"
  where "turn_into_distance f x y = Inf {( i  {0..<n}. f (u i) (u (Suc i)))| u (n::nat). u 0 = x  u n = y}"

locale Turn_into_distance =
  fixes f::"'a  'a  real"
  assumes nonneg: "f x y  0"
      and sym: "f x y = f y x"
      and self_zero: "f x x = 0"
      and weak_triangle: "f x z  sqrt 2 * max (f x y) (f y z)"
begin

text ‹The two lemmas below are useful when dealing with Inf results, as they always require
the set under consideration to be non-empty and bounded from below.›

lemma bdd_below [simp]:
  "bdd_below {( i = 0..<n. f (u i) (u (Suc i)))| u (n::nat). u 0 = x  u n = y}"
  apply (rule bdd_belowI[of _ 0]) using nonneg by (auto simp add: sum_nonneg)

lemma nonempty:
  "{i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x  u n = y}  {}"
proof -
  define u::"nat  'a" where "u = (λn. if n = 0 then x else y)"
  define n::nat where "n = 1"
  have "u 0 = x  u n = y" unfolding u_def n_def by auto
  then have "(i = 0..<n. f (u i) (u (Suc i)))  {i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x  u n = y}"
    by auto
  then show ?thesis by auto
qed

text ‹We can now prove that \verb+turn_into_distance f+ satisfies all the properties of a distance.
First, it is nonnegative.›

lemma TID_nonneg:
  "turn_into_distance f x y  0"
unfolding turn_into_distance_def apply (rule cInf_greatest[OF nonempty])
using nonneg by (auto simp add: sum_nonneg)

text ‹For the symmetry, we use the symmetry of $f$, and go backwards along a chain of points,
replacing a sequence from $x$ to $y$ with a sequence from $y$ to $x$.›

lemma TID_sym:
  "turn_into_distance f x y = turn_into_distance f y x"
proof -
  have "turn_into_distance f x y  Inf {( i  {0..<n}. f (u i) (u (Suc i)))| u (n::nat). u 0 = y  u n = x}" for x y
  proof (rule cInf_greatest[OF nonempty], auto)
    fix u::"nat  'a" and n assume U: "y = u 0" "x = u n"
    define v::"nat 'a" where "v = (λi. u (n-i))"
    have V: "v 0 = x" "v n = y" unfolding v_def using U by auto

    have "(i = 0..<n. f (u i) (u (Suc i))) = (i = 0..<n. (λi. f (u i) (u (Suc i))) (n-1-i))"
      apply (rule sum.reindex_bij_betw[symmetric])
      by (rule bij_betw_byWitness[of _ "λi. n-1-i"], auto)
    also have "... = ( i = 0..<n. f (v (Suc i)) (v i))"
      apply (rule sum.cong) unfolding v_def by (auto simp add: Suc_diff_Suc)
    also have "... = ( i = 0..<n. f (v i) (v (Suc i)))"
      using sym by auto
    finally have "(i = 0..<n. f (u i) (u (Suc i))) = ( i = 0..<n. f (v i) (v (Suc i)))"
      by simp

    moreover have "turn_into_distance f x y  ( i = 0..<n. f (v i) (v (Suc i)))"
      unfolding turn_into_distance_def apply (rule cInf_lower)
      using V by auto
    finally show "turn_into_distance f (u n) (u 0)  (i = 0..<n. f (u i) (u (Suc i)))"
      using U by auto
  qed
  then have *: "turn_into_distance f x y  turn_into_distance f y x" for x y
    unfolding turn_into_distance_def by auto
  show ?thesis using *[of x y] *[of y x] by simp
qed

text ‹There is a trivial upper bound by $f$, using the single chain $x, y$.›

lemma upper:
  "turn_into_distance f x y  f x y"
unfolding turn_into_distance_def proof (rule cInf_lower, auto)
  define u::"nat  'a" where "u = (λn. if n = 0 then x else y)"
  define n::nat where "n = 1"
  have "u 0 = x  u n = y  f x y = (i = 0..<n. f (u i) (u (Suc i)))" unfolding u_def n_def by auto
  then show "u n. f x y = (i = 0..<n. f (u i) (u (Suc i)))  u 0 = x  u n = y"
    by auto
qed

text ‹The new distance vanishes on a pair of equal points, as this is already the case for $f$.›

lemma TID_self_zero:
  "turn_into_distance f x x = 0"
using upper[of x x] TID_nonneg[of x x] self_zero[of x] by auto

text ‹For the triangular inequality, we concatenate a sequence from $x$ to $y$ almost realizing the
infimum, and a sequence from $y$ to $z$ almost realizing the infimum, to obtain a sequence from
$x$ to $z$ along which the sums of $f$ is almost bounded by
\verb|turn_into_distance f x y + turn_into_distance f y z|.
›

lemma triangle:
  "turn_into_distance f x z  turn_into_distance f x y + turn_into_distance f y z"
proof -
  have "turn_into_distance f x z  turn_into_distance f x y + turn_into_distance f y z + e" if "e > 0" for e
  proof -
    have "Inf {( i  {0..<n}. f (u i) (u (Suc i)))| u (n::nat). u 0 = x  u n = y} < turn_into_distance f x y + e/2"
      unfolding turn_into_distance_def using e > 0 by auto
    then have "a  {( i  {0..<n}. f (u i) (u (Suc i)))| u (n::nat). u 0 = x  u n = y}. a < turn_into_distance f x y + e/2"
      by (rule cInf_lessD[OF nonempty])
    then obtain u n where U: "u 0 = x" "u n = y" "( i  {0..<n}. f (u i) (u (Suc i))) < turn_into_distance f x y + e/2"
      by auto

    have "Inf {( i  {0..<m}. f (v i) (v (Suc i)))| v (m::nat). v 0 = y  v m = z} < turn_into_distance f y z + e/2"
      unfolding turn_into_distance_def using e > 0 by auto
    then have "a  {( i  {0..<m}. f (v i) (v (Suc i)))| v (m::nat). v 0 = y  v m = z}. a < turn_into_distance f y z + e/2"
      by (rule cInf_lessD[OF nonempty])
    then obtain v m where V: "v 0 = y" "v m = z" "( i  {0..<m}. f (v i) (v (Suc i))) < turn_into_distance f y z + e/2"
      by auto

    define w where "w = (λi. if i < n then u i else v (i-n))"
    have *: "w 0 = x" "w (n+m) = z"
      unfolding w_def using U V by auto
    have "turn_into_distance f x z  (i = 0..<n+m. f (w i) (w (Suc i)))"
      unfolding turn_into_distance_def apply (rule cInf_lower) using * by auto
    also have "... = (i = 0..<n. f (w i) (w (Suc i))) + (i = n..<n+m. f (w i) (w (Suc i)))"
      by (simp add: sum.atLeastLessThan_concat)
    also have "... = (i = 0..<n. f (w i) (w (Suc i))) + (i = 0..<m. f (w (i+n)) (w (Suc (i+n))))"
      by (auto intro!: sum.reindex_bij_betw[symmetric] bij_betw_byWitness[of _ "λi. i-n"])
    also have "... = (i = 0..<n. f (u i) (u (Suc i))) + (i = 0..<m. f (v i) (v (Suc i)))"
      unfolding w_def apply (auto intro!: sum.cong)
      using U(2) V(1) Suc_lessI by fastforce
    also have "... < turn_into_distance f x y + e/2 + turn_into_distance f y z + e/2"
      using U(3) V(3) by auto
    finally show ?thesis by auto
  qed
  then show ?thesis
    using field_le_epsilon by blast
qed

text ‹Now comes the only nontrivial statement of the construction, the fact that the new
distance is bounded from below by $f/2$.

Here is the mathematical proof. We show by induction that all chains from $x$ to
$y$ satisfy this bound. Assume this is done for all chains of length $ < n$, we do it for a
chain of length $n$. Write $S = \sum f(u_i, u_{i+1})$ for the sum along the chain. Introduce $p$
the last index where the sum is $\leq S/2$. Then the sum from $0$ to $p$ is $\leq S/2$, and the sum
from $p+1$ to $n$ is also $\leq S/2$ (by maximality of $p$). The induction assumption
gives that $f (x, u_p)$ is bounded by twice the sum from $0$ to $p$, which is at most $S$. Same
thing for $f(u_{p+1}, y)$. With the weird triangle inequality applied two times, we get
$f (x, y) \leq 2 \max(f(x,u_p), f(u_p, u_{p+1}), f(u_{p+1}, y)) \leq 2S$, as claimed.

The formalization presents no difficulty.
›

lemma lower:
  "f x y  2 * turn_into_distance f x y"
proof -
  have I: "f (u 0) (u n)  ( i  {0..<n}. f (u i) (u (Suc i))) * 2" for n u
  proof (induction n arbitrary: u rule: less_induct)
    case (less n)
    show "f (u 0) (u n)  (i = 0..<n. f (u i) (u (Suc i))) * 2"
    proof (cases "n = 0")
      case True
      then have "f (u 0) (u n) = 0" using self_zero by auto
      then show ?thesis using True by auto
    next
      case False
      then have "n > 0" by auto
      define S where "S = (i = 0..<n. f (u i) (u (Suc i)))"
      have "S  0" unfolding S_def using nonneg by (auto simp add: sum_nonneg)
      have "p. p < n  (i = 0..<p. f (u i) (u (Suc i)))  S/2  (i = Suc p..<n. f (u i) (u (Suc i)))  S/2"
      proof (cases "S = 0")
        case True
        have "(i = Suc 0..<n. f (u i) (u (Suc i))) = (i = 0..<n. f (u i) (u (Suc i))) - f(u 0) (u (Suc 0))"
          using sum.atLeast_Suc_lessThan[OF n > 0, of "λi. f (u i) (u (Suc i))"] by simp
        also have "...  S/2" using True S_def nonneg by auto
        finally have "0 < n  (i = 0..<0. f (u i) (u (Suc i)))  S/2  (i = Suc 0..<n. f (u i) (u (Suc i)))  S/2"
          using n > 0 S = 0 by auto
        then show ?thesis by auto
      next
        case False
        then have "S > 0" using S  0 by simp
        define A where "A = {q. q  n  (i = 0..<q. f (u i) (u (Suc i)))  S/2}"
        have "0  A" unfolding A_def using S > 0 n > 0 by auto
        have "n  A" unfolding A_def using S > 0 unfolding S_def by auto
        define p where "p = Max A"
        have "p  A" unfolding p_def apply (rule Max_in) using 0  A unfolding A_def by auto
        then have L: "p  n" "(i = 0..<p. f (u i) (u (Suc i)))  S/2" unfolding A_def by auto
        then have "p < n" using n  A p  A le_neq_trans by blast
        have "Suc p  A" unfolding p_def
          by (metis (no_types, lifting) A_def Max_ge Suc_n_not_le_n infinite_nat_iff_unbounded mem_Collect_eq not_le p_def)
        then have *: "(i = 0..<Suc p. f (u i) (u (Suc i))) > S/2"
          unfolding A_def using p < n by auto
        have "( i = Suc p..<n. f (u i) (u (Suc i))) = S - (i = 0..<Suc p. f (u i) (u (Suc i)))"
          unfolding S_def using p < n by (metis (full_types) Suc_le_eq sum_diff_nat_ivl zero_le)
        also have "...  S/2" using * by auto
        finally have "p < n  (i = 0..<p. f (u i) (u (Suc i)))  S/2  (i = Suc p..<n. f (u i) (u (Suc i)))  S/2"
          using p < n L(2) by auto
        then show ?thesis by auto
      qed
      then obtain p where P: "p < n" "(i = 0..<p. f (u i) (u (Suc i)))  S/2" "(i = Suc p..<n. f (u i) (u (Suc i)))  S/2"
        by auto
      have "f (u 0) (u p)  (i = 0..<p. f (u i) (u (Suc i))) * 2"
        apply (rule less.IH) using p < n by auto
      then have A: "f (u 0) (u p)  S" using P(2) by auto
      have B: "f (u p) (u (Suc p))  S"
        apply (rule sum_nonneg_leq_bound[of "{0..<n}" "λi. f (u i) (u (Suc i))"])
        using nonneg S_def p < n by auto
      have "f (u (0 + Suc p)) (u ((n-Suc p) + Suc p))  (i = 0..<n-Suc p. f (u (i + Suc p)) (u (Suc i + Suc p))) * 2"
        apply (rule less.IH) using n > 0 by auto
      also have "... = 2 * (i = Suc p..<n. f (u i) (u (Suc i)))"
        by (auto intro!: sum.reindex_bij_betw bij_betw_byWitness[of _ "λi. i - Suc p"])
      also have "...  S" using P(3) by simp
      finally have C: "f (u (Suc p)) (u n)  S"
        using p < n by auto

      have "f (u 0) (u n)  sqrt 2 * max (f (u 0) (u p)) (f (u p) (u n))"
        using weak_triangle by simp
      also have "...  sqrt 2* max (f (u 0) (u p)) (sqrt 2 * max (f (u p) (u (Suc p))) (f (u (Suc p)) (u n)))"
        using weak_triangle by simp (meson max.cobounded2 order_trans)
      also have "...  sqrt 2 * max S (sqrt 2 * max S S)"
        using A B C by auto (simp add: le_max_iff_disj)
      also have "...  sqrt 2 * max (sqrt 2 * S) (sqrt 2 * max S S)"
        apply (intro mult_left_mono max.mono) using S  0 less_eq_real_def by auto
      also have "... = 2 * S"
        by auto
      finally show ?thesis
        unfolding S_def by simp
    qed
  qed
  have "f x y/2  turn_into_distance f x y"
    unfolding turn_into_distance_def by (rule cInf_greatest[OF nonempty], auto simp add: I)
  then show ?thesis by simp
qed

end (*of locale Turn_into_distance*)


section ‹The Gromov completion of a hyperbolic space›

subsection ‹The Gromov boundary as a set›

text ‹A sequence in a Gromov hyperbolic space converges to a point in the boundary if
the Gromov product $(u_n, u_m)_e$ tends to infinity when $m,n \to _infty$. The point at infinity
is defined as the equivalence class of such sequences, for the relation $u \sim v$ iff
$(u_n, v_n)_e \to \infty$ (or, equivalently, $(u_n, v_m)_e \to \infty$ when $m, n\to \infty$, or
one could also change basepoints). Hence, the Gromov boundary is naturally defined as a quotient
type. There is a difficulty: it can be empty in general, hence defining it as a type is not always
possible. One could introduce a new typeclass of Gromov hyperbolic spaces for which the boundary
is not empty (unboundedness is not enough, think of infinitely many segments $[0,n]$ all joined at
$0$), and then only define the boundary of such spaces. However, this is tedious. Rather, we
work with the Gromov completion (containing the space and its boundary), this is always not empty.
The price to pay is that, in the definition of the completion, we have to distinguish between
sequences converging to the boundary and sequences converging inside the space. This is more natural
to proceed in this way as the interesting features of the boundary come from the fact that its sits
at infinity of the initial space, so their relations (and the topology of $X \cup \partial X$) are
central.›

definition Gromov_converging_at_boundary::"(nat  ('a::Gromov_hyperbolic_space))  bool"
  where "Gromov_converging_at_boundary u = (a. (M::real). N. n  N.  m  N. Gromov_product_at a (u m) (u n)  M)"

lemma Gromov_converging_at_boundaryI:
  assumes "M. N. n  N. m  N. Gromov_product_at a (u m) (u n)  M"
  shows "Gromov_converging_at_boundary u"
unfolding Gromov_converging_at_boundary_def proof (auto)
  fix b::'a and M::real
  obtain N where *: "m n. n  N  m  N  Gromov_product_at a (u m) (u n)  M + dist a b"
    using assms[of "M + dist a b"] by auto
  have "Gromov_product_at b (u m) (u n)  M" if "m  N" "n  N" for m n
    using *[OF that] Gromov_product_at_diff1[of a "u m" "u n" b] by (smt Gromov_product_commute)
  then show "N. n  N. m  N. M  Gromov_product_at b (u m) (u n)" by auto
qed

lemma Gromov_converging_at_boundary_imp_unbounded:
  assumes "Gromov_converging_at_boundary u"
  shows "(λn. dist a (u n))  "
proof -
  have "N. n  N. dist a (u n)  M" for M::real
    using assms unfolding Gromov_converging_at_boundary_def Gromov_product_e_x_x[symmetric] by meson
  then show ?thesis
    unfolding tendsto_PInfty eventually_sequentially by (meson dual_order.strict_trans1 gt_ex less_ereal.simps(1))
qed

lemma Gromov_converging_at_boundary_imp_not_constant:
  "¬(Gromov_converging_at_boundary (λn. x))"
  using Gromov_converging_at_boundary_imp_unbounded[of "(λn. x)" "x"] Lim_bounded_PInfty by auto

lemma Gromov_converging_at_boundary_imp_not_constant':
  assumes "Gromov_converging_at_boundary u"
  shows "¬(m n. u m = u n)"
  using Gromov_converging_at_boundary_imp_not_constant
  by (metis (no_types) Gromov_converging_at_boundary_def assms order_refl)

text ‹We introduce a partial equivalence relation, defined over the sequences that converge to
infinity, and the constant sequences. Quotienting the space of admissible sequences by this
equivalence relation will give rise to the Gromov completion.›

definition Gromov_completion_rel::"(nat  'a::Gromov_hyperbolic_space)  (nat  'a)  bool"
  where "Gromov_completion_rel u v =
            (((Gromov_converging_at_boundary u  Gromov_converging_at_boundary v  (a. (λn. Gromov_product_at a (u n) (v n))  )))
             (n m. u n = v m  u n = u m  v n = v m))"

text ‹We need some basic lemmas to work separately with sequences tending to the boundary
and with constant sequences, as follows.›

lemma Gromov_completion_rel_const [simp]:
  "Gromov_completion_rel (λn. x) (λn. x)"
unfolding Gromov_completion_rel_def by auto

lemma Gromov_completion_rel_to_const:
  assumes "Gromov_completion_rel u (λn. x)"
  shows "u n = x"
using assms unfolding Gromov_completion_rel_def using Gromov_converging_at_boundary_imp_not_constant[of x] by auto

lemma Gromov_completion_rel_to_const':
  assumes "Gromov_completion_rel (λn. x) u"
  shows "u n = x"
using assms unfolding Gromov_completion_rel_def using Gromov_converging_at_boundary_imp_not_constant[of x] by auto

lemma Gromov_product_tendsto_PInf_a_b:
  assumes "(λn. Gromov_product_at a (u n) (v n))  "
  shows "(λn. Gromov_product_at b (u n) (v n))  "
proof (rule tendsto_sandwich[of "λn. ereal(Gromov_product_at a (u n) (v n)) + (- dist a b)" _ _ "λn. "])
  have "ereal(Gromov_product_at b (u n) (v n))  ereal(Gromov_product_at a (u n) (v n)) + (- dist a b)" for n
    using Gromov_product_at_diff1[of a "u n" "v n" b] by auto
  then show "F n in sequentially. ereal (Gromov_product_at a (u n) (v n)) + ereal (- dist a b)  ereal (Gromov_product_at b (u n) (v n))"
    by auto
  have "(λn. ereal(Gromov_product_at a (u n) (v n)) + (- dist a b))   + (- dist a b)"
    apply (intro tendsto_intros) using assms by auto
  then show "(λn. ereal (Gromov_product_at a (u n) (v n)) + ereal (- dist a b))  " by simp
qed (auto)

lemma Gromov_converging_at_boundary_rel:
  assumes "Gromov_converging_at_boundary u"
  shows "Gromov_completion_rel u u"
unfolding Gromov_completion_rel_def using Gromov_converging_at_boundary_imp_unbounded[OF assms] assms by auto

text ‹We can now prove that we indeed have an equivalence relation.›

lemma part_equivp_Gromov_completion_rel:
  "part_equivp Gromov_completion_rel"
proof (rule part_equivpI)
  show "x::(nat  'a). Gromov_completion_rel x x"
    apply (rule exI[of _ "λn. (SOME a::'a. True)"]) unfolding Gromov_completion_rel_def by (auto simp add: convergent_const)

  show "symp Gromov_completion_rel"
    unfolding symp_def Gromov_completion_rel_def by (auto simp add: Gromov_product_commute) metis+

  show "transp (Gromov_completion_rel::(nat  'a)  (nat  'a)  bool)"
  unfolding transp_def proof (intro allI impI)
    fix u v w::"nat'a"
    assume UV: "Gromov_completion_rel u v"
       and VW: "Gromov_completion_rel v w"
    show "Gromov_completion_rel u w"
    proof (cases "n m. v n = v m")
      case True
      define a where "a = v 0"
      have *: "v = (λn. a)" unfolding a_def using True by auto
      then have "u n = v 0" "w n = v 0" for n
        using Gromov_completion_rel_to_const' Gromov_completion_rel_to_const UV VW unfolding * by auto force
      then show ?thesis
        using UV VW unfolding Gromov_completion_rel_def by auto
    next
      case False
      have "(λn. Gromov_product_at a (u n) (w n))  " for a
      proof (rule tendsto_sandwich[of "λn. min (ereal (Gromov_product_at a (u n) (v n))) (ereal (Gromov_product_at a (v n) (w n))) + (- deltaG(TYPE('a)))" _ _ "λn. "])
        have "min (Gromov_product_at a (u n) (v n)) (Gromov_product_at a (v n) (w n)) - deltaG(TYPE('a))  Gromov_product_at a (u n) (w n)" for n
          by (rule hyperb_ineq)
        then have "min (ereal (Gromov_product_at a (u n) (v n))) (ereal (Gromov_product_at a (v n) (w n))) + ereal (- deltaG TYPE('a))  ereal (Gromov_product_at a (u n) (w n))" for n
          by (auto simp del: ereal_min simp add: ereal_min[symmetric])
        then show "F n in sequentially. min (ereal (Gromov_product_at a (u n) (v n))) (ereal (Gromov_product_at a (v n) (w n)))
                    + ereal (- deltaG TYPE('a))  ereal (Gromov_product_at a (u n) (w n))"
          unfolding eventually_sequentially by auto

        have "(λn. min (ereal (Gromov_product_at a (u n) (v n))) (ereal (Gromov_product_at a (v n) (w n))) + (- deltaG(TYPE('a))))  min   + (- deltaG(TYPE('a)))"
          apply (intro tendsto_intros) using UV VW False unfolding Gromov_completion_rel_def by auto
        then show "(λn. min (ereal (Gromov_product_at a (u n) (v n))) (ereal (Gromov_product_at a (v n) (w n))) + (- deltaG(TYPE('a))))  " by auto
      qed (auto)
      then show ?thesis
        using False UV VW unfolding Gromov_completion_rel_def by auto
    qed
  qed
qed

text ‹We can now define the Gromov completion of a Gromov hyperbolic space, considering either
sequences converging to a point on the boundary, or sequences converging inside the space, and
quotienting by the natural equivalence relation.›

quotient_type (overloaded) 'a Gromov_completion =
  "nat  ('a::Gromov_hyperbolic_space)"
  / partial: "Gromov_completion_rel"
by (rule part_equivp_Gromov_completion_rel)

text ‹The Gromov completion contains is made of a copy of the original space, and new points
forming the Gromov boundary.›

definition to_Gromov_completion::"('a::Gromov_hyperbolic_space)  'a Gromov_completion"
  where "to_Gromov_completion x = abs_Gromov_completion (λn. x)"

definition from_Gromov_completion::"('a::Gromov_hyperbolic_space) Gromov_completion  'a"
  where "from_Gromov_completion = inv to_Gromov_completion"

definition Gromov_boundary::"('a::Gromov_hyperbolic_space) Gromov_completion set"
  where "Gromov_boundary = UNIV - range to_Gromov_completion"

lemma to_Gromov_completion_inj:
  "inj to_Gromov_completion"
proof (rule injI)
  fix x y::'a assume H: "to_Gromov_completion x = to_Gromov_completion y"
  have "Gromov_completion_rel (λn. x) (λn. y)"
    apply (subst Quotient3_rel[OF Quotient3_Gromov_completion, symmetric])
    using H unfolding to_Gromov_completion_def by auto
  then show "x = y"
    using Gromov_completion_rel_to_const by auto
qed

lemma from_to_Gromov_completion [simp]:
  "from_Gromov_completion (to_Gromov_completion x) = x"
unfolding from_Gromov_completion_def by (simp add: to_Gromov_completion_inj)

lemma to_from_Gromov_completion:
  assumes "x  Gromov_boundary"
  shows "to_Gromov_completion (from_Gromov_completion x) = x"
using assms to_Gromov_completion_inj unfolding Gromov_boundary_def from_Gromov_completion_def
by (simp add: f_inv_into_f)

lemma not_in_Gromov_boundary:
  assumes "x  Gromov_boundary"
  shows "a. x = to_Gromov_completion a"
using assms unfolding Gromov_boundary_def by auto

lemma not_in_Gromov_boundary' [simp]:
  "to_Gromov_completion x  Gromov_boundary"
unfolding Gromov_boundary_def by auto

lemma abs_Gromov_completion_in_Gromov_boundary [simp]:
  assumes "Gromov_converging_at_boundary u"
  shows "abs_Gromov_completion u  Gromov_boundary"
using Gromov_completion_rel_to_const Gromov_converging_at_boundary_imp_not_constant'
  Gromov_converging_at_boundary_rel[OF assms]
  Quotient3_rel[OF Quotient3_Gromov_completion] assms not_in_Gromov_boundary to_Gromov_completion_def
  by fastforce

lemma rep_Gromov_completion_to_Gromov_completion [simp]:
  "rep_Gromov_completion (to_Gromov_completion y) = (λn. y)"
proof -
  have "Gromov_completion_rel (λn. y) (rep_Gromov_completion (abs_Gromov_completion (λn. y)))"
    by (metis Gromov_completion_rel_const Quotient3_Gromov_completion rep_abs_rsp)
  then show ?thesis
    unfolding to_Gromov_completion_def using Gromov_completion_rel_to_const' by blast
qed

text ‹To distinguish the case of points inside the space or in the boundary, we introduce the
following case distinction.›

lemma Gromov_completion_cases [case_names to_Gromov_completion boundary, cases type: Gromov_completion]:
  "(x. z = to_Gromov_completion x  P)  (z  Gromov_boundary  P)  P"
apply (cases "z  Gromov_boundary") using not_in_Gromov_boundary by auto


subsection ‹Extending the original distance and the original Gromov product to the completion›

text ‹In this subsection, we extend the Gromov product to the boundary, by taking limits along
sequences tending to the point in the boundary. This does not converge, but it does up to $\delta$,
so for definiteness we use a $\liminf$ over all sequences tending to the boundary point -- one
interest of this definition is that the extended Gromov product still satisfies the hyperbolicity
inequality. One difficulty is that this extended Gromov product can take infinite values (it does
so exactly on the pair $(x,x)$ where $x$ is in the boundary), so we should define this product
in extended nonnegative reals.

We also extend the original distance, by $+\infty$ on the boundary. This is not a really interesting
function, but it will be instrumental below. Again, this extended Gromov distance (not to be mistaken
for the genuine distance we will construct later on on the completion) takes values in extended
nonnegative reals.

Since the extended Gromov product and the extension of the original distance both take values in
$[0,+\infty]$, it may seem natural to define them in ennreal. This is the choice that was made in
a previous implementation, but it turns out that one keeps computing with these numbers, writing
down inequalities and subtractions. ennreal is ill suited for this kind of computations, as it only
works well with additions. Hence, the implementation was switched to ereal, where proofs are indeed
much smoother.

To define the extended Gromov product, one takes a limit of the Gromov product along any
sequence, as it does not depend up to $\delta$ on the chosen sequence. However, if one wants to
keep the exact inequality that defines hyperbolicity, but at all points, then using an infimum
is the best choice.›

definition extended_Gromov_product_at::"('a::Gromov_hyperbolic_space)  'a Gromov_completion  'a Gromov_completion  ereal"
  where "extended_Gromov_product_at e x y = Inf {liminf (λn. ereal(Gromov_product_at e (u n) (v n))) |u v. abs_Gromov_completion u = x  abs_Gromov_completion v = y  Gromov_completion_rel u u  Gromov_completion_rel v v}"

definition extended_Gromov_distance::"('a::Gromov_hyperbolic_space) Gromov_completion  'a Gromov_completion  ereal"
  where "extended_Gromov_distance x y =
              (if x  Gromov_boundary  y  Gromov_boundary then 
              else ereal (dist (inv to_Gromov_completion x) (inv to_Gromov_completion y)))"

text ‹The extended distance and the extended Gromov product are invariant under exchange
of the points, readily from the definition.›

lemma extended_Gromov_distance_commute:
  "extended_Gromov_distance x y = extended_Gromov_distance y x"
unfolding extended_Gromov_distance_def by (simp add: dist_commute)

lemma extended_Gromov_product_nonneg [mono_intros, simp]:
  "0  extended_Gromov_product_at e x y"
unfolding extended_Gromov_product_at_def by (rule Inf_greatest, auto intro: Liminf_bounded always_eventually)

lemma extended_Gromov_distance_nonneg [mono_intros, simp]:
  "0  extended_Gromov_distance x y"
unfolding extended_Gromov_distance_def by auto

lemma extended_Gromov_product_at_commute:
  "extended_Gromov_product_at e x y = extended_Gromov_product_at e y x"
unfolding extended_Gromov_product_at_def
proof (rule arg_cong[of _ _ Inf])
  have "{liminf (λn. ereal (Gromov_product_at e (u n) (v n))) |u v.
          abs_Gromov_completion u = x  abs_Gromov_completion v = y  Gromov_completion_rel u u  Gromov_completion_rel v v} =
        {liminf (λn. ereal (Gromov_product_at e (v n) (u n))) |u v.
          abs_Gromov_completion v = y  abs_Gromov_completion u = x  Gromov_completion_rel v v  Gromov_completion_rel u u}"
    by (auto simp add: Gromov_product_commute)
  then show "{liminf (λn. ereal (Gromov_product_at e (u n) (v n))) |u v.
      abs_Gromov_completion u = x  abs_Gromov_completion v = y  Gromov_completion_rel u u  Gromov_completion_rel v v} =
      {liminf (λn. ereal (Gromov_product_at e (u n) (v n))) |u v.
      abs_Gromov_completion u = y  abs_Gromov_completion v = x  Gromov_completion_rel u u  Gromov_completion_rel v v}"
    by auto
qed

text ‹Inside the space, the extended distance and the extended Gromov product coincide with the
original ones.›

lemma extended_Gromov_distance_inside [simp]:
  "extended_Gromov_distance (to_Gromov_completion x) (to_Gromov_completion y) = dist x y"
unfolding extended_Gromov_distance_def Gromov_boundary_def by (auto simp add: to_Gromov_completion_inj)

lemma extended_Gromov_product_inside [simp] :
  "extended_Gromov_product_at e (to_Gromov_completion x) (to_Gromov_completion y) = Gromov_product_at e x y"
proof -
  have A: "u = (λn. z)" if H: "abs_Gromov_completion u = abs_Gromov_completion (λn. z)" "Gromov_completion_rel u u" for u and z::'a
  proof -
    have "Gromov_completion_rel u (λn. z)"
      apply (subst Quotient3_rel[OF Quotient3_Gromov_completion, symmetric])
      using H uniformity_dist_class_def by auto
    then show ?thesis using Gromov_completion_rel_to_const by auto
  qed
  then have *: "{u. abs_Gromov_completion u = to_Gromov_completion z  Gromov_completion_rel u u} = {(λn. z)}" for z::'a
    unfolding to_Gromov_completion_def by auto
  have **: "{F u v |u v. abs_Gromov_completion u = to_Gromov_completion x  abs_Gromov_completion v = to_Gromov_completion y  Gromov_completion_rel u u  Gromov_completion_rel v v}
      = {F (λn. x) (λn. y)}" for F::"(nat  'a)  (nat  'a)  ereal"
    using *[of x] *[of y] unfolding extended_Gromov_product_at_def by (auto, smt mem_Collect_eq singletonD)

  have "extended_Gromov_product_at e (to_Gromov_completion x) (to_Gromov_completion y) = Inf {liminf (λn. ereal(Gromov_product_at e ((λn. x) n) ((λn. y) n)))}"
    unfolding extended_Gromov_product_at_def ** by simp
  also have "... = ereal(Gromov_product_at e x y)"
    by (auto simp add: Liminf_const)
  finally show "extended_Gromov_product_at e (to_Gromov_completion x) (to_Gromov_completion y) = Gromov_product_at e x y"
    by simp
qed

text ‹A point in the boundary is at infinite extended distance of everyone, including itself:
the extended distance is obtained by taking the supremum along all sequences tending to this point,
so even for one single point one can take two sequences tending to it at different speeds, which
results in an infinite extended distance.›

lemma extended_Gromov_distance_PInf_boundary [simp]:
  assumes "x  Gromov_boundary"
  shows "extended_Gromov_distance x y = " "extended_Gromov_distance y x = "
unfolding extended_Gromov_distance_def using assms by auto

text ‹By construction, the extended distance still satisfies the triangle inequality.›

lemma extended_Gromov_distance_triangle [mono_intros]:
  "extended_Gromov_distance x z  extended_Gromov_distance x y + extended_Gromov_distance y z"
proof (cases "x  Gromov_boundary  y  Gromov_boundary  z  Gromov_boundary")
  case True
  then have *: "extended_Gromov_distance x y + extended_Gromov_distance y z = " by auto
  show ?thesis by (simp add: *)
next
  case False
  then obtain a b c where abc: "x = to_Gromov_completion a" "y = to_Gromov_completion b" "z = to_Gromov_completion c"
    unfolding Gromov_boundary_def by auto
  show ?thesis
    unfolding abc using dist_triangle[of a c b] ennreal_leI by fastforce
qed

text ‹The extended Gromov product can be bounded by the extended distance, just like inside
the space.›

lemma extended_Gromov_product_le_dist [mono_intros]:
  "extended_Gromov_product_at e x y  extended_Gromov_distance (to_Gromov_completion e) x"
proof (cases x)
  case boundary
  then show ?thesis by simp
next
  case (to_Gromov_completion a)
  define v where "v = rep_Gromov_completion y"
  have *: "abs_Gromov_completion (λn. a) = x  abs_Gromov_completion v = y  Gromov_completion_rel (λn. a) (λn. a)  Gromov_completion_rel v v"
    unfolding v_def to_Gromov_completion to_Gromov_completion_def
    by (auto simp add: Quotient3_rep_reflp[OF Quotient3_Gromov_completion] Quotient3_abs_rep[OF Quotient3_Gromov_completion])
  have "extended_Gromov_product_at e x y  liminf (λn. ereal(Gromov_product_at e a (v n)))"
    unfolding extended_Gromov_product_at_def apply (rule Inf_lower) using * by force
  also have "...  liminf (λn. ereal(dist e a))"
    using Gromov_product_le_dist(1)[of e a] by (auto intro!: Liminf_mono)
  also have "... = ereal(dist e a)"
    by (simp add: Liminf_const)
  also have "... = extended_Gromov_distance (to_Gromov_completion e) x"
    unfolding to_Gromov_completion by auto
  finally show ?thesis by auto
qed

lemma extended_Gromov_product_le_dist' [mono_intros]:
  "extended_Gromov_product_at e x y  extended_Gromov_distance (to_Gromov_completion e) y"
using extended_Gromov_product_le_dist[of e y x] by (simp add: extended_Gromov_product_at_commute)

text ‹The Gromov product inside the space varies by at most the distance when one varies one of
the points. We will need the same statement for the extended Gromov product. The proof is done
using this inequality inside the space, and passing to the limit.›

lemma extended_Gromov_product_at_diff3 [mono_intros]:
  "extended_Gromov_product_at e x y  extended_Gromov_product_at e x z + extended_Gromov_distance y z"
proof (cases "(extended_Gromov_distance y z = )  (extended_Gromov_product_at e x z = )")
  case False
  then have "y  Gromov_boundary" "z  Gromov_boundary"
    using extended_Gromov_distance_PInf_boundary by auto
  then obtain b c where b: "y = to_Gromov_completion b" and c: "z = to_Gromov_completion c"
    unfolding Gromov_boundary_def by auto
  have "extended_Gromov_distance y z = ereal(dist b c)"
    unfolding b c by auto
  have "extended_Gromov_product_at e x y  (extended_Gromov_product_at e x z + extended_Gromov_distance y z) + h" if "h>0" for h
  proof -
    have "t{liminf (λn. ereal(Gromov_product_at e (u n) (w n))) |u w. abs_Gromov_completion u = x
                   abs_Gromov_completion w = z  Gromov_completion_rel u u  Gromov_completion_rel w w}.
          t < extended_Gromov_product_at e x z + h"
      apply (subst Inf_less_iff[symmetric]) using False h > 0 extended_Gromov_product_nonneg[of e x z] unfolding extended_Gromov_product_at_def[symmetric]
      by (metis add.right_neutral ereal_add_left_cancel_less order_refl)
    then obtain u w where H: "abs_Gromov_completion u = x" "abs_Gromov_completion w = z"
                          "Gromov_completion_rel u u" "Gromov_completion_rel w w"
                          "liminf (λn. ereal(Gromov_product_at e (u n) (w n))) < extended_Gromov_product_at e x z + h"
      by auto
    then have w: "w n = c" for n
      using c Gromov_completion_rel_to_const Quotient3_Gromov_completion Quotient3_rel to_Gromov_completion_def by fastforce
    define v where v: "v = (λn::nat. b)"
    have "abs_Gromov_completion v = y" "Gromov_completion_rel v v"
      unfolding v by (auto simp add: b to_Gromov_completion_def)

    have "Gromov_product_at e (u n) (v n)  Gromov_product_at e (u n) (w n) + dist b c" for n
      unfolding v w using Gromov_product_at_diff3[of e "u n" b c] by auto
    then have *: "ereal(Gromov_product_at e (u n) (v n))  ereal(Gromov_product_at e (u n) (w n)) + extended_Gromov_distance y z" for n
      unfolding extended_Gromov_distance y z = ereal(dist b c) by fastforce
    have "extended_Gromov_product_at e x y  liminf(λn. ereal(Gromov_product_at e (u n) (v n)))"
      unfolding extended_Gromov_product_at_def by (rule Inf_lower, auto, rule exI[of _ u], rule exI[of _ v], auto, fact+)
    also have "...  liminf(λn. ereal(Gromov_product_at e (u n) (w n)) + extended_Gromov_distance y z)"
      apply (rule Liminf_mono) using * unfolding eventually_sequentially by auto
    also have "... = liminf(λn. ereal(Gromov_product_at e (u n) (w n))) + extended_Gromov_distance y z"
      apply (rule Liminf_add_ereal_right) using False by auto
    also have "...  extended_Gromov_product_at e x z + h + extended_Gromov_distance y z"
      using less_imp_le[OF H(5)] by (auto intro: mono_intros)
    finally show ?thesis
      by (simp add: algebra_simps)
  qed
  then show ?thesis
    using ereal_le_epsilon by blast
next
  case True
  then show ?thesis by auto
qed

lemma extended_Gromov_product_at_diff2 [mono_intros]:
  "extended_Gromov_product_at e x y  extended_Gromov_product_at e z y + extended_Gromov_distance x z"
using extended_Gromov_product_at_diff3[of e y x z] by (simp add: extended_Gromov_product_at_commute)

lemma extended_Gromov_product_at_diff1 [mono_intros]:
  "extended_Gromov_product_at e x y  extended_Gromov_product_at f x y + dist e f"
proof (cases "extended_Gromov_product_at f x y = ")
  case False
  have "extended_Gromov_product_at e x y  (extended_Gromov_product_at f x y + dist e f) + h" if "h > 0" for h
  proof -
    have "t{liminf (λn. ereal(Gromov_product_at f (u n) (v n))) |u v. abs_Gromov_completion u = x
                 abs_Gromov_completion v = y  Gromov_completion_rel u u  Gromov_completion_rel v v}.
          t < extended_Gromov_product_at f x y + h"
      apply (subst Inf_less_iff[symmetric]) using False h > 0 extended_Gromov_product_nonneg[of f x y] unfolding extended_Gromov_product_at_def[symmetric]
      by (metis add.right_neutral ereal_add_left_cancel_less order_refl)
    then obtain u v where H: "abs_Gromov_completion u = x" "abs_Gromov_completion v = y"
                          "Gromov_completion_rel u u" "Gromov_completion_rel v v"
                          "liminf (λn. ereal(Gromov_product_at f (u n) (v n))) < extended_Gromov_product_at f x y + h"
      by auto

    have "Gromov_product_at e (u n) (v n)  Gromov_product_at f (u n) (v n) + dist e f" for n
      using Gromov_product_at_diff1[of e "u n" "v n" f] by auto
    then have *: "ereal(Gromov_product_at e (u n) (v n))  ereal(Gromov_product_at f (u n) (v n)) + dist e f" for n
      by fastforce
    have "extended_Gromov_product_at e x y  liminf(λn. ereal(Gromov_product_at e (u n) (v n)))"
      unfolding extended_Gromov_product_at_def by (rule Inf_lower, auto, rule exI[of _ u], rule exI[of _ v], auto, fact+)
    also have "...  liminf(λn. ereal(Gromov_product_at f (u n) (v n)) + dist e f)"
      apply (rule Liminf_mono) using * unfolding eventually_sequentially by auto
    also have "... = liminf(λn. ereal(Gromov_product_at f (u n) (v n))) + dist e f"
      apply (rule Liminf_add_ereal_right) using False by auto
    also have "...  extended_Gromov_product_at f x y + h + dist e f"
      using less_imp_le[OF H(5)] by (auto intro: mono_intros)
    finally show ?thesis
      by (simp add: algebra_simps)
  qed
  then show ?thesis
    using ereal_le_epsilon by blast
next
  case True
  then show ?thesis by auto
qed

text ‹A point in the Gromov boundary is represented by a sequence tending to infinity and
converging in the Gromov boundary, essentially by definition.›

lemma Gromov_boundary_abs_converging:
  assumes "x  Gromov_boundary" "abs_Gromov_completion u = x" "Gromov_completion_rel u u"
  shows "Gromov_converging_at_boundary u"
proof -
  have "Gromov_converging_at_boundary u  (m n. u n = u m)"
    using assms unfolding Gromov_completion_rel_def by auto
  moreover have "¬(m n. u n = u m)"
  proof (rule ccontr, simp)
    assume *: "m n. u n = u m"
    define z where "z = u 0"
    then have z: "u = (λn. z)"
      using * by auto
    then have "x = to_Gromov_completion z"
      using assms unfolding z to_Gromov_completion_def by auto
    then show False using x  Gromov_boundary unfolding Gromov_boundary_def by auto
  qed
  ultimately show ?thesis by auto
qed

lemma Gromov_boundary_rep_converging:
  assumes "x  Gromov_boundary"
  shows "Gromov_converging_at_boundary (rep_Gromov_completion x)"
apply (rule Gromov_boundary_abs_converging[OF assms])
using Quotient3_Gromov_completion Quotient3_abs_rep Quotient3_rep_reflp by fastforce+

text ‹We can characterize the points for which the Gromov product is infinite: they have to be
the same point, at infinity. This is essentially equivalent to the definition of the Gromov
completion, but there is some boilerplate to get the proof working.›

lemma Gromov_boundary_extended_product_PInf [simp]:
  "extended_Gromov_product_at e x y =   (x  Gromov_boundary  y = x)"
proof
  fix x y::"'a Gromov_completion" assume "x  Gromov_boundary  y = x"
  then have H: "y = x" "x  Gromov_boundary" by auto
  have *: "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = " if
                  "abs_Gromov_completion u = x" "abs_Gromov_completion v = y"
                  "Gromov_completion_rel u u" "Gromov_completion_rel v v" for u v
  proof -
    have "Gromov_converging_at_boundary u" "Gromov_converging_at_boundary v"
      using Gromov_boundary_abs_converging that H by auto
    have "Gromov_completion_rel u v" using that y = x
      using Quotient3_rel[OF Quotient3_Gromov_completion] by fastforce
    then have "(λn. Gromov_product_at e (u n) (v n))  "
      unfolding Gromov_completion_rel_def using Gromov_converging_at_boundary_imp_not_constant'[OF Gromov_converging_at_boundary u] by auto
    then show ?thesis
      by (simp add: tendsto_iff_Liminf_eq_Limsup)
  qed
  then show "extended_Gromov_product_at e x y = "
    unfolding extended_Gromov_product_at_def by (auto intro: Inf_eqI)
next
  fix x y::"'a Gromov_completion" assume H: "extended_Gromov_product_at e x y = "
  then have "extended_Gromov_distance (to_Gromov_completion e) x = "
    using extended_Gromov_product_le_dist[of e x y] neq_top_trans by auto
  then have "x  Gromov_boundary"
    by (metis ereal.distinct(1) extended_Gromov_distance_def infinity_ereal_def not_in_Gromov_boundary')
  have "extended_Gromov_distance (to_Gromov_completion e) y = "
    using extended_Gromov_product_le_dist[of e y x] neq_top_trans H by (auto simp add: extended_Gromov_product_at_commute)
  then have "y  Gromov_boundary"
    by (metis ereal.distinct(1) extended_Gromov_distance_def infinity_ereal_def not_in_Gromov_boundary')
  define u where "u = rep_Gromov_completion x"
  define v where "v = rep_Gromov_completion y"
  have A: "Gromov_converging_at_boundary u" "Gromov_converging_at_boundary v"
    unfolding u_def v_def using x  Gromov_boundary y  Gromov_boundary
    by (auto simp add: Gromov_boundary_rep_converging)

  have "abs_Gromov_completion u = x  abs_Gromov_completion v = y  Gromov_completion_rel u u  Gromov_completion_rel v v"
    unfolding u_def v_def
    using Quotient3_abs_rep[OF Quotient3_Gromov_completion] Quotient3_rep_reflp[OF Quotient3_Gromov_completion] by auto
  then have "extended_Gromov_product_at e x y  liminf (λn. ereal(Gromov_product_at e (u n) (v n)))"
    unfolding extended_Gromov_product_at_def by (auto intro!: Inf_lower)
  then have "(λn. ereal(Gromov_product_at e (u n) (v n)))  "
    unfolding H by (simp add: liminf_PInfty)
  then have "(λn. ereal(Gromov_product_at a (u n) (v n)))  " for a
    using Gromov_product_tendsto_PInf_a_b by auto

  then have "Gromov_completion_rel u v"
    unfolding Gromov_completion_rel_def using A by auto
  then have "abs_Gromov_completion u = abs_Gromov_completion v"
    using Quotient3_rel_abs[OF Quotient3_Gromov_completion] by auto
  then have "x = y"
    unfolding u_def v_def Quotient3_abs_rep[OF Quotient3_Gromov_completion] by auto
  then show "x  Gromov_boundary  y = x"
    using x  Gromov_boundary by auto
qed

text ‹As for points inside the space, we deduce that the extended Gromov product between $x$ and $x$
is just the extended distance to the basepoint.›

lemma extended_Gromov_product_e_x_x [simp]:
  "extended_Gromov_product_at e x x = extended_Gromov_distance (to_Gromov_completion e) x"
proof (cases x)
  case boundary
  then show ?thesis using Gromov_boundary_extended_product_PInf by auto
next
  case (to_Gromov_completion a)
  then show ?thesis by auto
qed

text ‹The inequality in terms of Gromov products characterizing hyperbolicity extends in the
same form to the Gromov completion, by taking limits of this inequality in the space.›

lemma extended_hyperb_ineq [mono_intros]:
  "extended_Gromov_product_at (e::'a::Gromov_hyperbolic_space) x z 
      min (extended_Gromov_product_at e x y) (extended_Gromov_product_at e y z) - deltaG(TYPE('a))"
proof -
  have "min (extended_Gromov_product_at e x y) (extended_Gromov_product_at e y z) - deltaG(TYPE('a)) 
    Inf {liminf (λn. ereal (Gromov_product_at e (u n) (v n))) |u v.
            abs_Gromov_completion u = x  abs_Gromov_completion v = z  Gromov_completion_rel u u  Gromov_completion_rel v v}"
  proof (rule cInf_greatest, auto)
    define u where "u = rep_Gromov_completion x"
    define w where "w = rep_Gromov_completion z"
    have "abs_Gromov_completion u = x  abs_Gromov_completion w = z  Gromov_completion_rel u u  Gromov_completion_rel w w"
      unfolding u_def w_def
      using Quotient3_abs_rep[OF Quotient3_Gromov_completion] Quotient3_rep_reflp[OF Quotient3_Gromov_completion] by auto
    then show "t u. Gromov_completion_rel u u 
            (v. abs_Gromov_completion v = z  abs_Gromov_completion u = x  t = liminf (λn. ereal (Gromov_product_at e (u n) (v n)))  Gromov_completion_rel v v)"
      by auto
  next
    fix u w assume H: "x = abs_Gromov_completion u" "z = abs_Gromov_completion w"
                      "Gromov_completion_rel u u" "Gromov_completion_rel w w"
    define v where "v = rep_Gromov_completion y"
    have Y: "y = abs_Gromov_completion v" "Gromov_completion_rel v v"
      unfolding v_def
      by (auto simp add: Quotient3_abs_rep[OF Quotient3_Gromov_completion] Quotient3_rep_reflp[OF Quotient3_Gromov_completion])

    have *: "min (ereal(Gromov_product_at e (u n) (v n))) (ereal(Gromov_product_at e (v n) (w n)))  ereal(Gromov_product_at e (u n) (w n)) + deltaG(TYPE('a))" for n
      by (subst ereal_min[symmetric], subst plus_ereal.simps(1), intro mono_intros)

    have "extended_Gromov_product_at e (abs_Gromov_completion u) y  liminf (λn. ereal(Gromov_product_at e (u n) (v n)))"
      unfolding extended_Gromov_product_at_def using Y H by (auto intro!: Inf_lower)
    moreover have "extended_Gromov_product_at e y (abs_Gromov_completion w)  liminf (λn. ereal(Gromov_product_at e (v n) (w n)))"
      unfolding extended_Gromov_product_at_def using Y H by (auto intro!: Inf_lower)
    ultimately have "min (extended_Gromov_product_at e (abs_Gromov_completion u) y) (extended_Gromov_product_at e y (abs_Gromov_completion w))
       min (liminf (λn. ereal(Gromov_product_at e (u n) (v n)))) (liminf (λn. ereal(Gromov_product_at e (v n) (w n))))"
      by (intro mono_intros, auto)
    also have "... = liminf (λn. min (ereal(Gromov_product_at e (u n) (v n))) (ereal(Gromov_product_at e (v n) (w n))))"
      by (rule Liminf_min_eq_min_Liminf[symmetric])
    also have "...  liminf (λn. ereal(Gromov_product_at e (u n) (w n)) + deltaG(TYPE('a)))"
      using * by (auto intro!: Liminf_mono)
    also have "... = liminf (λn. ereal(Gromov_product_at e (u n) (w n))) + deltaG(TYPE('a))"
      by (intro Liminf_add_ereal_right, auto)
    finally show "min (extended_Gromov_product_at e (abs_Gromov_completion u) y) (extended_Gromov_product_at e y (abs_Gromov_completion w))
                   liminf (λn. ereal (Gromov_product_at e (u n) (w n))) + ereal (deltaG TYPE('a))"
      by simp
  qed
  then show ?thesis unfolding extended_Gromov_product_at_def by auto
qed

lemma extended_hyperb_ineq' [mono_intros]:
  "extended_Gromov_product_at (e::'a::Gromov_hyperbolic_space) x z + deltaG(TYPE('a)) 
      min (extended_Gromov_product_at e x y) (extended_Gromov_product_at e y z)"
using extended_hyperb_ineq[of e x y z] unfolding ereal_minus_le_iff by (simp add: add.commute)

lemma zero_le_ereal [mono_intros]:
  assumes "0  z"
  shows "0  ereal z"
using assms by auto

lemma extended_hyperb_ineq_4_points' [mono_intros]:
  "Min {extended_Gromov_product_at (e::'a::Gromov_hyperbolic_space) x y, extended_Gromov_product_at e y z, extended_Gromov_product_at e z t}  extended_Gromov_product_at e x t + 2 * deltaG(TYPE('a))"
proof -
  have "min (extended_Gromov_product_at e x y + 0) (min (extended_Gromov_product_at e y z) (extended_Gromov_product_at e z t))
         min (extended_Gromov_product_at e x y + deltaG(TYPE('a))) (extended_Gromov_product_at e y t + deltaG(TYPE('a))) "
    by (intro mono_intros)
  also have "... = min (extended_Gromov_product_at e x y) (extended_Gromov_product_at e y t) + deltaG(TYPE('a))"
    by (simp add: add_mono_thms_linordered_semiring(3) dual_order.antisym min_def)
  also have "...  (extended_Gromov_product_at e x t + deltaG(TYPE('a))) + deltaG(TYPE('a))"
    by (intro mono_intros)
  finally show ?thesis apply (auto simp add: algebra_simps)
    by (metis (no_types, opaque_lifting) add.commute add.left_commute mult_2_right plus_ereal.simps(1))
qed

lemma extended_hyperb_ineq_4_points [mono_intros]:
  "Min {extended_Gromov_product_at (e::'a::Gromov_hyperbolic_space) x y, extended_Gromov_product_at e y z, extended_Gromov_product_at e z t} - 2 * deltaG(TYPE('a))  extended_Gromov_product_at e x t"
using extended_hyperb_ineq_4_points'[of e x y z] unfolding ereal_minus_le_iff by (simp add: add.commute)


subsection ‹Construction of the distance on the Gromov completion›

text ‹We want now to define the natural topology of the Gromov completion. Most textbooks
first define a topology on $\partial X$, or sometimes on
$X \cup \partial X$, and then much later a distance on $\partial X$ (but they never do the tedious
verification that the distance defines the same topology as the topology defined before). I have
not seen one textbook defining a distance on $X \cup \partial X$. It turns out that one can in fact
define a distance on $X \cup \partial X$, whose restriction to $\partial X$ is the usual distance
on the Gromov boundary, and define the topology of $X \cup \partial X$ using it. For formalization
purposes, this is very convenient as topologies defined with distances are automatically nice and
tractable (no need to check separation axioms, for instance). The price to pay is that, once
we have defined the distance, we have to check that it defines the right notion of convergence
one expects.

What we would like to take for the distance is
$d(x,y) = e^{-(x,y)_o}$, where $o$ is some fixed basepoint in the space. However, this
does not behave like a distance at small scales (but it is essentially the right thing at large
scales), and it does not really satisfy the triangle inequality. However, $e^{-\epsilon (x,y)_o}$
almost satisfies the triangle inequality if $\epsilon$ is small enough, i.e., it is equivalent
to a function satisfying the triangle inequality. This gives a genuine distance on the boundary,
but not inside the space as it does not vanish on pairs $(x,x)$.

A third try would be to take $d(x,y) = \min(\tilde d(x,y), e^{-\epsilon (x,y)_o})$ where
$\tilde d$ is the natural extension of $d$ to the Gromov completion (it is infinite if $x$ or $y$
belongs to the boundary). However, we can not prove that it is equivalent to a distance.

Finally, it works with $d(x,y) \asymp \min(\tilde d(x,y)^{1/2}, e^{-\epsilon (x,y)_o}$. This is
what we will prove below. To construct the distance, we use the results proved in
the locale \verb+Turn_into_distance+. For this, we need to check that our quasi-distance
satisfies a weird version of the triangular inequality.

All this construction depends on a basepoint, that we fix arbitrarily once and for all.
›

definition epsilonG::"('a::Gromov_hyperbolic_space) itself  real"
  where "epsilonG _ = ln 2 / (2+2*deltaG(TYPE('a)))"

definition basepoint::"'a"
  where "basepoint = (SOME a. True)"

lemma constant_in_extended_predist_pos [simp, mono_intros]:
  "epsilonG(TYPE('a::Gromov_hyperbolic_space)) > 0"
  "epsilonG(TYPE('a::Gromov_hyperbolic_space))  0"
  "ennreal (epsilonG(TYPE('a))) * top = top"
proof -
  have *: "2+2*deltaG(TYPE('a))  2 + 2 * 0"
    by (intro mono_intros, auto)
  show **: "epsilonG(TYPE('a)) > 0"
    unfolding epsilonG_def apply (auto simp add: divide_simps) using * by auto
  then show "ennreal (epsilonG(TYPE('a))) * top = top"
    using ennreal_mult_top by auto
  show "epsilonG(TYPE('a::Gromov_hyperbolic_space))  0"
    using ** by simp
qed

definition extended_predist::"('a::Gromov_hyperbolic_space) Gromov_completion  'a Gromov_completion  real"
  where "extended_predist x y = real_of_ereal (min (esqrt (extended_Gromov_distance x y))
          (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)))"

lemma extended_predist_ereal:
  "ereal (extended_predist x (y::('a::Gromov_hyperbolic_space) Gromov_completion)) = min (esqrt (extended_Gromov_distance x y))
          (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y))"
proof -
  have "eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)  eexp (0)"
    by (intro mono_intros, simp add: ereal_mult_le_0_iff)
  then have A: "min (esqrt (extended_Gromov_distance x y)) (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y))  1"
    unfolding min_def using order_trans by fastforce
  show ?thesis
    unfolding extended_predist_def apply (rule ereal_real') using A by auto
qed

lemma extended_predist_nonneg [simp, mono_intros]:
  "extended_predist x y  0"
unfolding extended_predist_def min_def by (auto intro: real_of_ereal_pos)

lemma extended_predist_commute:
  "extended_predist x y = extended_predist y x"
unfolding extended_predist_def by (simp add: extended_Gromov_distance_commute extended_Gromov_product_at_commute)

lemma extended_predist_self0 [simp]:
  "extended_predist x y = 0  x = y"
proof (auto)
  show "extended_predist y y = 0"
  proof (cases y)
    case boundary
    then have *: "extended_Gromov_product_at basepoint y y = "
      using Gromov_boundary_extended_product_PInf by auto
    show ?thesis unfolding extended_predist_def * apply (auto simp add: min_def)
      using constant_in_extended_predist_pos(1)[where ?'a = 'a] boundary by auto
  next
    case (to_Gromov_completion a)
    then show ?thesis unfolding extended_predist_def by (auto simp add: min_def)
  qed
  assume "extended_predist x y = 0"
  then have "esqrt (extended_Gromov_distance x y) = 0  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y) = 0"
    by (metis extended_predist_ereal min_def zero_ereal_def)
    then show "x = y"
  proof
    assume "esqrt (extended_Gromov_distance x y) = 0"
    then have *: "extended_Gromov_distance x y = 0"
      using extended_Gromov_distance_nonneg by (metis ereal_zero_mult esqrt_square)
    then have "¬(x  Gromov_boundary)" "¬(y  Gromov_boundary)" by auto
    then obtain a b where ab: "x = to_Gromov_completion a" "y = to_Gromov_completion b"
      unfolding Gromov_boundary_def by auto
    have "a = b" using * unfolding ab by auto
    then show "x = y" using ab by auto
  next
    assume "eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y) = 0"
    then have "extended_Gromov_product_at basepoint x y = "
      by auto
    then show "x = y"
      using Gromov_boundary_extended_product_PInf[of basepoint x y] by auto
  qed
qed

lemma extended_predist_le1 [simp, mono_intros]:
  "extended_predist x y  1"
proof -
  have "eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)  eexp (0)"
    by (intro mono_intros, simp add: ereal_mult_le_0_iff)
  then have "min (esqrt (extended_Gromov_distance x y)) (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y))  1"
    unfolding min_def using order_trans by fastforce
  then show ?thesis
    unfolding extended_predist_def by (simp add: real_of_ereal_le_1)
qed

lemma extended_predist_weak_triangle:
  "extended_predist x z  sqrt 2 * max (extended_predist x y) (extended_predist y z)"
proof -
  have Z: "esqrt 2 = eexp (ereal(ln 2/2))"
    by (subst esqrt_eq_iff_square, auto simp add: exp_add[symmetric])

  have A: "eexp(ereal(epsilonG TYPE('a)) * 1)  esqrt 2"
    unfolding Z epsilonG_def apply auto
    apply (auto simp add: algebra_simps divide_simps intro!: mono_intros)
    using delta_nonneg[where ?'a = 'a] by auto

  text ‹We have to show an inequality $d(x, z) \leq \sqrt{2} \max(d(x,y), d(y,z))$. Each of $d(x,y)$
  and $d(y,z)$ is either the extended distance, or the exponential of minus the Gromov product,
  depending on which is smaller. We split according to the four cases.›

  have "(esqrt (extended_Gromov_distance x y)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)
         esqrt (extended_Gromov_distance x y)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y))
        
      ((esqrt (extended_Gromov_distance y z)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint y z)
         esqrt (extended_Gromov_distance y z)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint y z)))"
    by auto
  then have "ereal(extended_predist x z)  ereal (sqrt 2) * max (ereal(extended_predist x y)) (ereal (extended_predist y z))"
  proof (auto)

    text ‹First, consider the case where the minimum is the extended distance for both cases.
    Then $ed(x,z) \leq ed(x,y) + ed(y,z) \leq 2 \max(ed(x,y), ed(y,z))$. Therefore, $ed(x,z)^{1/2}
    \leq \sqrt{2} \max(ed(x,y)^{1/2}, ed(y,z)^{1/2})$. As predist is defined using
    the square root of $ed$, this readily gives the result.›
    assume H: "esqrt (extended_Gromov_distance x y)  eexp (ereal (- epsilonG TYPE('a)) * extended_Gromov_product_at basepoint x y)"
              "esqrt (extended_Gromov_distance y z)  eexp (ereal (- epsilonG TYPE('a)) * extended_Gromov_product_at basepoint y z)"
    have "extended_Gromov_distance x z  extended_Gromov_distance x y + extended_Gromov_distance y z"
      by (rule extended_Gromov_distance_triangle)
    also have "...  2 * max (extended_Gromov_distance x y) (extended_Gromov_distance y z)"
      by (simp add: add_mono add_mono_thms_linordered_semiring(1) mult_2_ereal)
    finally have "esqrt (extended_Gromov_distance x z)  esqrt (2 * max (extended_Gromov_distance x y) (extended_Gromov_distance y z))"
      by (intro mono_intros)
    also have "... = esqrt 2 * max (esqrt (extended_Gromov_distance x y)) (esqrt (extended_Gromov_distance y z))"
      by (auto simp add: esqrt_mult max_of_mono[OF esqrt_mono])
    finally show ?thesis unfolding extended_predist_ereal min_def using H by auto

  next
    text ‹Next, consider the case where the minimum comes from the Gromov product for both cases.
    Then, the conclusion will come for the hyperbolicity inequality (which is valid in the Gromov
    completion as well). There is an additive loss of $\delta$ in this inequality, which is converted
    to a multiplicative loss after taking the exponential to get the distance. Since, in the formula
    for the distance, the Gromov product is multiplied by a constant $\epsilon$ by design, the loss
    we get in the end is $\exp(\delta \epsilon)$. The precise value of $\epsilon$ we have taken is
    designed so that this is at most $\sqrt{2}$, giving the desired conclusion.›
    assume H: "eexp (ereal (- epsilonG TYPE('a)) * extended_Gromov_product_at basepoint x y)  esqrt (extended_Gromov_distance x y)"
              "eexp (ereal (- epsilonG TYPE('a)) * extended_Gromov_product_at basepoint y z)  esqrt (extended_Gromov_distance y z)"

    text ‹First, check that $\epsilon$ and $\delta$ satisfy the required inequality
    $\exp(\epsilon \delta) \leq \sqrt{2}$ (but in the extended reals as this is what we will use.›
    have B: "eexp (epsilonG(TYPE('a)) * deltaG(TYPE('a)))  esqrt 2"
      unfolding epsilonG_def esqrt 2 = eexp (ereal(ln 2/2))
      apply (auto simp add: algebra_simps divide_simps intro!: mono_intros)
      using delta_nonneg[where ?'a = 'a] by auto

    text ‹We start the computation. First, use the hyperbolicity inequality.›
    have "eexp (- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x z)
       eexp (- epsilonG TYPE('a) * ((min (extended_Gromov_product_at basepoint x y) (extended_Gromov_product_at basepoint y z) - deltaG(TYPE('a)))))"
      apply (subst uminus_ereal.simps(1)[symmetric], subst ereal_mult_minus_left)+ by (intro mono_intros)
    text ‹Use distributivity to isolate the term $\epsilon \delta$. This requires some care
    as multiplication is not distributive in general in ereal.›
    also have "... = eexp (- epsilonG TYPE('a) * min (extended_Gromov_product_at basepoint x y) (extended_Gromov_product_at basepoint y z)
            + epsilonG TYPE('a) * deltaG TYPE('a))"
      apply (rule cong[of eexp], auto)
      apply (subst times_ereal.simps(1)[symmetric])
      apply (subst ereal_distrib_minus_left, auto)
      apply (subst uminus_ereal.simps(1)[symmetric])+
      apply (subst ereal_minus(6))
      by simp

    text ‹Use multiplicativity of exponential to extract the multiplicative error factor.›
    also have "... = eexp(- epsilonG TYPE('a) * (min (extended_Gromov_product_at basepoint x y) (extended_Gromov_product_at basepoint y z)))
                    * eexp(epsilonG(TYPE('a))* deltaG(TYPE('a)))"
      by (rule eexp_add_mult, auto)
    text ‹Extract the min outside of the exponential, using that all functions are monotonic.›
    also have "... = eexp(epsilonG(TYPE('a))* deltaG(TYPE('a)))
                    * (max (eexp(- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y))
                            (eexp(- epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z)))"
      apply (subst max_of_antimono[of "λ (t::ereal). -epsilonG TYPE('a) * t", symmetric])
      apply (metis antimonoI constant_in_extended_predist_pos(2) enn2ereal_ennreal enn2ereal_nonneg ereal_minus_le_minus ereal_mult_left_mono ereal_mult_minus_left uminus_ereal.simps(1))
      apply (subst max_of_mono[OF eexp_mono])
      apply (simp add: mult.commute)
      done
    text ‹We recognize the distance of $x$ to $y$ and the distance from $y$ to $z$ on the right.›
    also have "... = eexp(epsilonG(TYPE('a)) * deltaG(TYPE('a))) * (max (ereal (extended_predist x y)) (extended_predist y z))"
      unfolding extended_predist_ereal min_def using H by auto
    also have "...  esqrt 2 * max (ereal(extended_predist x y)) (ereal(extended_predist y z))"
      apply (intro mono_intros B) using extended_predist_nonneg[of x y] by (simp add: max_def)
    finally show ?thesis unfolding extended_predist_ereal min_def by auto

  next
    text ‹Next consider the case where $d(x,y)$ comes from the exponential of minus the Gromov product,
    but $d(y,z)$ comes from their extended distance. Then $d(y,z) \leq 1$ (as $d(y,z)$ is smaller
    then the exponential of minus the Gromov distance, which is at most $1$), and this is all we use:
    the Gromov product between $x$ and $y$ or $x$ and $z$ differ by at most the distance from $y$ to $z$,
    i.e., $1$. Then the result follows directly as $\exp(\epsilon) \leq \sqrt{2}$, by the choice of
    $\epsilon$.›
    assume H: "eexp (- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y)  esqrt (extended_Gromov_distance x y)"
              "esqrt (extended_Gromov_distance y z)  eexp (- epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z)"
    then have "esqrt(extended_Gromov_distance y z)  1"
      by (auto intro!: order_trans[OF H(2)] simp add: ereal_mult_le_0_iff)
    then have "extended_Gromov_distance y z  1"
      by (metis eq_iff esqrt_mono2 esqrt_simps(2) esqrt_square extended_Gromov_distance_nonneg le_cases zero_less_one_ereal)

    have "ereal(extended_predist x z)  eexp(- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x z)"
      unfolding extended_predist_ereal min_def by auto
    also have "...  eexp(- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y
                          + epsilonG TYPE('a) * extended_Gromov_distance y z)"
      apply (intro mono_intros) apply (subst uminus_ereal.simps(1)[symmetric])+ apply (subst ereal_mult_minus_left)+
      apply (intro mono_intros)
      using extended_Gromov_product_at_diff3[of basepoint x y z]
      by (meson constant_in_extended_predist_pos(2) ereal_le_distrib ereal_mult_left_mono order_trans zero_le_ereal)
    also have "...  eexp(-epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y + ereal(epsilonG TYPE('a)) * 1)"
      by (intro mono_intros, fact)
    also have "... = eexp(-epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y) * eexp(ereal(epsilonG TYPE('a)) * 1)"
      by (rule eexp_add_mult, auto)
    also have "...  eexp(-epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y) * esqrt 2"
      by (intro mono_intros A)
    also have "... = esqrt 2 * ereal(extended_predist x y)"
      unfolding extended_predist_ereal min_def using H by (auto simp add: mult.commute)
    also have "...  esqrt 2 * max (ereal(extended_predist x y)) (ereal(extended_predist y z))"
      unfolding max_def by (auto intro!: mono_intros)
    finally show ?thesis by auto

  next
    text ‹The last case is the symmetric of the previous one, and is proved similarly.›
    assume H: "eexp (- epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z)  esqrt (extended_Gromov_distance y z)"
              "esqrt (extended_Gromov_distance x y)  eexp (- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x y)"
    then have "esqrt(extended_Gromov_distance x y)  1"
      by (auto intro!: order_trans[OF H(2)] simp add: ereal_mult_le_0_iff)
    then have "extended_Gromov_distance x y  1"
      by (metis eq_iff esqrt_mono2 esqrt_simps(2) esqrt_square extended_Gromov_distance_nonneg le_cases zero_less_one_ereal)

    have "ereal(extended_predist x z)  eexp(- epsilonG TYPE('a) * extended_Gromov_product_at basepoint x z)"
      unfolding extended_predist_ereal min_def by auto
    also have "...  eexp(- epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z
                          + epsilonG TYPE('a) * extended_Gromov_distance x y)"
      apply (intro mono_intros) apply (subst uminus_ereal.simps(1)[symmetric])+ apply (subst ereal_mult_minus_left)+
      apply (intro mono_intros)
      using extended_Gromov_product_at_diff3[of basepoint z y x]
      apply (simp add: extended_Gromov_product_at_commute extended_Gromov_distance_commute)
      by (meson constant_in_extended_predist_pos(2) ereal_le_distrib ereal_mult_left_mono order_trans zero_le_ereal)
    also have "...  eexp(-epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z + ereal(epsilonG TYPE('a)) * 1)"
      by (intro mono_intros, fact)
    also have "... = eexp(-epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z) * eexp(ereal(epsilonG TYPE('a)) * 1)"
      by (rule eexp_add_mult, auto)
    also have "...  eexp(-epsilonG TYPE('a) * extended_Gromov_product_at basepoint y z) * esqrt 2"
      by (intro mono_intros A)
    also have "... = esqrt 2 * ereal(extended_predist y z)"
      unfolding extended_predist_ereal min_def using H by (auto simp add: mult.commute)
    also have "...  esqrt 2 * max (ereal(extended_predist x y)) (ereal(extended_predist y z))"
      unfolding max_def by (auto intro!: mono_intros)
    finally show ?thesis by auto
  qed
  then show "extended_predist x z  sqrt 2 * max (extended_predist x y) (extended_predist y z)"
    unfolding ereal_sqrt2[symmetric] max_of_mono[OF ereal_mono] times_ereal.simps(1) by auto
qed

instantiation Gromov_completion :: (Gromov_hyperbolic_space) metric_space
begin

definition dist_Gromov_completion::"('a::Gromov_hyperbolic_space) Gromov_completion  'a Gromov_completion  real"
  where "dist_Gromov_completion = turn_into_distance extended_predist"

text ‹To define a metric space in the current library of Isabelle/HOL, one should also introduce
a uniformity structure and a topology, as follows (they are prescribed by the distance):›

definition uniformity_Gromov_completion::"(('a Gromov_completion) × ('a Gromov_completion)) filter"
  where "uniformity_Gromov_completion = (INF e{0 <..}. principal {(x, y). dist x y < e})"

definition open_Gromov_completion :: "'a Gromov_completion set  bool"
  where "open_Gromov_completion U = (xU. eventually (λ(x', y). x' = x  y  U) uniformity)"

instance proof
  interpret Turn_into_distance extended_predist
    by (standard, auto intro: extended_predist_weak_triangle extended_predist_commute)
  fix x y z::"'a Gromov_completion"
  show "(dist x y = 0) = (x = y)"
    using TID_nonneg[of x y] lower[of x y] TID_self_zero upper[of x y] extended_predist_self0[of x y] unfolding dist_Gromov_completion_def
    by (auto, linarith)
  show "dist x y  dist x z + dist y z"
    unfolding dist_Gromov_completion_def using triangle by (simp add: TID_sym)
qed (auto simp add: uniformity_Gromov_completion_def open_Gromov_completion_def)
end

text ‹The only relevant property of the distance on the Gromov completion is that it is comparable
to the minimum of (the square root of) the extended distance, and the exponential of minus the Gromov
product. The precise formula we use to define it is just an implementation detail, in a sense.
We summarize these properties in the next theorem.
From this point on, we will only use this, and never come back to the definition based on
\verb+extended_predist+ and \verb+turn_into_distance+.›

theorem Gromov_completion_dist_comparison [mono_intros]:
  fixes x y::"('a::Gromov_hyperbolic_space) Gromov_completion"
  shows "ereal(dist x y)  esqrt(extended_Gromov_distance x y)"
        "ereal(dist x y)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)"
        "min (esqrt(extended_Gromov_distance x y)) (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y))  2 * ereal(dist x y)"
proof -
  interpret Turn_into_distance extended_predist
    by (standard, auto intro: extended_predist_weak_triangle extended_predist_commute)
  have "ereal(dist x y)  ereal(extended_predist x y)"
    unfolding dist_Gromov_completion_def by (auto intro!: upper mono_intros)
  then show "ereal(dist x y)  esqrt(extended_Gromov_distance x y)"
            "ereal(dist x y)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)"
    unfolding extended_predist_ereal by auto
  have "ereal(extended_predist x y)  ereal(2 * dist x y)"
    unfolding dist_Gromov_completion_def by (auto intro!: lower mono_intros)
  also have "... = 2 * ereal (dist x y)"
    by simp
  finally show "min (esqrt(extended_Gromov_distance x y)) (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y))  2 * ereal(dist x y)"
    unfolding extended_predist_ereal by auto
qed

lemma Gromov_completion_dist_le_1 [simp, mono_intros]:
  fixes x y::"('a::Gromov_hyperbolic_space) Gromov_completion"
  shows "dist x y  1"
proof -
  have "ereal(dist x y)  eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)"
    using Gromov_completion_dist_comparison(2)[of x y] by simp
  also have "...  eexp(-0)"
    by (intro mono_intros) (simp add: ereal_mult_le_0_iff)
  finally show ?thesis
    by auto
qed

text ‹To avoid computations with exponentials, the following lemma is very convenient. It asserts
that if $x$ is close enough to infinity, and $y$ is close enough to $x$, then the Gromov product
between $x$ and $y$ is large.›

lemma large_Gromov_product_approx:
  assumes "(M::ereal) < "
  shows "e D. e > 0  D <   (x y. dist