# Theory Prime_Number_Theorem_Library

```section ‹Auxiliary material›
theory Prime_Number_Theorem_Library
imports
Zeta_Function.Zeta_Function
"HOL-Real_Asymp.Real_Asymp"
begin

text ‹Conflicting notation from \<^theory>‹HOL-Analysis.Infinite_Sum››
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)

lemma homotopic_loopsI:
fixes h :: "real × real ⇒ _"
assumes "continuous_on ({0..1} × {0..1}) h"
"h ` ({0..1} × {0..1}) ⊆ s"
"⋀x. x ∈ {0..1} ⟹ h (0, x) = p x"
"⋀x. x ∈ {0..1} ⟹ h (1, x) = q x"
"⋀x. x ∈ {0..1} ⟹ pathfinish (h ∘ Pair x) = pathstart (h ∘ Pair x)"
shows   "homotopic_loops s p q"
using assms unfolding homotopic_loops by (intro exI[of _ h]) auto

lemma homotopic_pathsI:
fixes h :: "real × real ⇒ _"
assumes "continuous_on ({0..1} × {0..1}) h"
assumes "h ` ({0..1} × {0..1}) ⊆ s"
assumes "⋀x. x ∈ {0..1} ⟹ h (0, x) = p x"
assumes "⋀x. x ∈ {0..1} ⟹ h (1, x) = q x"
assumes "⋀x. x ∈ {0..1} ⟹ pathstart (h ∘ Pair x) = pathstart p"
assumes "⋀x. x ∈ {0..1} ⟹ pathfinish (h ∘ Pair x) = pathfinish p"
shows   "homotopic_paths s p q"
using assms unfolding homotopic_paths by (intro exI[of _ h]) auto

lemma sum_upto_ln_conv_sum_upto_mangoldt:
"sum_upto (λn. ln (real n)) x = sum_upto (λn. mangoldt n * nat ⌊x / real n⌋) x"
proof -
have "sum_upto (λn. ln (real n)) x =
sum_upto (λn. ∑d | d dvd n. mangoldt d) x"
by (intro sum_upto_cong) (simp_all add: mangoldt_sum)
also have "… = sum_upto (λk. sum_upto (λd. mangoldt k) (x / real k)) x"
by (rule sum_upto_sum_divisors)
also have "… = sum_upto (λn. mangoldt n * nat ⌊x / real n⌋) x"
unfolding sum_upto_altdef by (simp add: mult_ac)
finally show ?thesis .
qed

lemma ln_fact_conv_sum_upto_mangoldt:
"ln (fact n) = sum_upto (λk. mangoldt k * (n div k)) n"
proof -
have [simp]: "{0<..Suc n} = insert (Suc n) {0<..n}" for n by auto
have "ln (fact n) = sum_upto (λn. ln (real n)) n"
by (induction n) (auto simp: sum_upto_altdef nat_add_distrib ln_mult)
also have "… = sum_upto (λk. mangoldt k * (n div k)) n"
unfolding sum_upto_ln_conv_sum_upto_mangoldt
by (intro sum_upto_cong) (auto simp: floor_divide_of_nat_eq)
finally show ?thesis .
qed

lemma fds_abs_converges_comparison_test:
fixes s :: "'a :: dirichlet_series"
assumes "eventually (λn. norm (fds_nth f n) ≤ fds_nth g n) at_top" and "fds_converges g (s ∙ 1)"
shows   "fds_abs_converges f s"
unfolding fds_abs_converges_def
proof (rule summable_comparison_test_ev)
from assms(2) show "summable (λn. fds_nth g n / n powr (s ∙ 1))"
by (auto simp: fds_converges_def)
from assms(1) eventually_gt_at_top[of 0]
show "eventually (λn. norm (norm (fds_nth f n / nat_power n s)) ≤
fds_nth g n / real n powr (s ∙ 1)) at_top"
by eventually_elim (auto simp: norm_divide norm_nat_power intro!: divide_right_mono)
qed

lemma fds_converges_scaleR [intro]:
assumes "fds_converges f s"
shows   "fds_converges (c *⇩R f) s"
proof -
from assms have "summable (λn. c *⇩R (fds_nth f n / nat_power n s))"
by (intro summable_scaleR_right) (auto simp: fds_converges_def)
also have "(λn. c *⇩R (fds_nth f n / nat_power n s)) = (λn. (c *⇩R fds_nth f n / nat_power n s))"
finally show ?thesis by (simp add: fds_converges_def)
qed

lemma fds_abs_converges_scaleR [intro]:
assumes "fds_abs_converges f s"
shows   "fds_abs_converges (c *⇩R f) s"
proof -
from assms have "summable (λn. abs c * norm (fds_nth f n / nat_power n s))"
by (intro summable_mult) (auto simp: fds_abs_converges_def)
also have "(λn. abs c * norm (fds_nth f n / nat_power n s)) =
(λn. norm ((c *⇩R fds_nth f n) / nat_power n s))" by (simp add: norm_divide)
finally show ?thesis by (simp add: fds_abs_converges_def)
qed

lemma conv_abscissa_scaleR: "conv_abscissa (scaleR c f) ≤ conv_abscissa f"
by (rule conv_abscissa_mono) auto

lemma abs_conv_abscissa_scaleR: "abs_conv_abscissa (scaleR c f) ≤ abs_conv_abscissa f"
by (rule abs_conv_abscissa_mono) auto

lemma fds_abs_converges_mult_const_left [intro]:
"fds_abs_converges f s ⟹ fds_abs_converges (fds_const c * f) s"
by (auto simp: fds_abs_converges_def norm_mult norm_divide dest: summable_mult[of _ "norm c"])

lemma conv_abscissa_mult_const_left:
"conv_abscissa (fds_const c * f) ≤ conv_abscissa f"
by (intro conv_abscissa_mono) auto

lemma abs_conv_abscissa_mult_const_left:
"abs_conv_abscissa (fds_const c * f) ≤ abs_conv_abscissa f"
by (intro abs_conv_abscissa_mono) auto

lemma fds_abs_converges_mult_const_right [intro]:
"fds_abs_converges f s ⟹ fds_abs_converges (f * fds_const c) s"
by (metis mult.commute fds_abs_converges_mult_const_left)

lemma conv_abscissa_mult_const_right:
"conv_abscissa (f * fds_const c) ≤ conv_abscissa f"
by (intro conv_abscissa_mono) auto

lemma abs_conv_abscissa_mult_const_right:
"abs_conv_abscissa (f * fds_const c) ≤ abs_conv_abscissa f"
by (intro abs_conv_abscissa_mono) auto

lemma bounded_coeffs_imp_fds_abs_converges:
fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
assumes "Bseq (fds_nth f)" "s ∙ 1 > 1"
shows   "fds_abs_converges f s"
proof -
from assms obtain C where C: "⋀n. norm (fds_nth f n) ≤ C"
by (auto simp: Bseq_def)
show ?thesis
proof (rule fds_abs_converges_comparison_test)
from ‹s ∙ 1 > 1› show "fds_converges (C *⇩R fds_zeta) (s ∙ 1)"
by (intro fds_abs_converges_imp_converges) auto
from C show "eventually (λn. norm (fds_nth f n) ≤ fds_nth (C *⇩R fds_zeta) n) at_top"
by (intro always_eventually) (auto simp: fds_nth_zeta)
qed
qed

lemma bounded_coeffs_imp_fds_abs_converges':
fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
assumes "Bseq (λn. fds_nth f n * nat_power n s0)" "s ∙ 1 > 1 - s0 ∙ 1"
shows   "fds_abs_converges f s"
proof -
have "fds_nth (fds_shift s0 f) = (λn. fds_nth f n * nat_power n s0)"
by (auto simp: fun_eq_iff)
with assms have "Bseq (fds_nth (fds_shift s0 f))" by simp
with assms(2) have "fds_abs_converges (fds_shift s0 f) (s + s0)"
by (intro bounded_coeffs_imp_fds_abs_converges) (auto simp: algebra_simps)
thus ?thesis by simp
qed

lemma bounded_coeffs_imp_abs_conv_abscissa_le:
fixes s :: "'a :: dirichlet_series" and f :: "'a fds" and c :: ereal
assumes "Bseq (λn. fds_nth f n * nat_power n s)" "1 - s ∙ 1 ≤ c"
shows   "abs_conv_abscissa f ≤ c"
proof (rule abs_conv_abscissa_leI_weak)
fix x assume "c < ereal x"
have "ereal (1 - s ∙ 1) ≤ c" by fact
also have "… < ereal x" by fact
finally have "1 - s ∙ 1 < ereal x" by simp
thus "fds_abs_converges f (of_real x)"
by (intro bounded_coeffs_imp_fds_abs_converges'[OF assms(1)]) auto
qed

lemma bounded_coeffs_imp_abs_conv_abscissa_le_1:
fixes s :: "'a :: dirichlet_series" and f :: "'a fds"
assumes "Bseq (λn. fds_nth f n)"
shows   "abs_conv_abscissa f ≤ 1"
proof -
have [simp]: "fds_nth f n * nat_power n 0 = fds_nth f n" for n
by (cases "n = 0") auto
show ?thesis
by (rule bounded_coeffs_imp_abs_conv_abscissa_le[where s = 0]) (insert assms, auto simp:)
qed

(* EXAMPLE: This might make a good example to illustrate real_asymp *)
lemma
fixes a b c :: real
assumes ab: "a + b > 0" and c: "c < -1"
shows set_integrable_powr_at_top: "(λx. (b + x) powr c) absolutely_integrable_on {a<..}"
and   set_lebesgue_integral_powr_at_top:
"(∫x∈{a<..}. ((b + x) powr c) ∂lborel) = -((b + a) powr (c + 1) / (c + 1))"
and   powr_has_integral_at_top:
"((λx. (b + x) powr c) has_integral -((b + a) powr (c + 1) / (c + 1))) {a<..}"
proof -
let ?f = "λx. (b + x) powr c" and ?F = "λx. (b + x) powr (c + 1) / (c + 1)"
have limits: "((?F ∘ real_of_ereal) ⤏ ?F a) (at_right (ereal a))"
"((?F ∘ real_of_ereal) ⤏ 0) (at_left ∞)"
using c ab unfolding ereal_tendsto_simps1 by (real_asymp simp: field_simps)+
have 1: "set_integrable lborel (einterval a ∞) ?f" using ab c limits
by (intro interval_integral_FTC_nonneg) (auto intro!: derivative_eq_intros)
thus 2: "?f absolutely_integrable_on {a<..}"
by (auto simp: set_integrable_def integrable_completion)
have "LBINT x=ereal a..∞. (b + x) powr c = 0 - ?F a" using ab c limits
by (intro interval_integral_FTC_nonneg) (auto intro!: derivative_eq_intros)
thus 3: "(∫x∈{a<..}. ((b + x) powr c) ∂lborel) = -((b + a) powr (c + 1) / (c + 1))"
show "(?f has_integral -((b + a) powr (c + 1) / (c + 1))) {a<..}"
using set_borel_integral_eq_integral[OF 1] 3 by (simp add: has_integral_iff)
qed

lemma fds_converges_altdef2:
"fds_converges f s ⟷ convergent (λN. eval_fds (fds_truncate N f) s)"
unfolding fds_converges_def summable_iff_convergent' eval_fds_truncate
by (auto simp: not_le intro!: convergent_cong always_eventually sum.mono_neutral_right)

lemma tendsto_eval_fds_truncate:
assumes "fds_converges f s"
shows   "(λN. eval_fds (fds_truncate N f) s) ⇢ eval_fds f s"
proof -
have "(λN. eval_fds (fds_truncate N f) s) ⇢ eval_fds f s ⟷
(λN. ∑i≤N. fds_nth f i / nat_power i s) ⇢ eval_fds f s"
unfolding eval_fds_truncate
by (intro filterlim_cong always_eventually allI sum.mono_neutral_left) (auto simp: not_le)
also have … using assms
by (simp add: fds_converges_iff sums_def' atLeast0AtMost)
finally show ?thesis .
qed

lemma linepath_translate_left: "linepath (c + a) (c + a) = (λx. c + a) ∘ linepath a b"
by auto

lemma linepath_translate_right: "linepath (a + c) (b + c) = (λx. x + c) ∘ linepath a b"
by (auto simp: fun_eq_iff linepath_def algebra_simps)

lemma has_contour_integral_linepath_same_Im_iff:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "Im a = Im b" "Re a < Re b"
shows   "(f has_contour_integral I) (linepath a b) ⟷
((λx. f (of_real x + Im a * 𝗂)) has_integral I) {Re a..Re b}"
proof -
have deriv: "vector_derivative ((λx. x - Im a * 𝗂) ∘ linepath a b) (at y) = b - a" for y
using linepath_translate_right[of a "-Im a * 𝗂" b, symmetric] by simp
have "(f has_contour_integral I) (linepath a b) ⟷
((λx. f (x + Im a * 𝗂)) has_contour_integral I) (linepath (a - Im a * 𝗂) (b - Im a * 𝗂))"
using linepath_translate_right[of a "-Im a * 𝗂" b] deriv by (simp add: has_contour_integral)
also have "… ⟷ ((λx. f (x + Im a * 𝗂)) has_integral I) {Re a..Re b}" using assms
by (subst has_contour_integral_linepath_Reals_iff) (auto simp: complex_is_Real_iff)
finally show ?thesis .
qed

lemma contour_integrable_linepath_same_Im_iff:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "Im a = Im b" "Re a < Re b"
shows   "(f contour_integrable_on linepath a b) ⟷
(λx. f (of_real x + Im a * 𝗂)) integrable_on {Re a..Re b}"
using contour_integrable_on_def has_contour_integral_linepath_same_Im_iff[OF assms] by blast

lemma contour_integral_linepath_same_Im:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "Im a = Im b" "Re a < Re b"
shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (λx. f (x + Im a * 𝗂))"
proof (cases "f contour_integrable_on linepath a b")
case True
thus ?thesis using has_contour_integral_linepath_same_Im_iff[OF assms, of f]
using has_contour_integral_integral has_contour_integral_unique by blast
next
case False
thus ?thesis using contour_integrable_linepath_same_Im_iff[OF assms, of f]
qed

lemmas [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1

interpretation cis: periodic_fun_simple cis "2 * pi"

lemma analytic_onE_box:
assumes "f analytic_on A" "s ∈ A"
obtains a b where "Re a < Re b" "Im a < Im b" "s ∈ box a b" "f analytic_on box a b"
proof -
from assms obtain r where r: "r > 0" "f holomorphic_on ball s r"
by (auto simp: analytic_on_def)
with open_contains_box[of "ball s r" s] obtain a b
where "box a b ⊆ ball s r" "s ∈ box a b" "∀i∈Basis. a ∙ i < b ∙ i" by auto
moreover from r have "f analytic_on ball s r" by (simp add: analytic_on_open)
ultimately show ?thesis using that[of a b] analytic_on_subset[of _ "ball s r" "box a b"]
by (auto simp: Basis_complex_def)
qed

lemma Re_image_box:
assumes "Re a < Re b" "Im a < Im b"
shows   "Re ` box a b = {Re a<..<Re b}"
using inner_image_box[of "1::complex" a b] assms by (auto simp: Basis_complex_def)

lemma Im_image_box:
assumes "Re a < Re b" "Im a < Im b"
shows   "Im ` box a b = {Im a<..<Im b}"
using inner_image_box[of "𝗂::complex" a b] assms by (auto simp: Basis_complex_def)

lemma Re_image_cbox:
assumes "Re a ≤ Re b" "Im a ≤ Im b"
shows   "Re ` cbox a b = {Re a..Re b}"
using inner_image_cbox[of "1::complex" a b] assms by (auto simp: Basis_complex_def)

lemma Im_image_cbox:
assumes "Re a ≤ Re b" "Im a ≤ Im b"
shows   "Im ` cbox a b = {Im a..Im b}"
using inner_image_cbox[of "𝗂::complex" a b] assms by (auto simp: Basis_complex_def)

lemma analytic_onE_cball:
assumes "f analytic_on A" "s ∈ A" "ub > (0::real)"
obtains R where "R > 0" "R < ub" "f analytic_on cball s R"
proof -
from assms obtain r where "r > 0" "f holomorphic_on ball s r"
by (auto simp: analytic_on_def)
hence "f analytic_on ball s r" by (simp add: analytic_on_open)
hence "f analytic_on cball s (min (ub / 2) (r / 2))"
by (rule analytic_on_subset, subst cball_subset_ball_iff) (use ‹r > 0› in auto)
moreover have "min (ub / 2) (r / 2) > 0" and "min (ub / 2) (r / 2) < ub"
using ‹r > 0› and ‹ub > 0› by (auto simp: min_def)
ultimately show ?thesis using that[of "min (ub / 2) (r / 2)"]
by blast
qed

corollary analytic_pre_zeta' [analytic_intros]:
assumes "f analytic_on A" "a > 0"
shows   "(λx. pre_zeta a (f x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_pre_zeta[of a UNIV]] assms(2)
by (auto simp: o_def)

corollary analytic_hurwitz_zeta' [analytic_intros]:
assumes "f analytic_on A" "(⋀x. x ∈ A ⟹ f x ≠ 1)" "a > 0"
shows   "(λx. hurwitz_zeta a (f x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_hurwitz_zeta[of a "-{1}"]] assms(2,3)
by (auto simp: o_def)

corollary analytic_zeta' [analytic_intros]:
assumes "f analytic_on A" "(⋀x. x ∈ A ⟹ f x ≠ 1)"
shows   "(λx. zeta (f x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_zeta[of "-{1}"]] assms(2)
by (auto simp: o_def)

lemma logderiv_zeta_analytic: "(λs. deriv zeta s / zeta s) analytic_on {s. Re s ≥ 1} - {1}"
using zeta_Re_ge_1_nonzero by (auto intro!: analytic_intros)

lemma mult_real_sqrt: "x ≥ 0 ⟹ x * sqrt y = sqrt (x ^ 2 * y)"

lemma arcsin_pos: "x ∈ {0<..1} ⟹ arcsin x > 0"
using arcsin_less_arcsin[of 0 x] by simp

lemmas analytic_imp_holomorphic' = holomorphic_on_subset[OF analytic_imp_holomorphic]

lemma residue_simple':
assumes "open s" "0 ∈ s" "f holomorphic_on s"
shows   "residue (λw. f w / w) 0 = f 0"
using residue_simple[of s 0 f] assms by simp

lemma fds_converges_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top" "s = s'"
shows   "fds_converges f s ⟷ fds_converges g s'"
unfolding fds_converges_def
by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms)

lemma fds_abs_converges_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top" "s = s'"
shows   "fds_abs_converges f s ⟷ fds_abs_converges g s'"
unfolding fds_abs_converges_def
by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms)

lemma conv_abscissa_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top"
shows   "conv_abscissa f = conv_abscissa g"
proof -
have "fds_converges f = fds_converges g"
by (intro ext fds_converges_cong assms refl)
thus ?thesis by (simp add: conv_abscissa_def)
qed

lemma abs_conv_abscissa_cong:
assumes "eventually (λn. fds_nth f n = fds_nth g n) at_top"
shows   "abs_conv_abscissa f = abs_conv_abscissa g"
proof -
have "fds_abs_converges f = fds_abs_converges g"
by (intro ext fds_abs_converges_cong assms refl)
thus ?thesis by (simp add: abs_conv_abscissa_def)
qed

definition fds_remainder where
"fds_remainder m = fds_subseries (λn. n > m)"

lemma fds_nth_remainder: "fds_nth (fds_remainder m f) = (λn. if n > m then fds_nth f n else 0)"
by (simp add: fds_remainder_def fds_subseries_def fds_nth_fds')

lemma fds_converges_remainder_iff [simp]:
"fds_converges (fds_remainder m f) s ⟷ fds_converges f s"
by (intro fds_converges_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)

lemma fds_abs_converges_remainder_iff [simp]:
"fds_abs_converges (fds_remainder m f) s ⟷ fds_abs_converges f s"
by (intro fds_abs_converges_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)

lemma fds_converges_remainder [intro]:
"fds_converges f s ⟹ fds_converges (fds_remainder m f) s"
and fds_abs_converges_remainder [intro]:
"fds_abs_converges f s ⟹ fds_abs_converges (fds_remainder m f) s"
by simp_all

lemma conv_abscissa_remainder [simp]:
"conv_abscissa (fds_remainder m f) = conv_abscissa f"
by (intro conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)

lemma abs_conv_abscissa_remainder [simp]:
"abs_conv_abscissa (fds_remainder m f) = abs_conv_abscissa f"
by (intro abs_conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]])
(auto simp: fds_nth_remainder)

lemma eval_fds_remainder:
"eval_fds (fds_remainder m f) s = (∑n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)"
(is "_ = suminf (λn. ?f (n + Suc m))")
proof (cases "fds_converges f s")
case False
hence "¬fds_converges (fds_remainder m f) s" by simp
hence "(λx. (λn. fds_nth (fds_remainder m f) n / nat_power n s) sums x) = (λ_. False)"
by (auto simp: fds_converges_def summable_def)
hence "eval_fds (fds_remainder m f) s = (THE _. False)"
moreover from False have "¬summable (λn. ?f (n + Suc m))" unfolding fds_converges_def
by (subst summable_iff_shift) auto
hence "(λx. (λn. ?f (n + Suc m)) sums x) = (λ_. False)"
by (auto simp: summable_def)
hence "suminf (λn. ?f (n + Suc m)) = (THE _. False)"
ultimately show ?thesis by simp
next
case True
hence *: "fds_converges (fds_remainder m f) s" by simp
have "eval_fds (fds_remainder m f) s = (∑n. fds_nth (fds_remainder m f) n / nat_power n s)"
unfolding eval_fds_def ..
also have "… = (∑n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)"
using * unfolding fds_converges_def
by (subst suminf_minus_initial_segment) (auto simp: fds_nth_remainder)
also have "(λn. fds_nth (fds_remainder m f) (n + Suc m)) = (λn. fds_nth f (n + Suc m))"
by (intro ext) (auto simp: fds_nth_remainder)
finally show ?thesis .
qed

lemma fds_truncate_plus_remainder: "fds_truncate m f + fds_remainder m f = f"
by (intro fds_eqI) (auto simp: fds_truncate_def fds_remainder_def fds_subseries_def)

lemma holomorphic_fds_eval' [holomorphic_intros]:
assumes "g holomorphic_on A" "⋀x. x ∈ A ⟹ Re (g x) > conv_abscissa f"
shows   "(λx. eval_fds f (g x)) holomorphic_on A"
using holomorphic_on_compose_gen[OF assms(1) holomorphic_fds_eval[OF order.refl, of f]] assms(2)
by (auto simp: o_def)

lemma analytic_fds_eval' [analytic_intros]:
assumes "g analytic_on A" "⋀x. x ∈ A ⟹ Re (g x) > conv_abscissa f"
shows   "(λx. eval_fds f (g x)) analytic_on A"
using analytic_on_compose_gen[OF assms(1) analytic_fds_eval[OF order.refl, of f]] assms(2)
by (auto simp: o_def)

lemma continuous_on_linepath [continuous_intros]:
assumes "continuous_on A a" "continuous_on A b" "continuous_on A f"
shows   "continuous_on A (λx. linepath (a x) (b x) (f x))"
using assms by (auto simp: linepath_def intro!: continuous_intros assms)

lemma continuous_on_part_circlepath [continuous_intros]:
assumes "continuous_on A c" "continuous_on A r" "continuous_on A a" "continuous_on A b"
"continuous_on A f"
shows   "continuous_on A (λx. part_circlepath (c x) (r x) (a x) (b x) (f x))"
using assms by (auto simp: part_circlepath_def intro!: continuous_intros assms)

lemma homotopic_loops_part_circlepath:
assumes "sphere c r ⊆ A" and "r ≥ 0" and
"b1 = a1 + 2 * of_int k * pi" and "b2 = a2 + 2 * of_int k * pi"
shows   "homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)"
proof -
define h where "h = (λ(x,y). part_circlepath c r (linepath a1 a2 x) (linepath b1 b2 x) y)"
show ?thesis
proof (rule homotopic_loopsI)
show "continuous_on ({0..1} × {0..1}) h"
by (auto simp: h_def case_prod_unfold intro!: continuous_intros)
next
from assms have "h ` ({0..1} × {0..1}) ⊆ sphere c r"
by (auto simp: h_def part_circlepath_def dist_norm norm_mult)
also have "… ⊆ A" by fact
finally show "h ` ({0..1} × {0..1}) ⊆ A" .
next
fix x :: real assume x: "x ∈ {0..1}"
show "h (0, x) = part_circlepath c r a1 b1 x" and "h (1, x) = part_circlepath c r a2 b2 x"
have "cis (pi * (real_of_int k * 2)) = 1"
using cis.plus_of_int[of 0 k] by (simp add: algebra_simps)
thus "pathfinish (h ∘ Pair x) = pathstart (h ∘ Pair x)"
by (simp add: h_def o_def exp_eq_polar linepath_def algebra_simps
cis_mult [symmetric] cis_divide [symmetric] assms)
qed
qed

lemma part_circlepath_conv_subpath:
"part_circlepath c r a b = subpath (a / (2*pi)) (b / (2*pi)) (circlepath c r)"
by (simp add: part_circlepath_def circlepath_def subpath_def linepath_def algebra_simps exp_eq_polar)

lemma homotopic_paths_part_circlepath:
assumes "a ≤ b" "b ≤ c"
assumes "path_image (part_circlepath C r a c) ⊆ A" "r ≥ 0"
shows   "homotopic_paths A (part_circlepath C r a c)
(part_circlepath C r a b +++ part_circlepath C r b c)"
(is "homotopic_paths _ ?g (?h1 +++ ?h2)")
proof (cases "a = c")
case False
with assms have "a < c" by simp
define slope where "slope = (b - a) / (c - a)"
from assms and ‹a < c› have slope: "slope ∈ {0..1}"
by (auto simp: field_simps slope_def)
define f :: "real ⇒ real" where
"f = linepath 0 slope +++ linepath slope 1"

show ?thesis
proof (rule homotopic_paths_reparametrize)
fix t :: real assume t: "t ∈ {0..1}"
show "(?h1 +++ ?h2) t = ?g (f t)"
proof (cases "t ≤ 1 / 2")
case True
hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
also from True ‹a < c› have "(1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b"
unfolding f_def slope_def linepath_def joinpaths_def
by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
also from True have "C + r * cis … = (?h1 +++ ?h2) t"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
finally show ?thesis ..
next
case False
hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
also from False ‹a < c› have "(1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c"
unfolding f_def slope_def linepath_def joinpaths_def
by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
also from False have "C + r * cis … = (?h1 +++ ?h2) t"
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
finally show ?thesis ..
qed
next
from slope have "path_image f ⊆ {0..1}"
by (auto simp: f_def path_image_join closed_segment_eq_real_ivl)
thus "f ∈ {0..1} → {0..1}" by (force simp add: path_image_def)
next
have "path f" unfolding f_def by auto
thus "continuous_on {0..1} f" by (simp add: path_def)
qed (insert assms, auto simp: f_def joinpaths_def linepath_def)
next
case [simp]: True
with assms have [simp]: "b = c" by auto
have "part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c"
by (simp add: fun_eq_iff joinpaths_def part_circlepath_def)
thus ?thesis using assms by simp
qed

lemma path_image_part_circlepath_subset:
assumes "a ≤ a'" "a' ≤ b'" "b' ≤ b"
shows   "path_image (part_circlepath c r a' b') ⊆ path_image (part_circlepath c r a b)"
using assms by (subst (1 2) path_image_part_circlepath) auto

lemma part_circlepath_mirror:
assumes "a' = a + pi + 2 * pi * of_int k" "b' = b + pi + 2 * pi * of_int k" "c' = -c"
shows   "-part_circlepath c r a b = part_circlepath c' r a' b'"
proof
fix x :: real
have "part_circlepath c' r a' b' x = c' + r * cis (linepath a b x + pi + k * (2 * pi))"
by (simp add: part_circlepath_def exp_eq_polar assms linepath_translate_right mult_ac)
also have "cis (linepath a b x + pi + k * (2 * pi)) = cis (linepath a b x + pi)"
by (rule cis.plus_of_int)
also have "… = -cis (linepath a b x)"
also have "c' + r * … = -part_circlepath c r a b x"
by (simp add: part_circlepath_def assms exp_eq_polar)
finally show "(- part_circlepath c r a b) x = part_circlepath c' r a' b' x"
by simp
qed

lemma path_mirror [intro]: "path (g :: _ ⇒ 'b::topological_group_add) ⟹ path (-g)"
by (auto simp: path_def intro!: continuous_intros)

lemma path_mirror_iff [simp]: "path (-g :: _ ⇒ 'b::topological_group_add) ⟷ path g"
using path_mirror[of g] path_mirror[of "-g"] by (auto simp: fun_Compl_def)

lemma valid_path_mirror [intro]: "valid_path g ⟹ valid_path (-g)"
by (auto simp: valid_path_def fun_Compl_def piecewise_C1_differentiable_neg)

lemma valid_path_mirror_iff [simp]: "valid_path (-g) ⟷ valid_path g"
using valid_path_mirror[of g] valid_path_mirror[of "-g"] by (auto simp: fun_Compl_def)

lemma pathstart_mirror [simp]: "pathstart (-g) = -pathstart g"
and pathfinish_mirror [simp]: "pathfinish (-g) = -pathfinish g"

lemma path_image_mirror: "path_image (-g) = uminus ` path_image g"
by (auto simp: path_image_def)

lemma cos_le_zero:
assumes "x ∈ {pi/2..3*pi/2}"
shows   "cos x ≤ 0"
proof -
have "cos x = -cos (x - pi)" by (simp add: cos_diff)
moreover from assms have "cos (x - pi) ≥ 0"
by (intro cos_ge_zero) auto
ultimately show ?thesis by simp
qed

lemma cos_le_zero': "x ∈ {-3*pi/2..-pi/2} ⟹ cos x ≤ 0"
using cos_le_zero[of "-x"] by simp

lemma winding_number_join_pos_combined':
"⟦valid_path γ1 ∧ z ∉ path_image γ1 ∧ 0 < Re (winding_number γ1 z);
valid_path γ2 ∧ z ∉ path_image γ2 ∧ 0 < Re (winding_number γ2 z);
pathfinish γ1 = pathstart γ2⟧
⟹ valid_path(γ1 +++ γ2) ∧ z ∉ path_image(γ1 +++ γ2) ∧ 0 < Re(winding_number(γ1 +++ γ2) z)"
by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)

lemma Union_atLeastAtMost_real_of_nat:
assumes "a < b"
shows   "(⋃n∈{a..<b}. {real n..real (n + 1)}) = {real a..real b}"
proof (intro equalityI subsetI)
fix x assume x: "x ∈ {real a..real b}"
thus "x ∈ (⋃n∈{a..<b}. {real n..real (n + 1)})"
proof (cases "x = real b")
case True
with assms show ?thesis by (auto intro!: bexI[of _ "b - 1"])
next
case False
with x have x: "x ≥ real a" "x < real b" by simp_all
hence "x ≥ real (nat ⌊x⌋)" "x ≤ real (Suc (nat ⌊x⌋))" by linarith+
moreover from x have "nat ⌊x⌋ ≥ a" "nat ⌊x⌋ < b" by linarith+
ultimately show ?thesis by force
qed
qed auto

lemma nat_sum_has_integral_floor:
fixes f :: "nat ⇒ 'a :: banach"
assumes mn: "m < n"
shows "((λx. f (nat ⌊x⌋)) has_integral sum f {m..<n}) {real m..real n}"
proof -
define D where "D = (λi. {real i..real (Suc i)}) ` {m..<n}"
have D: "D division_of {m..n}"
using Union_atLeastAtMost_real_of_nat[OF mn] by (simp add: division_of_def D_def)
have "((λx. f (nat ⌊x⌋)) has_integral (∑X∈D. f (nat ⌊Inf X⌋))) {real m..real n}"
proof (rule has_integral_combine_division)
fix X assume X: "X ∈ D"
have "nat ⌊x⌋ = nat ⌊Inf X⌋" if "x ∈ X - {Sup X}" for x
using that X by (auto simp: D_def nat_eq_iff floor_eq_iff)
hence "((λx. f (nat ⌊x⌋)) has_integral f (nat ⌊Inf X⌋)) X ⟷
((λx. f (nat ⌊Inf X⌋)) has_integral f (nat ⌊Inf X⌋)) X" using X
by (intro has_integral_spike_eq[of "{Sup X}"]) auto
also from X have "…" using has_integral_const_real[of "f (nat ⌊Inf X⌋)" "Inf X" "Sup X"]
by (auto simp: D_def)
finally show "((λx. f (nat ⌊x⌋)) has_integral f (nat ⌊Inf X⌋)) X" .
qed fact+
also have "(∑X∈D. f (nat ⌊Inf X⌋)) = (∑k∈{m..<n}. f k)"
unfolding D_def by (subst sum.reindex) (auto simp: inj_on_def nat_add_distrib)
finally show ?thesis .
qed

lemma nat_sum_has_integral_ceiling:
fixes f :: "nat ⇒ 'a :: banach"
assumes mn: "m < n"
shows "((λx. f (nat ⌈x⌉)) has_integral sum f {m<..n}) {real m..real n}"
proof -
define D where "D = (λi. {real i..real (Suc i)}) ` {m..<n}"
have D: "D division_of {m..n}"
using Union_atLeastAtMost_real_of_nat[OF mn] by (simp add: division_of_def D_def)
have "((λx. f (nat ⌈x⌉)) has_integral (∑X∈D. f (nat ⌊Sup X⌋))) {real m..real n}"
proof (rule has_integral_combine_division)
fix X assume X: "X ∈ D"
have "nat ⌈x⌉ = nat ⌊Sup X⌋" if "x ∈ X - {Inf X}" for x
using that X by (auto simp: D_def nat_eq_iff ceiling_eq_iff)
hence "((λx. f (nat ⌈x⌉)) has_integral f (nat ⌊Sup X⌋)) X ⟷
((λx. f (nat ⌊Sup X⌋)) has_integral f (nat ⌊Sup X⌋)) X" using X
by (intro has_integral_spike_eq[of "{Inf X}"]) auto
also from X have "…" using has_integral_const_real[of "f (nat ⌊Sup X⌋)" "Inf X" "Sup X"]
by (auto simp: D_def)
finally show "((λx. f (nat ⌈x⌉)) has_integral f (nat ⌊Sup X⌋)) X" .
qed fact+
also have "(∑X∈D. f (nat ⌊Sup X⌋)) = (∑k∈{m..<n}. f (Suc k))"
unfolding D_def by (subst sum.reindex) (auto simp: inj_on_def nat_add_distrib)
also have "… = (∑k∈{m<..n}. f k)"
by (intro sum.reindex_bij_witness[of _ "λx. x - 1" Suc]) auto
finally show ?thesis .
qed

lemma zeta_partial_sum_le:
fixes x :: real and m :: nat
assumes x: "x ∈ {0<..1}"
shows "(∑k=1..m. real k powr (x - 1)) ≤ real m powr x / x"
proof -
consider "m = 0" | "m = 1" | "m > 1" by force
thus ?thesis
proof cases
assume m: "m > 1"
hence "{1..m} = insert 1 {1<..m}" by auto
also have "(∑k∈…. real k powr (x - 1)) = 1 + (∑k∈{1<..m}. real k powr (x - 1))"
by simp
also have "(∑k∈{1<..m}. real k powr (x - 1)) ≤ real m powr x / x - 1 / x"
proof (rule has_integral_le)
show "((λt. (nat ⌈t⌉) powr (x - 1)) has_integral (∑n∈{1<..m}. n powr (x - 1))) {real 1..m}"
using m by (intro nat_sum_has_integral_ceiling) auto
next
have "((λt. t powr (x - 1)) has_integral (real m powr x / x - real 1 powr x / x))
{real 1..real m}"
by (intro fundamental_theorem_of_calculus)
(insert x m, auto simp flip: has_real_derivative_iff_has_vector_derivative
intro!: derivative_eq_intros)
thus "((λt. t powr (x - 1)) has_integral (real m powr x / x - 1 / x)) {real 1..real m}"
by simp
qed (insert x, auto intro!: powr_mono2')
also have "1 + (real m powr x / x - 1 / x) ≤ real m powr x / x"
using x by (simp add: field_simps)
finally show ?thesis by simp
qed (use assms in auto)
qed

lemma zeta_partial_sum_le':
fixes x :: real and m :: nat
assumes x: "x > 0" and m: "m > 0"
shows   "(∑n=1..m. real n powr (x - 1)) ≤ m powr x * (1 / x + 1 / m)"
proof (cases "x > 1")
case False
with assms have "(∑n=1..m. real n powr (x - 1)) ≤ m powr x / x"
by (intro zeta_partial_sum_le) auto
also have "… ≤ m powr x * (1 / x + 1 / m)"
using assms by (simp add: field_simps)
finally show ?thesis .
next
case True
have "(∑n∈{1..m}. n powr (x - 1)) = (∑n∈insert m {0..<m}. n powr (x - 1))"
by (intro sum.mono_neutral_left) auto
also have "… = m powr (x - 1) + (∑n∈{0..<m}. n powr (x - 1))" by simp
also have "(∑n∈{0..<m}. n powr (x - 1)) ≤ real m powr x / x"
proof (rule has_integral_le)
show "((λt. (nat ⌊t⌋) powr (x - 1)) has_integral (∑n∈{0..<m}. n powr (x - 1))) {real 0..m}"
using m by (intro nat_sum_has_integral_floor) auto
next
show "((λt. t powr (x - 1)) has_integral (real m powr x / x)) {real 0..real m}"
using has_integral_powr_from_0[of "x - 1"] x by auto
next
fix t assume "t ∈ {real 0..real m}"
with ‹x > 1› show "real (nat ⌊t⌋) powr (x - 1) ≤ t powr (x - 1)"
by (cases "t = 0") (auto intro: powr_mono2)
qed
also have "m powr (x - 1) + m powr x / x = m powr x * (1 / x + 1 / m)"
using m x by (simp add: powr_diff field_simps)
finally show ?thesis by simp
qed

lemma natfun_bigo_1E:
assumes "(f :: nat ⇒ _) ∈ O(λ_. 1)"
obtains C where "C ≥ lb" "⋀n. norm (f n) ≤ C"
proof -
from assms obtain C N where "∀n≥N. norm (f n) ≤ C"
by (auto elim!: landau_o.bigE simp: eventually_at_top_linorder)
hence *: "norm (f n) ≤ Max ({C, lb} ∪ (norm ` f ` {..<N}))" for n
by (cases "n ≥ N") (subst Max_ge_iff; force simp: image_iff)+
moreover have "Max ({C, lb} ∪ (norm ` f ` {..<N})) ≥ lb"
by (intro Max.coboundedI) auto
ultimately show ?thesis using that by blast
qed

lemma natfun_bigo_iff_Bseq: "f ∈ O(λ_. 1) ⟷ Bseq f"
proof
assume "Bseq f"
then obtain C where "C > 0" "⋀n. norm (f n) ≤ C" by (auto simp: Bseq_def)
thus "f ∈ O(λ_. 1)" by (intro bigoI[of _ C]) auto
next
assume "f ∈ O(λ_. 1)"
from natfun_bigo_1E[OF this, where lb = 1] obtain C where "C ≥ 1" "⋀n. norm (f n) ≤ C"
by auto
thus "Bseq f" by (auto simp: Bseq_def intro!: exI[of _ C])
qed

lemma enn_decreasing_sum_le_set_nn_integral:
fixes f :: "real ⇒ ennreal"
assumes decreasing: "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f y ≤ f x"
shows "(∑n. f (real (Suc n))) ≤ set_nn_integral lborel {0..} f"
proof -
have "(∑n. (f (Suc n))) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. (f (Suc n)) ∂lborel)"
by (subst nn_integral_cmult_indicator) auto
also have "nat ⌈x⌉ = Suc n" if "x ∈ {real n<..real (Suc n)}" for x n
using that by (auto simp: nat_eq_iff ceiling_eq_iff)
hence "(∑n. ∫⇧+x∈{real n<..real (Suc n)}. (f (Suc n)) ∂lborel) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. (f (real (nat ⌈x⌉))) ∂lborel)"
by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def)
also have "… = (∫⇧+x∈(⋃i. {real i<..real (Suc i)}). (f (nat ⌈x::real⌉)) ∂lborel)"
by (subst nn_integral_disjoint_family)
(auto simp: disjoint_family_on_def)
also have "… ≤ (∫⇧+x∈{0..}. (f x) ∂lborel)"
by (intro nn_integral_mono) (auto simp: indicator_def intro!: decreasing)
finally show ?thesis .
qed

lemma abs_summable_on_uminus_iff:
"(λx. -f x) abs_summable_on A ⟷ f abs_summable_on A"

lemma abs_summable_on_cmult_right_iff:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field, second_countable_topology}"
assumes "c ≠ 0"
shows   "(λx. c * f x) abs_summable_on A ⟷ f abs_summable_on A"

lemma abs_summable_on_cmult_left_iff:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field, second_countable_topology}"
assumes "c ≠ 0"
shows   "(λx. f x * c) abs_summable_on A ⟷ f abs_summable_on A"

lemma decreasing_sum_le_integral:
fixes f :: "real ⇒ real"
assumes nonneg: "⋀x. x ≥ 0 ⟹ f x ≥ 0"
assumes decreasing: "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f y ≤ f x"
assumes integral: "(f has_integral I) {0..}"
shows   "summable (λi. f (real (Suc i)))" and "suminf (λi. f (real (Suc i))) ≤ I"
proof -
have [simp]: "I ≥ 0"
by (intro has_integral_nonneg[OF integral] nonneg) auto
have "(∑n. ennreal (f (Suc n))) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. ennreal (f (Suc n)) ∂lborel)"
by (subst nn_integral_cmult_indicator) auto
also have "nat ⌈x⌉ = Suc n" if "x ∈ {real n<..real (Suc n)}" for x n
using that by (auto simp: nat_eq_iff ceiling_eq_iff)
hence "(∑n. ∫⇧+x∈{real n<..real (Suc n)}. ennreal (f (Suc n)) ∂lborel) =
(∑n. ∫⇧+x∈{real n<..real (Suc n)}. ennreal (f (real (nat ⌈x⌉))) ∂lborel)"
by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def)
also have "… = (∫⇧+x∈(⋃i. {real i<..real (Suc i)}). ennreal (f (nat ⌈x::real⌉)) ∂lborel)"
by (subst nn_integral_disjoint_family)
(auto simp: disjoint_family_on_def intro!: measurable_completion)
also have "… ≤ (∫⇧+x∈{0..}. ennreal (f x) ∂lborel)"
by (intro nn_integral_mono) (auto simp: indicator_def nonneg intro!: decreasing)
also have "… = (∫⇧+ x. ennreal (indicat_real {0..} x * f x) ∂lborel)"
by (intro nn_integral_cong) (auto simp: indicator_def)
also have "… = ennreal I"
using nn_integral_has_integral_lebesgue[OF nonneg integral] by (auto simp: nonneg)
finally have *: "(∑n. ennreal (f (Suc n))) ≤ ennreal I" .
from * show summable: "summable (λi. f (real (Suc i)))"
by (intro summable_suminf_not_top) (auto simp: top_unique intro: nonneg)
note *
also from summable have "(∑n. ennreal (f (Suc n))) = ennreal (∑n. f (Suc n))"
by (subst suminf_ennreal2) (auto simp: o_def nonneg)
finally show "(∑n. f (real (Suc n))) ≤ I" by (subst (asm) ennreal_le_iff) auto
qed

lemma decreasing_sum_le_integral':
fixes f :: "real ⇒ real"
assumes "⋀x. x ≥ 0 ⟹ f x ≥ 0"
assumes "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f y ≤ f x"
assumes "(f has_integral I) {0..}"
shows   "summable (λi. f (real i))" and "suminf (λi. f (real i)) ≤ f 0 + I"
proof -
have "summable ((λi. f (real (Suc i))))"
using decreasing_sum_le_integral[OF assms] by (simp add: o_def)
thus *: "summable (λi. f (real i))" by (subst (asm) summable_Suc_iff)
have "(∑n. f (real (Suc n))) ≤ I" by (intro decreasing_sum_le_integral assms)
thus "suminf (λi. f (real i)) ≤ f 0 + I"
using * by (subst (asm) suminf_split_head) auto
qed

lemma of_nat_powr_neq_1_complex [simp]:
assumes "n > 1" "Re s ≠ 0"
shows   "of_nat n powr s ≠ (1::complex)"
proof -
have "norm (of_nat n powr s) = real n powr Re s"
also have "… ≠ 1"
using assms by (auto simp: powr_def)
finally show ?thesis by auto
qed

lemma fds_logderiv_completely_multiplicative:
fixes f :: "'a :: {real_normed_field} fds"
assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 ≠ 0"
shows   "fds_deriv f / f = - fds (λn. fds_nth f n * mangoldt n)"
proof -
have "fds_deriv f / f = - fds (λn. fds_nth f n * mangoldt n) * f / f"
using completely_multiplicative_fds_deriv[of "fds_nth f"] assms by simp
also have "… = - fds (λn. fds_nth f n * mangoldt n)"
using assms by (simp add: divide_fds_def fds_right_inverse)
finally show ?thesis .
qed

lemma fds_nth_logderiv_completely_multiplicative:
fixes f :: "'a :: {real_normed_field} fds"
assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 ≠ 0"
shows   "fds_nth (fds_deriv f / f) n = -fds_nth f n * mangoldt n"
using assms by (subst fds_logderiv_completely_multiplicative) (simp_all add: fds_nth_fds')

lemma eval_fds_logderiv_completely_multiplicative:
fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds"
defines "h ≡ fds_deriv f / f"
assumes "completely_multiplicative_function (fds_nth f)" and [simp]: "fds_nth f 1 ≠ 0"
assumes "s ∙ 1 > abs_conv_abscissa f"
shows  "(λp. of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))
abs_summable_on {p. prime p}" (is ?th1)
and  "eval_fds h s = -(∑⇩ap | prime p. of_real (ln (real p)) *
(1 / (1 - fds_nth f p / nat_power p s) - 1))" (is ?th2)
proof -
let ?P = "{p::nat. prime p}"
interpret f: completely_multiplicative_function "fds_nth f" by fact
have "fds_abs_converges h s"
using abs_conv_abscissa_completely_multiplicative_log_deriv[OF assms(2)] assms
by (intro fds_abs_converges) auto
hence *: "(λn. fds_nth h n / nat_power n s) abs_summable_on UNIV"
by (auto simp: h_def fds_abs_converges_altdef')

note *
also have "(λn. fds_nth h n / nat_power n s) abs_summable_on UNIV ⟷
(λx. -fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow"
unfolding h_def using fds_nth_logderiv_completely_multiplicative[OF assms(2)]
by (intro abs_summable_on_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
finally have sum1: "(λx. -fds_nth f x * mangoldt x / nat_power x s)
abs_summable_on Collect primepow"
by (rule abs_summable_on_subset) auto
also have "?this ⟷ (λ(p,k). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) /
nat_power (p ^ Suc k) s) abs_summable_on (?P × UNIV)"
using bij_betw_primepows unfolding case_prod_unfold
by (intro abs_summable_on_reindex_bij_betw [symmetric])
also have "… ⟷ (λ(p,k). -((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p))))
abs_summable_on (?P × UNIV)"
unfolding case_prod_unfold
by (intro abs_summable_on_cong, subst mangoldt_primepow)
(auto simp: f.mult f.power nat_power_mult_distrib nat_power_power_left power_divide
dest: prime_gt_1_nat)
finally have sum2: … .

have sum4: "summable (λn. (norm (fds_nth f p / nat_power p s)) ^ Suc n)" if p: "prime p" for p
proof -
have "summable (λn. ¦ln (real p)¦ * (norm (fds_nth f p / nat_power p s)) ^ Suc n)"
using p abs_summable_on_Sigma_project2[OF sum2, of p] unfolding abs_summable_on_nat_iff'
by (simp add: norm_power norm_mult norm_divide mult_ac del: power_Suc)
thus ?thesis by (rule summable_mult_D) (insert p, auto dest: prime_gt_1_nat)
qed
have sums: "(λn. (fds_nth f p / nat_power p s) ^ Suc n) sums
(1 / (1 - fds_nth f p / nat_power p s) - 1)" if p: "prime p" for p :: nat
proof -
from sum4[OF p] have "norm (fds_nth f p / nat_power p s) < 1"
unfolding summable_Suc_iff by (simp add: summable_geometric_iff)
from geometric_sums[OF this] show ?thesis by (subst sums_Suc_iff) auto
qed

have eq: "(∑⇩ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) =
-(of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))"
if p: "prime p" for p
proof -
have "(∑⇩ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) =
(∑⇩ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (-ln (real p))"
using sum4[of p] p
by (subst infsetsum_cmult_left [symmetric])
(auto simp: abs_summable_on_nat_iff' norm_power simp del: power_Suc)
also have "(∑⇩ak. (fds_nth f p / nat_power p s) ^ Suc k) =
(1 / (1 - fds_nth f p / nat_power p s) - 1)" using sum4[OF p] sums[OF p]
by (subst infsetsum_nat')
(auto simp: sums_iff abs_summable_on_nat_iff' norm_power simp del: power_Suc)
finally show ?thesis by (simp add: mult_ac)
qed

have sum3: "(λx. ∑⇩ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x))))
abs_summable_on {p. prime p}"
using sum2 by (rule abs_summable_on_Sigma_project1') auto
also have "?this ⟷ (λp. -(of_real (ln (real p)) *
(1 / (1 - fds_nth f p / nat_power p s) - 1))) abs_summable_on {p. prime p}"
by (intro abs_summable_on_cong eq) auto
also have "… ⟷ ?th1" by (subst abs_summable_on_uminus_iff) auto
finally show ?th1 .

have "eval_fds h s = (∑⇩an. fds_nth h n / nat_power n s)"
using * unfolding eval_fds_def by (subst infsetsum_nat') auto
also have "… = (∑⇩an ∈ {n. primepow n}. -fds_nth f n * mangoldt n / nat_power n s)"
unfolding h_def using fds_nth_logderiv_completely_multiplicative[OF assms(2)]
by (intro infsetsum_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
also have "… = (∑⇩a(p,k)∈(?P × UNIV). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) /
nat_power (p ^ Suc k) s)"
using bij_betw_primepows unfolding case_prod_unfold
by (intro infsetsum_reindex_bij_betw [symmetric])
also have "… = (∑⇩a(p,k)∈(?P × UNIV).
-((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))"
by (intro infsetsum_cong)
(auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat
nat_power_power_left divide_simps simp del: power_Suc)
also have "… = (∑⇩ap | prime p. ∑⇩ak.
- ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))"
using sum2 by (subst infsetsum_Times) (auto simp: case_prod_unfold)
also have "… = (∑⇩ap | prime p. -(of_real (ln (real p)) *
(1 / (1 - fds_nth f p / nat_power p s) - 1)))"
using eq by (intro infsetsum_cong) auto
finally show ?th2 by (subst (asm) infsetsum_uminus)
qed

lemma eval_fds_logderiv_zeta:
assumes "Re s > 1"
shows  "(λp. of_real (ln (real p)) / (p powr s - 1))
abs_summable_on {p. prime p}" (is ?th1)
and  "deriv zeta s / zeta s =
-(∑⇩ap | prime p. of_real (ln (real p)) / (p powr s - 1))" (is ?th2)
proof -
have *: "completely_multiplicative_function (fds_nth fds_zeta :: _ ⇒ complex)"
by standard auto
note abscissa = le_less_trans[OF abs_conv_abscissa_completely_multiplicative_log_deriv[OF *]]
have "(λp. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))
abs_summable_on {p. prime p}"
using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms by auto
also have "?this ⟷ (λp. ln (real p) / (p powr s - 1)) abs_summable_on {p. prime p}" using assms
by (intro abs_summable_on_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat)
finally show ?th1 .

from assms have ev: "eventually (λz. z ∈ {z. Re z > 1}) (nhds s)"
by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto
have "deriv zeta s = deriv (eval_fds fds_zeta) s"
by (intro deriv_cong_ev[OF eventually_mono[OF ev]]) (auto simp: eval_fds_zeta)
also have "deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s"
using assms zeta_Re_gt_1_nonzero[of s]
by (subst eval_fds_log_deriv) (auto simp: eval_fds_zeta eval_fds_deriv intro!: abscissa)
also have "eval_fds (fds_deriv fds_zeta / fds_zeta) s =
-(∑⇩ap | prime p. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))"
(is "_ = -?S") using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms by auto
also have "?S = (∑⇩ap | prime p. ln (real p) / (p powr s - 1))" using assms
by (intro infsetsum_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat)
finally show ?th2 .
qed

lemma sums_logderiv_zeta:
assumes "Re s > 1"
shows   "(λ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 -
note * = eval_fds_logderiv_zeta[OF assms]
from sums_infsetsum_nat[OF *(1)] and *(2) show ?thesis by simp
qed

lemma range_add_nat: "range (λn. n + c) = {(c::nat)..}"

lemma abs_summable_hurwitz_zeta:
assumes "Re s > 1" "a + real b > 0"
shows   "(λn. 1 / (of_nat n + a) powr s) abs_summable_on {b..}"
proof -
from assms have "summable (λn. cmod (1 / (of_nat (n + b) + a) powr s))"
using summable_hurwitz_zeta_real[of "Re s" "a + b"]
by (auto simp: norm_divide powr_minus field_simps norm_powr_real_powr)
hence "(λn. 1 / (of_nat (n + b) + a) powr s) abs_summable_on UNIV"