[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) geodesic_projection_exp_contracting:
  assumes "geodesic_segment G"
          "\<And>x y. x \<in> {a..b} \<Longrightarrow> y \<in> {a..b} \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C"
          "a \<le> b"
          "pa \<in> proj_set (f a) G"
          "pb \<in> proj_set (f b) G"
          "\<And>t. t \<in> {a..b} \<Longrightarrow> infdist (f t) G \<ge> D"
          "D \<ge> 15/2 * delta + C/2"
          "delta > deltaG(TYPE('a))"
          "C \<ge> 0"
          "lambda \<ge> 0"
  shows "dist pa pb \<le> max (5 * deltaG(TYPE('a))) ((4 * exp(1/2 * ln 2)) * lambda * (b-a) * exp(-(D-C/2) * ln 2 / (5 * delta)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "delta > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < delta
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
a \<le> b
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G
?t \<in> {a..b} \<Longrightarrow> D \<le> infdist (f ?t) G
15 / 2 * delta + C / 2 \<le> D
deltaG TYPE('a) < delta
0 \<le> C
0 \<le> lambda

goal (1 subgoal):
 1. 0 < delta
[PROOF STEP]
using local.delta_nonneg
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
a \<le> b
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G
?t \<in> {a..b} \<Longrightarrow> D \<le> infdist (f ?t) G
15 / 2 * delta + C / 2 \<le> D
deltaG TYPE('a) < delta
0 \<le> C
0 \<le> lambda
0 \<le> deltaG TYPE('a)

goal (1 subgoal):
 1. 0 < delta
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < delta

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "exp(15/2/5 * ln 2) = exp(ln 2) * exp(1/2 * ln (2::real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (15 / 2 / 5 * ln 2) = exp (ln 2) * exp (1 / 2 * ln 2)
[PROOF STEP]
unfolding mult_exp_exp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (15 / 2 / 5 * ln 2) = exp (ln 2 + 1 / 2 * ln 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (15 / 2 / 5 * ln 2) = exp (ln 2) * exp (1 / 2 * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (15 / 2 / 5 * ln 2) = exp (ln 2) * exp (1 / 2 * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = 2 * exp(1/2 * ln 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (ln 2) * exp (1 / 2 * ln 2) = 2 * exp (1 / 2 * ln 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
exp (ln 2) * exp (1 / 2 * ln 2) = 2 * exp (1 / 2 * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
exp (15 / 2 / 5 * ln 2) = 2 * exp (1 / 2 * ln 2)
[PROOF STEP]
have "exp(15/2/5 * ln 2) = 2 * exp(1/2 * ln (2::real))"
[PROOF STATE]
proof (prove)
using this:
exp (15 / 2 / 5 * ln 2) = 2 * exp (1 / 2 * ln 2)

goal (1 subgoal):
 1. exp (15 / 2 / 5 * ln 2) = 2 * exp (1 / 2 * ln 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (15 / 2 / 5 * ln 2) = 2 * exp (1 / 2 * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>The idea of the proof is to start with a sequence of points separated by $10 \delta + C$ along
  the original path, and push them by a fixed distance towards $G$ to bring them at distance at most
  $5 \delta$, thanks to the previous lemma. Then, discard half the points, and start again. This
  is possible while one is far enough from $G$. In the first step of the proof, we formalize this
  in the case where the process can be iterated long enough that, at the end, the projections on $G$
  are very close together. This is a simple induction, based on the previous lemma.\<close>
[PROOF STATE]
proof (state)
this:
exp (15 / 2 / 5 * ln 2) = 2 * exp (1 / 2 * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have Main: "\<And>c g p. (\<forall>i \<in> {0..2^k}. p i \<in> proj_set (g i) G)
            \<Longrightarrow> (\<forall>i \<in> {0..2^k}. dist (p i) (g i) \<ge> 5 * delta * k + 15/2 * delta + c/2)
            \<Longrightarrow> (\<forall>i \<in> {0..<2^k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c)
            \<Longrightarrow> c \<ge> 0
            \<Longrightarrow> dist (p 0) (p (2^k)) \<le> 5 * deltaG(TYPE('a))" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
 2. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c

goal (2 subgoals):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
 2. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c
[PROOF STEP]
have H: "p 0 \<in> proj_set (g 0) G"
                 "p 1 \<in> proj_set (g 1) G"
                 "dist (g 0) (g 1) \<le> 10 * delta + c"
                 "dist (p 0) (g 0) \<ge> 15/2 * delta + c/2"
                 "dist (p 1) (g 1) \<ge> 15/2 * delta + c/2"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c

goal (1 subgoal):
 1. (p 0 \<in> proj_set (g 0) G &&& p 1 \<in> proj_set (g 1) G) &&& dist (g 0) (g 1) \<le> 10 * delta + c &&& 15 / 2 * delta + c / 2 \<le> dist (p 0) (g 0) &&& 15 / 2 * delta + c / 2 \<le> dist (p 1) (g 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p 0 \<in> proj_set (g 0) G
p 1 \<in> proj_set (g 1) G
dist (g 0) (g 1) \<le> 10 * delta + c
15 / 2 * delta + c / 2 \<le> dist (p 0) (g 0)
15 / 2 * delta + c / 2 \<le> dist (p 1) (g 1)

goal (2 subgoals):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
 2. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
have "dist (p 0) (p 1) \<le> max (5 * deltaG(TYPE('a))) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p 1) \<le> max (5 * deltaG TYPE('a)) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a))
[PROOF STEP]
by (rule proj_along_geodesic_contraction[OF \<open>geodesic_segment G\<close> \<open>p 0 \<in> proj_set (g 0) G\<close> \<open>p 1 \<in> proj_set (g 1) G\<close>])
[PROOF STATE]
proof (state)
this:
dist (p 0) (p 1) \<le> max (5 * deltaG TYPE('a)) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a))

goal (2 subgoals):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
 2. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p 0) (p 1) \<le> max (5 * deltaG TYPE('a)) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a))

goal (2 subgoals):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
 2. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
have "... \<le> max (5 * deltaG(TYPE('a))) (5 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (5 * deltaG TYPE('a)) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a)) \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. deltaG TYPE('a) \<le> deltaG TYPE('a)
 2. 0 \<le> 5
 3. dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
using H \<open>delta > deltaG(TYPE('a))\<close>
[PROOF STATE]
proof (prove)
using this:
p 0 \<in> proj_set (g 0) G
p 1 \<in> proj_set (g 1) G
dist (g 0) (g 1) \<le> 10 * delta + c
15 / 2 * delta + c / 2 \<le> dist (p 0) (g 0)
15 / 2 * delta + c / 2 \<le> dist (p 1) (g 1)
deltaG TYPE('a) < delta

goal (3 subgoals):
 1. deltaG TYPE('a) \<le> deltaG TYPE('a)
 2. 0 \<le> 5
 3. dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (5 * deltaG TYPE('a)) (dist (g 0) (g 1) - dist (p 0) (g 0) - dist (p 1) (g 1) + 10 * deltaG TYPE('a)) \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))

goal (2 subgoals):
 1. \<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ 0}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ 0}. 5 * delta * real 0 + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ 0}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
 2. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (p 0) (p 1) \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))
[PROOF STEP]
show "dist (p 0) (p (2^0)) \<le> 5 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
dist (p 0) (p 1) \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ 0)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>i\<in>{0..2 ^ k}. ?p i \<in> proj_set (?g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + ?c / 2 \<le> dist (?p i) (?g i); \<forall>i\<in>{0..<2 ^ k}. dist (?g i) (?g (Suc i)) \<le> 10 * delta + ?c; 0 \<le> ?c\<rbrakk> \<Longrightarrow> dist (?p 0) (?p (2 ^ k)) \<le> 5 * deltaG TYPE('a)
\<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
have *: "5 * delta * real (k + 1) + 5 * delta = 5 * delta * real (Suc k + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real (k + 1) + 5 * delta = 5 * delta * real (Suc k + 1)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
5 * delta * real (k + 1) + 5 * delta = 5 * delta * real (Suc k + 1)

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
define h where "h = (\<lambda>i. geodesic_segment_param {p i--g i} (p i) (5 * delta * k + 15/2 * delta))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>i. geodesic_segment_param {p i--g i} (p i) (5 * delta * real k + 15 / 2 * delta))

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
have h_dist: "dist (h i) (h (Suc i)) \<le> 5 * delta" if "i \<in> {0..<2^(Suc k)}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (h i) (h (Suc i)) \<le> 5 * delta
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param {p i--g i} (p i) (5 * delta * real k + 15 / 2 * delta)) (geodesic_segment_param {p (Suc i)--g (Suc i)} (p (Suc i)) (5 * delta * real k + 15 / 2 * delta)) \<le> 5 * delta
[PROOF STEP]
apply (rule geodesic_projection_exp_contracting_aux[OF \<open>geodesic_segment G\<close> _ _ less_imp_le[OF \<open>delta > deltaG(TYPE('a))\<close>]])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. p i \<in> proj_set (g i) G
 2. p (Suc i) \<in> proj_set (g (Suc i)) G
 3. dist (g i) (g (Suc i)) \<le> 10 * delta + ?C
 4. 15 / 2 * delta \<le> 5 * delta * real k + 15 / 2 * delta
 5. 5 * delta * real k + 15 / 2 * delta + 5 * delta + ?C / 2 \<le> dist (p i) (g i)
 6. 5 * delta * real k + 15 / 2 * delta + 5 * delta + ?C / 2 \<le> dist (p (Suc i)) (g (Suc i))
 7. 0 \<le> ?C
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. p i \<in> proj_set (g i) G
 2. p (Suc i) \<in> proj_set (g (Suc i)) G
 3. dist (g i) (g (Suc i)) \<le> 10 * delta + ?C
 4. 15 / 2 * delta \<le> 5 * delta * real k + 15 / 2 * delta
 5. 5 * delta * real k + 15 / 2 * delta + 5 * delta + ?C / 2 \<le> dist (p i) (g i)
 6. 5 * delta * real k + 15 / 2 * delta + 5 * delta + ?C / 2 \<le> dist (p (Suc i)) (g (Suc i))
 7. 0 \<le> ?C
[PROOF STEP]
using Suc.prems that \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c
i \<in> {0..<2 ^ Suc k}
0 < delta

goal (7 subgoals):
 1. p i \<in> proj_set (g i) G
 2. p (Suc i) \<in> proj_set (g (Suc i)) G
 3. dist (g i) (g (Suc i)) \<le> 10 * delta + ?C
 4. 15 / 2 * delta \<le> 5 * delta * real k + 15 / 2 * delta
 5. 5 * delta * real k + 15 / 2 * delta + 5 * delta + ?C / 2 \<le> dist (p i) (g i)
 6. 5 * delta * real k + 15 / 2 * delta + 5 * delta + ?C / 2 \<le> dist (p (Suc i)) (g (Suc i))
 7. 0 \<le> ?C
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
?i \<in> {0..<2 ^ Suc k} \<Longrightarrow> dist (h ?i) (h (Suc ?i)) \<le> 5 * delta

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
define g' where "g' = (\<lambda>i. h (2 * i))"
[PROOF STATE]
proof (state)
this:
g' = (\<lambda>i. h (2 * i))

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
define p' where "p' = (\<lambda>i. p (2 * i))"
[PROOF STATE]
proof (state)
this:
p' = (\<lambda>i. p (2 * i))

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
have "dist (p' 0) (p' (2^k)) \<le> 5 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
proof (rule Suc.IH[where ?g = g' and ?c = 0])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. p' i \<in> proj_set (g' i) G
 2. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
 3. \<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
 4. 0 \<le> 0
[PROOF STEP]
show "\<forall>i\<in>{0..2 ^ k}. p' i \<in> proj_set (g' i) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{0..2 ^ k}. p' i \<in> proj_set (g' i) G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> p' i \<in> proj_set (g' i) G
[PROOF STEP]
fix i::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> p' i \<in> proj_set (g' i) G
[PROOF STEP]
assume "i \<in> {0..2^k}"
[PROOF STATE]
proof (state)
this:
i \<in> {0..2 ^ k}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> p' i \<in> proj_set (g' i) G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> {0..2 ^ k}
[PROOF STEP]
have *: "2 * i \<in> {0..2^(Suc k)}"
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ k}

goal (1 subgoal):
 1. 2 * i \<in> {0..2 ^ Suc k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * i \<in> {0..2 ^ Suc k}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> p' i \<in> proj_set (g' i) G
[PROOF STEP]
show "p' i \<in> proj_set (g' i) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' i \<in> proj_set (g' i) G
[PROOF STEP]
unfolding p'_def g'_def h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p (2 * i) \<in> proj_set (geodesic_segment_param {p (2 * i)--g (2 * i)} (p (2 * i)) (5 * delta * real k + 15 / 2 * delta)) G
[PROOF STEP]
apply (rule proj_set_geodesic_same_basepoint[of _ "g (2 * i)" _ "{p(2 * i)--g(2 * i)}"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. p (2 * i) \<in> proj_set (g (2 * i)) G
 2. geodesic_segment_between {p (2 * i)--g (2 * i)} (p (2 * i)) (g (2 * i))
 3. geodesic_segment_param {p (2 * i)--g (2 * i)} (p (2 * i)) (5 * delta * real k + 15 / 2 * delta) \<in> {p (2 * i)--g (2 * i)}
[PROOF STEP]
using Suc *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i\<in>{0..2 ^ k}. ?p i \<in> proj_set (?g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + ?c / 2 \<le> dist (?p i) (?g i); \<forall>i\<in>{0..<2 ^ k}. dist (?g i) (?g (Suc i)) \<le> 10 * delta + ?c; 0 \<le> ?c\<rbrakk> \<Longrightarrow> dist (?p 0) (?p (2 ^ k)) \<le> 5 * deltaG TYPE('a)
\<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c
2 * i \<in> {0..2 ^ Suc k}

goal (3 subgoals):
 1. p (2 * i) \<in> proj_set (g (2 * i)) G
 2. geodesic_segment_between {p (2 * i)--g (2 * i)} (p (2 * i)) (g (2 * i))
 3. geodesic_segment_param {p (2 * i)--g (2 * i)} (p (2 * i)) (5 * delta * real k + 15 / 2 * delta) \<in> {p (2 * i)--g (2 * i)}
[PROOF STEP]
by (auto simp add: geodesic_segment_param_in_segment)
[PROOF STATE]
proof (state)
this:
p' i \<in> proj_set (g' i) G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..2 ^ k}. p' i \<in> proj_set (g' i) G

goal (3 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
 2. \<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
 3. 0 \<le> 0
[PROOF STEP]
show "\<forall>i\<in>{0..2 ^ k}. 5 * delta * k + 15/2 * delta + 0/2 \<le> dist (p' i) (g' i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
fix i::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
assume "i \<in> {0..2^k}"
[PROOF STATE]
proof (state)
this:
i \<in> {0..2 ^ k}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> {0..2 ^ k}
[PROOF STEP]
have *: "2 * i \<in> {0..2^(Suc k)}"
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ k}

goal (1 subgoal):
 1. 2 * i \<in> {0..2 ^ Suc k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * i \<in> {0..2 ^ Suc k}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
have "5 * delta * k + 15/2 * delta \<le> 5 * delta * Suc k + 15/2 * delta + c/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta \<le> 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2
[PROOF STEP]
using \<open>delta > 0\<close> \<open>c \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < delta
0 \<le> c

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta \<le> 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta \<le> 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta \<le> 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
have "... \<le> dist (p (2 * i)) (g (2 * i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p (2 * i)) (g (2 * i))
[PROOF STEP]
using Suc *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i\<in>{0..2 ^ k}. ?p i \<in> proj_set (?g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + ?c / 2 \<le> dist (?p i) (?g i); \<forall>i\<in>{0..<2 ^ k}. dist (?g i) (?g (Suc i)) \<le> 10 * delta + ?c; 0 \<le> ?c\<rbrakk> \<Longrightarrow> dist (?p 0) (?p (2 ^ k)) \<le> 5 * deltaG TYPE('a)
\<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G
\<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i)
\<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c
0 \<le> c
2 * i \<in> {0..2 ^ Suc k}

goal (1 subgoal):
 1. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p (2 * i)) (g (2 * i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p (2 * i)) (g (2 * i))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
5 * delta * real k + 15 / 2 * delta \<le> dist (p (2 * i)) (g (2 * i))
[PROOF STEP]
have *: "5 * delta * k + 15/2 * delta \<le> dist (p (2 * i)) (g (2 * i))"
[PROOF STATE]
proof (prove)
using this:
5 * delta * real k + 15 / 2 * delta \<le> dist (p (2 * i)) (g (2 * i))

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta \<le> dist (p (2 * i)) (g (2 * i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta \<le> dist (p (2 * i)) (g (2 * i))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
have "dist (p' i) (g' i) = 5 * delta * k + 15/2 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p' i) (g' i) = 5 * delta * real k + 15 / 2 * delta
[PROOF STEP]
unfolding p'_def g'_def h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p (2 * i)) (geodesic_segment_param {p (2 * i)--g (2 * i)} (p (2 * i)) (5 * delta * real k + 15 / 2 * delta)) = 5 * delta * real k + 15 / 2 * delta
[PROOF STEP]
apply (rule geodesic_segment_param_in_geodesic_spaces(6))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta \<in> {0..dist (p (2 * i)) (g (2 * i))}
[PROOF STEP]
using * \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
5 * delta * real k + 15 / 2 * delta \<le> dist (p (2 * i)) (g (2 * i))
0 < delta

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta \<in> {0..dist (p (2 * i)) (g (2 * i))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p' i) (g' i) = 5 * delta * real k + 15 / 2 * delta

goal (1 subgoal):
 1. \<And>i. i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (p' i) (g' i) = 5 * delta * real k + 15 / 2 * delta
[PROOF STEP]
show "5 * delta * k + 15/2 * delta + 0/2 \<le> dist (p' i) (g' i)"
[PROOF STATE]
proof (prove)
using this:
dist (p' i) (g' i) = 5 * delta * real k + 15 / 2 * delta

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + 0 / 2 \<le> dist (p' i) (g' i)

goal (2 subgoals):
 1. \<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
 2. 0 \<le> 0
[PROOF STEP]
show "\<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
fix i::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
assume *: "i \<in> {0..<2 ^ k}"
[PROOF STATE]
proof (state)
this:
i \<in> {0..<2 ^ k}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
have "dist (g' i) (g' (Suc i)) = dist (h (2 * i)) (h (Suc (Suc (2 * i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g' i) (g' (Suc i)) = dist (h (2 * i)) (h (Suc (Suc (2 * i))))
[PROOF STEP]
unfolding g'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (h (2 * i)) (h (2 * Suc i)) = dist (h (2 * i)) (h (Suc (Suc (2 * i))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (g' i) (g' (Suc i)) = dist (h (2 * i)) (h (Suc (Suc (2 * i))))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (g' i) (g' (Suc i)) = dist (h (2 * i)) (h (Suc (Suc (2 * i))))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
have "... \<le> dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (h (2 * i)) (h (Suc (Suc (2 * i)))) \<le> dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i))))
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (h (2 * i)) (h (Suc (Suc (2 * i)))) \<le> dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i))))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (h (2 * i)) (h (Suc (Suc (2 * i)))) \<le> dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i))))

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
have "... \<le> 5 * delta + 5 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i)))) \<le> 5 * delta + 5 * delta
[PROOF STEP]
apply (intro mono_intros h_dist)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 2 * i \<in> {0..<2 ^ Suc k}
 2. Suc (2 * i) \<in> {0..<2 ^ Suc k}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<2 ^ k}

goal (2 subgoals):
 1. 2 * i \<in> {0..<2 ^ Suc k}
 2. Suc (2 * i) \<in> {0..<2 ^ Suc k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (h (2 * i)) (h (Suc (2 * i))) + dist (h (Suc (2 * i))) (h (Suc (Suc (2 * i)))) \<le> 5 * delta + 5 * delta

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (g' i) (g' (Suc i)) \<le> 5 * delta + 5 * delta
[PROOF STEP]
show "dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0"
[PROOF STATE]
proof (prove)
using this:
dist (g' i) (g' (Suc i)) \<le> 5 * delta + 5 * delta

goal (1 subgoal):
 1. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + 0

goal (1 subgoal):
 1. 0 \<le> 0
[PROOF STEP]
qed (simp)
[PROOF STATE]
proof (state)
this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>k c g p. \<lbrakk>\<And>c g p. \<lbrakk>\<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a); \<forall>i\<in>{0..2 ^ Suc k}. p i \<in> proj_set (g i) G; \<forall>i\<in>{0..2 ^ Suc k}. 5 * delta * real (Suc k) + 15 / 2 * delta + c / 2 \<le> dist (p i) (g i); \<forall>i\<in>{0..<2 ^ Suc k}. dist (g i) (g (Suc i)) \<le> 10 * delta + c; 0 \<le> c\<rbrakk> \<Longrightarrow> dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
show "dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
unfolding p'_def
[PROOF STATE]
proof (prove)
using this:
dist (p (2 * 0)) (p (2 * 2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ Suc k)) \<le> 5 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>i\<in>{0..2 ^ ?k1}. ?p i \<in> proj_set (?g i) G; \<forall>i\<in>{0..2 ^ ?k1}. 5 * delta * real ?k1 + 15 / 2 * delta + ?c / 2 \<le> dist (?p i) (?g i); \<forall>i\<in>{0..<2 ^ ?k1}. dist (?g i) (?g (Suc i)) \<le> 10 * delta + ?c; 0 \<le> ?c\<rbrakk> \<Longrightarrow> dist (?p 0) (?p (2 ^ ?k1)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>Now, we will apply the previous basic statement to points along our original path. We
  introduce $k$, the number of steps for which the pushing process can be done -- it only depends on
  the original distance $D$ to $G$. \<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>i\<in>{0..2 ^ ?k1}. ?p i \<in> proj_set (?g i) G; \<forall>i\<in>{0..2 ^ ?k1}. 5 * delta * real ?k1 + 15 / 2 * delta + ?c / 2 \<le> dist (?p i) (?g i); \<forall>i\<in>{0..<2 ^ ?k1}. dist (?g i) (?g (Suc i)) \<le> 10 * delta + ?c; 0 \<le> ?c\<rbrakk> \<Longrightarrow> dist (?p 0) (?p (2 ^ ?k1)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define k where "k = nat(floor((D - C/2 - 15/2 * delta)/(5 * delta)))"
[PROOF STATE]
proof (state)
this:
k = nat \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "int k = floor((D - C/2 - 15/2 * delta)/(5 * delta))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int k = \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (nat \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>) = \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>
[PROOF STEP]
apply (rule nat_0_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>
[PROOF STEP]
using \<open>D \<ge> 15/2 * delta + C/2\<close> \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
15 / 2 * delta + C / 2 \<le> D
0 < delta

goal (1 subgoal):
 1. 0 \<le> \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int k = \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int k = \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>
[PROOF STEP]
have "k \<le> (D - C/2 - 15/2 * delta)/(5 * delta)" "(D - C/2 - 15/2 * delta)/(5 * delta) \<le> k + 1"
[PROOF STATE]
proof (prove)
using this:
int k = \<lfloor>(D - C / 2 - 15 / 2 * delta) / (5 * delta)\<rfloor>

goal (1 subgoal):
 1. real k \<le> (D - C / 2 - 15 / 2 * delta) / (5 * delta) &&& (D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
real k \<le> (D - C / 2 - 15 / 2 * delta) / (5 * delta)
(D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real k \<le> (D - C / 2 - 15 / 2 * delta) / (5 * delta)
(D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)
[PROOF STEP]
have k: "D \<ge> 5 * delta * k + 15/2 * delta + C/2" "D \<le> 5 * delta * (k+1) + 15/2 * delta + C/2"
[PROOF STATE]
proof (prove)
using this:
real k \<le> (D - C / 2 - 15 / 2 * delta) / (5 * delta)
(D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D &&& D \<le> 5 * delta * real (k + 1) + 15 / 2 * delta + C / 2
[PROOF STEP]
using \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
real k \<le> (D - C / 2 - 15 / 2 * delta) / (5 * delta)
(D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)
0 < delta

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D &&& D \<le> 5 * delta * real (k + 1) + 15 / 2 * delta + C / 2
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D
D \<le> 5 * delta * real (k + 1) + 15 / 2 * delta + C / 2

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "exp((D-C/2)/(5 * delta) * ln 2) * exp(-15/2/5 * ln 2) = exp(((D-C/2-15/2 * delta)/(5 * delta)) * ln 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp ((D - C / 2) / (5 * delta) * ln 2) * exp (- 15 / 2 / 5 * ln 2) = exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2)
[PROOF STEP]
unfolding mult_exp_exp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp ((D - C / 2) / (5 * delta) * ln 2 + - 15 / 2 / 5 * ln 2) = exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2)
[PROOF STEP]
using \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < delta

goal (1 subgoal):
 1. exp ((D - C / 2) / (5 * delta) * ln 2 + - 15 / 2 / 5 * ln 2) = exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2)
[PROOF STEP]
by (simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
exp ((D - C / 2) / (5 * delta) * ln 2) * exp (- 15 / 2 / 5 * ln 2) = exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp ((D - C / 2) / (5 * delta) * ln 2) * exp (- 15 / 2 / 5 * ln 2) = exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... \<le> exp((k+1) * ln 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2) \<le> exp (real (k + 1) * ln 2)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)
 2. 1 \<le> 2
[PROOF STEP]
using k(2) \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
D \<le> 5 * delta * real (k + 1) + 15 / 2 * delta + C / 2
0 < delta

goal (2 subgoals):
 1. (D - C / 2 - 15 / 2 * delta) / (5 * delta) \<le> real (k + 1)
 2. 1 \<le> 2
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2) \<le> exp (real (k + 1) * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp ((D - C / 2 - 15 / 2 * delta) / (5 * delta) * ln 2) \<le> exp (real (k + 1) * ln 2)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = 2^(k+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (real (k + 1) * ln 2) = 2 ^ (k + 1)
[PROOF STEP]
by (subst powr_realpow[symmetric], auto simp add: powr_def)
[PROOF STATE]
proof (state)
this:
exp (real (k + 1) * ln 2) = 2 ^ (k + 1)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (real (k + 1) * ln 2) = 2 ^ (k + 1)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = 2 * 2^k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k + 1) = 2 * 2 ^ k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ (k + 1) = 2 * 2 ^ k

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
exp ((D - C / 2) / (5 * delta) * ln 2) * exp (- 15 / 2 / 5 * ln 2) \<le> 2 * 2 ^ k
[PROOF STEP]
have k': "1/2^k \<le> 2 * exp(15/2/5 * ln 2) * exp(- ((D-C/2) * ln 2 / (5 * delta)))"
[PROOF STATE]
proof (prove)
using this:
exp ((D - C / 2) / (5 * delta) * ln 2) * exp (- 15 / 2 / 5 * ln 2) \<le> 2 * 2 ^ k

goal (1 subgoal):
 1. 1 / 2 ^ k \<le> 2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps exp_minus)
[PROOF STATE]
proof (state)
this:
1 / 2 ^ k \<le> 2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>We separate the proof into two cases. If the path is not too long, then it can be covered by
  $2^k$ points at distance at most $10 \delta + C$. By the basic statement, it follows that the diameter
  of the projection is at most $5 \delta$. Otherwise, we subdivide the path into $2^N$ points at
  distance at most $10 \delta + C$, with $N \geq k$, and apply the basic statement to blocks of $2^k$
  consecutive points. It follows that the projections of $g_0, g_{2^k}, g_{2\cdot 2^k},\dotsc$ are
  at distances at most $5 \delta$. Hence, the first and last projections are at distance at most
  $2^{N-k} \cdot 5 \delta$, which is the desired bound.\<close>
[PROOF STATE]
proof (state)
this:
1 / 2 ^ k \<le> 2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
proof (cases "lambda * (b-a) \<le> 10 * delta * 2^k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>First, treat the case where the path is rather short.\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lambda * (b - a) \<le> 10 * delta * 2 ^ k

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define g::"nat \<Rightarrow> 'a" where "g = (\<lambda>i. f(a + (b-a) * i/2^k))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. f (a + (b - a) * real x / 2 ^ k))

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "g 0 = f a" "g(2^k) = f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g 0 = f a &&& g (2 ^ k) = f b
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a + (b - a) * real 0 / 2 ^ k) = f a &&& f (a + (b - a) * real (2 ^ k) / 2 ^ k) = f b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g 0 = f a
g (2 ^ k) = f b

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have *: "a + (b-a) * i/2^k \<in> {a..b}" if "i \<in> {0..2^k}" for i::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
have "a + (b - a) * (real i / 2 ^ k) \<le> a + (b-a) * (2^k/2^k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (b - a) * (real i / 2 ^ k) \<le> a + (b - a) * (2 ^ k / 2 ^ k)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. real i \<le> 2 ^ k
 2. 0 \<le> 2 ^ k
 3. 0 \<le> b - a
[PROOF STEP]
using that \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ k}
a \<le> b

goal (3 subgoals):
 1. real i \<le> 2 ^ k
 2. 0 \<le> 2 ^ k
 3. 0 \<le> b - a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + (b - a) * (real i / 2 ^ k) \<le> a + (b - a) * (2 ^ k / 2 ^ k)

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a + (b - a) * (real i / 2 ^ k) \<le> a + (b - a) * (2 ^ k / 2 ^ k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a + (b - a) * (real i / 2 ^ k) \<le> a + (b - a) * (2 ^ k / 2 ^ k)

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
using \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
a + (b - a) * (real i / 2 ^ k) \<le> a + (b - a) * (2 ^ k / 2 ^ k)
a \<le> b

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + (b - a) * real i / 2 ^ k \<in> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ k} \<Longrightarrow> a + (b - a) * real ?i / 2 ^ k \<in> {a..b}

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have A: "dist (g i) (g (Suc i)) \<le> 10 * delta + C" if "i \<in> {0..<2^k}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
have "dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b-a) * i/2^k) (a + (b-a) * (Suc i)/2^k) + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f (a + (b - a) * real i / 2 ^ k)) (f (a + (b - a) * real (Suc i) / 2 ^ k)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C
[PROOF STEP]
apply (intro assms(2) *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i \<in> {0..2 ^ k}
 2. Suc i \<in> {0..2 ^ k}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<2 ^ k}

goal (2 subgoals):
 1. i \<in> {0..2 ^ k}
 2. Suc i \<in> {0..2 ^ k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
have "... = lambda * (b-a)/2^k + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C = lambda * (b - a) / 2 ^ k + C
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * \<bar>a + (b - a) * real i / 2 ^ k - (a + (b - a) * real (Suc i) / 2 ^ k)\<bar> + C = lambda * (b - a) / 2 ^ k + C
[PROOF STEP]
using \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. lambda * \<bar>a + (b - a) * real i / 2 ^ k - (a + (b - a) * real (Suc i) / 2 ^ k)\<bar> + C = lambda * (b - a) / 2 ^ k + C
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C = lambda * (b - a) / 2 ^ k + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lambda * dist (a + (b - a) * real i / 2 ^ k) (a + (b - a) * real (Suc i) / 2 ^ k) + C = lambda * (b - a) / 2 ^ k + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
have "... \<le> 10 * delta + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (b - a) / 2 ^ k + C \<le> 10 * delta + C
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
lambda * (b - a) \<le> 10 * delta * 2 ^ k

goal (1 subgoal):
 1. lambda * (b - a) / 2 ^ k + C \<le> 10 * delta + C
[PROOF STEP]
by (simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
lambda * (b - a) / 2 ^ k + C \<le> 10 * delta + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (g i) (g (Suc i)) \<le> 10 * delta + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (g i) (g (Suc i)) \<le> 10 * delta + C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g ?i) (g (Suc ?i)) \<le> 10 * delta + C

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define p where "p = (\<lambda>i. if i = 0 then pa else if i = 2^k then pb else SOME p. p \<in> proj_set (g i) G)"
[PROOF STATE]
proof (state)
this:
p = (\<lambda>i. if i = 0 then pa else if i = 2 ^ k then pb else SOME p. p \<in> proj_set (g i) G)

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have B: "p i \<in> proj_set (g i) G" if "i \<in> {0..2^k}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
proof (cases "i = 0 \<or> i = 2^k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<or> i = 2 ^ k \<Longrightarrow> p i \<in> proj_set (g i) G
 2. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 0 \<or> i = 2 ^ k

goal (2 subgoals):
 1. i = 0 \<or> i = 2 ^ k \<Longrightarrow> p i \<in> proj_set (g i) G
 2. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0 \<or> i = 2 ^ k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0 \<or> i = 2 ^ k

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
using \<open>pa \<in> proj_set (f a) G\<close> \<open>pb \<in> proj_set (f b) G\<close>
[PROOF STATE]
proof (prove)
using this:
i = 0 \<or> i = 2 ^ k
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
unfolding p_def g_def
[PROOF STATE]
proof (prove)
using this:
i = 0 \<or> i = 2 ^ k
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G

goal (1 subgoal):
 1. (if i = 0 then pa else if i = 2 ^ k then pb else SOME p. p \<in> proj_set (f (a + (b - a) * real i / 2 ^ k)) G) \<in> proj_set (f (a + (b - a) * real i / 2 ^ k)) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p i \<in> proj_set (g i) G

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (i = 0 \<or> i = 2 ^ k)

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (i = 0 \<or> i = 2 ^ k)
[PROOF STEP]
have "p i = (SOME p. p \<in> proj_set (g i) G)"
[PROOF STATE]
proof (prove)
using this:
\<not> (i = 0 \<or> i = 2 ^ k)

goal (1 subgoal):
 1. p i = (SOME p. p \<in> proj_set (g i) G)
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
\<not> (i = 0 \<or> i = 2 ^ k)

goal (1 subgoal):
 1. (if i = 0 then pa else if i = 2 ^ k then pb else SOME p. p \<in> proj_set (g i) G) = (SOME p. p \<in> proj_set (g i) G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p i = (SOME p. p \<in> proj_set (g i) G)

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p i = (SOME p. p \<in> proj_set (g i) G)

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
have "proj_set (g i) G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj_set (g i) G \<noteq> {}
[PROOF STEP]
apply (rule proj_set_nonempty_of_proper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
using geodesic_segment_topology[OF \<open>geodesic_segment G\<close>]
[PROOF STATE]
proof (prove)
using this:
compact G
connected G
path_connected G
bounded G
closed G
G \<noteq> {}
proper G

goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj_set (g i) G \<noteq> {}

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ k) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p i = (SOME p. p \<in> proj_set (g i) G)
proj_set (g i) G \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p i = (SOME p. p \<in> proj_set (g i) G)
proj_set (g i) G \<noteq> {}

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
using some_in_eq
[PROOF STATE]
proof (prove)
using this:
p i = (SOME p. p \<in> proj_set (g i) G)
proj_set (g i) G \<noteq> {}
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p i \<in> proj_set (g i) G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ k} \<Longrightarrow> p ?i \<in> proj_set (g ?i) G

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have C: "dist (p i) (g i) \<ge> 5 * delta * k + 15/2 * delta + C/2" if "i \<in> {0..2^k}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
have "5 * delta * k + 15/2 * delta + C/2 \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D
[PROOF STEP]
using k(1)
[PROOF STATE]
proof (prove)
using this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
have "... \<le> infdist (g i) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<le> infdist (g i) G
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<le> infdist (f (a + (b - a) * real i / 2 ^ k)) G
[PROOF STEP]
apply (rule \<open>\<And>t. t \<in> {a..b} \<Longrightarrow> infdist (f t) G \<ge> D\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
using * that
[PROOF STATE]
proof (prove)
using this:
?i \<in> {0..2 ^ k} \<Longrightarrow> a + (b - a) * real ?i / 2 ^ k \<in> {a..b}
i \<in> {0..2 ^ k}

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ k \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<le> infdist (g i) G

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D \<le> infdist (g i) G

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
have "... = dist (p i) (g i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (g i) G = dist (p i) (g i)
[PROOF STEP]
using that proj_setD(2)[OF B[OF that]]
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ k}
dist (g i) (p i) = infdist (g i) G

goal (1 subgoal):
 1. infdist (g i) G = dist (p i) (g i)
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
infdist (g i) G = dist (p i) (g i)

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p ?i) (g ?i)

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "dist (p 0) (p (2^k)) \<le> 5 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
apply (rule Main[where ?g = g and ?c = C])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G
 2. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
 3. \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + C
 4. 0 \<le> C
[PROOF STEP]
using A B C \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
?i \<in> {0..<2 ^ k} \<Longrightarrow> dist (g ?i) (g (Suc ?i)) \<le> 10 * delta + C
?i \<in> {0..2 ^ k} \<Longrightarrow> p ?i \<in> proj_set (g ?i) G
?i \<in> {0..2 ^ k} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p ?i) (g ?i)
0 \<le> C

goal (4 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. p i \<in> proj_set (g i) G
 2. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
 3. \<forall>i\<in>{0..<2 ^ k}. dist (g i) (g (Suc i)) \<le> 10 * delta + C
 4. 0 \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (2 subgoals):
 1. lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
 2. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (p 0) (p (2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
dist (if 0 = 0 then pa else if 0 = 2 ^ k then pb else SOME p. p \<in> proj_set (g 0) G) (if 2 ^ k = 0 then pa else if 2 ^ k = 2 ^ k then pb else SOME p. p \<in> proj_set (g (2 ^ k)) G) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>Now, the case where the path is long. We introduce $N$ such that it is roughly of length
    $2^N \cdot 10 \delta$.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have *: "10 * delta * 2^k \<le> lambda * (b-a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 10 * delta * 2 ^ k \<le> lambda * (b - a)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k

goal (1 subgoal):
 1. 10 * delta * 2 ^ k \<le> lambda * (b - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
10 * delta * 2 ^ k \<le> lambda * (b - a)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "lambda * (b-a) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < lambda * (b - a)
[PROOF STEP]
using \<open>delta > 0\<close> False \<open>0 \<le> lambda\<close> assms(3) less_eq_real_def mult_le_0_iff
[PROOF STATE]
proof (prove)
using this:
0 < delta
\<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k
0 \<le> lambda
a \<le> b
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
(?a * ?b \<le> (0::?'a)) = ((0::?'a) \<le> ?a \<and> ?b \<le> (0::?'a) \<or> ?a \<le> (0::?'a) \<and> (0::?'a) \<le> ?b)

goal (1 subgoal):
 1. 0 < lambda * (b - a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < lambda * (b - a)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < lambda * (b - a)
[PROOF STEP]
have "a < b" "lambda > 0"
[PROOF STATE]
proof (prove)
using this:
0 < lambda * (b - a)

goal (1 subgoal):
 1. a < b &&& 0 < lambda
[PROOF STEP]
using \<open>a \<le> b\<close> \<open>lambda \<ge> 0\<close> less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
0 < lambda * (b - a)
a \<le> b
0 \<le> lambda
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

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

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define n where "n = nat(floor(log 2 (lambda * (b-a)/(10 * delta))))"
[PROOF STATE]
proof (state)
this:
n = nat \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "log 2 (lambda * (b-a)/(10 * delta)) \<ge> log 2 (2^k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (2 ^ k) \<le> log 2 (lambda * (b - a) / (10 * delta))
[PROOF STEP]
apply (subst log_le_cancel_iff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. 1 < 2
 2. 0 < 2 ^ k
 3. 0 < lambda * (b - a) / (10 * delta)
 4. 2 ^ k \<le> lambda * (b - a) / (10 * delta)
[PROOF STEP]
using * \<open>delta > 0\<close> \<open>a < b\<close> \<open>lambda > 0\<close>
[PROOF STATE]
proof (prove)
using this:
10 * delta * 2 ^ k \<le> lambda * (b - a)
0 < delta
a < b
0 < lambda

goal (4 subgoals):
 1. 1 < 2
 2. 0 < 2 ^ k
 3. 0 < lambda * (b - a) / (10 * delta)
 4. 2 ^ k \<le> lambda * (b - a) / (10 * delta)
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
log 2 (2 ^ k) \<le> log 2 (lambda * (b - a) / (10 * delta))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
log 2 (2 ^ k) \<le> log 2 (lambda * (b - a) / (10 * delta))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "log 2 (2^k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (2 ^ k) = real k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
log 2 (2 ^ k) = real k

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
log 2 (2 ^ k) \<le> log 2 (lambda * (b - a) / (10 * delta))
log 2 (2 ^ k) = real k
[PROOF STEP]
have A: "log 2 (lambda * (b-a)/(10 * delta)) \<ge> k"
[PROOF STATE]
proof (prove)
using this:
log 2 (2 ^ k) \<le> log 2 (lambda * (b - a) / (10 * delta))
log 2 (2 ^ k) = real k

goal (1 subgoal):
 1. real k \<le> log 2 (lambda * (b - a) / (10 * delta))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real k \<le> log 2 (lambda * (b - a) / (10 * delta))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have **: "int n = floor(log 2 (lambda * (b-a)/(10 * delta)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>
[PROOF STEP]
unfolding n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (nat \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>) = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>
[PROOF STEP]
apply (rule nat_0_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
real k \<le> log 2 (lambda * (b - a) / (10 * delta))

goal (1 subgoal):
 1. 0 \<le> \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>
[PROOF STEP]
have "log 2 (2^n) \<le> log 2 (lambda * (b-a)/(10 * delta))"
[PROOF STATE]
proof (prove)
using this:
int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>

goal (1 subgoal):
 1. log 2 (2 ^ n) \<le> log 2 (lambda * (b - a) / (10 * delta))
[PROOF STEP]
apply (subst log_nat_power, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor> \<Longrightarrow> real n \<le> log 2 (lambda * (b - a) / (10 * delta))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
log 2 (2 ^ n) \<le> log 2 (lambda * (b - a) / (10 * delta))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
log 2 (2 ^ n) \<le> log 2 (lambda * (b - a) / (10 * delta))
[PROOF STEP]
have I: "2^n \<le> lambda * (b-a)/(10 * delta)"
[PROOF STATE]
proof (prove)
using this:
log 2 (2 ^ n) \<le> log 2 (lambda * (b - a) / (10 * delta))

goal (1 subgoal):
 1. 2 ^ n \<le> lambda * (b - a) / (10 * delta)
[PROOF STEP]
using \<open>0 < lambda * (b - a)\<close> \<open>0 < delta\<close>
[PROOF STATE]
proof (prove)
using this:
log 2 (2 ^ n) \<le> log 2 (lambda * (b - a) / (10 * delta))
0 < lambda * (b - a)
0 < delta

goal (1 subgoal):
 1. 2 ^ n \<le> lambda * (b - a) / (10 * delta)
[PROOF STEP]
by (simp add: le_log_iff powr_realpow)
[PROOF STATE]
proof (state)
this:
2 ^ n \<le> lambda * (b - a) / (10 * delta)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "log 2 (lambda * (b-a)/(10 * delta)) \<le> log 2 (2^(n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (lambda * (b - a) / (10 * delta)) \<le> log 2 (2 ^ (n + 1))
[PROOF STEP]
apply (subst log_nat_power, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (lambda * (b - a) / (10 * delta)) \<le> 1 + real n
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>

goal (1 subgoal):
 1. log 2 (lambda * (b - a) / (10 * delta)) \<le> 1 + real n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
log 2 (lambda * (b - a) / (10 * delta)) \<le> log 2 (2 ^ (n + 1))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
log 2 (lambda * (b - a) / (10 * delta)) \<le> log 2 (2 ^ (n + 1))
[PROOF STEP]
have J: "lambda * (b-a)/(10 * delta) \<le> 2^(n+1)"
[PROOF STATE]
proof (prove)
using this:
log 2 (lambda * (b - a) / (10 * delta)) \<le> log 2 (2 ^ (n + 1))

goal (1 subgoal):
 1. lambda * (b - a) / (10 * delta) \<le> 2 ^ (n + 1)
[PROOF STEP]
using \<open>0 < lambda * (b - a)\<close> \<open>0 < delta\<close>
[PROOF STATE]
proof (prove)
using this:
log 2 (lambda * (b - a) / (10 * delta)) \<le> log 2 (2 ^ (n + 1))
0 < lambda * (b - a)
0 < delta

goal (1 subgoal):
 1. lambda * (b - a) / (10 * delta) \<le> 2 ^ (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda * (b - a) / (10 * delta) \<le> 2 ^ (n + 1)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have K: "k \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> n
[PROOF STEP]
using A **
[PROOF STATE]
proof (prove)
using this:
real k \<le> log 2 (lambda * (b - a) / (10 * delta))
int n = \<lfloor>log 2 (lambda * (b - a) / (10 * delta))\<rfloor>

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

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define N where "N = n+1"
[PROOF STATE]
proof (state)
this:
N = n + 1

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have N: "k+1 \<le> N" "lambda * (b-a) / 2^N \<le> 10 *delta" "2 ^ N \<le> lambda * (b - a) / (5 * delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + 1 \<le> N &&& lambda * (b - a) / 2 ^ N \<le> 10 * delta &&& 2 ^ N \<le> lambda * (b - a) / (5 * delta)
[PROOF STEP]
using I J K \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> lambda * (b - a) / (10 * delta)
lambda * (b - a) / (10 * delta) \<le> 2 ^ (n + 1)
k \<le> n
0 < delta

goal (1 subgoal):
 1. k + 1 \<le> N &&& lambda * (b - a) / 2 ^ N \<le> 10 * delta &&& 2 ^ N \<le> lambda * (b - a) / (5 * delta)
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> lambda * (b - a) / (10 * delta)
lambda * (b - a) / (10 * delta) \<le> 2 ^ (n + 1)
k \<le> n
0 < delta

goal (1 subgoal):
 1. k + 1 \<le> n + 1 &&& lambda * (b - a) / 2 ^ (n + 1) \<le> 10 * delta &&& 2 ^ (n + 1) \<le> lambda * (b - a) / (5 * delta)
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
k + 1 \<le> N
lambda * (b - a) / 2 ^ N \<le> 10 * delta
2 ^ N \<le> lambda * (b - a) / (5 * delta)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k + 1 \<le> N
lambda * (b - a) / 2 ^ N \<le> 10 * delta
2 ^ N \<le> lambda * (b - a) / (5 * delta)
[PROOF STEP]
have "2 ^ k \<noteq> (0::real)" "k \<le> N"
[PROOF STATE]
proof (prove)
using this:
k + 1 \<le> N
lambda * (b - a) / 2 ^ N \<le> 10 * delta
2 ^ N \<le> lambda * (b - a) / (5 * delta)

goal (1 subgoal):
 1. 2 ^ k \<noteq> 0 &&& k \<le> N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ k \<noteq> 0
k \<le> N

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ k \<noteq> 0
k \<le> N
[PROOF STEP]
have "(2^(N-k)::real) = 2^N/2^k"
[PROOF STATE]
proof (prove)
using this:
2 ^ k \<noteq> 0
k \<le> N

goal (1 subgoal):
 1. 2 ^ (N - k) = 2 ^ N / 2 ^ k
[PROOF STEP]
by (metis (no_types) add_diff_cancel_left' le_Suc_ex nonzero_mult_div_cancel_left power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (N - k) = 2 ^ N / 2 ^ k

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>Define $2^N$ points along the path, separated by at most $10\delta$, and their projections.\<close>
[PROOF STATE]
proof (state)
this:
2 ^ (N - k) = 2 ^ N / 2 ^ k

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define g::"nat \<Rightarrow> 'a" where "g = (\<lambda>i. f(a + (b-a) * i/2^N))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. f (a + (b - a) * real x / 2 ^ N))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "g 0 = f a" "g(2^N) = f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g 0 = f a &&& g (2 ^ N) = f b
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a + (b - a) * real 0 / 2 ^ N) = f a &&& f (a + (b - a) * real (2 ^ N) / 2 ^ N) = f b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g 0 = f a
g (2 ^ N) = f b

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have *: "a + (b-a) * i/2^N \<in> {a..b}" if "i \<in> {0..2^N}" for i::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
have "a + (b - a) * (real i / 2 ^ N) \<le> a + (b-a) * (2^N/2^N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (b - a) * (real i / 2 ^ N) \<le> a + (b - a) * (2 ^ N / 2 ^ N)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. real i \<le> 2 ^ N
 2. 0 \<le> 2 ^ N
 3. 0 \<le> b - a
[PROOF STEP]
using that \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ N}
a \<le> b

goal (3 subgoals):
 1. real i \<le> 2 ^ N
 2. 0 \<le> 2 ^ N
 3. 0 \<le> b - a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + (b - a) * (real i / 2 ^ N) \<le> a + (b - a) * (2 ^ N / 2 ^ N)

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a + (b - a) * (real i / 2 ^ N) \<le> a + (b - a) * (2 ^ N / 2 ^ N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a + (b - a) * (real i / 2 ^ N) \<le> a + (b - a) * (2 ^ N / 2 ^ N)

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
using \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
a + (b - a) * (real i / 2 ^ N) \<le> a + (b - a) * (2 ^ N / 2 ^ N)
a \<le> b

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + (b - a) * real i / 2 ^ N \<in> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ N} \<Longrightarrow> a + (b - a) * real ?i / 2 ^ N \<in> {a..b}

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have A: "dist (g i) (g (Suc i)) \<le> 10 * delta + C" if "i \<in> {0..<2^N}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
have "dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b-a) * i/2^N) (a + (b-a) * (Suc i)/2^N) + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f (a + (b - a) * real i / 2 ^ N)) (f (a + (b - a) * real (Suc i) / 2 ^ N)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C
[PROOF STEP]
apply (intro assms(2) *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i \<in> {0..2 ^ N}
 2. Suc i \<in> {0..2 ^ N}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<2 ^ N}

goal (2 subgoals):
 1. i \<in> {0..2 ^ N}
 2. Suc i \<in> {0..2 ^ N}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (g i) (g (Suc i)) \<le> lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
have "... = lambda * (b-a)/2^N + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C = lambda * (b - a) / 2 ^ N + C
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * \<bar>a + (b - a) * real i / 2 ^ N - (a + (b - a) * real (Suc i) / 2 ^ N)\<bar> + C = lambda * (b - a) / 2 ^ N + C
[PROOF STEP]
using \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. lambda * \<bar>a + (b - a) * real i / 2 ^ N - (a + (b - a) * real (Suc i) / 2 ^ N)\<bar> + C = lambda * (b - a) / 2 ^ N + C
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C = lambda * (b - a) / 2 ^ N + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lambda * dist (a + (b - a) * real i / 2 ^ N) (a + (b - a) * real (Suc i) / 2 ^ N) + C = lambda * (b - a) / 2 ^ N + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
have "... \<le> 10 * delta + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (b - a) / 2 ^ N + C \<le> 10 * delta + C
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
k + 1 \<le> N
lambda * (b - a) / 2 ^ N \<le> 10 * delta
2 ^ N \<le> lambda * (b - a) / (5 * delta)

goal (1 subgoal):
 1. lambda * (b - a) / 2 ^ N + C \<le> 10 * delta + C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lambda * (b - a) / 2 ^ N + C \<le> 10 * delta + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (g i) (g (Suc i)) \<le> 10 * delta + C

goal (1 subgoal):
 1. dist (g i) (g (Suc i)) \<le> 10 * delta + C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (g i) (g (Suc i)) \<le> 10 * delta + C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..<2 ^ N} \<Longrightarrow> dist (g ?i) (g (Suc ?i)) \<le> 10 * delta + C

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
define p where "p = (\<lambda>i. if i = 0 then pa else if i = 2^N then pb else SOME p. p \<in> proj_set (g i) G)"
[PROOF STATE]
proof (state)
this:
p = (\<lambda>i. if i = 0 then pa else if i = 2 ^ N then pb else SOME p. p \<in> proj_set (g i) G)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have B: "p i \<in> proj_set (g i) G" if "i \<in> {0..2^N}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
proof (cases "i = 0 \<or> i = 2^N")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<or> i = 2 ^ N \<Longrightarrow> p i \<in> proj_set (g i) G
 2. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 0 \<or> i = 2 ^ N

goal (2 subgoals):
 1. i = 0 \<or> i = 2 ^ N \<Longrightarrow> p i \<in> proj_set (g i) G
 2. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0 \<or> i = 2 ^ N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0 \<or> i = 2 ^ N

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
using \<open>pa \<in> proj_set (f a) G\<close> \<open>pb \<in> proj_set (f b) G\<close>
[PROOF STATE]
proof (prove)
using this:
i = 0 \<or> i = 2 ^ N
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
unfolding p_def g_def
[PROOF STATE]
proof (prove)
using this:
i = 0 \<or> i = 2 ^ N
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G

goal (1 subgoal):
 1. (if i = 0 then pa else if i = 2 ^ N then pb else SOME p. p \<in> proj_set (f (a + (b - a) * real i / 2 ^ N)) G) \<in> proj_set (f (a + (b - a) * real i / 2 ^ N)) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p i \<in> proj_set (g i) G

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (i = 0 \<or> i = 2 ^ N)

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (i = 0 \<or> i = 2 ^ N)
[PROOF STEP]
have "p i = (SOME p. p \<in> proj_set (g i) G)"
[PROOF STATE]
proof (prove)
using this:
\<not> (i = 0 \<or> i = 2 ^ N)

goal (1 subgoal):
 1. p i = (SOME p. p \<in> proj_set (g i) G)
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
\<not> (i = 0 \<or> i = 2 ^ N)

goal (1 subgoal):
 1. (if i = 0 then pa else if i = 2 ^ N then pb else SOME p. p \<in> proj_set (g i) G) = (SOME p. p \<in> proj_set (g i) G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p i = (SOME p. p \<in> proj_set (g i) G)

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p i = (SOME p. p \<in> proj_set (g i) G)

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
have "proj_set (g i) G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj_set (g i) G \<noteq> {}
[PROOF STEP]
apply (rule proj_set_nonempty_of_proper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
using geodesic_segment_topology[OF \<open>geodesic_segment G\<close>]
[PROOF STATE]
proof (prove)
using this:
compact G
connected G
path_connected G
bounded G
closed G
G \<noteq> {}
proper G

goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj_set (g i) G \<noteq> {}

goal (1 subgoal):
 1. \<not> (i = 0 \<or> i = 2 ^ N) \<Longrightarrow> p i \<in> proj_set (g i) G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p i = (SOME p. p \<in> proj_set (g i) G)
proj_set (g i) G \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p i = (SOME p. p \<in> proj_set (g i) G)
proj_set (g i) G \<noteq> {}

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
using some_in_eq
[PROOF STATE]
proof (prove)
using this:
p i = (SOME p. p \<in> proj_set (g i) G)
proj_set (g i) G \<noteq> {}
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. p i \<in> proj_set (g i) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p i \<in> proj_set (g i) G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ N} \<Longrightarrow> p ?i \<in> proj_set (g ?i) G

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have C: "dist (p i) (g i) \<ge> 5 * delta * k + 15/2 * delta + C/2" if "i \<in> {0..2^N}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
have "5 * delta * k + 15/2 * delta + C/2 \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D
[PROOF STEP]
using k(1)
[PROOF STATE]
proof (prove)
using this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> D

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
have "... \<le> infdist (g i) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<le> infdist (g i) G
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<le> infdist (f (a + (b - a) * real i / 2 ^ N)) G
[PROOF STEP]
apply (rule \<open>\<And>t. t \<in> {a..b} \<Longrightarrow> infdist (f t) G \<ge> D\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
using * that
[PROOF STATE]
proof (prove)
using this:
?i \<in> {0..2 ^ N} \<Longrightarrow> a + (b - a) * real ?i / 2 ^ N \<in> {a..b}
i \<in> {0..2 ^ N}

goal (1 subgoal):
 1. a + (b - a) * real i / 2 ^ N \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<le> infdist (g i) G

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D \<le> infdist (g i) G

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
have "... = dist (p i) (g i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (g i) G = dist (p i) (g i)
[PROOF STEP]
using that proj_setD(2)[OF B[OF that]]
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ N}
dist (g i) (p i) = infdist (g i) G

goal (1 subgoal):
 1. infdist (g i) G = dist (p i) (g i)
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
infdist (g i) G = dist (p i) (g i)

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)

goal (1 subgoal):
 1. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p i) (g i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ N} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p ?i) (g ?i)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>Use the basic statement to show that, along packets of size $2^k$, the projections
    are within $5\delta$ of each other.\<close>
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ N} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p ?i) (g ?i)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have I: "dist (p (2^k * j)) (p (2^k * (Suc j))) \<le> 5 * delta" if "j \<in> {0..<2^(N-k)}" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
have I: "i + 2^k * j \<in> {0..2^N}" if "i \<in> {0..2^k}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..2 ^ N}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..2 ^ N}
[PROOF STEP]
have "i + 2 ^ k * j \<le> 2^k + 2^k * (2^(N-k)-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + 2 ^ k * j \<le> 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i \<le> 2 ^ k
 2. j \<le> 2 ^ (N - k) - 1
[PROOF STEP]
using that \<open>j \<in> {0..<2^(N-k)}\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..2 ^ k}
j \<in> {0..<2 ^ (N - k)}

goal (2 subgoals):
 1. i \<le> 2 ^ k
 2. j \<le> 2 ^ (N - k) - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + 2 ^ k * j \<le> 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1)

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..2 ^ N}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
i + 2 ^ k * j \<le> 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1)

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..2 ^ N}
[PROOF STEP]
have "... = 2^N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1) = 2 ^ N
[PROOF STEP]
using \<open>k +1 \<le> N\<close>
[PROOF STATE]
proof (prove)
using this:
k + 1 \<le> N

goal (1 subgoal):
 1. 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1) = 2 ^ N
[PROOF STEP]
by (auto simp add: algebra_simps semiring_normalization_rules(26))
[PROOF STATE]
proof (state)
this:
2 ^ k + 2 ^ k * (2 ^ (N - k) - 1) = 2 ^ N

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..2 ^ N}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
i + 2 ^ k * j \<le> 2 ^ N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i + 2 ^ k * j \<le> 2 ^ N

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..2 ^ N}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + 2 ^ k * j \<in> {0..2 ^ N}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..2 ^ k} \<Longrightarrow> ?i + 2 ^ k * j \<in> {0..2 ^ N}

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
have I': "i + 2^k * j \<in> {0..<2^N}" if "i \<in> {0..<2^k}" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..<2 ^ N}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..<2 ^ N}
[PROOF STEP]
have "i + 2 ^ k * j < 2^k + 2^k * (2^(N-k)-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + 2 ^ k * j < 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < 2 ^ k
 2. j \<le> 2 ^ (N - k) - 1
[PROOF STEP]
using that \<open>j \<in> {0..<2^(N-k)}\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<2 ^ k}
j \<in> {0..<2 ^ (N - k)}

goal (2 subgoals):
 1. i < 2 ^ k
 2. j \<le> 2 ^ (N - k) - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + 2 ^ k * j < 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1)

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..<2 ^ N}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
i + 2 ^ k * j < 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1)

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..<2 ^ N}
[PROOF STEP]
have "... = 2^N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1) = 2 ^ N
[PROOF STEP]
using \<open>k +1 \<le> N\<close>
[PROOF STATE]
proof (prove)
using this:
k + 1 \<le> N

goal (1 subgoal):
 1. 2 ^ k + 2 ^ k * (2 ^ (N - k) - 1) = 2 ^ N
[PROOF STEP]
by (auto simp add: algebra_simps semiring_normalization_rules(26))
[PROOF STATE]
proof (state)
this:
2 ^ k + 2 ^ k * (2 ^ (N - k) - 1) = 2 ^ N

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..<2 ^ N}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
i + 2 ^ k * j < 2 ^ N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i + 2 ^ k * j < 2 ^ N

goal (1 subgoal):
 1. i + 2 ^ k * j \<in> {0..<2 ^ N}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + 2 ^ k * j \<in> {0..<2 ^ N}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> {0..<2 ^ k} \<Longrightarrow> ?i + 2 ^ k * j \<in> {0..<2 ^ N}

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
define g' where "g' = (\<lambda>i. g (i + 2^k * j))"
[PROOF STATE]
proof (state)
this:
g' = (\<lambda>i. g (i + 2 ^ k * j))

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
define p' where "p' = (\<lambda>i. p (i + 2^k * j))"
[PROOF STATE]
proof (state)
this:
p' = (\<lambda>i. p (i + 2 ^ k * j))

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
have "dist (p' 0) (p' (2^k)) \<le> 5 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
apply (rule Main[where ?g = g' and ?c = C])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. p' i \<in> proj_set (g' i) G
 2. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p' i) (g' i)
 3. \<forall>i\<in>{0..<2 ^ k}. dist (g' i) (g' (Suc i)) \<le> 10 * delta + C
 4. 0 \<le> C
[PROOF STEP]
unfolding p'_def g'_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. p (i + 2 ^ k * j) \<in> proj_set (g (i + 2 ^ k * j)) G
 2. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p (i + 2 ^ k * j)) (g (i + 2 ^ k * j))
 3. \<forall>i\<in>{0..<2 ^ k}. dist (g (i + 2 ^ k * j)) (g (Suc i + 2 ^ k * j)) \<le> 10 * delta + C
 4. 0 \<le> C
[PROOF STEP]
using A B C I I' \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
?i \<in> {0..<2 ^ N} \<Longrightarrow> dist (g ?i) (g (Suc ?i)) \<le> 10 * delta + C
?i \<in> {0..2 ^ N} \<Longrightarrow> p ?i \<in> proj_set (g ?i) G
?i \<in> {0..2 ^ N} \<Longrightarrow> 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p ?i) (g ?i)
?i \<in> {0..2 ^ k} \<Longrightarrow> ?i + 2 ^ k * j \<in> {0..2 ^ N}
?i \<in> {0..<2 ^ k} \<Longrightarrow> ?i + 2 ^ k * j \<in> {0..<2 ^ N}
0 \<le> C

goal (4 subgoals):
 1. \<forall>i\<in>{0..2 ^ k}. p (i + 2 ^ k * j) \<in> proj_set (g (i + 2 ^ k * j)) G
 2. \<forall>i\<in>{0..2 ^ k}. 5 * delta * real k + 15 / 2 * delta + C / 2 \<le> dist (p (i + 2 ^ k * j)) (g (i + 2 ^ k * j))
 3. \<forall>i\<in>{0..<2 ^ k}. dist (g (i + 2 ^ k * j)) (g (Suc i + 2 ^ k * j)) \<le> 10 * delta + C
 4. 0 \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
have "... \<le> 5 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * deltaG TYPE('a) \<le> 5 * delta
[PROOF STEP]
using \<open>deltaG(TYPE('a)) < delta\<close>
[PROOF STATE]
proof (prove)
using this:
deltaG TYPE('a) < delta

goal (1 subgoal):
 1. 5 * deltaG TYPE('a) \<le> 5 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
5 * deltaG TYPE('a) \<le> 5 * delta

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * delta
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (p' 0) (p' (2 ^ k)) \<le> 5 * delta

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
unfolding p'_def
[PROOF STATE]
proof (prove)
using this:
dist (p (0 + 2 ^ k * j)) (p (2 ^ k + 2 ^ k * j)) \<le> 5 * delta

goal (1 subgoal):
 1. dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> 5 * delta

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j \<in> {0..<2 ^ (N - k)} \<Longrightarrow> dist (p (2 ^ k * ?j)) (p (2 ^ k * Suc ?j)) \<le> 5 * delta

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
text \<open>Control the total distance by adding the contributions of blocks of size $2^k$.\<close>
[PROOF STATE]
proof (state)
this:
?j \<in> {0..<2 ^ (N - k)} \<Longrightarrow> dist (p (2 ^ k * ?j)) (p (2 ^ k * Suc ?j)) \<le> 5 * delta

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have *: "dist (p 0) (p(2^k * j)) \<le> (\<Sum>i<j. dist (p (2^k * i)) (p (2^k * (Suc i))))" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
proof (induction j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
have "dist (p 0) (p(2^k * (Suc j))) \<le> dist (p 0) (p(2^k * j)) + dist (p(2^k * j)) (p(2^k * (Suc j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * Suc j)) \<le> dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * Suc j)) \<le> dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))

goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * Suc j)) \<le> dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))

goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
have "... \<le> (\<Sum>i<j. dist (p (2^k * i)) (p (2^k * (Suc i)))) + dist (p(2^k * j)) (p(2^k * (Suc j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))

goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * j)) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j))

goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
have "... = (\<Sum>i<Suc j. dist (p (2^k * i)) (p (2^k * (Suc i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) = (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) + dist (p (2 ^ k * j)) (p (2 ^ k * Suc j)) = (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (2 subgoals):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
 2. \<And>j. dist (p 0) (p (2 ^ k * j)) \<le> (\<Sum>i<j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<Longrightarrow> dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * Suc j)) \<le> (\<Sum>i<Suc j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * 0)) \<le> (\<Sum>i<0. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * ?j)) \<le> (\<Sum>i<?j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "dist pa pb = dist (p 0) (p (2^N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa pb = dist (p 0) (p (2 ^ N))
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa pb = dist (if 0 = 0 then pa else if 0 = 2 ^ N then pb else SOME p. p \<in> proj_set (g 0) G) (if 2 ^ N = 0 then pa else if 2 ^ N = 2 ^ N then pb else SOME p. p \<in> proj_set (g (2 ^ N)) G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist pa pb = dist (p 0) (p (2 ^ N))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist pa pb = dist (p 0) (p (2 ^ N))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = dist (p 0) (p (2^k * 2^(N-k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p (2 ^ N)) = dist (p 0) (p (2 ^ k * 2 ^ (N - k)))
[PROOF STEP]
using \<open>k +1 \<le> N\<close>
[PROOF STATE]
proof (prove)
using this:
k + 1 \<le> N

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ N)) = dist (p 0) (p (2 ^ k * 2 ^ (N - k)))
[PROOF STEP]
by (auto simp add: semiring_normalization_rules(26))
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ N)) = dist (p 0) (p (2 ^ k * 2 ^ (N - k)))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ N)) = dist (p 0) (p (2 ^ k * 2 ^ (N - k)))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... \<le> (\<Sum>i<2^(N-k). dist (p (2^k * i)) (p (2^k * (Suc i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * 2 ^ (N - k))) \<le> (\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist (p 0) (p (2 ^ k * ?j)) \<le> (\<Sum>i<?j. dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. dist (p 0) (p (2 ^ k * 2 ^ (N - k))) \<le> (\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * 2 ^ (N - k))) \<le> (\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p 0) (p (2 ^ k * 2 ^ (N - k))) \<le> (\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... \<le> (\<Sum>(i::nat)<2^(N-k). 5 * delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<le> (\<Sum>i<2 ^ (N - k). 5 * delta)
[PROOF STEP]
apply (rule sum_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {..<2 ^ (N - k)} \<Longrightarrow> dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)) \<le> 5 * delta
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
?j \<in> {0..<2 ^ (N - k)} \<Longrightarrow> dist (p (2 ^ k * ?j)) (p (2 ^ k * Suc ?j)) \<le> 5 * delta

goal (1 subgoal):
 1. \<And>i. i \<in> {..<2 ^ (N - k)} \<Longrightarrow> dist (p (2 ^ k * i)) (p (2 ^ k * Suc i)) \<le> 5 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<le> (\<Sum>i<2 ^ (N - k). 5 * delta)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (N - k). dist (p (2 ^ k * i)) (p (2 ^ k * Suc i))) \<le> (\<Sum>i<2 ^ (N - k). 5 * delta)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = 5 * delta * 2^(N-k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ (N - k). 5 * delta) = 5 * delta * 2 ^ (N - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (N - k). 5 * delta) = 5 * delta * 2 ^ (N - k)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (N - k). 5 * delta) = 5 * delta * 2 ^ (N - k)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = 5 * delta * 2^N * (1/ 2^k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * 2 ^ (N - k) = 5 * delta * 2 ^ N * (1 / 2 ^ k)
[PROOF STEP]
unfolding \<open>(2^(N-k)::real) = 2^N/2^k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * (2 ^ N / 2 ^ k) = 5 * delta * 2 ^ N * (1 / 2 ^ k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 * delta * 2 ^ (N - k) = 5 * delta * 2 ^ N * (1 / 2 ^ k)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
5 * delta * 2 ^ (N - k) = 5 * delta * 2 ^ N * (1 / 2 ^ k)

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... \<le> 5 * delta * (2 * lambda * (b-a)/(10 * delta)) * (2 * exp(15/2/5 * ln 2) * exp(- ((D-C/2) * ln 2 / (5 * delta))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * 2 ^ N * (1 / 2 ^ k) \<le> 5 * delta * (2 * lambda * (b - a) / (10 * delta)) * (2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta))))
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. 2 ^ N \<le> 2 * lambda * (b - a) / (10 * delta)
 2. 0 \<le> 5 * delta
 3. 1 / 2 ^ k \<le> 2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))
 4. 0 \<le> 5 * delta * (2 * lambda * (b - a) / (10 * delta))
 5. 0 \<le> 1 / 2 ^ k
[PROOF STEP]
using \<open>delta > 0\<close> \<open>lambda > 0\<close> \<open>a < b\<close> k' N
[PROOF STATE]
proof (prove)
using this:
0 < delta
0 < lambda
a < b
1 / 2 ^ k \<le> 2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))
k + 1 \<le> N
lambda * (b - a) / 2 ^ N \<le> 10 * delta
2 ^ N \<le> lambda * (b - a) / (5 * delta)

goal (5 subgoals):
 1. 2 ^ N \<le> 2 * lambda * (b - a) / (10 * delta)
 2. 0 \<le> 5 * delta
 3. 1 / 2 ^ k \<le> 2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))
 4. 0 \<le> 5 * delta * (2 * lambda * (b - a) / (10 * delta))
 5. 0 \<le> 1 / 2 ^ k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
5 * delta * 2 ^ N * (1 / 2 ^ k) \<le> 5 * delta * (2 * lambda * (b - a) / (10 * delta)) * (2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta))))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
5 * delta * 2 ^ N * (1 / 2 ^ k) \<le> 5 * delta * (2 * lambda * (b - a) / (10 * delta)) * (2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta))))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "... = (2 * exp(15/2/5 * ln 2)) * lambda * (b-a) * exp(-(D-C/2) * ln 2 / (5 * delta))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 * delta * (2 * lambda * (b - a) / (10 * delta)) * (2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))) = 2 * exp (15 / 2 / 5 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta))
[PROOF STEP]
using \<open>delta > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < delta

goal (1 subgoal):
 1. 5 * delta * (2 * lambda * (b - a) / (10 * delta)) * (2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))) = 2 * exp (15 / 2 / 5 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta))
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
5 * delta * (2 * lambda * (b - a) / (10 * delta)) * (2 * exp (15 / 2 / 5 * ln 2) * exp (- ((D - C / 2) * ln 2 / (5 * delta)))) = 2 * exp (15 / 2 / 5 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta))

goal (1 subgoal):
 1. \<not> lambda * (b - a) \<le> 10 * delta * 2 ^ k \<Longrightarrow> dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist pa pb \<le> 2 * exp (15 / 2 / 5 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist pa pb \<le> 2 * exp (15 / 2 / 5 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta))

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
unfolding \<open>exp(15/2/5 * ln 2) = 2 * exp(1/2 * ln (2::real))\<close>
[PROOF STATE]
proof (prove)
using this:
dist pa pb \<le> 2 * (2 * exp (1 / 2 * ln 2)) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta))

goal (1 subgoal):
 1. dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist pa pb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - C / 2) * ln 2 / (5 * delta)))

goal:
No subgoals!
[PROOF STEP]
qed