# Theory Gromov_Boundary

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

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

"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

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}"
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)"
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)"
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]
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
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]
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
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
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›

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

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)"
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)))"
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])
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)"
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]
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)"
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 = (∀x∈U. 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