[STATEMENT]
lemma bx_le_x: "x \<ge> 0 \<Longrightarrow> b \<in> set bs \<Longrightarrow>  b * x \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> x; b \<in> set bs\<rbrakk> \<Longrightarrow> b * x \<le> x
[PROOF STEP]
using b_pos[of b] b_less_1[of b]
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs \<Longrightarrow> 0 < b
b \<in> set bs \<Longrightarrow> b < 1

goal (1 subgoal):
 1. \<lbrakk>0 \<le> x; b \<in> set bs\<rbrakk> \<Longrightarrow> b * x \<le> x
[PROOF STEP]
by (intro mult_left_le_one_le) (simp_all)


[STATEMENT]
lemma x0_pos: "x\<^sub>0 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x\<^sub>0
[PROOF STEP]
using x0_ge_1
[PROOF STATE]
proof (prove)
using this:
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. 0 < x\<^sub>0
[PROOF STEP]
by simp


[STATEMENT]
lemma step_diff:
  assumes "i < k" "x \<ge> x\<^sub>1"
  shows   "bs ! i * x + (hs ! i) x + 1 < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
have "bs ! i * x + (hs ! i) x + 1 \<le> bs ! i * x + \<bar>(hs ! i) x\<bar> + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 \<le> bs ! i * x + \<bar>(hs ! i) x\<bar> + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x + 1 \<le> bs ! i * x + \<bar>(hs ! i) x\<bar> + 1

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x + 1 \<le> bs ! i * x + \<bar>(hs ! i) x\<bar> + 1

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have "\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: h_bounds)
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "x*(1 - bs ! i - hb / ln x powr (1 + e)) > 1"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. 1 < x * (1 - bs ! i - hb / ln x powr (1 + e))
[PROOF STEP]
by (simp add: x0_hb_bound2)
[PROOF STATE]
proof (state)
this:
1 < x * (1 - bs ! i - hb / ln x powr (1 + e))

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
hence "bs ! i * x + hb * x / ln x powr (1 + e) + 1 < x"
[PROOF STATE]
proof (prove)
using this:
1 < x * (1 - bs ! i - hb / ln x powr (1 + e))

goal (1 subgoal):
 1. bs ! i * x + hb * x / ln x powr (1 + e) + 1 < x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
bs ! i * x + hb * x / ln x powr (1 + e) + 1 < x

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> bs ! i * x + xa + 1 \<le> bs ! i * x + y + 1) \<Longrightarrow> bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> bs ! i * x + xa + 1 \<le> bs ! i * x + y + 1) \<Longrightarrow> bs ! i * x + (hs ! i) x + 1 < x

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x + 1 < x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_le_x: "i < k \<Longrightarrow> x \<ge> x\<^sub>1 \<Longrightarrow> bs ! i * x + (hs ! i) x \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < k; x\<^sub>1 \<le> x\<rbrakk> \<Longrightarrow> bs ! i * x + (hs ! i) x \<le> x
[PROOF STEP]
by (drule (1) step_diff) simp


[STATEMENT]
lemma x0_hb_bound0': "\<And>x b. x \<ge> x\<^sub>0 \<Longrightarrow> b \<in> set bs \<Longrightarrow> hb / ln x powr (1 + e) < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x b. \<lbrakk>x\<^sub>0 \<le> x; b \<in> set bs\<rbrakk> \<Longrightarrow> hb / ln x powr (1 + e) < b
[PROOF STEP]
by (drule (1) x0_hb_bound0, erule less_le_trans) (simp add: b_pos)


[STATEMENT]
lemma step_pos:
  assumes "i < k" "x \<ge> x\<^sub>1"
  shows   "bs ! i * x + (hs ! i) x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "hb / ln x powr (1 + e) < bs ! i"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. hb / ln x powr (1 + e) < bs ! i
[PROOF STEP]
by (simp add: x0_hb_bound0')
[PROOF STATE]
proof (state)
this:
hb / ln x powr (1 + e) < bs ! i

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
with assms x0_pos x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1
hb / ln x powr (1 + e) < bs ! i
[PROOF STEP]
have "x * 0 < x * (bs ! i - hb / ln x powr (1 + e))"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1
hb / ln x powr (1 + e) < bs ! i

goal (1 subgoal):
 1. x * 0 < x * (bs ! i - hb / ln x powr (1 + e))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * 0 < x * (bs ! i - hb / ln x powr (1 + e))

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * 0 < x * (bs ! i - hb / ln x powr (1 + e))

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
have "... = bs ! i * x - hb * x / ln x powr (1 + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (bs ! i - hb / ln x powr (1 + e)) = bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x * (bs ! i - hb / ln x powr (1 + e)) = bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * (bs ! i - hb / ln x powr (1 + e)) = bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have "-hb * x / ln x powr (1 + e) \<le> -\<bar>(hs ! i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. - hb * x / ln x powr (1 + e) \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by (simp add: h_bounds)
[PROOF STATE]
proof (state)
this:
- hb * x / ln x powr (1 + e) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
hence "bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + -\<bar>(hs ! i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
- hb * x / ln x powr (1 + e) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
have "-\<bar>(hs ! i) x\<bar> \<le> (hs ! i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> bs ! i * x + xa \<le> bs ! i * x + y) \<Longrightarrow> x * 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
show "bs ! i * x + (hs ! i) x > 0"
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> bs ! i * x + xa \<le> bs ! i * x + y) \<Longrightarrow> x * 0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x + (hs ! i) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_nonneg: "i < k \<Longrightarrow> x \<ge> x\<^sub>1 \<Longrightarrow> bs ! i * x + (hs ! i) x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < k; x\<^sub>1 \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
by (drule (1) step_pos) simp


[STATEMENT]
lemma step_nonneg': "i < k \<Longrightarrow> x \<ge> x\<^sub>1 \<Longrightarrow> bs ! i + (hs ! i) x / x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < k; x\<^sub>1 \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> bs ! i + (hs ! i) x / x
[PROOF STEP]
by (frule (1) step_nonneg, insert x0_pos x0_le_x1) (simp_all add: field_simps)


[STATEMENT]
lemma hb_nonneg: "hb \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
from k_not_0 and length_hs
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
length hs = k
[PROOF STEP]
have "hs \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
length hs = k

goal (1 subgoal):
 1. hs \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hs \<noteq> []

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hs \<noteq> []
[PROOF STEP]
obtain h where h: "h \<in> set hs"
[PROOF STATE]
proof (prove)
using this:
hs \<noteq> []

goal (1 subgoal):
 1. (\<And>h. h \<in> set hs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases hs) auto
[PROOF STATE]
proof (state)
this:
h \<in> set hs

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
have "0 \<le> \<bar>h x\<^sub>1\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<bar>h x\<^sub>1\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> \<bar>h x\<^sub>1\<bar>

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> \<bar>h x\<^sub>1\<bar>

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
from h
[PROOF STATE]
proof (chain)
picking this:
h \<in> set hs
[PROOF STEP]
have "\<bar>h x\<^sub>1\<bar> \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
h \<in> set hs

goal (1 subgoal):
 1. \<bar>h x\<^sub>1\<bar> \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)
[PROOF STEP]
by (intro h_bounds) simp_all
[PROOF STATE]
proof (state)
this:
\<bar>h x\<^sub>1\<bar> \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)
[PROOF STEP]
have "0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)

goal (1 subgoal):
 1. 0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
hence "0 \<le> ... * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e)

goal (1 subgoal):
 1. 0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e) * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1)
[PROOF STEP]
by (rule mult_nonneg_nonneg) (intro divide_nonneg_nonneg, insert x1_pos, simp_all)
[PROOF STATE]
proof (state)
this:
0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e) * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1)

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e) * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1)

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
have "... = hb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e) * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1) = hb
[PROOF STEP]
using x1_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < x\<^sub>1

goal (1 subgoal):
 1. hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e) * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1) = hb
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
hb * x\<^sub>1 / ln x\<^sub>1 powr (1 + e) * (ln x\<^sub>1 powr (1 + e) / x\<^sub>1) = hb

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> hb
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> hb

goal (1 subgoal):
 1. 0 \<le> hb
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 \<le> hb

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound3:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "x - (bs ! i * x + (hs ! i) x) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
have "-(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "... \<le> hb * x / ln x powr (1 + e)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: h_bounds)
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
have "... = x * (hb / ln x powr (1 + e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb * x / ln x powr (1 + e) = x * (hb / ln x powr (1 + e))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hb * x / ln x powr (1 + e) = x * (hb / ln x powr (1 + e))

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hb * x / ln x powr (1 + e) = x * (hb / ln x powr (1 + e))

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
from assms x0_pos x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "... < x * bs ! i"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x * (hb / ln x powr (1 + e)) < x * bs ! i
[PROOF STEP]
by (intro mult_strict_left_mono x0_hb_bound0') simp_all
[PROOF STATE]
proof (state)
this:
x * (hb / ln x powr (1 + e)) < x * bs ! i

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- (hs ! i) x < x * bs ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- (hs ! i) x < x * bs ! i

goal (1 subgoal):
 1. x - (bs ! i * x + (hs ! i) x) \<le> x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x - (bs ! i * x + (hs ! i) x) \<le> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound4:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "(bs ! i + (hs ! i) x / x) > bs ! i / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "hb / ln x powr (1 + e) < bs ! i / 2"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. hb / ln x powr (1 + e) < bs ! i / 2
[PROOF STEP]
by (intro x0_hb_bound0) simp_all
[PROOF STATE]
proof (state)
this:
hb / ln x powr (1 + e) < bs ! i / 2

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
with assms x0_pos x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1
hb / ln x powr (1 + e) < bs ! i / 2
[PROOF STEP]
have "(-bs ! i / 2) * x < (-hb / ln x powr (1 + e)) * x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1
hb / ln x powr (1 + e) < bs ! i / 2

goal (1 subgoal):
 1. - bs ! i / 2 * x < - hb / ln x powr (1 + e) * x
[PROOF STEP]
by (intro mult_strict_right_mono) simp_all
[PROOF STATE]
proof (state)
this:
- bs ! i / 2 * x < - hb / ln x powr (1 + e) * x

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- bs ! i / 2 * x < - hb / ln x powr (1 + e) * x

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
from assms x0_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
[PROOF STEP]
have "... \<le> -\<bar>(hs ! i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0

goal (1 subgoal):
 1. - hb / ln x powr (1 + e) * x \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
using h_bounds
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
\<lbrakk>x\<^sub>1 \<le> ?x; ?h \<in> set hs\<rbrakk> \<Longrightarrow> \<bar>?h ?x\<bar> \<le> hb * ?x / ln ?x powr (1 + e)

goal (1 subgoal):
 1. - hb / ln x powr (1 + e) * x \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- hb / ln x powr (1 + e) * x \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- hb / ln x powr (1 + e) * x \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
have "... \<le> (hs ! i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- bs ! i / 2 * x < (hs ! i) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- bs ! i / 2 * x < (hs ! i) x

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
using assms x1_pos
[PROOF STATE]
proof (prove)
using this:
- bs ! i / 2 * x < (hs ! i) x
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i + (hs ! i) x / x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound4': "x \<ge> x\<^sub>1 \<Longrightarrow> i < k \<Longrightarrow> (bs ! i + (hs ! i) x / x) \<ge> bs ! i / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> bs ! i / 2 \<le> bs ! i + (hs ! i) x / x
[PROOF STEP]
by (drule (1) x0_hb_bound4) simp


[STATEMENT]
lemma x0_hb_bound5:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "(bs ! i + (hs ! i) x / x) \<le> bs ! i * 3/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
have "(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "... \<le> hb * x / ln x powr (1 + e)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: h_bounds)
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
have "... = x * (hb / ln x powr (1 + e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb * x / ln x powr (1 + e) = x * (hb / ln x powr (1 + e))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hb * x / ln x powr (1 + e) = x * (hb / ln x powr (1 + e))

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hb * x / ln x powr (1 + e) = x * (hb / ln x powr (1 + e))

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
from assms x0_pos x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "... < x * (bs ! i / 2)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x * (hb / ln x powr (1 + e)) < x * (bs ! i / 2)
[PROOF STEP]
by (intro mult_strict_left_mono x0_hb_bound0) simp_all
[PROOF STATE]
proof (state)
this:
x * (hb / ln x powr (1 + e)) < x * (bs ! i / 2)

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(hs ! i) x < x * (bs ! i / 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x < x * (bs ! i / 2)

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
using assms x1_pos
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x < x * (bs ! i / 2)
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1

goal (1 subgoal):
 1. bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
bs ! i + (hs ! i) x / x \<le> bs ! i * 3 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound6:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "hb / ln x powr (1 + e) < (1 - bs ! i) / 2"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. hb / ln x powr (1 + e) < (1 - bs ! i) / 2
[PROOF STEP]
using x0_hb_bound1
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
\<lbrakk>x\<^sub>0 \<le> ?x; ?b \<in> set bs\<rbrakk> \<Longrightarrow> hb / ln ?x powr (1 + e) < (1 - ?b) / 2

goal (1 subgoal):
 1. hb / ln x powr (1 + e) < (1 - bs ! i) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hb / ln x powr (1 + e) < (1 - bs ! i) / 2

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
with assms x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1
hb / ln x powr (1 + e) < (1 - bs ! i) / 2
[PROOF STEP]
have "x * ((1 - bs ! i) / 2) \<le> x * (1 - (bs ! i + hb / ln x powr (1 + e)))"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1
hb / ln x powr (1 + e) < (1 - bs ! i) / 2

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x * (1 - (bs ! i + hb / ln x powr (1 + e)))
[PROOF STEP]
by (intro mult_left_mono) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
x * ((1 - bs ! i) / 2) \<le> x * (1 - (bs ! i + hb / ln x powr (1 + e)))

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * ((1 - bs ! i) / 2) \<le> x * (1 - (bs ! i + hb / ln x powr (1 + e)))

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "... = x - bs ! i * x + -hb * x / ln x powr (1 + e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (1 - (bs ! i + hb / ln x powr (1 + e))) = x - bs ! i * x + - hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x * (1 - (bs ! i + hb / ln x powr (1 + e))) = x - bs ! i * x + - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * (1 - (bs ! i + hb / ln x powr (1 + e))) = x - bs ! i * x + - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from h_bounds assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>1 \<le> ?x; ?h \<in> set hs\<rbrakk> \<Longrightarrow> \<bar>?h ?x\<bar> \<le> hb * ?x / ln ?x powr (1 + e)
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "-hb * x / ln x powr (1 + e) \<le> -\<bar>(hs ! i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x; ?h \<in> set hs\<rbrakk> \<Longrightarrow> \<bar>?h ?x\<bar> \<le> hb * ?x / ln ?x powr (1 + e)
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. - hb * x / ln x powr (1 + e) \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by (simp add: length_hs)
[PROOF STATE]
proof (state)
this:
- hb * x / ln x powr (1 + e) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- hb * x / ln x powr (1 + e) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "... \<le> -(hs ! i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<bar>(hs ! i) x\<bar> \<le> - (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- \<bar>(hs ! i) x\<bar> \<le> - (hs ! i) x

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> x - bs ! i * x + xa \<le> x - bs ! i * x + y; \<And>xa y. xa \<le> y \<Longrightarrow> x - bs ! i * x + xa \<le> x - bs ! i * x + y\<rbrakk> \<Longrightarrow> x * ((1 - bs ! i) / 2) \<le> x - bs ! i * x + - (hs ! i) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> x - bs ! i * x + xa \<le> x - bs ! i * x + y; \<And>xa y. xa \<le> y \<Longrightarrow> x - bs ! i * x + xa \<le> x - bs ! i * x + y\<rbrakk> \<Longrightarrow> x * ((1 - bs ! i) / 2) \<le> x - bs ! i * x + - (hs ! i) x

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x * ((1 - bs ! i) / 2) \<le> x - (bs ! i * x + (hs ! i) x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound7:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "bs!i*x + (hs!i) x > x\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have x': "x \<ge> x\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from x1_ge assms
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> 2 * x\<^sub>0 * inverse ?b \<le> x\<^sub>1
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "2 * x\<^sub>0 * inverse (bs!i) \<le> x\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> 2 * x\<^sub>0 * inverse ?b \<le> x\<^sub>1
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
with assms b_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
?b \<in> set bs \<Longrightarrow> 0 < ?b
2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1
[PROOF STEP]
have "x\<^sub>0 \<le> x\<^sub>1 * (bs!i / 2)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
?b \<in> set bs \<Longrightarrow> 0 < ?b
2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 \<le> x\<^sub>1 * (bs ! i / 2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x\<^sub>1 * (bs ! i / 2)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x\<^sub>1 * (bs ! i / 2)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms x'
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x
[PROOF STEP]
have "bs!i/2 < bs!i + (hs!i) x / x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
by (intro x0_hb_bound4)
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i + (hs ! i) x / x

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i + (hs ! i) x / x

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms step_nonneg' x'
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
\<lbrakk>?i < k; x\<^sub>1 \<le> ?x\<rbrakk> \<Longrightarrow> 0 \<le> bs ! ?i + (hs ! ?i) ?x / ?x
x\<^sub>0 \<le> x
[PROOF STEP]
have "x\<^sub>1 * ... \<le> x * ..."
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
\<lbrakk>?i < k; x\<^sub>1 \<le> ?x\<rbrakk> \<Longrightarrow> 0 \<le> bs ! ?i + (hs ! ?i) ?x / ?x
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. x\<^sub>1 * (bs ! i + (hs ! i) x / x) \<le> x * (bs ! i + (hs ! i) x / x)
[PROOF STEP]
by (intro mult_right_mono) (simp_all)
[PROOF STATE]
proof (state)
this:
x\<^sub>1 * (bs ! i + (hs ! i) x / x) \<le> x * (bs ! i + (hs ! i) x / x)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sub>1 * (bs ! i + (hs ! i) x / x) \<le> x * (bs ! i + (hs ! i) x / x)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1
[PROOF STEP]
have "x * (bs!i + (hs!i) x / x) = bs!i*x + (hs!i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1

goal (1 subgoal):
 1. x * (bs ! i + (hs ! i) x / x) = bs ! i * x + (hs ! i) x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x * (bs ! i + (hs ! i) x / x) = bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x < y \<Longrightarrow> x\<^sub>1 * x < x\<^sub>1 * y) \<Longrightarrow> x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> x\<^sub>1 * x < x\<^sub>1 * y) \<Longrightarrow> x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
using x1_pos
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> x\<^sub>1 * x < x\<^sub>1 * y) \<Longrightarrow> x\<^sub>0 < bs ! i * x + (hs ! i) x
0 < x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound7': "x \<ge> x\<^sub>1 \<Longrightarrow> i < k \<Longrightarrow> bs!i*x + (hs!i) x > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> 1 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by (rule le_less_trans[OF _ x0_hb_bound7]) (insert x0_le_x1 x0_ge_1, simp_all)


[STATEMENT]
lemma x0_hb_bound8:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "bs!i*x - hb * x / ln x powr (1+e) > x\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "2 * x\<^sub>0 * inverse (bs!i) \<le> x\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1
[PROOF STEP]
by (intro x1_ge) simp_all
[PROOF STATE]
proof (state)
this:
2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
with b_pos assms
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> 0 < ?b
x\<^sub>1 \<le> x
i < k
2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1
[PROOF STEP]
have "x\<^sub>0 \<le> x\<^sub>1 * (bs!i/2)"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> 0 < ?b
x\<^sub>1 \<le> x
i < k
2 * x\<^sub>0 * inverse (bs ! i) \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 \<le> x\<^sub>1 * (bs ! i / 2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x\<^sub>1 * (bs ! i / 2)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x\<^sub>1 * (bs ! i / 2)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
from assms b_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
?b \<in> set bs \<Longrightarrow> 0 < ?b
[PROOF STEP]
have "... \<le> x * (bs!i/2)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
?b \<in> set bs \<Longrightarrow> 0 < ?b

goal (1 subgoal):
 1. x\<^sub>1 * (bs ! i / 2) \<le> x * (bs ! i / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>1 * (bs ! i / 2) \<le> x * (bs ! i / 2)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sub>1 * (bs ! i / 2) \<le> x * (bs ! i / 2)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "hb / ln x powr (1+e) < bs!i/2"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. hb / ln x powr (1 + e) < bs ! i / 2
[PROOF STEP]
by (intro x0_hb_bound0) simp_all
[PROOF STATE]
proof (state)
this:
hb / ln x powr (1 + e) < bs ! i / 2

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
hb / ln x powr (1 + e) < bs ! i / 2
[PROOF STEP]
have "bs!i/2 < bs!i - hb / ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
hb / ln x powr (1 + e) < bs ! i / 2

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i - hb / ln x powr (1 + e)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i - hb / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i - hb / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
have "x * ... = bs!i*x - hb * x / ln x powr (1+e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (bs ! i - hb / ln x powr (1 + e)) = bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x * (bs ! i - hb / ln x powr (1 + e)) = bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa < y \<Longrightarrow> x * xa < x * y) \<Longrightarrow> x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa < y \<Longrightarrow> x * xa < x * y) \<Longrightarrow> x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
using assms x1_pos
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa < y \<Longrightarrow> x * xa < x * y) \<Longrightarrow> x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound8':
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "bs!i*x + hb * x / ln x powr (1+e) > x\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "x\<^sub>0 < bs!i*x - hb * x / ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
by (rule x0_hb_bound8)
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
from assms hb_nonneg x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 \<le> hb
0 < x\<^sub>1
[PROOF STEP]
have "hb * x / ln x powr (1+e) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 \<le> hb
0 < x\<^sub>1

goal (1 subgoal):
 1. 0 \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
by (intro mult_nonneg_nonneg divide_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
hence "bs!i*x - hb * x / ln x powr (1+e) \<le> bs!i*x + hb * x / ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x0_hb_bound9:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "ln (bs!i*x + (hs!i) x) powr -(e/2) < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
from b_pos assms
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> 0 < ?b
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "0 < bs!i/2"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> 0 < ?b
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 0 < bs ! i / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < bs ! i / 2

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < bs ! i / 2

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "... < bs!i + (hs!i) x / x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. bs ! i / 2 < bs ! i + (hs ! i) x / x
[PROOF STEP]
by (intro x0_hb_bound4) simp_all
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i + (hs ! i) x / x

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i / 2 < bs ! i + (hs ! i) x / x

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
from assms x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1
[PROOF STEP]
have "x * ... = bs!i*x + (hs!i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1

goal (1 subgoal):
 1. x * (bs ! i + (hs ! i) x / x) = bs ! i * x + (hs ! i) x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x * (bs ! i + (hs ! i) x / x) = bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa < y \<Longrightarrow> x * xa < x * y) \<Longrightarrow> x * 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
have pos: "bs!i*x + (hs!i) x > 0"
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa < y \<Longrightarrow> x * xa < x * y) \<Longrightarrow> x * 0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
using assms x1_pos
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa < y \<Longrightarrow> x * xa < x * y) \<Longrightarrow> x * 0 < bs ! i * x + (hs ! i) x
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
from x0_hb_bound8[OF assms] x0_ge_1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
1 \<le> x\<^sub>0
[PROOF STEP]
have pos': "bs!i*x - hb * x / ln x powr (1+e) > 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. 1 < bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "-(hb * x / ln x powr (1+e)) \<le> -\<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. - (hb * x / ln x powr (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by (intro le_imp_neg_le h_bounds) simp_all
[PROOF STATE]
proof (state)
this:
- (hb * x / ln x powr (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- (hb * x / ln x powr (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
have "... \<le> (hs!i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- (hb * x / ln x powr (1 + e)) \<le> (hs ! i) x
[PROOF STEP]
have "ln (bs!i*x - hb * x / ln x powr (1+e)) \<le> ln (bs!i*x + (hs!i) x)"
[PROOF STATE]
proof (prove)
using this:
- (hb * x / ln x powr (1 + e)) \<le> (hs ! i) x

goal (1 subgoal):
 1. ln (bs ! i * x - hb * x / ln x powr (1 + e)) \<le> ln (bs ! i * x + (hs ! i) x)
[PROOF STEP]
using assms b_pos x0_pos pos'
[PROOF STATE]
proof (prove)
using this:
- (hb * x / ln x powr (1 + e)) \<le> (hs ! i) x
x\<^sub>1 \<le> x
i < k
?b \<in> set bs \<Longrightarrow> 0 < ?b
0 < x\<^sub>0
1 < bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. ln (bs ! i * x - hb * x / ln x powr (1 + e)) \<le> ln (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (intro ln_mono mult_pos_pos pos) simp_all
[PROOF STATE]
proof (state)
this:
ln (bs ! i * x - hb * x / ln x powr (1 + e)) \<le> ln (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
hence "ln (bs!i*x + (hs!i) x) powr -(e/2) \<le> ln (bs!i*x - hb * x / ln x powr (1+e)) powr -(e/2)"
[PROOF STATE]
proof (prove)
using this:
ln (bs ! i * x - hb * x / ln x powr (1 + e)) \<le> ln (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) \<le> ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2)
[PROOF STEP]
using assms e_pos asymptotics5[of x] pos'
[PROOF STATE]
proof (prove)
using this:
ln (bs ! i * x - hb * x / ln x powr (1 + e)) \<le> ln (bs ! i * x + (hs ! i) x)
x\<^sub>1 \<le> x
i < k
0 < e
\<lbrakk>x\<^sub>0 \<le> x; ?i < k\<rbrakk> \<Longrightarrow> ln (bs ! ?i * x - hb * x * ln x powr - (1 + e)) powr (- e / 2) < 1
1 < bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) \<le> ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2)
[PROOF STEP]
by (intro powr_mono2' ln_gt_zero) simp_all
[PROOF STATE]
proof (state)
this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) \<le> ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2)

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) \<le> ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2)

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
have "... < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2) < 1
[PROOF STEP]
using asymptotics5[of x i] assms x0_le_x1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> x; i < k\<rbrakk> \<Longrightarrow> ln (bs ! i * x - hb * x * ln x powr - (1 + e)) powr (- e / 2) < 1
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2) < 1
[PROOF STEP]
by (subst (asm) powr_minus) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
ln (bs ! i * x - hb * x / ln x powr (1 + e)) powr - (e / 2) < 1

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1

goal (1 subgoal):
 1. ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma akra_bazzi_measure_decreases:
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "akra_bazzi_measure (bs!i*x + (hs!i) x) < akra_bazzi_measure x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
from step_diff assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i < k; x\<^sub>1 \<le> ?x\<rbrakk> \<Longrightarrow> bs ! ?i * ?x + (hs ! ?i) ?x + 1 < ?x
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "(bs!i * x + (hs!i) x) + 1 < x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i < k; x\<^sub>1 \<le> ?x\<rbrakk> \<Longrightarrow> bs ! ?i * ?x + (hs ! ?i) ?x + 1 < ?x
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x + 1 < x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x + 1 < x

goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
hence "\<lceil>(bs!i * x + (hs!i) x) + 1\<rceil> \<le> \<lceil>x\<rceil>"
[PROOF STATE]
proof (prove)
using this:
bs ! i * x + (hs ! i) x + 1 < x

goal (1 subgoal):
 1. \<lceil>bs ! i * x + (hs ! i) x + 1\<rceil> \<le> \<lceil>x\<rceil>
[PROOF STEP]
by (intro ceiling_mono) simp
[PROOF STATE]
proof (state)
this:
\<lceil>bs ! i * x + (hs ! i) x + 1\<rceil> \<le> \<lceil>x\<rceil>

goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
hence "\<lceil>(bs!i * x + (hs!i) x)\<rceil> < \<lceil>x\<rceil>"
[PROOF STATE]
proof (prove)
using this:
\<lceil>bs ! i * x + (hs ! i) x + 1\<rceil> \<le> \<lceil>x\<rceil>

goal (1 subgoal):
 1. \<lceil>bs ! i * x + (hs ! i) x\<rceil> < \<lceil>x\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>bs ! i * x + (hs ! i) x\<rceil> < \<lceil>x\<rceil>

goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
with assms x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1
\<lceil>bs ! i * x + (hs ! i) x\<rceil> < \<lceil>x\<rceil>
[PROOF STEP]
have "nat \<lceil>(bs!i * x + (hs!i) x)\<rceil> < nat \<lceil>x\<rceil>"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < x\<^sub>1
\<lceil>bs ! i * x + (hs ! i) x\<rceil> < \<lceil>x\<rceil>

goal (1 subgoal):
 1. nat \<lceil>bs ! i * x + (hs ! i) x\<rceil> < nat \<lceil>x\<rceil>
[PROOF STEP]
by (subst nat_mono_iff) simp_all
[PROOF STATE]
proof (state)
this:
nat \<lceil>bs ! i * x + (hs ! i) x\<rceil> < nat \<lceil>x\<rceil>

goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nat \<lceil>bs ! i * x + (hs ! i) x\<rceil> < nat \<lceil>x\<rceil>

goal (1 subgoal):
 1. akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x
[PROOF STEP]
unfolding akra_bazzi_measure_def
[PROOF STATE]
proof (prove)
using this:
nat \<lceil>bs ! i * x + (hs ! i) x\<rceil> < nat \<lceil>x\<rceil>

goal (1 subgoal):
 1. nat \<lceil>bs ! i * x + (hs ! i) x\<rceil> < nat \<lceil>x\<rceil>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
akra_bazzi_measure (bs ! i * x + (hs ! i) x) < akra_bazzi_measure x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma akra_bazzi_induct[consumes 1, case_names base rec]:
  assumes "x \<ge> x\<^sub>0"
  assumes base: "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> P x"
  assumes rec:  "\<And>x. x > x\<^sub>1 \<Longrightarrow> (\<And>i. i < k \<Longrightarrow> P (bs!i*x + (hs!i) x)) \<Longrightarrow> P x"
  shows   "P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x
[PROOF STEP]
proof (insert \<open>x \<ge> x\<^sub>0\<close>, induction "akra_bazzi_measure x" arbitrary: x rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>xa. \<lbrakk>akra_bazzi_measure xa < akra_bazzi_measure x; x\<^sub>0 \<le> xa\<rbrakk> \<Longrightarrow> P xa; x\<^sub>0 \<le> x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
\<lbrakk>akra_bazzi_measure ?x < akra_bazzi_measure x; x\<^sub>0 \<le> ?x\<rbrakk> \<Longrightarrow> P ?x
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>xa. \<lbrakk>akra_bazzi_measure xa < akra_bazzi_measure x; x\<^sub>0 \<le> xa\<rbrakk> \<Longrightarrow> P xa; x\<^sub>0 \<le> x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x
[PROOF STEP]
proof (cases "x \<le> x\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> x\<^sub>1 \<Longrightarrow> P x
 2. \<not> x \<le> x\<^sub>1 \<Longrightarrow> P x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<le> x\<^sub>1

goal (2 subgoals):
 1. x \<le> x\<^sub>1 \<Longrightarrow> P x
 2. \<not> x \<le> x\<^sub>1 \<Longrightarrow> P x
[PROOF STEP]
with base and \<open>x \<ge> x\<^sub>0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> P ?x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> P ?x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. P x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P x

goal (1 subgoal):
 1. \<not> x \<le> x\<^sub>1 \<Longrightarrow> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> x\<^sub>1 \<Longrightarrow> P x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<le> x\<^sub>1

goal (1 subgoal):
 1. \<not> x \<le> x\<^sub>1 \<Longrightarrow> P x
[PROOF STEP]
hence x: "x > x\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>1 < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>1 < x

goal (1 subgoal):
 1. \<not> x \<le> x\<^sub>1 \<Longrightarrow> P x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x

goal (1 subgoal):
 1. P x
[PROOF STEP]
proof (rule rec)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> P (bs ! i * x + (hs ! i) x)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> P (bs ! i * x + (hs ! i) x)
[PROOF STEP]
assume i: "i < k"
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> P (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from x0_hb_bound7[OF _ i, of x] x
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x \<Longrightarrow> x\<^sub>0 < bs ! i * x + (hs ! i) x
x\<^sub>1 < x
[PROOF STEP]
have "bs!i*x + (hs!i) x \<ge> x\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x \<Longrightarrow> x\<^sub>0 < bs ! i * x + (hs ! i) x
x\<^sub>1 < x

goal (1 subgoal):
 1. x\<^sub>0 \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> P (bs ! i * x + (hs ! i) x)
[PROOF STEP]
with i x
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 < x
x\<^sub>0 \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
show "P (bs ! i * x + (hs ! i) x)"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 < x
x\<^sub>0 \<le> bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. P (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (intro less akra_bazzi_measure_decreases) simp_all
[PROOF STATE]
proof (state)
this:
P (bs ! i * x + (hs ! i) x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma akra_bazzi_integrable:
  "a \<ge> x\<^sub>0 \<Longrightarrow> a \<le> b \<Longrightarrow> integrable (\<lambda>x. g x / x powr (p + 1)) a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>0 \<le> a; a \<le> b\<rbrakk> \<Longrightarrow> integrable (\<lambda>x. g x / x powr (p + 1)) a b
[PROOF STEP]
by (rule integrable_subinterval[OF g_integrable, of b]) simp_all


[STATEMENT]
lemma f_nonneg: "x \<ge> x\<^sub>0 \<Longrightarrow> f x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 \<le> x \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
proof (induction x rule: akra_bazzi_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 0 \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
case (base x)
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 0 \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
with f_base[of x]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 0 \<le> f x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 0 \<le> f x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
case (rec x)
[PROOF STATE]
proof (state)
this:
x\<^sub>1 < x
?i < k \<Longrightarrow> 0 \<le> f (bs ! ?i * x + (hs ! ?i) x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
with x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x\<^sub>1
x\<^sub>1 < x
?i < k \<Longrightarrow> 0 \<le> f (bs ! ?i * x + (hs ! ?i) x)
[PROOF STEP]
have "g x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x\<^sub>1
x\<^sub>1 < x
?i < k \<Longrightarrow> 0 \<le> f (bs ! ?i * x + (hs ! ?i) x)

goal (1 subgoal):
 1. 0 \<le> g x
[PROOF STEP]
by (intro g_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 \<le> g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
assume i: "i < k"
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
with rec.IH
[PROOF STATE]
proof (chain)
picking this:
?i < k \<Longrightarrow> 0 \<le> f (bs ! ?i * x + (hs ! ?i) x)
i < k
[PROOF STEP]
have "f (bs!i*x + (hs!i) x) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
?i < k \<Longrightarrow> 0 \<le> f (bs ! ?i * x + (hs ! ?i) x)
i < k

goal (1 subgoal):
 1. 0 \<le> f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> f (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i < k
0 \<le> f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "as!i * f (bs!i*x + (hs!i) x) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
i < k
0 \<le> f (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. 0 \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (intro mult_nonneg_nonneg[OF a_ge_0]) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> as ! i * f (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < k \<Longrightarrow> 0 \<le> as ! ?i2 * f (bs ! ?i2 * x + (hs ! ?i2) x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
hence "(\<Sum>i<k. as!i * f (bs!i*x + (hs!i) x)) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
?i2 < k \<Longrightarrow> 0 \<le> as ! ?i2 * f (bs ! ?i2 * x + (hs ! ?i2) x)

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))
[PROOF STEP]
by (intro sum_nonneg) blast
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> 0 \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> 0 \<le> f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> g x
0 \<le> (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))
[PROOF STEP]
show "f x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> g x
0 \<le> (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))

goal (1 subgoal):
 1. 0 \<le> f x
[PROOF STEP]
using rec.hyps
[PROOF STATE]
proof (prove)
using this:
0 \<le> g x
0 \<le> (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))
x\<^sub>1 < x

goal (1 subgoal):
 1. 0 \<le> f x
[PROOF STEP]
by (subst f_rec) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_approx_aux:
  assumes "x \<ge> x\<^sub>0"
  shows   "1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
[PROOF STEP]
have "integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. 0 \<le> integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
by (intro integral_nonneg ballI g_nonneg divide_nonneg_nonneg g_integrable) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

goal (1 subgoal):
 1. 1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

goal (1 subgoal):
 1. 1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_approx_pos: "x \<ge> x\<^sub>0 \<Longrightarrow> f_approx x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 \<le> x \<Longrightarrow> 0 < f_approx x
[PROOF STEP]
unfolding f_approx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 \<le> x \<Longrightarrow> 0 < x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x)
[PROOF STEP]
by (intro mult_pos_pos, insert x0_pos, simp, drule f_approx_aux, simp)


[STATEMENT]
lemma f_approx_nonneg: "x \<ge> x\<^sub>0 \<Longrightarrow> f_approx x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 \<le> x \<Longrightarrow> 0 \<le> f_approx x
[PROOF STEP]
using f_approx_pos[of x]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x \<Longrightarrow> 0 < f_approx x

goal (1 subgoal):
 1. x\<^sub>0 \<le> x \<Longrightarrow> 0 \<le> f_approx x
[PROOF STEP]
by simp


[STATEMENT]
lemma f_approx_bounded_below:
  obtains c where "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> f_approx x \<ge> c" "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume x: "x \<ge> x\<^sub>0" "x \<le> x\<^sub>1"
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with x0_pos
[PROOF STATE]
proof (chain)
picking this:
0 < x\<^sub>0
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
have "x powr p \<ge> min (x\<^sub>0 powr p) (x\<^sub>1 powr p)"
[PROOF STATE]
proof (prove)
using this:
0 < x\<^sub>0
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. min (x\<^sub>0 powr p) (x\<^sub>1 powr p) \<le> x powr p
[PROOF STEP]
by (intro powr_lower_bound) simp_all
[PROOF STATE]
proof (state)
this:
min (x\<^sub>0 powr p) (x\<^sub>1 powr p) \<le> x powr p

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
min (x\<^sub>0 powr p) (x\<^sub>1 powr p) \<le> x powr p
[PROOF STEP]
have "f_approx x \<ge> min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
min (x\<^sub>0 powr p) (x\<^sub>1 powr p) \<le> x powr p

goal (1 subgoal):
 1. min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1 \<le> f_approx x
[PROOF STEP]
unfolding f_approx_def
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
min (x\<^sub>0 powr p) (x\<^sub>1 powr p) \<le> x powr p

goal (1 subgoal):
 1. min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1 \<le> x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x)
[PROOF STEP]
by (intro mult_mono f_approx_aux) simp_all
[PROOF STATE]
proof (state)
this:
min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1 \<le> f_approx x

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1 \<le> f_approx ?x2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx x; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this x0_pos x1_pos
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1 \<le> f_approx ?x2
0 < x\<^sub>0
0 < x\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> min (x\<^sub>0 powr p) (x\<^sub>1 powr p) * 1 \<le> f_approx ?x2
0 < x\<^sub>0
0 < x\<^sub>1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of "min (x\<^sub>0 powr p) (x\<^sub>1 powr p)"]) auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma asymptotics_aux:
  assumes "x \<ge> x\<^sub>1" "i < k"
  assumes "s \<equiv> (if p \<ge> 0 then 1 else -1)"
  shows "(bs!i*x - s*hb*x*ln x powr -(1+e)) powr p \<le> (bs!i*x + (hs!i) x) powr p" (is "?thesis1")
  and   "(bs!i*x + (hs!i) x) powr p \<le> (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p" (is "?thesis2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p &&& (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from assms x1_gt_1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
1 < x\<^sub>1
[PROOF STEP]
have ln_x_pos: "ln x > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
1 < x\<^sub>1

goal (1 subgoal):
 1. 0 < ln x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < ln x

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from assms x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
0 < x\<^sub>1
[PROOF STEP]
have x_pos: "x > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
0 < x\<^sub>1

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

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have *: "hb / ln x powr (1+e) < bs!i/2"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. hb / ln x powr (1 + e) < bs ! i / 2
[PROOF STEP]
by (intro x0_hb_bound0) simp_all
[PROOF STATE]
proof (state)
this:
hb / ln x powr (1 + e) < bs ! i / 2

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
with hb_nonneg ln_x_pos
[PROOF STATE]
proof (chain)
picking this:
0 \<le> hb
0 < ln x
hb / ln x powr (1 + e) < bs ! i / 2
[PROOF STEP]
have "(bs!i - hb * ln x powr -(1+e)) > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> hb
0 < ln x
hb / ln x powr (1 + e) < bs ! i / 2

goal (1 subgoal):
 1. 0 < bs ! i - hb * ln x powr - (1 + e)
[PROOF STEP]
by (subst powr_minus) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
0 < bs ! i - hb * ln x powr - (1 + e)

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
hb / ln x powr (1 + e) < bs ! i / 2
0 < bs ! i - hb * ln x powr - (1 + e)
[PROOF STEP]
have "0 < x * (bs!i - hb * ln x powr -(1+e))"
[PROOF STATE]
proof (prove)
using this:
hb / ln x powr (1 + e) < bs ! i / 2
0 < bs ! i - hb * ln x powr - (1 + e)

goal (1 subgoal):
 1. 0 < x * (bs ! i - hb * ln x powr - (1 + e))
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
hb / ln x powr (1 + e) < bs ! i / 2
0 < bs ! i - hb * ln x powr - (1 + e)
0 < x

goal (1 subgoal):
 1. 0 < x * (bs ! i - hb * ln x powr - (1 + e))
[PROOF STEP]
by (subst (asm) powr_minus, intro mult_pos_pos)
[PROOF STATE]
proof (state)
this:
0 < x * (bs ! i - hb * ln x powr - (1 + e))

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
hence A: "0 < bs!i*x - hb * x * ln x powr -(1+e)"
[PROOF STATE]
proof (prove)
using this:
0 < x * (bs ! i - hb * ln x powr - (1 + e))

goal (1 subgoal):
 1. 0 < bs ! i * x - hb * x * ln x powr - (1 + e)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x - hb * x * ln x powr - (1 + e)

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
[PROOF STEP]
have "-(hb*x*ln x powr -(1+e)) \<le> -\<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1

goal (1 subgoal):
 1. - (hb * x * ln x powr - (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
using h_bounds[of x "hs!i"]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
\<lbrakk>x\<^sub>1 \<le> x; hs ! i \<in> set hs\<rbrakk> \<Longrightarrow> \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. - (hb * x * ln x powr - (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by (subst neg_le_iff_le, subst powr_minus) (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
- (hb * x * ln x powr - (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- (hb * x * ln x powr - (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
have "... \<le> (hs!i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- (hb * x * ln x powr - (1 + e)) \<le> (hs ! i) x
[PROOF STEP]
have B: "bs!i*x - hb*x*ln x powr -(1+e) \<le> bs!i*x + (hs!i) x"
[PROOF STATE]
proof (prove)
using this:
- (hb * x * ln x powr - (1 + e)) \<le> (hs ! i) x

goal (1 subgoal):
 1. bs ! i * x - hb * x * ln x powr - (1 + e) \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x - hb * x * ln x powr - (1 + e) \<le> bs ! i * x + (hs ! i) x

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
have "(hs!i) x \<le> \<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
[PROOF STEP]
have "... \<le> (hb*x*ln x powr -(1+e))"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x * ln x powr - (1 + e)
[PROOF STEP]
using h_bounds[of x "hs!i"]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
s \<equiv> if 0 \<le> p then 1 else - 1
\<lbrakk>x\<^sub>1 \<le> x; hs ! i \<in> set hs\<rbrakk> \<Longrightarrow> \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x * ln x powr - (1 + e)
[PROOF STEP]
by (subst powr_minus) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x * ln x powr - (1 + e)

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)
[PROOF STEP]
have C: "bs!i*x + hb*x*ln x powr -(1+e) \<ge> bs!i*x + (hs!i) x"
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x * ln x powr - (1 + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x * ln x powr - (1 + e)

goal (2 subgoals):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
 2. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from A B C
[PROOF STATE]
proof (chain)
picking this:
0 < bs ! i * x - hb * x * ln x powr - (1 + e)
bs ! i * x - hb * x * ln x powr - (1 + e) \<le> bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x * ln x powr - (1 + e)
[PROOF STEP]
show ?thesis1
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i * x - hb * x * ln x powr - (1 + e)
bs ! i * x - hb * x * ln x powr - (1 + e) \<le> bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
[PROOF STEP]
by (cases "p \<ge> 0") (auto intro: powr_mono2 powr_mono2' simp: assms(3))
[PROOF STATE]
proof (state)
this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
from A B C
[PROOF STATE]
proof (chain)
picking this:
0 < bs ! i * x - hb * x * ln x powr - (1 + e)
bs ! i * x - hb * x * ln x powr - (1 + e) \<le> bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x * ln x powr - (1 + e)
[PROOF STEP]
show ?thesis2
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i * x - hb * x * ln x powr - (1 + e)
bs ! i * x - hb * x * ln x powr - (1 + e) \<le> bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
by (cases "p \<ge> 0") (auto intro: powr_mono2 powr_mono2' simp: assms(3))
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p

goal:
No subgoals!
[PROOF STEP]
qed