[STATEMENT]
lemma Gromov_hyperbolic_invariant_under_quasi_isometry_explicit:
  fixes f::"'a::geodesic_space \<Rightarrow> 'b::Gromov_hyperbolic_space_geodesic"
  assumes "lambda C-quasi_isometry f"
  shows "Gromov_hyperbolic_subset (752 * lambda^3 * (C + deltaG(TYPE('b)))) (UNIV::('a set))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
have C: "lambda \<ge> 1" "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
using quasi_isometry_onD[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; ?y \<in> UNIV\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> UNIV; ?y \<in> UNIV\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
text \<open>The Morse lemma gives a control bounded by $K$ below. Following the proof, we deduce
  a bound on the thinness of triangles by an ugly constant $L$. We bound it by a more tractable
  (albeit still ugly) constant $M$.\<close>
[PROOF STATE]
proof (state)
this:
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
define K where "K = 92 * lambda^2 * (C + deltaG(TYPE('b)))"
[PROOF STATE]
proof (state)
this:
K = 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
have HD: "hausdorff_distance (f`G) {f a--f b} \<le> K" if "geodesic_segment_between G a b" for G a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f a--f b} \<le> K
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f a--f b} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
by (rule geodesic_quasi_isometric_image[OF assms that])
[PROOF STATE]
proof (state)
this:
geodesic_segment_between ?G ?a ?b \<Longrightarrow> hausdorff_distance (f ` ?G) {f ?a--f ?b} \<le> K

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
define L where "L = lambda * (4 * 1 * deltaG(TYPE('b)) + 1 * 1 * C + 2 * K)"
[PROOF STATE]
proof (state)
this:
L = lambda * (4 * 1 * deltaG TYPE('b) + 1 * 1 * C + 2 * K)

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
define M where "M = 188 * lambda^3 * (C + deltaG(TYPE('b)))"
[PROOF STATE]
proof (state)
this:
M = 188 * lambda ^ 3 * (C + deltaG TYPE('b))

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
have "L \<le> lambda * (4 * lambda^2 * deltaG(TYPE('b)) + 4 * lambda^2 * C + 2 * K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<le> lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * K)
[PROOF STEP]
unfolding L_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (4 * 1 * deltaG TYPE('b) + 1 * 1 * C + 2 * K) \<le> lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * K)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. 1 \<le> lambda\<^sup>2
 2. 0 \<le> 4
 3. 1 \<le> 4
 4. 1 \<le> lambda\<^sup>2
 5. 0 \<le> 4
 6. 0 \<le> 1
 7. 0 \<le> C
 8. 0 \<le> lambda
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C

goal (8 subgoals):
 1. 1 \<le> lambda\<^sup>2
 2. 0 \<le> 4
 3. 1 \<le> 4
 4. 1 \<le> lambda\<^sup>2
 5. 0 \<le> 4
 6. 0 \<le> 1
 7. 0 \<le> C
 8. 0 \<le> lambda
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<le> lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * K)

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
L \<le> lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * K)

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
have "... = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * K) = M
[PROOF STEP]
unfolding M_def K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * (92 * lambda\<^sup>2 * (C + deltaG TYPE('b)))) = 188 * lambda ^ 3 * (C + deltaG TYPE('b))
[PROOF STEP]
by (auto simp add: algebra_simps power2_eq_square power3_eq_cube)
[PROOF STATE]
proof (state)
this:
lambda * (4 * lambda\<^sup>2 * deltaG TYPE('b) + 4 * lambda\<^sup>2 * C + 2 * K) = M

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
L \<le> M
[PROOF STEP]
have "L \<le> M"
[PROOF STATE]
proof (prove)
using this:
L \<le> M

goal (1 subgoal):
 1. L \<le> M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
L \<le> M

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
text \<open>After these preliminaries, we start the real argument per se, showing that triangles
  are thin in the type b.\<close>
[PROOF STATE]
proof (state)
this:
L \<le> M

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
have Thin: "infdist w (Gxz \<union> Gyz) \<le> M" if
    H: "geodesic_segment_between Gxy x y" "geodesic_segment_between Gxz x z" "geodesic_segment_between Gyz y z" "w \<in> Gxy"
    for w x y z::'a and Gxy Gyz Gxz
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
obtain w2 where w2: "w2 \<in> {f x--f y}" "infdist (f w) {f x--f y} = dist (f w) w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w2. \<lbrakk>w2 \<in> {f x--f y}; infdist (f w) {f x--f y} = dist (f w) w2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infdist_proper_attained[OF proper_of_compact, of "{f x--f y}" "f w"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>compact {f x--f y}; {f x--f y} \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>c\<in>{f x--f y}. infdist (f w) {f x--f y} = dist (f w) c

goal (1 subgoal):
 1. (\<And>w2. \<lbrakk>w2 \<in> {f x--f y}; infdist (f w) {f x--f y} = dist (f w) w2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w2 \<in> {f x--f y}
infdist (f w) {f x--f y} = dist (f w) w2

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "dist (f w) w2 = infdist (f w) {f x-- f y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f w) w2 = infdist (f w) {f x--f y}
[PROOF STEP]
using w2
[PROOF STATE]
proof (prove)
using this:
w2 \<in> {f x--f y}
infdist (f w) {f x--f y} = dist (f w) w2

goal (1 subgoal):
 1. dist (f w) w2 = infdist (f w) {f x--f y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f w) w2 = infdist (f w) {f x--f y}

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f w) w2 = infdist (f w) {f x--f y}

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "... \<le> hausdorff_distance (f`Gxy) {f x-- f y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f w) {f x--f y} \<le> hausdorff_distance (f ` Gxy) {f x--f y}
[PROOF STEP]
using geodesic_segment_topology(4)[OF geodesic_segmentI] H
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between ?G ?x1 ?y1 \<Longrightarrow> bounded ?G
geodesic_segment_between Gxy x y
geodesic_segment_between Gxz x z
geodesic_segment_between Gyz y z
w \<in> Gxy

goal (1 subgoal):
 1. infdist (f w) {f x--f y} \<le> hausdorff_distance (f ` Gxy) {f x--f y}
[PROOF STEP]
by (auto intro!: quasi_isometry_on_bounded[OF quasi_isometry_on_subset[OF assms]] infdist_le_hausdorff_distance)
[PROOF STATE]
proof (state)
this:
infdist (f w) {f x--f y} \<le> hausdorff_distance (f ` Gxy) {f x--f y}

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infdist (f w) {f x--f y} \<le> hausdorff_distance (f ` Gxy) {f x--f y}

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "... \<le> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` Gxy) {f x--f y} \<le> K
[PROOF STEP]
using HD[OF H(1)]
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` Gxy) {f x--f y} \<le> K

goal (1 subgoal):
 1. hausdorff_distance (f ` Gxy) {f x--f y} \<le> K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` Gxy) {f x--f y} \<le> K

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f w) w2 \<le> K
[PROOF STEP]
have *: "dist (f w) w2 \<le> K"
[PROOF STATE]
proof (prove)
using this:
dist (f w) w2 \<le> K

goal (1 subgoal):
 1. dist (f w) w2 \<le> K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f w) w2 \<le> K

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "infdist w2 (f`Gxz \<union> f`Gyz) \<le> infdist w2 ({f x--f z} \<union> {f y--f z})
                + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f`Gxz \<union> f`Gyz)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 ({f x--f z} \<union> {f y--f z}) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz)
[PROOF STEP]
apply (rule hausdorff_distance_infdist_triangle)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {f x--f z} \<union> {f y--f z} \<noteq> {}
 2. bounded ({f x--f z} \<union> {f y--f z})
 3. bounded (f ` Gxz \<union> f ` Gyz)
[PROOF STEP]
using geodesic_segment_topology(4)[OF geodesic_segmentI] H
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between ?G ?x1 ?y1 \<Longrightarrow> bounded ?G
geodesic_segment_between Gxy x y
geodesic_segment_between Gxz x z
geodesic_segment_between Gyz y z
w \<in> Gxy

goal (3 subgoals):
 1. {f x--f z} \<union> {f y--f z} \<noteq> {}
 2. bounded ({f x--f z} \<union> {f y--f z})
 3. bounded (f ` Gxz \<union> f ` Gyz)
[PROOF STEP]
by (auto intro!: quasi_isometry_on_bounded[OF quasi_isometry_on_subset[OF assms]])
[PROOF STATE]
proof (state)
this:
infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 ({f x--f z} \<union> {f y--f z}) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz)

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 ({f x--f z} \<union> {f y--f z}) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz)

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "... \<le> 4 * deltaG(TYPE('b)) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f`Gxz \<union> f`Gyz)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w2 ({f x--f z} \<union> {f y--f z}) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz)
[PROOF STEP]
apply (simp, rule thin_triangles[of "{f x--f z}" "f z" "f x" "{f y--f z}" "f y" "{f x--f y}" w2])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. geodesic_segment_between {f x--f z} (f z) (f x)
 2. geodesic_segment_between {f y--f z} (f z) (f y)
 3. geodesic_segment_between {f x--f y} (f x) (f y)
 4. w2 \<in> {f x--f y}
[PROOF STEP]
using w2
[PROOF STATE]
proof (prove)
using this:
w2 \<in> {f x--f y}
infdist (f w) {f x--f y} = dist (f w) w2

goal (4 subgoals):
 1. geodesic_segment_between {f x--f z} (f z) (f x)
 2. geodesic_segment_between {f y--f z} (f z) (f y)
 3. geodesic_segment_between {f x--f y} (f x) (f y)
 4. w2 \<in> {f x--f y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w2 \<in> {f x--f y}; infdist (f w) {f x--f y} = dist (f w) w2\<rbrakk> \<Longrightarrow> geodesic_segment_between {f x--f z} (f z) (f x)
 2. \<lbrakk>w2 \<in> {f x--f y}; infdist (f w) {f x--f y} = dist (f w) w2\<rbrakk> \<Longrightarrow> geodesic_segment_between {f y--f z} (f z) (f y)
[PROOF STEP]
using geodesic_segment_commute some_geodesic_is_geodesic_segment(1)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between ?G ?x ?y \<Longrightarrow> geodesic_segment_between ?G ?y ?x
geodesic_segment_between {?x--?y} ?x ?y

goal (2 subgoals):
 1. \<lbrakk>w2 \<in> {f x--f y}; infdist (f w) {f x--f y} = dist (f w) w2\<rbrakk> \<Longrightarrow> geodesic_segment_between {f x--f z} (f z) (f x)
 2. \<lbrakk>w2 \<in> {f x--f y}; infdist (f w) {f x--f y} = dist (f w) w2\<rbrakk> \<Longrightarrow> geodesic_segment_between {f y--f z} (f z) (f y)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
infdist w2 ({f x--f z} \<union> {f y--f z}) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz)

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infdist w2 ({f x--f z} \<union> {f y--f z}) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz)

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "... \<le> 4 * deltaG(TYPE('b)) + max (hausdorff_distance {f x--f z} (f`Gxz)) (hausdorff_distance {f y--f z} (f`Gyz))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * deltaG TYPE('b) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + max (hausdorff_distance {f x--f z} (f ` Gxz)) (hausdorff_distance {f y--f z} (f ` Gyz))
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {f x--f z} \<noteq> {}
 2. {f y--f z} \<noteq> {}
 3. f ` Gxz \<noteq> {}
 4. f ` Gyz \<noteq> {}
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between Gxy x y
geodesic_segment_between Gxz x z
geodesic_segment_between Gyz y z
w \<in> Gxy

goal (4 subgoals):
 1. {f x--f z} \<noteq> {}
 2. {f y--f z} \<noteq> {}
 3. f ` Gxz \<noteq> {}
 4. f ` Gyz \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 * deltaG TYPE('b) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + max (hausdorff_distance {f x--f z} (f ` Gxz)) (hausdorff_distance {f y--f z} (f ` Gyz))

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
4 * deltaG TYPE('b) + hausdorff_distance ({f x--f z} \<union> {f y--f z}) (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + max (hausdorff_distance {f x--f z} (f ` Gxz)) (hausdorff_distance {f y--f z} (f ` Gyz))

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "... \<le> 4 * deltaG(TYPE('b)) + K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * deltaG TYPE('b) + max (hausdorff_distance {f x--f z} (f ` Gxz)) (hausdorff_distance {f y--f z} (f ` Gyz)) \<le> 4 * deltaG TYPE('b) + K
[PROOF STEP]
using HD[OF H(2)] HD[OF H(3)]
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` Gxz) {f x--f z} \<le> K
hausdorff_distance (f ` Gyz) {f y--f z} \<le> K

goal (1 subgoal):
 1. 4 * deltaG TYPE('b) + max (hausdorff_distance {f x--f z} (f ` Gxz)) (hausdorff_distance {f y--f z} (f ` Gyz)) \<le> 4 * deltaG TYPE('b) + K
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
4 * deltaG TYPE('b) + max (hausdorff_distance {f x--f z} (f ` Gxz)) (hausdorff_distance {f y--f z} (f ` Gyz)) \<le> 4 * deltaG TYPE('b) + K

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + K
[PROOF STEP]
have **: "infdist w2 (f`Gxz \<union> f`Gyz) \<le> 4 * deltaG(TYPE('b)) + K"
[PROOF STATE]
proof (prove)
using this:
infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + K

goal (1 subgoal):
 1. infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + K

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "infdist (f w) (f`Gxz \<union> f`Gyz) \<le> infdist w2 (f`Gxz \<union> f`Gyz) + dist (f w) w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f w) (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 (f ` Gxz \<union> f ` Gyz) + dist (f w) w2
[PROOF STEP]
by (rule infdist_triangle)
[PROOF STATE]
proof (state)
this:
infdist (f w) (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 (f ` Gxz \<union> f ` Gyz) + dist (f w) w2

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infdist (f w) (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 (f ` Gxz \<union> f ` Gyz) + dist (f w) w2
[PROOF STEP]
have A: "infdist (f w) (f`(Gxz \<union> Gyz)) \<le> 4 * deltaG(TYPE('b)) + 2 * K"
[PROOF STATE]
proof (prove)
using this:
infdist (f w) (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 (f ` Gxz \<union> f ` Gyz) + dist (f w) w2

goal (1 subgoal):
 1. infdist (f w) (f ` (Gxz \<union> Gyz)) \<le> 4 * deltaG TYPE('b) + 2 * K
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
infdist (f w) (f ` Gxz \<union> f ` Gyz) \<le> infdist w2 (f ` Gxz \<union> f ` Gyz) + dist (f w) w2
dist (f w) w2 \<le> K
infdist w2 (f ` Gxz \<union> f ` Gyz) \<le> 4 * deltaG TYPE('b) + K

goal (1 subgoal):
 1. infdist (f w) (f ` (Gxz \<union> Gyz)) \<le> 4 * deltaG TYPE('b) + 2 * K
[PROOF STEP]
by (auto simp add: image_Un)
[PROOF STATE]
proof (state)
this:
infdist (f w) (f ` (Gxz \<union> Gyz)) \<le> 4 * deltaG TYPE('b) + 2 * K

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
have "infdist w (Gxz \<union> Gyz) \<le> L + epsilon" if "epsilon > 0" for epsilon
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
have *: "epsilon/lambda > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < epsilon / lambda
[PROOF STEP]
using that C
[PROOF STATE]
proof (prove)
using this:
0 < epsilon
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. 0 < epsilon / lambda
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < epsilon / lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
have "\<exists>z \<in> f`(Gxz \<union> Gyz). dist (f w) z < 4 * deltaG(TYPE('b)) + 2 * K + epsilon/lambda"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>f ` (Gxz \<union> Gyz). dist (f w) z < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
[PROOF STEP]
apply (rule infdist_almost_attained)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. infdist (f w) (f ` (Gxz \<union> Gyz)) < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
 2. f ` (Gxz \<union> Gyz) \<noteq> {}
[PROOF STEP]
using A * H(2)
[PROOF STATE]
proof (prove)
using this:
infdist (f w) (f ` (Gxz \<union> Gyz)) \<le> 4 * deltaG TYPE('b) + 2 * K
0 < epsilon / lambda
geodesic_segment_between Gxz x z

goal (2 subgoals):
 1. infdist (f w) (f ` (Gxz \<union> Gyz)) < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
 2. f ` (Gxz \<union> Gyz) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>f ` (Gxz \<union> Gyz). dist (f w) z < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z\<in>f ` (Gxz \<union> Gyz). dist (f w) z < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
[PROOF STEP]
obtain z where z: "z \<in> Gxz \<union> Gyz" "dist (f w) (f z) < 4 * deltaG(TYPE('b)) + 2 * K + epsilon/lambda"
[PROOF STATE]
proof (prove)
using this:
\<exists>z\<in>f ` (Gxz \<union> Gyz). dist (f w) z < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> Gxz \<union> Gyz; dist (f w) (f z) < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> Gxz \<union> Gyz
dist (f w) (f z) < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
have "infdist w (Gxz \<union> Gyz) \<le> dist w z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> dist w z
[PROOF STEP]
by (auto intro!: infdist_le z(1))
[PROOF STATE]
proof (state)
this:
infdist w (Gxz \<union> Gyz) \<le> dist w z

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infdist w (Gxz \<union> Gyz) \<le> dist w z

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
have "... \<le> lambda * dist (f w) (f z) + C * lambda"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist w z \<le> lambda * dist (f w) (f z) + C * lambda
[PROOF STEP]
using quasi_isometry_onD[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; ?y \<in> UNIV\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> UNIV; ?y \<in> UNIV\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. dist w z \<le> lambda * dist (f w) (f z) + C * lambda
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
dist w z \<le> lambda * dist (f w) (f z) + C * lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist w z \<le> lambda * dist (f w) (f z) + C * lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
have "... \<le> lambda * (4 * deltaG(TYPE('b)) + 2 * K + epsilon/lambda) + C * lambda"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist (f w) (f z) + C * lambda \<le> lambda * (4 * deltaG TYPE('b) + 2 * K + epsilon / lambda) + C * lambda
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist (f w) (f z) \<le> 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
 2. 0 \<le> lambda
[PROOF STEP]
using z(2) C
[PROOF STATE]
proof (prove)
using this:
dist (f w) (f z) < 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
1 \<le> lambda
0 \<le> C

goal (2 subgoals):
 1. dist (f w) (f z) \<le> 4 * deltaG TYPE('b) + 2 * K + epsilon / lambda
 2. 0 \<le> lambda
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda * dist (f w) (f z) + C * lambda \<le> lambda * (4 * deltaG TYPE('b) + 2 * K + epsilon / lambda) + C * lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lambda * dist (f w) (f z) + C * lambda \<le> lambda * (4 * deltaG TYPE('b) + 2 * K + epsilon / lambda) + C * lambda

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
have "... = L + epsilon"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (4 * deltaG TYPE('b) + 2 * K + epsilon / lambda) + C * lambda = L + epsilon
[PROOF STEP]
unfolding K_def L_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (4 * deltaG TYPE('b) + 2 * (92 * lambda\<^sup>2 * (C + deltaG TYPE('b))) + epsilon / lambda) + C * lambda = lambda * (4 * 1 * deltaG TYPE('b) + 1 * 1 * C + 2 * (92 * lambda\<^sup>2 * (C + deltaG TYPE('b)))) + epsilon
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. lambda * (4 * deltaG TYPE('b) + 2 * (92 * lambda\<^sup>2 * (C + deltaG TYPE('b))) + epsilon / lambda) + C * lambda = lambda * (4 * 1 * deltaG TYPE('b) + 1 * 1 * C + 2 * (92 * lambda\<^sup>2 * (C + deltaG TYPE('b)))) + epsilon
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
lambda * (4 * deltaG TYPE('b) + 2 * K + epsilon / lambda) + C * lambda = L + epsilon

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist w (Gxz \<union> Gyz) \<le> L + epsilon

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L + epsilon
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
infdist w (Gxz \<union> Gyz) \<le> L + epsilon

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?epsilon \<Longrightarrow> infdist w (Gxz \<union> Gyz) \<le> L + ?epsilon

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?epsilon \<Longrightarrow> infdist w (Gxz \<union> Gyz) \<le> L + ?epsilon
[PROOF STEP]
have "infdist w (Gxz \<union> Gyz) \<le> L"
[PROOF STATE]
proof (prove)
using this:
0 < ?epsilon \<Longrightarrow> infdist w (Gxz \<union> Gyz) \<le> L + ?epsilon

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L
[PROOF STEP]
using field_le_epsilon
[PROOF STATE]
proof (prove)
using this:
0 < ?epsilon \<Longrightarrow> infdist w (Gxz \<union> Gyz) \<le> L + ?epsilon
(\<And>e. (0::?'a) < e \<Longrightarrow> ?x \<le> ?y + e) \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infdist w (Gxz \<union> Gyz) \<le> L

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infdist w (Gxz \<union> Gyz) \<le> L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist w (Gxz \<union> Gyz) \<le> L

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
using \<open>L \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
infdist w (Gxz \<union> Gyz) \<le> L
L \<le> M

goal (1 subgoal):
 1. infdist w (Gxz \<union> Gyz) \<le> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist w (Gxz \<union> Gyz) \<le> M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>geodesic_segment_between ?Gxy ?x ?y; geodesic_segment_between ?Gxz ?x ?z; geodesic_segment_between ?Gyz ?y ?z; ?w \<in> ?Gxy\<rbrakk> \<Longrightarrow> infdist ?w (?Gxz \<union> ?Gyz) \<le> M

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>geodesic_segment_between ?Gxy ?x ?y; geodesic_segment_between ?Gxz ?x ?z; geodesic_segment_between ?Gyz ?y ?z; ?w \<in> ?Gxy\<rbrakk> \<Longrightarrow> infdist ?w (?Gxz \<union> ?Gyz) \<le> M
[PROOF STEP]
have "Gromov_hyperbolic_subset (4 * M) (UNIV::'a set)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>geodesic_segment_between ?Gxy ?x ?y; geodesic_segment_between ?Gxz ?x ?z; geodesic_segment_between ?Gyz ?y ?z; ?w \<in> ?Gxy\<rbrakk> \<Longrightarrow> infdist ?w (?Gxz \<union> ?Gyz) \<le> M

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (4 * M) UNIV
[PROOF STEP]
using thin_triangles_implies_hyperbolic[OF Thin]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>geodesic_segment_between ?Gxy ?x ?y; geodesic_segment_between ?Gxz ?x ?z; geodesic_segment_between ?Gyz ?y ?z; ?w \<in> ?Gxy\<rbrakk> \<Longrightarrow> infdist ?w (?Gxz \<union> ?Gyz) \<le> M
\<lbrakk>\<And>x y z w Gxy Gyz Gxz. \<lbrakk>geodesic_segment_between Gxy x y; geodesic_segment_between Gxz x z; geodesic_segment_between Gyz y z; w \<in> Gxy\<rbrakk> \<Longrightarrow> geodesic_segment_between (?Gxy1 x y z w Gxy Gyz Gxz) (?x1 x y z w Gxy Gyz Gxz) (?y1 x y z w Gxy Gyz Gxz); \<And>x y z w Gxy Gyz Gxz. \<lbrakk>geodesic_segment_between Gxy x y; geodesic_segment_between Gxz x z; geodesic_segment_between Gyz y z; w \<in> Gxy\<rbrakk> \<Longrightarrow> geodesic_segment_between Gxz (?x1 x y z w Gxy Gyz Gxz) (?z1 x y z w Gxy Gyz Gxz); \<And>x y z w Gxy Gyz Gxz. \<lbrakk>geodesic_segment_between Gxy x y; geodesic_segment_between Gxz x z; geodesic_segment_between Gyz y z; w \<in> Gxy\<rbrakk> \<Longrightarrow> geodesic_segment_between Gyz (?y1 x y z w Gxy Gyz Gxz) (?z1 x y z w Gxy Gyz Gxz); \<And>x y z w Gxy Gyz Gxz. \<lbrakk>geodesic_segment_between Gxy x y; geodesic_segment_between Gxz x z; geodesic_segment_between Gyz y z; w \<in> Gxy\<rbrakk> \<Longrightarrow> w \<in> ?Gxy1 x y z w Gxy Gyz Gxz\<rbrakk> \<Longrightarrow> Gromov_hyperbolic_subset (4 * M) UNIV

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (4 * M) UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gromov_hyperbolic_subset (4 * M) UNIV

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Gromov_hyperbolic_subset (4 * M) UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Gromov_hyperbolic_subset (4 * M) UNIV

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
using this:
Gromov_hyperbolic_subset (4 * (188 * lambda ^ 3 * (C + deltaG TYPE('b)))) UNIV

goal (1 subgoal):
 1. Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Gromov_hyperbolic_invariant_under_quasi_isometry:
  assumes "quasi_isometric (UNIV::('a::geodesic_space) set) (UNIV::('b::Gromov_hyperbolic_space_geodesic) set)"
  shows "\<exists>delta. Gromov_hyperbolic_subset delta (UNIV::'a set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>delta. Gromov_hyperbolic_subset delta UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>delta. Gromov_hyperbolic_subset delta UNIV
[PROOF STEP]
obtain C lambda f where f: "lambda C-quasi_isometry_between (UNIV::'a set) (UNIV::'b set) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry_between UNIV UNIV f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quasi_isometric UNIV UNIV

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry_between UNIV UNIV f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding quasi_isometric_def
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C. Ex (lambda C -quasi_isometry_between UNIV UNIV)

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry_between UNIV UNIV f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda C -quasi_isometry_between UNIV UNIV f

goal (1 subgoal):
 1. \<exists>delta. Gromov_hyperbolic_subset delta UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>delta. Gromov_hyperbolic_subset delta UNIV
[PROOF STEP]
using Gromov_hyperbolic_invariant_under_quasi_isometry_explicit[OF quasi_isometry_betweenD(1)[OF f]]
[PROOF STATE]
proof (prove)
using this:
Gromov_hyperbolic_subset (752 * lambda ^ 3 * (C + deltaG TYPE('b))) UNIV

goal (1 subgoal):
 1. \<exists>delta. Gromov_hyperbolic_subset delta UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>delta. Gromov_hyperbolic_subset delta UNIV

goal:
No subgoals!
[PROOF STEP]
qed