[STATEMENT]
lemma eval_fds_logderiv_zeta:
  assumes "Re s > 1"
  shows  "(\<lambda>p. of_real (ln (real p)) / (p powr s - 1))
            abs_summable_on {p. prime p}" (is ?th1)
    and  "deriv zeta s / zeta s =
            -(\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) / (p powr s - 1))" (is ?th2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p} &&& deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
 2. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have *: "completely_multiplicative_function (fds_nth fds_zeta :: _ \<Rightarrow> complex)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth fds_zeta)
[PROOF STEP]
by standard auto
[PROOF STATE]
proof (state)
this:
completely_multiplicative_function (fds_nth fds_zeta)

goal (2 subgoals):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
 2. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
note abscissa = le_less_trans[OF abs_conv_abscissa_completely_multiplicative_log_deriv[OF *]]
[PROOF STATE]
proof (state)
this:
\<lbrakk>fds_nth fds_zeta 1 \<noteq> 0; abs_conv_abscissa fds_zeta < ?z\<rbrakk> \<Longrightarrow> abs_conv_abscissa (fds_deriv fds_zeta / fds_zeta) < ?z

goal (2 subgoals):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
 2. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have "(\<lambda>p. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))
           abs_summable_on {p. prime p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}
[PROOF STEP]
using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fds_nth fds_zeta 1 \<noteq> 0; abs_conv_abscissa fds_zeta < ereal (s \<bullet> 1)\<rbrakk> \<Longrightarrow> (\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / nat_power p s) - 1)) abs_summable_on {p. prime p}
\<lbrakk>fds_nth fds_zeta 1 \<noteq> 0; abs_conv_abscissa fds_zeta < ereal (s \<bullet> 1)\<rbrakk> \<Longrightarrow> eval_fds (fds_deriv fds_zeta / fds_zeta) s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / nat_power p s) - 1))
1 < Re s

goal (1 subgoal):
 1. (\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}

goal (2 subgoals):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
 2. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}

goal (2 subgoals):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
 2. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have "?this \<longleftrightarrow> (\<lambda>p. ln (real p) / (p powr s - 1)) abs_summable_on {p. prime p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}) = ((\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < Re s

goal (1 subgoal):
 1. ((\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}) = ((\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p})
[PROOF STEP]
by (intro abs_summable_on_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
((\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) abs_summable_on {p. prime p}) = ((\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p})

goal (2 subgoals):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
 2. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
[PROOF STEP]
show ?th1
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}

goal (1 subgoal):
 1. (\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < Re s
[PROOF STEP]
have ev: "eventually (\<lambda>z. z \<in> {z. Re z > 1}) (nhds s)"
[PROOF STATE]
proof (prove)
using this:
1 < Re s

goal (1 subgoal):
 1. \<forall>\<^sub>F z in nhds s. z \<in> {z. 1 < Re z}
[PROOF STEP]
by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F z in nhds s. z \<in> {z. 1 < Re z}

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have "deriv zeta s = deriv (eval_fds fds_zeta) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv zeta s = deriv (eval_fds fds_zeta) s
[PROOF STEP]
by (intro deriv_cong_ev[OF eventually_mono[OF ev]]) (auto simp: eval_fds_zeta)
[PROOF STATE]
proof (state)
this:
deriv zeta s = deriv (eval_fds fds_zeta) s

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deriv zeta s = deriv (eval_fds fds_zeta) s

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have "deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s
[PROOF STEP]
using assms zeta_Re_gt_1_nonzero[of s]
[PROOF STATE]
proof (prove)
using this:
1 < Re s
1 < Re s \<Longrightarrow> zeta s \<noteq> 0

goal (1 subgoal):
 1. deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s
[PROOF STEP]
by (subst eval_fds_log_deriv) (auto simp: eval_fds_zeta eval_fds_deriv intro!: abscissa)
[PROOF STATE]
proof (state)
this:
deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have "eval_fds (fds_deriv fds_zeta / fds_zeta) s =
               -(\<Sum>\<^sub>ap | prime p. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))"
    (is "_ = -?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta / fds_zeta) s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1))
[PROOF STEP]
using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fds_nth fds_zeta 1 \<noteq> 0; abs_conv_abscissa fds_zeta < ereal (s \<bullet> 1)\<rbrakk> \<Longrightarrow> (\<lambda>p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / nat_power p s) - 1)) abs_summable_on {p. prime p}
\<lbrakk>fds_nth fds_zeta 1 \<noteq> 0; abs_conv_abscissa fds_zeta < ereal (s \<bullet> 1)\<rbrakk> \<Longrightarrow> eval_fds (fds_deriv fds_zeta / fds_zeta) s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / nat_power p s) - 1))
1 < Re s

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta / fds_zeta) s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval_fds (fds_deriv fds_zeta / fds_zeta) s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1))

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_fds (fds_deriv fds_zeta / fds_zeta) s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1))

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
have "?S = (\<Sum>\<^sub>ap | prime p. ln (real p) / (p powr s - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) = (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < Re s

goal (1 subgoal):
 1. (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) = (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
by (intro infsetsum_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) * (1 / (1 - fds_nth fds_zeta p / of_nat p powr s) - 1)) = (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
show ?th2
[PROOF STATE]
proof (prove)
using this:
deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))

goal (1 subgoal):
 1. deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sums_logderiv_zeta:
  assumes "Re s > 1"
  shows   "(\<lambda>p. if prime p then of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums
             -(deriv zeta s / zeta s)" (is "?f sums _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. if prime p then complex_of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums - (deriv zeta s / zeta s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>p. if prime p then complex_of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums - (deriv zeta s / zeta s)
[PROOF STEP]
note * = eval_fds_logderiv_zeta[OF assms]
[PROOF STATE]
proof (state)
this:
(\<lambda>p. complex_of_real (ln (real p)) / (of_nat p powr s - 1)) abs_summable_on {p. prime p}
deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))

goal (1 subgoal):
 1. (\<lambda>p. if prime p then complex_of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums - (deriv zeta s / zeta s)
[PROOF STEP]
from sums_infsetsum_nat[OF *(1)] and *(2)
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. if n \<in> {p. prime p} then complex_of_real (ln (real n)) / (of_nat n powr s - 1) else 0) sums (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. if n \<in> {p. prime p} then complex_of_real (ln (real n)) / (of_nat n powr s - 1) else 0) sums (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))
deriv zeta s / zeta s = - (\<Sum>\<^sub>ap | prime p. complex_of_real (ln (real p)) / (of_nat p powr s - 1))

goal (1 subgoal):
 1. (\<lambda>p. if prime p then complex_of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums - (deriv zeta s / zeta s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>p. if prime p then complex_of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums - (deriv zeta s / zeta s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_conv_abscissa_diff_le:
  "abs_conv_abscissa (f - g :: 'a :: dirichlet_series fds) \<le>
     max (abs_conv_abscissa f) (abs_conv_abscissa g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa (f - g) \<le> max (abs_conv_abscissa f) (abs_conv_abscissa g)
[PROOF STEP]
using abs_conv_abscissa_add_le[of f "-g"]
[PROOF STATE]
proof (prove)
using this:
abs_conv_abscissa (f + - g) \<le> max (abs_conv_abscissa f) (abs_conv_abscissa (- g))

goal (1 subgoal):
 1. abs_conv_abscissa (f - g) \<le> max (abs_conv_abscissa f) (abs_conv_abscissa g)
[PROOF STEP]
by auto


[STATEMENT]
lemma abs_conv_abscissa_diff_leI:
  "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \<le> d \<Longrightarrow> abs_conv_abscissa g \<le> d \<Longrightarrow>
     abs_conv_abscissa (f - g) \<le> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs_conv_abscissa f \<le> d; abs_conv_abscissa g \<le> d\<rbrakk> \<Longrightarrow> abs_conv_abscissa (f - g) \<le> d
[PROOF STEP]
using abs_conv_abscissa_diff_le[of f g]
[PROOF STATE]
proof (prove)
using this:
abs_conv_abscissa (f - g) \<le> max (abs_conv_abscissa f) (abs_conv_abscissa g)

goal (1 subgoal):
 1. \<lbrakk>abs_conv_abscissa f \<le> d; abs_conv_abscissa g \<le> d\<rbrakk> \<Longrightarrow> abs_conv_abscissa (f - g) \<le> d
[PROOF STEP]
by (auto simp: le_max_iff_disj)


[STATEMENT]
lemma range_add_nat: "range (\<lambda>n. n + c) = {(c::nat)..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>n. n + c) = {c..}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x n. n \<in> UNIV \<Longrightarrow> c \<le> n + c
 2. \<And>x. c \<le> x \<Longrightarrow> x \<in> range (\<lambda>n. n + c)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x n. n \<in> UNIV \<Longrightarrow> c \<le> n + c
 2. \<And>x. c \<le> x \<Longrightarrow> x \<in> range (\<lambda>n. n + c)
[PROOF STEP]
assume "x \<ge> c"
[PROOF STATE]
proof (state)
this:
c \<le> x

goal (2 subgoals):
 1. \<And>x n. n \<in> UNIV \<Longrightarrow> c \<le> n + c
 2. \<And>x. c \<le> x \<Longrightarrow> x \<in> range (\<lambda>n. n + c)
[PROOF STEP]
hence "x = x - c + c"
[PROOF STATE]
proof (prove)
using this:
c \<le> x

goal (1 subgoal):
 1. x = x - c + c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = x - c + c

goal (2 subgoals):
 1. \<And>x n. n \<in> UNIV \<Longrightarrow> c \<le> n + c
 2. \<And>x. c \<le> x \<Longrightarrow> x \<in> range (\<lambda>n. n + c)
[PROOF STEP]
thus "x \<in> range (\<lambda>n. n + c)"
[PROOF STATE]
proof (prove)
using this:
x = x - c + c

goal (1 subgoal):
 1. x \<in> range (\<lambda>n. n + c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> range (\<lambda>n. n + c)

goal (1 subgoal):
 1. \<And>x n. n \<in> UNIV \<Longrightarrow> c \<le> n + c
[PROOF STEP]
qed auto


[STATEMENT]
lemma abs_summable_hurwitz_zeta:
  assumes "Re s > 1" "a + real b > 0"
  shows   "(\<lambda>n. 1 / (of_nat n + a) powr s) abs_summable_on {b..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < Re s
0 < a + real b
[PROOF STEP]
have "summable (\<lambda>n. cmod (1 / (of_nat (n + b) + a) powr s))"
[PROOF STATE]
proof (prove)
using this:
1 < Re s
0 < a + real b

goal (1 subgoal):
 1. summable (\<lambda>n. cmod (1 / complex_of_real (real (n + b) + a) powr s))
[PROOF STEP]
using summable_hurwitz_zeta_real[of "Re s" "a + b"]
[PROOF STATE]
proof (prove)
using this:
1 < Re s
0 < a + real b
\<lbrakk>1 < Re s; 0 < a + real b\<rbrakk> \<Longrightarrow> summable (\<lambda>n. (real n + (a + real b)) powr - Re s)

goal (1 subgoal):
 1. summable (\<lambda>n. cmod (1 / complex_of_real (real (n + b) + a) powr s))
[PROOF STEP]
by (auto simp: norm_divide powr_minus field_simps norm_powr_real_powr)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. cmod (1 / complex_of_real (real (n + b) + a) powr s))

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
hence "(\<lambda>n. 1 / (of_nat (n + b) + a) powr s) abs_summable_on UNIV"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. cmod (1 / complex_of_real (real (n + b) + a) powr s))

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real (n + b) + a) powr s) abs_summable_on UNIV
[PROOF STEP]
by (auto simp: abs_summable_on_nat_iff' add_ac)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. 1 / complex_of_real (real (n + b) + a) powr s) abs_summable_on UNIV

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. 1 / complex_of_real (real (n + b) + a) powr s) abs_summable_on UNIV

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
have "?this \<longleftrightarrow> (\<lambda>n. 1 / (of_nat n + a) powr s) abs_summable_on range (\<lambda>n. n + b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>n. 1 / complex_of_real (real (n + b) + a) powr s) abs_summable_on UNIV) = ((\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on range (\<lambda>n. n + b))
[PROOF STEP]
by (rule abs_summable_on_reindex_iff) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>n. 1 / complex_of_real (real (n + b) + a) powr s) abs_summable_on UNIV) = ((\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on range (\<lambda>n. n + b))

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>n. 1 / complex_of_real (real (n + b) + a) powr s) abs_summable_on UNIV) = ((\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on range (\<lambda>n. n + b))

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
have "range (\<lambda>n. n + b) = {b..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>n. n + b) = {b..}
[PROOF STEP]
by (rule range_add_nat)
[PROOF STATE]
proof (state)
this:
range (\<lambda>n. n + b) = {b..}

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}

goal (1 subgoal):
 1. (\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>n. 1 / complex_of_real (real n + a) powr s) abs_summable_on {b..}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hurwitz_zeta_nat_conv_infsetsum:
  assumes "a > 0" and "Re s > 1"
  shows   "hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr -s)"
          "hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr -s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s) &&& hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
 2. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
have "hurwitz_zeta (real a) s = (\<Sum>n. of_nat (n + a) powr -s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>n. of_nat (n + a) powr - s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < a
1 < Re s

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>n. of_nat (n + a) powr - s)
[PROOF STEP]
by (subst hurwitz_zeta_conv_suminf) auto
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (real a) s = (\<Sum>n. of_nat (n + a) powr - s)

goal (2 subgoals):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
 2. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (real a) s = (\<Sum>n. of_nat (n + a) powr - s)

goal (2 subgoals):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
 2. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>an. of_nat (n + a) powr -s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. of_nat (n + a) powr - s) = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
[PROOF STEP]
using abs_summable_hurwitz_zeta[of s a 0] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < Re s; 0 < real a + real 0\<rbrakk> \<Longrightarrow> (\<lambda>n. 1 / complex_of_real (real n + real a) powr s) abs_summable_on {0..}
0 < a
1 < Re s

goal (1 subgoal):
 1. (\<Sum>n. of_nat (n + a) powr - s) = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
[PROOF STEP]
by (intro infsetsum_nat' [symmetric]) (auto simp: powr_minus field_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. of_nat (n + a) powr - s) = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)

goal (2 subgoals):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
 2. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
[PROOF STEP]
show "hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr -s)"
[PROOF STATE]
proof (prove)
using this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an. of_nat (n + a) powr - s)

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>an\<in>range (\<lambda>n. n + a). of_nat n powr -s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>an. of_nat (n + a) powr - s) = (\<Sum>\<^sub>an\<in>range (\<lambda>n. n + a). of_nat n powr - s)
[PROOF STEP]
by (rule infsetsum_reindex [symmetric]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>an. of_nat (n + a) powr - s) = (\<Sum>\<^sub>an\<in>range (\<lambda>n. n + a). of_nat n powr - s)

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>an. of_nat (n + a) powr - s) = (\<Sum>\<^sub>an\<in>range (\<lambda>n. n + a). of_nat n powr - s)

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
have "range (\<lambda>n. n + a) = {a..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>n. n + a) = {a..}
[PROOF STEP]
by (rule range_add_nat)
[PROOF STATE]
proof (state)
this:
range (\<lambda>n. n + a) = {a..}

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
show "hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr -s)"
[PROOF STATE]
proof (prove)
using this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)

goal (1 subgoal):
 1. hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
hurwitz_zeta (real a) s = (\<Sum>\<^sub>an\<in>{a..}. of_nat n powr - s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_pre_zeta [continuous_intros]:
  assumes "continuous_on A f" "a > 0"
  shows   "continuous_on A (\<lambda>x. pre_zeta a (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on A (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on A (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
continuous_on A f
0 < a
[PROOF STEP]
have "continuous_on UNIV (pre_zeta a)"
[PROOF STATE]
proof (prove)
using this:
continuous_on A f
0 < a

goal (1 subgoal):
 1. continuous_on UNIV (pre_zeta a)
[PROOF STEP]
by (intro holomorphic_on_imp_continuous_on[OF holomorphic_pre_zeta]) auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (pre_zeta a)

goal (1 subgoal):
 1. continuous_on A (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
from continuous_on_compose2[OF this assms(1)]
[PROOF STATE]
proof (chain)
picking this:
f ` A \<subseteq> UNIV \<Longrightarrow> continuous_on A (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` A \<subseteq> UNIV \<Longrightarrow> continuous_on A (\<lambda>x. pre_zeta a (f x))

goal (1 subgoal):
 1. continuous_on A (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
continuous_on A (\<lambda>x. pre_zeta a (f x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_pre_zeta [continuous_intros]:
  assumes "continuous (at x within A) f" "a > 0"
  shows   "continuous (at x within A) (\<lambda>x. pre_zeta a (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at x within A) (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous (at x within A) (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
have "continuous (at z) (pre_zeta a)" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (pre_zeta a) z
[PROOF STEP]
by (rule continuous_on_interior[of UNIV]) (insert assms, auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
isCont (pre_zeta a) ?z

goal (1 subgoal):
 1. continuous (at x within A) (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
from continuous_within_compose3[OF this assms(1)]
[PROOF STATE]
proof (chain)
picking this:
continuous (at x within A) (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
continuous (at x within A) (\<lambda>x. pre_zeta a (f x))

goal (1 subgoal):
 1. continuous (at x within A) (\<lambda>x. pre_zeta a (f x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
continuous (at x within A) (\<lambda>x. pre_zeta a (f x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pre_zeta_bound:
  assumes "0 < Re s" and a: "a > 0"
  shows   "norm (pre_zeta a s) \<le> (1 + norm s / Re s) / 2 * a powr -Re s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
let ?f = "\<lambda>x. - (s * (x + a) powr (-1-s))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
let ?g' = "\<lambda>x. norm s * (x + a) powr (-1-Re s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
let ?g = "\<lambda>x. -norm s / Re s * (x + a) powr (-Re s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
define R where "R = EM_remainder 1 ?f 0"
[PROOF STATE]
proof (state)
this:
R = EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) 0

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
have [simp]: "-Re s - 1 = -1 - Re s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Re s - 1 = - 1 - Re s
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
- Re s - 1 = - 1 - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
have "\<bar>frac x - 1 / 2\<bar> \<le> 1 / 2" for x :: real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>frac x - 1 / 2\<bar> \<le> 1 / 2
[PROOF STEP]
unfolding frac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x - real_of_int \<lfloor>x\<rfloor> - 1 / 2\<bar> \<le> 1 / 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<bar>frac ?x - 1 / 2\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
hence "\<bar>pbernpoly (Suc 0) x\<bar> \<le> 1 / 2" for x
[PROOF STATE]
proof (prove)
using this:
\<bar>frac ?x - 1 / 2\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. \<bar>pbernpoly (Suc 0) x\<bar> \<le> 1 / 2
[PROOF STEP]
by (simp add: pbernpoly_def bernpoly_def)
[PROOF STATE]
proof (state)
this:
\<bar>pbernpoly (Suc 0) ?x\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>pbernpoly (Suc 0) ?x\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
have "((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top
[PROOF STEP]
using \<open>Re s > 0\<close> \<open>a > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Re s
0 < a

goal (1 subgoal):
 1. ((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>pbernpoly (Suc 0) ?x\<bar> \<le> 1 / 2
((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top
[PROOF STEP]
have *: "\<forall>x. x \<ge> real 0 \<longrightarrow> norm (EM_remainder 1 ?f (int x)) \<le>
                           (1 / 2) / fact 1 * (-?g (real x))"
[PROOF STATE]
proof (prove)
using this:
\<bar>pbernpoly (Suc 0) ?x\<bar> \<le> 1 / 2
((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. \<forall>x. real 0 \<le> real x \<longrightarrow> cmod (EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) (int x)) \<le> 1 / 2 / fact 1 * - (- cmod s / Re s * (real x + a) powr - Re s)
[PROOF STEP]
using \<open>a > 0\<close> \<open>Re s > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>pbernpoly (Suc 0) ?x\<bar> \<le> 1 / 2
((\<lambda>b. cmod s * (b + a) powr - Re s / Re s) \<longlongrightarrow> 0) at_top
0 < a
0 < Re s

goal (1 subgoal):
 1. \<forall>x. real 0 \<le> real x \<longrightarrow> cmod (EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) (int x)) \<le> 1 / 2 / fact 1 * - (- cmod s / Re s * (real x + a) powr - Re s)
[PROOF STEP]
by (intro norm_EM_remainder_le_strong_nat'[where g' = ?g' and Y = "{}"])
       (auto intro!: continuous_intros derivative_eq_intros
             simp: field_simps norm_mult norm_powr_real_powr add_eq_0_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x. real 0 \<le> real x \<longrightarrow> cmod (EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) (int x)) \<le> 1 / 2 / fact 1 * - (- cmod s / Re s * (real x + a) powr - Re s)

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
have R: "norm R \<le> norm s / (2 * Re s) * a powr -Re s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod R \<le> cmod s / (2 * Re s) * a powr - Re s
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) 0) \<le> cmod s / (2 * Re s) * a powr - Re s
[PROOF STEP]
using spec[OF *, of 0]
[PROOF STATE]
proof (prove)
using this:
real 0 \<le> real 0 \<longrightarrow> cmod (EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) (int 0)) \<le> 1 / 2 / fact 1 * - (- cmod s / Re s * (real 0 + a) powr - Re s)

goal (1 subgoal):
 1. cmod (EM_remainder 1 (\<lambda>x. - (s * complex_of_real (x + a) powr (- 1 - s))) 0) \<le> cmod s / (2 * Re s) * a powr - Re s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod R \<le> cmod s / (2 * Re s) * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < Re s
0 < a
[PROOF STEP]
have "pre_zeta a s = a powr -s / 2 + R"
[PROOF STATE]
proof (prove)
using this:
0 < Re s
0 < a

goal (1 subgoal):
 1. pre_zeta a s = complex_of_real a powr - s / 2 + R
[PROOF STEP]
by (simp add: pre_zeta_def pre_zeta_aux_def R_def)
[PROOF STATE]
proof (state)
this:
pre_zeta a s = complex_of_real a powr - s / 2 + R

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pre_zeta a s = complex_of_real a powr - s / 2 + R

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
have "norm \<dots> \<le> a powr -Re s / 2 + norm s / (2 * Re s) * a powr -Re s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (complex_of_real a powr - s / 2 + R) \<le> a powr - Re s / 2 + cmod s / (2 * Re s) * a powr - Re s
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. cmod (complex_of_real a powr - s / 2 + R) \<le> a powr - Re s / 2 + cmod s / (2 * Re s) * a powr - Re s
[PROOF STEP]
by (intro order.trans[OF norm_triangle_ineq] add_mono R) (auto simp: norm_powr_real_powr)
[PROOF STATE]
proof (state)
this:
cmod (complex_of_real a powr - s / 2 + R) \<le> a powr - Re s / 2 + cmod s / (2 * Re s) * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (complex_of_real a powr - s / 2 + R) \<le> a powr - Re s / 2 + cmod s / (2 * Re s) * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
have "\<dots> = (1 + norm s / Re s) / 2 * a powr -Re s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a powr - Re s / 2 + cmod s / (2 * Re s) * a powr - Re s = (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
a powr - Re s / 2 + cmod s / (2 * Re s) * a powr - Re s = (1 + cmod s / Re s) / 2 * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pre_zeta_bound':
  assumes "0 < Re s" and a: "a > 0"
  shows   "norm (pre_zeta a s) \<le> norm s / (Re s * a powr Re s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < Re s
0 < a
[PROOF STEP]
have "norm (pre_zeta a s) \<le> (1 + norm s / Re s) / 2 * a powr -Re s"
[PROOF STATE]
proof (prove)
using this:
0 < Re s
0 < a

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s
[PROOF STEP]
by (intro pre_zeta_bound) auto
[PROOF STATE]
proof (state)
this:
cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (pre_zeta a s) \<le> (1 + cmod s / Re s) / 2 * a powr - Re s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
have "\<dots> = (Re s + norm s) / 2 / (Re s * a powr Re s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + cmod s / Re s) / 2 * a powr - Re s = (Re s + cmod s) / 2 / (Re s * a powr Re s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < Re s
0 < a

goal (1 subgoal):
 1. (1 + cmod s / Re s) / 2 * a powr - Re s = (Re s + cmod s) / 2 / (Re s * a powr Re s)
[PROOF STEP]
by (auto simp: field_simps powr_minus)
[PROOF STATE]
proof (state)
this:
(1 + cmod s / Re s) / 2 * a powr - Re s = (Re s + cmod s) / 2 / (Re s * a powr Re s)

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 + cmod s / Re s) / 2 * a powr - Re s = (Re s + cmod s) / 2 / (Re s * a powr Re s)

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
have "Re s + norm s \<le> norm s + norm s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re s + cmod s \<le> cmod s + cmod s
[PROOF STEP]
by (intro add_right_mono complex_Re_le_cmod)
[PROOF STATE]
proof (state)
this:
Re s + cmod s \<le> cmod s + cmod s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re s + cmod s \<le> cmod s + cmod s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
have "(norm s + norm s) / 2 = norm s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod s + cmod s) / 2 = cmod s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(cmod s + cmod s) / 2 = cmod s

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x / 2 / (Re s * a powr Re s) \<le> y / 2 / (Re s * a powr Re s)) \<Longrightarrow> cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
show "norm (pre_zeta a s) \<le> norm s / (Re s * a powr Re s)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x / 2 / (Re s * a powr Re s) \<le> y / 2 / (Re s * a powr Re s)) \<Longrightarrow> cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x / 2 / (Re s * a powr Re s) \<le> y / 2 / (Re s * a powr Re s)) \<Longrightarrow> cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
0 < Re s
0 < a

goal (1 subgoal):
 1. cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)
[PROOF STEP]
by (simp add: divide_right_mono)
[PROOF STATE]
proof (state)
this:
cmod (pre_zeta a s) \<le> cmod s / (Re s * a powr Re s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma summable_comparison_test_bigo:
  fixes f :: "nat \<Rightarrow> real"
  assumes "summable (\<lambda>n. norm (g n))" "f \<in> O(g)"
  shows   "summable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
from \<open>f \<in> O(g)\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> O(g)
[PROOF STEP]
obtain C where C: "eventually (\<lambda>x. norm (f x) \<le> C * norm (g x)) at_top"
[PROOF STATE]
proof (prove)
using this:
f \<in> O(g)

goal (1 subgoal):
 1. (\<And>C. \<forall>\<^sub>F x in sequentially. norm (f x) \<le> C * norm (g x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: landau_o.bigE)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. norm (f x) \<le> C * norm (g x)

goal (1 subgoal):
 1. summable f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. norm (f x) \<le> C * norm (g x)

goal (1 subgoal):
 1. summable f
[PROOF STEP]
by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
[PROOF STATE]
proof (state)
this:
summable f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deriv_zeta_eq:
  assumes s: "s \<noteq> 1"
  shows   "deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> 1
[PROOF STEP]
have ev: "eventually (\<lambda>z. z \<noteq> 1) (nhds s)"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F z in nhds s. z \<noteq> 1
[PROOF STEP]
by (intro t1_space_nhds)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F z in nhds s. z \<noteq> 1

goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
have [derivative_intros]: "(pre_zeta 1 has_field_derivative deriv (pre_zeta 1) s) (at s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pre_zeta 1 has_field_derivative deriv (pre_zeta 1) s) (at s)
[PROOF STEP]
by (intro holomorphic_derivI[of _ UNIV] holomorphic_intros) auto
[PROOF STATE]
proof (state)
this:
(pre_zeta 1 has_field_derivative deriv (pre_zeta 1) s) (at s)

goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
have "((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative
          (deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2)) (at s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 1

goal (1 subgoal):
 1. ((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)
[PROOF STEP]
by (auto intro!: derivative_eq_intros simp: power2_eq_square)
[PROOF STATE]
proof (state)
this:
((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)

goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)

goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
have "?this \<longleftrightarrow> (zeta has_field_derivative (deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2)) (at s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s) = (zeta has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)
[PROOF STEP]
by (intro has_field_derivative_cong_ev eventually_mono[OF ev])
       (auto simp: zeta_def hurwitz_zeta_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s) = (zeta has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)

goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(zeta has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(zeta has_field_derivative deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2) (at s)

goal (1 subgoal):
 1. deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2
[PROOF STEP]
by (rule DERIV_imp_deriv)
[PROOF STATE]
proof (state)
this:
deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zeta_remove_zero:
  assumes "Re s \<ge> 1"
  shows   "(s - 1) * pre_zeta 1 s + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
proof (cases "s = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
 2. s \<noteq> 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s \<noteq> 1

goal (2 subgoals):
 1. s = 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
 2. s \<noteq> 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
hence "(s - 1) * pre_zeta 1 s + 1 = (s - 1) * zeta s"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 1

goal (1 subgoal):
 1. (s - 1) * pre_zeta 1 s + 1 = (s - 1) * zeta s
[PROOF STEP]
by (simp add: zeta_def hurwitz_zeta_def divide_simps)
[PROOF STATE]
proof (state)
this:
(s - 1) * pre_zeta 1 s + 1 = (s - 1) * zeta s

goal (2 subgoals):
 1. s = 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
 2. s \<noteq> 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(s - 1) * pre_zeta 1 s + 1 = (s - 1) * zeta s

goal (2 subgoals):
 1. s = 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
 2. s \<noteq> 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
from False assms
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> 1
1 \<le> Re s
[PROOF STEP]
have "\<dots> \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 1
1 \<le> Re s

goal (1 subgoal):
 1. (s - 1) * zeta s \<noteq> 0
[PROOF STEP]
using zeta_Re_ge_1_nonzero[of s]
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 1
1 \<le> Re s
\<lbrakk>1 \<le> Re s; s \<noteq> 1\<rbrakk> \<Longrightarrow> zeta s \<noteq> 0

goal (1 subgoal):
 1. (s - 1) * zeta s \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s - 1) * zeta s \<noteq> 0

goal (2 subgoals):
 1. s = 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
 2. s \<noteq> 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(s - 1) * pre_zeta 1 s + 1 \<noteq> 0

goal (1 subgoal):
 1. (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(s - 1) * pre_zeta 1 s + 1 \<noteq> 0

goal (1 subgoal):
 1. s = 1 \<Longrightarrow> (s - 1) * pre_zeta 1 s + 1 \<noteq> 0
[PROOF STEP]
qed auto


[STATEMENT]
lemma eval_fds_deriv_zeta:
  assumes "Re s > 1"
  shows   "eval_fds (fds_deriv fds_zeta) s = deriv zeta s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
have ev: "eventually (\<lambda>z. z \<in> {z. Re z > 1}) (nhds s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F z in nhds s. z \<in> {z. 1 < Re z}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < Re s

goal (1 subgoal):
 1. \<forall>\<^sub>F z in nhds s. z \<in> {z. 1 < Re z}
[PROOF STEP]
by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F z in nhds s. z \<in> {z. 1 < Re z}

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < Re s
[PROOF STEP]
have "eval_fds (fds_deriv fds_zeta) s = deriv (eval_fds fds_zeta) s"
[PROOF STATE]
proof (prove)
using this:
1 < Re s

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv (eval_fds fds_zeta) s
[PROOF STEP]
by (subst eval_fds_deriv) auto
[PROOF STATE]
proof (state)
this:
eval_fds (fds_deriv fds_zeta) s = deriv (eval_fds fds_zeta) s

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_fds (fds_deriv fds_zeta) s = deriv (eval_fds fds_zeta) s

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
have "\<dots> = deriv zeta s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (eval_fds fds_zeta) s = deriv zeta s
[PROOF STEP]
by (intro deriv_cong_ev eventually_mono[OF ev]) (auto simp: eval_fds_zeta)
[PROOF STATE]
proof (state)
this:
deriv (eval_fds fds_zeta) s = deriv zeta s

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval_fds (fds_deriv fds_zeta) s = deriv zeta s

goal (1 subgoal):
 1. eval_fds (fds_deriv fds_zeta) s = deriv zeta s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eval_fds (fds_deriv fds_zeta) s = deriv zeta s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_sorted_list_of_set [simp]:
  "finite A \<Longrightarrow> length (sorted_list_of_set A) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> length (sorted_list_of_set A) = card A
[PROOF STEP]
by (metis length_remdups_card_conv length_sort set_sorted_list_of_set
            sorted_list_of_set_sort_remdups)


[STATEMENT]
lemma le_nat_iff': "x \<le> nat y \<longleftrightarrow> x = 0 \<and> y \<le> 0 \<or> int x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> nat y) = (x = 0 \<and> y \<le> 0 \<or> int x \<le> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_upto_plus1:
  assumes "x \<ge> 0"
  shows   "sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
have "sum_upto f (x + 1) = sum f {0<..Suc (nat \<lfloor>x\<rfloor>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto f (x + 1) = sum f {0<..Suc (nat \<lfloor>x\<rfloor>)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> x

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum f {0<..Suc (nat \<lfloor>x\<rfloor>)}
[PROOF STEP]
by (simp add: sum_upto_altdef nat_add_distrib)
[PROOF STATE]
proof (state)
this:
sum_upto f (x + 1) = sum f {0<..Suc (nat \<lfloor>x\<rfloor>)}

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_upto f (x + 1) = sum f {0<..Suc (nat \<lfloor>x\<rfloor>)}

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
have "{0<..Suc (nat \<lfloor>x\<rfloor>)} = insert (Suc (nat \<lfloor>x\<rfloor>)) {0<..nat \<lfloor>x\<rfloor>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0<..Suc (nat \<lfloor>x\<rfloor>)} = insert (Suc (nat \<lfloor>x\<rfloor>)) {0<..nat \<lfloor>x\<rfloor>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0<..Suc (nat \<lfloor>x\<rfloor>)} = insert (Suc (nat \<lfloor>x\<rfloor>)) {0<..nat \<lfloor>x\<rfloor>}

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{0<..Suc (nat \<lfloor>x\<rfloor>)} = insert (Suc (nat \<lfloor>x\<rfloor>)) {0<..nat \<lfloor>x\<rfloor>}

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
have "sum f \<dots> = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (insert (Suc (nat \<lfloor>x\<rfloor>)) {0<..nat \<lfloor>x\<rfloor>}) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
by (subst sum.insert) (auto simp: sum_upto_altdef add_ac)
[PROOF STATE]
proof (state)
this:
sum f (insert (Suc (nat \<lfloor>x\<rfloor>)) {0<..nat \<lfloor>x\<rfloor>}) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))

goal (1 subgoal):
 1. sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \<lfloor>x\<rfloor>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_upto_minus1:
  assumes "x \<ge> 1"
  shows   "sum_upto f (x - 1) = (sum_upto f x - f (nat \<lfloor>x\<rfloor>) :: 'a :: ab_group_add)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto f (x - 1) = sum_upto f x - f (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
using sum_upto_plus1[of "x - 1" f] assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> x - 1 \<Longrightarrow> sum_upto f (x - 1 + 1) = sum_upto f (x - 1) + f (Suc (nat \<lfloor>x - 1\<rfloor>))
1 \<le> x

goal (1 subgoal):
 1. sum_upto f (x - 1) = sum_upto f x - f (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
by (simp add: algebra_simps nat_diff_distrib)


[STATEMENT]
lemma integral_smallo:
  fixes f g g' :: "real \<Rightarrow> real"
  assumes "f \<in> o(g')" and "filterlim g at_top at_top"
  assumes "\<And>a' x. a \<le> a' \<Longrightarrow> a' \<le> x \<Longrightarrow> f integrable_on {a'..x}"
  assumes deriv: "\<And>x. x \<ge> a \<Longrightarrow> (g has_field_derivative g' x) (at x)"
  assumes cont: "continuous_on {a..} g'"
  assumes nonneg: "\<And>x. x \<ge> a \<Longrightarrow> g' x \<ge> 0"
  shows   "(\<lambda>x. integral {a..x} f) \<in> o(g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> o(g)
[PROOF STEP]
proof (rule landau_o.smallI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
fix c :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
assume c: "c > 0"
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
note [continuous_intros] = continuous_on_subset[OF cont]
[PROOF STATE]
proof (state)
this:
?t \<subseteq> {a..} \<Longrightarrow> continuous_on ?t g'

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
define c' where "c' = c / 2"
[PROOF STATE]
proof (state)
this:
c' = c / 2

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
0 < c
[PROOF STEP]
have c': "c' > 0"
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. 0 < c'
[PROOF STEP]
by (simp add: c'_def)
[PROOF STATE]
proof (state)
this:
0 < c'

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
from landau_o.smallD[OF assms(1) this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at_top. norm (f x) \<le> c' * norm (g' x)
[PROOF STEP]
obtain b where b: "\<And>x. x \<ge> b \<Longrightarrow> norm (f x) \<le> c' * norm (g' x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. norm (f x) \<le> c' * norm (g' x)

goal (1 subgoal):
 1. (\<And>b. (\<And>x. b \<le> x \<Longrightarrow> norm (f x) \<le> c' * norm (g' x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> c' * norm (g' n)

goal (1 subgoal):
 1. (\<And>b. (\<And>x. b \<le> x \<Longrightarrow> norm (f x) \<le> c' * norm (g' x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<le> ?x \<Longrightarrow> norm (f ?x) \<le> c' * norm (g' ?x)

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
define b' where "b' = max a b"
[PROOF STATE]
proof (state)
this:
b' = max a b

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
define D where "D = norm (integral {a..b'} f)"
[PROOF STATE]
proof (state)
this:
D = norm (integral {a..b'} f)

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "filterlim (\<lambda>x. c' * g x) at_top at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x at_top. c' * g x :> at_top
[PROOF STEP]
using c'
[PROOF STATE]
proof (prove)
using this:
0 < c'

goal (1 subgoal):
 1. LIM x at_top. c' * g x :> at_top
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] assms)
[PROOF STATE]
proof (state)
this:
LIM x at_top. c' * g x :> at_top

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
hence "eventually (\<lambda>x. c' * g x \<ge> D - c' * g b') at_top"
[PROOF STATE]
proof (prove)
using this:
LIM x at_top. c' * g x :> at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. D - c' * g b' \<le> c' * g x
[PROOF STEP]
by (auto simp: filterlim_at_top)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. D - c' * g b' \<le> c' * g x

goal (1 subgoal):
 1. \<And>c. 0 < c \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
thus "eventually (\<lambda>x. norm (integral {a..x} f) \<le> c * norm (g x)) at_top"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. D - c' * g b' \<le> c' * g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
using eventually_ge_at_top[of b']
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. D - c' * g b' \<le> c' * g x
eventually ((\<le>) b') at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
D - c' * g b' \<le> c' * g x
b' \<le> x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have b': "a \<le> b'" "b \<le> b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b' &&& b \<le> b'
[PROOF STEP]
by (auto simp: b'_def)
[PROOF STATE]
proof (state)
this:
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
from elim b'
[PROOF STATE]
proof (chain)
picking this:
D - c' * g b' \<le> c' * g x
b' \<le> x
a \<le> b'
b \<le> b'
[PROOF STEP]
have integrable: "(\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}"
[PROOF STATE]
proof (prove)
using this:
D - c' * g b' \<le> c' * g x
b' \<le> x
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. (\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}
[PROOF STEP]
by (intro integrable_continuous_real continuous_intros) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "integral {a..x} f = integral {a..b'} f + integral {b'..x} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {a..x} f = integral {a..b'} f + integral {b'..x} f
[PROOF STEP]
using elim b'
[PROOF STATE]
proof (prove)
using this:
D - c' * g b' \<le> c' * g x
b' \<le> x
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. integral {a..x} f = integral {a..b'} f + integral {b'..x} f
[PROOF STEP]
by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] assms) auto
[PROOF STATE]
proof (state)
this:
integral {a..x} f = integral {a..b'} f + integral {b'..x} f

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {a..x} f = integral {a..b'} f + integral {b'..x} f

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "norm \<dots> \<le> D + norm (integral {b'..x} f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {a..b'} f + integral {b'..x} f) \<le> D + norm (integral {b'..x} f)
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {a..b'} f + integral {b'..x} f) \<le> norm (integral {a..b'} f) + norm (integral {b'..x} f)
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (integral {a..b'} f + integral {b'..x} f) \<le> D + norm (integral {b'..x} f)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral {a..b'} f + integral {b'..x} f) \<le> D + norm (integral {b'..x} f)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c' * norm (g' x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c' * norm (g' x))
[PROOF STEP]
using b' elim assms c' integrable
[PROOF STATE]
proof (prove)
using this:
a \<le> b'
b \<le> b'
D - c' * g b' \<le> c' * g x
b' \<le> x
f \<in> o(g')
filterlim g at_top at_top
\<lbrakk>a \<le> ?a'; ?a' \<le> ?x\<rbrakk> \<Longrightarrow> f integrable_on {?a'..?x}
a \<le> ?x \<Longrightarrow> (g has_real_derivative g' ?x) (at ?x)
continuous_on {a..} g'
a \<le> ?x \<Longrightarrow> 0 \<le> g' ?x
0 < c'
(\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}

goal (1 subgoal):
 1. norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c' * norm (g' x))
[PROOF STEP]
by (intro integral_norm_bound_integral b assms) auto
[PROOF STATE]
proof (state)
this:
norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c' * norm (g' x))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c' * norm (g' x))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "\<dots> = c' * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {b'..x} (\<lambda>x. c' * norm (g' x)) = c' * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. c' * norm (g' x)) = c' * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. c' * norm (g' x)) = c' * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'
[PROOF STEP]
using assms b'
[PROOF STATE]
proof (prove)
using this:
f \<in> o(g')
filterlim g at_top at_top
\<lbrakk>a \<le> ?a'; ?a' \<le> ?x\<rbrakk> \<Longrightarrow> f integrable_on {?a'..?x}
a \<le> ?x \<Longrightarrow> (g has_real_derivative g' ?x) (at ?x)
continuous_on {a..} g'
a \<le> ?x \<Longrightarrow> 0 \<le> g' ?x
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'
[PROOF STEP]
by (intro integral_cong) auto
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "(g' has_integral (g x - g b')) {b'..x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g' has_integral g x - g b') {b'..x}
[PROOF STEP]
using b' elim
[PROOF STATE]
proof (prove)
using this:
a \<le> b'
b \<le> b'
D - c' * g b' \<le> c' * g x
b' \<le> x

goal (1 subgoal):
 1. (g' has_integral g x - g b') {b'..x}
[PROOF STEP]
by (intro fundamental_theorem_of_calculus)
         (auto simp flip: has_real_derivative_iff_has_vector_derivative
               intro!: has_field_derivative_at_within[OF deriv])
[PROOF STATE]
proof (state)
this:
(g' has_integral g x - g b') {b'..x}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
hence "integral {b'..x} g' = g x - g b'"
[PROOF STATE]
proof (prove)
using this:
(g' has_integral g x - g b') {b'..x}

goal (1 subgoal):
 1. integral {b'..x} g' = g x - g b'
[PROOF STEP]
by (simp add: has_integral_iff)
[PROOF STATE]
proof (state)
this:
integral {b'..x} g' = g x - g b'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {b'..x} g' = g x - g b'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "D + c' * (g x - g b') \<le> c * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D + c' * (g x - g b') \<le> c * g x
[PROOF STEP]
using elim
[PROOF STATE]
proof (prove)
using this:
D - c' * g b' \<le> c' * g x
b' \<le> x

goal (1 subgoal):
 1. D + c' * (g x - g b') \<le> c * g x
[PROOF STEP]
by (simp add: field_simps c'_def)
[PROOF STATE]
proof (state)
this:
D + c' * (g x - g b') \<le> c * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D + c' * (g x - g b') \<le> c * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
have "\<dots> \<le> c * norm (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * g x \<le> c * norm (g x)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. c * g x \<le> c * norm (g x)
[PROOF STEP]
by (intro mult_left_mono) auto
[PROOF STATE]
proof (state)
this:
c * g x \<le> c * norm (g x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c' * g b' \<le> c' * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> D + x \<le> D + y) \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> D + x \<le> D + y) \<Longrightarrow> norm (integral {a..x} f) \<le> c * norm (g x)

goal (1 subgoal):
 1. norm (integral {a..x} f) \<le> c * norm (g x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (integral {a..x} f) \<le> c * norm (g x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> c * norm (g x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma integral_bigo:
  fixes f g g' :: "real \<Rightarrow> real"
  assumes "f \<in> O(g')" and "filterlim g at_top at_top"
  assumes "\<And>a' x. a \<le> a' \<Longrightarrow> a' \<le> x \<Longrightarrow> f integrable_on {a'..x}"
  assumes deriv: "\<And>x. x \<ge> a \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..})"
  assumes cont: "continuous_on {a..} g'"
  assumes nonneg: "\<And>x. x \<ge> a \<Longrightarrow> g' x \<ge> 0"
  shows   "(\<lambda>x. integral {a..x} f) \<in> O(g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
note [continuous_intros] = continuous_on_subset[OF cont]
[PROOF STATE]
proof (state)
this:
?t \<subseteq> {a..} \<Longrightarrow> continuous_on ?t g'

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
from landau_o.bigE[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>c. \<lbrakk>0 < c; \<forall>\<^sub>F x in at_top. norm (f x) \<le> c * norm (g' x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain c b where c: "c > 0" and b: "\<And>x. x \<ge> b \<Longrightarrow> norm (f x) \<le> c * norm (g' x)"
[PROOF STATE]
proof (prove)
using this:
(\<And>c. \<lbrakk>0 < c; \<forall>\<^sub>F x in at_top. norm (f x) \<le> c * norm (g' x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c b. \<lbrakk>0 < c; \<And>x. b \<le> x \<Longrightarrow> norm (f x) \<le> c * norm (g' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
(\<And>c. \<lbrakk>0 < c; \<exists>N. \<forall>n\<ge>N. norm (f n) \<le> c * norm (g' n)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c b. \<lbrakk>0 < c; \<And>x. b \<le> x \<Longrightarrow> norm (f x) \<le> c * norm (g' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0 < c
b \<le> ?x \<Longrightarrow> norm (f ?x) \<le> c * norm (g' ?x)

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
define c' where "c' = c / 2"
[PROOF STATE]
proof (state)
this:
c' = c / 2

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
define b' where "b' = max a b"
[PROOF STATE]
proof (state)
this:
b' = max a b

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
define D where "D = norm (integral {a..b'} f)"
[PROOF STATE]
proof (state)
this:
D = norm (integral {a..b'} f)

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
have "filterlim (\<lambda>x. c * g x) at_top at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x at_top. c * g x :> at_top
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. LIM x at_top. c * g x :> at_top
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] assms)
[PROOF STATE]
proof (state)
this:
LIM x at_top. c * g x :> at_top

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
hence "eventually (\<lambda>x. c * g x \<ge> D - c * g b') at_top"
[PROOF STATE]
proof (prove)
using this:
LIM x at_top. c * g x :> at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. D - c * g b' \<le> c * g x
[PROOF STEP]
by (auto simp: filterlim_at_top)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. D - c * g b' \<le> c * g x

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
hence "eventually (\<lambda>x. norm (integral {a..x} f) \<le> 2 * c * norm (g x)) at_top"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. D - c * g b' \<le> c * g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
using eventually_ge_at_top[of b']
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. D - c * g b' \<le> c * g x
eventually ((\<le>) b') at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
D - c * g b' \<le> c * g x
b' \<le> x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have b': "a \<le> b'" "b \<le> b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b' &&& b \<le> b'
[PROOF STEP]
by (auto simp: b'_def)
[PROOF STATE]
proof (state)
this:
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
from elim b'
[PROOF STATE]
proof (chain)
picking this:
D - c * g b' \<le> c * g x
b' \<le> x
a \<le> b'
b \<le> b'
[PROOF STEP]
have integrable: "(\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}"
[PROOF STATE]
proof (prove)
using this:
D - c * g b' \<le> c * g x
b' \<le> x
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. (\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}
[PROOF STEP]
by (intro integrable_continuous_real continuous_intros) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "integral {a..x} f = integral {a..b'} f + integral {b'..x} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {a..x} f = integral {a..b'} f + integral {b'..x} f
[PROOF STEP]
using elim b'
[PROOF STATE]
proof (prove)
using this:
D - c * g b' \<le> c * g x
b' \<le> x
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. integral {a..x} f = integral {a..b'} f + integral {b'..x} f
[PROOF STEP]
by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] assms) auto
[PROOF STATE]
proof (state)
this:
integral {a..x} f = integral {a..b'} f + integral {b'..x} f

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {a..x} f = integral {a..b'} f + integral {b'..x} f

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "norm \<dots> \<le> D + norm (integral {b'..x} f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {a..b'} f + integral {b'..x} f) \<le> D + norm (integral {b'..x} f)
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {a..b'} f + integral {b'..x} f) \<le> norm (integral {a..b'} f) + norm (integral {b'..x} f)
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (integral {a..b'} f + integral {b'..x} f) \<le> D + norm (integral {b'..x} f)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral {a..b'} f + integral {b'..x} f) \<le> D + norm (integral {b'..x} f)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c * norm (g' x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c * norm (g' x))
[PROOF STEP]
using b' elim assms c integrable
[PROOF STATE]
proof (prove)
using this:
a \<le> b'
b \<le> b'
D - c * g b' \<le> c * g x
b' \<le> x
f \<in> O(g')
filterlim g at_top at_top
\<lbrakk>a \<le> ?a'; ?a' \<le> ?x\<rbrakk> \<Longrightarrow> f integrable_on {?a'..?x}
a \<le> ?x \<Longrightarrow> (g has_real_derivative g' ?x) (at ?x within {a..})
continuous_on {a..} g'
a \<le> ?x \<Longrightarrow> 0 \<le> g' ?x
0 < c
(\<lambda>x. \<bar>g' x\<bar>) integrable_on {b'..x}

goal (1 subgoal):
 1. norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c * norm (g' x))
[PROOF STEP]
by (intro integral_norm_bound_integral b assms) auto
[PROOF STATE]
proof (state)
this:
norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c * norm (g' x))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral {b'..x} f) \<le> integral {b'..x} (\<lambda>x. c * norm (g' x))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "\<dots> = c * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {b'..x} (\<lambda>x. c * norm (g' x)) = c * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. c * norm (g' x)) = c * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. c * norm (g' x)) = c * integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'
[PROOF STEP]
using assms b'
[PROOF STATE]
proof (prove)
using this:
f \<in> O(g')
filterlim g at_top at_top
\<lbrakk>a \<le> ?a'; ?a' \<le> ?x\<rbrakk> \<Longrightarrow> f integrable_on {?a'..?x}
a \<le> ?x \<Longrightarrow> (g has_real_derivative g' ?x) (at ?x within {a..})
continuous_on {a..} g'
a \<le> ?x \<Longrightarrow> 0 \<le> g' ?x
a \<le> b'
b \<le> b'

goal (1 subgoal):
 1. integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'
[PROOF STEP]
by (intro integral_cong) auto
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {b'..x} (\<lambda>x. \<bar>g' x\<bar>) = integral {b'..x} g'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "(g' has_integral (g x - g b')) {b'..x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g' has_integral g x - g b') {b'..x}
[PROOF STEP]
using b' elim
[PROOF STATE]
proof (prove)
using this:
a \<le> b'
b \<le> b'
D - c * g b' \<le> c * g x
b' \<le> x

goal (1 subgoal):
 1. (g' has_integral g x - g b') {b'..x}
[PROOF STEP]
by (intro fundamental_theorem_of_calculus)
         (auto simp flip: has_real_derivative_iff_has_vector_derivative
               intro!: DERIV_subset[OF deriv])
[PROOF STATE]
proof (state)
this:
(g' has_integral g x - g b') {b'..x}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
hence "integral {b'..x} g' = g x - g b'"
[PROOF STATE]
proof (prove)
using this:
(g' has_integral g x - g b') {b'..x}

goal (1 subgoal):
 1. integral {b'..x} g' = g x - g b'
[PROOF STEP]
by (simp add: has_integral_iff)
[PROOF STATE]
proof (state)
this:
integral {b'..x} g' = g x - g b'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {b'..x} g' = g x - g b'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "D + c * (g x - g b') \<le> 2 * c * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D + c * (g x - g b') \<le> 2 * c * g x
[PROOF STEP]
using elim
[PROOF STATE]
proof (prove)
using this:
D - c * g b' \<le> c * g x
b' \<le> x

goal (1 subgoal):
 1. D + c * (g x - g b') \<le> 2 * c * g x
[PROOF STEP]
by (simp add: field_simps c'_def)
[PROOF STATE]
proof (state)
this:
D + c * (g x - g b') \<le> 2 * c * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D + c * (g x - g b') \<le> 2 * c * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
have "\<dots> \<le> 2 * c * norm (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * c * g x \<le> 2 * c * norm (g x)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. 2 * c * g x \<le> 2 * c * norm (g x)
[PROOF STEP]
by (intro mult_left_mono) auto
[PROOF STATE]
proof (state)
this:
2 * c * g x \<le> 2 * c * norm (g x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>D - c * g b' \<le> c * g x; b' \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> D + x \<le> D + y) \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> D + x \<le> D + y) \<Longrightarrow> norm (integral {a..x} f) \<le> 2 * c * norm (g x)

goal (1 subgoal):
 1. norm (integral {a..x} f) \<le> 2 * c * norm (g x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (integral {a..x} f) \<le> 2 * c * norm (g x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> 2 * c * norm (g x)

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. norm (integral {a..x} f) \<le> 2 * c * norm (g x)

goal (1 subgoal):
 1. (\<lambda>x. integral {a..x} f) \<in> O(g)
[PROOF STEP]
by (rule bigoI)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. integral {a..x} f) \<in> O(g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primepows_le_subset:
  assumes x: "x > 0" and l: "l > 0"
  shows   "{(p, i). prime p \<and> l \<le> i \<and> real (p ^ i) \<le> x} \<subseteq> {..nat \<lfloor>root l x\<rfloor>} \<times> {..nat \<lfloor>log 2 x\<rfloor>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(p, i). prime p \<and> l \<le> i \<and> real (p ^ i) \<le> x} \<subseteq> {..nat \<lfloor>root l x\<rfloor>} \<times> {..nat \<lfloor>log 2 x\<rfloor>}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
fix p i :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
assume pi: "prime p" "i \<ge> l" "real (p ^ i) \<le> x"
[PROOF STATE]
proof (state)
this:
prime p
l \<le> i
real (p ^ i) \<le> x

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
have "real p ^ l \<le> real p ^ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real p ^ l \<le> real p ^ i
[PROOF STEP]
using pi x l
[PROOF STATE]
proof (prove)
using this:
prime p
l \<le> i
real (p ^ i) \<le> x
0 < x
0 < l

goal (1 subgoal):
 1. real p ^ l \<le> real p ^ i
[PROOF STEP]
by (intro power_increasing) (auto dest: prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
real p ^ l \<le> real p ^ i

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real p ^ l \<le> real p ^ i

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
have "\<dots> \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real p ^ i \<le> x
[PROOF STEP]
using pi
[PROOF STATE]
proof (prove)
using this:
prime p
l \<le> i
real (p ^ i) \<le> x

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

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real p ^ l \<le> x
[PROOF STEP]
have "root l (real p ^ l) \<le> root l x"
[PROOF STATE]
proof (prove)
using this:
real p ^ l \<le> x

goal (1 subgoal):
 1. root l (real p ^ l) \<le> root l x
[PROOF STEP]
using x pi l
[PROOF STATE]
proof (prove)
using this:
real p ^ l \<le> x
0 < x
prime p
l \<le> i
real (p ^ i) \<le> x
0 < l

goal (1 subgoal):
 1. root l (real p ^ l) \<le> root l x
[PROOF STEP]
by (subst real_root_le_iff) auto
[PROOF STATE]
proof (state)
this:
root l (real p ^ l) \<le> root l x

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
root l (real p ^ l) \<le> root l x

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
have "root l (real p ^ l) = real p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root l (real p ^ l) = real p
[PROOF STEP]
using pi l
[PROOF STATE]
proof (prove)
using this:
prime p
l \<le> i
real (p ^ i) \<le> x
0 < l

goal (1 subgoal):
 1. root l (real p ^ l) = real p
[PROOF STEP]
by (subst real_root_pos2) auto
[PROOF STATE]
proof (state)
this:
root l (real p ^ l) = real p

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> a \<le> nat \<lfloor>root l x\<rfloor>
 2. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real p \<le> root l x
[PROOF STEP]
show "p \<le> nat \<lfloor>root l x\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
real p \<le> root l x

goal (1 subgoal):
 1. p \<le> nat \<lfloor>root l x\<rfloor>
[PROOF STEP]
using pi l x
[PROOF STATE]
proof (prove)
using this:
real p \<le> root l x
prime p
l \<le> i
real (p ^ i) \<le> x
0 < l
0 < x

goal (1 subgoal):
 1. p \<le> nat \<lfloor>root l x\<rfloor>
[PROOF STEP]
by (simp add: le_nat_iff' le_floor_iff)
[PROOF STATE]
proof (state)
this:
p \<le> nat \<lfloor>root l x\<rfloor>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
from pi
[PROOF STATE]
proof (chain)
picking this:
prime p
l \<le> i
real (p ^ i) \<le> x
[PROOF STEP]
have "2 ^ i \<le> real p ^ i"
[PROOF STATE]
proof (prove)
using this:
prime p
l \<le> i
real (p ^ i) \<le> x

goal (1 subgoal):
 1. 2 ^ i \<le> real p ^ i
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
prime p
l \<le> i
real (p ^ i) \<le> x
0 < l

goal (1 subgoal):
 1. 2 ^ i \<le> real p ^ i
[PROOF STEP]
by (intro power_mono) (auto dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
2 ^ i \<le> real p ^ i

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 ^ i \<le> real p ^ i

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
have "\<dots> \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real p ^ i \<le> x
[PROOF STEP]
using pi
[PROOF STATE]
proof (prove)
using this:
prime p
l \<le> i
real (p ^ i) \<le> x

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>prime a; l \<le> b; real (a ^ b) \<le> x\<rbrakk> \<Longrightarrow> b \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 ^ i \<le> x
[PROOF STEP]
show "i \<le> nat \<lfloor>log 2 x\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
2 ^ i \<le> x

goal (1 subgoal):
 1. i \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
using pi x
[PROOF STATE]
proof (prove)
using this:
2 ^ i \<le> x
prime p
l \<le> i
real (p ^ i) \<le> x
0 < x

goal (1 subgoal):
 1. i \<le> nat \<lfloor>log 2 x\<rfloor>
[PROOF STEP]
by (auto simp: le_nat_iff' le_floor_iff le_log_iff powr_realpow)
[PROOF STATE]
proof (state)
this:
i \<le> nat \<lfloor>log 2 x\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mangoldt_non_primepow: "\<not>primepow n \<Longrightarrow> mangoldt n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> primepow n \<Longrightarrow> mangoldt n = (0::'a)
[PROOF STEP]
by (auto simp: mangoldt_def)


[STATEMENT]
lemma le_imp_bigo_real:
  assumes "c \<ge> 0" "eventually (\<lambda>x. f x \<le> c * (g x :: real)) F" "eventually (\<lambda>x. 0 \<le> f x) F"
  shows   "f \<in> O[F](g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> O[F](g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> O[F](g)
[PROOF STEP]
have "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. f x \<le> c * g x
\<forall>\<^sub>F x in F. 0 \<le> f x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f x \<le> c * g x; 0 \<le> f x\<rbrakk> \<Longrightarrow> norm (f x) \<le> c * norm (g x)
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
f x \<le> c * g x
0 \<le> f x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>f x \<le> c * g x; 0 \<le> f x\<rbrakk> \<Longrightarrow> norm (f x) \<le> c * norm (g x)
[PROOF STEP]
have "norm (f x) \<le> c * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (f x) \<le> c * g x
[PROOF STEP]
using elim
[PROOF STATE]
proof (prove)
using this:
f x \<le> c * g x
0 \<le> f x

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>f x \<le> c * g x; 0 \<le> f x\<rbrakk> \<Longrightarrow> norm (f x) \<le> c * norm (g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (f x) \<le> c * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>f x \<le> c * g x; 0 \<le> f x\<rbrakk> \<Longrightarrow> norm (f x) \<le> c * norm (g x)
[PROOF STEP]
have "\<dots> \<le> c * norm (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * g x \<le> c * norm (g x)
[PROOF STEP]
by (intro mult_left_mono assms) auto
[PROOF STATE]
proof (state)
this:
c * g x \<le> c * norm (g x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>f x \<le> c * g x; 0 \<le> f x\<rbrakk> \<Longrightarrow> norm (f x) \<le> c * norm (g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (f x) \<le> c * norm (g x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
norm (f x) \<le> c * norm (g x)

goal (1 subgoal):
 1. norm (f x) \<le> c * norm (g x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm (f x) \<le> c * norm (g x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)

goal (1 subgoal):
 1. f \<in> O[F](g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)

goal (1 subgoal):
 1. f \<in> O[F](g)
[PROOF STEP]
by (intro bigoI[of _ c]) auto
[PROOF STATE]
proof (state)
this:
f \<in> O[F](g)

goal:
No subgoals!
[PROOF STEP]
qed