[STATEMENT]
lemma f_approx_bounded_above:
  obtains c where "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> f_approx x \<le> 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_approx x \<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_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m1 = "max (x\<^sub>0 powr p) (x\<^sub>1 powr p)"
[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_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m2 = "max (x\<^sub>0 powr (-(p+1))) (x\<^sub>1 powr (-(p+1)))"
[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_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m3 = "gb2 * ?m2"
[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_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m4 = "1 + (x\<^sub>1 - x\<^sub>0) * ?m3"
[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_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?int = "\<lambda>x. integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 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_approx x \<le> c; 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> f_approx x \<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_approx x \<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_approx x \<le> c; 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 \<le> ?m1" "?m1 \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < x\<^sub>0
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

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

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

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix u
[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_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume u: "u \<in> {x\<^sub>0..x}"
[PROOF STATE]
proof (state)
this:
u \<in> {x\<^sub>0..x}

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "g u / u powr (p + 1) = g u * u powr (-(p+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g u / u powr (p + 1) = g u * u powr - (p + 1)
[PROOF STEP]
by (subst powr_minus) (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
g u / u powr (p + 1) = g u * u powr - (p + 1)

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from u x x0_pos
[PROOF STATE]
proof (chain)
picking this:
u \<in> {x\<^sub>0..x}
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 < x\<^sub>0
[PROOF STEP]
have "u powr (-(p+1)) \<le> ?m2"
[PROOF STATE]
proof (prove)
using this:
u \<in> {x\<^sub>0..x}
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 < x\<^sub>0

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "g u * u powr (-(p+1)) \<le> g u * ?m2"
[PROOF STATE]
proof (prove)
using this:
u powr - (p + 1) \<le> max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. g u * u powr - (p + 1) \<le> g u * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
[PROOF STEP]
using u g_nonneg x0_pos
[PROOF STATE]
proof (prove)
using this:
u powr - (p + 1) \<le> max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
u \<in> {x\<^sub>0..x}
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
0 < x\<^sub>0

goal (1 subgoal):
 1. g u * u powr - (p + 1) \<le> g u * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
[PROOF STEP]
by (intro mult_left_mono) simp_all
[PROOF STATE]
proof (state)
this:
g u * u powr - (p + 1) \<le> g u * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g u * u powr - (p + 1) \<le> g u * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x u x0_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
u \<in> {x\<^sub>0..x}
0 < x\<^sub>0
[PROOF STEP]
have "g u \<le> gb2"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
u \<in> {x\<^sub>0..x}
0 < x\<^sub>0

goal (1 subgoal):
 1. g u \<le> gb2
[PROOF STEP]
by (intro g_bounded) simp_all
[PROOF STATE]
proof (state)
this:
g u \<le> gb2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "g u * ?m2 \<le> gb2 * ?m2"
[PROOF STATE]
proof (prove)
using this:
g u \<le> gb2

goal (1 subgoal):
 1. g u * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
[PROOF STEP]
by (intro mult_right_mono) (simp_all add: max_def)
[PROOF STATE]
proof (state)
this:
g u * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g u / u powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
[PROOF STEP]
have "g u / u powr (p + 1) \<le> ?m3"
[PROOF STATE]
proof (prove)
using this:
g u / u powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. g u / u powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
g u / u powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?u2 \<in> {x\<^sub>0..x} \<Longrightarrow> g ?u2 / ?u2 powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note A = this
[PROOF STATE]
proof (state)
this:
?u2 \<in> {x\<^sub>0..x} \<Longrightarrow> g ?u2 / ?u2 powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?u2 \<in> {x\<^sub>0..x} \<Longrightarrow> g ?u2 / ?u2 powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from A x gb2_nonneg
[PROOF STATE]
proof (chain)
picking this:
?u2 \<in> {x\<^sub>0..x} \<Longrightarrow> g ?u2 / ?u2 powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 \<le> gb2
[PROOF STEP]
have "?int x \<le> integral (\<lambda>_. ?m3) x\<^sub>0 x"
[PROOF STATE]
proof (prove)
using this:
?u2 \<in> {x\<^sub>0..x} \<Longrightarrow> g ?u2 / ?u2 powr (p + 1) \<le> gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 \<le> gb2

goal (1 subgoal):
 1. integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> integral (\<lambda>_. gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) x\<^sub>0 x
[PROOF STEP]
by (intro integral_le akra_bazzi_integrable integrable_const mult_nonneg_nonneg)
           (simp_all add: le_max_iff_disj)
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> integral (\<lambda>_. gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) x\<^sub>0 x

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> integral (\<lambda>_. gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) x\<^sub>0 x

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x gb2_nonneg
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 \<le> gb2
[PROOF STEP]
have "... \<le> (x - x\<^sub>0) * ?m3"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 \<le> gb2

goal (1 subgoal):
 1. integral (\<lambda>_. gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) x\<^sub>0 x \<le> (x - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))
[PROOF STEP]
by (subst integral_const) (simp_all add: le_max_iff_disj)
[PROOF STATE]
proof (state)
this:
integral (\<lambda>_. gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) x\<^sub>0 x \<le> (x - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (\<lambda>_. gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) x\<^sub>0 x \<le> (x - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x gb2_nonneg
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 \<le> gb2
[PROOF STEP]
have "... \<le> (x\<^sub>1 - x\<^sub>0) * ?m3"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
0 \<le> gb2

goal (1 subgoal):
 1. (x - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) \<le> (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))
[PROOF STEP]
by (intro mult_right_mono mult_nonneg_nonneg) (simp_all add: max_def)
[PROOF STATE]
proof (state)
this:
(x - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))) \<le> (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))
[PROOF STEP]
have "1 + ?int x \<le> ?m4"
[PROOF STATE]
proof (prove)
using this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> 1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> 1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))

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

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 akra_bazzi_integrable) (simp_all add: powr_def field_simps)
[PROOF STATE]
proof (state)
this:
0 \<le> integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "1 + ?int x \<ge> 0"
[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. 0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x powr p \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p)
0 \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p)
1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> 1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))
0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
have "f_approx x \<le> ?m1 * ?m4"
[PROOF STATE]
proof (prove)
using this:
x powr p \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p)
0 \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p)
1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> 1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))
0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

goal (1 subgoal):
 1. f_approx x \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p) * (1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))))
[PROOF STEP]
unfolding f_approx_def
[PROOF STATE]
proof (prove)
using this:
x powr p \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p)
0 \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p)
1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x \<le> 1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))
0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<le> c; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "f_approx x \<le> max 1 (?m1 * ?m4)"
[PROOF STATE]
proof (prove)
using this:
f_approx x \<le> max (x\<^sub>0 powr p) (x\<^sub>1 powr p) * (1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1))))

goal (1 subgoal):
 1. f_approx x \<le> max 1 (max (x\<^sub>0 powr p) (x\<^sub>1 powr p) * (1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f_approx x \<le> max 1 (max (x\<^sub>0 powr p) (x\<^sub>1 powr p) * (1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))))

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx x \<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_approx ?x2 \<le> max 1 (max (x\<^sub>0 powr p) (x\<^sub>1 powr p) * (1 + (x\<^sub>1 - x\<^sub>0) * (gb2 * max (x\<^sub>0 powr - (p + 1)) (x\<^sub>1 powr - (p + 1)))))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. inverse c * f_approx x \<le> 1
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
inverse c * f_approx x \<le> 1

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

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

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

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

goal (1 subgoal):
 1. inverse c * f_approx x * fb2 \<le> 1 * f x
[PROOF STEP]
using fb2_pos
[PROOF STATE]
proof (prove)
using this:
inverse c * f_approx x \<le> 1
fb2 \<le> f x
0 < fb2

goal (1 subgoal):
 1. inverse c * f_approx x * fb2 \<le> 1 * f x
[PROOF STEP]
by (intro mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
inverse c * f_approx x * fb2 \<le> 1 * f x

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

goal (1 subgoal):
 1. inverse c * fb2 * f_approx x \<le> f x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
inverse c * fb2 * f_approx x \<le> f x

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c * f_approx x) \<le> f x; c \<le> c'; 0 < c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "min c' (inverse c * fb2) * f_approx x \<le> inverse c * fb2 * f_approx x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min c' (inverse c * fb2) * f_approx x \<le> inverse c * fb2 * f_approx x
[PROOF STEP]
using f_approx_nonneg x c
[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
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f_approx ?x \<le> c
0 < c

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

goal (1 subgoal):
 1. 2 * (min c' (inverse c * fb2) / 2 * f_approx x) \<le> f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * (min c' (inverse c * fb2) / 2 * f_approx x) \<le> f x

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c * f_approx x) \<le> f 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> 2 * (min c' (inverse c * fb2) / 2 * f_approx ?x2) \<le> f ?x2

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c * f_approx x) \<le> f 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> 2 * (min c' (inverse c * fb2) / 2 * f_approx ?x2) \<le> f ?x2

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

goal (1 subgoal):
 1. min c' (inverse c * fb2) / 2 \<le> c'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
min c' (inverse c * fb2) / 2 \<le> c'

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

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

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

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c * f_approx x) \<le> f 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> 2 * (min c' (inverse c * fb2) / 2 * f_approx ?x2) \<le> f ?x2
min c' (inverse c * fb2) / 2 \<le> c'
0 < min c' (inverse c * fb2) / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x2; ?x2 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (min c' (inverse c * fb2) / 2 * f_approx ?x2) \<le> f ?x2
min c' (inverse c * fb2) / 2 \<le> c'
0 < min c' (inverse c * fb2) / 2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma akra_bazzi_lower:
  obtains c5 where "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> f x \<ge> c5 * f_approx x" "c5 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain c4 where c4: "\<And>x i. x \<ge> x\<^sub>1 \<Longrightarrow> i < k \<Longrightarrow> g_approx i x \<le> c4 * g x" "c4 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule g_bounds2) blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> g_approx ?i ?x \<le> c4 * g ?x
0 < c4

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "inverse c4 / 2 > 0"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> g_approx ?i ?x \<le> c4 * g ?x
0 < c4

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

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < inverse c4 / 2
[PROOF STEP]
obtain c5 where c5: "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> 2 * (c5 * f_approx x) \<le> f x"
                           "c5 \<le> inverse c4 / 2" "c5 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < inverse c4 / 2

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx x) \<le> f x; c5 \<le> inverse c4 / 2; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule f_bounded_below) blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5

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

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume x: "x \<ge> x\<^sub>0"
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c5 x
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
x\<^sub>0 \<le> x
[PROOF STEP]
have  " c5 * 1 * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. c5 * 1 * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
by (intro mult_right_mono mult_left_mono f_approx_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
c5 * 1 * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * 1 * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
[PROOF STEP]
have "c5 * (1 + ln x powr (-e/2)) * f_approx x \<le> f x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. c5 * (1 + ln x powr (- e / 2)) * f_approx x \<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> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<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> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
have "1 + ln x powr (-e/2) \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + ln x powr (- e / 2) \<le> 2
[PROOF STEP]
using asymptotics3 base
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> ?x \<Longrightarrow> (1 + ln ?x powr (- e / 2)) / 2 \<le> 1
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

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

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
hence "(1 + ln x powr (-e/2)) * (c5 * f_approx x) \<le> 2 * (c5 * f_approx x)"
[PROOF STATE]
proof (prove)
using this:
1 + ln x powr (- e / 2) \<le> 2

goal (1 subgoal):
 1. (1 + ln x powr (- e / 2)) * (c5 * f_approx x) \<le> 2 * (c5 * f_approx x)
[PROOF STEP]
using c5 f_approx_nonneg base x0_ge_1
[PROOF STATE]
proof (prove)
using this:
1 + ln x powr (- e / 2) \<le> 2
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> f_approx ?x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. (1 + ln x powr (- e / 2)) * (c5 * f_approx x) \<le> 2 * (c5 * f_approx x)
[PROOF STEP]
by (intro mult_right_mono mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
(1 + ln x powr (- e / 2)) * (c5 * f_approx x) \<le> 2 * (c5 * f_approx x)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 + ln x powr (- e / 2)) * (c5 * f_approx x) \<le> 2 * (c5 * f_approx x)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
from base
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
have "2 * (c5 * f_approx x) \<le> f x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. 2 * (c5 * f_approx x) \<le> f x
[PROOF STEP]
by (intro c5) simp_all
[PROOF STATE]
proof (state)
this:
2 * (c5 * f_approx x) \<le> f x

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1 + ln x powr (- e / 2)) * (c5 * f_approx x) \<le> f x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(1 + ln x powr (- e / 2)) * (c5 * f_approx x) \<le> f x

goal (1 subgoal):
 1. c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<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> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
case (rec x)
[PROOF STATE]
proof (state)
this:
x\<^sub>1 < x
?i < k \<Longrightarrow> c5 * (1 + ln (bs ! ?i * x + (hs ! ?i) x) powr (- e / 2)) * f_approx (bs ! ?i * x + (hs ! ?i) x) \<le> f (bs ! ?i * x + (hs ! ?i) x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
let ?a = "\<lambda>i. as!i" and ?b = "\<lambda>i. bs!i" and ?h = "\<lambda>i. hs!i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
let ?int = "integral (\<lambda>u. g u / u powr (p+1)) x\<^sub>0 x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
let ?int1 = "\<lambda>i. integral (\<lambda>u. g u / u powr (p+1)) x\<^sub>0 (?b i*x+?h i x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
let ?int2 = "\<lambda>i. integral (\<lambda>u. g u / u powr (p+1)) (?b i*x+?h i x) x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
let ?l = "ln x powr (-e/2)" and ?l' = "\<lambda>i. ln (?b i*x + ?h i x) powr (-e/2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
from rec and x0_le_x1 x0_ge_1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
?i < k \<Longrightarrow> c5 * (1 + ln (bs ! ?i * x + (hs ! ?i) x) powr (- e / 2)) * f_approx (bs ! ?i * x + (hs ! ?i) x) \<le> f (bs ! ?i * x + (hs ! ?i) x)
x\<^sub>0 \<le> x\<^sub>1
1 \<le> x\<^sub>0
[PROOF STEP]
have x: "x \<ge> x\<^sub>0" and x_gt_1: "x > 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
?i < k \<Longrightarrow> c5 * (1 + ln (bs ! ?i * x + (hs ! ?i) x) powr (- e / 2)) * f_approx (bs ! ?i * x + (hs ! ?i) x) \<le> f (bs ! ?i * x + (hs ! ?i) x)
x\<^sub>0 \<le> x\<^sub>1
1 \<le> x\<^sub>0

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
with x0_pos
[PROOF STATE]
proof (chain)
picking this:
0 < x\<^sub>0
x\<^sub>0 \<le> x
1 < x
[PROOF STEP]
have x_pos: "x > 0" and x_nonneg: "x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < x\<^sub>0
x\<^sub>0 \<le> x
1 < x

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
from c5 c4
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> g_approx ?i ?x \<le> c4 * g ?x
0 < c4
[PROOF STEP]
have "c5 * c4 \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> g_approx ?i ?x \<le> c4 * g ?x
0 < c4

goal (1 subgoal):
 1. c5 * c4 \<le> 1 / 2
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
c5 * c4 \<le> 1 / 2

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c5 * c4 \<le> 1 / 2

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
from asymptotics3 x
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> ?x \<Longrightarrow> (1 + ln ?x powr (- e / 2)) / 2 \<le> 1
x\<^sub>0 \<le> x
[PROOF STEP]
have "(1 + ?l) \<le> 2"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> ?x \<Longrightarrow> (1 + ln ?x powr (- e / 2)) / 2 \<le> 1
x\<^sub>0 \<le> x

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c5 * c4 \<le> 1 / 2
1 + ln x powr (- e / 2) \<le> 2
[PROOF STEP]
have "(c5*c4)*(1 + ?l) \<le> (1/2) * 2"
[PROOF STATE]
proof (prove)
using this:
c5 * c4 \<le> 1 / 2
1 + ln x powr (- e / 2) \<le> 2

goal (1 subgoal):
 1. c5 * c4 * (1 + ln x powr (- e / 2)) \<le> 1 / 2 * 2
[PROOF STEP]
by (rule mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
c5 * c4 * (1 + ln x powr (- e / 2)) \<le> 1 / 2 * 2

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
hence "0 \<le> 1 - c5*c4*(1 + ?l)"
[PROOF STATE]
proof (prove)
using this:
c5 * c4 * (1 + ln x powr (- e / 2)) \<le> 1 / 2 * 2

goal (1 subgoal):
 1. 0 \<le> 1 - c5 * c4 * (1 + ln x powr (- e / 2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> 1 - c5 * c4 * (1 + ln x powr (- e / 2))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
with g_nonneg[OF x]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> g x
0 \<le> 1 - c5 * c4 * (1 + ln x powr (- e / 2))
[PROOF STEP]
have "0 \<le> g x * ..."
[PROOF STATE]
proof (prove)
using this:
0 \<le> g x
0 \<le> 1 - c5 * c4 * (1 + ln x powr (- e / 2))

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
hence "c5 * (1 + ?l) * f_approx x \<le> c5 * (1 + ?l) * f_approx x + g x - c5*c4*(1 + ?l) * g x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> g x * (1 - c5 * c4 * (1 + ln x powr (- e / 2)))

goal (1 subgoal):
 1. c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x + g x - c5 * c4 * (1 + ln x powr (- e / 2)) * g x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x + g x - c5 * c4 * (1 + ln x powr (- e / 2)) * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> c5 * (1 + ln x powr (- e / 2)) * f_approx x + g x - c5 * c4 * (1 + ln x powr (- e / 2)) * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
from x_gt_1
[PROOF STATE]
proof (chain)
picking this:
1 < x
[PROOF STEP]
have "... = c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p) + g x"
[PROOF STATE]
proof (prove)
using this:
1 < x

goal (1 subgoal):
 1. c5 * (1 + ln x powr (- e / 2)) * f_approx x + g x - c5 * c4 * (1 + ln x powr (- e / 2)) * g x = c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) + g x
[PROOF STEP]
by (simp add: field_simps f_approx_def powr_minus)
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x + g x - c5 * c4 * (1 + ln x powr (- e / 2)) * g x = c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x + g x - c5 * c4 * (1 + ln x powr (- e / 2)) * g x = c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
have "c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p) =
                 (\<Sum>i<k. (?a i * ?b i powr p) * (c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) = (\<Sum>i<k. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)))
[PROOF STEP]
by (subst sum_distrib_right[symmetric]) (simp add: p_props)
[PROOF STATE]
proof (state)
this:
c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) = (\<Sum>i<k. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) = (\<Sum>i<k. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
have "... \<le> (\<Sum>i<k. ?a i * f (?b i*x + ?h i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p))) \<le> (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))
[PROOF STEP]
proof (intro sum_mono, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (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> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
let ?f = "c5 * ?a i * (?b i * x) powr p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from rec.hyps i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
i < k
[PROOF STEP]
have "x\<^sub>0 < bs ! i * x + (hs ! i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k

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

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
hence "1 + ?int1 i \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

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

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
hence int_nonneg: "1 + ?int1 i \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

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

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "(?a i * ?b i powr p) * (c5 * x powr p * (1 + ?l) * (1 + ?int - c4*g x/x powr p)) =
            ?f * (1 + ?l) * (1 + ?int - c4*g x/x powr p)" (is "?expr = ?A * ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) = c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)
[PROOF STEP]
using x_pos b_pos[of "bs!i"] i
[PROOF STATE]
proof (prove)
using this:
0 < x
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
i < k

goal (1 subgoal):
 1. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) = c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)
[PROOF STEP]
by (subst powr_mult) simp_all
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) = c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) = c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from rec.hyps i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
i < k
[PROOF STEP]
have "g_approx i x \<le> c4 * g x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k

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

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
hence "c4*g x/x powr p \<ge> ?int2 i"
[PROOF STATE]
proof (prove)
using this:
g_approx i x \<le> c4 * g x

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

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

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

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
hence "?A * ?B \<le> ?A * (1 + (?int - ?int2 i))"
[PROOF STATE]
proof (prove)
using this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * g x / x powr p

goal (1 subgoal):
 1. c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) \<le> c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x))
[PROOF STEP]
using i c5 a_ge_0
[PROOF STATE]
proof (prove)
using this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * g x / x powr p
i < k
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
?a \<in> set as \<Longrightarrow> 0 \<le> ?a

goal (1 subgoal):
 1. c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) \<le> c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x))
[PROOF STEP]
by (intro mult_left_mono mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) \<le> c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p) \<le> c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from rec.hyps i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
i < k
[PROOF STEP]
have "x\<^sub>0 < bs ! i * x + (hs ! i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k

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

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
hence "?int - ?int2 i = ?int1 i"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)
[PROOF STEP]
apply (subst diff_eq_eq, subst eq_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>0 < bs ! i * x + (hs ! i) x; x\<^sub>0 < bs ! i * x + (hs ! i) x\<rbrakk> \<Longrightarrow> integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x) + integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
apply (intro integral_combine akra_bazzi_integrable)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x\<^sub>0 < bs ! i * x + (hs ! i) x; x\<^sub>0 < bs ! i * x + (hs ! i) x\<rbrakk> \<Longrightarrow> x\<^sub>0 \<le> bs ! i * x + (hs ! i) x
 2. \<lbrakk>x\<^sub>0 < bs ! i * x + (hs ! i) x; x\<^sub>0 < bs ! i * x + (hs ! i) x\<rbrakk> \<Longrightarrow> bs ! i * x + (hs ! i) x \<le> x
 3. \<lbrakk>x\<^sub>0 < bs ! i * x + (hs ! i) x; x\<^sub>0 < bs ! i * x + (hs ! i) x\<rbrakk> \<Longrightarrow> x\<^sub>0 \<le> x\<^sub>0
 4. \<lbrakk>x\<^sub>0 < bs ! i * x + (hs ! i) x; x\<^sub>0 < bs ! i * x + (hs ! i) x\<rbrakk> \<Longrightarrow> x\<^sub>0 \<le> x
[PROOF STEP]
apply (insert rec.hyps step_le_x[OF i, of x], simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "?A * (1 + ?int1 i) = (c5*?a i*(1 + ?int1 i)) * ((?b i*x) powr p * (1 + ?l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) = c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2)))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) = c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) = c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "... \<le> (c5*?a i*(1 + ?int1 i)) * ((?b i*x + ?h i x) powr p * (1 + ?l' i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2))) \<le> c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))
[PROOF STEP]
using rec.hyps i c5 a_ge_0 int_nonneg
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 2 * (c5 * f_approx ?x) \<le> f ?x
c5 \<le> inverse c4 / 2
0 < c5
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2))) \<le> c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))
[PROOF STEP]
by (intro mult_left_mono asymptotics1' mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2))) \<le> c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 + ln x powr (- e / 2))) \<le> c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
have "... = ?a i*(c5*(1 + ?l' i)*f_approx (?b i*x + ?h i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))) = as ! i * (c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))
[PROOF STEP]
by (simp add: algebra_simps f_approx_def)
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))) = as ! i * (c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c5 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))) = as ! i * (c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < k
[PROOF STEP]
have "... \<le> ?a i * f (?b i*x + ?h i x)"
[PROOF STATE]
proof (prove)
using this:
i < k

goal (1 subgoal):
 1. as ! i * (c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (intro mult_left_mono a_ge_0 rec.IH) simp_all
[PROOF STATE]
proof (state)
this:
as ! i * (c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
show "?expr \<le> ?a i * f (?b i*x + ?h i x)"
[PROOF STATE]
proof (prove)
using this:
as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p)) \<le> as ! i * f (bs ! i * x + (hs ! i) x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p))) \<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> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * bs ! i powr p * (c5 * x powr p * (1 + ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c4 * g x / x powr p))) \<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> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
have "... + g x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x = f x
[PROOF STEP]
using f_rec[of x] rec.hyps x0_le_x1
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x \<Longrightarrow> f x = g x + (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))
x\<^sub>1 < x
x\<^sub>0 \<le> x\<^sub>1

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> c5 * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x) \<le> f (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + g x \<le> y + g x) \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + g x \<le> y + g x) \<Longrightarrow> c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x

goal (1 subgoal):
 1. c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c5 * (1 + ln x powr (- e / 2)) * f_approx x \<le> f x

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

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

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

goal (1 subgoal):
 1. (\<And>c5. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x; 0 < c5\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this and c5(3)
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> ?x2 \<Longrightarrow> c5 * f_approx ?x2 \<le> f ?x2
0 < c5
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> ?x2 \<Longrightarrow> c5 * f_approx ?x2 \<le> f ?x2
0 < c5

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma akra_bazzi_bigomega:
  "f \<in> \<Omega>(\<lambda>x. x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> \<Omega>(\<lambda>x. x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x))
[PROOF STEP]
apply (fold f_approx_def, rule akra_bazzi_lower, erule landau_omega.bigI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c5. (\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x) \<Longrightarrow> \<forall>\<^sub>F x in at_top. c5 * norm (f_approx x) \<le> norm (f x)
[PROOF STEP]
apply (subst eventually_at_top_linorder, rule exI[of _ x\<^sub>0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c5. (\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> c5 * f_approx x \<le> f x) \<Longrightarrow> \<forall>n\<ge>x\<^sub>0. c5 * norm (f_approx n) \<le> norm (f n)
[PROOF STEP]
apply (simp add: f_nonneg f_approx_nonneg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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

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

goal (1 subgoal):
 1. c1 * g x \<le> g u
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
have "u \<in> {C*x..x}"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
C * x \<le> bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. u \<in> {C * x..x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> {C * x..x}

goal (1 subgoal):
 1. c1 * g x \<le> g u
[PROOF STEP]
with assms g_growth1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
\<forall>x\<ge>x\<^sub>1. \<forall>u\<in>{C * x..x}. c1 * g x \<le> g u
u \<in> {C * x..x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
\<forall>x\<ge>x\<^sub>1. \<forall>u\<in>{C * x..x}. c1 * g x \<le> g u
u \<in> {C * x..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:
No subgoals!
[PROOF STEP]
qed