Theory Gromov_Boundary
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
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 = (∀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 x y ≤ e ⟶ extended_Gromov_distance x (to_Gromov_completion basepoint) ≥ D ⟶ extended_Gromov_product_at basepoint x y ≥ M)"
proof -
obtain M0::real where "M ≤ ereal M0" using assms by (cases M, auto)
define e::real where "e = exp(-epsilonG(TYPE('a)) * M0)/2"
define D::ereal where "D = ereal M0 + 4"
have "e > 0"
unfolding e_def by auto
moreover have "D < ∞"
unfolding D_def by auto
moreover have "extended_Gromov_product_at basepoint x y ≥ M0"
if "dist x y ≤ e" "extended_Gromov_distance x (to_Gromov_completion basepoint) ≥ D" for x y::"'a Gromov_completion"
proof (cases "esqrt(extended_Gromov_distance x y) ≤ eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)")
case False
then have "eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y) ≤ 2 * ereal(dist x y)"
using Gromov_completion_dist_comparison(3)[of x y] unfolding min_def by auto
also have "... ≤ exp(-epsilonG(TYPE('a)) * M0)"
using ‹dist x y ≤ e› unfolding e_def by (auto simp add: numeral_mult_ennreal)
finally have "ereal M0 ≤ extended_Gromov_product_at basepoint x y"
unfolding eexp_ereal[symmetric] apply (simp only: eexp_le_eexp_iff_le)
unfolding times_ereal.simps(1)[symmetric] uminus_ereal.simps(1)[symmetric] ereal_mult_minus_left ereal_minus_le_minus
using ereal_mult_le_mult_iff[of "ereal (epsilonG TYPE('a))"] apply auto
by (metis ‹⋀r p. ereal (r * p) = ereal r * ereal p›)
then show "M0 ≤ extended_Gromov_product_at basepoint x y"
by auto
next
case True
then have "esqrt(extended_Gromov_distance x y) ≤ 2 * ereal(dist x y)"
using Gromov_completion_dist_comparison(3)[of x y] unfolding min_def by auto
also have "... ≤ esqrt 4"
by simp
finally have *: "extended_Gromov_distance x y ≤ 4"
unfolding esqrt_le using antisym by fastforce
have "ereal M0+4 ≤ D"
unfolding D_def by auto
also have "... ≤ extended_Gromov_product_at basepoint x x"
using that by (auto simp add: extended_Gromov_distance_commute)
also have "... ≤ extended_Gromov_product_at basepoint x y + extended_Gromov_distance x y"
by (rule extended_Gromov_product_at_diff3[of basepoint x x y])
also have "... ≤ extended_Gromov_product_at basepoint x y + 4"
by (intro mono_intros *)
finally show "M0 ≤ extended_Gromov_product_at basepoint x y"
by (metis (no_types, lifting) PInfty_neq_ereal(1) add.commute add_nonneg_nonneg ereal_add_strict_mono ereal_le_distrib mult_2_ereal not_le numeral_Bit0 numeral_eq_ereal one_add_one zero_less_one_ereal)
qed
ultimately show ?thesis using order_trans[OF ‹M ≤ ereal M0›] by force
qed
text ‹On the other hand, far away from infinity, it is equivalent to control the extended Gromov
distance or the new distance on the space.›
lemma inside_Gromov_distance_approx:
assumes "C < (∞::ereal)"
shows "∃e > 0. ∀x y. extended_Gromov_distance (to_Gromov_completion basepoint) x ≤ C ⟶ dist x y ≤ e
⟶ esqrt(extended_Gromov_distance x y) ≤ 2 * ereal(dist x y)"
proof -
obtain C0 where "C ≤ ereal C0" using assms by (cases C, auto)
define e0 where "e0 = exp(-epsilonG(TYPE('a)) * C0)"
have "e0 > 0"
unfolding e0_def using assms by auto
define e where "e = e0/4"
have "e > 0"
unfolding e_def using ‹e0 > 0› by auto
moreover have "esqrt(extended_Gromov_distance x y) ≤ 2 * ereal(dist x y)"
if "extended_Gromov_distance (to_Gromov_completion basepoint) x ≤ C0" "dist x y ≤ e" for x y::"'a Gromov_completion"
proof -
have R: "min a b ≤ c ⟹ a ≤ c ∨ b ≤ c" for a b c::ereal unfolding min_def
by presburger
have "2 * ereal (dist x y) ≤ 2 * ereal e"
using that by (intro mono_intros, auto)
also have "... = ereal(e0/2)"
unfolding e_def by auto
also have "... < ereal e0"
apply (intro mono_intros) using ‹e0 > 0› by auto
also have "... ≤ eexp(-epsilonG(TYPE('a)) * extended_Gromov_distance (to_Gromov_completion basepoint) x)"
unfolding e0_def eexp_ereal[symmetric] ereal_mult_minus_left mult_minus_left uminus_ereal.simps(1)[symmetric] times_ereal.simps(1)[symmetric]
by (intro mono_intros that)
also have "... ≤ eexp(-epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint x y)"
unfolding ereal_mult_minus_left mult_minus_left uminus_ereal.simps(1)[symmetric] times_ereal.simps(1)[symmetric]
by (intro mono_intros)
finally show ?thesis
using R[OF Gromov_completion_dist_comparison(3)[of x y]] by auto
qed
ultimately show ?thesis using order_trans[OF _ ‹C ≤ ereal C0›] by auto
qed
subsection ‹Characterizing convergence in the Gromov boundary›
text ‹The convergence of sequences in the Gromov boundary can be characterized, essentially
by definition: sequences tend to a point at infinity iff the Gromov product with this point tends
to infinity, while sequences tend to a point inside iff the extended distance tends to $0$. In both
cases, it is just a matter of unfolding the definition of the distance, and see which one of the two
terms (exponential of minus the Gromov product, or extended distance) realizes the minimum. We have
constructed the distance essentially so that this property is satisfied.
We could also have defined first the topology, satisfying these conditions, but then we would have
had to check that it coincides with the topology that the distance defines, so it seems more
economical to proceed in this way.›
lemma Gromov_completion_boundary_limit:
assumes "x ∈ Gromov_boundary"
shows "(u ⤏ x) F ⟷ ((λn. extended_Gromov_product_at basepoint (u n) x) ⤏ ∞) F"
proof
assume *: "((λn. extended_Gromov_product_at basepoint (u n) x) ⤏ ∞) F"
have "((λn. ereal(dist (u n) x)) ⤏ 0) F"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "(λn. eexp (-epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x))"])
have "((λn. eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x)) ⤏ eexp (- epsilonG(TYPE('a)) * (∞::ereal))) F"
apply (intro tendsto_intros *) by auto
then show "((λn. eexp (-epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x)) ⤏ 0) F"
using constant_in_extended_predist_pos(1)[where ?'a = 'a] by auto
qed (auto simp add: Gromov_completion_dist_comparison)
then have "((λn. real_of_ereal(ereal(dist (u n) x))) ⤏ 0) F"
by (simp add: zero_ereal_def)
then show "(u ⤏ x) F"
by (subst tendsto_dist_iff, auto)
next
assume *: "(u ⤏ x) F"
have A: "1 / ereal (- epsilonG TYPE('a)) * (ereal (- epsilonG TYPE('a))) = 1"
apply auto using constant_in_extended_predist_pos(1)[where ?'a = 'a] by auto
have a: "esqrt(extended_Gromov_distance (u n) x) = ∞" for n
unfolding extended_Gromov_distance_PInf_boundary(2)[OF assms, of "u n"] by auto
have "min (esqrt(extended_Gromov_distance (u n) x)) (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x))
= eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x)" for n
unfolding a min_def using neq_top_trans by force
moreover have "((λn. min (esqrt(extended_Gromov_distance (u n) x)) (eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x))) ⤏ 0) F"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. 2 * ereal(dist (u n) x)"])
have "((λn. 2 * ereal (dist (u n) x)) ⤏ 2 * ereal 0) F"
apply (intro tendsto_intros) using * tendsto_dist_iff by auto
then show "((λn. 2 * ereal (dist (u n) x)) ⤏ 0) F" by (simp add: zero_ereal_def)
show "∀⇩F n in F. 0 ≤ min (esqrt (extended_Gromov_distance (u n) x)) (eexp (ereal (- epsilonG TYPE('a)) * extended_Gromov_product_at basepoint (u n) x))"
by (rule always_eventually, auto)
show "∀⇩F n in F.
min (esqrt (extended_Gromov_distance (u n) x)) (eexp (ereal (- epsilonG TYPE('a)) * extended_Gromov_product_at basepoint (u n) x)) ≤ 2 * ereal (dist (u n) x)"
apply (rule always_eventually) using Gromov_completion_dist_comparison(3) by auto
qed (auto)
ultimately have "((λn. eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x)) ⤏ 0) F"
by auto
then have "((λn. - epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x) ⤏ -∞) F"
unfolding eexp_special_values(3)[symmetric] eexp_tendsto' by auto
then have "((λn. 1/ereal(-epsilonG(TYPE('a))) * (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (u n) x)) ⤏ 1/ereal(-epsilonG(TYPE('a))) * (-∞)) F"
by (intro tendsto_intros, auto)
moreover have "1/ereal(-epsilonG(TYPE('a))) * (-∞) = ∞"
apply auto using constant_in_extended_predist_pos(1)[where ?'a = 'a] by auto
ultimately show "((λn. extended_Gromov_product_at basepoint (u n) x) ⤏ ∞) F"
unfolding ab_semigroup_mult_class.mult_ac(1)[symmetric] A by auto
qed
lemma extended_Gromov_product_tendsto_PInf_a_b:
assumes "((λn. extended_Gromov_product_at a (u n) (v n)) ⤏ ∞) F"
shows "((λn. extended_Gromov_product_at b (u n) (v n)) ⤏ ∞) F"
proof (rule tendsto_sandwich[of "λn. extended_Gromov_product_at a (u n) (v n) - dist a b" _ _ "λ_. ∞"])
have "extended_Gromov_product_at a (u n) (v n) - ereal (dist a b) ≤ extended_Gromov_product_at b (u n) (v n)" for n
using extended_Gromov_product_at_diff1[of a "u n" "v n" b] by (simp add: add.commute ereal_minus_le_iff)
then show "∀⇩F n in F. extended_Gromov_product_at a (u n) (v n) - ereal (dist a b) ≤ extended_Gromov_product_at b (u n) (v n)"
by auto
have "((λn. extended_Gromov_product_at a (u n) (v n) - ereal (dist a b)) ⤏ ∞ - ereal (dist a b)) F"
by (intro tendsto_intros assms) auto
then show "((λn. extended_Gromov_product_at a (u n) (v n) - ereal (dist a b)) ⤏ ∞) F"
by auto
qed (auto)
lemma Gromov_completion_inside_limit:
assumes "x ∉ Gromov_boundary"
shows "(u ⤏ x) F ⟷ ((λn. extended_Gromov_distance (u n) x) ⤏ 0) F"
proof
assume *: "((λn. extended_Gromov_distance (u n) x) ⤏ 0) F"
have "((λn. ereal(dist (u n) x)) ⤏ ereal 0) F"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. esqrt (extended_Gromov_distance (u n) x)"])
have "((λn. esqrt (extended_Gromov_distance (u n) x)) ⤏ esqrt 0) F"
by (intro tendsto_intros *)
then show "((λn. esqrt (extended_Gromov_distance (u n) x)) ⤏ ereal 0) F"
by (simp add: zero_ereal_def)
qed (auto simp add: Gromov_completion_dist_comparison zero_ereal_def)
then have "((λn. real_of_ereal(ereal(dist (u n) x))) ⤏ 0) F"
by (intro lim_real_of_ereal)
then show "(u ⤏ x) F"
by (subst tendsto_dist_iff, auto)
next
assume *: "(u ⤏ x) F"
have "x ∈ range to_Gromov_completion" using assms unfolding Gromov_boundary_def by auto
have "((λn. esqrt(extended_Gromov_distance (u n) x)) ⤏ 0) F"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. 2 * ereal(dist (u n) x)"])
have A: "extended_Gromov_distance (to_Gromov_completion basepoint) x < ∞"
by (simp add: assms extended_Gromov_distance_def)
obtain e where e: "e > 0" "⋀y. dist x y ≤ e ⟹ esqrt(extended_Gromov_distance x y) ≤ 2 * ereal (dist x y)"
using inside_Gromov_distance_approx[OF A] by auto
have B: "eventually (λn. dist x (u n) < e) F"
using order_tendstoD(2)[OF iffD1[OF tendsto_dist_iff *] ‹e > 0›] by (simp add: dist_commute)
then have "eventually (λn. esqrt(extended_Gromov_distance x (u n)) ≤ 2 * ereal (dist x (u n))) F"
using eventually_mono[OF _ e(2)] less_imp_le by (metis (mono_tags, lifting))
then show "eventually (λn. esqrt(extended_Gromov_distance (u n) x) ≤ 2 * ereal (dist (u n) x)) F"
by (simp add: dist_commute extended_Gromov_distance_commute)
have "((λn. 2 * ereal(dist (u n) x)) ⤏ 2 * ereal 0) F"
apply (intro tendsto_intros) using tendsto_dist_iff * by auto
then show "((λn. 2 * ereal(dist (u n) x)) ⤏ 0) F"
by (simp add: zero_ereal_def)
qed (auto)
then have "((λn. esqrt(extended_Gromov_distance (u n) x) * esqrt(extended_Gromov_distance (u n) x)) ⤏ 0 * 0) F"
by (intro tendsto_intros, auto)
then show "((λn. extended_Gromov_distance (u n) x) ⤏ 0) F"
by auto
qed
lemma to_Gromov_completion_lim [simp, tendsto_intros]:
"((λn. to_Gromov_completion (u n)) ⤏ to_Gromov_completion a) F ⟷ (u ⤏ a) F"
proof (subst Gromov_completion_inside_limit, auto)
assume "((λn. ereal (dist (u n) a)) ⤏ 0) F"
then have "((λn. real_of_ereal(ereal (dist (u n) a))) ⤏ 0) F"
unfolding zero_ereal_def by (rule lim_real_of_ereal)
then show "(u ⤏ a) F"
by (subst tendsto_dist_iff, auto)
next
assume "(u ⤏ a) F"
then have "((λn. dist (u n) a) ⤏ 0) F"
using tendsto_dist_iff by auto
then show "((λn. ereal (dist (u n) a)) ⤏ 0) F"
unfolding zero_ereal_def by (intro tendsto_intros)
qed
text ‹Now, we can also come back to our original definition of the completion, where points on the
boundary correspond to equivalence classes of sequences whose mutual Gromov product tends to
infinity. We show that this is compatible with our topology: the sequences that are in the equivalence
class of a point on the boundary are exactly the sequences that converge to this point. This is also
a direct consequence of the definitions, although the proof requires some unfolding (and playing
with the hyperbolicity inequality several times).›
text ‹First, we show that a sequence in the equivalence class of $x$ converges to $x$.›
lemma Gromov_completion_converge_to_boundary_aux:
assumes "x ∈ Gromov_boundary" "abs_Gromov_completion v = x" "Gromov_completion_rel v v"
shows "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x) ⇢ ∞"
proof -
have A: "eventually (λn. extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x ≥ ereal M) sequentially" for M
proof -
have "Gromov_converging_at_boundary v"
using Gromov_boundary_abs_converging assms by blast
then obtain N where N: "⋀m n. m ≥ N ⟹ n ≥ N ⟹ Gromov_product_at basepoint (v m) (v n) ≥ M + deltaG(TYPE('a))"
unfolding Gromov_converging_at_boundary_def by metis
have "extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x ≥ ereal M" if "n ≥ N" for n
unfolding extended_Gromov_product_at_def proof (rule Inf_greatest, auto)
fix wv wx assume H: "abs_Gromov_completion wv = to_Gromov_completion (v n)"
"x = abs_Gromov_completion wx"
"Gromov_completion_rel wv wv" "Gromov_completion_rel wx wx"
then have wv: "wv p = v n" for p
using Gromov_completion_rel_to_const Quotient3_Gromov_completion Quotient3_rel to_Gromov_completion_def by fastforce
have "Gromov_completion_rel v wx"
using assms H Quotient3_rel[OF Quotient3_Gromov_completion] by auto
then have *: "(λp. Gromov_product_at basepoint (v p) (wx p)) ⇢ ∞"
unfolding Gromov_completion_rel_def using Gromov_converging_at_boundary_imp_not_constant' ‹Gromov_converging_at_boundary v› by auto
have "eventually (λp. ereal(Gromov_product_at basepoint (v p) (wx p)) > M + deltaG(TYPE('a))) sequentially"
using order_tendstoD[OF *, of "ereal (M + deltaG TYPE('a))"] by auto
then obtain P where P: "⋀p. p ≥ P ⟹ ereal(Gromov_product_at basepoint (v p) (wx p)) > M + deltaG(TYPE('a))"
unfolding eventually_sequentially by auto
have *: "ereal (Gromov_product_at basepoint (v n) (wx p)) ≥ ereal M" if "p ≥ max P N" for p
proof (intro mono_intros)
have "M ≤ min (M + deltaG(TYPE('a))) (M + deltaG(TYPE('a))) - deltaG(TYPE('a))"
by auto
also have "... ≤ min (Gromov_product_at basepoint (v n) (v p)) (Gromov_product_at basepoint (v p) (wx p)) - deltaG(TYPE('a))"
apply (intro mono_intros)
using N[OF ‹n ≥ N›, of p] ‹p ≥ max P N› P[of p] ‹p ≥ max P N› by auto
also have "... ≤ Gromov_product_at basepoint (v n) (wx p) "
by (rule hyperb_ineq)
finally show "M ≤ Gromov_product_at basepoint (v n) (wx p) "
by simp
qed
then have "eventually (λp. ereal (Gromov_product_at basepoint (v n) (wx p)) ≥ ereal M) sequentially"
unfolding eventually_sequentially by metis
then show "ereal M ≤ liminf (λp. ereal (Gromov_product_at basepoint (wv p) (wx p)))"
unfolding wv by (simp add: Liminf_bounded)
qed
then show ?thesis unfolding eventually_sequentially by auto
qed
have B: "eventually (λn. extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x > M) sequentially" if "M < ∞" for M
proof -
obtain N where "ereal N > M" using ‹M < ∞› ereal_dense2 by blast
then have "a ≥ ereal N ⟹ a > M" for a by auto
then show ?thesis using A[of N] eventually_elim2 by force
qed
then show ?thesis
by (rule order_tendstoI, auto)
qed
text ‹Then, we prove the converse and therefore the equivalence.›
lemma Gromov_completion_converge_to_boundary:
assumes "x ∈ Gromov_boundary"
shows "((λn. to_Gromov_completion (u n)) ⇢ x) ⟷ (Gromov_completion_rel u u ∧ abs_Gromov_completion u = x)"
proof
assume "Gromov_completion_rel u u ∧ abs_Gromov_completion u = x"
then show "((λn. to_Gromov_completion(u n)) ⇢ x)"
using Gromov_completion_converge_to_boundary_aux[OF assms, of u] unfolding Gromov_completion_boundary_limit[OF assms] by auto
next
assume H: "(λn. to_Gromov_completion (u n)) ⇢ x"
have Lu: "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x) ⇢ ∞"
using iffD1[OF Gromov_completion_boundary_limit[OF assms] H] by simp
have A: "∃N. ∀n ≥ N. ∀ m ≥ N. Gromov_product_at basepoint (u m) (u n) ≥ M" for M
proof -
have "eventually (λn. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x > M + deltaG(TYPE('a))) sequentially"
by (rule order_tendstoD[OF Lu], auto)
then obtain N where N: "⋀n. n ≥ N ⟹ extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x > M + deltaG(TYPE('a))"
unfolding eventually_sequentially by auto
have "Gromov_product_at basepoint (u m) (u n) ≥ M" if "n ≥ N" "m ≥ N" for m n
proof -
have "ereal M ≤ min (ereal (M + deltaG(TYPE('a)))) (ereal (M + deltaG(TYPE('a)))) - ereal(deltaG(TYPE('a)))"
by simp
also have "... ≤ min (extended_Gromov_product_at basepoint (to_Gromov_completion (u m)) x) (extended_Gromov_product_at basepoint x (to_Gromov_completion (u n))) - deltaG(TYPE('a))"
apply (intro mono_intros) using N[OF ‹n ≥ N›] N[OF ‹m ≥ N›]
by (auto simp add: extended_Gromov_product_at_commute)
also have "... ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (u m)) (to_Gromov_completion (u n))"
by (rule extended_hyperb_ineq)
finally show ?thesis by auto
qed
then show ?thesis by auto
qed
have "∃N. ∀n ≥ N. ∀ m ≥ N. Gromov_product_at a (u m) (u n) ≥ M" for M a
proof -
obtain N where N: "⋀m n. m ≥ N ⟹ n ≥ N ⟹ Gromov_product_at basepoint (u m) (u n) ≥ M + dist a basepoint"
using A[of "M + dist a basepoint"] by auto
have "Gromov_product_at a (u m) (u n) ≥ M" if "m ≥ N" "n ≥ N" for m n
using N[OF that] Gromov_product_at_diff1[of a "u m" "u n" basepoint] by auto
then show ?thesis by auto
qed
then have "Gromov_converging_at_boundary u"
unfolding Gromov_converging_at_boundary_def by auto
then have "Gromov_completion_rel u u" using Gromov_converging_at_boundary_rel by auto
define v where "v = rep_Gromov_completion x"
then have "Gromov_converging_at_boundary v"
using Gromov_boundary_rep_converging[OF assms] by auto
have v: "abs_Gromov_completion v = x" "Gromov_completion_rel v v"
using Quotient3_abs_rep[OF Quotient3_Gromov_completion] Quotient3_rep_reflp[OF Quotient3_Gromov_completion]
unfolding v_def by auto
then have Lv: "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x) ⇢ ∞"
using Gromov_completion_converge_to_boundary_aux[OF assms] by auto
have *: "(λn. min (extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x) (extended_Gromov_product_at basepoint x (to_Gromov_completion (v n))) -
ereal (deltaG TYPE('a))) ⇢ min ∞ ∞ - ereal (deltaG TYPE('a))"
apply (intro tendsto_intros) using Lu Lv by (auto simp add: extended_Gromov_product_at_commute)
have "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) (to_Gromov_completion (v n))) ⇢ ∞"
apply (rule tendsto_sandwich[of "λn. min (extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x)
(extended_Gromov_product_at basepoint x (to_Gromov_completion (v n))) - deltaG(TYPE('a))" _ _ "λ_. ∞"])
using extended_hyperb_ineq not_eventuallyD apply blast using * by auto
then have "(λn. Gromov_product_at basepoint (u n) (v n)) ⇢ ∞"
by auto
then have "(λn. 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 ‹Gromov_converging_at_boundary u› ‹Gromov_converging_at_boundary v› by auto
then have "abs_Gromov_completion u = abs_Gromov_completion v"
using Quotient3_rel[OF Quotient3_Gromov_completion] v(2) ‹Gromov_completion_rel u u› by auto
then have "abs_Gromov_completion u = x"
using v(1) by auto
then show "Gromov_completion_rel u u ∧ abs_Gromov_completion u = x"
using ‹Gromov_completion_rel u u› by auto
qed
text ‹In particular, it follows that a sequence which is \verb+Gromov_converging_at_boundary+ is
indeed converging to a point on the boundary, the equivalence class of this sequence.›
lemma Gromov_converging_at_boundary_converges:
assumes "Gromov_converging_at_boundary u"
shows "∃x ∈ Gromov_boundary. (λn. to_Gromov_completion (u n)) ⇢ x"
apply (rule bexI[of _ "abs_Gromov_completion u"])
apply (subst Gromov_completion_converge_to_boundary)
using assms by (auto simp add: Gromov_converging_at_boundary_rel)
lemma Gromov_converging_at_boundary_converges':
assumes "Gromov_converging_at_boundary u"
shows "convergent (λn. to_Gromov_completion (u n))"
unfolding convergent_def using Gromov_converging_at_boundary_converges[OF assms] by auto
lemma lim_imp_Gromov_converging_at_boundary:
fixes u::"nat ⇒ 'a::Gromov_hyperbolic_space"
assumes "(λn. to_Gromov_completion (u n)) ⇢ x" "x ∈ Gromov_boundary"
shows "Gromov_converging_at_boundary u"
using Gromov_boundary_abs_converging Gromov_completion_converge_to_boundary assms by blast
text ‹If two sequences tend to the same point at infinity, then their Gromov product tends to
infinity.›
lemma same_limit_imp_Gromov_product_tendsto_infinity:
assumes "z ∈ Gromov_boundary"
"(λn. to_Gromov_completion (u n)) ⇢ z"
"(λn. to_Gromov_completion (v n)) ⇢ z"
shows "∃N. ∀n ≥ N. ∀m ≥ N. Gromov_product_at a (u n) (v m) ≥ C"
proof -
have "Gromov_completion_rel u u" "Gromov_completion_rel v v" "abs_Gromov_completion u = abs_Gromov_completion v"
using iffD1[OF Gromov_completion_converge_to_boundary[OF assms(1)]] assms by auto
then have *: "Gromov_completion_rel u v"
using Quotient3_Gromov_completion Quotient3_rel by fastforce
have **: "Gromov_converging_at_boundary u"
using assms lim_imp_Gromov_converging_at_boundary by blast
then obtain M where M: "⋀m n. m ≥ M ⟹ n ≥ M ⟹ Gromov_product_at a (u m) (u n) ≥ C + deltaG(TYPE('a))"
unfolding Gromov_converging_at_boundary_def by blast
have "(λn. Gromov_product_at a (u n) (v n)) ⇢ ∞"
using * Gromov_converging_at_boundary_imp_not_constant'[OF **] unfolding Gromov_completion_rel_def by auto
then have "eventually (λn. Gromov_product_at a (u n) (v n) ≥ C + deltaG(TYPE('a))) sequentially"
by (meson Lim_PInfty ereal_less_eq(3) eventually_sequentiallyI)
then obtain N where N: "⋀n. n ≥ N ⟹ Gromov_product_at a (u n) (v n) ≥ C + deltaG(TYPE('a))"
unfolding eventually_sequentially by auto
have "Gromov_product_at a (u n) (v m) ≥ C" if "n ≥ max M N" "m ≥ max M N" for m n
proof -
have "C + deltaG(TYPE('a)) ≤ min (Gromov_product_at a (u n) (u m)) (Gromov_product_at a (u m) (v m))"
using M N that by auto
also have "... ≤ Gromov_product_at a (u n) (v m) + deltaG(TYPE('a))"
by (intro mono_intros)
finally show ?thesis by simp
qed
then show ?thesis
by blast
qed
text ‹An admissible sequence converges in the Gromov boundary, to the point it defines. This
follows from the definition of the topology in the two cases, inner and boundary.›
lemma abs_Gromov_completion_limit:
assumes "Gromov_completion_rel u u"
shows "(λn. to_Gromov_completion (u n)) ⇢ abs_Gromov_completion u"
proof (cases "abs_Gromov_completion u")
case (to_Gromov_completion x)
then show ?thesis
using Gromov_completion_rel_to_const Quotient3_Gromov_completion Quotient3_rel assms to_Gromov_completion_def by fastforce
next
case boundary
show ?thesis
unfolding Gromov_completion_converge_to_boundary[OF boundary]
using assms Gromov_boundary_rep_converging Gromov_converging_at_boundary_rel Quotient3_Gromov_completion Quotient3_abs_rep boundary by fastforce
qed
text ‹In particular, a point in the Gromov boundary is the limit of
its representative sequence in the space.›
lemma rep_Gromov_completion_limit:
"(λn. to_Gromov_completion (rep_Gromov_completion x n)) ⇢ x"
using abs_Gromov_completion_limit[of "rep_Gromov_completion x"] Quotient3_Gromov_completion Quotient3_abs_rep Quotient3_rep_reflp by fastforce
subsection ‹Continuity properties of the extended Gromov product and distance›
text ‹We have defined our extended Gromov product in terms of sequences satisfying the equivalence
relation. However, we would like to avoid this definition as much as possible, and express things
in terms of the topology of the space. Hence, we reformulate this definition in topological terms,
first when one of the two points is inside and the other one is on the boundary, then for all
cases, and then we come back to the case where one point is inside, removing the assumption that
the other one is on the boundary.›
lemma extended_Gromov_product_inside_boundary_aux:
assumes "y ∈ Gromov_boundary"
shows "extended_Gromov_product_at e (to_Gromov_completion x) y = Inf {liminf (λn. ereal(Gromov_product_at e x (v n))) |v. (λn. to_Gromov_completion (v n)) ⇢ y}"
proof -
have A: "abs_Gromov_completion v = to_Gromov_completion x ∧ Gromov_completion_rel v v ⟷ (v = (λn. x))" for v
apply (auto simp add: to_Gromov_completion_def)
by (metis (mono_tags) Gromov_completion_rel_def Quotient3_Gromov_completion abs_Gromov_completion_in_Gromov_boundary not_in_Gromov_boundary' rep_Gromov_completion_to_Gromov_completion rep_abs_rsp to_Gromov_completion_def)
have *: "{F u v |u v. abs_Gromov_completion u = to_Gromov_completion x ∧ abs_Gromov_completion v = y ∧ Gromov_completion_rel u u ∧ Gromov_completion_rel v v}
= {F (λn. x) v |v. (λn. to_Gromov_completion (v n)) ⇢ y}" for F::"(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ ereal"
unfolding Gromov_completion_converge_to_boundary[OF ‹y ∈ Gromov_boundary›] using A by force
show ?thesis
unfolding extended_Gromov_product_at_def * by simp
qed
lemma extended_Gromov_product_boundary_inside_aux:
assumes "y ∈ Gromov_boundary"
shows "extended_Gromov_product_at e y (to_Gromov_completion x) = Inf {liminf (λn. ereal(Gromov_product_at e (v n) x)) |v. (λn. to_Gromov_completion (v n)) ⇢ y}"
using extended_Gromov_product_inside_boundary_aux[OF assms] by (simp add: extended_Gromov_product_at_commute Gromov_product_commute)
lemma extended_Gromov_product_at_topological:
"extended_Gromov_product_at e x y = Inf {liminf (λn. ereal(Gromov_product_at e (u n) (v n))) |u v. (λn. to_Gromov_completion (u n)) ⇢ x ∧ (λn. to_Gromov_completion (v n)) ⇢ y}"
proof (cases x)
case boundary
show ?thesis
proof (cases y)
case boundary
then show ?thesis
unfolding extended_Gromov_product_at_def Gromov_completion_converge_to_boundary[OF ‹x ∈ Gromov_boundary›] Gromov_completion_converge_to_boundary[OF ‹y ∈ Gromov_boundary›]
by meson
next
case (to_Gromov_completion yi)
have A: "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = liminf (λn. ereal (Gromov_product_at e (u n) yi))" if "v ⇢ yi" for u v
proof -
define h where "h = (λn. Gromov_product_at e (u n) (v n) - Gromov_product_at e (u n) yi)"
have h: "h ⇢ 0"
apply (rule tendsto_rabs_zero_cancel, rule tendsto_sandwich[of "λn. 0" _ _ "λn. dist (v n) yi"])
unfolding h_def using Gromov_product_at_diff3[of e _ _ yi] that apply auto
using tendsto_dist_iff by blast
have *: "ereal (Gromov_product_at e (u n) (v n)) = h n + ereal (Gromov_product_at e (u n) yi)" for n
unfolding h_def by auto
have "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = 0 + liminf (λn. ereal (Gromov_product_at e (u n) yi))"
unfolding * apply (rule ereal_liminf_lim_add) using h by (auto simp add: zero_ereal_def)
then show ?thesis by simp
qed
show ?thesis
unfolding to_Gromov_completion extended_Gromov_product_boundary_inside_aux[OF ‹x ∈ Gromov_boundary›] apply (rule cong[of Inf Inf], auto)
using A by fast+
qed
next
case (to_Gromov_completion xi)
show ?thesis
proof (cases y)
case boundary
have A: "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = liminf (λn. ereal (Gromov_product_at e xi (v n)))" if "u ⇢ xi" for u v
proof -
define h where "h = (λn. Gromov_product_at e (u n) (v n) - Gromov_product_at e xi (v n))"
have h: "h ⇢ 0"
apply (rule tendsto_rabs_zero_cancel, rule tendsto_sandwich[of "λn. 0" _ _ "λn. dist (u n) xi"])
unfolding h_def using Gromov_product_at_diff2[of e _ _ xi] that apply auto
using tendsto_dist_iff by blast
have *: "ereal (Gromov_product_at e (u n) (v n)) = h n + ereal (Gromov_product_at e xi (v n))" for n
unfolding h_def by auto
have "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = 0 + liminf (λn. ereal (Gromov_product_at e xi (v n)))"
unfolding * apply (rule ereal_liminf_lim_add) using h by (auto simp add: zero_ereal_def)
then show ?thesis by simp
qed
show ?thesis
unfolding to_Gromov_completion extended_Gromov_product_inside_boundary_aux[OF ‹y ∈ Gromov_boundary›] apply (rule cong[of Inf Inf], auto)
using A by fast+
next
case (to_Gromov_completion yi)
have B: "liminf (λn. Gromov_product_at e (u n) (v n)) = Gromov_product_at e xi yi" if "u ⇢ xi" "v ⇢ yi" for u v
proof -
have "(λn. Gromov_product_at e (u n) (v n)) ⇢ Gromov_product_at e xi yi"
apply (rule Gromov_product_at_continuous) using that by auto
then show "liminf (λn. Gromov_product_at e (u n) (v n)) = Gromov_product_at e xi yi"
by (simp add: lim_imp_Liminf)
qed
have *: "{liminf (λn. ereal (Gromov_product_at e (u n) (v n))) |u v. u ⇢ xi ∧ v ⇢ yi} = {ereal (Gromov_product_at e xi yi)}"
using B apply auto by (rule exI[of _ "λn. xi"], rule exI[of _ "λn. yi"], auto)
show ?thesis
unfolding ‹x = to_Gromov_completion xi› ‹y = to_Gromov_completion yi› by (auto simp add: *)
qed
qed
lemma extended_Gromov_product_inside_boundary:
"extended_Gromov_product_at e (to_Gromov_completion x) y = Inf {liminf (λn. ereal(Gromov_product_at e x (v n))) |v. (λn. to_Gromov_completion (v n)) ⇢ y}"
proof -
have A: "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = liminf (λn. ereal (Gromov_product_at e x (v n)))" if "u ⇢ x" for u v
proof -
define h where "h = (λn. Gromov_product_at e (u n) (v n) - Gromov_product_at e x (v n))"
have h: "h ⇢ 0"
apply (rule tendsto_rabs_zero_cancel, rule tendsto_sandwich[of "λn. 0" _ _ "λn. dist (u n) x"])
unfolding h_def using Gromov_product_at_diff2[of e _ _ x] that apply auto
using tendsto_dist_iff by blast
have *: "ereal (Gromov_product_at e (u n) (v n)) = h n + ereal (Gromov_product_at e x (v n))" for n
unfolding h_def by auto
have "liminf (λn. ereal (Gromov_product_at e (u n) (v n))) = 0 + liminf (λn. ereal (Gromov_product_at e x (v n)))"
unfolding * apply (rule ereal_liminf_lim_add) using h by (auto simp add: zero_ereal_def)
then show ?thesis by simp
qed
show ?thesis
unfolding extended_Gromov_product_at_topological apply (rule cong[of Inf Inf], auto)
using A by fast+
qed
lemma extended_Gromov_product_boundary_inside:
"extended_Gromov_product_at e y (to_Gromov_completion x) = Inf {liminf (λn. ereal(Gromov_product_at e (v n) x)) |v. (λn. to_Gromov_completion (v n)) ⇢ y}"
using extended_Gromov_product_inside_boundary by (simp add: extended_Gromov_product_at_commute Gromov_product_commute)
text ‹Now, we compare the extended Gromov product to a sequence of Gromov products for converging
sequences. As the extended Gromov product is defined as an Inf of limings, it is clearly smaller
than the liminf. More interestingly, it is also of the order of magnitude of the limsup, for
whatever sequence one uses. In other words, it is canonically defined, up to $2 \delta$.›
lemma extended_Gromov_product_le_liminf:
assumes "(λn. to_Gromov_completion (u n)) ⇢ xi"
"(λn. to_Gromov_completion (v n)) ⇢ eta"
shows "liminf (λn. Gromov_product_at e (u n) (v n)) ≥ extended_Gromov_product_at e xi eta"
unfolding extended_Gromov_product_at_topological using assms by (auto intro!: Inf_lower)
lemma limsup_le_extended_Gromov_product_inside:
assumes "(λn. to_Gromov_completion (v n)) ⇢ (eta::('a::Gromov_hyperbolic_space) Gromov_completion)"
shows "limsup (λn. Gromov_product_at e x (v n)) ≤ extended_Gromov_product_at e (to_Gromov_completion x) eta + deltaG(TYPE('a))"
proof (cases eta)
case boundary
have A: "limsup (λn. Gromov_product_at e x (v n)) ≤ liminf (λn. Gromov_product_at e x (v' n)) + deltaG(TYPE('a))"
if H: "(λn. to_Gromov_completion (v' n)) ⇢ eta" for v'
proof -
have "ereal a ≤ liminf (λn. Gromov_product_at e x (v' n)) + deltaG(TYPE('a))" if L: "ereal a < limsup (λn. Gromov_product_at e x (v n))" for a
proof -
obtain Nv where Nv: "⋀m n. m ≥ Nv ⟹ n ≥ Nv ⟹ Gromov_product_at e (v m) (v' n) ≥ a"
using same_limit_imp_Gromov_product_tendsto_infinity[OF ‹eta ∈ Gromov_boundary› assms H] by blast
obtain N where N: "ereal a < Gromov_product_at e x (v N)" "N ≥ Nv"
using limsup_obtain[OF L] by blast
have *: "a - deltaG(TYPE('a)) ≤ Gromov_product_at e x (v' n)" if "n ≥ Nv" for n
proof -
have "a ≤ min (Gromov_product_at e x (v N)) (Gromov_product_at e (v N) (v' n))"
apply auto using N(1) Nv[OF ‹N ≥ Nv› ‹n ≥ Nv›] by auto
also have "... ≤ Gromov_product_at e x (v' n) + deltaG(TYPE('a))"
by (intro mono_intros)
finally show ?thesis by auto
qed
have "a - deltaG(TYPE('a)) ≤ liminf (λn. Gromov_product_at e x (v' n))"
apply (rule Liminf_bounded) unfolding eventually_sequentially using * by fastforce
then show ?thesis
unfolding ereal_minus(1)[symmetric] by (subst ereal_minus_le[symmetric], auto)
qed
then show ?thesis
using ereal_dense2 not_less by blast
qed
have "limsup (λn. Gromov_product_at e x (v n)) - deltaG(TYPE('a)) ≤ extended_Gromov_product_at e (to_Gromov_completion x) eta"
unfolding extended_Gromov_product_inside_boundary by (rule Inf_greatest, auto simp add: A)
then show ?thesis by auto
next
case (to_Gromov_completion y)
then have "v ⇢ y" using assms by auto
have L: "(λn. Gromov_product_at e x (v n)) ⇢ ereal(Gromov_product_at e x y)"
using Gromov_product_at_continuous[OF _ _ ‹v ⇢ y›, of "λn. e" e "λn. x" x] by auto
show ?thesis
unfolding to_Gromov_completion using lim_imp_Limsup[OF _ L] by auto
qed
lemma limsup_le_extended_Gromov_product_inside':
assumes "(λn. to_Gromov_completion (v n)) ⇢ (eta::('a::Gromov_hyperbolic_space) Gromov_completion)"
shows "limsup (λn. Gromov_product_at e (v n) x) ≤ extended_Gromov_product_at e eta (to_Gromov_completion x) + deltaG(TYPE('a))"
using limsup_le_extended_Gromov_product_inside[OF assms] by (simp add: Gromov_product_commute extended_Gromov_product_at_commute)
lemma limsup_le_extended_Gromov_product:
assumes "(λn. to_Gromov_completion (u n)) ⇢ (xi::('a::Gromov_hyperbolic_space) Gromov_completion)"
"(λn. to_Gromov_completion (v n)) ⇢ eta"
shows "limsup (λn. Gromov_product_at e (u n) (v n)) ≤ extended_Gromov_product_at e xi eta + 2 * deltaG(TYPE('a))"
proof -
consider "xi ∈ Gromov_boundary ∧ eta ∈ Gromov_boundary" | "xi ∉ Gromov_boundary" | "eta ∉ Gromov_boundary"
by blast
then show ?thesis
proof (cases)
case 1
then have B: "xi ∈ Gromov_boundary" "eta ∈ Gromov_boundary" by auto
have A: "limsup (λn. Gromov_product_at e (u n) (v n)) ≤ liminf (λn. Gromov_product_at e (u' n) (v' n)) + 2 * deltaG(TYPE('a))"
if H: "(λn. to_Gromov_completion (u' n)) ⇢ xi" "(λn. to_Gromov_completion (v' n)) ⇢ eta" for u' v'
proof -
have "ereal a ≤ liminf (λn. Gromov_product_at e (u' n) (v' n)) + 2 * deltaG(TYPE('a))" if L: "ereal a < limsup (λn. Gromov_product_at e (u n) (v n))" for a
proof -
obtain Nu where Nu: "⋀m n. m ≥ Nu ⟹ n ≥ Nu ⟹ Gromov_product_at e (u' m) (u n) ≥ a"
using same_limit_imp_Gromov_product_tendsto_infinity[OF ‹xi ∈ Gromov_boundary› H(1) assms(1)] by blast
obtain Nv where Nv: "⋀m n. m ≥ Nv ⟹ n ≥ Nv ⟹ Gromov_product_at e (v m) (v' n) ≥ a"
using same_limit_imp_Gromov_product_tendsto_infinity[OF ‹eta ∈ Gromov_boundary› assms(2) H(2)] by blast
obtain N where N: "ereal a < Gromov_product_at e (u N) (v N)" "N ≥ max Nu Nv"
using limsup_obtain[OF L] by blast
then have "N ≥ Nu" "N ≥ Nv" by auto
have *: "a - 2 * deltaG(TYPE('a)) ≤ Gromov_product_at e (u' n) (v' n)" if "n ≥ max Nu Nv" for n
proof -
have n: "n ≥ Nu" "n ≥ Nv" using that by auto
have "a ≤ Min {Gromov_product_at e (u' n) (u N), Gromov_product_at e (u N) (v N), Gromov_product_at e (v N) (v' n)}"
apply auto using N(1) Nu[OF n(1) ‹N ≥ Nu›] Nv[OF ‹N ≥ Nv› n(2)] by auto
also have "... ≤ Gromov_product_at e (u' n) (v' n) + 2 * deltaG(TYPE('a))"
by (intro mono_intros)
finally show ?thesis by auto
qed
have "a - 2 * deltaG(TYPE('a)) ≤ liminf (λn. Gromov_product_at e (u' n) (v' n))"
apply (rule Liminf_bounded) unfolding eventually_sequentially using * by fastforce
then show ?thesis
unfolding ereal_minus(1)[symmetric] by (subst ereal_minus_le[symmetric], auto)
qed
then show ?thesis
using ereal_dense2 not_less by blast
qed
have "limsup (λn. Gromov_product_at e (u n) (v n)) - 2 * deltaG(TYPE('a)) ≤ extended_Gromov_product_at e xi eta"
unfolding extended_Gromov_product_at_topological by (rule Inf_greatest, auto simp add: A)
then show ?thesis by auto
next
case 2
then obtain x where x: "xi = to_Gromov_completion x" by (cases xi, auto)
have A: "limsup (λn. ereal (Gromov_product_at e (u n) (v n))) = limsup (λn. ereal (Gromov_product_at e x (v n)))"
proof -
define h where "h = (λn. Gromov_product_at e (u n) (v n) - Gromov_product_at e x (v n))"
have h: "h ⇢ 0"
apply (rule tendsto_rabs_zero_cancel, rule tendsto_sandwich[of "λn. 0" _ _ "λn. dist (u n) x"])
unfolding h_def using Gromov_product_at_diff2[of e _ _ x] assms(1) unfolding x apply auto
using tendsto_dist_iff by blast
have *: "ereal (Gromov_product_at e (u n) (v n)) = h n + ereal (Gromov_product_at e x (v n))" for n
unfolding h_def by auto
have "limsup (λn. ereal (Gromov_product_at e (u n) (v n))) = 0 + limsup (λn. ereal (Gromov_product_at e x (v n)))"
unfolding * apply (rule ereal_limsup_lim_add) using h by (auto simp add: zero_ereal_def)
then show ?thesis by simp
qed
have *: "ereal (deltaG TYPE('a)) ≤ ereal (2 * deltaG TYPE('a))"
by auto
show ?thesis
unfolding A x using limsup_le_extended_Gromov_product_inside[OF assms(2), of e x] *
by (meson add_left_mono order.trans)
next
case 3
then obtain y where y: "eta = to_Gromov_completion y" by (cases eta, auto)
have A: "limsup (λn. ereal (Gromov_product_at e (u n) (v n))) = limsup (λn. ereal (Gromov_product_at e (u n) y))"
proof -
define h where "h = (λn. Gromov_product_at e (u n) (v n) - Gromov_product_at e (u n) y)"
have h: "h ⇢ 0"
apply (rule tendsto_rabs_zero_cancel, rule tendsto_sandwich[of "λn. 0" _ _ "λn. dist (v n) y"])
unfolding h_def using Gromov_product_at_diff3[of e _ _ y] assms(2) unfolding y apply auto
using tendsto_dist_iff by blast
have *: "ereal (Gromov_product_at e (u n) (v n)) = h n + ereal (Gromov_product_at e (u n) y)" for n
unfolding h_def by auto
have "limsup (λn. ereal (Gromov_product_at e (u n) (v n))) = 0 + limsup (λn. ereal (Gromov_product_at e (u n) y))"
unfolding * apply (rule ereal_limsup_lim_add) using h by (auto simp add: zero_ereal_def)
then show ?thesis by simp
qed
have *: "ereal (deltaG TYPE('a)) ≤ ereal (2 * deltaG TYPE('a))"
by auto
show ?thesis
unfolding A y using limsup_le_extended_Gromov_product_inside'[OF assms(1), of e y] *
by (meson add_left_mono order.trans)
qed
qed
text ‹One can then extend to the boundary the fact that $(y,z)_x + (x,z)_y = d(x,y)$, up to a
constant $\delta$, by taking this identity inside and passing to the limit.›
lemma extended_Gromov_product_add_le:
"extended_Gromov_product_at x xi (to_Gromov_completion y) + extended_Gromov_product_at y xi (to_Gromov_completion x) ≤ dist x y"
proof -
obtain u where u: "(λn. to_Gromov_completion (u n)) ⇢ xi"
using rep_Gromov_completion_limit by blast
have "liminf (λn. ereal (Gromov_product_at a b (u n))) ≥ 0" for a b
by (rule Liminf_bounded[OF always_eventually], auto)
then have *: "liminf (λn. ereal (Gromov_product_at a b (u n))) ≠ -∞" for a b
by auto
have "extended_Gromov_product_at x xi (to_Gromov_completion y) + extended_Gromov_product_at y xi (to_Gromov_completion x)
≤ liminf (λn. ereal (Gromov_product_at x y (u n))) + liminf (λn. Gromov_product_at y x (u n))"
apply (intro mono_intros)
using extended_Gromov_product_le_liminf [OF u, of "λn. y" "to_Gromov_completion y" x]
extended_Gromov_product_le_liminf [OF u, of "λn. x" "to_Gromov_completion x" y] by (auto simp add: Gromov_product_commute)
also have "... ≤ liminf (λn. ereal (Gromov_product_at x y (u n)) + Gromov_product_at y x (u n))"
by (rule ereal_liminf_add_mono, auto simp add: *)
also have "... = dist x y"
apply (simp add: Gromov_product_add)
by (metis lim_imp_Liminf sequentially_bot tendsto_const)
finally show ?thesis by auto
qed
lemma extended_Gromov_product_add_ge:
"extended_Gromov_product_at (x::'a::Gromov_hyperbolic_space) xi (to_Gromov_completion y) + extended_Gromov_product_at y xi (to_Gromov_completion x) ≥ dist x y - deltaG(TYPE('a))"
proof -
have A: "dist x y - extended_Gromov_product_at y (to_Gromov_completion x) xi - deltaG(TYPE('a)) ≤ liminf (λn. ereal (Gromov_product_at x y (u n)))"
if "(λn. to_Gromov_completion (u n)) ⇢ xi" for u
proof -
have "dist x y = liminf (λn. ereal (Gromov_product_at x y (u n)) + Gromov_product_at y x (u n))"
apply (simp add: Gromov_product_add)
by (metis lim_imp_Liminf sequentially_bot tendsto_const)
also have "... ≤ liminf (λn. ereal (Gromov_product_at x y (u n))) + limsup (λn. Gromov_product_at y x (u n))"
by (rule ereal_liminf_limsup_add)
also have "... ≤ liminf (λn. ereal (Gromov_product_at x y (u n))) + (extended_Gromov_product_at y (to_Gromov_completion x) xi + deltaG(TYPE('a)))"
by (intro mono_intros limsup_le_extended_Gromov_product_inside[OF that])
finally show ?thesis by (auto simp add: algebra_simps)
qed
have "dist x y - extended_Gromov_product_at y (to_Gromov_completion x) xi - deltaG(TYPE('a)) ≤ extended_Gromov_product_at x (to_Gromov_completion y) xi"
unfolding extended_Gromov_product_inside_boundary[of x] apply (rule Inf_greatest) using A by auto
then show ?thesis
apply (auto simp add: algebra_simps extended_Gromov_product_at_commute)
unfolding ereal_minus(1)[symmetric] by (subst ereal_minus_le, auto simp add: algebra_simps)
qed
text ‹If one perturbs a sequence inside the space by a bounded distance, one does not change the
limit on the boundary.›
lemma Gromov_converging_at_boundary_bounded_perturbation:
assumes "(λn. to_Gromov_completion (u n)) ⇢ x"
"x ∈ Gromov_boundary"
"⋀n. dist (u n) (v n) ≤ C"
shows "(λn. to_Gromov_completion (v n)) ⇢ x"
proof -
have "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x) ⇢ ∞"
proof (rule tendsto_sandwich[of "λn. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x - C" _ _ "λn. ∞"])
show "∀⇩F n in sequentially. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x - ereal C ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x"
proof (rule always_eventually, auto)
fix n::nat
have "extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x
+ extended_Gromov_distance (to_Gromov_completion (u n)) (to_Gromov_completion (v n))"
by (intro mono_intros)
also have "... ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x + C"
using assms(3)[of n] by (intro mono_intros, auto)
finally show "extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (v n)) x + ereal C"
by auto
qed
have "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x - ereal C) ⇢ ∞ - ereal C"
apply (intro tendsto_intros)
unfolding Gromov_completion_boundary_limit[OF ‹x ∈ Gromov_boundary›, symmetric] using assms(1) by auto
then show "(λn. extended_Gromov_product_at basepoint (to_Gromov_completion (u n)) x - ereal C) ⇢ ∞"
by auto
qed (auto)
then show ?thesis
unfolding Gromov_completion_boundary_limit[OF ‹x ∈ Gromov_boundary›] by simp
qed
text ‹We prove that the extended Gromov distance is a continuous function of one variable,
by separating the different cases at infinity and inside the space. Note that it is not a
continuous function of both variables: if $u_n$ is inside the space but tends to a point $x$ in the
boundary, then the extended Gromov distance between $u_n$ and $u_n$ is $0$, but for the limit it is
$\infty$.›
lemma extended_Gromov_distance_continuous:
"continuous_on UNIV (λy. extended_Gromov_distance x y)"
proof (cases x)
text ‹First, if $x$ is in the boundary, then all distances to $x$ are infinite, and the statement
is trivial.›
case boundary
then have *: "extended_Gromov_distance x y = ∞" for y
by auto
show ?thesis
unfolding * using continuous_on_topological by blast
next
text ‹Next, consider the case where $x$ is inside the space. We split according to whether $y$ is
inside the space or at infinity.›
case (to_Gromov_completion a)
have "(λn. extended_Gromov_distance x (u n)) ⇢ extended_Gromov_distance x y" if "u ⇢ y" for u y
proof (cases y)
text ‹If $y$ is at infinity, then we know that the Gromov product of $u_n$ and $y$ tends to
infinity. Therefore, the extended distance from $u_n$ to any fixed point also tends to infinity
(as the Gromov product is bounded from below by the extended distance).›
case boundary
have *: "(λn. extended_Gromov_product_at a (u n) y) ⇢ ∞"
by (rule extended_Gromov_product_tendsto_PInf_a_b[OF iffD1[OF Gromov_completion_boundary_limit, OF boundary ‹u ⇢ y›]])
have "(λn. extended_Gromov_distance x (u n)) ⇢ ∞"
apply (rule tendsto_sandwich[of "λn. extended_Gromov_product_at a (u n) y" _ _ "λ_. ∞"])
unfolding to_Gromov_completion using extended_Gromov_product_le_dist[of a "u _" y] * by auto
then show ?thesis using boundary by auto
next
text ‹If $y$ is inside the space, then we use the triangular inequality for the extended Gromov
distance to conclure.›
case (to_Gromov_completion b)
then have F: "y ∉ Gromov_boundary" by auto
have *: "(λn. extended_Gromov_distance (u n) y) ⇢ 0"
by (rule iffD1[OF Gromov_completion_inside_limit[OF F] ‹u ⇢ y›])
show "(λn. extended_Gromov_distance x (u n)) ⇢ extended_Gromov_distance x y"
proof (rule tendsto_sandwich[of "λn. extended_Gromov_distance x y - extended_Gromov_distance (u n) y" _ _
"λn. extended_Gromov_distance x y + extended_Gromov_distance (u n) y"])
have "extended_Gromov_distance x y - extended_Gromov_distance (u n) y ≤ extended_Gromov_distance x (u n)" for n
using extended_Gromov_distance_triangle[of y x "u n"]
by (auto simp add: extended_Gromov_distance_commute F ennreal_minus_le_iff extended_Gromov_distance_def)
then show "∀⇩F n in sequentially. extended_Gromov_distance x y - extended_Gromov_distance (u n) y ≤ extended_Gromov_distance x (u n)"
by auto
have "extended_Gromov_distance x (u n) ≤ extended_Gromov_distance x y + extended_Gromov_distance (u n) y" for n
using extended_Gromov_distance_triangle[of x "u n" y] by (auto simp add: extended_Gromov_distance_commute)
then show "∀⇩F n in sequentially. extended_Gromov_distance x (u n) ≤ extended_Gromov_distance x y + extended_Gromov_distance (u n) y"
by auto
have "(λn. extended_Gromov_distance x y - extended_Gromov_distance (u n) y) ⇢ extended_Gromov_distance x y - 0"
by (intro tendsto_intros *, auto)
then show "(λn. extended_Gromov_distance x y - extended_Gromov_distance (u n) y) ⇢ extended_Gromov_distance x y"
by simp
have "(λn. extended_Gromov_distance x y + extended_Gromov_distance (u n) y) ⇢ extended_Gromov_distance x y + 0"
by (intro tendsto_intros *, auto)
then show "(λn. extended_Gromov_distance x y + extended_Gromov_distance (u n) y) ⇢ extended_Gromov_distance x y"
by simp
qed
qed
then show ?thesis
unfolding continuous_on_sequentially comp_def by auto
qed
lemma extended_Gromov_distance_continuous':
"continuous_on UNIV (λx. extended_Gromov_distance x y)"
using extended_Gromov_distance_continuous[of y] extended_Gromov_distance_commute[of _ y] by auto
subsection ‹Topology of the Gromov boundary›
text ‹We deduce the basic fact that the original space is open in the Gromov completion from the
continuity of the extended distance.›
lemma to_Gromov_completion_range_open:
"open (range to_Gromov_completion)"
proof -
have *: "range to_Gromov_completion = (λx. extended_Gromov_distance (to_Gromov_completion basepoint) x)-`{..<∞}"
using Gromov_boundary_def extended_Gromov_distance_PInf_boundary(2) by fastforce
show ?thesis
unfolding * using extended_Gromov_distance_continuous open_lessThan open_vimage by blast
qed
lemma Gromov_boundary_closed:
"closed Gromov_boundary"
unfolding Gromov_boundary_def using to_Gromov_completion_range_open by auto
text ‹The original space is also dense in its Gromov completion, as all points at infinity are
by definition limits of some sequence in the space.›
lemma to_Gromov_completion_range_dense [simp]:
"closure (range to_Gromov_completion) = UNIV"
apply (auto simp add: closure_sequential) using rep_Gromov_completion_limit by force
lemma to_Gromov_completion_homeomorphism:
"homeomorphism_on UNIV to_Gromov_completion"
by (rule homeomorphism_on_sequentially, auto)
lemma to_Gromov_completion_continuous:
"continuous_on UNIV to_Gromov_completion"
by (rule homeomorphism_on_continuous[OF to_Gromov_completion_homeomorphism])
lemma from_Gromov_completion_continuous:
"homeomorphism_on (range to_Gromov_completion) from_Gromov_completion"
"continuous_on (range to_Gromov_completion) from_Gromov_completion"
"⋀x::('a::Gromov_hyperbolic_space) Gromov_completion. x ∈ range to_Gromov_completion ⟹ continuous (at x) from_Gromov_completion"
proof -
show *: "homeomorphism_on (range to_Gromov_completion) from_Gromov_completion"
using homeomorphism_on_inverse[OF to_Gromov_completion_homeomorphism] unfolding from_Gromov_completion_def[symmetric] by simp
show "continuous_on (range to_Gromov_completion) from_Gromov_completion"
by (simp add: * homeomorphism_on_continuous)
then show "continuous (at x) from_Gromov_completion" if "x ∈ range to_Gromov_completion" for x::"'a Gromov_completion"
using continuous_on_eq_continuous_at that to_Gromov_completion_range_open by auto
qed
text ‹The Gromov boundary is always complete. Indeed, consider a Cauchy sequence $u_n$ in the
boundary, and approximate well enough $u_n$ by a point $v_n$ inside. Then the sequence $v_n$
is Gromov converging at infinity (the respective Gromov products tend to infinity essentially
by definition), and its limit point is the limit of the original sequence $u$.›
proposition Gromov_boundary_complete:
"complete Gromov_boundary"
proof (rule completeI)
fix u::"nat ⇒ 'a Gromov_completion" assume "∀n. u n ∈ Gromov_boundary" "Cauchy u"
then have u: "⋀n. u n ∈ Gromov_boundary" by auto
have *: "∃x ∈ range to_Gromov_completion. dist (u n) x < 1/real(n+1)" for n
by (rule closure_approachableD, auto simp add: to_Gromov_completion_range_dense)
have "∃v. ∀n. dist (to_Gromov_completion (v n)) (u n) < 1/real(n+1)"
using of_nat_less_top apply (intro choice) using * by (auto simp add: dist_commute)
then obtain v where v: "⋀n. dist (to_Gromov_completion (v n)) (u n) < 1/real(n+1)"
by blast
have "(λn. dist (to_Gromov_completion (v n)) (u n)) ⇢ 0"
apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. 1/real(n+1)"])
using v LIMSEQ_ignore_initial_segment[OF lim_1_over_n, of 1] unfolding eventually_sequentially
by (auto simp add: less_imp_le)
have "Gromov_converging_at_boundary v"
proof (rule Gromov_converging_at_boundaryI[of basepoint])
fix M::real
obtain D1 e1 where D1: "e1 > 0" "D1 < ∞" "⋀x y::'a Gromov_completion. dist x y ≤ e1 ⟹ extended_Gromov_distance x (to_Gromov_completion basepoint) ≥ D1 ⟹ extended_Gromov_product_at basepoint x y ≥ ereal M"
using large_Gromov_product_approx[of "ereal M"] by auto
obtain D2 e2 where D2: "e2 > 0" "D2 < ∞" "⋀x y::'a Gromov_completion. dist x y ≤ e2 ⟹ extended_Gromov_distance x (to_Gromov_completion basepoint) ≥ D2 ⟹ extended_Gromov_product_at basepoint x y ≥ D1"
using large_Gromov_product_approx[OF ‹D1 < ∞›] by auto
define e where "e = (min e1 e2)/3"
have "e > 0" unfolding e_def using ‹e1 > 0› ‹e2 > 0› by auto
then obtain N1 where N1: "⋀n m. n ≥ N1 ⟹ m ≥ N1 ⟹ dist (u n) (u m) < e"
using ‹Cauchy u› unfolding Cauchy_def by blast
have "eventually (λn. dist (to_Gromov_completion (v n)) (u n) < e) sequentially"
by (rule order_tendstoD[OF ‹(λn. dist (to_Gromov_completion (v n)) (u n)) ⇢ 0›], fact)
then obtain N2 where N2: "⋀n. n ≥ N2 ⟹ dist (to_Gromov_completion (v n)) (u n) < e"
unfolding eventually_sequentially by auto
have "ereal M ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (v m)) (to_Gromov_completion (v n))"
if "n ≥ max N1 N2" "m ≥ max N1 N2" for m n
proof (rule D1(3))
have "dist (to_Gromov_completion (v m)) (to_Gromov_completion (v n))
≤ dist (to_Gromov_completion (v m)) (u m) + dist (u m) (u n) + dist (u n) (to_Gromov_completion (v n))"
by (intro mono_intros)
also have "... ≤ e + e + e"
apply (intro mono_intros)
using N1[of m n] N2[of n] N2[of m] that by (auto simp add: dist_commute)
also have "... ≤ e1" unfolding e_def by auto
finally show "dist (to_Gromov_completion (v m)) (to_Gromov_completion (v n)) ≤ e1" by simp
have "e ≤ e2" unfolding e_def using ‹e2 > 0› by auto
have "D1 ≤ extended_Gromov_product_at basepoint (u m) (to_Gromov_completion (v m))"
apply (rule D2(3)) using N2[of m] that ‹e ≤ e2› u[of m] by (auto simp add: dist_commute)
also have "... ≤ extended_Gromov_distance (to_Gromov_completion basepoint) (to_Gromov_completion (v m))"
using extended_Gromov_product_le_dist[of basepoint "to_Gromov_completion (v m)" "u m"]
by (simp add: extended_Gromov_product_at_commute)
finally show "D1 ≤ extended_Gromov_distance (to_Gromov_completion (v m)) (to_Gromov_completion basepoint)"
by (simp add: extended_Gromov_distance_commute)
qed
then have "M ≤ Gromov_product_at basepoint (v m) (v n)" if "n ≥ max N1 N2" "m ≥ max N1 N2" for m n
using that by auto
then show "∃N. ∀n ≥ N. ∀m ≥ N. M ≤ Gromov_product_at basepoint (v m) (v n)"
by blast
qed
then obtain l where l: "l ∈ Gromov_boundary" "(λn. to_Gromov_completion (v n)) ⇢ l"
using Gromov_converging_at_boundary_converges by blast
have "(λn. dist (u n) l) ⇢ 0+0"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (u n) (to_Gromov_completion (v n)) + dist (to_Gromov_completion (v n)) l"])
show "(λn. dist (u n) (to_Gromov_completion (v n)) + dist (to_Gromov_completion (v n)) l) ⇢ 0 + 0"
apply (intro tendsto_intros)
using iffD1[OF tendsto_dist_iff l(2)] ‹(λn. dist (to_Gromov_completion (v n)) (u n)) ⇢ 0›
by (auto simp add: dist_commute)
qed (auto simp add: dist_triangle)
then have "u ⇢ l"
using iffD2[OF tendsto_dist_iff] by auto
then show "∃l∈Gromov_boundary. u ⇢ l"
using l(1) by auto
qed
text ‹When the initial space is complete, then the whole Gromov completion is also complete:
for Cauchy sequences tending to the Gromov boundary, then the convergence is proved as in the
completeness of the boundary above. For Cauchy sequences that remain bounded, the convergence
is reduced to the convergence inside the original space, which holds by assumption.›
proposition Gromov_completion_complete:
assumes "complete (UNIV::'a::Gromov_hyperbolic_space set)"
shows "complete (UNIV::'a Gromov_completion set)"
proof (rule completeI, auto)
fix u0::"nat ⇒ 'a Gromov_completion" assume "Cauchy u0"
show "∃l. u0 ⇢ l"
proof (cases "limsup (λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n)) = ∞")
case True
then obtain r where r: "strict_mono r" "(λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 (r n))) ⇢ ∞"
using limsup_subseq_lim[of "(λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n))"] unfolding comp_def
by auto
define u where "u = u0 o r"
then have "(λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u n)) ⇢ ∞"
unfolding comp_def using r(2) by simp
have "Cauchy u"
using ‹Cauchy u0› r(1) u_def by (simp add: Cauchy_subseq_Cauchy)
have *: "∃x ∈ range to_Gromov_completion. dist (u n) x < 1/real(n+1)" for n
by (rule closure_approachableD, auto)
have "∃v. ∀n. dist (to_Gromov_completion (v n)) (u n) < 1/real(n+1)"
using of_nat_less_top apply (intro choice) using * by (auto simp add: dist_commute)
then obtain v where v: "⋀n. dist (to_Gromov_completion (v n)) (u n) < 1/real(n+1)"
by blast
have "(λn. dist (to_Gromov_completion (v n)) (u n)) ⇢ 0"
apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. 1/real(n+1)"])
using v LIMSEQ_ignore_initial_segment[OF lim_1_over_n, of 1] unfolding eventually_sequentially
by (auto simp add: less_imp_le)
have "Gromov_converging_at_boundary v"
proof (rule Gromov_converging_at_boundaryI[of basepoint])
fix M::real
obtain D1 e1 where D1: "e1 > 0" "D1 < ∞" "⋀x y::'a Gromov_completion. dist x y ≤ e1 ⟹ extended_Gromov_distance x (to_Gromov_completion basepoint) ≥ D1 ⟹ extended_Gromov_product_at basepoint x y ≥ ereal M"
using large_Gromov_product_approx[of "ereal M"] by auto
obtain D2 e2 where D2: "e2 > 0" "D2 < ∞" "⋀x y::'a Gromov_completion. dist x y ≤ e2 ⟹ extended_Gromov_distance x (to_Gromov_completion basepoint) ≥ D2 ⟹ extended_Gromov_product_at basepoint x y ≥ D1"
using large_Gromov_product_approx[OF ‹D1 < ∞›] by auto
define e where "e = (min e1 e2)/3"
have "e > 0" unfolding e_def using ‹e1 > 0› ‹e2 > 0› by auto
then obtain N1 where N1: "⋀n m. n ≥ N1 ⟹ m ≥ N1 ⟹ dist (u n) (u m) < e"
using ‹Cauchy u› unfolding Cauchy_def by blast
have "eventually (λn. dist (to_Gromov_completion (v n)) (u n) < e) sequentially"
by (rule order_tendstoD[OF ‹(λn. dist (to_Gromov_completion (v n)) (u n)) ⇢ 0›], fact)
then obtain N2 where N2: "⋀n. n ≥ N2 ⟹ dist (to_Gromov_completion (v n)) (u n) < e"
unfolding eventually_sequentially by auto
have "eventually (λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u n) > D2) sequentially"
by (rule order_tendstoD[OF ‹(λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u n)) ⇢ ∞›], fact)
then obtain N3 where N3: "⋀n. n ≥ N3 ⟹ extended_Gromov_distance (to_Gromov_completion basepoint) (u n) > D2"
unfolding eventually_sequentially by auto
define N where "N = N1+N2+N3"
have N: "N ≥ N1" "N ≥ N2" "N ≥ N3" unfolding N_def by auto
have "ereal M ≤ extended_Gromov_product_at basepoint (to_Gromov_completion (v m)) (to_Gromov_completion (v n))"
if "n ≥ N" "m ≥ N" for m n
proof (rule D1(3))
have "dist (to_Gromov_completion (v m)) (to_Gromov_completion (v n))
≤ dist (to_Gromov_completion (v m)) (u m) + dist (u m) (u n) + dist (u n) (to_Gromov_completion (v n))"
by (intro mono_intros)
also have "... ≤ e + e + e"
apply (intro mono_intros)
using N1[of m n] N2[of n] N2[of m] that N by (auto simp add: dist_commute)
also have "... ≤ e1" unfolding e_def by auto
finally show "dist (to_Gromov_completion (v m)) (to_Gromov_completion (v n)) ≤ e1" by simp
have "e ≤ e2" unfolding e_def using ‹e2 > 0› by auto
have "D1 ≤ extended_Gromov_product_at basepoint (u m) (to_Gromov_completion (v m))"
apply (rule D2(3)) using N2[of m] N3[of m] that N ‹e ≤ e2›
by (auto simp add: dist_commute extended_Gromov_distance_commute)
also have "... ≤ extended_Gromov_distance (to_Gromov_completion basepoint) (to_Gromov_completion (v m))"
using extended_Gromov_product_le_dist[of basepoint "to_Gromov_completion (v m)" "u m"]
by (simp add: extended_Gromov_product_at_commute)
finally show "D1 ≤ extended_Gromov_distance (to_Gromov_completion (v m)) (to_Gromov_completion basepoint)"
by (simp add: extended_Gromov_distance_commute)
qed
then have "M ≤ Gromov_product_at basepoint (v m) (v n)" if "n ≥ N" "m ≥ N" for m n
using that by auto
then show "∃N. ∀n ≥ N. ∀m ≥ N. M ≤ Gromov_product_at basepoint (v m) (v n)"
by blast
qed
then obtain l where l: "l ∈ Gromov_boundary" "(λn. to_Gromov_completion (v n)) ⇢ l"
using Gromov_converging_at_boundary_converges by blast
have "(λn. dist (u n) l) ⇢ 0+0"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (u n) (to_Gromov_completion (v n)) + dist (to_Gromov_completion (v n)) l"])
show "(λn. dist (u n) (to_Gromov_completion (v n)) + dist (to_Gromov_completion (v n)) l) ⇢ 0 + 0"
apply (intro tendsto_intros)
using iffD1[OF tendsto_dist_iff l(2)] ‹(λn. dist (to_Gromov_completion (v n)) (u n)) ⇢ 0›
by (auto simp add: dist_commute)
qed (auto simp add: dist_triangle)
then have "u ⇢ l"
using iffD2[OF tendsto_dist_iff] by auto
then have "u0 ⇢ l"
unfolding u_def using r(1) ‹Cauchy u0› Cauchy_converges_subseq by auto
then show "∃l. u0 ⇢ l"
by auto
next
case False
define C where "C = limsup (λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n)) + 1"
have "C < ∞" unfolding C_def using False less_top by fastforce
have *: "limsup (λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n)) ≥ 0"
by (intro le_Limsup always_eventually, auto)
have "limsup (λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n)) < C"
unfolding C_def using False * ereal_add_left_cancel_less by force
then have "eventually (λn. extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n) < C) sequentially"
using Limsup_lessD by blast
then obtain N where N: "⋀n. n ≥ N ⟹ extended_Gromov_distance (to_Gromov_completion basepoint) (u0 n) < C"
unfolding eventually_sequentially by auto
define r where "r = (λn. n + N)"
have r: "strict_mono r" unfolding r_def strict_mono_def by auto
define u where "u = (u0 o r)"
have "Cauchy u"
using ‹Cauchy u0› r(1) u_def by (simp add: Cauchy_subseq_Cauchy)
have u: "extended_Gromov_distance (to_Gromov_completion basepoint) (u n) ≤ C" for n
unfolding u_def comp_def r_def using N by (auto simp add: less_imp_le)
define v where "v = (λn. from_Gromov_completion (u n))"
have uv: "u n = to_Gromov_completion (v n)" for n
unfolding v_def apply (rule to_from_Gromov_completion[symmetric]) using u[of n] ‹C < ∞› by auto
have "Cauchy v"
proof (rule metric_CauchyI)
obtain a::real where a: "a > 0" "⋀x y::'a Gromov_completion. extended_Gromov_distance (to_Gromov_completion basepoint) x ≤ C ⟹ dist x y ≤ a
⟹ esqrt(extended_Gromov_distance x y) ≤ 2 * ereal(dist x y)"
using inside_Gromov_distance_approx[OF ‹C < ∞›] by auto
fix e::real assume "e > 0"
define e2 where "e2 = min (sqrt (e/2) /2) a"
have "e2 > 0" unfolding e2_def using ‹e > 0› ‹a > 0› by auto
then obtain N where N: "⋀m n. m ≥ N ⟹ n ≥ N ⟹ dist (u m) (u n) < e2"
using ‹Cauchy u› unfolding Cauchy_def by blast
have "dist (v m) (v n) < e" if "n ≥ N" "m ≥ N" for m n
proof -
have "ereal(sqrt(dist (v m) (v n))) = esqrt(extended_Gromov_distance (u m) (u n))"
unfolding uv by (auto simp add: esqrt_ereal_ereal_sqrt)
also have "... ≤ 2 * ereal(dist (u m) (u n))"
apply (rule a(2)) using u[of m] N[OF ‹m ≥ N› ‹n ≥ N›] unfolding e2_def by auto
also have "... = ereal(2 * dist (u m) (u n))"
by simp
also have "... ≤ ereal(2 * e2)"
apply (intro mono_intros) using N[OF ‹m ≥ N› ‹n ≥ N›] less_imp_le by auto
finally have "sqrt(dist (v m) (v n)) ≤ 2 * e2"
using ‹e2 > 0› by auto
also have "... ≤ sqrt (e/2)"
unfolding e2_def by auto
finally have "dist (v m) (v n) ≤ e/2"
by auto
then show ?thesis
using ‹e > 0› by auto
qed
then show "∃M. ∀m ≥ M. ∀n ≥ M. dist (v m) (v n) < e" by auto
qed
then obtain l where "v ⇢ l"
using ‹complete (UNIV::'a set)› complete_def by blast
then have "u ⇢ (to_Gromov_completion l)"
unfolding uv by auto
then have "u0 ⇢ (to_Gromov_completion l)"
unfolding u_def using r(1) ‹Cauchy u0› Cauchy_converges_subseq by auto
then show "∃l. u0 ⇢ l"
by auto
qed
qed
instance Gromov_completion::("{Gromov_hyperbolic_space, complete_space}") complete_space
apply standard
using Gromov_completion_complete complete_def convergent_def complete_UNIV by auto
text ‹When the original space is proper, i.e., closed balls are compact, and geodesic, then the
Gromov completion (and therefore the Gromov boundary) are compact. The idea to extract a convergent
subsequence of a sequence $u_n$ in the boundary is to take the point $v_n$ at distance $T$ along
a geodesic tending to the point $u_n$ on the boundary, where $T$ is fixed and large. The points
$v_n$ live in a bounded subset of the space, hence they have a convergent subsequence $v_{j(n)}$.
It follows that $u_{j(n)}$ is almost converging, up to an error that tends to $0$ when $T$ tends
to infinity. By a diagonal argument, we obtain a convergent subsequence of $u_n$.
As we have already proved that the space is complete, there is a shortcut to the above argument,
avoiding subsequences and diagonal argument altogether. Indeed, in a complete space it suffices
to show that for any $\epsilon > 0$ it is covered by finitely many balls of radius $\epsilon$ to get
the compactness. This is what we do in the following proof, although the argument is precisely
modelled on the first proof we have explained.›
theorem Gromov_completion_compact:
assumes "proper (UNIV::'a::Gromov_hyperbolic_space_geodesic set)"
shows "compact (UNIV::'a Gromov_completion set)"
proof -
have "∃k. finite k ∧ (UNIV::'a Gromov_completion set) ⊆ (⋃x∈k. ball x e)" if "e > 0" for e
proof -
define D::real where "D = max 0 (-ln(e/4)/epsilonG(TYPE('a)))"
have "D ≥ 0" unfolding D_def by auto
have "exp(-epsilonG(TYPE('a)) * D) ≤ exp(ln (e / 4))"
unfolding D_def apply (intro mono_intros) unfolding max_def
apply auto
using constant_in_extended_predist_pos(1)[where ?'a = 'a] by (auto simp add: divide_simps)
then have "exp(-epsilonG(TYPE('a)) * D) ≤ e/4" using ‹e > 0› by auto
define e0::real where "e0 = e * e / 16"
have "e0 > 0" using ‹e > 0› unfolding e0_def by auto
obtain k::"'a set" where k: "finite k" "cball basepoint D ⊆ (⋃x∈k. ball x e0)"
using compact_eq_totally_bounded[of "cball (basepoint::'a) D"] assms ‹e0 > 0›
unfolding proper_def by auto
have A: "∃y ∈ k. dist (to_Gromov_completion y) (to_Gromov_completion x) ≤ e/4" if "dist basepoint x ≤ D" for x::'a
proof -
obtain z where z: "z ∈ k" "dist z x < e0" using ‹dist basepoint x ≤ D› k(2) by auto
have "ereal(dist (to_Gromov_completion z) (to_Gromov_completion x)) ≤ esqrt(extended_Gromov_distance (to_Gromov_completion z) (to_Gromov_completion x))"
by (intro mono_intros)
also have "... = ereal(sqrt (dist z x))"
by auto
finally have "dist (to_Gromov_completion z) (to_Gromov_completion x) ≤ sqrt (dist z x)"
by auto
also have "... ≤ sqrt e0"
using z(2) by auto
also have "... ≤ e/4"
unfolding e0_def using ‹e > 0› by (auto simp add: less_imp_le real_sqrt_divide)
finally have "dist (to_Gromov_completion z) (to_Gromov_completion x) ≤ e/4"
by auto
then show ?thesis
using ‹z ∈ k› by auto
qed
have B: "∃y ∈ k. dist (to_Gromov_completion y) (to_Gromov_completion x) ≤ e/2" for x
proof (cases "dist basepoint x ≤ D")
case True
have "e/4 ≤ e/2" using ‹e > 0› by auto
then show ?thesis using A[OF True] by force
next
case False
define x2 where "x2 = geodesic_segment_param {basepoint--x} basepoint D"
have *: "Gromov_product_at basepoint x x2 = D"
unfolding x2_def apply (rule Gromov_product_geodesic_segment) using False ‹D ≥ 0› by auto
have "ereal(dist (to_Gromov_completion x) (to_Gromov_completion x2))
≤ eexp (- epsilonG(TYPE('a)) * extended_Gromov_product_at basepoint (to_Gromov_completion x) (to_Gromov_completion x2))"
by (intro mono_intros)
also have "... = eexp (- epsilonG(TYPE('a)) * ereal D)"
using * by auto
also have "... = ereal(exp(-epsilonG(TYPE('a)) * D))"
by auto
also have "... ≤ ereal(e/4)"
by (intro mono_intros, fact)
finally have "dist (to_Gromov_completion x) (to_Gromov_completion x2) ≤ e/4"
using ‹e > 0› by auto
have "dist basepoint x2 ≤ D"
unfolding x2_def using False ‹0 ≤ D› by auto
then obtain y where "y ∈ k" "dist (to_Gromov_completion y) (to_Gromov_completion x2) ≤ e/4"
using A by auto
have "dist (to_Gromov_completion y) (to_Gromov_completion x)
≤ dist (to_Gromov_completion y) (to_Gromov_completion x2) + dist (to_Gromov_completion x) (to_Gromov_completion x2)"
by (intro mono_intros)
also have "... ≤ e/4 + e/4"
by (intro mono_intros, fact, fact)
also have "... = e/2" by simp
finally show ?thesis using ‹y ∈ k› by auto
qed
have C: "∃y ∈ k. dist (to_Gromov_completion y) x < e" for x
proof -
obtain x1 where x1: "dist x x1 < e/2" "x1 ∈ range to_Gromov_completion"
using to_Gromov_completion_range_dense ‹e > 0›
by (metis (no_types, opaque_lifting) UNIV_I closure_approachableD divide_pos_pos zero_less_numeral)
then obtain z where z: "x1 = to_Gromov_completion z" by auto
then obtain y where y: "y ∈ k" "dist (to_Gromov_completion y) (to_Gromov_completion z) ≤ e/2"
using B by auto
have "dist (to_Gromov_completion y) x ≤
dist (to_Gromov_completion y) (to_Gromov_completion z) + dist x x1"
unfolding z by (intro mono_intros)
also have "... < e/2 + e/2"
using x1(1) y(2) by auto
also have "... = e"
by auto
finally show ?thesis using ‹y ∈ k› by auto
qed
show ?thesis
apply (rule exI[of _ "to_Gromov_completion`k"])
using C ‹finite k› by auto
qed
then show ?thesis
unfolding compact_eq_totally_bounded
using Gromov_completion_complete[OF complete_of_proper[OF assms]] by auto
qed
text ‹If the inner space is second countable, so is its completion, as the former is dense in the
latter.›
instance Gromov_completion::("{Gromov_hyperbolic_space, second_countable_topology}") second_countable_topology
proof
obtain A::"'a set" where "countable A" "closure A = UNIV"
using second_countable_metric_dense_subset by auto
define Ab where "Ab = to_Gromov_completion`A"
have "range to_Gromov_completion ⊆ closure Ab"
unfolding Ab_def
by (metis ‹closure A = UNIV› closed_closure closure_subset image_closure_subset to_Gromov_completion_continuous)
then have "closure Ab = UNIV"
by (metis closed_closure closure_minimal dual_order.antisym to_Gromov_completion_range_dense top_greatest)
moreover have "countable Ab" unfolding Ab_def using ‹countable A› by auto
ultimately have "∃Ab::'a Gromov_completion set. countable Ab ∧ closure Ab = UNIV"
by auto
then show "∃B::'a Gromov_completion set set. countable B ∧ open = generate_topology B"
using second_countable_iff_dense_countable_subset topological_basis_imp_subbasis by auto
qed
text ‹The same follows readily for the Polish space property.›
instance metric_completion::("{Gromov_hyperbolic_space, polish_space}") polish_space
by standard
subsection ‹The Gromov completion of the real line.›
text ‹We show in the paragraph that the Gromov completion of the real line is obtained by adding
one point at $+\infty$ and one point at $-\infty$. In other words, it coincides with ereal.
To show this, we have to understand which sequences of reals are Gromov-converging to the
boundary. We show in the next lemma that they are exactly the sequences that converge to $-\infty$
or to $+\infty$.›
lemma real_Gromov_converging_to_boundary:
fixes u::"nat ⇒ real"
shows "Gromov_converging_at_boundary u ⟷ ((u ⇢ ∞) ∨ (u ⇢ - ∞))"
proof -
have *: "Gromov_product_at 0 m n ≥ min m n" for m n::real
unfolding Gromov_product_at_def dist_real_def by auto
have A: "Gromov_converging_at_boundary u" if "u ⇢ ∞" for u::"nat ⇒ real"
proof (rule Gromov_converging_at_boundaryI[of 0])
fix M::real
have "eventually (λn. ereal (u n) > M) sequentially"
by (rule order_tendstoD(1)[OF ‹u ⇢ ∞›, of "ereal M"], auto)
then obtain N where "⋀n. n ≥ N ⟹ ereal (u n) > M"
unfolding eventually_sequentially by auto
then have A: "u n ≥ M" if "n ≥ N" for n
by (simp add: less_imp_le that)
have "M ≤ Gromov_product_at 0 (u m) (u n)" if "n ≥ N" "m ≥ N" for m n
using A[OF ‹m ≥ N›] A[OF ‹n ≥ N›] *[of "u m" "u n"] by auto
then show "∃N. ∀n ≥ N. ∀m ≥ N. M ≤ Gromov_product_at 0 (u m) (u n)"
by auto
qed
have *: "Gromov_product_at 0 m n ≥ - max m n" for m n::real
unfolding Gromov_product_at_def dist_real_def by auto
have B: "Gromov_converging_at_boundary u" if "u ⇢ -∞" for u::"nat ⇒ real"
proof (rule Gromov_converging_at_boundaryI[of 0])
fix M::real
have "eventually (λn. ereal (u n) < - M) sequentially"
by (rule order_tendstoD(2)[OF ‹u ⇢ -∞›, of "ereal (-M)"], auto)
then obtain N where "⋀n. n ≥ N ⟹ ereal (u n) < - M"
unfolding eventually_sequentially by auto
then have A: "u n ≤ - M" if "n ≥ N" for n
by (simp add: less_imp_le that)
have "M ≤ Gromov_product_at 0 (u m) (u n)" if "n ≥ N" "m ≥ N" for m n
using A[OF ‹m ≥ N›] A[OF ‹n ≥ N›] *[of "u m" "u n"] by auto
then show "∃N. ∀n ≥ N. ∀m ≥ N. M ≤ Gromov_product_at 0 (u m) (u n)"
by auto
qed
have L: "(u ⇢ ∞) ∨ (u ⇢ - ∞)" if "Gromov_converging_at_boundary u" for u::"nat ⇒ real"
proof -
have "(λn. abs(u n)) ⇢ ∞"
using Gromov_converging_at_boundary_imp_unbounded[OF that, of 0] unfolding dist_real_def by auto
obtain r where r: "strict_mono r" "(λn. ereal (u (r n))) ⇢ liminf (λn. ereal(u n))"
using liminf_subseq_lim[of "λn. ereal(u n)"] unfolding comp_def by auto
have "(λn. abs(ereal (u (r n)))) ⇢ abs(liminf (λn. ereal(u n)))"
apply (intro tendsto_intros) using r(2) by auto
moreover have "(λn. abs(ereal (u (r n)))) ⇢ ∞"
using ‹(λn. abs(u n)) ⇢ ∞› apply auto
using filterlim_compose filterlim_subseq[OF r(1)] by blast
ultimately have A: "abs(liminf (λn. ereal(u n))) = ∞"
using LIMSEQ_unique by auto
obtain r where r: "strict_mono r" "(λn. ereal (u (r n))) ⇢ limsup (λn. ereal(u n))"
using limsup_subseq_lim[of "λn. ereal(u n)"] unfolding comp_def by auto
have "(λn. abs(ereal (u (r n)))) ⇢ abs(limsup (λn. ereal(u n)))"
apply (intro tendsto_intros) using r(2) by auto
moreover have "(λn. abs(ereal (u (r n)))) ⇢ ∞"
using ‹(λn. abs(u n)) ⇢ ∞› apply auto
using filterlim_compose filterlim_subseq[OF r(1)] by blast
ultimately have B: "abs(limsup (λn. ereal(u n))) = ∞"
using LIMSEQ_unique by auto
have "¬(liminf u = - ∞ ∧ limsup u = ∞)"
proof (rule ccontr, auto)
assume "liminf u = -∞" "limsup u = ∞"
have "∃N. ∀n ≥ N. ∀m ≥ N. Gromov_product_at 0 (u m) (u n) ≥ 1"
using that unfolding Gromov_converging_at_boundary_def by blast
then obtain N where N: "⋀m n. m ≥ N ⟹ n ≥ N ⟹ Gromov_product_at 0 (u m) (u n) ≥ 1"
by auto
have "∃n ≥ N. ereal(u n) > ereal 0"
apply (rule limsup_obtain) unfolding ‹limsup u = ∞› by auto
then obtain n where n: "n ≥ N" "u n > 0" by auto
have "∃n ≥ N. ereal(u n) < ereal 0"
apply (rule liminf_obtain) unfolding ‹liminf u = -∞› by auto
then obtain m where m: "m ≥ N" "u m < 0" by auto
have "Gromov_product_at 0 (u m) (u n) = 0"
unfolding Gromov_product_at_def dist_real_def using m n by auto
then show False using N[OF m(1) n(1)] by auto
qed
then have "liminf u = ∞ ∨ limsup u = - ∞"
using A B by auto
then show ?thesis
by (simp add: Liminf_PInfty Limsup_MInfty)
qed
show ?thesis using L A B by auto
qed
text ‹There is one single point at infinity in the Gromov completion of reals, i.e., two
sequences tending to infinity are equivalent.›
lemma real_Gromov_completion_rel_PInf:
fixes u v::"nat ⇒ real"
assumes "u ⇢ ∞" "v ⇢ ∞"
shows "Gromov_completion_rel u v"
proof -
have *: "Gromov_product_at 0 m n ≥ min m n" for m n::real
unfolding Gromov_product_at_def dist_real_def by auto
have **: "Gromov_product_at a m n ≥ min m n - abs a" for m n a::real
using Gromov_product_at_diff1[of 0 m n a] *[of m n] by auto
have "(λn. Gromov_product_at a (u n) (v n)) ⇢ ∞" for a
proof (rule tendsto_sandwich[of "λn. min (u n) (v n) - abs a" _ _ "λn. ∞"])
have "ereal (min (u n) (v n) - ¦a¦) ≤ ereal (Gromov_product_at a (u n) (v n))" for n
using **[of "u n" "v n" a] by auto
then show "∀⇩F n in sequentially. ereal (min (u n) (v n) - ¦a¦) ≤ ereal (Gromov_product_at a (u n) (v n))"
by auto
have "(λx. min (ereal(u x)) (ereal (v x)) - ereal ¦a¦) ⇢ min ∞ ∞ - ereal ¦a¦"
apply (intro tendsto_intros) using assms by auto
then show "(λx. ereal (min (u x) (v x) - ¦a¦)) ⇢ ∞"
apply auto unfolding ereal_minus(1)[symmetric] by auto
qed (auto)
moreover have "Gromov_converging_at_boundary u" "Gromov_converging_at_boundary v"
using real_Gromov_converging_to_boundary assms by auto
ultimately show ?thesis unfolding Gromov_completion_rel_def by auto
qed
text ‹There is one single point at minus infinity in the Gromov completion of reals, i.e., two
sequences tending to minus infinity are equivalent.›
lemma real_Gromov_completion_rel_MInf:
fixes u v::"nat ⇒ real"
assumes "u ⇢ -∞" "v ⇢ -∞"
shows "Gromov_completion_rel u v"
proof -
have *: "Gromov_product_at 0 m n ≥ - max m n" for m n::real
unfolding Gromov_product_at_def dist_real_def by auto
have **: "Gromov_product_at a m n ≥ - max m n - abs a" for m n a::real
using Gromov_product_at_diff1[of 0 m n a] *[of m n] by auto
have "(λn. Gromov_product_at a (u n) (v n)) ⇢ ∞" for a
proof (rule tendsto_sandwich[of "λn. min (-u n) (-v n) - abs a" _ _ "λn. ∞"])
have "ereal (min (-u n) (-v n) - ¦a¦) ≤ ereal (Gromov_product_at a (u n) (v n))" for n
using **[of "u n" "v n" a] by auto
then show "∀⇩F n in sequentially. ereal (min (-u n) (-v n) - ¦a¦) ≤ ereal (Gromov_product_at a (u n) (v n))"
by auto
have "(λx. min (-ereal(u x)) (-ereal (v x)) - ereal ¦a¦) ⇢ min (-(-∞)) (-(-∞)) - ereal ¦a¦"
apply (intro tendsto_intros) using assms by auto
then show "(λx. ereal (min (-u x) (-v x) - ¦a¦)) ⇢ ∞"
apply auto unfolding ereal_minus(1)[symmetric] by auto
qed (auto)
moreover have "Gromov_converging_at_boundary u" "Gromov_converging_at_boundary v"
using real_Gromov_converging_to_boundary assms by auto
ultimately show ?thesis unfolding Gromov_completion_rel_def by auto
qed
text ‹It follows from the two lemmas above that the Gromov completion of reals is obtained by
adding one single point at infinity and one single point at minus infinity. Hence, it is in
bijection with the extended reals.›
function to_real_Gromov_completion::"ereal ⇒ real Gromov_completion"
where "to_real_Gromov_completion (ereal r) = to_Gromov_completion r"
| "to_real_Gromov_completion (∞) = abs_Gromov_completion (λn. n)"
| "to_real_Gromov_completion (-∞) = abs_Gromov_completion (λn. -n)"
by (auto intro: ereal_cases)
termination by standard (rule wf_empty)
text ‹To prove the bijectivity, we prove by hand injectivity and surjectivity using the above
lemmas.›
lemma bij_to_real_Gromov_completion:
"bij to_real_Gromov_completion"
proof -
have [simp]: "Gromov_completion_rel (λn. n) (λn. n)"
by (intro real_Gromov_completion_rel_PInf tendsto_intros)
have [simp]: "Gromov_completion_rel (λn. -real n) (λn. -real n)"
by (intro real_Gromov_completion_rel_MInf tendsto_intros)
have "∃x. to_real_Gromov_completion x = y" for y
proof (cases y)
case (to_Gromov_completion x)
then have "y = to_real_Gromov_completion x" by auto
then show ?thesis by blast
next
case boundary
define u where u: "u = rep_Gromov_completion y"
have y: "abs_Gromov_completion u = y" "Gromov_completion_rel u u"
unfolding u using Quotient3_abs_rep[OF Quotient3_Gromov_completion]
Quotient3_rep_reflp[OF Quotient3_Gromov_completion] by auto
have "Gromov_converging_at_boundary u"
using u boundary by (simp add: Gromov_boundary_rep_converging)
then have "(u ⇢ ∞) ∨ (u ⇢ - ∞)" using real_Gromov_converging_to_boundary by auto
then show ?thesis
proof
assume "u ⇢ ∞"
have "abs_Gromov_completion (λn. n) = abs_Gromov_completion u "
apply (rule Quotient3_rel_abs[OF Quotient3_Gromov_completion])
by (intro real_Gromov_completion_rel_PInf[OF _ ‹u ⇢ ∞›] tendsto_intros)
then have "to_real_Gromov_completion ∞ = y"
unfolding y by auto
then show ?thesis by blast
next
assume "u ⇢ -∞"
have "abs_Gromov_completion (λn. -real n) = abs_Gromov_completion u "
apply (rule Quotient3_rel_abs[OF Quotient3_Gromov_completion])
by (intro real_Gromov_completion_rel_MInf[OF _ ‹u ⇢ -∞›] tendsto_intros)
then have "to_real_Gromov_completion (-∞) = y"
unfolding y by auto
then show ?thesis by blast
qed
qed
then have "surj to_real_Gromov_completion"
unfolding surj_def by metis
have "to_real_Gromov_completion ∞ ∈ Gromov_boundary"
"to_real_Gromov_completion (-∞) ∈ Gromov_boundary"
by (auto intro!: abs_Gromov_completion_in_Gromov_boundary tendsto_intros simp add: real_Gromov_converging_to_boundary)
moreover have "to_real_Gromov_completion ∞ ≠ to_real_Gromov_completion (-∞)"
proof -
have "Gromov_product_at 0 (real n) (-real n) = 0" for n::nat
unfolding Gromov_product_at_def dist_real_def by auto
then have *: "(λn. ereal(Gromov_product_at 0 (real n) (-real n))) ⇢ ereal 0" by auto
have "¬((λn. Gromov_product_at 0 (real n) (-real n)) ⇢ ∞)"
using LIMSEQ_unique[OF *] by fastforce
then have "¬(Gromov_completion_rel (λn. n) (λn. -n))"
unfolding Gromov_completion_rel_def by auto (metis nat.simps(3) of_nat_0 of_nat_eq_0_iff)
then show ?thesis
using Quotient3_rel[OF Quotient3_Gromov_completion, of "λn. n" "λn. -real n"] by auto
qed
ultimately have "x = y" if "to_real_Gromov_completion x = to_real_Gromov_completion y" for x y
using that injD[OF to_Gromov_completion_inj] apply (cases x y rule: ereal2_cases)
by (auto) (metis not_in_Gromov_boundary')+
then have "inj to_real_Gromov_completion"
unfolding inj_def by auto
then show "bij to_real_Gromov_completion"
using ‹surj to_real_Gromov_completion› by (simp add: bijI)
qed
text ‹Next, we prove that we have a homeomorphism. By compactness of ereals, it suffices to show
that the inclusion map is continuous everywhere. It would be a pain to distinguish all the time if points are
at infinity or not, we rather use a criterion saying that it suffices to prove sequential
continuity for sequences taking values in a dense subset of the space, here we take the reals.
Hence, it suffices to show that if a sequence of reals $v_n$ converges to a limit $a$ in the
extended reals, then the image of $v_n$ in the Gromov completion (which is an inner point) converges
to the point corresponding to $a$. We treat separately the cases $a\in \mathbb{R}$, $a = \infty$ and
$a = -\infty$. In the first case, everything is trivial. In the other cases, we have characterized
in general sequences inside the space that converge to a boundary point, as sequences in the equivalence
class defining this boundary point. Since we have described explicitly these equivalence classes in
the case of the Gromov completion of the reals (they are respectively the sequences tending to
$\infty$ and to $-\infty$), the result follows readily without any additional computation.›
proposition homeo_to_real_Gromov_completion:
"homeomorphism_on UNIV to_real_Gromov_completion"
proof (rule homeomorphism_on_compact)
show "inj to_real_Gromov_completion"
using bij_to_real_Gromov_completion by (simp add: bij_betw_def)
show "compact (UNIV::ereal set)"
by (simp add: compact_UNIV)
show "continuous_on UNIV to_real_Gromov_completion"
proof (rule continuous_on_extension_sequentially[of _ "{-∞<..<∞}"], auto)
fix u::"nat ⇒ ereal" and b::ereal assume u: "∀n. u n ≠ - ∞ ∧ u n ≠ ∞" "u ⇢ b"
define v where "v = (λn. real_of_ereal (u n))"
have uv: "u n = ereal (v n)" for n
using u unfolding v_def by (simp add: ereal_infinity_cases ereal_real)
show "(λn. to_real_Gromov_completion (u n)) ⇢ to_real_Gromov_completion b"
proof (cases b)
case (real r)
then show ?thesis using ‹u ⇢ b› unfolding uv by auto
next
case PInf
then have *: "(λn. ereal (v n)) ⇢ ∞" using ‹u ⇢ b› unfolding uv by auto
have A: "Gromov_completion_rel real v" "Gromov_completion_rel real real" "Gromov_completion_rel v v"
by (auto intro!: real_Gromov_completion_rel_PInf * tendsto_intros)
then have B: "abs_Gromov_completion v = abs_Gromov_completion real"
using Quotient3_rel_abs[OF Quotient3_Gromov_completion] by force
then show ?thesis using ‹u ⇢ b› PInf
unfolding uv apply auto
apply (subst Gromov_completion_converge_to_boundary)
using id_nat_ereal_tendsto_PInf real_Gromov_converging_to_boundary A B by auto
next
case MInf
then have *: "(λn. ereal (v n)) ⇢ -∞" using ‹u ⇢ b› unfolding uv by auto
have A: "Gromov_completion_rel (λn. -real n) v" "Gromov_completion_rel (λn. -real n) (λn. -real n)" "Gromov_completion_rel v v"
by (auto intro!: real_Gromov_completion_rel_MInf * tendsto_intros)
then have B: "abs_Gromov_completion v = abs_Gromov_completion (λn. -real n)"
using Quotient3_rel_abs[OF Quotient3_Gromov_completion] by force
then show ?thesis using ‹u ⇢ b› MInf
unfolding uv apply auto
apply (subst Gromov_completion_converge_to_boundary)
using id_nat_ereal_tendsto_PInf real_Gromov_converging_to_boundary A B
by (auto simp add: ereal_minus_real_tendsto_MInf)
qed
qed
qed
end