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 theoryHOL-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))"
    by (simp add: scaleR_conv_of_real)
  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))"
    by (simp add: interval_integral_to_infinity_eq)
  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. iN. 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]
    by (simp add: not_integrable_contour_integral not_integrable_integral)
qed


lemmas [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1

interpretation cis: periodic_fun_simple cis "2 * pi"
  by standard (simp_all add: complex_eq_iff)

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" "iBasis. 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)"
  by (simp add: real_sqrt_mult)

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)"
    by (simp add: eval_fds_def suminf_def)
  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)"
    by (simp add: suminf_def)
  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"
      by (simp_all add: h_def linepath_def)
    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)
           (simp add: algebra_simps)?
      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)
           (simp add: algebra_simps)?
      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)"
    by (simp add: minus_cis)
  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"
  by (simp_all add: pathstart_def pathfinish_def)

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 (XD. 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 "(XD. 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 (XD. 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 "(XD. 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)) = (ninsert 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 "nN. 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"
  by (simp add: abs_summable_on_def)

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"
  by (simp add: abs_summable_on_altdef assms)

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"
  by (simp add: abs_summable_on_altdef assms)

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"
    by (simp add: norm_powr_real_powr)
  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)..}"
  using Nat.le_imp_diff_is_add by auto

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"
    by (auto simp: abs_summable_on_nat_iff' add_ac)
  also have "?this  (λn. 1 / (of_nat n + a) powr s) abs_summable_on range (λn. n + b)"
    by (rule abs_summable_on_reindex_iff) auto
  also have "range (λn. n + b) = {b..}" by (rule range_add_nat)
  finally show ?thesis .
qed

lemma hurwitz_zeta_nat_conv_infsetsum:
  assumes "a > 0