[STATEMENT]
lemma Busemann_function_eq_additive_strength:
  assumes "isometry f" "Gromov_extension f xi = xi"
  shows "\<bar>Busemann_function_at xi ((f^^n) x) (x::'a::Gromov_hyperbolic_space) - real n * additive_strength f xi\<bar> \<le> 2 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
define u where "u = (\<lambda>y n. Busemann_function_at xi ((f^^n) y) y)"
[PROOF STATE]
proof (state)
this:
u = (\<lambda>y n. Busemann_function_at xi ((f ^^ n) y) y)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have *: "abs(u y (m+n) - u y m - u y n) \<le> 2 * deltaG(TYPE('a))" for n m y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u y (m + n) - u y m - u y n\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>u y (m + n) - u y m - u y n\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have P: "Gromov_extension (f^^m) xi = xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gromov_extension (f ^^ m) xi = xi
[PROOF STEP]
unfolding Gromov_extension_isometry_iterates[OF assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gromov_extension f ^^ m) xi = xi
[PROOF STEP]
apply (induction m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Gromov_extension f ^^ 0) xi = xi
 2. \<And>m. (Gromov_extension f ^^ m) xi = xi \<Longrightarrow> (Gromov_extension f ^^ Suc m) xi = xi
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry f
Gromov_extension f xi = xi

goal (2 subgoals):
 1. (Gromov_extension f ^^ 0) xi = xi
 2. \<And>m. (Gromov_extension f ^^ m) xi = xi \<Longrightarrow> (Gromov_extension f ^^ Suc m) xi = xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gromov_extension (f ^^ m) xi = xi

goal (1 subgoal):
 1. \<bar>u y (m + n) - u y m - u y n\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have *: "u y n = Busemann_function_at xi ((f^^m) ((f^^n) y)) ((f^^m) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u y n = Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)
[PROOF STEP]
apply (subst P[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u y n = Busemann_function_at (Gromov_extension (f ^^ m) xi) ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)
[PROOF STEP]
unfolding Busemann_function_isometry[OF isometry_iterates[OF \<open>isometry f\<close>]] u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Busemann_function_at xi ((f ^^ n) y) y = Busemann_function_at xi ((f ^^ n) y) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u y n = Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)

goal (1 subgoal):
 1. \<bar>u y (m + n) - u y m - u y n\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u y (m + n) - u y m - u y n\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u y (m + n) - u y m - Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ (m + n)) y) y - Busemann_function_at xi ((f ^^ m) y) y - Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
using Busemann_function_quasi_morphism[of xi "(f^^(m+n)) y" "(f^^m) y" y]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ (m + n)) y) ((f ^^ m) y) + Busemann_function_at xi ((f ^^ m) y) y - Busemann_function_at xi ((f ^^ (m + n)) y) y\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ (m + n)) y) y - Busemann_function_at xi ((f ^^ m) y) y - Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding funpow_add comp_def
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y) + Busemann_function_at xi ((f ^^ m) y) y - Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) y\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) y - Busemann_function_at xi ((f ^^ m) y) y - Busemann_function_at xi ((f ^^ m) ((f ^^ n) y)) ((f ^^ m) y)\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>u y (m + n) - u y m - u y n\<bar> \<le> 2 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>u ?y (?m + ?n) - u ?y ?m - u ?y ?n\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
define l where "l = (\<lambda>y. lim (\<lambda>n. u y n/n))"
[PROOF STATE]
proof (state)
this:
l = (\<lambda>y. lim (\<lambda>n. u y n / real n))

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have A: "abs(u y k - k * l y) \<le> 2 * deltaG(TYPE('a))" for y k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u y k - real k * l y\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u y k - real k * lim (\<lambda>n. u y n / real n)\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
using almost_additive_converges(2) *
[PROOF STATE]
proof (prove)
using this:
(\<And>m n. \<bar>?u (m + n) - ?u m - ?u n\<bar> \<le> ?C) \<Longrightarrow> \<bar>?u ?k - real ?k * lim (\<lambda>n. ?u n / real n)\<bar> \<le> ?C
\<bar>u ?y (?m + ?n) - u ?y ?m - u ?y ?n\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>u y k - real k * lim (\<lambda>n. u y n / real n)\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>u ?y ?k - real ?k * l ?y\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>u ?y ?k - real ?k * l ?y\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have *: "abs(Busemann_function_at xi ((f^^k) y) y - k * l y) \<le> 2 * deltaG(TYPE('a))" for y k
[PROOF STATE]
proof (prove)
using this:
\<bar>u ?y ?k - real ?k * l ?y\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ k) y) y - real k * l y\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ ?k) ?y) ?y - real ?k * l ?y\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ k) y) y - real k * l y\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>Busemann_function_at xi ((f ^^ ?k) ?y) ?y - real ?k * l ?y\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have "l basepoint = additive_strength f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l basepoint = additive_strength f xi
[PROOF STEP]
unfolding l_def u_def additive_strength_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (\<lambda>n. Busemann_function_at xi ((f ^^ n) basepoint) basepoint / real n) = lim (\<lambda>n. Busemann_function_at xi ((f ^^ n) basepoint) basepoint / real n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l basepoint = additive_strength f xi

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have "abs(k * l basepoint - k * l x) \<le> 4 * deltaG(TYPE('a)) + 2 * dist basepoint x" for k::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
have "abs(k * l basepoint - k * l x) = abs((Busemann_function_at xi ((f^^k) x) x - k * l x) - (Busemann_function_at xi ((f^^k) basepoint) basepoint - k * l basepoint)
                                                + (Busemann_function_at xi ((f^^k) basepoint) basepoint - Busemann_function_at xi ((f^^k) x) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> = \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x - (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint) + (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x)\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>real k * l basepoint - real k * l x\<bar> = \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x - (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint) + (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x)\<bar>

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real k * l basepoint - real k * l x\<bar> = \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x - (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint) + (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x)\<bar>

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
have "... \<le> abs (Busemann_function_at xi ((f^^k) x) x - k * l x) + abs (Busemann_function_at xi ((f^^k) basepoint) basepoint - k * l basepoint)
                      + abs (Busemann_function_at xi ((f^^k) basepoint) basepoint - Busemann_function_at xi ((f^^k) x) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x - (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint) + (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x)\<bar> \<le> \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x - (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint) + (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x)\<bar> \<le> \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x\<bar>

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x - (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint) + (Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x)\<bar> \<le> \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x\<bar>

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
have "... \<le> 2 * deltaG(TYPE('a)) + 2 * deltaG(TYPE('a)) + (dist ((f^^k) basepoint) ((f^^k) x) + dist basepoint x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x\<bar> \<le> 2 * deltaG TYPE('a) + 2 * deltaG TYPE('a) + (dist ((f ^^ k) basepoint) ((f ^^ k) x) + dist basepoint x)
[PROOF STEP]
by (intro mono_intros *)
[PROOF STATE]
proof (state)
this:
\<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x\<bar> \<le> 2 * deltaG TYPE('a) + 2 * deltaG TYPE('a) + (dist ((f ^^ k) basepoint) ((f ^^ k) x) + dist basepoint x)

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Busemann_function_at xi ((f ^^ k) x) x - real k * l x\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - real k * l basepoint\<bar> + \<bar>Busemann_function_at xi ((f ^^ k) basepoint) basepoint - Busemann_function_at xi ((f ^^ k) x) x\<bar> \<le> 2 * deltaG TYPE('a) + 2 * deltaG TYPE('a) + (dist ((f ^^ k) basepoint) ((f ^^ k) x) + dist basepoint x)

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
have "... = 4 * deltaG(TYPE('a)) + 2 * dist basepoint x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * deltaG TYPE('a) + 2 * deltaG TYPE('a) + (dist ((f ^^ k) basepoint) ((f ^^ k) x) + dist basepoint x) = 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
unfolding isometryD[OF isometry_iterates[OF assms(1)]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * deltaG TYPE('a) + 2 * deltaG TYPE('a) + (dist basepoint x + dist basepoint x) = 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * deltaG TYPE('a) + 2 * deltaG TYPE('a) + (dist ((f ^^ k) basepoint) ((f ^^ k) x) + dist basepoint x) = 4 * deltaG TYPE('a) + 2 * dist basepoint x

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x

goal (1 subgoal):
 1. \<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>real k * l basepoint - real k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>real ?k * l basepoint - real ?k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>real ?k * l basepoint - real ?k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
have "u = v" if H: "\<And>k::nat. abs(k * u - k * v) \<le> C" for u v C::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u = v
[PROOF STEP]
have "(\<lambda>n. abs(u - v)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<bar>u - v\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (rule tendsto_sandwich[of "\<lambda>n. 0" _ _ "\<lambda>n::nat. C/n"], auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n
 2. (\<lambda>x. C / real x) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. C*(1/n)) \<longlonglongrightarrow> C * 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. C * (1 / real x)) \<longlonglongrightarrow> C * 0
[PROOF STEP]
by (intro tendsto_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. C * (1 / real x)) \<longlonglongrightarrow> C * 0

goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n
 2. (\<lambda>x. C / real x) \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. C * (1 / real x)) \<longlonglongrightarrow> C * 0
[PROOF STEP]
show "(\<lambda>n. C/n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. C * (1 / real x)) \<longlonglongrightarrow> C * 0

goal (1 subgoal):
 1. (\<lambda>x. C / real x) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. C / real x) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n
[PROOF STEP]
have "\<bar>u - v\<bar> \<le> C / real n" if "n \<ge> 1" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u - v\<bar> \<le> C / real n
[PROOF STEP]
using H[of n] that
[PROOF STATE]
proof (prove)
using this:
\<bar>real n * u - real n * v\<bar> \<le> C
1 \<le> n

goal (1 subgoal):
 1. \<bar>u - v\<bar> \<le> C / real n
[PROOF STEP]
apply (simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bar>u * real n - v * real n\<bar> \<le> C; Suc 0 \<le> n\<rbrakk> \<Longrightarrow> real n * \<bar>u - v\<bar> \<le> C
[PROOF STEP]
by (metis H abs_mult abs_of_nat right_diff_distrib')
[PROOF STATE]
proof (state)
this:
1 \<le> ?n \<Longrightarrow> \<bar>u - v\<bar> \<le> C / real ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ?n \<Longrightarrow> \<bar>u - v\<bar> \<le> C / real ?n
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n"
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> \<bar>u - v\<bar> \<le> C / real ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> \<bar>u - v\<bar> \<le> C / real ?n

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. \<bar>u - v\<bar> \<le> C / real n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. \<bar>u - v\<bar> \<le> C / real n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<bar>u - v\<bar>) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. u = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<bar>u - v\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<bar>u - v\<bar>) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by (metis LIMSEQ_const_iff abs_0_eq eq_iff_diff_eq_0)
[PROOF STATE]
proof (state)
this:
u = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<And>x. \<bar>real x * ?u - real x * ?v\<bar> \<le> ?C) \<Longrightarrow> ?u = ?v

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>real ?k * l basepoint - real ?k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
(\<And>x. \<bar>real x * ?u - real x * ?v\<bar> \<le> ?C) \<Longrightarrow> ?u = ?v
[PROOF STEP]
have "l basepoint = l x"
[PROOF STATE]
proof (prove)
using this:
\<bar>real ?k * l basepoint - real ?k * l x\<bar> \<le> 4 * deltaG TYPE('a) + 2 * dist basepoint x
(\<And>x. \<bar>real x * ?u - real x * ?v\<bar> \<le> ?C) \<Longrightarrow> ?u = ?v

goal (1 subgoal):
 1. l basepoint = l x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l basepoint = l x

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
using A[of x n]
[PROOF STATE]
proof (prove)
using this:
\<bar>u x n - real n * l x\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding u_def \<open>l basepoint = l x\<close>[symmetric] \<open>l basepoint = additive_strength f xi\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma additive_strength_as_limit [tendsto_intros]:
  assumes "isometry f" "Gromov_extension f xi = xi"
  shows "(\<lambda>n. Busemann_function_at xi ((f^^n) x) x/n) \<longlonglongrightarrow> additive_strength f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. Busemann_function_at xi ((f ^^ n) x) x / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. Busemann_function_at xi ((f ^^ n) x) x / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
have "(\<lambda>n. abs(Busemann_function_at xi ((f^^n) x) x/n - additive_strength f xi)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule tendsto_sandwich[of "\<lambda>n. 0" _ _ "\<lambda>n. (2 * deltaG(TYPE('a))) * (1/real n)"], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a) / real n
 2. (\<lambda>n. 2 * deltaG TYPE('a) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>N. \<forall>n\<ge>N. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a) / real n
 2. (\<lambda>n. 2 * deltaG TYPE('a) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule exI[of _ 1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n\<ge>1. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a) / real n
 2. (\<lambda>n. 2 * deltaG TYPE('a) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
using Busemann_function_eq_additive_strength[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ ?n) ?x) ?x - real ?n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)

goal (2 subgoals):
 1. \<forall>n\<ge>1. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a) / real n
 2. (\<lambda>n. 2 * deltaG TYPE('a) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. 2 * deltaG TYPE('a) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
using tendsto_mult[OF _ lim_1_over_n]
[PROOF STATE]
proof (prove)
using this:
?f \<longlonglongrightarrow> ?a \<Longrightarrow> (\<lambda>x. ?f x * ((1::?'a1) / of_nat x)) \<longlonglongrightarrow> ?a * (0::?'a1)

goal (1 subgoal):
 1. (\<lambda>n. 2 * deltaG TYPE('a) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar>) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. Busemann_function_at xi ((f ^^ n) x) x / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar>) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. Busemann_function_at xi ((f ^^ n) x) x / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
using LIM_zero_iff tendsto_rabs_zero_cancel
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<bar>Busemann_function_at xi ((f ^^ n) x) x / real n - additive_strength f xi\<bar>) \<longlonglongrightarrow> 0
((\<lambda>x. ?f x - ?l) \<longlongrightarrow> (0::?'b)) ?F = (?f \<longlongrightarrow> ?l) ?F
((\<lambda>x. \<bar>?f x\<bar>) \<longlongrightarrow> 0) ?F \<Longrightarrow> (?f \<longlongrightarrow> 0) ?F

goal (1 subgoal):
 1. (\<lambda>n. Busemann_function_at xi ((f ^^ n) x) x / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Busemann_function_at xi ((f ^^ n) x) x / real n) \<longlonglongrightarrow> additive_strength f xi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_le_additive_strength:
  assumes "isometry (f::'a::Gromov_hyperbolic_space \<Rightarrow> 'a)" "Gromov_extension f xi = xi" "additive_strength f xi \<ge> 0" "n \<ge> 1"
  shows "dist x ((f^^n) x) \<le> dist x (f x) + real n * additive_strength f xi + ceiling (log 2 n) * 16 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
have A: "\<And>n. n \<in> {1..2^k} \<Longrightarrow> dist x ((f^^n) x) - real n * additive_strength f xi \<le> dist x (f x) + k * 16 * deltaG(TYPE('a))" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a)
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. n \<in> {1..2 ^ 0} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
 2. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n \<in> {1..2 ^ 0}

goal (2 subgoals):
 1. \<And>n. n \<in> {1..2 ^ 0} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
 2. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. n \<in> {1..2 ^ 0} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
 2. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
assume "n \<in> {1..2^0}"
[PROOF STATE]
proof (state)
this:
n \<in> {1..2 ^ 0}

goal (2 subgoals):
 1. \<And>n. n \<in> {1..2 ^ 0} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
 2. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> {1..2 ^ 0}
[PROOF STEP]
have "n = 1"
[PROOF STATE]
proof (prove)
using this:
n \<in> {1..2 ^ 0}

goal (1 subgoal):
 1. n = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 1

goal (2 subgoals):
 1. \<And>n. n \<in> {1..2 ^ 0} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
 2. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 1
[PROOF STEP]
show "dist x ((f^^n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
n = 1

goal (1 subgoal):
 1. dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
n = 1
0 \<le> additive_strength f xi

goal (1 subgoal):
 1. dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real 0 * 16 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ ?n) x) - real ?n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a)
n \<in> {1..2 ^ Suc k}

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
fix N::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
assume "N \<in> {1..2^(Suc k)}"
[PROOF STATE]
proof (state)
this:
N \<in> {1..2 ^ Suc k}

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<in> {1..2 ^ Suc k}
[PROOF STEP]
consider "N \<in> {1..2^k}" | "N \<in> {2^k<..2^(Suc k)}"
[PROOF STATE]
proof (prove)
using this:
N \<in> {1..2 ^ Suc k}

goal (1 subgoal):
 1. \<lbrakk>N \<in> {1..2 ^ k} \<Longrightarrow> thesis; N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using not_le
[PROOF STATE]
proof (prove)
using this:
N \<in> {1..2 ^ Suc k}
(\<not> ?x \<le> ?y) = (?y < ?x)

goal (1 subgoal):
 1. \<lbrakk>N \<in> {1..2 ^ k} \<Longrightarrow> thesis; N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>N \<in> {1..2 ^ k} \<Longrightarrow> ?thesis; N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<And>n. n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a); n \<in> {1..2 ^ Suc k}\<rbrakk> \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>N \<in> {1..2 ^ k} \<Longrightarrow> ?thesis; N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>N \<in> {1..2 ^ k} \<Longrightarrow> ?thesis; N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. N \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
 2. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
N \<in> {1..2 ^ k}

goal (2 subgoals):
 1. N \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
 2. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
by (rule order_trans[OF Suc.IH[OF 1]], auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
N \<in> {2 ^ k<..2 ^ Suc k}

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
define m::nat where "m = N - 2^k"
[PROOF STATE]
proof (state)
this:
m = N - 2 ^ k

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
define n::nat where "n = 2^k"
[PROOF STATE]
proof (state)
this:
n = 2 ^ k

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have nm: "N = n+m" "m \<in> {1..2^k}" "n \<in> {1..2^k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N = n + m &&& m \<in> {1..2 ^ k} &&& n \<in> {1..2 ^ k}
[PROOF STEP]
unfolding m_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N = 2 ^ k + (N - 2 ^ k) &&& N - 2 ^ k \<in> {1..2 ^ k} &&& 2 ^ k \<in> {1..2 ^ k}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
N \<in> {2 ^ k<..2 ^ Suc k}

goal (1 subgoal):
 1. N = 2 ^ k + (N - 2 ^ k) &&& N - 2 ^ k \<in> {1..2 ^ k} &&& 2 ^ k \<in> {1..2 ^ k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N = n + m
m \<in> {1..2 ^ k}
n \<in> {1..2 ^ k}

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have *: "(f^^(n+m)) x = (f^^n) ((f^^m) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ (n + m)) x = (f ^^ n) ((f ^^ m) x)
[PROOF STEP]
unfolding funpow_add comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ n) ((f ^^ m) x) = (f ^^ n) ((f ^^ m) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f ^^ (n + m)) x = (f ^^ n) ((f ^^ m) x)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have **: "(f^^(n+m)) x = (f^^m) ((f^^n) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ (n + m)) x = (f ^^ m) ((f ^^ n) x)
[PROOF STEP]
apply (subst add.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ (m + n)) x = (f ^^ m) ((f ^^ n) x)
[PROOF STEP]
unfolding funpow_add comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ m) ((f ^^ n) x) = (f ^^ m) ((f ^^ n) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f ^^ (n + m)) x = (f ^^ m) ((f ^^ n) x)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have "dist x ((f^^N) x) - N * additive_strength f xi - 2 * deltaG(TYPE('a)) \<le> dist x ((f^^(n+m)) x) - Busemann_function_at xi ((f^^(n+m)) x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ N) x) - real N * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x
[PROOF STEP]
unfolding nm(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ (n + m)) x) - real (n + m) * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x
[PROOF STEP]
using Busemann_function_eq_additive_strength[OF assms(1) assms(2), of "n+m" x]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ (n + m)) x) x - real (n + m) * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ (n + m)) x) - real (n + m) * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ N) x) - real N * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ N) x) - real N * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have "... \<le> max (dist x ((f^^n) x) - Busemann_function_at xi ((f^^n) x) x) (dist ((f^^n) x) ((f^^(n+m)) x) - Busemann_function_at xi ((f^^(n+m)) x) ((f^^n) x) - 2 * Busemann_function_at xi ((f^^n) x) x) + 8 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x \<le> max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a)
[PROOF STEP]
using dist_minus_Busemann_max_ineq
[PROOF STATE]
proof (prove)
using this:
dist ?x ?z - Busemann_function_at ?xi ?z ?x \<le> max (dist ?x ?y - Busemann_function_at ?xi ?y ?x) (dist ?y ?z - Busemann_function_at ?xi ?z ?y - 2 * Busemann_function_at ?xi ?y ?x) + 8 * deltaG TYPE(?'a)

goal (1 subgoal):
 1. dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x \<le> max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x \<le> max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) x \<le> max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have "... \<le> max (dist x ((f^^n) x) - (n * additive_strength f xi - 2 * deltaG(TYPE('a)))) (dist ((f^^n) x) ((f^^(n+m)) x) - (m * additive_strength f xi - 2 * deltaG(TYPE('a))) - 2 * (n * additive_strength f xi - 2 * deltaG(TYPE('a)))) + 8 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a)
[PROOF STEP]
unfolding **
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ m) ((f ^^ n) x)) - Busemann_function_at xi ((f ^^ m) ((f ^^ n) x)) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ m) ((f ^^ n) x)) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. real n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> Busemann_function_at xi ((f ^^ n) x) x
 2. real m * additive_strength f xi - 2 * deltaG TYPE('a) \<le> Busemann_function_at xi ((f ^^ m) ((f ^^ n) x)) ((f ^^ n) x)
 3. real n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> Busemann_function_at xi ((f ^^ n) x) x
 4. 0 \<le> 2
[PROOF STEP]
using Busemann_function_eq_additive_strength[OF assms(1) assms(2), of n x] Busemann_function_eq_additive_strength[OF assms(1) assms(2), of m "(f^^n) x"]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at xi ((f ^^ m) ((f ^^ n) x)) ((f ^^ n) x) - real m * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)

goal (4 subgoals):
 1. real n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> Busemann_function_at xi ((f ^^ n) x) x
 2. real m * additive_strength f xi - 2 * deltaG TYPE('a) \<le> Busemann_function_at xi ((f ^^ m) ((f ^^ n) x)) ((f ^^ n) x)
 3. real n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> Busemann_function_at xi ((f ^^ n) x) x
 4. 0 \<le> 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - Busemann_function_at xi ((f ^^ n) x) x) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - Busemann_function_at xi ((f ^^ (n + m)) x) ((f ^^ n) x) - 2 * Busemann_function_at xi ((f ^^ n) x) x) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have "... \<le> max (dist x ((f^^n) x) - n * additive_strength f xi + 6 * deltaG(TYPE('a))) (dist x ((f^^m) x) - m * additive_strength f xi + 6 * deltaG(TYPE('a))) + 8 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a)
[PROOF STEP]
unfolding * isometryD(2)[OF isometry_iterates[OF assms(1)], of n]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist x ((f ^^ m) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
0 \<le> additive_strength f xi

goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist x ((f ^^ m) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a)
[PROOF STEP]
by (intro mono_intros, auto)
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - (real n * additive_strength f xi - 2 * deltaG TYPE('a))) (dist ((f ^^ n) x) ((f ^^ (n + m)) x) - (real m * additive_strength f xi - 2 * deltaG TYPE('a)) - 2 * (real n * additive_strength f xi - 2 * deltaG TYPE('a))) + 8 * deltaG TYPE('a) \<le> max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have "... = max (dist x ((f^^n) x) - n * additive_strength f xi) (dist x ((f^^m) x) - m * additive_strength f xi) + 14 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a) = max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a)
[PROOF STEP]
unfolding max_add_distrib_left[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 6 * deltaG TYPE('a) + 8 * deltaG TYPE('a) = max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a) = max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - real n * additive_strength f xi + 6 * deltaG TYPE('a)) (dist x ((f ^^ m) x) - real m * additive_strength f xi + 6 * deltaG TYPE('a)) + 8 * deltaG TYPE('a) = max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
have "... \<le> dist x (f x) + k * 16 * deltaG(TYPE('a)) + 14 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a) \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a) + 14 * deltaG TYPE('a)
[PROOF STEP]
using nm
[PROOF STATE]
proof (prove)
using this:
N = n + m
m \<in> {1..2 ^ k}
n \<in> {1..2 ^ k}

goal (1 subgoal):
 1. max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a) \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a) + 14 * deltaG TYPE('a)
[PROOF STEP]
by (auto intro!: Suc.IH)
[PROOF STATE]
proof (state)
this:
max (dist x ((f ^^ n) x) - real n * additive_strength f xi) (dist x ((f ^^ m) x) - real m * additive_strength f xi) + 14 * deltaG TYPE('a) \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a) + 14 * deltaG TYPE('a)

goal (1 subgoal):
 1. N \<in> {2 ^ k<..2 ^ Suc k} \<Longrightarrow> dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x ((f ^^ N) x) - real N * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a) + 14 * deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x ((f ^^ N) x) - real N * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a) + 14 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ N) x) - real N * additive_strength f xi \<le> dist x (f x) + real (Suc k) * 16 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?n \<in> {1..2 ^ ?k1} \<Longrightarrow> dist x ((f ^^ ?n) x) - real ?n * additive_strength f xi \<le> dist x (f x) + real ?k1 * 16 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
define k::nat where "k = nat(ceiling (log 2 n))"
[PROOF STATE]
proof (state)
this:
k = nat \<lceil>log 2 (real n)\<rceil>

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
have "n \<le> 2^k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> 2 ^ k
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> 2 ^ nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
by (meson less_log2_of_power not_le real_nat_ceiling_ge)
[PROOF STATE]
proof (state)
this:
n \<le> 2 ^ k

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> 2 ^ k
[PROOF STEP]
have "dist x ((f^^n) x) - real n * additive_strength f xi \<le> dist x (f x) + k * 16 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
n \<le> 2 ^ k

goal (1 subgoal):
 1. dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a)
[PROOF STEP]
using A[of n k] \<open>n \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> 2 ^ k
n \<in> {1..2 ^ k} \<Longrightarrow> dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real k * 16 * deltaG TYPE('a)
1 \<le> n

goal (1 subgoal):
 1. dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
have "real (nat \<lceil>log 2 (real n)\<rceil>) = real_of_int \<lceil>log 2 (real n)\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (nat \<lceil>log 2 (real n)\<rceil>) = real_of_int \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
by (metis Transcendental.log_one \<open>n \<le> 2 ^ k\<close> assms(4) ceiling_zero int_ops(2) k_def le_antisym nat_eq_iff2 of_int_1 of_int_of_nat_eq order_refl power_0)
[PROOF STATE]
proof (state)
this:
real (nat \<lceil>log 2 (real n)\<rceil>) = real_of_int \<lceil>log 2 (real n)\<rceil>

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a)
real (nat \<lceil>log 2 (real n)\<rceil>) = real_of_int \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (k * 16) * deltaG TYPE('a)
real (nat \<lceil>log 2 (real n)\<rceil>) = real_of_int \<lceil>log 2 (real n)\<rceil>

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
using this:
dist x ((f ^^ n) x) - real n * additive_strength f xi \<le> dist x (f x) + real (nat \<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
real (nat \<lceil>log 2 (real n)\<rceil>) = real_of_int \<lceil>log 2 (real n)\<rceil>

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma additive_strength_inv:
  assumes "isometry (f::'a::Gromov_hyperbolic_space \<Rightarrow> 'a)" "Gromov_extension f xi = xi"
  shows "additive_strength (inv f) xi = - additive_strength f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
have *: "(inv f ^^ n) ((f ^^ n) x) = x" for n x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv f ^^ n) ((f ^^ n) x) = x
[PROOF STEP]
by (metis assms(1) comp_apply inv_fn_o_fn_is_id isometry_inverse(2))
[PROOF STATE]
proof (state)
this:
(inv f ^^ ?n) ((f ^^ ?n) ?x) = ?x

goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
have A: "abs(real n * additive_strength f xi + real n * additive_strength (inv f) xi) \<le> 6 * deltaG (TYPE('a))" for n::nat and x::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real n * additive_strength f xi + real n * additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a)
[PROOF STEP]
using Busemann_function_quasi_morphism[of xi x "(f^^n) x" x] Busemann_function_eq_additive_strength[OF assms, of n x] Busemann_function_eq_additive_strength[OF isometry_inverse(1)[OF assms(1)]
    Gromov_extension_inv_fixed_point[OF assms], of n "(f^^n) x"]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi x ((f ^^ n) x) + Busemann_function_at xi ((f ^^ n) x) x - Busemann_function_at xi x x\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at xi ((inv f ^^ n) ((f ^^ n) x)) ((f ^^ n) x) - real n * additive_strength (inv f) xi\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>real n * additive_strength f xi + real n * additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi x ((f ^^ n) x) + Busemann_function_at xi ((f ^^ n) x) x - Busemann_function_at xi x x\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at xi x ((f ^^ n) x) - real n * additive_strength (inv f) xi\<bar> \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>real n * additive_strength f xi + real n * additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>real ?n * additive_strength f xi + real ?n * additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a)

goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
have B: "abs(additive_strength f xi + additive_strength (inv f) xi) \<le> 6 * deltaG(TYPE('a)) * (1/n)" if "n \<ge> 1" for n::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real n)
[PROOF STEP]
using that A[of n]
[PROOF STATE]
proof (prove)
using this:
1 \<le> n
\<bar>real n * additive_strength f xi + real n * additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real n)
[PROOF STEP]
apply (simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 \<le> n; \<bar>real n * additive_strength f xi + real n * additive_strength (inv f) xi\<bar> \<le> deltaG TYPE('a) * 6\<rbrakk> \<Longrightarrow> real n * \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> deltaG TYPE('a) * 6
[PROOF STEP]
unfolding distrib_left[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 \<le> n; \<bar>real n * (additive_strength f xi + additive_strength (inv f) xi)\<bar> \<le> deltaG TYPE('a) * 6\<rbrakk> \<Longrightarrow> real n * \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> deltaG TYPE('a) * 6
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> ?n \<Longrightarrow> \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real ?n)

goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
have "(\<lambda>n. abs(additive_strength f xi + additive_strength (inv f) xi)) \<longlonglongrightarrow> 6 * deltaG(TYPE('a)) * 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar>) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
apply (rule tendsto_sandwich[of "\<lambda>n. 0" _ _ "\<lambda>n. 6 * deltaG(TYPE('a)) * (1/real n)"], simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>\<^sub>F n in sequentially. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real n)
 2. (\<lambda>n. 0) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
 3. (\<lambda>n. 6 * deltaG TYPE('a) * (1 / real n)) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<exists>N. \<forall>n\<ge>N. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real n)
 2. (\<lambda>n. 0) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
 3. (\<lambda>n. 6 * deltaG TYPE('a) * (1 / real n)) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
apply (rule exI[of _ 1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>n\<ge>1. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real n)
 2. (\<lambda>n. 0) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
 3. (\<lambda>n. 6 * deltaG TYPE('a) * (1 / real n)) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real ?n)

goal (3 subgoals):
 1. \<forall>n\<ge>1. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar> \<le> 6 * deltaG TYPE('a) * (1 / real n)
 2. (\<lambda>n. 0) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
 3. (\<lambda>n. 6 * deltaG TYPE('a) * (1 / real n)) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<lambda>n. 0) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
 2. (\<lambda>n. 6 * deltaG TYPE('a) * (1 / real n)) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
by (simp, intro tendsto_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar>) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0

goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar>) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar>) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0

goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
using LIMSEQ_unique mult_zero_right tendsto_const
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<bar>additive_strength f xi + additive_strength (inv f) xi\<bar>) \<longlonglongrightarrow> 6 * deltaG TYPE('a) * 0
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b
?a * (0::?'a) = (0::?'a)
((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F

goal (1 subgoal):
 1. additive_strength (inv f) xi = - additive_strength f xi
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
additive_strength (inv f) xi = - additive_strength f xi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stable_translation_length_eq_additive_strength_aux:
  assumes "isometry (f::'a::Gromov_hyperbolic_space \<Rightarrow> 'a)" "Gromov_extension f xi = xi" "additive_strength f xi \<ge> 0"
  shows "stable_translation_length f = additive_strength f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length f = additive_strength f xi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stable_translation_length f = additive_strength f xi
[PROOF STEP]
have "(\<lambda>n. dist x ((f^^n) x)/n) \<longlonglongrightarrow> additive_strength f xi" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x ((f ^^ n) x) / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
proof (rule tendsto_sandwich[of "\<lambda>n. (n * additive_strength f xi - 2 * deltaG(TYPE('a)))/real n" _ _ "\<lambda>n. (dist x (f x) + n * additive_strength f xi + ceiling (log 2 n) * 16 * deltaG(TYPE('a)))/ n"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
 2. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 3. (\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
 4. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
have "n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ n) x)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ n) x)
[PROOF STEP]
using Busemann_function_eq_additive_strength[OF assms(1) assms(2), of n x] Busemann_function_le_dist[of xi "(f^^n) x" x]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ n) x) x - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at xi ((f ^^ n) x) x\<bar> \<le> dist ((f ^^ n) x) x

goal (1 subgoal):
 1. real n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ n) x)
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
real ?n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ ?n) x)

goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
 2. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 3. (\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
 4. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real ?n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ ?n) x)
[PROOF STEP]
have "(n * additive_strength f xi - 2 * deltaG TYPE('a)) / n \<le> dist x ((f ^^ n) x) / n" if "n \<ge> 1" for n
[PROOF STATE]
proof (prove)
using this:
real ?n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ ?n) x)

goal (1 subgoal):
 1. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
real ?n * additive_strength f xi - 2 * deltaG TYPE('a) \<le> dist x ((f ^^ ?n) x)
1 \<le> n

goal (1 subgoal):
 1. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
[PROOF STEP]
by (simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
1 \<le> ?n \<Longrightarrow> (real ?n * additive_strength f xi - 2 * deltaG TYPE('a)) / real ?n \<le> dist x ((f ^^ ?n) x) / real ?n

goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
 2. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 3. (\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
 4. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ?n \<Longrightarrow> (real ?n * additive_strength f xi - 2 * deltaG TYPE('a)) / real ?n \<le> dist x ((f ^^ ?n) x) / real ?n
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n"
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> (real ?n * additive_strength f xi - 2 * deltaG TYPE('a)) / real ?n \<le> dist x ((f ^^ ?n) x) / real ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> (real ?n * additive_strength f xi - 2 * deltaG TYPE('a)) / real ?n \<le> dist x ((f ^^ ?n) x) / real ?n

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n \<le> dist x ((f ^^ n) x) / real n

goal (3 subgoals):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 2. (\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
 3. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
have B: "(\<lambda>n. additive_strength f xi - (2 * deltaG(TYPE('a))) * (1/n)) \<longlonglongrightarrow> additive_strength f xi - (2 * deltaG(TYPE('a))) * 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real x)) \<longlonglongrightarrow> additive_strength f xi - 2 * deltaG TYPE('a) * 0
[PROOF STEP]
by (intro tendsto_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real x)) \<longlonglongrightarrow> additive_strength f xi - 2 * deltaG TYPE('a) * 0

goal (3 subgoals):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 2. (\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
 3. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
show "(\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
proof (rule Lim_transform_eventually)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?f \<longlonglongrightarrow> additive_strength f xi
 2. \<forall>\<^sub>F x in sequentially. ?f x = (real x * additive_strength f xi - 2 * deltaG TYPE('a)) / real x
[PROOF STEP]
show "eventually (\<lambda>n. additive_strength f xi - (2 * deltaG(TYPE('a))) * (1/n) = (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real n) = (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real n) = (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n
[PROOF STEP]
apply (rule exI[of _ 1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>1. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real n) = (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n
[PROOF STEP]
by (simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real n) = (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n

goal (1 subgoal):
 1. (\<lambda>n. additive_strength f xi - 2 * deltaG TYPE('a) * (1 / real n)) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
qed (use B in auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (real n * additive_strength f xi - 2 * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi

goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 2. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
have "dist x ((f^^n) x) \<le> dist x (f x) + n * additive_strength f xi + ceiling (log 2 n) * 16 * deltaG(TYPE('a))" if "n \<ge> 1" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
using dist_le_additive_strength[OF assms that]
[PROOF STATE]
proof (prove)
using this:
dist ?x ((f ^^ n) ?x) \<le> dist ?x (f ?x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) \<le> dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)

goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 2. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) \<le> dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
have "(dist x ((f^^n) x))/n \<le> (dist x (f x) + n * additive_strength f xi + ceiling (log 2 n) * 16 * deltaG(TYPE('a)))/n" if "n \<ge> 1" for n
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) \<le> dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) \<le> dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)
1 \<le> n

goal (1 subgoal):
 1. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
by (simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) / real ?n \<le> (dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)) / real ?n

goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
 2. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) / real ?n \<le> (dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)) / real ?n
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n"
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) / real ?n \<le> (dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)) / real ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> dist x ((f ^^ ?n) x) / real ?n \<le> (dist x (f x) + real ?n * additive_strength f xi + real_of_int (\<lceil>log 2 (real ?n)\<rceil> * 16) * deltaG TYPE('a)) / real ?n

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n

goal (1 subgoal):
 1. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
have B: "(\<lambda>n. dist x (f x) * (1/n) + additive_strength f xi + 16 * deltaG TYPE('a) * (\<lceil>log 2 n\<rceil> / n)) \<longlonglongrightarrow> dist x (f x) * 0 + additive_strength f xi + 16 * deltaG TYPE('a) * 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n)) \<longlonglongrightarrow> dist x (f x) * 0 + additive_strength f xi + 16 * deltaG TYPE('a) * 0
[PROOF STEP]
by (intro tendsto_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n)) \<longlonglongrightarrow> dist x (f x) * 0 + additive_strength f xi + 16 * deltaG TYPE('a) * 0

goal (1 subgoal):
 1. (\<lambda>xa. (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
show "(\<lambda>n. (dist x (f x) + n * additive_strength f xi + real_of_int (\<lceil>log 2 n\<rceil> * 16) * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
proof (rule Lim_transform_eventually)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?f \<longlonglongrightarrow> additive_strength f xi
 2. \<forall>\<^sub>F xa in sequentially. ?f xa = (dist x (f x) + real xa * additive_strength f xi + real_of_int (\<lceil>log 2 (real xa)\<rceil> * 16) * deltaG TYPE('a)) / real xa
[PROOF STEP]
show "eventually (\<lambda>n. dist x (f x) * (1/n) + additive_strength f xi + 16 * deltaG TYPE('a) * (\<lceil>log 2 n\<rceil> / n) = (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n) = (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n) = (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
apply (rule exI[of _ 1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>1. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n) = (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n
[PROOF STEP]
by (simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n) = (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n

goal (1 subgoal):
 1. (\<lambda>n. dist x (f x) * (1 / real n) + additive_strength f xi + 16 * deltaG TYPE('a) * (real_of_int \<lceil>log 2 (real n)\<rceil> / real n)) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
qed (use B in auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (dist x (f x) + real n * additive_strength f xi + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)) / real n) \<longlonglongrightarrow> additive_strength f xi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist ?x ((f ^^ n) ?x) / real n) \<longlonglongrightarrow> additive_strength f xi

goal (1 subgoal):
 1. stable_translation_length f = additive_strength f xi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. dist ?x ((f ^^ n) ?x) / real n) \<longlonglongrightarrow> additive_strength f xi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist ?x ((f ^^ n) ?x) / real n) \<longlonglongrightarrow> additive_strength f xi

goal (1 subgoal):
 1. stable_translation_length f = additive_strength f xi
[PROOF STEP]
using LIMSEQ_unique stable_translation_length_as_pointwise_limit[OF isometryD(4)[OF assms(1)]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist ?x ((f ^^ n) ?x) / real n) \<longlonglongrightarrow> additive_strength f xi
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b
(\<lambda>n. dist ?x ((f ^^ n) ?x) / real n) \<longlonglongrightarrow> stable_translation_length f

goal (1 subgoal):
 1. stable_translation_length f = additive_strength f xi
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stable_translation_length f = additive_strength f xi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stable_translation_length_eq_additive_strength:
  assumes "isometry (f::'a::Gromov_hyperbolic_space \<Rightarrow> 'a)" "Gromov_extension f xi = xi"
  shows "stable_translation_length f = abs(additive_strength f xi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
proof (cases "additive_strength f xi \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
 2. \<not> 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> additive_strength f xi

goal (2 subgoals):
 1. 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
 2. \<not> 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> additive_strength f xi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> additive_strength f xi

goal (1 subgoal):
 1. stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
using stable_translation_length_eq_additive_strength_aux[OF assms]
[PROOF STATE]
proof (prove)
using this:
0 \<le> additive_strength f xi
0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = additive_strength f xi

goal (1 subgoal):
 1. stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stable_translation_length f = \<bar>additive_strength f xi\<bar>

goal (1 subgoal):
 1. \<not> 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> additive_strength f xi

goal (1 subgoal):
 1. \<not> 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 \<le> additive_strength f xi
[PROOF STEP]
have *: "abs(additive_strength f xi) = additive_strength (inv f) xi"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> additive_strength f xi

goal (1 subgoal):
 1. \<bar>additive_strength f xi\<bar> = additive_strength (inv f) xi
[PROOF STEP]
unfolding additive_strength_inv[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> additive_strength f xi

goal (1 subgoal):
 1. \<bar>additive_strength f xi\<bar> = - additive_strength f xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>additive_strength f xi\<bar> = additive_strength (inv f) xi

goal (1 subgoal):
 1. \<not> 0 \<le> additive_strength f xi \<Longrightarrow> stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length f = \<bar>additive_strength f xi\<bar>
[PROOF STEP]
unfolding * stable_translation_length_inv[OF assms(1), symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length (inv f) = additive_strength (inv f) xi
[PROOF STEP]
using stable_translation_length_eq_additive_strength_aux[OF isometry_inverse(1)[OF assms(1)] Gromov_extension_inv_fixed_point[OF assms]] *
[PROOF STATE]
proof (prove)
using this:
0 \<le> additive_strength (inv f) xi \<Longrightarrow> stable_translation_length (inv f) = additive_strength (inv f) xi
\<bar>additive_strength f xi\<bar> = additive_strength (inv f) xi

goal (1 subgoal):
 1. stable_translation_length (inv f) = additive_strength (inv f) xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stable_translation_length f = \<bar>additive_strength f xi\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma elliptic_isometryD:
  assumes "elliptic_isometry f"
  shows "bounded {(f^^n) x |n. True}"
        "isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {(f ^^ n) x |n. True} &&& isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f

goal (1 subgoal):
 1. bounded {(f ^^ n) x |n. True} &&& isometry f
[PROOF STEP]
unfolding elliptic_isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry f \<and> (\<forall>x. bounded {(f ^^ n) x |n. True})

goal (1 subgoal):
 1. bounded {(f ^^ n) x |n. True} &&& isometry f
[PROOF STEP]
by auto


[STATEMENT]
lemma elliptic_isometryI [intro]:
  assumes "bounded {(f^^n) x |n. True}"
          "isometry f"
  shows "elliptic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
have "bounded {(f^^n) y |n. True}" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {(f ^^ n) y |n. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded {(f ^^ n) y |n. True}
[PROOF STEP]
obtain c e where c: "\<And>n. dist c ((f^^n) x) \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c e. (\<And>n. dist c ((f ^^ n) x) \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) x |n. True}

goal (1 subgoal):
 1. (\<And>c e. (\<And>n. dist c ((f ^^ n) x) \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
\<exists>xa e. \<forall>y\<in>{(f ^^ n) x |n. True}. dist xa y \<le> e

goal (1 subgoal):
 1. (\<And>c e. (\<And>n. dist c ((f ^^ n) x) \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ ?n) x) \<le> e

goal (1 subgoal):
 1. bounded {(f ^^ n) y |n. True}
[PROOF STEP]
have "dist c ((f^^n) y) \<le> e + dist x y" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
have "dist c ((f^^n) y) \<le> dist c ((f^^n) x) + dist ((f^^n) x) ((f^^n) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> dist c ((f ^^ n) x) + dist ((f ^^ n) x) ((f ^^ n) y)
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ n) y) \<le> dist c ((f ^^ n) x) + dist ((f ^^ n) x) ((f ^^ n) y)

goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ n) y) \<le> dist c ((f ^^ n) x) + dist ((f ^^ n) x) ((f ^^ n) y)

goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
have "... \<le> e + dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c ((f ^^ n) x) + dist ((f ^^ n) x) ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
using c[of n] isometry_iterates[OF assms(2), of n]
[PROOF STATE]
proof (prove)
using this:
dist c ((f ^^ n) x) \<le> e
isometry (f ^^ n)

goal (1 subgoal):
 1. dist c ((f ^^ n) x) + dist ((f ^^ n) x) ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
by (intro mono_intros, auto simp add: isometryD)
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ n) x) + dist ((f ^^ n) x) ((f ^^ n) y) \<le> e + dist x y

goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist c ((f ^^ n) y) \<le> e + dist x y

goal (1 subgoal):
 1. dist c ((f ^^ n) y) \<le> e + dist x y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ n) y) \<le> e + dist x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ ?n) y) \<le> e + dist x y

goal (1 subgoal):
 1. bounded {(f ^^ n) y |n. True}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist c ((f ^^ ?n) y) \<le> e + dist x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist c ((f ^^ ?n) y) \<le> e + dist x y

goal (1 subgoal):
 1. bounded {(f ^^ n) y |n. True}
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
dist c ((f ^^ ?n) y) \<le> e + dist x y

goal (1 subgoal):
 1. \<exists>x e. \<forall>y\<in>{(f ^^ n) y |n. True}. dist x y \<le> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded {(f ^^ n) y |n. True}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bounded {(f ^^ n) ?y |n. True}

goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded {(f ^^ n) ?y |n. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) ?y |n. True}

goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
unfolding elliptic_isometry_def
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) ?y |n. True}

goal (1 subgoal):
 1. isometry f \<and> (\<forall>x. bounded {(f ^^ n) x |n. True})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) ?y |n. True}
bounded {(f ^^ n) x |n. True}
isometry f

goal (1 subgoal):
 1. isometry f \<and> (\<forall>x. bounded {(f ^^ n) x |n. True})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elliptic_isometry f

goal:
No subgoals!
[PROOF STEP]
qed