[STATEMENT]
lemma elliptic_isometry_inv:
  assumes "elliptic_isometry f"
  shows "elliptic_isometry (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
obtain c e where A: "\<And>n. dist c ((f^^n) basepoint) \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c e. (\<And>n. dist c ((f ^^ n) basepoint) \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using elliptic_isometryD(1)[OF assms, of basepoint]
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) basepoint |n. True}

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

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

goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
have "c = (f^^n) (((inv f)^^n) c)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (f ^^ n) ((inv f ^^ n) c)
[PROOF STEP]
using fn_o_inv_fn_is_id[OF isometry_inverse(2)[OF elliptic_isometryD(2)[OF assms]], of n]
[PROOF STATE]
proof (prove)
using this:
f ^^ n \<circ> inv f ^^ n = (\<lambda>x. x)

goal (1 subgoal):
 1. c = (f ^^ n) ((inv f ^^ n) c)
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f ^^ n) ((inv f ^^ n) x)) = (\<lambda>x. x)

goal (1 subgoal):
 1. c = (f ^^ n) ((inv f ^^ n) c)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
c = (f ^^ ?n) ((inv f ^^ ?n) c)

goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = (f ^^ ?n) ((inv f ^^ ?n) c)
[PROOF STEP]
have "dist ((f^^n) (((inv f)^^n) c)) ((f^^n) basepoint) \<le> e" for n
[PROOF STATE]
proof (prove)
using this:
c = (f ^^ ?n) ((inv f ^^ ?n) c)

goal (1 subgoal):
 1. dist ((f ^^ n) ((inv f ^^ n) c)) ((f ^^ n) basepoint) \<le> e
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
c = (f ^^ ?n) ((inv f ^^ ?n) c)
dist c ((f ^^ ?n) basepoint) \<le> e

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

goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist ((f ^^ ?n) ((inv f ^^ ?n) c)) ((f ^^ ?n) basepoint) \<le> e
[PROOF STEP]
have B: "dist basepoint (((inv f)^^n) c) \<le> e" for n
[PROOF STATE]
proof (prove)
using this:
dist ((f ^^ ?n) ((inv f ^^ ?n) c)) ((f ^^ ?n) basepoint) \<le> e

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) c) \<le> e
[PROOF STEP]
unfolding isometryD(2)[OF isometry_iterates[OF elliptic_isometryD(2)[OF assms]]]
[PROOF STATE]
proof (prove)
using this:
dist ((inv f ^^ ?n) c) basepoint \<le> e

goal (1 subgoal):
 1. dist basepoint ((inv f ^^ n) c) \<le> e
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist basepoint ((inv f ^^ ?n) c) \<le> e

goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry (inv f)
[PROOF STEP]
apply (rule elliptic_isometryI[of _ c])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bounded {(inv f ^^ n) c |n. True}
 2. isometry (inv f)
[PROOF STEP]
using isometry_inverse(1)[OF elliptic_isometryD(2)[OF assms]] B
[PROOF STATE]
proof (prove)
using this:
isometry (inv f)
dist basepoint ((inv f ^^ ?n) c) \<le> e

goal (2 subgoals):
 1. bounded {(inv f ^^ n) c |n. True}
 2. isometry (inv f)
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
isometry (inv f)
dist basepoint ((inv f ^^ ?n) c) \<le> e

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma elliptic_isometry_inv_iff:
  assumes "bij f"
  shows "elliptic_isometry (inv f) \<longleftrightarrow> elliptic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry (inv f) = elliptic_isometry f
[PROOF STEP]
using elliptic_isometry_inv[of f] elliptic_isometry_inv[of "inv f"] inv_inv_eq[OF assms]
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f \<Longrightarrow> elliptic_isometry (inv f)
elliptic_isometry (inv f) \<Longrightarrow> elliptic_isometry (inv (inv f))
inv (inv f) = f

goal (1 subgoal):
 1. elliptic_isometry (inv f) = elliptic_isometry f
[PROOF STEP]
by auto


[STATEMENT]
lemma elliptic_isometry_id:
  "elliptic_isometry id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry id
[PROOF STEP]
by (intro elliptic_isometryI isometryI, auto)


[STATEMENT]
lemma elliptic_isometry_stable_translation_length:
  assumes "elliptic_isometry f"
  shows "stable_translation_length f = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
obtain x::'a where True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (True \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
True

goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
have "bounded {(f^^n) x|n. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {(f ^^ n) x |n. True}
[PROOF STEP]
using elliptic_isometryD[OF assms]
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) ?x |n. True}
isometry f

goal (1 subgoal):
 1. bounded {(f ^^ n) x |n. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded {(f ^^ n) x |n. True}

goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded {(f ^^ n) x |n. True}
[PROOF STEP]
obtain c C where cC: "\<And>n. dist c ((f^^n) x) \<le> C"
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) x |n. True}

goal (1 subgoal):
 1. (\<And>c C. (\<And>n. dist c ((f ^^ n) x) \<le> C) \<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 C. (\<And>n. dist c ((f ^^ n) x) \<le> C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist c ((f ^^ ?n) x) \<le> C

goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
have "(\<lambda>n. dist x ((f^^n) x)/n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x ((f ^^ n) x) / real n) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (rule tendsto_sandwich[of "\<lambda>_. 0" _ sequentially "\<lambda>n. 2 * C / n"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> dist x ((f ^^ n) x) / real n
 2. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> 2 * C / real n
 3. (\<lambda>_. 0) \<longlonglongrightarrow> 0
 4. (\<lambda>x. 2 * C / real x) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. 2 * C * (1 / real n)) \<longlonglongrightarrow> 2 * C * 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. 2 * C * (1 / real n)) \<longlonglongrightarrow> 2 * C * 0
[PROOF STEP]
by (intro tendsto_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. 2 * C * (1 / real n)) \<longlonglongrightarrow> 2 * C * 0

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

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

goal (3 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> dist x ((f ^^ n) x) / real n
 2. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> 2 * C / real n
 3. (\<lambda>_. 0) \<longlonglongrightarrow> 0
[PROOF STEP]
have "dist x ((f ^^ n) x) / real n \<le> 2 * C / real n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x ((f ^^ n) x) / real n \<le> 2 * C / real n
[PROOF STEP]
using cC[of 0] cC[of n] dist_triangle[of x "(f^^n) x" c]
[PROOF STATE]
proof (prove)
using this:
dist c ((f ^^ 0) x) \<le> C
dist c ((f ^^ n) x) \<le> C
dist x ((f ^^ n) x) \<le> dist x c + dist c ((f ^^ n) x)

goal (1 subgoal):
 1. dist x ((f ^^ n) x) / real n \<le> 2 * C / real n
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps dist_commute)
[PROOF STATE]
proof (state)
this:
dist x ((f ^^ ?n) x) / real ?n \<le> 2 * C / real ?n

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

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. dist x ((f ^^ n) x) / real n \<le> 2 * C / 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> 2 * C / real n

goal (2 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> dist x ((f ^^ n) x) / real n
 2. (\<lambda>_. 0) \<longlonglongrightarrow> 0
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x ((f ^^ n) x) / real n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x ((f ^^ n) x) / real n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. stable_translation_length f = 0
[PROOF STEP]
have "(\<lambda>n. dist x ((f^^n) x)/n) \<longlonglongrightarrow> stable_translation_length f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist x ((f ^^ n) x) / real n) \<longlonglongrightarrow> stable_translation_length f
[PROOF STEP]
by (rule stable_translation_length_as_pointwise_limit[OF isometry_on_lipschitz[OF isometryD(1)[OF elliptic_isometryD(2)[OF assms]]]])
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist x ((f ^^ n) x) / real n) \<longlonglongrightarrow> stable_translation_length f

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_with_fixed_point_is_elliptic:
  assumes "isometry f" "f x = x"
  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 *: "(f^^n) x = x" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ n) x = x
[PROOF STEP]
apply (induction n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (f ^^ 0) x = x
 2. \<And>n. (f ^^ n) x = x \<Longrightarrow> (f ^^ Suc n) x = x
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
f x = x

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

goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
apply (rule elliptic_isometryI[of _ x, OF _ assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {(f ^^ n) x |n. True}
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {uu_. \<exists>n. uu_ = x \<and> True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elliptic_isometry f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parabolic_isometryD:
  assumes "parabolic_isometry f"
  shows "isometry f"
        "\<not>bounded {(f^^n) x|n. True}"
        "stable_translation_length f = 0"
        "\<not>elliptic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (isometry f &&& \<not> bounded {(f ^^ n) x |n. True}) &&& stable_translation_length f = 0 &&& \<not> elliptic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
parabolic_isometry f

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

goal (1 subgoal):
 1. (isometry f &&& \<not> bounded {(f ^^ n) x |n. True}) &&& stable_translation_length f = 0 &&& \<not> elliptic_isometry f
[PROOF STEP]
by auto


[STATEMENT]
lemma parabolic_isometryI:
  assumes "isometry f"
          "\<not>bounded {(f^^n) x|n. True}"
          "stable_translation_length f = 0"
  shows "parabolic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parabolic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry f
\<not> bounded {(f ^^ n) x |n. True}
stable_translation_length f = 0

goal (1 subgoal):
 1. parabolic_isometry f
[PROOF STEP]
unfolding parabolic_isometry_def elliptic_isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry f
\<not> bounded {(f ^^ n) x |n. True}
stable_translation_length f = 0

goal (1 subgoal):
 1. isometry f \<and> \<not> (isometry f \<and> (\<forall>x. bounded {(f ^^ n) x |n. True})) \<and> stable_translation_length f = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma loxodromic_isometryD:
  assumes "loxodromic_isometry f"
  shows "isometry f"
        "\<not>bounded {(f^^n) x|n. True}"
        "stable_translation_length f > 0"
        "\<not>elliptic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (isometry f &&& \<not> bounded {(f ^^ n) x |n. True}) &&& 0 < stable_translation_length f &&& \<not> elliptic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
loxodromic_isometry f

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

goal (1 subgoal):
 1. (isometry f &&& \<not> bounded {(f ^^ n) x |n. True}) &&& 0 < stable_translation_length f &&& \<not> elliptic_isometry f
[PROOF STEP]
by (auto, meson dual_order.antisym not_le stable_translation_length_nonneg)


[STATEMENT]
lemma loxodromic_isometryI:
  assumes "isometry f"
          "stable_translation_length f \<noteq> 0"
  shows "loxodromic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loxodromic_isometry f
[PROOF STEP]
using assms elliptic_isometry_stable_translation_length
[PROOF STATE]
proof (prove)
using this:
isometry f
stable_translation_length f \<noteq> 0
elliptic_isometry ?f \<Longrightarrow> stable_translation_length ?f = 0

goal (1 subgoal):
 1. loxodromic_isometry f
[PROOF STEP]
unfolding loxodromic_isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry f
stable_translation_length f \<noteq> 0
elliptic_isometry ?f \<Longrightarrow> stable_translation_length ?f = 0

goal (1 subgoal):
 1. isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma elliptic_or_parabolic_or_loxodromic:
  assumes "isometry f"
  shows "elliptic_isometry f \<or> parabolic_isometry f \<or> loxodromic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry f \<or> parabolic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry f

goal (1 subgoal):
 1. elliptic_isometry f \<or> parabolic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
unfolding parabolic_isometry_def loxodromic_isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry f

goal (1 subgoal):
 1. elliptic_isometry f \<or> isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f = 0 \<or> isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma elliptic_imp_not_parabolic_loxodromic:
  assumes "elliptic_isometry f"
  shows "\<not>parabolic_isometry f"
        "\<not>loxodromic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> parabolic_isometry f &&& \<not> loxodromic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f

goal (1 subgoal):
 1. \<not> parabolic_isometry f &&& \<not> loxodromic_isometry f
[PROOF STEP]
unfolding parabolic_isometry_def loxodromic_isometry_def
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f

goal (1 subgoal):
 1. \<not> (isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f = 0) &&& \<not> (isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f \<noteq> 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma parabolic_imp_not_elliptic_loxodromic:
  assumes "parabolic_isometry f"
  shows "\<not>elliptic_isometry f"
        "\<not>loxodromic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> elliptic_isometry f &&& \<not> loxodromic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
parabolic_isometry f

goal (1 subgoal):
 1. \<not> elliptic_isometry f &&& \<not> loxodromic_isometry f
[PROOF STEP]
unfolding parabolic_isometry_def loxodromic_isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f = 0

goal (1 subgoal):
 1. \<not> elliptic_isometry f &&& \<not> (isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f \<noteq> 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma loxodromic_imp_not_elliptic_parabolic:
  assumes "loxodromic_isometry f"
  shows "\<not>elliptic_isometry f"
        "\<not>parabolic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> elliptic_isometry f &&& \<not> parabolic_isometry f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
loxodromic_isometry f

goal (1 subgoal):
 1. \<not> elliptic_isometry f &&& \<not> parabolic_isometry f
[PROOF STEP]
unfolding parabolic_isometry_def loxodromic_isometry_def
[PROOF STATE]
proof (prove)
using this:
isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f \<noteq> 0

goal (1 subgoal):
 1. \<not> elliptic_isometry f &&& \<not> (isometry f \<and> \<not> elliptic_isometry f \<and> stable_translation_length f = 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma parabolic_isometry_inv:
  assumes "parabolic_isometry f"
  shows "parabolic_isometry (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parabolic_isometry (inv f)
[PROOF STEP]
unfolding parabolic_isometry_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry (inv f) \<and> \<not> elliptic_isometry (inv f) \<and> stable_translation_length (inv f) = 0
[PROOF STEP]
using isometry_inverse[of f] elliptic_isometry_inv_iff[of f]
parabolic_isometryD[OF assms] stable_translation_length_inv[of f]
[PROOF STATE]
proof (prove)
using this:
isometry f \<Longrightarrow> isometry (inv f)
isometry f \<Longrightarrow> bij f
bij f \<Longrightarrow> elliptic_isometry (inv f) = elliptic_isometry f
isometry f
\<not> bounded {(f ^^ n) ?x |n. True}
stable_translation_length f = 0
\<not> elliptic_isometry f
isometry f \<Longrightarrow> stable_translation_length (inv f) = stable_translation_length f

goal (1 subgoal):
 1. isometry (inv f) \<and> \<not> elliptic_isometry (inv f) \<and> stable_translation_length (inv f) = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma loxodromic_isometry_inv:
  assumes "loxodromic_isometry f"
  shows "loxodromic_isometry (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loxodromic_isometry (inv f)
[PROOF STEP]
unfolding loxodromic_isometry_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry (inv f) \<and> \<not> elliptic_isometry (inv f) \<and> stable_translation_length (inv f) \<noteq> 0
[PROOF STEP]
using isometry_inverse[of f] elliptic_isometry_inv_iff[of f]
loxodromic_isometryD[OF assms] stable_translation_length_inv[of f]
[PROOF STATE]
proof (prove)
using this:
isometry f \<Longrightarrow> isometry (inv f)
isometry f \<Longrightarrow> bij f
bij f \<Longrightarrow> elliptic_isometry (inv f) = elliptic_isometry f
isometry f
\<not> bounded {(f ^^ n) ?x |n. True}
0 < stable_translation_length f
\<not> elliptic_isometry f
isometry f \<Longrightarrow> stable_translation_length (inv f) = stable_translation_length f

goal (1 subgoal):
 1. isometry (inv f) \<and> \<not> elliptic_isometry (inv f) \<and> stable_translation_length (inv f) \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma high_scores:
  fixes u::"nat \<Rightarrow> real" and i::nat and C::real
  assumes "\<not>(bdd_above (range u))"
  shows "\<exists>n. (\<forall>l \<le> n. u l \<le> u n) \<and> u n \<ge> C \<and> n \<ge> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
define M where "M = max C (Max {u l|l. l < i})"
[PROOF STATE]
proof (state)
this:
M = max C (Max {u l |l. l < i})

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
define n where "n = Inf {m. u m > M}"
[PROOF STATE]
proof (state)
this:
n = Inf {m. M < u m}

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
have "\<not>(range u \<subseteq> {..M})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> range u \<subseteq> {..M}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> bdd_above (range u)

goal (1 subgoal):
 1. \<not> range u \<subseteq> {..M}
[PROOF STEP]
by (meson bdd_above_Iic bdd_above_mono)
[PROOF STATE]
proof (state)
this:
\<not> range u \<subseteq> {..M}

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> range u \<subseteq> {..M}
[PROOF STEP]
have "{m. u m > M} \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<not> range u \<subseteq> {..M}

goal (1 subgoal):
 1. {m. M < u m} \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> range u \<subseteq> {..M}
\<not> bdd_above (range u)

goal (1 subgoal):
 1. {m. M < u m} \<noteq> {}
[PROOF STEP]
by (simp add: image_subset_iff not_less)
[PROOF STATE]
proof (state)
this:
{m. M < u m} \<noteq> {}

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{m. M < u m} \<noteq> {}
[PROOF STEP]
have "n \<in> {m. u m > M}"
[PROOF STATE]
proof (prove)
using this:
{m. M < u m} \<noteq> {}

goal (1 subgoal):
 1. n \<in> {m. M < u m}
[PROOF STEP]
unfolding n_def
[PROOF STATE]
proof (prove)
using this:
{m. M < u m} \<noteq> {}

goal (1 subgoal):
 1. Inf {m. M < u m} \<in> {m. M < u m}
[PROOF STEP]
using Inf_nat_def1
[PROOF STATE]
proof (prove)
using this:
{m. M < u m} \<noteq> {}
?K \<noteq> {} \<Longrightarrow> Inf ?K \<in> ?K

goal (1 subgoal):
 1. Inf {m. M < u m} \<in> {m. M < u m}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
n \<in> {m. M < u m}

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> {m. M < u m}
[PROOF STEP]
have "u n > M"
[PROOF STATE]
proof (prove)
using this:
n \<in> {m. M < u m}

goal (1 subgoal):
 1. M < u n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M < u n

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
have "n \<ge> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> False
[PROOF STEP]
assume "\<not> i \<le> n"
[PROOF STATE]
proof (state)
this:
\<not> i \<le> n

goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> i \<le> n
[PROOF STEP]
have *: "n < i"
[PROOF STATE]
proof (prove)
using this:
\<not> i \<le> n

goal (1 subgoal):
 1. n < i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < i

goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> False
[PROOF STEP]
have "u n \<le> Max {u l|l. l < i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n \<le> Max {u l |l. l < i}
[PROOF STEP]
apply (rule Max_ge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {u l |l. l < i}
 2. u n \<in> {u l |l. l < i}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n < i

goal (2 subgoals):
 1. finite {u l |l. l < i}
 2. u n \<in> {u l |l. l < i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u n \<le> Max {u l |l. l < i}

goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u n \<le> Max {u l |l. l < i}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
u n \<le> Max {u l |l. l < i}

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>u n > M\<close> M_def
[PROOF STATE]
proof (prove)
using this:
u n \<le> Max {u l |l. l < i}
M < u n
M = max C (Max {u l |l. l < i})

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<le> n

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<le> n

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
have "u l \<le> u n" if "l \<le> n" for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u l \<le> u n
[PROOF STEP]
proof (cases "l = n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = n \<Longrightarrow> u l \<le> u n
 2. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l = n

goal (2 subgoals):
 1. l = n \<Longrightarrow> u l \<le> u n
 2. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l = n

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

goal (1 subgoal):
 1. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
l \<noteq> n

goal (1 subgoal):
 1. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> n
[PROOF STEP]
have "l < n"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> n

goal (1 subgoal):
 1. l < n
[PROOF STEP]
using \<open>l \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
l \<noteq> n
l \<le> n

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

goal (1 subgoal):
 1. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l < n
[PROOF STEP]
have "l \<notin> {m. u m > M}"
[PROOF STATE]
proof (prove)
using this:
l < n

goal (1 subgoal):
 1. l \<notin> {m. M < u m}
[PROOF STEP]
unfolding n_def
[PROOF STATE]
proof (prove)
using this:
l < Inf {m. M < u m}

goal (1 subgoal):
 1. l \<notin> {m. M < u m}
[PROOF STEP]
by (meson bdd_below_def cInf_lower not_le zero_le)
[PROOF STATE]
proof (state)
this:
l \<notin> {m. M < u m}

goal (1 subgoal):
 1. l \<noteq> n \<Longrightarrow> u l \<le> u n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<notin> {m. M < u m}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<notin> {m. M < u m}

goal (1 subgoal):
 1. u l \<le> u n
[PROOF STEP]
using \<open>u n > M\<close>
[PROOF STATE]
proof (prove)
using this:
l \<notin> {m. M < u m}
M < u n

goal (1 subgoal):
 1. u l \<le> u n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u l \<le> u n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?l \<le> n \<Longrightarrow> u ?l \<le> u n

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<le> n
?l \<le> n \<Longrightarrow> u ?l \<le> u n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> n
?l \<le> n \<Longrightarrow> u ?l \<le> u n

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
using \<open>u n > M\<close> M_def less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
i \<le> n
?l \<le> n \<Longrightarrow> u ?l \<le> u n
M < u n
M = max C (Max {u l |l. l < i})
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. \<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> C \<le> u n \<and> i \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_not_elliptic_has_attracting_fixed_point:
  assumes "isometry f"
          "\<not>(elliptic_isometry f)"
  shows "\<exists>xi \<in> Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
define u where "u = (\<lambda>n. dist basepoint ((f^^n) basepoint))"
[PROOF STATE]
proof (state)
this:
u = (\<lambda>n. dist basepoint ((f ^^ n) basepoint))

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have NB: "\<not>(bdd_above (range u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bdd_above (range u)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above (range u) \<Longrightarrow> False
[PROOF STEP]
assume "bdd_above (range u)"
[PROOF STATE]
proof (state)
this:
bdd_above (range u)

goal (1 subgoal):
 1. bdd_above (range u) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bdd_above (range u)
[PROOF STEP]
obtain C where *: "\<And>n. u n \<le> C"
[PROOF STATE]
proof (prove)
using this:
bdd_above (range u)

goal (1 subgoal):
 1. (\<And>C. (\<And>n. u n \<le> C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding bdd_above_def
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>x\<in>range u. x \<le> M

goal (1 subgoal):
 1. (\<And>C. (\<And>n. u n \<le> C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u ?n \<le> C

goal (1 subgoal):
 1. bdd_above (range u) \<Longrightarrow> False
[PROOF STEP]
have "bounded {(f^^n) basepoint|n. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {(f ^^ n) basepoint |n. True}
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x e. \<forall>y\<in>{(f ^^ n) basepoint |n. True}. dist x y \<le> e
[PROOF STEP]
apply (rule exI[of _ basepoint], rule exI[of _ C])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>{(f ^^ n) basepoint |n. True}. dist basepoint y \<le> C
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
u ?n \<le> C

goal (1 subgoal):
 1. \<forall>y\<in>{(f ^^ n) basepoint |n. True}. dist basepoint y \<le> C
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ ?n) basepoint) \<le> C

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

goal (1 subgoal):
 1. bdd_above (range u) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded {(f ^^ n) basepoint |n. True}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) basepoint |n. True}

goal (1 subgoal):
 1. False
[PROOF STEP]
using elliptic_isometryI assms
[PROOF STATE]
proof (prove)
using this:
bounded {(f ^^ n) basepoint |n. True}
\<lbrakk>bounded {(?f ^^ n) ?x |n. True}; isometry ?f\<rbrakk> \<Longrightarrow> elliptic_isometry ?f
isometry f
\<not> elliptic_isometry f

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> bdd_above (range u)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have "\<exists>r. \<forall>n. ((\<forall>l \<le> r n. u l \<le> u (r n)) \<and> u (r n) \<ge> 2 * n) \<and> r (Suc n) \<ge> r n + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. \<forall>n. ((\<forall>l\<le>r n. u l \<le> u (r n)) \<and> 2 * real n \<le> u (r n)) \<and> r n + 1 \<le> r (Suc n)
[PROOF STEP]
apply (rule dependent_nat_choice)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>x. (\<forall>l\<le>x. u l \<le> u x) \<and> 2 * real 0 \<le> u x
 2. \<And>x n. (\<forall>l\<le>x. u l \<le> u x) \<and> 2 * real n \<le> u x \<Longrightarrow> \<exists>y. ((\<forall>l\<le>y. u l \<le> u y) \<and> 2 * real (Suc n) \<le> u y) \<and> x + 1 \<le> y
[PROOF STEP]
using high_scores[OF NB]
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (\<forall>l\<le>n. u l \<le> u n) \<and> ?C \<le> u n \<and> ?i \<le> n

goal (2 subgoals):
 1. \<exists>x. (\<forall>l\<le>x. u l \<le> u x) \<and> 2 * real 0 \<le> u x
 2. \<And>x n. (\<forall>l\<le>x. u l \<le> u x) \<and> 2 * real n \<le> u x \<Longrightarrow> \<exists>y. ((\<forall>l\<le>y. u l \<le> u y) \<and> 2 * real (Suc n) \<le> u y) \<and> x + 1 \<le> y
[PROOF STEP]
by (auto) blast
[PROOF STATE]
proof (state)
this:
\<exists>r. \<forall>n. ((\<forall>l\<le>r n. u l \<le> u (r n)) \<and> 2 * real n \<le> u (r n)) \<and> r n + 1 \<le> r (Suc n)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r. \<forall>n. ((\<forall>l\<le>r n. u l \<le> u (r n)) \<and> 2 * real n \<le> u (r n)) \<and> r n + 1 \<le> r (Suc n)
[PROOF STEP]
obtain r::"nat \<Rightarrow> nat" where r: "\<And>n l. l \<le> r n \<Longrightarrow> u l \<le> u (r n)"
                                       "\<And>n. u (r n) \<ge> 2 * n" "\<And>n. r (Suc n) \<ge> r n + 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>r. \<forall>n. ((\<forall>l\<le>r n. u l \<le> u (r n)) \<and> 2 * real n \<le> u (r n)) \<and> r n + 1 \<le> r (Suc n)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>\<And>n l. l \<le> r n \<Longrightarrow> u l \<le> u (r n); \<And>n. real (2 * n) \<le> u (r n); \<And>n. r n + 1 \<le> r (Suc n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?l \<le> r ?n \<Longrightarrow> u ?l \<le> u (r ?n)
real (2 * ?n) \<le> u (r ?n)
r ?n + 1 \<le> r (Suc ?n)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?l \<le> r ?n \<Longrightarrow> u ?l \<le> u (r ?n)
real (2 * ?n) \<le> u (r ?n)
r ?n + 1 \<le> r (Suc ?n)
[PROOF STEP]
have "strict_mono r"
[PROOF STATE]
proof (prove)
using this:
?l \<le> r ?n \<Longrightarrow> u ?l \<le> u (r ?n)
real (2 * ?n) \<le> u (r ?n)
r ?n + 1 \<le> r (Suc ?n)

goal (1 subgoal):
 1. strict_mono r
[PROOF STEP]
by (metis Suc_eq_plus1 Suc_le_lessD strict_monoI_Suc)
[PROOF STATE]
proof (state)
this:
strict_mono r

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_mono r
[PROOF STEP]
have "r n \<ge> n" for n
[PROOF STATE]
proof (prove)
using this:
strict_mono r

goal (1 subgoal):
 1. n \<le> r n
[PROOF STEP]
by (simp add: seq_suble)
[PROOF STATE]
proof (state)
this:
?n \<le> r ?n

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have A: "dist ((f^^(r p)) basepoint) ((f^^(r n)) basepoint) \<le> dist basepoint ((f^^(r n)) basepoint)" if "n \<ge> p" for n p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
have "r n \<ge> r p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r p \<le> r n
[PROOF STEP]
using \<open>n \<ge> p\<close> \<open>strict_mono r\<close>
[PROOF STATE]
proof (prove)
using this:
p \<le> n
strict_mono r

goal (1 subgoal):
 1. r p \<le> r n
[PROOF STEP]
by (simp add: strict_mono_less_eq)
[PROOF STATE]
proof (state)
this:
r p \<le> r n

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r p \<le> r n
[PROOF STEP]
have *: "f^^((r n)) = (f^^(r p)) o (f^^(r n - r p))"
[PROOF STATE]
proof (prove)
using this:
r p \<le> r n

goal (1 subgoal):
 1. f ^^ r n = f ^^ r p \<circ> f ^^ (r n - r p)
[PROOF STEP]
unfolding funpow_add[symmetric]
[PROOF STATE]
proof (prove)
using this:
r p \<le> r n

goal (1 subgoal):
 1. f ^^ r n = f ^^ (r p + (r n - r p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ^^ r n = f ^^ r p \<circ> f ^^ (r n - r p)

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
have "dist ((f^^(r p)) basepoint) ((f^^(r n)) basepoint) = dist ((f^^(r p)) basepoint) ((f^^(r p)) ((f^^(r n - r p)) basepoint))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) = dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint))
[PROOF STEP]
unfolding * comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint)) = dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) = dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint))

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) = dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint))

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
have "... = dist basepoint ((f^^(r n - r p)) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint)) = dist basepoint ((f ^^ (r n - r p)) basepoint)
[PROOF STEP]
using isometry_iterates[OF assms(1), of "r p"] isometryD
[PROOF STATE]
proof (prove)
using this:
isometry (f ^^ r p)
isometry ?f \<Longrightarrow> isometry_on UNIV ?f
isometry ?f \<Longrightarrow> dist (?f ?x) (?f ?y) = dist ?x ?y
isometry ?f \<Longrightarrow> surj ?f
isometry ?f \<Longrightarrow> 1-lipschitz_on UNIV ?f
isometry ?f \<Longrightarrow> isUCont ?f
isometry ?f \<Longrightarrow> continuous_on UNIV ?f

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint)) = dist basepoint ((f ^^ (r n - r p)) basepoint)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint)) = dist basepoint ((f ^^ (r n - r p)) basepoint)

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist ((f ^^ r p) basepoint) ((f ^^ r p) ((f ^^ (r n - r p)) basepoint)) = dist basepoint ((f ^^ (r n - r p)) basepoint)

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
have "... \<le> dist basepoint ((f^^(r n)) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist basepoint ((f ^^ (r n - r p)) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
using r(1)[of "r n - r p" n]
[PROOF STATE]
proof (prove)
using this:
r n - r p \<le> r n \<Longrightarrow> u (r n - r p) \<le> u (r n)

goal (1 subgoal):
 1. dist basepoint ((f ^^ (r n - r p)) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
r n - r p \<le> r n \<Longrightarrow> dist basepoint ((f ^^ (r n - r p)) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. dist basepoint ((f ^^ (r n - r p)) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ (r n - r p)) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p \<le> ?n \<Longrightarrow> dist ((f ^^ r ?p) basepoint) ((f ^^ r ?n) basepoint) \<le> dist basepoint ((f ^^ r ?n) basepoint)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have *: "Gromov_product_at basepoint ((f^^(r p)) basepoint) ((f^^(r n)) basepoint) \<ge> p" if "n \<ge> p" for n p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
have "2 * Gromov_product_at basepoint ((f^^(r p)) basepoint) ((f^^(r n)) basepoint)
            = dist basepoint ((f^^(r p)) basepoint) + dist basepoint ((f^^(r n)) basepoint)
              - dist ((f^^(r p)) basepoint) ((f^^(r n)) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) = dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
unfolding Gromov_product_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * ((dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)) / 2) = dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) = dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) = dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
have "... \<ge> dist basepoint ((f^^(r p)) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist basepoint ((f ^^ r p) basepoint) \<le> dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
using A[OF that]
[PROOF STATE]
proof (prove)
using this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. dist basepoint ((f ^^ r p) basepoint) \<le> dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ r p) basepoint) \<le> dist basepoint ((f ^^ r p) basepoint) + dist basepoint ((f ^^ r n) basepoint) - dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist basepoint ((f ^^ r p) basepoint) \<le> 2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
show "Gromov_product_at basepoint ((f^^(r p)) basepoint) ((f^^(r n)) basepoint) \<ge> p"
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ r p) basepoint) \<le> 2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
using r(2)[of p]
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ r p) basepoint) \<le> 2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
real (2 * p) \<le> u (r p)

goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ r p) basepoint) \<le> 2 * Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
real (2 * p) \<le> dist basepoint ((f ^^ r p) basepoint)

goal (1 subgoal):
 1. real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p \<le> ?n \<Longrightarrow> real ?p \<le> Gromov_product_at basepoint ((f ^^ r ?p) basepoint) ((f ^^ r ?n) basepoint)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have *: "Gromov_product_at basepoint ((f^^(r p)) basepoint) ((f^^(r n)) basepoint) \<ge> N" if "n \<ge> N" "p \<ge> N" for n p N
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real N \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
using *[of n p] *[of p n] that
[PROOF STATE]
proof (prove)
using this:
n \<le> p \<Longrightarrow> real n \<le> Gromov_product_at basepoint ((f ^^ r n) basepoint) ((f ^^ r p) basepoint)
p \<le> n \<Longrightarrow> real p \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
N \<le> n
N \<le> p

goal (1 subgoal):
 1. real N \<le> Gromov_product_at basepoint ((f ^^ r p) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
by (auto simp add: Gromov_product_commute intro: le_cases[of n p])
[PROOF STATE]
proof (state)
this:
\<lbrakk>?N \<le> ?n; ?N \<le> ?p\<rbrakk> \<Longrightarrow> real ?N \<le> Gromov_product_at basepoint ((f ^^ r ?p) basepoint) ((f ^^ r ?n) basepoint)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have "Gromov_converging_at_boundary (\<lambda>n. (f^^(r n)) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gromov_converging_at_boundary (\<lambda>n. (f ^^ r n) basepoint)
[PROOF STEP]
apply (rule Gromov_converging_at_boundaryI[of basepoint])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. M \<le> Gromov_product_at basepoint ((f ^^ r m) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?N \<le> ?n; ?N \<le> ?p\<rbrakk> \<Longrightarrow> real ?N \<le> Gromov_product_at basepoint ((f ^^ r ?p) basepoint) ((f ^^ r ?n) basepoint)

goal (1 subgoal):
 1. \<And>M. \<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. M \<le> Gromov_product_at basepoint ((f ^^ r m) basepoint) ((f ^^ r n) basepoint)
[PROOF STEP]
by (meson dual_order.trans real_arch_simple)
[PROOF STATE]
proof (state)
this:
Gromov_converging_at_boundary (\<lambda>n. (f ^^ r n) basepoint)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
with Gromov_converging_at_boundary_converges[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>Gromov_boundary. (\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> x
Gromov_converging_at_boundary (\<lambda>n. (f ^^ r n) basepoint)
[PROOF STEP]
obtain xi where xi: "(\<lambda>n. to_Gromov_completion ((f^^(r n)) basepoint)) \<longlonglongrightarrow> xi" "xi \<in> Gromov_boundary"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>Gromov_boundary. (\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> x
Gromov_converging_at_boundary (\<lambda>n. (f ^^ r n) basepoint)

goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>(\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> xi; xi \<in> Gromov_boundary\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> xi
xi \<in> Gromov_boundary

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> xi
xi \<in> Gromov_boundary
[PROOF STEP]
have *: "(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f^^(r n)) basepoint))) \<longlonglongrightarrow> xi"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> xi
xi \<in> Gromov_boundary

goal (1 subgoal):
 1. (\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> xi
[PROOF STEP]
apply (simp, rule Gromov_converging_at_boundary_bounded_perturbation[of _ _ _ "dist basepoint (f basepoint)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> xi; xi \<in> Gromov_boundary\<rbrakk> \<Longrightarrow> dist ((f ^^ r n) basepoint) (f ((f ^^ r n) basepoint)) \<le> dist basepoint (f basepoint)
[PROOF STEP]
by (simp add: assms(1) funpow_swap1 isometryD(2) isometry_iterates)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> xi

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> xi

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have "(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f^^(r n)) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi
[PROOF STEP]
using continuous_on_tendsto_compose[OF Gromov_extension_isometry(2)[OF assms(1)] xi(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xi \<in> UNIV; \<forall>\<^sub>F x in sequentially. to_Gromov_completion ((f ^^ r x) basepoint) \<in> UNIV\<rbrakk> \<Longrightarrow> (\<lambda>x. Gromov_extension f (to_Gromov_completion ((f ^^ r x) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi

goal (1 subgoal):
 1. (\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> xi
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi
[PROOF STEP]
have fxi: "Gromov_extension f xi = xi"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> xi
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi

goal (1 subgoal):
 1. Gromov_extension f xi = xi
[PROOF STEP]
using LIMSEQ_unique
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> xi
(\<lambda>n. Gromov_extension f (to_Gromov_completion ((f ^^ r n) basepoint))) \<longlonglongrightarrow> Gromov_extension f xi
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b

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

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have "Busemann_function_at (to_Gromov_completion ((f^^(r n)) basepoint)) ((f^^(r p)) basepoint) basepoint \<le> 0" if "n \<ge> p" for n p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Busemann_function_at (to_Gromov_completion ((f ^^ r n) basepoint)) ((f ^^ r p) basepoint) basepoint \<le> 0
[PROOF STEP]
unfolding Busemann_function_inner
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) - dist basepoint ((f ^^ r n) basepoint) \<le> 0
[PROOF STEP]
using A[OF that]
[PROOF STATE]
proof (prove)
using this:
dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) \<le> dist basepoint ((f ^^ r n) basepoint)

goal (1 subgoal):
 1. dist ((f ^^ r p) basepoint) ((f ^^ r n) basepoint) - dist basepoint ((f ^^ r n) basepoint) \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?p \<le> ?n \<Longrightarrow> Busemann_function_at (to_Gromov_completion ((f ^^ r ?n) basepoint)) ((f ^^ r ?p) basepoint) basepoint \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?p \<le> ?n \<Longrightarrow> Busemann_function_at (to_Gromov_completion ((f ^^ r ?n) basepoint)) ((f ^^ r ?p) basepoint) basepoint \<le> 0
[PROOF STEP]
have A: "eventually (\<lambda>n. Busemann_function_at (to_Gromov_completion ((f^^(r n)) basepoint)) ((f^^(r p)) basepoint) basepoint \<le> 0) sequentially" for p
[PROOF STATE]
proof (prove)
using this:
?p \<le> ?n \<Longrightarrow> Busemann_function_at (to_Gromov_completion ((f ^^ r ?n) basepoint)) ((f ^^ r ?p) basepoint) basepoint \<le> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. Busemann_function_at (to_Gromov_completion ((f ^^ r n) basepoint)) ((f ^^ r p) basepoint) basepoint \<le> 0
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
?p \<le> ?n \<Longrightarrow> Busemann_function_at (to_Gromov_completion ((f ^^ r ?n) basepoint)) ((f ^^ r ?p) basepoint) basepoint \<le> 0

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. Busemann_function_at (to_Gromov_completion ((f ^^ r n) basepoint)) ((f ^^ r p) basepoint) basepoint \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. Busemann_function_at (to_Gromov_completion ((f ^^ r n) basepoint)) ((f ^^ r ?p) basepoint) basepoint \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have B: "eventually (\<lambda>n. Busemann_function_at (to_Gromov_completion ((f^^(r n)) basepoint)) ((f^^(r p)) basepoint) basepoint \<ge> Busemann_function_at xi ((f^^(r p)) basepoint) basepoint - 2 * deltaG(TYPE('a)) - 1) sequentially" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. Busemann_function_at xi ((f ^^ r p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> Busemann_function_at (to_Gromov_completion ((f ^^ r n) basepoint)) ((f ^^ r p) basepoint) basepoint
[PROOF STEP]
by (rule eventually_mono[OF Busemann_function_inside_approx[OF _ xi(1), of 1 "((f^^(r p)) basepoint)" basepoint, simplified]], simp)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> Busemann_function_at (to_Gromov_completion ((f ^^ r n) basepoint)) ((f ^^ r ?p) basepoint) basepoint

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have "eventually (\<lambda>n. Busemann_function_at xi ((f^^(r p)) basepoint) basepoint - 2 * deltaG(TYPE('a)) - 1 \<le> 0) sequentially" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. Busemann_function_at xi ((f ^^ r p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0
[PROOF STEP]
by (rule eventually_mono[OF eventually_conj[OF A[of p] B[of p]]], simp)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0
[PROOF STEP]
have *: "Busemann_function_at xi ((f^^(r p)) basepoint) basepoint - 2 * deltaG(TYPE('a)) - 1 \<le> 0" for p
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0

goal (1 subgoal):
 1. Busemann_function_at xi ((f ^^ r p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0
[PROOF STEP]
have A: "Busemann_function_at xi ((f^^(r p)) basepoint) basepoint / (r p) - (2 * deltaG(TYPE('a)) + 1) * (1/r p) \<le> 0" if "p \<ge> 1" for p
[PROOF STATE]
proof (prove)
using this:
Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0

goal (1 subgoal):
 1. Busemann_function_at xi ((f ^^ r p) basepoint) basepoint / real (r p) - (2 * deltaG TYPE('a) + 1) * (1 / real (r p)) \<le> 0
[PROOF STEP]
using order_trans[OF that \<open>p \<le> r p\<close>]
[PROOF STATE]
proof (prove)
using this:
Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint - 2 * deltaG TYPE('a) - 1 \<le> 0
1 \<le> r p

goal (1 subgoal):
 1. Busemann_function_at xi ((f ^^ r p) basepoint) basepoint / real (r p) - (2 * deltaG TYPE('a) + 1) * (1 / real (r p)) \<le> 0
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
1 \<le> ?p \<Longrightarrow> Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint / real (r ?p) - (2 * deltaG TYPE('a) + 1) * (1 / real (r ?p)) \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have B: "(\<lambda>p. Busemann_function_at xi ((f^^(p)) basepoint) basepoint / p - (2 * deltaG(TYPE('a)) + 1) * (1/p)) \<longlonglongrightarrow> additive_strength f xi - (2 * deltaG(TYPE('a)) + 1) * 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. Busemann_function_at xi ((f ^^ p) basepoint) basepoint / real p - (2 * deltaG TYPE('a) + 1) * (1 / real p)) \<longlonglongrightarrow> additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0
[PROOF STEP]
by (intro tendsto_intros assms fxi)
[PROOF STATE]
proof (state)
this:
(\<lambda>p. Busemann_function_at xi ((f ^^ p) basepoint) basepoint / real p - (2 * deltaG TYPE('a) + 1) * (1 / real p)) \<longlonglongrightarrow> additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
have "additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0 \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0 \<le> 0
[PROOF STEP]
apply (rule LIMSEQ_le_const2[OF LIMSEQ_subseq_LIMSEQ[OF B \<open>strict_mono r\<close>]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. ((\<lambda>p. Busemann_function_at xi ((f ^^ p) basepoint) basepoint / real p - (2 * deltaG TYPE('a) + 1) * (1 / real p)) \<circ> r) n \<le> 0
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?p \<Longrightarrow> Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint / real (r ?p) - (2 * deltaG TYPE('a) + 1) * (1 / real (r ?p)) \<le> 0

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. ((\<lambda>p. Busemann_function_at xi ((f ^^ p) basepoint) basepoint / real p - (2 * deltaG TYPE('a) + 1) * (1 / real p)) \<circ> r) n \<le> 0
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?p \<Longrightarrow> Busemann_function_at xi ((f ^^ r ?p) basepoint) basepoint / real (r ?p) - (2 * deltaG TYPE('a) + 1) * (1 / real (r ?p)) \<le> 0

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. Busemann_function_at xi ((f ^^ r n) basepoint) basepoint / real (r n) - (2 * deltaG TYPE('a) + 1) * (1 / real (r n)) \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0 \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0 \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0 \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
using xi fxi
[PROOF STATE]
proof (prove)
using this:
additive_strength f xi - (2 * deltaG TYPE('a) + 1) * 0 \<le> 0
(\<lambda>n. to_Gromov_completion ((f ^^ r n) basepoint)) \<longlonglongrightarrow> xi
xi \<in> Gromov_boundary
Gromov_extension f xi = xi

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<le> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_not_elliptic_has_repelling_fixed_point:
  assumes "isometry f"
          "\<not>(elliptic_isometry f)"
  shows "\<exists>xi \<in> Gromov_boundary. Gromov_extension f xi = xi \<and> additive_strength f xi \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
have *: "\<not>elliptic_isometry (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> elliptic_isometry (inv f)
[PROOF STEP]
using elliptic_isometry_inv_iff isometry_inverse(2)[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
bij ?f \<Longrightarrow> elliptic_isometry (inv ?f) = elliptic_isometry ?f
bij f
\<not> elliptic_isometry f

goal (1 subgoal):
 1. \<not> elliptic_isometry (inv f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> elliptic_isometry (inv f)

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
obtain xi where xi: "xi \<in> Gromov_boundary" "Gromov_extension (inv f) xi = xi" "additive_strength (inv f) xi \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension (inv f) xi = xi; additive_strength (inv f) xi \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using isometry_not_elliptic_has_attracting_fixed_point[OF isometry_inverse(1)[OF assms(1)] *]
[PROOF STATE]
proof (prove)
using this:
\<exists>xi\<in>Gromov_boundary. Gromov_extension (inv f) xi = xi \<and> additive_strength (inv f) xi \<le> 0

goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension (inv f) xi = xi; additive_strength (inv f) xi \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension (inv f) xi = xi
additive_strength (inv f) xi \<le> 0

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
have *: "Gromov_extension f xi = xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gromov_extension f xi = xi
[PROOF STEP]
using Gromov_extension_inv_fixed_point[OF isometry_inverse(1)[OF assms(1)] xi(2)] inv_inv_eq[OF isometry_inverse(2)[OF assms(1)]]
[PROOF STATE]
proof (prove)
using this:
Gromov_extension (inv (inv f)) xi = xi
inv (inv f) = f

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

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Gromov_extension f xi = xi

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
have "additive_strength f xi \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> additive_strength f xi
[PROOF STEP]
using additive_strength_inv[OF assms(1) *] xi(3)
[PROOF STATE]
proof (prove)
using this:
additive_strength (inv f) xi = - additive_strength f xi
additive_strength (inv f) xi \<le> 0

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

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Gromov_extension f xi = xi
0 \<le> additive_strength f xi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Gromov_extension f xi = xi
0 \<le> additive_strength f xi

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
using xi(1)
[PROOF STATE]
proof (prove)
using this:
Gromov_extension f xi = xi
0 \<le> additive_strength f xi
xi \<in> Gromov_boundary

goal (1 subgoal):
 1. \<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xi\<in>Gromov_boundary. Gromov_extension f xi = xi \<and> 0 \<le> additive_strength f xi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parabolic_fixed_point:
  assumes "parabolic_isometry f"
  shows "neutral_fixed_point f \<in> Gromov_boundary"
        "Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f"
        "additive_strength f (neutral_fixed_point f) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neutral_fixed_point f \<in> Gromov_boundary &&& Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f &&& additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. neutral_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f
 3. additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
obtain xi where xi: "xi \<in> Gromov_boundary" "Gromov_extension f xi = xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension f xi = xi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using isometry_not_elliptic_has_attracting_fixed_point parabolic_isometryD[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isometry ?f; \<not> elliptic_isometry ?f\<rbrakk> \<Longrightarrow> \<exists>xi\<in>Gromov_boundary. Gromov_extension ?f xi = xi \<and> additive_strength ?f xi \<le> 0
isometry f
\<not> bounded {(f ^^ n) ?x |n. True}
stable_translation_length f = 0
\<not> elliptic_isometry f

goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension f xi = xi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi

goal (3 subgoals):
 1. neutral_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f
 3. additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi

goal (3 subgoals):
 1. neutral_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f
 3. additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
have "additive_strength f xi = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive_strength f xi = 0
[PROOF STEP]
using stable_translation_length_eq_additive_strength[OF parabolic_isometryD(1)[OF assms] xi(2)]
    parabolic_isometryD(3)[OF assms]
[PROOF STATE]
proof (prove)
using this:
stable_translation_length f = \<bar>additive_strength f xi\<bar>
stable_translation_length f = 0

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

goal (3 subgoals):
 1. neutral_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f
 3. additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
additive_strength f xi = 0
[PROOF STEP]
have A: "\<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0"
[PROOF STATE]
proof (prove)
using this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
additive_strength f xi = 0

goal (1 subgoal):
 1. \<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0

goal (3 subgoals):
 1. neutral_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f
 3. additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
show "neutral_fixed_point f \<in> Gromov_boundary"
        "Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f"
        "additive_strength f (neutral_fixed_point f) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neutral_fixed_point f \<in> Gromov_boundary &&& Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f &&& additive_strength f (neutral_fixed_point f) = 0
[PROOF STEP]
unfolding neutral_fixed_point_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) \<in> Gromov_boundary &&& Gromov_extension f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) = (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) &&& additive_strength f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) = 0
[PROOF STEP]
using someI_ex[OF A]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x = 0) \<in> Gromov_boundary \<and> Gromov_extension f (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x = 0) = (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x = 0) \<and> additive_strength f (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x = 0) = 0

goal (1 subgoal):
 1. (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) \<in> Gromov_boundary &&& Gromov_extension f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) = (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) &&& additive_strength f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi = 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
neutral_fixed_point f \<in> Gromov_boundary
Gromov_extension f (neutral_fixed_point f) = neutral_fixed_point f
additive_strength f (neutral_fixed_point f) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem parabolic_unique_fixed_point:
  assumes "parabolic_isometry f"
  shows "Gromov_extension f xi = xi \<longleftrightarrow> xi = neutral_fixed_point f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gromov_extension f xi = xi) = (xi = neutral_fixed_point f)
[PROOF STEP]
proof (auto simp add: parabolic_fixed_point[OF assms])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gromov_extension f xi = xi \<Longrightarrow> xi = neutral_fixed_point f
[PROOF STEP]
assume H: "Gromov_extension f xi = xi"
[PROOF STATE]
proof (state)
this:
Gromov_extension f xi = xi

goal (1 subgoal):
 1. Gromov_extension f xi = xi \<Longrightarrow> xi = neutral_fixed_point f
[PROOF STEP]
have *: "additive_strength f xi = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive_strength f xi = 0
[PROOF STEP]
using stable_translation_length_eq_additive_strength[OF parabolic_isometryD(1)[OF assms] H]
    parabolic_isometryD(3)[OF assms]
[PROOF STATE]
proof (prove)
using this:
stable_translation_length f = \<bar>additive_strength f xi\<bar>
stable_translation_length f = 0

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

goal (1 subgoal):
 1. Gromov_extension f xi = xi \<Longrightarrow> xi = neutral_fixed_point f
[PROOF STEP]
show "xi = neutral_fixed_point f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xi = neutral_fixed_point f
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xi \<noteq> neutral_fixed_point f \<Longrightarrow> False
[PROOF STEP]
assume N: "xi \<noteq> neutral_fixed_point f"
[PROOF STATE]
proof (state)
this:
xi \<noteq> neutral_fixed_point f

goal (1 subgoal):
 1. xi \<noteq> neutral_fixed_point f \<Longrightarrow> False
[PROOF STEP]
define C where "C = 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) + 4 * deltaG(TYPE('a))"
[PROOF STATE]
proof (state)
this:
C = 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) + 4 * deltaG TYPE('a)

goal (1 subgoal):
 1. xi \<noteq> neutral_fixed_point f \<Longrightarrow> False
[PROOF STEP]
have A: "dist basepoint ((f^^n) basepoint) \<le> C" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
have "dist ((f^^n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG(TYPE('a))
            \<le> max (Busemann_function_at xi ((f^^n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f^^n) basepoint) basepoint)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint)
[PROOF STEP]
using dist_le_max_Busemann_functions[OF N]
[PROOF STATE]
proof (prove)
using this:
dist ?x ?y \<le> 2 * real_of_ereal (extended_Gromov_product_at ?y xi (neutral_fixed_point f)) + max (Busemann_function_at xi ?x ?y) (Busemann_function_at (neutral_fixed_point f) ?x ?y) + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
have "... \<le> max (n * additive_strength f xi + 2 * deltaG(TYPE('a))) (n * additive_strength f (neutral_fixed_point f) + 2 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint) \<le> max (real n * additive_strength f xi + 2 * deltaG TYPE('a)) (real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a))
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Busemann_function_at xi ((f ^^ n) basepoint) basepoint \<le> real n * additive_strength f xi + 2 * deltaG TYPE('a)
 2. Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint \<le> real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a)
[PROOF STEP]
using Busemann_function_eq_additive_strength[OF parabolic_isometryD(1)[OF assms] H, of n basepoint]
        Busemann_function_eq_additive_strength[OF parabolic_isometryD(1)[OF assms] parabolic_fixed_point(2)[OF assms], of n basepoint]
[PROOF STATE]
proof (prove)
using this:
\<bar>Busemann_function_at xi ((f ^^ n) basepoint) basepoint - real n * additive_strength f xi\<bar> \<le> 2 * deltaG TYPE('a)
\<bar>Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint - real n * additive_strength f (neutral_fixed_point f)\<bar> \<le> 2 * deltaG TYPE('a)

goal (2 subgoals):
 1. Busemann_function_at xi ((f ^^ n) basepoint) basepoint \<le> real n * additive_strength f xi + 2 * deltaG TYPE('a)
 2. Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint \<le> real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint) \<le> max (real n * additive_strength f xi + 2 * deltaG TYPE('a)) (real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (Busemann_function_at xi ((f ^^ n) basepoint) basepoint) (Busemann_function_at (neutral_fixed_point f) ((f ^^ n) basepoint) basepoint) \<le> max (real n * additive_strength f xi + 2 * deltaG TYPE('a)) (real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
have "... = 2 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (real n * additive_strength f xi + 2 * deltaG TYPE('a)) (real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a)) = 2 * deltaG TYPE('a)
[PROOF STEP]
unfolding * parabolic_fixed_point[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (real n * 0 + 2 * deltaG TYPE('a)) (real n * 0 + 2 * deltaG TYPE('a)) = 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (real n * additive_strength f xi + 2 * deltaG TYPE('a)) (real n * additive_strength f (neutral_fixed_point f) + 2 * deltaG TYPE('a)) = 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> 2 * deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> C
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
dist ((f ^^ n) basepoint) basepoint - 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) - 2 * deltaG TYPE('a) \<le> 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> 2 * real_of_ereal (extended_Gromov_product_at basepoint xi (neutral_fixed_point f)) + 4 * deltaG TYPE('a)
[PROOF STEP]
by (simp add: algebra_simps dist_commute)
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ n) basepoint) \<le> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ ?n) basepoint) \<le> C

goal (1 subgoal):
 1. xi \<noteq> neutral_fixed_point f \<Longrightarrow> False
[PROOF STEP]
have "elliptic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
apply (rule elliptic_isometryI[of _ basepoint])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bounded {(f ^^ n) basepoint |n. True}
 2. isometry f
[PROOF STEP]
using parabolic_isometryD(1)[OF assms] A
[PROOF STATE]
proof (prove)
using this:
isometry f
dist basepoint ((f ^^ ?n) basepoint) \<le> C

goal (2 subgoals):
 1. bounded {(f ^^ n) basepoint |n. True}
 2. isometry f
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
isometry f
dist basepoint ((f ^^ ?n) basepoint) \<le> C

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

goal (1 subgoal):
 1. xi \<noteq> neutral_fixed_point f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elliptic_isometry f
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f

goal (1 subgoal):
 1. False
[PROOF STEP]
using elliptic_imp_not_parabolic_loxodromic assms
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f
elliptic_isometry ?f \<Longrightarrow> \<not> parabolic_isometry ?f
elliptic_isometry ?f \<Longrightarrow> \<not> loxodromic_isometry ?f
parabolic_isometry f

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xi = neutral_fixed_point f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parabolic_logarithmic_growth:
  assumes "parabolic_isometry (f::'a::Gromov_hyperbolic_space \<Rightarrow> 'a)" "n \<ge> 1"
  shows "dist x ((f^^n) x) \<le> dist x (f x) + 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_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
using dist_le_additive_strength[OF parabolic_isometryD(1)[OF assms(1)] parabolic_fixed_point(2)[OF assms(1)] _ assms(2)]
parabolic_isometryD(3)[OF assms(1)] stable_translation_length_eq_additive_strength[OF parabolic_isometryD(1)[OF assms(1)] parabolic_fixed_point(2)[OF assms(1)]]
[PROOF STATE]
proof (prove)
using this:
0 \<le> additive_strength f (neutral_fixed_point f) \<Longrightarrow> dist ?x ((f ^^ n) ?x) \<le> dist ?x (f ?x) + real n * additive_strength f (neutral_fixed_point f) + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
stable_translation_length f = 0
stable_translation_length f = \<bar>additive_strength f (neutral_fixed_point f)\<bar>

goal (1 subgoal):
 1. dist x ((f ^^ n) x) \<le> dist x (f x) + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)
[PROOF STEP]
by auto


[STATEMENT]
lemma tree_no_parabolic_isometry:
  assumes "isometry (f::'a::Gromov_hyperbolic_space_0 \<Rightarrow> 'a)"
  shows "elliptic_isometry f \<or> loxodromic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elliptic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
have "\<not>parabolic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> parabolic_isometry f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. parabolic_isometry f \<Longrightarrow> False
[PROOF STEP]
assume P: "parabolic_isometry f"
[PROOF STATE]
proof (state)
this:
parabolic_isometry f

goal (1 subgoal):
 1. parabolic_isometry f \<Longrightarrow> False
[PROOF STEP]
have "dist basepoint ((f^^n) basepoint) \<le> dist basepoint (f basepoint)" if "n \<ge> 1" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> dist basepoint (f basepoint)
[PROOF STEP]
using parabolic_logarithmic_growth[OF P that, of basepoint]
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ n) basepoint) \<le> dist basepoint (f basepoint) + real_of_int (\<lceil>log 2 (real n)\<rceil> * 16) * deltaG TYPE('a)

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

goal (1 subgoal):
 1. parabolic_isometry f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ?n \<Longrightarrow> dist basepoint ((f ^^ ?n) basepoint) \<le> dist basepoint (f basepoint)
[PROOF STEP]
have *: "dist basepoint ((f^^n) basepoint) \<le> dist basepoint (f basepoint)" for n
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?n \<Longrightarrow> dist basepoint ((f ^^ ?n) basepoint) \<le> dist basepoint (f basepoint)

goal (1 subgoal):
 1. dist basepoint ((f ^^ n) basepoint) \<le> dist basepoint (f basepoint)
[PROOF STEP]
by (cases "n \<ge> 1", auto simp add: not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
dist basepoint ((f ^^ ?n) basepoint) \<le> dist basepoint (f basepoint)

goal (1 subgoal):
 1. parabolic_isometry f \<Longrightarrow> False
[PROOF STEP]
have "elliptic_isometry f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elliptic_isometry f
[PROOF STEP]
apply (rule elliptic_isometryI[OF _ assms, of basepoint])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {(f ^^ n) basepoint |n. True}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist basepoint ((f ^^ ?n) basepoint) \<le> dist basepoint (f basepoint)

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

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

goal (1 subgoal):
 1. parabolic_isometry f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elliptic_isometry f
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f

goal (1 subgoal):
 1. False
[PROOF STEP]
using elliptic_imp_not_parabolic_loxodromic P
[PROOF STATE]
proof (prove)
using this:
elliptic_isometry f
elliptic_isometry ?f \<Longrightarrow> \<not> parabolic_isometry ?f
elliptic_isometry ?f \<Longrightarrow> \<not> loxodromic_isometry ?f
parabolic_isometry f

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> parabolic_isometry f

goal (1 subgoal):
 1. elliptic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> parabolic_isometry f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> parabolic_isometry f

goal (1 subgoal):
 1. elliptic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
using elliptic_or_parabolic_or_loxodromic[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<not> parabolic_isometry f
elliptic_isometry f \<or> parabolic_isometry f \<or> loxodromic_isometry f

goal (1 subgoal):
 1. elliptic_isometry f \<or> loxodromic_isometry f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elliptic_isometry f \<or> loxodromic_isometry f

goal:
No subgoals!
[PROOF STEP]
qed