[STATEMENT]
lemma g_bounds1:
  obtains c3 where
    "\<And>x i. x \<ge> x\<^sub>1 \<Longrightarrow> i < k \<Longrightarrow> c3 * g x \<le> g_approx i x" "c3 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define c3 where "c3 =
    Min {c1*((1-b)/2) / max 1 (max ((b/2) powr (p+1)) ((b*3/2) powr (p+1))) |b. b \<in> set bs}"
[PROOF STATE]
proof (state)
this:
c3 = Min {c1 * ((1 - b) / 2) / max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c3 = Min {c1 * ((1 - b) / 2) / max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume b: "b \<in> set bs"
[PROOF STATE]
proof (state)
this:
b \<in> set bs

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?x = "max 1 (max ((b/2) powr (p+1)) ((b*3/2) powr (p+1)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "?x \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "?x > 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
by (rule less_le_trans[OF zero_less_one])
[PROOF STATE]
proof (state)
this:
0 < max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with b b_less_1 c1_pos
[PROOF STATE]
proof (chain)
picking this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> ?b < 1
0 < c1
0 < max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
have "c1*((1-b)/2) / ?x > 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> ?b < 1
0 < c1
0 < max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < c1 * ((1 - b) / 2) / max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
by (intro divide_pos_pos mult_pos_pos) (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
0 < c1 * ((1 - b) / 2) / max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in> set bs \<Longrightarrow> 0 < c1 * ((1 - ?b2) / 2) / max 1 (max ((?b2 / 2) powr (p + 1)) ((?b2 * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "c3 > 0"
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> set bs \<Longrightarrow> 0 < c1 * ((1 - ?b2) / 2) / max 1 (max ((?b2 / 2) powr (p + 1)) ((?b2 * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < c3
[PROOF STEP]
unfolding c3_def
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> set bs \<Longrightarrow> 0 < c1 * ((1 - ?b2) / 2) / max 1 (max ((?b2 / 2) powr (p + 1)) ((?b2 * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < Min {c1 * ((1 - b) / 2) / max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}
[PROOF STEP]
by (subst Min_gr_iff) auto
[PROOF STATE]
proof (state)
this:
0 < c3

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume i: "i < k" and x: "x \<ge> x\<^sub>1"
[PROOF STATE]
proof (state)
this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with b_less_1
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> ?b < 1
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have b_less_1': "bs ! i < 1"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> ?b < 1
i < k
x\<^sub>1 \<le> x

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m = "max 1 (max ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from i x
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have "c3 \<le> c1*((1-bs!i)/2) / ?m"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))
[PROOF STEP]
unfolding c3_def
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. Min {c1 * ((1 - b) / 2) / max 1 (max ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs} \<le> c1 * ((1 - bs ! i) / 2) / max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))
[PROOF STEP]
by (intro Min.coboundedI) auto
[PROOF STATE]
proof (state)
this:
c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "max 1 ((bs!i + (hs ! i) x / x) powr (p+1)) \<le> max 1 (max ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))
[PROOF STEP]
apply (insert x i x0_le_x1 x1_pos step_pos[OF i x] b_pos[OF b_in_bs[OF i]],
             rule max.mono, simp, cases "p + 1 \<ge> 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; x\<^sub>0 \<le> x\<^sub>1; 0 < x\<^sub>1; 0 < bs ! i * x + (hs ! i) x; 0 < bs ! i; 0 \<le> p + 1\<rbrakk> \<Longrightarrow> (bs ! i + (hs ! i) x / x) powr (p + 1) \<le> max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))
 2. \<lbrakk>x\<^sub>1 \<le> x; i < k; x\<^sub>0 \<le> x\<^sub>1; 0 < x\<^sub>1; 0 < bs ! i * x + (hs ! i) x; 0 < bs ! i; \<not> 0 \<le> p + 1\<rbrakk> \<Longrightarrow> (bs ! i + (hs ! i) x / x) powr (p + 1) \<le> max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))
[PROOF STEP]
apply (rule order.trans[OF powr_mono2[OF _ _ x0_hb_bound5] max.cobounded2], simp_all add: field_simps) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; x\<^sub>0 \<le> x\<^sub>1; 0 < x\<^sub>1; 0 < bs ! i * x + (hs ! i) x; 0 < bs ! i; \<not> 0 \<le> p + 1\<rbrakk> \<Longrightarrow> (bs ! i + (hs ! i) x / x) powr (p + 1) \<le> max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))
[PROOF STEP]
apply (rule order.trans[OF powr_mono2'[OF _ _ x0_hb_bound4'] max.cobounded1], simp_all add: field_simps) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with b_less_1' c1_pos
[PROOF STATE]
proof (chain)
picking this:
bs ! i < 1
0 < c1
max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))
[PROOF STEP]
have "c1*((1-bs!i)/2) / ?m \<le>
          c1*((1-bs!i)/2) / max 1 ((bs!i + (hs ! i) x / x) powr (p+1))"
[PROOF STATE]
proof (prove)
using this:
bs ! i < 1
0 < c1
max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. c1 * ((1 - bs ! i) / 2) / max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
by (intro divide_left_mono mult_nonneg_nonneg) (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c1 * ((1 - bs ! i) / 2) / max 1 (max ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
have "c3 \<le> c1*((1-bs!i)/2) / max 1 ((bs!i + (hs ! i) x / x) powr (p+1))"
[PROOF STATE]
proof (prove)
using this:
c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c3 \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < k; x\<^sub>1 \<le> ?x2\<rbrakk> \<Longrightarrow> c3 \<le> c1 * ((1 - bs ! ?i2) / 2) / max 1 ((bs ! ?i2 + (hs ! ?i2) ?x2 / ?x2) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note c3 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < k; x\<^sub>1 \<le> ?x2\<rbrakk> \<Longrightarrow> c3 \<le> c1 * ((1 - bs ! ?i2) / 2) / max 1 ((bs ! ?i2 + (hs ! ?i2) ?x2 / ?x2) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < k; x\<^sub>1 \<le> ?x2\<rbrakk> \<Longrightarrow> c3 \<le> c1 * ((1 - bs ! ?i2) / 2) / max 1 ((bs ! ?i2 + (hs ! ?i2) ?x2 / ?x2) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x :: real and i :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume x: "x \<ge> x\<^sub>1" and i: "i < k"
[PROOF STATE]
proof (state)
this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
0 < x\<^sub>1
[PROOF STEP]
have x_pos: "x > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
0 < x\<^sub>1

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?x' = "bs ! i * x + (hs ! i) x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?x'' = "bs ! i + (hs ! i) x / x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x x1_ge_1 x0_le_x1 i c1_pos g_growth1'
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
1 \<le> x\<^sub>1
x\<^sub>0 \<le> x\<^sub>1
i < k
0 < c1
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k; ?u \<in> {bs ! ?i * ?x + (hs ! ?i) ?x..?x}\<rbrakk> \<Longrightarrow> c1 * g ?x \<le> g ?u
[PROOF STEP]
have c1: "c1 > 0" "\<forall>u\<in>{?x'..x}. g u \<ge> c1 * g x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
1 \<le> x\<^sub>1
x\<^sub>0 \<le> x\<^sub>1
i < k
0 < c1
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k; ?u \<in> {bs ! ?i * ?x + (hs ! ?i) ?x..?x}\<rbrakk> \<Longrightarrow> c1 * g ?x \<le> g ?u

goal (1 subgoal):
 1. 0 < c1 &&& \<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < c1
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define b' where "b' = (1 - bs!i)/2"
[PROOF STATE]
proof (state)
this:
b' = (1 - bs ! i) / 2

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x x0_le_x1 i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
i < k
[PROOF STEP]
have x'_le_x: "?x' \<le> x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
i < k

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m = "max (?x' powr (p + 1)) (x powr (p + 1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define m' where "m' = max 1 (?x'' powr (p + 1))"
[PROOF STATE]
proof (state)
this:
m' = max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have [simp]: "bs ! i > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < bs ! i
[PROOF STEP]
by (intro b_pos nth_mem) (simp add: i length_bs)
[PROOF STATE]
proof (state)
this:
0 < bs ! i

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x x0_le_x1 i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
i < k
[PROOF STEP]
have x'_pos: "?x' > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
i < k

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have m_pos: "?m > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
unfolding max_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (if (bs ! i * x + (hs ! i) x) powr (p + 1) \<le> x powr (p + 1) then x powr (p + 1) else (bs ! i * x + (hs ! i) x) powr (p + 1))
[PROOF STEP]
using x_pos step_pos[OF i x]
[PROOF STATE]
proof (prove)
using this:
0 < x
0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. 0 < (if (bs ! i * x + (hs ! i) x) powr (p + 1) \<le> x powr (p + 1) then x powr (p + 1) else (bs ! i * x + (hs ! i) x) powr (p + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with x x0_le_x1 c1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
0 < c1
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u
0 < max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
have c1_g_m_nonneg: "c1 * g x / ?m \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
0 < c1
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u
0 < max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))

goal (1 subgoal):
 1. 0 \<le> c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
by (intro mult_nonneg_nonneg divide_nonneg_pos g_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x i g_nonneg x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "c3 * (g x / x powr p) \<le> (c1*b'/m') * (g x / x powr p)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. c3 * (g x / x powr p) \<le> c1 * b' / m' * (g x / x powr p)
[PROOF STEP]
unfolding m'_def b'_def
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. c3 * (g x / x powr p) \<le> c1 * ((1 - bs ! i) / 2) / max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) * (g x / x powr p)
[PROOF STEP]
by (intro mult_right_mono c3) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
c3 * (g x / x powr p) \<le> c1 * b' / m' * (g x / x powr p)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c3 * (g x / x powr p) \<le> c1 * b' / m' * (g x / x powr p)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x_pos
[PROOF STATE]
proof (chain)
picking this:
0 < x
[PROOF STEP]
have "... = (x * b') * (c1 * g x / (x powr (p + 1) * m'))"
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. c1 * b' / m' * (g x / x powr p) = x * b' * (c1 * g x / (x powr (p + 1) * m'))
[PROOF STEP]
by (simp add: field_simps powr_add)
[PROOF STATE]
proof (state)
this:
c1 * b' / m' * (g x / x powr p) = x * b' * (c1 * g x / (x powr (p + 1) * m'))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c1 * b' / m' * (g x / x powr p) = x * b' * (c1 * g x / (x powr (p + 1) * m'))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x i c1_pos x1_pos x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < c1
0 < x\<^sub>1
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "... \<le> (x - ?x') * (c1 * g x / (x powr (p + 1) * m'))"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < c1
0 < x\<^sub>1
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x * b' * (c1 * g x / (x powr (p + 1) * m')) \<le> (x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / (x powr (p + 1) * m'))
[PROOF STEP]
unfolding b'_def m'_def
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < c1
0 < x\<^sub>1
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x * ((1 - bs ! i) / 2) * (c1 * g x / (x powr (p + 1) * max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)))) \<le> (x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / (x powr (p + 1) * max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))))
[PROOF STEP]
by (intro x0_hb_bound6 mult_right_mono mult_nonneg_nonneg
                                        divide_nonneg_nonneg g_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
x * b' * (c1 * g x / (x powr (p + 1) * m')) \<le> (x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / (x powr (p + 1) * m'))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * b' * (c1 * g x / (x powr (p + 1) * m')) \<le> (x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / (x powr (p + 1) * m'))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x powr (p + 1) * m' =
                 max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr (p + 1) * m' = max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)
[PROOF STEP]
unfolding m'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr (p + 1) * max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) = max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. x powr (p + 1) * max 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) = max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)
[PROOF STEP]
by (subst max.commute, intro max_mult_left) simp
[PROOF STATE]
proof (state)
this:
x powr (p + 1) * m' = max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x powr (p + 1) * m' = max (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) =
                 (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "... = (bs ! i * x + (hs ! i) x) powr (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1) = (bs ! i * x + (hs ! i) x) powr (p + 1)
[PROOF STEP]
using x x1_pos step_pos[OF i x] x_pos i x0_le_x1 x_pos
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
0 < x\<^sub>1
0 < bs ! i * x + (hs ! i) x
0 < x
i < k
x\<^sub>0 \<le> x\<^sub>1
0 < x

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1) = (bs ! i * x + (hs ! i) x) powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x powr (p + 1) * 1 = x powr (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr (p + 1) * 1 = x powr (p + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x powr (p + 1) * 1 = x powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x powr (p + 1) * 1 = x powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(x - ?x') * (c1 * g x / ?m) = integral (\<lambda>_. c1 * g x / ?m) ?x' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) = integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
using x'_le_x
[PROOF STATE]
proof (prove)
using this:
bs ! i * x + (hs ! i) x \<le> x

goal (1 subgoal):
 1. (x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) = integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
by (subst integral_const[OF c1_g_m_nonneg]) auto
[PROOF STATE]
proof (state)
this:
(x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) = integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) = integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(x - (bs ! i * x + (hs ! i) x)) * (c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) = integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "u powr (p + 1) \<le> ?m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u powr (p + 1) \<le> max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
using x u x'_pos
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. u powr (p + 1) \<le> max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
by (intro powr_upper_bound mult_pos_pos) simp_all
[PROOF STATE]
proof (state)
this:
u powr (p + 1) \<le> max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x'_pos u
[PROOF STATE]
proof (chain)
picking this:
0 < bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
[PROOF STEP]
have "u \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x

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

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> u

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c1 and u
[PROOF STATE]
proof (chain)
picking this:
0 < c1
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
[PROOF STEP]
have "c1 * g x \<le> g u"
[PROOF STATE]
proof (prove)
using this:
0 < c1
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u
bs ! i * x + (hs ! i) x \<le> u
u \<le> x

goal (1 subgoal):
 1. c1 * g x \<le> g u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c1 * g x \<le> g u

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u powr (p + 1) \<le> max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
0 \<le> u
c1 * g x \<le> g u
[PROOF STEP]
have "c1 * g x * u powr (p + 1) \<le> g u * ?m"
[PROOF STATE]
proof (prove)
using this:
u powr (p + 1) \<le> max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
0 \<le> u
c1 * g x \<le> g u

goal (1 subgoal):
 1. c1 * g x * u powr (p + 1) \<le> g u * max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
using c1 x u x0_hb_bound7[OF x i]
[PROOF STATE]
proof (prove)
using this:
u powr (p + 1) \<le> max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
0 \<le> u
c1 * g x \<le> g u
0 < c1
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. c1 * g x \<le> g u
x\<^sub>1 \<le> x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. c1 * g x * u powr (p + 1) \<le> g u * max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
by (intro mult_mono g_nonneg) auto
[PROOF STATE]
proof (state)
this:
c1 * g x * u powr (p + 1) \<le> g u * max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with m_pos u step_pos[OF i x]
[PROOF STATE]
proof (chain)
picking this:
0 < max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
0 < bs ! i * x + (hs ! i) x
c1 * g x * u powr (p + 1) \<le> g u * max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
[PROOF STEP]
have "c1 * g x / ?m \<le> g u / u powr (p + 1)"
[PROOF STATE]
proof (prove)
using this:
0 < max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
0 < bs ! i * x + (hs ! i) x
c1 * g x * u powr (p + 1) \<le> g u * max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))

goal (1 subgoal):
 1. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> g u / u powr (p + 1)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> g u / u powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>bs ! i * x + (hs ! i) x \<le> ?u2; ?u2 \<le> x\<rbrakk> \<Longrightarrow> c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> g ?u2 / ?u2 powr (p + 1)

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "integral (\<lambda>_. c1 * g x / ?m) ?x' x \<le> integral (\<lambda>u. g u / u powr (p + 1)) ?x' x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bs ! i * x + (hs ! i) x \<le> ?u2; ?u2 \<le> x\<rbrakk> \<Longrightarrow> c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> g ?u2 / ?u2 powr (p + 1)

goal (1 subgoal):
 1. integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
using x0_hb_bound7[OF x i] x'_le_x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bs ! i * x + (hs ! i) x \<le> ?u2; ?u2 \<le> x\<rbrakk> \<Longrightarrow> c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> g ?u2 / ?u2 powr (p + 1)
x\<^sub>0 < bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> x

goal (1 subgoal):
 1. integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
by (intro integral_le ballI akra_bazzi_integrable integrable_const c1_g_m_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
integral (\<lambda>_. c1 * g x / max ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c3 * (g x / x powr p) \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
have "c3 * g x \<le> g_approx i x"
[PROOF STATE]
proof (prove)
using this:
c3 * (g x / x powr p) \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. c3 * g x \<le> g_approx i x
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
c3 * (g x / x powr p) \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
0 < x

goal (1 subgoal):
 1. c3 * g x \<le> g_approx i x
[PROOF STEP]
unfolding g_approx_def
[PROOF STATE]
proof (prove)
using this:
c3 * (g x / x powr p) \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
0 < x

goal (1 subgoal):
 1. c3 * g x \<le> x powr p * integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
c3 * g x \<le> g_approx i x

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>1 \<le> ?x2; ?i2 < k\<rbrakk> \<Longrightarrow> c3 * g ?x2 \<le> g_approx ?i2 ?x2

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x2; ?i2 < k\<rbrakk> \<Longrightarrow> c3 * g ?x2 \<le> g_approx ?i2 ?x2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that \<open>c3 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x2; ?i2 < k\<rbrakk> \<Longrightarrow> c3 * g ?x2 \<le> g_approx ?i2 ?x2
\<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> ?c3.0 * g x \<le> g_approx i x; 0 < ?c3.0\<rbrakk> \<Longrightarrow> thesis
0 < c3

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_bounded_above:
  assumes c': "c' > 0"
  obtains c where "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> f x \<le> (1/2) * (c * f_approx x)" "c \<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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain c where c: "\<And>x. x\<^sub>0 \<le> x \<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]
by (rule f_approx_bounded_below) blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx ?x
0 < c

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have fb1_nonneg: "fb1 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> fb1
[PROOF STEP]
using f_base1[of "x\<^sub>0"] f_nonneg[of x\<^sub>0] x0_le_x1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> x\<^sub>0; x\<^sub>0 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x\<^sub>0 \<le> fb1
x\<^sub>0 \<le> x\<^sub>0 \<Longrightarrow> 0 \<le> f x\<^sub>0
x\<^sub>0 \<le> x\<^sub>1

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 \<le> fb1

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with f_base1 x0_pos
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> fb1
0 < x\<^sub>0
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
have "f x \<le> fb1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> fb1
0 < x\<^sub>0
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f x \<le> fb1

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c and x
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx ?x
0 < c
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
have "f_approx x \<ge> c"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx ?x
0 < c
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. c \<le> f_approx x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f x \<le> fb1
c \<le> f_approx x
[PROOF STEP]
have "f x * c \<le> fb1 * f_approx x"
[PROOF STATE]
proof (prove)
using this:
f x \<le> fb1
c \<le> f_approx x

goal (1 subgoal):
 1. f x * c \<le> fb1 * f_approx x
[PROOF STEP]
using c fb1_nonneg
[PROOF STATE]
proof (prove)
using this:
f x \<le> fb1
c \<le> f_approx x
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx ?x
0 < c
0 \<le> fb1

goal (1 subgoal):
 1. f x * c \<le> fb1 * f_approx x
[PROOF STEP]
by (intro mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
f x * c \<le> fb1 * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x * c \<le> fb1 * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from f_approx_nonneg x
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> f_approx ?x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
have "... \<le> (fb1 + 1) * f_approx x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> f_approx ?x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. fb1 * f_approx x \<le> (fb1 + 1) * f_approx x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
fb1 * f_approx x \<le> (fb1 + 1) * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f x * c \<le> (fb1 + 1) * f_approx x
[PROOF STEP]
have "f x \<le> ((fb1+1) / c) * f_approx x"
[PROOF STATE]
proof (prove)
using this:
f x * c \<le> (fb1 + 1) * f_approx x

goal (1 subgoal):
 1. f x \<le> (fb1 + 1) / c * f_approx x
[PROOF STEP]
by (simp add: field_simps c)
[PROOF STATE]
proof (state)
this:
f x \<le> (fb1 + 1) / c * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x \<le> (fb1 + 1) / c * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "... \<le> max ((fb1+1) / c) c' * f_approx x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fb1 + 1) / c * f_approx x \<le> max ((fb1 + 1) / c) c' * f_approx x
[PROOF STEP]
by (intro mult_right_mono) (simp_all add: f_approx_nonneg x)
[PROOF STATE]
proof (state)
this:
(fb1 + 1) / c * f_approx x \<le> max ((fb1 + 1) / c) c' * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f x \<le> max ((fb1 + 1) / c) c' * f_approx x
[PROOF STEP]
have "f x \<le> 1/2 * (max ((fb1+1) / c) c' * 2 * f_approx x)"
[PROOF STATE]
proof (prove)
using this:
f x \<le> max ((fb1 + 1) / c) c' * f_approx x

goal (1 subgoal):
 1. f x \<le> 1 / 2 * (max ((fb1 + 1) / c) c' * 2 * f_approx x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x \<le> 1 / 2 * (max ((fb1 + 1) / c) c' * 2 * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 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> f ?x2 \<le> 1 / 2 * (max ((fb1 + 1) / c) c' * 2 * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x2 \<le> 1 / 2 * (max ((fb1 + 1) / c) c' * 2 * 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> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "max ((fb1+1) / c) c' * 2 \<ge> max ((fb1+1) / c) c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max ((fb1 + 1) / c) c' \<le> max ((fb1 + 1) / c) c' * 2
[PROOF STEP]
by (subst mult_le_cancel_left1) (insert c', simp)
[PROOF STATE]
proof (state)
this:
max ((fb1 + 1) / c) c' \<le> max ((fb1 + 1) / c) c' * 2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "max ((fb1+1) / c) c' * 2 \<ge> c'"
[PROOF STATE]
proof (prove)
using this:
max ((fb1 + 1) / c) c' \<le> max ((fb1 + 1) / c) c' * 2

goal (1 subgoal):
 1. c' \<le> max ((fb1 + 1) / c) c' * 2
[PROOF STEP]
by (rule order.trans[OF max.cobounded2])
[PROOF STATE]
proof (state)
this:
c' \<le> max ((fb1 + 1) / c) c' * 2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c' \<le> max ((fb1 + 1) / c) c' * 2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from fb1_nonneg and c
[PROOF STATE]
proof (chain)
picking this:
0 \<le> fb1
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx ?x
0 < c
[PROOF STEP]
have "(fb1+1) / c > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> fb1
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c \<le> f_approx ?x
0 < c

goal (1 subgoal):
 1. 0 < (fb1 + 1) / c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < (fb1 + 1) / c

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "max ((fb1+1) / c) c' * 2 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < (fb1 + 1) / c

goal (1 subgoal):
 1. 0 < max ((fb1 + 1) / c) c' * 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < max ((fb1 + 1) / c) c' * 2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c * f_approx x); c' \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x2 \<le> 1 / 2 * (max ((fb1 + 1) / c) c' * 2 * f_approx ?x2)
c' \<le> max ((fb1 + 1) / c) c' * 2
0 < max ((fb1 + 1) / c) c' * 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x2 \<le> 1 / 2 * (max ((fb1 + 1) / c) c' * 2 * f_approx ?x2)
c' \<le> max ((fb1 + 1) / c) c' * 2
0 < max ((fb1 + 1) / c) c' * 2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed