Theory Dirichlet_Series.Dirichlet_Series_Analysis

(*
    File:      Dirichlet_Series_Analysis.thy
    Author:    Manuel Eberl, TU München
*)
section ‹Analytic properties of Dirichlet series›
theory Dirichlet_Series_Analysis
imports
  "HOL-Complex_Analysis.Complex_Analysis"
  "HOL-Library.Going_To_Filter"
  "HOL-Real_Asymp.Real_Asymp"
  Dirichlet_Series
  Moebius_Mu
  Partial_Summation
  Euler_Products
begin

text ‹Conflicting notation from theoryHOL-Analysis.Infinite_Sum
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)

text ‹
  The following illustrates a concept we will need later on: A property holds for
  f› going to F› if we can find e.\,g.\ a sequence that tends to F› and whose elements
  eventually satisfy P›.
›
lemma frequently_going_toI:
  assumes "filterlim (λn. f (g n)) F G"
  assumes "eventually (λn. P (g n)) G"
  assumes "eventually (λn. g n  A) G"
  assumes "G  bot"
  shows   "frequently P (f going_to F within A)"
  unfolding frequently_def
proof
  assume "eventually (λx. ¬P x) (f going_to F within A)"
  hence "eventually (λx. ¬P x) (inf (filtercomap f F) (principal A))"
    by (simp add: going_to_within_def)
  moreover have "filterlim (λn. g n) (inf (filtercomap f F) (principal A)) G"
    using assms unfolding filterlim_inf filterlim_principal
    by (auto simp add: filterlim_iff_le_filtercomap filtercomap_filtercomap)
  ultimately have "eventually (λn. ¬P (g n)) G"
    by (rule eventually_compose_filterlim)
  with assms(2) have "eventually (λ_. False) G" by eventually_elim auto
  with assms(4) show False by simp
qed

lemma frequently_filtercomapI:
  assumes "filterlim (λn. f (g n)) F G"
  assumes "eventually (λn. P (g n)) G"
  assumes "G  bot"
  shows   "frequently P (filtercomap f F)"
  using frequently_going_toI[of f g F G P UNIV] assms by (simp add: going_to_def)

lemma frequently_going_to_at_topE:
  fixes f :: "'a  real"
  assumes "frequently P (f going_to at_top)"
  obtains g where "n. P (g n)" and "filterlim (λn. f (g n)) at_top sequentially"
proof -
  from assms have "k. x. f x  real k  P x"
    by (auto simp: frequently_def eventually_going_to_at_top_linorder)
  hence "g. k. f (g k)  real k  P (g k)"
    by metis
  then obtain g where g: "k. f (g k)  real k" "k. P (g k)"
    by blast
  have "filterlim (λn. f (g n)) at_top sequentially"
    by (rule filterlim_at_top_mono[OF filterlim_real_sequentially]) (use g in auto)
  from g(2) and this show ?thesis using that[of g] by blast
qed

text ‹
  Apostol often uses statements like `$P(s_k)$ for all $k$ in an infinite sequence
  $s_k$ such that $\mathfrak{R}(s_k)\longrightarrow\infty$ as $k\to\infty$'.

  Instead, we write @{prop "frequently P (Re going_to at_top)"}. This lemma shows that
  our statement is equivalent to his.
›
lemma frequently_going_to_at_top_iff:
  "frequently P (f going_to (at_top :: real filter)) 
     (g. n. P (g n)  filterlim (λn. f (g n)) at_top sequentially)"
  by (auto intro: frequently_going_toI elim!: frequently_going_to_at_topE)
(* END TODO *)

lemma surj_bullet_1: "surj (λs::'a::{real_normed_algebra_1, real_inner}. s  1)"
proof (rule surjI)
  fix x :: real show "(x *R 1)  (1 :: 'a) = x"
    by (simp add: dot_square_norm)
qed  

lemma bullet_1_going_to_at_top_neq_bot [simp]:
  "((λs::'a::{real_normed_algebra_1, real_inner}. s  1) going_to at_top)  bot"
  unfolding going_to_def by (rule filtercomap_neq_bot_surj[OF _ surj_bullet_1]) auto



lemma fds_abs_converges_altdef:
  "fds_abs_converges f s  (λn. fds_nth f n / nat_power n s) abs_summable_on {1..}"
  by (auto simp add: fds_abs_converges_def abs_summable_on_nat_iff
           intro!: summable_cong eventually_mono[OF eventually_gt_at_top[of 0]])

lemma fds_abs_converges_altdef':
  "fds_abs_converges f s  (λn. fds_nth f n / nat_power n s) abs_summable_on UNIV"
  by (subst fds_abs_converges_altdef, rule abs_summable_on_cong_neutral) (auto simp: Suc_le_eq)

lemma eval_fds_altdef:
  assumes "fds_abs_converges f s"
  shows   "eval_fds f s = (an. fds_nth f n / nat_power n s)"
proof -
  have "fds_abs_converges f s  (λn. fds_nth f n / nat_power n s) abs_summable_on UNIV"
    unfolding fds_abs_converges_altdef 
    by (intro abs_summable_on_cong_neutral) (auto simp: Suc_le_eq)
  with assms show ?thesis unfolding eval_fds_def fds_abs_converges_altdef
    by (intro infsetsum_nat' [symmetric]) simp_all
qed

lemma multiplicative_function_divide_nat_power:
  fixes f :: "nat  'a :: {nat_power, field}"
  assumes "multiplicative_function f"
  shows   "multiplicative_function (λn. f n / nat_power n s)"
proof
  interpret f: multiplicative_function f by fact
  show "f 0 / nat_power 0 s = 0" "f 1 / nat_power 1 s = 1"
    by simp_all
  fix a b :: nat assume "a > 1" "b > 1" "coprime a b"
  thus "f (a * b) / nat_power (a * b) s = f a / nat_power a s * (f b / nat_power b s)"
    by (simp_all add: f.mult_coprime nat_power_mult_distrib)
qed

lemma completely_multiplicative_function_divide_nat_power:
  fixes f :: "nat  'a :: {nat_power, field}"
  assumes "completely_multiplicative_function f"
  shows   "completely_multiplicative_function (λn. f n / nat_power n s)"
proof
  interpret f: completely_multiplicative_function f by fact
  show "f 0 / nat_power 0 s = 0" "f (Suc 0) / nat_power (Suc 0) s = 1"
    by simp_all
  fix a b :: nat assume "a > 1" "b > 1"
  thus "f (a * b) / nat_power (a * b) s = f a / nat_power a s * (f b / nat_power b s)"
    by (simp_all add: f.mult nat_power_mult_distrib)
qed

subsection ‹Convergence and absolute convergence›

class nat_power_normed_field = nat_power_field + real_normed_field + real_inner + real_algebra_1 +
  fixes real_power :: "real  'a  'a"
  assumes real_power_nat_power: "n > 0  real_power (real n) c = nat_power n c"
  assumes real_power_1_right_aux: "d > 0  real_power d 1 = d *R 1"
  assumes real_power_add: "d > 0  real_power d (a + b) = real_power d a * real_power d b"
  assumes real_power_nonzero [simp]: "d > 0  real_power d a  0"
  assumes norm_real_power: "x > 0  norm (real_power x c) = x powr (c  1)"
  assumes nat_power_of_real_aux: "nat_power n (x *R 1) = ((real n powr x) *R 1)"
  assumes has_field_derivative_nat_power_aux:
            "x::'a. n > 0  LIM y inf_class.inf
              (Inf (principal ` {S. open S  x  S})) (principal (UNIV - {x})).
                (nat_power n y - nat_power n x - ln (real n) *R nat_power n x * (y - x)) /R
                norm (y - x) :> Inf (principal ` {S. open S  0  S})"
  assumes has_vector_derivative_real_power_aux:
            "x > 0  filterlim (λy. (real_power y c - real_power x (c :: 'a) -
               (y - x) *R (c * real_power x (c - 1))) /R
               norm (y - x)) (INF S{S. open S  0  S}. principal S) (at x)"
  assumes norm_nat_power: "n > 0  norm (nat_power n y) = real n powr (y  1)"
begin

lemma real_power_diff: "d > 0  real_power d (a - b) = real_power d a / real_power d b"
  using real_power_add[of d b "a - b"] by (simp add: field_simps)

end

lemma real_power_1_right [simp]: "d > 0  real_power d 1 = of_real d"
  using real_power_1_right_aux[of d] by (simp add: scaleR_conv_of_real)


lemma has_vector_derivative_real_power [derivative_intros]:
  "x > 0  ((λy. real_power y c) has_vector_derivative c * real_power x (c - 1)) (at x within A)"
  by (rule has_vector_derivative_at_within)
     (insert has_vector_derivative_real_power_aux[of x c],
      simp add: has_vector_derivative_def has_derivative_def
                nhds_def bounded_linear_scaleR_left)
              
lemma has_field_derivative_nat_power [derivative_intros]:
  "n > 0  ((λy. nat_power n y) has_field_derivative ln (real n) *R nat_power n x)
     (at (x :: 'a :: nat_power_normed_field) within A)"
  by (rule has_field_derivative_at_within)
     (insert has_field_derivative_nat_power_aux[of n x],
      simp only: has_field_derivative_def has_derivative_def netlimit_at,
      simp add: nhds_def at_within_def bounded_linear_mult_right)
              
lemma continuous_on_real_power [continuous_intros]: 
  "A  {0<..}  continuous_on A (λx. real_power x s)"
  by (rule continuous_on_vector_derivative has_vector_derivative_real_power)+ auto

instantiation real :: nat_power_normed_field
begin

definition real_power_real :: "real  real  real" where
  [simp]: "real_power_real = (powr)"
  
instance proof (standard, goal_cases)
  case (7 n x)
  hence "((λx. nat_power n x) has_field_derivative ln (real n) *R nat_power n x) (at x)"
    by (auto intro!: derivative_eq_intros simp: powr_def)
  thus ?case unfolding has_field_derivative_def netlimit_at has_derivative_def
    by (simp add: nhds_def at_within_def)
next
  case (8 x c)
  hence "((λy. real_power y c) has_vector_derivative c * real_power x (c - 1)) (at x)"
    by (auto intro!: derivative_eq_intros
             simp: has_real_derivative_iff_has_vector_derivative [symmetric])
  thus ?case by (simp add: has_vector_derivative_def has_derivative_def nhds_def)
qed (simp_all add: powr_add)

end


instantiation complex :: nat_power_normed_field
begin
  
definition nat_power_complex :: "nat  complex  complex" where
   [simp]: "nat_power_complex n z = of_nat n powr z"

definition real_power_complex :: "real  complex  complex" where
  [simp]: "real_power_complex = (λx y. of_real x powr y)"
  
instance proof
  fix m n :: nat and z :: complex
  assume "m > 0" "n > 0"
  thus "nat_power (m * n) z = nat_power m z * nat_power n z"
    unfolding nat_power_complex_def of_nat_mult by (subst powr_times_real) simp_all
next
  fix n :: nat and z :: complex
  assume "n > 0"
  show "norm (nat_power n z) = real n powr (z  1)" unfolding nat_power_complex_def
    using norm_powr_real_powr[of "of_nat n" z] by simp
next
  fix n :: nat and x :: complex assume n: "n > 0"
  hence "((λx. nat_power n x) has_field_derivative ln (real n) *R nat_power n x) (at x)"
    by (auto intro!: derivative_eq_intros simp: powr_def scaleR_conv_of_real mult_ac)
  thus "LIM y inf_class.inf (Inf (principal ` {S. open S  x  S})) (principal (UNIV - {x})).
           (nat_power n y - nat_power n x - ln (real n) *R nat_power n x * (y - x)) /R
           cmod (y - x) :> (Inf (principal ` {S. open S  0  S}))"
    unfolding has_field_derivative_def netlimit_at has_derivative_def
    by (simp add: nhds_def at_within_def)
next
  fix x :: real and c :: complex assume "x > 0"
  hence "((λy. real_power y c) has_vector_derivative c * real_power x (c - 1)) (at x)"
    by (auto intro!: derivative_eq_intros has_vector_derivative_real_field)
  thus "LIM y at x. (real_power y c - real_power x c - (y - x) *R (c * real_power x (c - 1))) /R
           norm (y - x) :> INF S{S. open S  0  S}. principal S"
    by (simp add: has_vector_derivative_def has_derivative_def nhds_def)
next
  fix n :: nat and x :: real
  show "nat_power n (x *R 1 :: complex) = (real n powr x) *R 1"
    by (simp add: powr_Reals_eq scaleR_conv_of_real)
qed (auto simp: powr_def exp_add exp_of_nat_mult [symmetric] algebra_simps scaleR_conv_of_real
          simp del: Ln_of_nat)

end

lemma nat_power_of_real [simp]:
  "nat_power n (of_real x :: 'a :: nat_power_normed_field) = of_real (real n powr x)"
  using nat_power_of_real_aux[of n x] by (simp add: scaleR_conv_of_real)

lemma fds_abs_converges_of_real [simp]: 
  "fds_abs_converges (fds_of_real f) 
     (of_real s :: 'a :: {nat_power_normed_field,banach})  fds_abs_converges f s"
  unfolding fds_abs_converges_def
  by (subst (1 2) summable_Suc_iff [symmetric]) (simp add: norm_divide norm_nat_power)

lemma eval_fds_of_real [simp]:
  assumes "fds_converges f s"
  shows   "eval_fds (fds_of_real f) (of_real s :: 'a :: {nat_power_normed_field,banach}) = 
             of_real (eval_fds f s)"
  using assms unfolding eval_fds_def by (auto simp: fds_converges_def suminf_of_real)

lemma fds_abs_summable_zeta_iff [simp]:
  fixes s :: "'a :: {banach, nat_power_normed_field}"
  shows "fds_abs_converges fds_zeta s  s  1 > (1 :: real)"
proof -
  have "fds_abs_converges fds_zeta s  summable (λn. real n powr -(s  1))"
    unfolding fds_abs_converges_def
    by (intro summable_cong always_eventually)
       (auto simp: norm_divide fds_nth_zeta powr_minus norm_nat_power divide_simps)
  also have "  s  1 > 1" by (simp add: summable_real_powr_iff)
  finally show ?thesis .
qed

lemma fds_abs_summable_zeta: 
  "(s :: 'a :: {banach, nat_power_normed_field})  1 > 1  fds_abs_converges fds_zeta s"
  by simp


lemma fds_abs_converges_moebius_mu:
  fixes s :: "'a :: {banach,nat_power_normed_field}"
  assumes "s  1 > 1"
  shows   "fds_abs_converges (fds moebius_mu) s"
  unfolding fds_abs_converges_def
proof (rule summable_comparison_test, intro exI allI impI)
  fix n :: nat
  show "norm (norm (fds_nth (fds moebius_mu) n / nat_power n s))  real n powr (-s  1)"
    by (auto simp: powr_minus divide_simps abs_moebius_mu_le norm_nat_power norm_divide
                   moebius_mu_def norm_power)
next
  from assms show "summable (λn. real n powr (-s  1))" by (simp add: summable_real_powr_iff)
qed


definition conv_abscissa
    :: "'a :: {nat_power,banach,real_normed_field, real_inner} fds  ereal" where
  "conv_abscissa f = (INF s{s. fds_converges f s}. ereal (s  1))"

definition abs_conv_abscissa
    :: "'a :: {nat_power,banach,real_normed_field, real_inner} fds  ereal" where
  "abs_conv_abscissa f = (INF s{s. fds_abs_converges f s}. ereal (s  1))"

lemma conv_abscissa_mono:
  assumes "s. fds_converges g s  fds_converges f s"
  shows   "conv_abscissa f  conv_abscissa g"
  unfolding conv_abscissa_def by (rule INF_mono) (use assms in auto)

lemma abs_conv_abscissa_mono:
  assumes "s. fds_abs_converges g s  fds_abs_converges f s"
  shows   "abs_conv_abscissa f  abs_conv_abscissa g"
  unfolding abs_conv_abscissa_def by (rule INF_mono) (use assms in auto)


class dirichlet_series = euclidean_space + real_normed_field + nat_power_normed_field +
  assumes one_in_Basis: "1  Basis"
    
instance real :: dirichlet_series by standard simp_all
instance complex :: dirichlet_series by standard (simp_all add: Basis_complex_def)

context
  assumes "SORT_CONSTRAINT('a :: dirichlet_series)"
begin

lemma fds_abs_converges_Re_le:
  fixes f :: "'a fds"
  assumes "fds_abs_converges f z" "z  1  z'  1"
  shows   "fds_abs_converges f z'"
  unfolding fds_abs_converges_def
proof (rule summable_comparison_test, intro exI allI impI)
  fix n :: nat assume n: "n  1"
  thus "norm (norm (fds_nth f n / nat_power n z'))  norm (fds_nth f n / nat_power n z)"
    using assms(2) by (simp add: norm_divide norm_nat_power divide_simps powr_mono mult_left_mono)
qed (insert assms(1), simp add: fds_abs_converges_def)

lemma fds_abs_converges:
  assumes "s  1 > abs_conv_abscissa (f :: 'a fds)"
  shows   "fds_abs_converges f s"
proof -
  from assms obtain s0 where "fds_abs_converges f s0" "s0  1 < s  1"
    by (auto simp: INF_less_iff abs_conv_abscissa_def)
  with fds_abs_converges_Re_le[OF this(1), of s] this(2) show ?thesis by simp
qed

lemma fds_abs_diverges:
  assumes "s  1 < abs_conv_abscissa (f :: 'a fds)"
  shows   "¬fds_abs_converges f s"
proof
  assume "fds_abs_converges f s"
  hence "abs_conv_abscissa f  s  1" unfolding abs_conv_abscissa_def
    by (intro INF_lower) auto
  with assms show False by simp
qed


lemma uniformly_Cauchy_eval_fds_aux:
  fixes s0 :: "'a :: dirichlet_series"
  assumes bounded: "Bseq (λn. kn. fds_nth f k / nat_power k s0)"
  assumes B: "compact B" "z. z  B  z  1 > s0  1"
  shows   "uniformly_Cauchy_on B (λN z. nN. fds_nth f n / nat_power n z)"
proof (cases "B = {}")
  case False
  show ?thesis
  proof (rule uniformly_Cauchy_onI', goal_cases)
    case (1 ε)
    define σ where "σ = Inf ((λs. s  1) ` B)"
    have σ_le: "s  1  σ" if "s  B" for s
      unfolding σ_def using that 
      by (intro cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded B) auto
    have "σ  ((λs. s  1) ` B)"
      unfolding σ_def using B B  {}
      by (intro closed_contains_Inf bounded_inner_imp_bdd_below compact_imp_bounded B 
            compact_imp_closed compact_continuous_image continuous_intros) auto
    with B(2) have σ_gt: "σ > s0  1" by auto
    define δ where "δ = σ - s0  1"
      
    have "bounded B" by (rule compact_imp_bounded) fact
    then obtain norm_B_aux where norm_B_aux: "s. s  B  norm s  norm_B_aux" 
      by (auto simp: bounded_iff)
    define norm_B where "norm_B = norm_B_aux + norm s0"
    from norm_B_aux have norm_B: "norm (s - s0)  norm_B" if "s  B" for s
      using norm_triangle_ineq4[of s s0] norm_B_aux[OF that] by (simp add: norm_B_def)
    then have "0  norm_B"
      by (meson σ  (λs. s  1) ` B imageE norm_ge_zero order.trans)
    define A where "A = sum_upto (λk. fds_nth f k / nat_power k s0)"
    from bounded obtain C_aux where C_aux: "n. norm (kn. fds_nth f k / nat_power k s0)  C_aux"
      by (auto simp: Bseq_def)
    define C where "C = max C_aux 1"
    have C_pos: "C > 0" by (simp add: C_def)
    have C: "norm (A x)  C" for x
    proof -
      have "A x = (knat x. fds_nth f k / nat_power k s0)"
        unfolding A_def sum_upto_altdef by (intro sum.mono_neutral_left) auto
      also have "norm   C_aux" by (rule C_aux)
      also have "  C" by (simp add: C_def)
      finally show ?thesis .
    qed
    
    have "(λm. 2 * C * (1 + norm_B / δ) * real m powr (-δ))  0" unfolding δ_def using σ_gt
      by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially) simp_all
    from order_tendstoD(2)[OF this ε > 0] obtain M where
      M: "m. m  M  2 * C * (1 + norm_B / δ) * real m powr - δ < ε" 
      by (auto simp: eventually_at_top_linorder)
      
    show ?case
    proof (intro exI[of _ "max M 1"] ballI allI impI, goal_cases)
      case (1 s m n)
      from 1 have s: "s  1 > s0  1" using B(2)[of s] by simp
      have mn: "m  M" "m < n" "m > 0" "n > 0" using 1 by (simp_all add: )
      have "dist (nm. fds_nth f n / nat_power n s) (nn. fds_nth f n / nat_power n s) =
              dist (nn. fds_nth f n / nat_power n s) (nm. fds_nth f n / nat_power n s)"
        by (simp add: dist_commute)
      also from 1 have " = norm (k{..n}-{..m}. fds_nth f k / nat_power k s)"
        by (subst Groups_Big.sum_diff) (simp_all add: dist_norm)
      also from 1 have "{..n} - {..m} = real -` {real m<..real n}" by auto
      also have "(k. fds_nth f k / nat_power k s) = 
                   (k. fds_nth f k / nat_power k s0 * real_power (real k) (s0 - s))"
        (is "_ = ?S") by (intro sum.cong refl) (simp_all add: nat_power_diff real_power_nat_power)
      also have *: "((λt. A t * ((s0 - s) * real_power t (s0 - s - 1))) has_integral
                    (A (real n) * real_power n (s0 - s) - A (real m) * real_power m (s0 - s) - ?S))
                    {real m..real n}" (is "(?h has_integral _) _") unfolding A_def using mn
        by (intro partial_summation_strong[of "{}"]) 
           (auto intro!: derivative_eq_intros continuous_intros)
      hence "?S = A (real n) * nat_power n (s0 - s) - A (real m) * nat_power m (s0 - s) -
                    integral {real m..real n} ?h"
        using mn by (simp add: has_integral_iff real_power_nat_power)
      also have "norm   norm (A (real n) * nat_power n (s0 - s)) +
                    norm (A (real m) * nat_power m (s0 - s)) + norm (integral {real m..real n} ?h)"
        by (intro order.trans[OF norm_triangle_ineq4] add_right_mono order.refl)
      also have "norm (A (real n) * nat_power n (s0 - s))  C * nat_power m ((s0 - s)  1)"
        using mn s  B C_pos s
        by (auto simp: norm_mult norm_nat_power algebra_simps intro!: mult_mono C powr_mono2')
      also have "norm (A (real m) * nat_power m (s0 - s))  C * nat_power m ((s0 - s)  1)"
        using mn by (auto simp: norm_mult norm_nat_power intro!: mult_mono C)
      also have "norm (integral {real m..real n} ?h)  
                   integral {real m..real n} (λt. C * (norm (s0 - s) * t powr ((s0 - s)  1 - 1)))"
      proof (intro integral_norm_bound_integral ballI, goal_cases)
        case 1
        with * show ?case by (simp add: has_integral_iff)
      next
        case 2
        from mn show ?case by (auto intro!: integrable_continuous_real continuous_intros)
      next
        case (3 t)
        thus ?case unfolding norm_mult using C_pos mn 
          by (intro mult_mono C) (auto simp: norm_real_power dot_square_norm algebra_simps)
      qed
      also have " = C * norm (s0 - s) * integral {real m..real n} (λt. t powr ((s0 - s)  1 - 1))"
        by (simp add: algebra_simps dot_square_norm)
      also {
        have "((λt. t powr ((s0 - s)  1 - 1)) has_integral 
                     (real n powr ((s0 - s)  1) / ((s0 - s)  1) - 
                      real m powr ((s0 - s)  1) / ((s0 - s)  1))) {m..n}" 
          (is "(?l has_integral ?I) _") using mn s
          by (intro fundamental_theorem_of_calculus)
             (auto intro!: derivative_eq_intros 
                   simp: has_real_derivative_iff_has_vector_derivative [symmetric] inner_diff_left)
        hence "integral {real m..real n} ?l = ?I" by (simp add: has_integral_iff)
        also have "  -(real m powr ((s0 - s)  1) / ((s0 - s)  1))" using s mn
          by (simp add: divide_simps inner_diff_left)
        also have " = 1 * (real m powr ((s0 - s)  1) / ((s - s0)  1))"
          using s by (simp add: field_simps inner_diff_left)
        also have "  2 * (real m powr ((s0 - s)  1) / ((s - s0)  1))" using mn s
          by (intro mult_right_mono divide_nonneg_pos) (simp_all add: inner_diff_left)
        finally have "integral {m..n} ?l  " .
      }
      hence "C * norm (s0 - s) * integral {real m..real n} (λt. t powr ((s0 - s)  1 - 1)) 
               C * norm (s0 - s) * (2 * (real m powr ((s0 - s)  1) / ((s - s0)  1)))" 
        using C_pos mn
        by (intro mult_mono mult_nonneg_nonneg integral_nonneg
              integrable_continuous_real continuous_intros) auto
      also have "C * nat_power m ((s0 - s)  1) + C * nat_power m ((s0 - s)  1) +  =
                   2 * C * nat_power m ((s0 - s)  1) * (1 + norm (s - s0) / ((s - s0)  1))"
        by (simp add: algebra_simps norm_minus_commute)
      also have "  2 * C * nat_power m (-δ) * (1 + norm_B / δ)" 
        using C_pos s mn σ_le[of s] s  B σ_gt 0  norm_B 
        unfolding nat_power_real_def δ_def
        by (intro mult_mono powr_mono frac_le add_mono norm_B; simp add: inner_diff_left)
      also have " = 2 * C * (1 + norm_B / δ) * real m powr (-δ)" by simp
      also from m  M have " < ε" by (rule M)
      finally show ?case by - simp_all
    qed
  qed
qed (auto simp: uniformly_Cauchy_on_def)

lemma uniformly_convergent_eval_fds_aux:
  assumes "Bseq (λn. kn. fds_nth f k / nat_power k (s0 :: 'a))"
  assumes B: "compact B" "z. z  B  z  1 > s0  1"
  shows   "uniformly_convergent_on B (λN z. nN. fds_nth f n / nat_power n z)"
  by (rule Cauchy_uniformly_convergent uniformly_Cauchy_eval_fds_aux assms)+

lemma uniformly_convergent_eval_fds_aux':
  assumes conv: "fds_converges f (s0 :: 'a)"
  assumes B: "compact B" "z. z  B  z  1 > s0  1"
  shows   "uniformly_convergent_on B (λN z. nN. fds_nth f n / nat_power n z)"
proof (rule uniformly_convergent_eval_fds_aux)
  from conv have "convergent (λn. kn. fds_nth f k / nat_power k s0)"
    by (simp add: fds_converges_def summable_iff_convergent')
  thus "Bseq (λn. kn. fds_nth f k / nat_power k s0)" by (rule convergent_imp_Bseq)
qed (insert assms, auto)

lemma bounded_partial_sums_imp_fps_converges:
  fixes s0 :: "'a :: dirichlet_series"
  assumes "Bseq (λn. kn. fds_nth f k / nat_power k s0)" and "s  1 > s0  1"
  shows   "fds_converges f s"
proof -
  have "uniformly_convergent_on {s} (λN z. nN. fds_nth f n / nat_power n z)" using assms(2)
    by (intro uniformly_convergent_eval_fds_aux[OF assms(1)]) auto
  thus ?thesis
    by (auto simp: fds_converges_def summable_iff_convergent'
             dest: uniformly_convergent_imp_convergent)
qed

theorem fds_converges_Re_le:
  assumes "fds_converges f (s0 :: 'a)" "s  1 > s0  1"
  shows   "fds_converges f s"
proof -
  have "uniformly_convergent_on {s} (λN z. nN. fds_nth f n / nat_power n z)"
    by (rule uniformly_convergent_eval_fds_aux' assms)+ (insert assms(2), auto)
  then obtain l where "uniform_limit {s} (λN z. nN. fds_nth f n / nat_power n z) l at_top"
    by (auto simp: uniformly_convergent_on_def)
  from tendsto_uniform_limitI[OF this, of s]
  have "(λn. fds_nth f n / nat_power n s) sums l s" unfolding sums_def'
    by (simp add: atLeast0AtMost)
  thus ?thesis by (simp add: fds_converges_def sums_iff)
qed

lemma fds_converges:
  assumes "s  1 > conv_abscissa (f :: 'a fds)"
  shows   "fds_converges f s"
proof -
  from assms obtain s0 where "fds_converges f s0" "s0  1 < s  1"
    by (auto simp: INF_less_iff conv_abscissa_def)
  with fds_converges_Re_le[OF this(1), of s] this(2) show ?thesis by simp
qed

lemma fds_diverges:
  assumes "s  1 < conv_abscissa (f :: 'a fds)"
  shows   "¬fds_converges f s"
proof
  assume "fds_converges f s"
  hence "conv_abscissa f  s  1" unfolding conv_abscissa_def
    by (intro INF_lower) auto
  with assms show False by simp
qed

theorem fds_converges_imp_abs_converges:
  assumes "fds_converges (f :: 'a fds) s" "s'  1 > s  1 + 1"
  shows   "fds_abs_converges f s'"
  unfolding fds_abs_converges_def
proof (rule summable_comparison_test_ev)
  from assms(2) show "summable (λn. real n powr ((s - s')  1))"
    by (subst summable_real_powr_iff) (simp_all add: inner_diff_left)
next
  from assms(1) have "(λn. fds_nth f n / nat_power n s)  0"
    unfolding fds_converges_def by (rule summable_LIMSEQ_zero)
  from tendsto_norm[OF this] have "(λn. norm (fds_nth f n / nat_power n s))  0" by simp
  hence "eventually (λn. norm (fds_nth f n / nat_power n s) < 1) at_top"
    by (rule order_tendstoD) simp_all
  thus "eventually (λn. norm (norm (fds_nth f n / nat_power n s'))  
          real n powr ((s - s')  1)) at_top"
  proof eventually_elim
    case (elim n)
    thus ?case
    proof (cases "n = 0")
      case False
      have "norm (fds_nth f n / nat_power n s') =
              norm (fds_nth f n) / real n powr (s'  1)" using False
        by (simp add: norm_divide norm_nat_power)
      also have " = norm (fds_nth f n / nat_power n s) / real n powr ((s' - s)  1)" using False
        by (simp add: norm_divide norm_nat_power inner_diff_left powr_diff)
      also have "  1 / real n powr ((s' - s)  1)" using elim
        by (intro divide_right_mono elim) simp_all
      also have " = real n powr ((s - s')  1)" using False
        by (simp add: field_simps inner_diff_left powr_diff) 
      finally show ?thesis by simp
    qed simp_all
  qed
qed

lemma conv_le_abs_conv_abscissa: "conv_abscissa f  abs_conv_abscissa f"
  unfolding conv_abscissa_def abs_conv_abscissa_def
  by (intro INF_superset_mono) auto

lemma conv_abscissa_PInf_iff: "conv_abscissa f =   (s. ¬fds_converges f s)"
  unfolding conv_abscissa_def by (subst Inf_eq_PInfty) auto

lemma conv_abscissa_PInfI [intro]: "(s. ¬fds_converges f s)  conv_abscissa f = "
  by (subst conv_abscissa_PInf_iff) auto
    
lemma conv_abscissa_MInf_iff: "conv_abscissa (f :: 'a fds) = -  (s. fds_converges f s)"
proof safe
  assume *: "s. fds_converges f s"
  have "conv_abscissa f  B" for B :: real
    using spec[OF *, of "of_real B"] fds_diverges[of "of_real B" f]
    by (cases "conv_abscissa f  B") simp_all
  thus "conv_abscissa f = -" by (rule ereal_bot)    
qed (auto intro: fds_converges)

lemma conv_abscissa_MInfI [intro]: "(s. fds_converges (f::'a fds) s)  conv_abscissa f = -"
  by (subst conv_abscissa_MInf_iff) auto

lemma abs_conv_abscissa_PInf_iff: "abs_conv_abscissa f =   (s. ¬fds_abs_converges f s)"
  unfolding abs_conv_abscissa_def by (subst Inf_eq_PInfty) auto

lemma abs_conv_abscissa_PInfI [intro]: "(s. ¬fds_converges f s)  abs_conv_abscissa f = "
  by (subst abs_conv_abscissa_PInf_iff) auto

lemma abs_conv_abscissa_MInf_iff: 
  "abs_conv_abscissa (f :: 'a fds) = -  (s. fds_abs_converges f s)"
proof safe
  assume *: "s. fds_abs_converges f s"
  have "abs_conv_abscissa f  B" for B :: real
    using spec[OF *, of "of_real B"] fds_abs_diverges[of "of_real B" f]
    by (cases "abs_conv_abscissa f  B") simp_all
  thus "abs_conv_abscissa f = -" by (rule ereal_bot)    
qed (auto intro: fds_abs_converges)

lemma abs_conv_abscissa_MInfI [intro]: 
  "(s. fds_abs_converges (f::'a fds) s)  abs_conv_abscissa f = -"
  by (subst abs_conv_abscissa_MInf_iff) auto

lemma conv_abscissa_geI:
  assumes "c'. ereal c' < c  s. s  1 = c'  ¬fds_converges f s"
  shows   "conv_abscissa (f :: 'a fds)  c"
proof (rule ccontr)
  assume "¬conv_abscissa f  c"
  hence "c > conv_abscissa f" by simp
  from ereal_dense2[OF this] obtain c' where "c > ereal c'" "c' > conv_abscissa f" by auto
  moreover from assms[OF this(1)] obtain s where "s  1 = c'" "¬fds_converges f s" by blast
  ultimately show False using fds_converges[of f s] by auto
qed

lemma conv_abscissa_leI:
  assumes "c'. ereal c' > c  s. s  1 = c'  fds_converges f s"
  shows   "conv_abscissa (f :: 'a fds)  c"
proof (rule ccontr)
  assume "¬conv_abscissa f  c"
  hence "c < conv_abscissa f" by simp
  from ereal_dense2[OF this] obtain c' where "c < ereal c'" "c' < conv_abscissa f" by auto
  moreover from assms[OF this(1)] obtain s where "s  1 = c'" "fds_converges f s" by blast
  ultimately show False using fds_diverges[of s f] by auto
qed

lemma abs_conv_abscissa_geI:
  assumes "c'. ereal c' < c  s. s  1 = c'  ¬fds_abs_converges f s"
  shows   "abs_conv_abscissa (f :: 'a fds)  c"
proof (rule ccontr)
  assume "¬abs_conv_abscissa f  c"
  hence "c > abs_conv_abscissa f" by simp
  from ereal_dense2[OF this] obtain c' where "c > ereal c'" "c' > abs_conv_abscissa f" by auto
  moreover from assms[OF this(1)] obtain s where "s  1 = c'" "¬fds_abs_converges f s" by blast
  ultimately show False using fds_abs_converges[of f s] by auto
qed  

lemma abs_conv_abscissa_leI:
  assumes "c'. ereal c' > c  s. s  1 = c'  fds_abs_converges f s"
  shows   "abs_conv_abscissa (f :: 'a fds)  c"
proof (rule ccontr)
  assume "¬abs_conv_abscissa f  c"
  hence "c < abs_conv_abscissa f" by simp
  from ereal_dense2[OF this] obtain c' where "c < ereal c'" "c' < abs_conv_abscissa f" by auto
  moreover from assms[OF this(1)] obtain s where "s  1 = c'" "fds_abs_converges f s" by blast
  ultimately show False using fds_abs_diverges[of s f] by auto
qed

lemma conv_abscissa_leI_weak:
  assumes "x. ereal x > d  fds_converges f (of_real x)"
  shows   "conv_abscissa (f :: 'a fds)  d"
proof (rule conv_abscissa_leI)
  fix x assume "d < ereal x"
  from assms[OF this] show "s. s  1 = x  fds_converges f s"
    by (intro exI[of _ "of_real x"]) auto
qed

lemma abs_conv_abscissa_leI_weak:
  assumes "x. ereal x > d  fds_abs_converges f (of_real x)"
  shows   "abs_conv_abscissa (f :: 'a fds)  d"
proof (rule abs_conv_abscissa_leI)
  fix x assume "d < ereal x"
  from assms[OF this] show "s. s  1 = x  fds_abs_converges f s"
    by (intro exI[of _ "of_real x"]) auto
qed

lemma conv_abscissa_truncate [simp]: 
  "conv_abscissa (fds_truncate m (f :: 'a fds)) = -"
  by (auto simp: conv_abscissa_MInf_iff)

lemma abs_conv_abscissa_truncate [simp]: 
  "abs_conv_abscissa (fds_truncate m (f :: 'a fds)) = -"
  by (auto simp: abs_conv_abscissa_MInf_iff)

  
theorem abs_conv_le_conv_abscissa_plus_1: "abs_conv_abscissa (f :: 'a fds)  conv_abscissa f + 1"
proof (rule abs_conv_abscissa_leI)
  fix c assume less: "conv_abscissa f + 1 < ereal c"
  define c' where "c' = (if conv_abscissa f = - then c - 2
                     else (c - 1 + real_of_ereal (conv_abscissa f)) / 2)"
  from less have c': "conv_abscissa f < ereal c'  c' < c - 1"
    by (cases "conv_abscissa f") (simp_all add: c'_def field_simps)
  
  from c' have "fds_converges f (of_real c')" 
    by (intro fds_converges) (simp_all add: inner_diff_left dot_square_norm)
  hence "fds_abs_converges f (of_real c)"
    by (rule fds_converges_imp_abs_converges) (insert c', simp_all)
  thus "s. s  1 = c  fds_abs_converges f s"
    by (intro exI[of _ "of_real c"]) auto
qed

  
lemma uniformly_convergent_eval_fds:
  assumes B: "compact B" "z. z  B  z  1 > conv_abscissa (f :: 'a fds)"
  shows   "uniformly_convergent_on B (λN z. nN. fds_nth f n / nat_power n z)"
proof (cases "B = {}")
  case False
  define σ where "σ = Inf ((λs. s  1) ` B)"
  have σ_le: "s  1  σ" if "s  B" for s
    unfolding σ_def using that 
    by (intro cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded B) auto
  have "σ  ((λs. s  1) ` B)"
    unfolding σ_def using B B  {}
    by (intro closed_contains_Inf bounded_inner_imp_bdd_below compact_imp_bounded B 
          compact_imp_closed compact_continuous_image continuous_intros) auto
  with B(2) have σ_gt: "σ > conv_abscissa f" by auto
  define s where "s = (if conv_abscissa f = - then σ - 1 else 
                         (σ + real_of_ereal (conv_abscissa f)) / 2)"
  from σ_gt have s: "conv_abscissa f < s  s < σ"
    by (cases "conv_abscissa f") (auto simp: s_def)
  show ?thesis using s compact B
    by (intro uniformly_convergent_eval_fds_aux'[of f "of_real s"] fds_converges)
       (auto dest: σ_le)
qed auto
    
corollary uniformly_convergent_eval_fds':
  assumes B: "compact B" "z. z  B  z  1 > conv_abscissa (f :: 'a fds)"
  shows   "uniformly_convergent_on B (λN z. n<N. fds_nth f n / nat_power n z)"
proof -
  from uniformly_convergent_eval_fds[OF assms] obtain l where
    "uniform_limit B (λN z. nN. fds_nth f n / nat_power n z) l at_top" 
    by (auto simp: uniformly_convergent_on_def)
  also have "(λN z. nN. fds_nth f n / nat_power n z) = 
                (λN z. n<Suc N. fds_nth f n / nat_power n z)"
    by (simp only: lessThan_Suc_atMost)
  finally have "uniform_limit B (λN z. n<N. fds_nth f n / nat_power n z) l at_top" 
    unfolding uniform_limit_iff by (subst (asm) eventually_sequentially_Suc)
  thus ?thesis by (auto simp: uniformly_convergent_on_def)
qed


subsection ‹Derivative of a Dirichlet series›

lemma fds_converges_deriv_aux:
  assumes conv: "fds_converges f (s0 :: 'a)" and gt: "s  1 > s0  1"
  shows "fds_converges (fds_deriv f) s"
proof -
  have "Cauchy (λn. kn. (-ln (real k) *R fds_nth f k) / nat_power k s)"
  proof (rule CauchyI', goal_cases)
    case (1 ε)
    define δ where "δ = s  1 - s0  1"
    define δ' where "δ' = δ / 2"
    from gt have δ_pos: "δ > 0" by (simp add: δ_def)
    define A where "A = sum_upto (λk. fds_nth f k / nat_power k s0)"
    from conv have "convergent (λn. kn. fds_nth f k / nat_power k s0)"
      by (simp add: fds_converges_def summable_iff_convergent')
    hence "Bseq (λn. kn. fds_nth f k / nat_power k s0)" by (rule convergent_imp_Bseq)
    then obtain C_aux where C_aux: "n. norm (kn. fds_nth f k / nat_power k s0)  C_aux"
      by (auto simp: Bseq_def)
    define C where "C = max C_aux 1"
    have C_pos: "C > 0" by (simp add: C_def)
    have C: "norm (A x)  C" for x
    proof -
      have "A x = (knat x. fds_nth f k / nat_power k s0)"
        unfolding A_def sum_upto_altdef by (intro sum.mono_neutral_left) auto
      also have "norm   C_aux" by (rule C_aux)
      also have "  C" by (simp add: C_def)
      finally show ?thesis .
    qed
    define C' where "C' = 2 * C + C * (norm (s0 - s) * (1 + 1 / δ) + 1) / δ"
  
    have "(λm. C' * real m powr (-δ'))  0" unfolding δ'_def using gt δ_pos
      by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially) simp_all
    from order_tendstoD(2)[OF this ε > 0] obtain M1 where
      M1: "m. m  M1  C' * real m powr - δ' < ε" 
      by (auto simp: eventually_at_top_linorder)
    have "((λx. ln (real x) / real x powr δ')  0) at_top" using δ_pos
      by (intro lim_ln_over_power) (simp_all add: δ'_def)
    from order_tendstoD(2)[OF this zero_less_one] eventually_gt_at_top[of "1::nat"]
      have "eventually (λn. ln (real n)  n powr δ') at_top" by eventually_elim simp_all
    then obtain M2 where M2: "n. n  M2  ln (real n)  n powr δ'"
      by (auto simp: eventually_at_top_linorder)
    let ?f' = "λk. -ln (real k) *R fds_nth f k"

    show ?case
    proof (intro exI[of _ "max (max M1 M2) 1"] allI impI, goal_cases)
      case (1 m n)
      hence mn: "m  M1" "m  M2" "m > 0" "m < n" by simp_all
      define g :: "real  'a" where "g = (λt. real_power t (s0 - s) * of_real (ln t))"
      define g' :: "real  'a"            
        where "g' = (λt. real_power t (s0 - s - 1) * ((s0 - s) * of_real (ln t) + 1))"
      define norm_g' :: "real  real"
        where "norm_g' = (λt. t powr (-δ - 1) * (norm (s0 - s) * ln t + 1))"
      define norm_g :: "real  real"
        where "norm_g = (λt. -(t powr -δ) * (norm (s0 - s) * (δ * ln t + 1) + δ) / δ^2)"
      have g_g': "(g has_vector_derivative g' t) (at t)" if "t  {real m..real n}" for t 
        using mn that by (auto simp: g_def g'_def real_power_diff field_simps real_power_add 
                               intro!: derivative_eq_intros)
      have [continuous_intros]: "continuous_on {real m..real n} g" using mn
        by (auto simp: g_def intro!: continuous_intros)
        
      let ?S = "kreal -` {real m<..real n}. fds_nth f k / nat_power k s0 * g k"
      have "dist (km. ?f' k / nat_power k s) (kn. ?f' k / nat_power k s) =
              norm (k{..n} - {..m}. fds_nth f k / nat_power k s * of_real (ln (real k)))" 
        using mn by (subst sum_diff) 
           (simp_all add: dist_norm norm_minus_commute sum_negf scaleR_conv_of_real mult_ac)
      also have "{..n} - {..m} = real -` {real m<..real n}" by auto
      also have "(k. fds_nth f k / nat_power k s * of_real (ln (real k))) = 
        (k. fds_nth f k / nat_power k s0 * g k)" using mn unfolding g_def
        by (intro sum.cong refl) (auto simp: real_power_nat_power field_simps nat_power_diff)
      also have *: "((λt. A t * g' t) has_integral
                    (A (real n) * g n - A (real m) * g m - ?S))
                    {real m..real n}" (is "(?h has_integral _) _") unfolding A_def using mn
        by (intro partial_summation_strong[of "{}"])
           (auto intro!: g_g' simp: field_simps continuous_intros)
      hence "?S = A (real n) * g n - A (real m) * g m - integral {real m..real n} ?h"
        using mn by (simp add: has_integral_iff field_simps)
      also have "norm   norm (A (real n) * g n) + norm (A (real m) * g m) + 
                             norm (integral {real m..real n} ?h)"
        by (intro order.trans[OF norm_triangle_ineq4] add_right_mono order.refl)
      also have "norm (A (real n) * g n)  C * norm (g n)"
        unfolding norm_mult using mn C_pos by (intro mult_mono C) auto
      also have "norm (g n)  n powr -δ * n powr δ'" using mn M2[of n]
        by (simp add: g_def norm_real_power norm_mult δ_def inner_diff_left)
      also have " = n powr -δ'" using mn 
        by (simp add: δ'_def powr_minus field_simps powr_add [symmetric])
      also have "norm (A (real m) * g m)  C * norm (g m)"
        unfolding norm_mult using mn C_pos by (intro mult_mono C) auto
      also have "norm (g m)  m powr -δ * m powr δ'" using mn M2[of m]
        by (simp add: g_def norm_real_power norm_mult δ_def inner_diff_left)
      also have " = m powr -δ'" using mn 
        by (simp add: δ'_def powr_minus field_simps powr_add [symmetric])
      also have "C * real n powr - δ'  C * real m powr - δ'" using δ_pos mn C_pos
        by (intro mult_left_mono powr_mono2') (simp_all add: δ'_def)
      also have " +  = 2 * " by simp
      also have "norm (integral {m..n} ?h)  integral {m..n} (λt. C * norm_g' t)"
      proof (intro integral_norm_bound_integral ballI, goal_cases)
        case 1
        with * show ?case by (simp add: has_integral_iff)
      next
        case 2
        from mn show ?case 
          by (auto intro!: integrable_continuous_real continuous_intros simp: norm_g'_def)
      next
        case (3 t)
        have "norm (g' t)  norm_g' t" unfolding g'_def norm_g'_def using 3 mn
          unfolding norm_mult
          by (intro mult_mono order.trans[OF norm_triangle_ineq])
             (auto simp: norm_real_power inner_diff_left dot_square_norm norm_mult δ_def
                   intro!: mult_left_mono)
        thus ?case unfolding norm_mult using C_pos mn 
          by (intro mult_mono C) simp_all
      qed
      also have " = C * integral {m..n} norm_g'"
        unfolding norm_g'_def by (simp add: norm_g'_def δ_def inner_diff_left)
      also {
        have "(norm_g' has_integral (norm_g n - norm_g m)) {m..n}"
          unfolding norm_g'_def norm_g_def power2_eq_square using mn δ_pos
          by (intro fundamental_theorem_of_calculus)
             (auto simp: has_real_derivative_iff_has_vector_derivative [symmetric] 
                 field_simps powr_diff intro!: derivative_eq_intros)
        hence "integral {m..n} norm_g' = norm_g n - norm_g m" by (simp add: has_integral_iff)
        also have "norm_g n  0" unfolding norm_g_def using δ_pos mn
          by (intro divide_nonpos_pos mult_nonpos_nonneg add_nonneg_nonneg mult_nonneg_nonneg)
             simp_all
        hence "norm_g n - norm_g m  -norm_g m" by simp
        also have " = real m powr -δ * ln (real m) * (norm (s0 - s)) / δ +
                        real m powr -δ * ((norm (s0 - s) / δ + 1) / δ)" using δ_pos
          by (simp add: field_simps norm_g_def power2_eq_square)
        also {
          have "ln (real m)  real m powr δ'" using M2[of m] mn by simp
          also have "real m powr -δ *  = real m powr -δ'"
            by (simp add: powr_add [symmetric] δ'_def)
          finally have "real m powr -δ * ln (real m) * (norm (s0 - s)) / δ 
                           * (norm (s0 - s)) / δ" using δ_pos
            by (intro divide_right_mono mult_right_mono) (simp_all add: mult_left_mono)
        }
        also have "real m powr -δ * ((norm (s0 - s) / δ + 1) / δ) 
                     real m powr -δ' * ((norm (s0 - s) / δ + 1) / δ)" using mn δ_pos
          by (intro mult_right_mono powr_mono) (simp_all add: δ'_def)
        also have "real m powr - δ' * norm (s0 - s) / δ +  =
                     real m powr -δ' * (norm (s0 - s) * (1 + 1 / δ) + 1) / δ" using δ_pos
          by (simp add: field_simps power2_eq_square)
        finally have "integral {real m..real n} norm_g' 
                        real m powr - δ' * (norm (s0 - s) * (1 + 1 / δ) + 1) / δ" by - simp_all
      }
      also have "2 * (C * m powr - δ') + C * (m powr - δ' * (norm (s0 - s) * (1 + 1 / δ) + 1) / δ) =
                   C' * m powr -δ'" by (simp add: algebra_simps C'_def)
      also have " < ε" using M1[of m] mn by simp
      finally show ?case using C_pos by - simp_all
    qed
  qed
  from Cauchy_convergent[OF this] 
    show ?thesis by (simp add: summable_iff_convergent' fds_converges_def fds_nth_deriv)
qed

theorem
  assumes "s  1 > conv_abscissa (f :: 'a fds)"
  shows   fds_converges_deriv: "fds_converges (fds_deriv f) s"
    and   has_field_derivative_eval_fds [derivative_intros]:
            "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s within A)"
proof -
  define s1 :: real where
    "s1 = (if conv_abscissa f = - then s  1 - 2 else
             (s  1 * 1 / 3 + real_of_ereal (conv_abscissa f) * 2 / 3))"
  define s2 :: real where
    "s2 = (if conv_abscissa f = - then s  1 - 1 else
             (s  1 * 2 / 3 + real_of_ereal (conv_abscissa f) * 1 / 3))"
  from assms have s: "conv_abscissa f < s1  s1 < s2  s2 < s  1"
    by (cases "conv_abscissa f") (auto simp: s1_def s2_def field_simps)
  from s have *: "fds_converges f (of_real s1)" by (intro fds_converges) simp_all
  thus conv': "fds_converges (fds_deriv f) s"
    by (rule fds_converges_deriv_aux) (insert s, simp_all)
  from * have conv: "fds_converges (fds_deriv f) (of_real s2)"
    by (rule fds_converges_deriv_aux) (insert s, simp_all)
      
  define δ :: real where "δ = (s  1 - s2) / 2"
  from s have δ_pos: "δ > 0" by (simp add: δ_def)
  
  have "uniformly_convergent_on (cball s δ) 
          (λn s. kn. fds_nth (fds_deriv f) k / nat_power k s)"
  proof (intro uniformly_convergent_eval_fds_aux'[OF conv])
    fix s'' :: 'a assume s'': "s''  cball s δ"
    have "dist (s  1) (s''  1)  dist s s''" 
      by (intro Euclidean_dist_upper) (simp_all add: one_in_Basis)
    also from s'' have "  δ" by simp
    finally show "s''  1 > (of_real s2 :: 'a)  1" using s
      by (auto simp: δ_def dist_real_def abs_if split: if_splits)
  qed (insert δ_pos, auto)
  then obtain l where 
     "uniform_limit (cball s δ) (λn s. kn. fds_nth (fds_deriv f) k / nat_power k s) l at_top"
    by (auto simp: uniformly_convergent_on_def)
  also have "(λn s. kn. fds_nth (fds_deriv f) k / nat_power k s) =
               (λn s. k<Suc n. fds_nth (fds_deriv f) k / nat_power k s)"
    by (simp only: lessThan_Suc_atMost)
  finally have "uniform_limit (cball s δ) (λn s. k<n. fds_nth (fds_deriv f) k / nat_power k s) 
                  l at_top"
    unfolding uniform_limit_iff by (subst (asm) eventually_sequentially_Suc)
  hence *: "uniformly_convergent_on (cball s δ) 
              (λn s. k<n. fds_nth (fds_deriv f) k / nat_power k s)"
    unfolding uniformly_convergent_on_def by blast
      
  have "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s)"
    unfolding eval_fds_def
  proof (rule has_field_derivative_series'(2)[OF _ _ *])
    show "s  cball s δ" "s  interior (cball s δ)" using s by (simp_all add: δ_def)
    show "summable (λn. fds_nth f n / nat_power n s)"
      using assms fds_converges[of f s] by (simp add: fds_converges_def)
  next
    fix s' :: 'a and n :: nat
    show "((λs. fds_nth f n / nat_power n s) has_field_derivative
            fds_nth (fds_deriv f) n / nat_power n s') (at s' within cball s δ)"
      by (cases "n = 0") 
         (simp, auto intro!: derivative_eq_intros simp: fds_nth_deriv field_simps)
  qed (auto simp: fds_nth_deriv intro!: derivative_eq_intros)
  thus "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s within A)"
    by (rule has_field_derivative_at_within)
qed

lemmas has_field_derivative_eval_fds' [derivative_intros] = 
  DERIV_chain2[OF has_field_derivative_eval_fds]

lemma continuous_eval_fds [continuous_intros]:
  assumes "s  1 > conv_abscissa f"
  shows   "continuous (at s within A) (eval_fds (f :: 'a :: dirichlet_series fds))"
proof -
  have "isCont (eval_fds f) s"
    by (rule has_field_derivative_eval_fds DERIV_isCont assms)+
  thus ?thesis by (rule continuous_within_subset) auto
qed

lemma continuous_eval_fds' [continuous_intros]:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "continuous (at s within A) g" "g s  1 > conv_abscissa f"
  shows   "continuous (at s within A) (λx. eval_fds f (g x))"
  by (rule continuous_within_compose3[OF _ assms(1)] continuous_intros assms)+

lemma continuous_on_eval_fds [continuous_intros]:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "A  {s. s  1 > conv_abscissa f}"
  shows   "continuous_on A (eval_fds f)"
  by (rule DERIV_continuous_on derivative_intros)+ (insert assms, auto)

lemma continuous_on_eval_fds' [continuous_intros]:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "continuous_on A g" "g ` A  {s. s  1 > conv_abscissa f}"
  shows   "continuous_on A (λx. eval_fds f (g x))"
  by (rule continuous_on_compose2[OF continuous_on_eval_fds assms(1)])
     (insert assms, auto simp: image_iff)

lemma conv_abscissa_deriv_le:
  fixes f :: "'a fds"
  shows "conv_abscissa (fds_deriv f)  conv_abscissa f"
proof (rule conv_abscissa_leI)
  fix c' :: real
  assume "ereal c' > conv_abscissa f"
  thus "s. s  1 = c'  fds_converges (fds_deriv f) s"
    by (intro exI[of _ "of_real c'"]) (auto simp: fds_converges_deriv)
qed

lemma abs_conv_abscissa_integral:
  fixes f :: "'a fds"
  shows "abs_conv_abscissa (fds_integral a f) = abs_conv_abscissa f"
proof (rule antisym)
  show "abs_conv_abscissa (fds_integral a f)  abs_conv_abscissa f"
  proof (rule abs_conv_abscissa_leI, goal_cases)
    case (1 c)
    have "fds_abs_converges (fds_integral a f) (of_real c)"
      unfolding fds_abs_converges_def
    proof (rule summable_comparison_test_ev)
      from 1 have "fds_abs_converges f (of_real c)"
        by (intro fds_abs_converges) auto
      thus "summable (λn. norm (fds_nth f n / nat_power n (of_real c)))"
        by (simp add: fds_abs_converges_def)
    next
      show "F n in sequentially. norm (norm (fds_nth (fds_integral a f) n / nat_power n (of_real c)))  
              norm (fds_nth f n / nat_power n (of_real c))"
        using eventually_gt_at_top[of 3]
      proof eventually_elim
        case (elim n)
        from elim and exp_le have "ln (exp 1)  ln (real n)"
          by (subst ln_le_cancel_iff) auto
        hence "1 * norm (fds_nth f n)  ln (real n) * norm (fds_nth f n)"
          by (intro mult_right_mono) auto
        with elim show ?case
          by (simp add: norm_divide norm_nat_power fds_integral_def field_simps)
      qed
    qed
    thus ?case by (intro exI[of _ "of_real c"]) auto
  qed
next
  show "abs_conv_abscissa f  abs_conv_abscissa (fds_integral a f)" (is "_  ?s0")
  proof (cases "abs_conv_abscissa (fds_integral a f) = ")
    case False
    show ?thesis
    proof (rule abs_conv_abscissa_leI)
      fix c :: real
      define ε where "ε = (if ?s0 = - then 1 else (c - real_of_ereal ?s0) / 2)"
      assume "ereal c > ?s0"
      with False have ε: "ε > 0" "c - ε > ?s0"
        by (cases ?s0; force simp: ε_def field_simps)+
  
      have "fds_abs_converges f (of_real c)"
        unfolding fds_abs_converges_def
      proof (rule summable_comparison_test_ev)
        from ε have "fds_abs_converges (fds_integral a f) (of_real (c - ε))"
          by (intro fds_abs_converges) (auto simp: algebra_simps)
        thus "summable (λn. norm (fds_nth (fds_integral a f) n / nat_power n (of_real (c - ε))))"
          by (simp add: fds_abs_converges_def)
      next
        have "F n in at_top. ln (real n) / real n powr ε < 1"
          by (rule order_tendstoD lim_ln_over_power ε > 0 zero_less_one)+
        thus "F n in sequentially. norm (norm (fds_nth f n / nat_power n (of_real c)))
                 norm (fds_nth (fds_integral a f) n / nat_power n (of_real (c - ε)))"
          using eventually_gt_at_top[of 1]
        proof eventually_elim
          case (elim n)
          hence "ln (real n) * norm (fds_nth f n)  real n powr ε * norm (fds_nth f n)"
            by (intro mult_right_mono) auto
          with elim show ?case
            by (simp add: norm_divide norm_nat_power field_simps 
                          powr_diff inner_diff_left fds_integral_def)
        qed
      qed
      thus "s. s  1 = c  fds_abs_converges f s"
        by (intro exI[of _ "of_real c"]) auto
    qed
  qed auto
qed

lemma abs_conv_abscissa_ln: 
  "abs_conv_abscissa (fds_ln l (f :: 'a :: dirichlet_series fds)) = 
     abs_conv_abscissa (fds_deriv f / f)"
  by (simp add: fds_ln_def abs_conv_abscissa_integral)

lemma abs_conv_abscissa_deriv:
  fixes f :: "'a fds"
  shows "abs_conv_abscissa (fds_deriv f) = abs_conv_abscissa f"
proof -
  have "abs_conv_abscissa (fds_deriv f) = 
          abs_conv_abscissa (fds_integral (fds_nth f 1) (fds_deriv f))"
    by (rule abs_conv_abscissa_integral [symmetric])
  also have "fds_integral (fds_nth f 1) (fds_deriv f) = f"
    by (rule fds_integral_fds_deriv)
  finally show ?thesis .
qed

lemma abs_conv_abscissa_higher_deriv:
  "abs_conv_abscissa ((fds_deriv ^^ n) f) = abs_conv_abscissa (f :: 'a :: dirichlet_series fds)"
  by (induction n) (simp_all add: abs_conv_abscissa_deriv)

lemma conv_abscissa_higher_deriv_le:
  "conv_abscissa ((fds_deriv ^^ n) f)  conv_abscissa (f :: 'a :: dirichlet_series fds)"
  by (induction n) (auto intro: order.trans[OF conv_abscissa_deriv_le])

lemma abs_conv_abscissa_restrict:
  "abs_conv_abscissa (fds_subseries P f)  abs_conv_abscissa f"
  by (rule abs_conv_abscissa_mono) auto

lemma eval_fds_deriv:
  fixes f :: "'a fds"
  assumes "s  1 > conv_abscissa f"
  shows   "eval_fds (fds_deriv f) s = deriv (eval_fds f) s"
  by (intro DERIV_imp_deriv [symmetric] derivative_intros assms)

lemma eval_fds_higher_deriv:
  assumes "(s :: 'a :: dirichlet_series)  1 > conv_abscissa f"
  shows   "eval_fds ((fds_deriv ^^ n) f) s = (deriv ^^ n) (eval_fds f) s"
  using assms
proof (induction n arbitrary: f s)
  case (Suc n f s)
  have ev: "eventually (λs. s  {s. s  1 > conv_abscissa f}) (nhds s)"
    using Suc.prems open_halfspace_gt[of _ "1::'a"]
    by (intro eventually_nhds_in_open, cases "conv_abscissa f")
       (auto simp: open_halfspace_gt inner_commute)
  have "eval_fds ((fds_deriv ^^ Suc n) f) s = eval_fds ((fds_deriv ^^ n) (fds_deriv f)) s"
    by (subst funpow_Suc_right) simp
  also have " = (deriv ^^ n) (eval_fds (fds_deriv f)) s"
    by (intro Suc.IH le_less_trans[OF conv_abscissa_deriv_le] Suc.prems)
  also have " = (deriv ^^ n) (deriv (eval_fds f)) s"
    by (intro higher_deriv_cong_ev refl eventually_mono[OF ev] eval_fds_deriv) auto
  also have " = (deriv ^^ Suc n) (eval_fds f) s"
    by (subst funpow_Suc_right) simp
  finally show ?case .
qed auto

end


subsection ‹Multiplication of two series›

lemma 
  fixes f g :: "nat  'a :: {banach, real_normed_field, second_countable_topology, nat_power}"
  fixes s :: 'a
  assumes [simp]: "f 0 = 0" "g 0 = 0"
  assumes summable: "summable (λn. norm (f n / nat_power n s))"
                    "summable (λn. norm (g n / nat_power n s))"
  shows   summable_dirichlet_prod: "summable (λn. norm (dirichlet_prod f g n / nat_power n s))"
    and   suminf_dirichlet_prod:
            "(n. dirichlet_prod f g n / nat_power n s) = 
               (n. f n / nat_power n s) * (n. g n / nat_power n s)"
proof -
  have summable': "(λn. f n / nat_power n s) abs_summable_on A"
                  "(λn. g n / nat_power n s) abs_summable_on A" for A
    by ((rule abs_summable_on_subset[OF _ subset_UNIV], insert summable, 
        simp add: abs_summable_on_nat_iff'); fail)+
  have f_g: "f a / nat_power a s * (g b / nat_power b s) =
              f a * g b / nat_power (a * b) s" for a b
    by (cases "a * b = 0") (auto simp: nat_power_mult_distrib)

  have eq: "(a(m, n){(m, n). m * n = x}. f m * g n / nat_power x s) =
              dirichlet_prod f g x / nat_power x s" for x :: nat
  proof (cases "x > 0")
    case False
    hence "(a(m,n) | m * n = x. f m * g n / nat_power x s) = (a(m,n) | m * n = x. 0)"
      by (intro infsetsum_cong) auto
    with False show ?thesis by simp
  next
    case True
    from finite_divisors_nat'[OF this] show ?thesis 
      by (simp add: dirichlet_prod_altdef2 case_prod_unfold sum_divide_distrib)
  qed

  have "(λ(m,n). (f m / nat_power m s) * (g n / nat_power n s)) abs_summable_on UNIV × UNIV"
    using summable' by (intro abs_summable_on_product) auto
  also have "?this  (λ(m,n). f m * g n / nat_power (m*n) s) abs_summable_on UNIV"
    using f_g by (intro abs_summable_on_cong) auto
  also have "  (λ(x,(m,n)). f m * g n / nat_power (m*n) s) abs_summable_on 
                           (SIGMA x:UNIV. {(m,n). m * n = x})"
    unfolding case_prod_unfold
    by (rule abs_summable_on_reindex_bij_betw [symmetric]) 
       (auto simp: bij_betw_def inj_on_def image_iff)
  also have "  (λ(x,(m,n)). f m * g n / nat_power x s) abs_summable_on 
                           (SIGMA x:UNIV. {(m,n). m * n = x})"
    by (intro abs_summable_on_cong) auto
  finally have summable'':  .
  from abs_summable_on_Sigma_project1'[OF this]
    show summable''': "summable (λn. norm (dirichlet_prod f g n / nat_power n s))"
    by (simp add: eq abs_summable_on_nat_iff')

  have "(n. f n / nat_power n s) * (n. g n / nat_power n s) =
          (an. f n / nat_power n s) * (an. g n / nat_power n s)"
    using summable' by (simp add: infsetsum_nat')
  also have " = (a(m,n). (f m / nat_power m s) * (g n / nat_power n s))"
    using summable' by (subst infsetsum_product [symmetric]) simp_all
  also have " = (a(m,n). f m * g n / nat_power (m * n) s)"
    using f_g by (intro infsetsum_cong refl) auto
  also have " = (a(x,(m,n))(SIGMA x:UNIV. {(m,n). m * n = x}). 
                      f m * g n / nat_power (m * n) s)" 
    unfolding case_prod_unfold
    by (rule infsetsum_reindex_bij_betw [symmetric]) (auto simp: bij_betw_def inj_on_def image_iff)
  also have " = (a(x,(m,n))(SIGMA x:UNIV. {(m,n). m * n = x}). 
                      f m * g n / nat_power x s)"
    by (intro infsetsum_cong refl) (auto simp: case_prod_unfold)
  also have " = (ax. dirichlet_prod f g x / nat_power x s)"
    (is "_ = infsetsum ?T _") using summable'' by (subst infsetsum_Sigma) (auto simp: eq)
  also have " = (x. dirichlet_prod f g x / nat_power x s)"
    using summable''' by (intro infsetsum_nat') (simp_all add: abs_summable_on_nat_iff')
  finally show " = (n. f n / nat_power n s) * (n. g n / nat_power n s)" ..
qed

lemma 
  fixes f g :: "nat  real"
  fixes s :: real
  assumes "f 0 = 0" "g 0 = 0"
  assumes summable: "summable (λn. norm (f n / real n powr s))"
                    "summable (λn. norm (g n / real n powr s))"
  shows   summable_dirichlet_prod_real: "summable (λn. norm (dirichlet_prod f g n / real n powr s))"
    and   suminf_dirichlet_prod_real:
            "(n. dirichlet_prod f g n / real n powr s) = 
               (n. f n / nat_power n s) * (n. g n / real n powr s)"
  using summable_dirichlet_prod[of f g s] suminf_dirichlet_prod[of f g s] assms by simp_all

lemma fds_abs_converges_mult: 
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  assumes "fds_abs_converges f s" "fds_abs_converges g s"
  shows   "fds_abs_converges (f * g) s"
  using summable_dirichlet_prod[OF _ _ assms[unfolded fds_abs_converges_def]]
  by (simp add: fds_abs_converges_def fds_nth_mult)

lemma fds_abs_converges_power: 
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  shows "fds_abs_converges f s  fds_abs_converges (f ^ n) s"
  by (induction n) (auto intro!: fds_abs_converges_mult)

lemma fds_abs_converges_prod: 
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  shows "(x. x  A  fds_abs_converges (f x) s)  fds_abs_converges (prod f A) s"
  by (induction A rule: infinite_finite_induct) (auto intro!: fds_abs_converges_mult)

lemma abs_conv_abscissa_mult_le:
  "abs_conv_abscissa (f * g :: 'a :: dirichlet_series fds)  
      max (abs_conv_abscissa f) (abs_conv_abscissa g)"
proof (rule abs_conv_abscissa_leI, goal_cases)
  case (1 c')
  thus ?case
    by (auto intro!: exI[of _ "of_real c'"] fds_abs_converges_mult intro: fds_abs_converges)
qed

lemma abs_conv_abscissa_mult_leI:
  "abs_conv_abscissa (f :: 'a :: dirichlet_series fds)  d 
   abs_conv_abscissa g  d  abs_conv_abscissa (f * g)  d"
  using abs_conv_abscissa_mult_le[of f g] by (auto simp add: le_max_iff_disj)

lemma abs_conv_abscissa_shift [simp]:
  "abs_conv_abscissa (fds_shift c f) = abs_conv_abscissa (f :: 'a :: dirichlet_series fds) + c  1"
proof -
  have "abs_conv_abscissa (fds_shift c f)  abs_conv_abscissa f + c  1" for c :: 'a and f
  proof (rule abs_conv_abscissa_leI)
    fix d assume "abs_conv_abscissa f + c  1 < ereal d"
    hence "abs_conv_abscissa f < ereal (d - c  1)" by (cases "abs_conv_abscissa f") auto
    hence "fds_abs_converges (fds_shift c f) (of_real d)"
      by (auto intro!: fds_abs_converges_shift fds_abs_converges simp: algebra_simps)
    thus "s. s  1 = d  fds_abs_converges (fds_shift c f) s"
      by (auto intro!: exI[of _ "of_real d"])
  qed
  note * = this[of c f] this[of "-c" "fds_shift c f"]
  show ?thesis by (cases "abs_conv_abscissa (fds_shift c f)"; cases "abs_conv_abscissa f")
                  (insert *, auto intro!: antisym)
qed

lemma eval_fds_mult:
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  assumes "fds_abs_converges f s" "fds_abs_converges g s"
  shows   "eval_fds (f * g) s = eval_fds f s * eval_fds g s"
  using suminf_dirichlet_prod[OF _ _ assms[unfolded fds_abs_converges_def]]
  by (simp_all add: eval_fds_def fds_nth_mult)

lemma eval_fds_power:
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  assumes "fds_abs_converges f s"
  shows "eval_fds (f ^ n) s = eval_fds f s ^ n"
  using assms by (induction n) (simp_all add: eval_fds_mult fds_abs_converges_power)

lemma eval_fds_prod:
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  assumes "(x. x  A  fds_abs_converges (f x) s)"
  shows "eval_fds (prod f A) s = (xA. eval_fds (f x) s)" using assms
  by (induction A rule: infinite_finite_induct) (auto simp: eval_fds_mult fds_abs_converges_prod)

lemma eval_fds_inverse:
  fixes s :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology}"
  assumes "fds_abs_converges f s" "fds_abs_converges (inverse f) s" "fds_nth f 1  0"
  shows   "eval_fds (inverse f) s = inverse (eval_fds f s)"
proof -
  have "eval_fds (inverse f * f) s = eval_fds (inverse f) s * eval_fds f s"
    by (intro eval_fds_mult assms)
  also have "inverse f * f = 1" by (intro fds_left_inverse assms)
  also have "eval_fds 1 s = 1" by simp
  finally show ?thesis by (auto simp: divide_simps)
qed

lemma eval_fds_integral_has_field_derivative:
  fixes s :: "'a :: dirichlet_series"
  assumes "ereal (s  1) > abs_conv_abscissa f"
  assumes "fds_nth f 1 = 0"
  shows   "(eval_fds (fds_integral c f) has_field_derivative eval_fds f s) (at s)"
proof -
  have "conv_abscissa (fds_integral c f)  abs_conv_abscissa (fds_integral c f)"
    by (rule conv_le_abs_conv_abscissa)
  also from assms have " < ereal (s  1)" by (simp add: abs_conv_abscissa_integral)
  finally have "(eval_fds (fds_integral c f) has_field_derivative 
                  eval_fds (fds_deriv (fds_integral c f)) s) (at s)"
    by (intro derivative_eq_intros) auto
  also from assms have "fds_deriv (fds_integral c f) = f"
    by simp
  finally show ?thesis .
qed

lemma holomorphic_fds_eval [holomorphic_intros]:
  "A  {z. Re z > conv_abscissa f}  eval_fds f holomorphic_on A"
  unfolding holomorphic_on_def field_differentiable_def
  by (rule ballI exI derivative_intros)+ auto
    
lemma analytic_fds_eval [holomorphic_intros]:
  assumes "A  {z. Re z > conv_abscissa f}"
  shows   "eval_fds f analytic_on A"
proof -
  have "eval_fds f analytic_on {z. Re z > conv_abscissa f}"
  proof (subst analytic_on_open)
    show "open {z. Re z > conv_abscissa f}"
      by (cases "conv_abscissa f") (simp_all add: open_halfspace_Re_gt)
  qed (intro holomorphic_intros, simp_all)
  from analytic_on_subset[OF this assms] show ?thesis .
qed

lemma conv_abscissa_0 [simp]: 
  "conv_abscissa (0 :: 'a :: dirichlet_series fds) = -"
  by (auto simp: conv_abscissa_MInf_iff)

lemma abs_conv_abscissa_0 [simp]: 
  "abs_conv_abscissa (0 :: 'a :: dirichlet_series fds) = -"
  by (auto simp: abs_conv_abscissa_MInf_iff)

lemma conv_abscissa_1 [simp]: 
  "conv_abscissa (1 :: 'a :: dirichlet_series fds) = -"
  by (auto simp: conv_abscissa_MInf_iff)

lemma abs_conv_abscissa_1 [simp]: 
  "abs_conv_abscissa (1 :: 'a :: dirichlet_series fds) = -"
  by (auto simp: abs_conv_abscissa_MInf_iff)

lemma conv_abscissa_const [simp]: 
  "conv_abscissa (fds_const (c :: 'a :: dirichlet_series)) = -"
  by (auto simp: conv_abscissa_MInf_iff)

lemma abs_conv_abscissa_const [simp]: 
  "abs_conv_abscissa (fds_const (c :: 'a :: dirichlet_series)) = -"
  by (auto simp: abs_conv_abscissa_MInf_iff)

lemma conv_abscissa_numeral [simp]: 
  "conv_abscissa (numeral n :: 'a :: dirichlet_series fds) = -"
  by (auto simp: numeral_fds)

lemma abs_conv_abscissa_numeral [simp]: 
  "abs_conv_abscissa (numeral n :: 'a :: dirichlet_series fds) = -"
  by (auto simp: numeral_fds)

lemma abs_conv_abscissa_power_le:
  "abs_conv_abscissa (f ^ n :: 'a :: dirichlet_series fds)  abs_conv_abscissa f"
  by (induction n) (auto intro!: order.trans[OF abs_conv_abscissa_mult_le])

lemma abs_conv_abscissa_power_leI:
  "abs_conv_abscissa (f :: 'a :: dirichlet_series fds)  d  abs_conv_abscissa (f ^ n)  d"
  by (rule order.trans[OF abs_conv_abscissa_power_le])

lemma abs_conv_abscissa_prod_le:
  assumes "x. x  A  abs_conv_abscissa (f x :: 'a :: dirichlet_series fds)  d"
  shows   "abs_conv_abscissa (prod f A)  d" using assms
  by (induction A rule: infinite_finite_induct) (auto intro!: abs_conv_abscissa_mult_leI)

lemma conv_abscissa_add_le:
  "conv_abscissa (f + g :: 'a :: dirichlet_series fds)  max (conv_abscissa f) (conv_abscissa g)"
  by (rule conv_abscissa_leI_weak) (auto intro!: fds_converges_add intro: fds_converges)

lemma conv_abscissa_add_leI:
  "conv_abscissa (f :: 'a :: dirichlet_series fds)  d  conv_abscissa g  d  
     conv_abscissa (f + g)  d"
  using conv_abscissa_add_le[of f g] by (auto simp: le_max_iff_disj)

lemma conv_abscissa_sum_leI:
  assumes "x. x  A  conv_abscissa (f x :: 'a :: dirichlet_series fds)  d"
  shows   "conv_abscissa (sum f A)  d" using assms
  by (induction A rule: infinite_finite_induct) (auto intro!: conv_abscissa_add_leI)

lemma abs_conv_abscissa_add_le:
  "abs_conv_abscissa (f + g :: 'a :: dirichlet_series fds)  max (abs_conv_abscissa f) (abs_conv_abscissa g)"
  by (rule abs_conv_abscissa_leI_weak) (auto intro!: fds_abs_converges_add intro: fds_abs_converges)

lemma abs_conv_abscissa_add_leI:
  "abs_conv_abscissa (f :: 'a :: dirichlet_series fds)  d  abs_conv_abscissa g  d  
     abs_conv_abscissa (f + g)  d"
  using abs_conv_abscissa_add_le[of f g] by (auto simp: le_max_iff_disj)

lemma abs_conv_abscissa_sum_leI:
  assumes "x. x  A  abs_conv_abscissa (f x :: 'a :: dirichlet_series fds)  d"
  shows   "abs_conv_abscissa (sum f A)  d" using assms
  by (induction A rule: infinite_finite_induct) (auto intro!: abs_conv_abscissa_add_leI)

lemma fds_converges_cmult_left [intro]:
  assumes "fds_converges f s"
  shows   "fds_converges (fds_const c * f) s"
proof -
  from assms have "summable (λn. c * (fds_nth f n / nat_power n s))"
    by (intro summable_mult) (auto simp: fds_converges_def)
  thus ?thesis by (simp add: fds_converges_def mult_ac)
qed

lemma fds_converges_cmult_right [intro]:
  assumes "fds_converges f s"
  shows   "fds_converges (f * fds_const c) s"
  using fds_converges_cmult_left[OF assms] by (simp add: mult_ac)

lemma conv_abscissa_cmult_left [simp]:
  fixes c :: "'a :: dirichlet_series" assumes "c  0"
  shows "conv_abscissa (fds_const c * f) = conv_abscissa f"
proof -
  have "fds_converges (fds_const c * f) s  fds_converges f s" for s
  proof
    assume "fds_converges (fds_const c * f) s"
    hence "fds_converges (fds_const (inverse c) * (fds_const c * f)) s"
      by (rule fds_converges_cmult_left)
    also have "fds_const (inverse c) * (fds_const c * f) = fds_const (inverse c * c) * f"
      by simp
    also have "inverse c * c = 1"
      using assms by simp
    finally show "fds_converges f s" by simp
  qed auto
  thus ?thesis by (simp add: conv_abscissa_def)
qed

lemma conv_abscissa_cmult_right [simp]:
  fixes c :: "'a :: dirichlet_series" assumes "c  0"
  shows "conv_abscissa (f * fds_const c) = conv_abscissa f"
  using assms by (subst mult.commute) auto

lemma abs_conv_abscissa_cmult: 
  fixes c :: "'a :: dirichlet_series" assumes "c  0"
  shows "abs_conv_abscissa (fds_const c * f) = abs_conv_abscissa f"
proof (intro antisym)
  have "abs_conv_abscissa (fds_const (inverse c) * (fds_const c * f))  
          abs_conv_abscissa (fds_const c * f)"
    using abs_conv_abscissa_mult_le[of "fds_const (inverse c)" "fds_const c * f"]
    by (auto simp: max_def)
  also have "fds_const (inverse c) * (fds_const c * f) = fds_const (inverse c * c) * f"
    by (simp add: mult_ac)
  also have "inverse c * c = 1" using assms by simp
  finally show "abs_conv_abscissa f  abs_conv_abscissa (fds_const c * f)" by simp
qed (insert abs_conv_abscissa_mult_le[of "fds_const c" f], auto simp: max_def)

lemma conv_abscissa_minus [simp]:
  fixes f :: "'a :: dirichlet_series fds"
  shows "conv_abscissa (-f) = conv_abscissa f"
  using conv_abscissa_cmult_left[of "-1" f] by simp

lemma abs_conv_abscissa_minus [simp]:
  fixes f :: "'a :: dirichlet_series fds"
  shows "abs_conv_abscissa (-f) = abs_conv_abscissa f"
  using abs_conv_abscissa_cmult[of "-1" f] by simp

lemma conv_abscissa_diff_le:
  "conv_abscissa (f - g :: 'a :: dirichlet_series fds)  max (conv_abscissa f) (conv_abscissa g)"
  using conv_abscissa_add_le[of f "-g"] by simp

lemma conv_abscissa_diff_leI:
  "conv_abscissa (f :: 'a :: dirichlet_series fds)  d  conv_abscissa g  d  
     conv_abscissa (f - g)  d"
  using conv_abscissa_add_le[of f "-g"] by (auto simp: le_max_iff_disj)

lemma abs_conv_abscissa_diff_le:
  "abs_conv_abscissa (f - g :: 'a :: dirichlet_series fds) 
     max (abs_conv_abscissa f) (abs_conv_abscissa g)"
  using abs_conv_abscissa_add_le[of f "-g"] by simp

lemma abs_conv_abscissa_diff_leI:
  "abs_conv_abscissa (f :: 'a :: dirichlet_series fds)  d  abs_conv_abscissa g  d  
     abs_conv_abscissa (f - g)  d"
  using abs_conv_abscissa_add_le[of f "-g"] by (auto simp: le_max_iff_disj)

lemmas eval_fds_integral_has_field_derivative' [derivative_intros] = 
  DERIV_chain'[OF _ eval_fds_integral_has_field_derivative]

lemma abs_conv_abscissa_completely_multiplicative_log_deriv:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1  0"
  shows   "abs_conv_abscissa (fds_deriv f / f)  abs_conv_abscissa f"
proof -
  have "fds_deriv f = - fds (λn. fds_nth f n * mangoldt n) * f"
    using assms by (subst completely_multiplicative_fds_deriv') simp_all
  also have " / f = - fds (λn. fds_nth f n * mangoldt n) * (f * inverse f)"
    by (simp add: divide_fds_def)
  also have "f * inverse f = 1" using assms by (intro fds_right_inverse)
  finally have "fds_deriv f / f = - fds (λn. fds_nth f n * mangoldt n)" by simp
  also have "abs_conv_abscissa  = 
               abs_conv_abscissa (fds (λn. fds_nth f n * mangoldt n))" 
    (is "_ = abs_conv_abscissa ?f") by (rule abs_conv_abscissa_minus)
  also have "  abs_conv_abscissa f"
  proof (rule abs_conv_abscissa_leI, goal_cases)
    case (1 c)
    have "fds_abs_converges ?f (of_real c)" unfolding fds_abs_converges_def
    proof (rule summable_comparison_test_ev)
      from 1 have "fds_abs_converges (fds_deriv f) (of_real c)" 
        by (intro fds_abs_converges) (auto simp: abs_conv_abscissa_deriv)
      thus "summable (λn. ¦ln (real n)¦ * norm (fds_nth f n) / norm (nat_power n (of_real c :: 'a)))"
        by (simp add: fds_abs_converges_def fds_deriv_def fds_nth_fds' 
                      scaleR_conv_of_real powr_minus norm_mult norm_divide norm_nat_power)
    next
      show "F n in sequentially.
              norm (norm (fds_nth (fds (λn. fds_nth f n * mangoldt n)) n /
                 nat_power n (of_real c)))
               ¦ln (real n)¦ * norm (fds_nth f n) / norm (nat_power n (of_real c) :: 'a)"
        using eventually_gt_at_top[of 0]
      proof eventually_elim
        case (elim n)
        have "norm (norm (fds_nth (fds (λn. fds_nth f n * mangoldt n)) n /
                  nat_power n (of_real c))) =
                norm (fds_nth f n) * mangoldt n / real n powr c"
          using elim by (simp add: fds_nth_fds' norm_mult norm_divide 
                                   norm_nat_power abs_mult mangoldt_nonneg)
        also have "  norm (fds_nth f n) * ln n / real n powr c" using elim
          by (intro mult_left_mono divide_right_mono mangoldt_le)
             (simp_all add: mangoldt_def)
        finally show ?case using elim by (simp add: norm_nat_power algebra_simps)
      qed
    qed
    thus ?case by (intro exI[of _ "of_real c"]) auto
  qed
  finally show ?thesis .
qed

  
subsection ‹Uniqueness›
  
context
  assumes "SORT_CONSTRAINT ('a :: dirichlet_series)"
begin

lemma norm_dirichlet_series_cutoff_le:
  assumes "fds_abs_converges f (s0 :: 'a)" "N > 0" "s  1  c" "c  s0  1"
  shows   "summable (λn. fds_nth f (n + N) / nat_power (n + N) s)"
          "summable (λn. norm (fds_nth f (n + N)) / nat_power (n + N) c)"
    and   "norm (n. fds_nth f (n + N) / nat_power (n + N) s)  
             (n. norm (fds_nth f (n + N)) / nat_power (n + N) c) / nat_power N (s  1 - c)"
proof -
  from assms have "fds_abs_converges f (of_real c)" 
    using fds_abs_converges_Re_le[of f s0 "of_real c"] by auto
  hence "summable (λn. norm (fds_nth f (n + N) / nat_power (n + N) (of_real c)))"
    unfolding fds_abs_converges_def by (rule summable_ignore_initial_segment)
  also have "?this  summable (λn. norm (fds_nth f (n + N)) / nat_power (n + N) c)"
    by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) 
       (auto simp: norm_divide norm_nat_power)
  finally show *: "summable (λn. norm (fds_nth f (n + N)) / nat_power (n + N) c)" .

  from assms have "fds_abs_converges f s" using fds_abs_converges_Re_le[of f s0 s] by auto
  hence **: "summable (λn. norm (fds_nth f (n + N) / nat_power (n + N) s))"
    unfolding fds_abs_converges_def by (rule summable_ignore_initial_segment)
  thus "summable (λn. fds_nth f (n + N) / nat_power (n + N) s)"
    by (rule summable_norm_cancel)

  have "norm (n. fds_nth f (n + N) / nat_power (n + N) s)
           (n. norm (fds_nth f (n + N) / nat_power (n + N) s))"
    by (intro summable_norm **) 
  also have "  (n. norm (fds_nth f (n + N)) / nat_power (n + N) c / nat_power N (s  1 - c))"
  proof (intro suminf_le * ** summable_divide allI)
    fix n :: nat
    have "real N powr (s  1 - c)  real (n + N) powr (s  1 - c)"
      using assms by (intro powr_mono2) simp_all
    also have "real (n + N) powr c *  = real (n + N) powr (s  1)"
      by (simp add: powr_diff)
    finally have "norm (fds_nth f (n + N)) / real (n + N) powr (s  1) 
                    norm (fds_nth f (n + N)) / (real (n + N) powr c * real N powr (s  1 - c))"
      using N > 0 by (intro divide_left_mono) (simp_all add: mult_left_mono)
    thus "norm (fds_nth f (n + N) / nat_power (n + N) s)  
            norm (fds_nth f (n + N)) / nat_power (n + N) c / nat_power N (s  1 - c)"
      using N > 0 by (simp add: norm_divide norm_nat_power )
  qed
  also have " = (n. norm (fds_nth f (n + N)) / nat_power (n + N) c) / nat_power N (s  1 - c)"
    using * by (rule suminf_divide)
  finally show "norm (n. fds_nth f (n + N) / nat_power (n + N) s)  " .
qed

lemma eval_fds_zeroD_aux:
  fixes h :: "'a fds"
  assumes conv: "fds_abs_converges h (s0 :: 'a)"
  assumes freq: "frequently (λs. eval_fds h s = 0) ((λs. s  1) going_to at_top)"
  shows   "h = 0"
proof (rule ccontr)
  assume "h  0"
  hence ex: "n>0. fds_nth h n  0" by (auto simp: fds_eq_iff)
  define N :: nat where "N = (LEAST n. n > 0  fds_nth h n  0)"
  have N: "N > 0" "fds_nth h N  0" 
    using LeastI_ex[OF ex, folded N_def] by auto
  have less_N: "fds_nth h n = 0" if "n < N" for n
    using Least_le[of "λn. n > 0  fds_nth h n  0" n, folded N_def] that
    by (cases "n = 0") (auto simp: not_less)
      
  define c where "c = s0  1"
  define remainder where "remainder = (λs. (n. fds_nth h (n + Suc N) / nat_power (n + Suc N) s))"
  define A where "A = (n. norm (fds_nth h (n + Suc N)) / nat_power (n + Suc N) c) *
                         nat_power (Suc N) c"

  have eq: "fds_nth h N = nat_power N s * eval_fds h s - nat_power N s * remainder s"
    if "s  1  c" for s :: 'a
  proof -
    from conv and that have conv': "fds_abs_converges h s" 
      unfolding c_def by (rule fds_abs_converges_Re_le)
    hence conv'': "fds_converges h s" by blast
    from conv'' have "(λn. fds_nth h n / nat_power n s) sums eval_fds h s"
      by (simp add: fds_converges_iff)
    hence "(λn. fds_nth h (n + Suc N) / nat_power (n + Suc N) s) sums 
             (eval_fds h s - (n<Suc N. fds_nth h n / nat_power n s))"
      by (rule sums_split_initial_segment)
    also have "(n<Suc N. fds_nth h n / nat_power n s) = 
                 (n<Suc N. if n = N then fds_nth h N / nat_power N s else 0)"
      by (intro sum.cong refl) (auto simp: less_N)
    also have " = fds_nth h N / nat_power N s" by (subst sum.delta) auto
    finally show ?thesis unfolding remainder_def using N > 0 by (auto simp: sums_iff field_simps)
  qed
  
  have remainder_bound: "norm (remainder s)  A / real (Suc N) powr (s  1)"
    if "s  1  c" for s :: 'a
  proof -
    note * = norm_dirichlet_series_cutoff_le[of h s0 "Suc N" c s, folded remainder_def]
    have "norm (remainder s)  (n. norm (fds_nth h (n + Suc N)) /
           nat_power (n + Suc N) c) / nat_power (Suc N) (s  1 - c)"
      using that assms unfolding remainder_def by (intro *) (simp_all add: c_def)
    also have " = A / real (Suc N) powr (s  1)" by (simp add: A_def powr_diff)
    finally show ?thesis .
  qed

  from freq have "c. s. s  1  c  eval_fds h s = 0"
    unfolding frequently_def by (auto simp: eventually_going_to_at_top_linorder)
  hence "k. s. s  1  real k  eval_fds h s = 0" by blast
  then obtain S where S: "k. S k  1  real k  eval_fds h (S k) = 0"
    by metis
  have S_limit: "filterlim (λk. S k  1) at_top sequentially"
    by (rule filterlim_at_top_mono[OF filterlim_real_sequentially]) (use S in auto)

  have "eventually (λk. real k  c) sequentially" by real_asymp
  hence "eventually (λk. norm (fds_nth h N)  
           (real N / real (Suc N)) powr (S k  1) * A) sequentially"
  proof eventually_elim
    case (elim k)
    hence "norm (fds_nth h N) = real N powr (S k  1) *  norm (remainder (S k))"
      (is "_ = _ * ?X") using N > 0 S[of k] eq[of "S k"]
      by (auto simp: norm_mult norm_nat_power c_def)
    also have "norm (remainder (S k))  A / real (Suc N) powr (S k  1)"
      using elim S[of k] by (intro remainder_bound) (simp_all add: c_def)
    finally show ?case
      using N by (simp add: mult_left_mono powr_divide field_simps del: of_nat_Suc)
  qed
  moreover have "((λk. (real N / real (Suc N)) powr (S k  1) * A)  0) sequentially"
    by (rule filterlim_compose[OF _ S_limit]) (use N > 0 in real_asymp)
  ultimately have "((λ_. fds_nth h N)  0) sequentially"
    by (rule Lim_null_comparison)
  hence "fds_nth h N = 0" by (simp add: tendsto_const_iff)
  with fds_nth h N  0 show False by contradiction
qed

lemma eval_fds_zeroD:
  fixes h :: "'a fds"
  assumes conv: "conv_abscissa h < "
  assumes freq: "frequently (λs. eval_fds h s = 0) ((λs. s  1) going_to at_top)"
  shows   "h = 0"
proof -
  have [simp]: "2  (1 :: 'a) = 2"
    using of_real_inner_1[of 2] unfolding of_real_numeral by simp
  from conv obtain s where "fds_converges h s"
    by auto
  hence "fds_abs_converges h (s + 2)"
    by (rule fds_converges_imp_abs_converges) (auto simp: algebra_simps)
  from this assms(2-) show ?thesis by (rule eval_fds_zeroD_aux)
qed

lemma eval_fds_eqD:
  fixes f g :: "'a fds"
  assumes conv: "conv_abscissa f < " "conv_abscissa g < "
  assumes eq:   "frequently (λs. eval_fds f s = eval_fds g s) ((λs. s  1) going_to at_top)"
  shows   "f = g"
proof -
  have conv': "conv_abscissa (f - g) < "
    using assms by (intro le_less_trans[OF conv_abscissa_diff_le]) (auto simp: max_def)

  have "max (conv_abscissa f) (conv_abscissa g) < "
    using conv by (auto simp: max_def)
  from ereal_dense2[OF this] obtain c where c: "max (conv_abscissa f) (conv_abscissa g) < ereal c"
    by auto

  (* TODO: something like "frequently_elim" would be great here *)
  have "frequently (λs. eval_fds f s = eval_fds g s  s  1  c) ((λs. s  1) going_to at_top)"
    using eq by (rule frequently_eventually_frequently) auto
  hence *: "frequently (λs. eval_fds (f - g) s = 0) ((λs. s  1) going_to at_top)"
  proof (rule frequently_mono [rotated], safe, goal_cases)
    case (1 s)
    thus ?case using c
      by (subst eval_fds_diff) (auto intro!: fds_converges intro: less_le_trans)
  qed
  have "f - g = 0" by (rule eval_fds_zeroD fds_abs_converges_diff assms * conv')+
  thus ?thesis by simp
qed

end


subsection ‹Limit at infinity›

lemma eval_fds_at_top_tail_bound:
  fixes f :: "'a :: dirichlet_series fds"
  assumes c: "ereal c > abs_conv_abscissa f"
  defines "B  (n. norm (fds_nth f (n+2)) / real (n+2) powr c) * 2 powr c"
  assumes s: "s  1  c"
  shows   "norm (eval_fds f s - fds_nth f 1)  B / 2 powr (s  1)"
proof -
  from c have "fds_abs_converges f (of_real c)" by (intro fds_abs_converges) simp_all
  also have "?this  summable (λn. norm (fds_nth f n) / real n powr c)"
    unfolding fds_abs_converges_def
    by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) 
       (auto simp: norm_divide norm_nat_power norm_powr_real_powr)
  finally have summable_c:  .

  note c
  also from s have "ereal c  ereal (s  1)" by simp
  finally have "fds_abs_converges f s" by (intro fds_abs_converges) auto
  hence summable: "summable (λn. norm (fds_nth f n / nat_power n s))"
    by (simp add: fds_abs_converges_def)
  from summable_norm_cancel[OF this]
    have "(λn. fds_nth f n / nat_power n s) sums eval_fds f s"
    by (simp add: eval_fds_def sums_iff)
  from sums_split_initial_segment[OF this, of "Suc (Suc 0)"]
    have "norm (eval_fds f s - fds_nth f 1) = norm (n. fds_nth f (n+2) / nat_power (n+2) s)"
    by (auto simp: sums_iff)
  also have "  (n. norm (fds_nth f (n+2) / nat_power (n+2) s))"
    by (intro summable_norm summable_ignore_initial_segment summable)
  also have "  (n. norm (fds_nth f (n+2)) / real (n+2) powr c / 2 powr (s  1 - c))"
  proof (intro suminf_le allI)
    fix n :: nat
    have "norm (fds_nth f (n + 2) / nat_power (n + 2) s) =
            norm (fds_nth f (n + 2)) / real (n+2) powr c / real (n+2) powr (s  1 - c)"
      by (simp add: field_simps powr_diff norm_divide norm_nat_power)
    also have "  norm (fds_nth f (n + 2)) / real (n+2) powr c / 2 powr (s  1 - c)" using s
      by (intro divide_left_mono divide_nonneg_pos powr_mono2 mult_pos_pos) simp_all
    finally show "norm (fds_nth f (n + 2) / nat_power (n + 2) s)  " .
  qed (intro summable_ignore_initial_segment summable summable_divide summable_c)+
  also have " = (n. norm (fds_nth f (n+2)) / real (n+2) powr c) / 2 powr (s  1 - c)"
    by (intro suminf_divide summable_ignore_initial_segment summable_c)
  also have " = B / 2 powr (s  1)" by (simp add: B_def powr_diff)
  finally show ?thesis .
qed

lemma tendsto_eval_fds_Re_at_top:
  assumes "conv_abscissa (f :: 'a :: dirichlet_series fds)  "
  assumes lim: "filterlim (λx. S x  1) at_top F"
  shows   "((λx. eval_fds f (S x))  fds_nth f 1) F"
proof -
  from assms(1) have "abs_conv_abscissa f < "
    using abs_conv_le_conv_abscissa_plus_1[of f] by auto
  from ereal_dense2[OF this] obtain c where c: "abs_conv_abscissa f < ereal c" by auto
  define B where "B = (n. norm (fds_nth f (n+2)) / real (n+2) powr c) * 2 powr c"

  have *: "norm (eval_fds f s - fds_nth f 1)  B / 2 powr (s  1)" if s: "s  1  c" for s
    using eval_fds_at_top_tail_bound[of f c s] that c by (simp add: B_def)
  moreover from lim have "eventually (λx. S x  1  c) F" by (auto simp: filterlim_at_top)
  ultimately have "eventually (λx. norm (eval_fds f (S x) - fds_nth f 1)  
                      B / 2 powr (S x  1)) F" by (auto elim!: eventually_mono)
  moreover have "((λx. B / 2 powr (S x  1))  0) F"
    using filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of "ln 2"] _ lim]
    by (intro real_tendsto_divide_at_top[OF tendsto_const])
       (auto simp: powr_def mult_ac intro!: filterlim_compose[OF exp_at_top])
  ultimately have "((λx. eval_fds f (S x) - fds_nth f 1)  0) F"
    by (rule Lim_null_comparison)
  thus ?thesis by (subst (asm) Lim_null [symmetric])
qed

lemma tendsto_eval_fds_Re_at_top':
  assumes "conv_abscissa (f :: complex fds)  "
  shows   "uniform_limit UNIV (λσ t. eval_fds f (of_real σ + of_real t * 𝗂)
                       ) (λ_ .fds_nth f 1) at_top"
proof -
  from assms(1) have "abs_conv_abscissa f < "
    using abs_conv_le_conv_abscissa_plus_1[of f] by auto
  from ereal_dense2[OF this] obtain c where c: "abs_conv_abscissa f < ereal c" by auto
  define B where "B  (n. norm (fds_nth f (n+2)) / real (n+2) powr c) * 2 powr c"

  show ?thesis
    unfolding uniform_limit_iff
  proof safe
    fix ε :: real assume "ε > 0"
    hence "eventually (λσ. B / 2 powr σ < ε) at_top"
      by real_asymp
    thus "eventually (λσ. tUNIV.
            dist (eval_fds f (of_real σ + of_real t * 𝗂)) (fds_nth f 1) < ε) at_top"
      using eventually_ge_at_top[of c]
    proof eventually_elim
      case (elim σ)
      show ?case
      proof
        fix t :: real
        have "dist (eval_fds f (of_real σ + of_real t * 𝗂)) (fds_nth f 1)  B / 2 powr σ"
          using eval_fds_at_top_tail_bound[of f c "of_real σ + of_real t * 𝗂"] elim c
          by (simp add: dist_norm B_def)
        also have " < ε" by fact
        finally show "dist (eval_fds f (of_real σ + of_real t * 𝗂)) (fds_nth f 1) < ε" .
      qed
    qed
  qed
qed

lemma tendsto_eval_fds_Re_going_to_at_top:
  assumes "conv_abscissa (f :: 'a :: dirichlet_series fds)  "
  shows   "((λs. eval_fds f s)  fds_nth f 1) ((λs. s  1) going_to at_top)"
  using assms by (rule tendsto_eval_fds_Re_at_top) auto

lemma tendsto_eval_fds_Re_going_to_at_top':
  assumes "conv_abscissa (f :: complex fds)  "
  shows   "((λs. eval_fds f s)  fds_nth f 1) (Re going_to at_top)"
  using assms by (rule tendsto_eval_fds_Re_at_top) auto

text ‹
  Any Dirichlet series that is not identically zero and does not diverge everywhere
  has a half-plane in which it converges and is non-zero.
›
theorem fds_nonzero_halfplane_exists:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "conv_abscissa f < " "f  0"
  shows   "eventually (λs. fds_converges f s  eval_fds f s  0) ((λs. s  1) going_to at_top)"
proof -
  from ereal_dense2[OF assms(1)] obtain c where c: "conv_abscissa f < ereal c" by auto
  have "eventually (λs::'a. s  1 > c) ((λs. s  1) going_to at_top)"
    using eventually_gt_at_top[of c] by auto
  hence "eventually (λs. fds_converges f s) ((λs. s  1) going_to at_top)"
    by eventually_elim (use c in auto intro!: fds_converges simp: less_le_trans)
  moreover have "eventually (λs. eval_fds f s  0) ((λs. s  1) going_to at_top)"
    using eval_fds_zeroD[OF assms(1)] assms(2) by (auto simp: frequently_def)
  ultimately show ?thesis by (rule eventually_conj)
qed 


subsection ‹Normed series›

lemma fds_converges_norm_iff [simp]: 
  fixes s :: "'a :: {nat_power_normed_field,banach}"
  shows "fds_converges (fds_norm f) (s  1)  fds_abs_converges f s"
  unfolding fds_converges_def fds_abs_converges_def
  by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]])
     (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power)

lemma fds_abs_converges_norm_iff [simp]: 
  fixes s :: "'a :: {nat_power_normed_field,banach}"
  shows "fds_abs_converges (fds_norm f) (s  1)  fds_abs_converges f s"
  unfolding fds_abs_converges_def
  by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]])
     (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power)

lemma fds_converges_norm_iff': 
  fixes f :: "'a :: {nat_power_normed_field,banach} fds"
  shows "fds_converges (fds_norm f) s  fds_abs_converges f (of_real s)"
  unfolding fds_converges_def fds_abs_converges_def
  by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]])
     (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power)

lemma fds_abs_converges_norm_iff': 
  fixes f :: "'a :: {nat_power_normed_field,banach} fds"
  shows "fds_abs_converges (fds_norm f) s  fds_abs_converges f (of_real s)"
  unfolding fds_abs_converges_def
  by (rule summable_cong [OF eventually_mono[OF eventually_gt_at_top[of 0]]])
     (simp add: fds_abs_converges_def fds_norm_def fds_nth_fds' norm_divide norm_nat_power)

lemma abs_conv_abscissa_norm [simp]: 
  fixes f :: "'a :: dirichlet_series fds"
  shows "abs_conv_abscissa (fds_norm f) = abs_conv_abscissa f"
proof (rule antisym)
  show "abs_conv_abscissa f  abs_conv_abscissa (fds_norm f)"
  proof (rule abs_conv_abscissa_leI_weak)
    fix x assume "abs_conv_abscissa (fds_norm f) < ereal x"
    hence "fds_abs_converges (fds_norm f) (of_real x)" by (intro fds_abs_converges) auto
    thus "fds_abs_converges f (of_real x)" by (simp add: fds_abs_converges_norm_iff')
  qed
qed (auto intro!: abs_conv_abscissa_leI_weak simp: fds_abs_converges_norm_iff' fds_abs_converges)

lemma conv_abscissa_norm [simp]: 
  fixes f :: "'a :: dirichlet_series fds"
  shows "conv_abscissa (fds_norm f) = abs_conv_abscissa f"
proof (rule antisym)
  show "abs_conv_abscissa f  conv_abscissa (fds_norm f)"
  proof (rule abs_conv_abscissa_leI_weak)
    fix x assume "conv_abscissa (fds_norm f) < ereal x"
    hence "fds_converges (fds_norm f) (of_real x)" by (intro fds_converges) auto
    thus "fds_abs_converges f (of_real x)" by (simp add: fds_converges_norm_iff')
  qed
qed (auto intro!: conv_abscissa_leI_weak simp: fds_abs_converges)

lemma 
  fixes f g :: "'a :: dirichlet_series fds"
  assumes "fds_abs_converges (fds_norm f) s" "fds_abs_converges (fds_norm g) s"
  shows   fds_abs_converges_norm_mult: "fds_abs_converges (fds_norm (f * g)) s"
  and     eval_fds_norm_mult_le: 
            "eval_fds (fds_norm (f * g)) s  eval_fds (fds_norm f) s * eval_fds (fds_norm g) s"
proof -
  show conv: "fds_abs_converges (fds_norm (f * g)) s" unfolding fds_abs_converges_def
  proof (rule summable_comparison_test_ev)
    have "fds_abs_converges (fds_norm f * fds_norm g) s" by (rule fds_abs_converges_mult assms)+
    thus "summable (λn. norm (fds_nth (fds_norm f * fds_norm g) n) / nat_power n s)"
      by (simp add: fds_abs_converges_def)
  qed (auto intro!: always_eventually divide_right_mono order.trans[OF fds_nth_norm_mult_le] 
            simp: norm_divide)
  have conv': "fds_abs_converges (fds_norm f * fds_norm g) s"
    by (intro fds_abs_converges_mult assms)
  hence "eval_fds (fds_norm (f * g)) s  eval_fds (fds_norm f * fds_norm g) s"
    using conv unfolding eval_fds_def fds_abs_converges_def norm_divide
    by (intro suminf_le allI divide_right_mono) (simp_all add: norm_mult fds_nth_norm_mult_le)
  also have " = eval_fds (fds_norm f) s * eval_fds (fds_norm g) s"
    by (intro eval_fds_mult assms)
  finally show "eval_fds (fds_norm (f * g)) s  eval_fds (fds_norm f) s * eval_fds (fds_norm g) s" .
qed

lemma eval_fds_norm_nonneg:
  assumes "fds_abs_converges (fds_norm f) s"
  shows   "eval_fds (fds_norm f) s  0"
  using assms unfolding eval_fds_def fds_abs_converges_def
  by (intro suminf_nonneg) auto

lemma
  fixes f :: "'a :: dirichlet_series fds"
  assumes "fds_abs_converges (fds_norm f) s"
  shows   fds_abs_converges_norm_power: "fds_abs_converges (fds_norm (f ^ n)) s"
  and     eval_fds_norm_power_le: 
            "eval_fds (fds_norm (f ^ n)) s  eval_fds (fds_norm f) s ^ n"
proof -
  show *: "fds_abs_converges (fds_norm (f ^ n)) s" for n
    by (induction n) (auto intro!: fds_abs_converges_norm_mult assms)
  show "eval_fds (fds_norm (f ^ n)) s  eval_fds (fds_norm f) s ^ n"
    by (induction n) (auto intro!: order.trans[OF eval_fds_norm_mult_le] assms * 
                                   mult_left_mono eval_fds_norm_nonneg)
qed


subsection ‹Logarithms of Dirichlet series›

(* TODO: Move ? *)
lemma eventually_gt_ereal_at_top: "c    eventually (λx. ereal x > c) at_top"
  by (cases c) auto

lemma eval_fds_log_deriv:
  fixes s :: "'a :: dirichlet_series"
  assumes "fds_nth f 1  0" "s  1 > abs_conv_abscissa f" 
           "s  1 > abs_conv_abscissa (fds_deriv f / f)"
  assumes "eval_fds f s  0"
  shows   "eval_fds (fds_deriv f / f) s = eval_fds (fds_deriv f) s / eval_fds f s"
proof -
  have "eval_fds (fds_deriv f / f * f) s = eval_fds (fds_deriv f / f) s * eval_fds f s"
    using assms by (intro eval_fds_mult fds_abs_converges) auto
  also have "fds_deriv f / f * f = fds_deriv f * (f * inverse f)"
    by (simp add: divide_fds_def algebra_simps)
  also have "f * inverse f = 1" using assms by (intro fds_right_inverse)
  finally show ?thesis using assms by simp
qed

text ‹
  Given a sufficiently nice absolutely convergent Dirichlet series that converges
  to some function $f(s)$ and a holomorphic branch of $\ln f(s)$, we can construct 
  a Dirichlet series that absolutely converges to that logarithm.
›
lemma eval_fds_ln:
  fixes s0 :: ereal
  assumes nz: "s. Re s > s0  eval_fds f s  0" "fds_nth f 1  0"
  assumes l: "exp l = fds_nth f 1" "((g  of_real)  l) at_top"
  assumes g: "s. Re s > s0  exp (g s) = eval_fds f s"
  assumes holo_g: "g holomorphic_on {s. Re s > s0}"
  assumes "ereal (Re s) > s0"
  assumes "s0  abs_conv_abscissa f" and "s0  abs_conv_abscissa (fds_deriv f / f)"
  shows   "eval_fds (fds_ln l f) s = g s"
proof -
  let ?s0 = "abs_conv_abscissa f" and ?s1 = "abs_conv_abscissa (inverse f)"
  let ?h = "λs. eval_fds (fds_ln l f) s - g s"
  let ?A = "{s. Re s > s0}"
  have open_A: "open ?A" by (cases s0) (auto simp: open_halfspace_Re_gt)

  have "conv_abscissa f  abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa)
  moreover from assms have "  " by auto
  ultimately have "conv_abscissa f  " by auto

  have "conv_abscissa (fds_ln l f)  abs_conv_abscissa (fds_ln l f)"
    by (rule conv_le_abs_conv_abscissa)
  also have "  abs_conv_abscissa (fds_deriv f / f)"
    unfolding fds_ln_def by (simp add: abs_conv_abscissa_integral)
  finally have "conv_abscissa (fds_ln l f)  "
    using assms by (auto simp: max_def abs_conv_abscissa_deriv split: if_splits)

  have deriv_g [derivative_intros]:
    "(g has_field_derivative eval_fds (fds_deriv f) s / eval_fds f s) (at s within B)"
    if s: "Re s > s0" for s B
  proof -
    have "conv_abscissa f  abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa)
    also have "  s0" using assms by simp
    also have " < Re s" by fact
    finally have s': "Re s > conv_abscissa f" .

    have deriv_g: "(g has_field_derivative deriv g s) (at s)"
      using holomorphic_derivI[OF holo_g open_A, of s] s
      by (auto simp: at_within_open[OF _ open_A])
    have "((λs. exp (g s)) has_field_derivative eval_fds f s * deriv g s) (at s)" (is ?P)
      by (rule derivative_eq_intros deriv_g s)+ (insert s, simp_all add: g)
    also from s have ev: "eventually (λt. t  ?A) (nhds s)"
      by (intro eventually_nhds_in_open open_A) auto
    have "?P  (eval_fds f has_field_derivative eval_fds f s * deriv g s) (at s)"
      by (intro DERIV_cong_ev refl eventually_mono[OF ev]) (auto simp: g)
    finally have "(eval_fds f has_field_derivative eval_fds f s * deriv g s) (at s)" .
    moreover have "(eval_fds f has_field_derivative eval_fds (fds_deriv f) s) (at s)"
      using s' assms by (intro derivative_intros) auto
    ultimately have "eval_fds f s * deriv g s = eval_fds (fds_deriv f) s"
      by (rule DERIV_unique)
    hence "deriv g s = eval_fds (fds_deriv f) s / eval_fds f s"
      using s nz by (simp add: field_simps)
    with deriv_g show ?thesis by (auto intro: has_field_derivative_at_within)
  qed  

  have "c. z{z. Re z > s0}. ?h z = c"
  proof (rule has_field_derivative_zero_constant, goal_cases)
    case 1
    show ?case using convex_halfspace_gt[of _ "1::complex"]
      by (cases s0) auto
  next
    case (2 z)
    have "conv_abscissa (fds_ln l f)  abs_conv_abscissa (fds_ln l f)"
      by (rule conv_le_abs_conv_abscissa)
    also have "  abs_conv_abscissa (fds_deriv f / f)"
      by (simp add: abs_conv_abscissa_ln)
    also have " < Re z" using 2 assms by (auto simp: abs_conv_abscissa_deriv)
    finally have s1: "conv_abscissa (fds_ln l f) < ereal (Re z)" .

    have "conv_abscissa f  abs_conv_abscissa f"
      by (rule conv_le_abs_conv_abscissa)
    also have " < Re z" using 2 assms by auto
    finally have s2: "conv_abscissa f < ereal (Re z)" .

    from l have "fds_nth f 1  0" by auto
    with 2 assms have *: "eval_fds (fds_deriv f / f) z = eval_fds (fds_deriv f) z / (eval_fds f z)"
      by (auto simp: eval_fds_log_deriv)
    have "eval_fds f z  0" using 2 assms by auto
    show ?case using s1 s2 2 nz
      by (auto intro!: derivative_eq_intros simp: * field_simps)
  qed
  then obtain c where c: "z. Re z > s0  ?h z = c" by blast

  have "(at_top :: real filter)  bot" by simp
  moreover from assms have "s0  " by auto
  have "eventually (λx. c = (?h  of_real) x) at_top"
    using eventually_gt_ereal_at_top[OF s0  ] by eventually_elim (simp add: c)
  hence "((?h  of_real)  c) at_top"
    by (force intro: Lim_transform_eventually) 
  moreover have "((?h  of_real)  fds_nth (fds_ln l f) 1 - l) at_top"
    using conv_abscissa (fds_ln l f)   and l unfolding o_def
    by (intro tendsto_intros tendsto_eval_fds_Re_at_top) (auto simp: filterlim_ident)
  ultimately have "c = fds_nth (fds_ln l f) 1 - l"
    by (rule tendsto_unique)
  with c[OF Re s > s0] and l and nz show ?thesis
    by (simp add: exp_minus field_simps)
qed

text ‹
  Less explicitly: For a sufficiently nice absolutely convergent Dirichlet series converging
  to a function $f(s)$, the formal logarithm absolutely converges to some logarithm of $f(s)$.
›
lemma eval_fds_ln':
  fixes s0 :: ereal
  assumes "ereal (Re s) > s0"
  assumes "s0  abs_conv_abscissa f" and "s0  abs_conv_abscissa (fds_deriv f / f)"
      and nz: "s. Re s > s0  eval_fds f s  0" "fds_nth f 1  0"
  assumes l: "exp l = fds_nth f 1"
  shows   "exp (eval_fds (fds_ln l f) s) = eval_fds f s"
proof -
  let ?s0 = "abs_conv_abscissa f" and ?s1 = "abs_conv_abscissa (inverse f)"
  let ?h = "λs. eval_fds f s * exp (-eval_fds (fds_ln l f) s)"

  have "conv_abscissa f  abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa)
  moreover from assms have "  " by auto
  ultimately have "conv_abscissa f  " by auto

  have "conv_abscissa (fds_ln l f)  abs_conv_abscissa (fds_ln l f)"
    by (rule conv_le_abs_conv_abscissa)
  also have "  abs_conv_abscissa (fds_deriv f / f)"
    unfolding fds_ln_def by (simp add: abs_conv_abscissa_integral)
  finally have "conv_abscissa (fds_ln l f)  "
    using assms by (auto simp: max_def abs_conv_abscissa_deriv split: if_splits)

  have "c. z{z. Re z > s0}. ?h z = c"
  proof (rule has_field_derivative_zero_constant, goal_cases)
    case 1
    show ?case using convex_halfspace_gt[of _ "1::complex"]
      by (cases s0) auto
  next
    case (2 z)
    have "conv_abscissa (fds_ln l f)  abs_conv_abscissa (fds_ln l f)"
      by (rule conv_le_abs_conv_abscissa)
    also have "  abs_conv_abscissa (fds_deriv f / f)"
      unfolding fds_ln_def by (simp add: abs_conv_abscissa_integral)
    also have " < Re z" using 2 assms by (auto simp: abs_conv_abscissa_deriv)
    finally have s1: "conv_abscissa (fds_ln l f) < ereal (Re z)" .

    have "conv_abscissa f  abs_conv_abscissa f"
      by (rule conv_le_abs_conv_abscissa)
    also have " < Re z" using 2 assms by auto
    finally have s2: "conv_abscissa f < ereal (Re z)" .

    from l have "fds_nth f 1  0" by auto
    with 2 assms have *: "eval_fds (fds_deriv f / f) z = eval_fds (fds_deriv f) z / (eval_fds f z)"
      by (subst eval_fds_log_deriv) auto
    have "eval_fds f z  0" using 2 assms by auto
    thus ?case using s1 s2
      by (auto intro!: derivative_eq_intros simp: *)
  qed
  then obtain c where c: "z. Re z > s0  ?h z = c" by blast

  have "(at_top :: real filter)  bot" by simp
  moreover from assms have "s0  " by auto
  have "eventually (λx. c = (?h  of_real) x) at_top"
    using eventually_gt_ereal_at_top[OF s0  ] by eventually_elim (simp add: c)
  hence "((?h  of_real)  c) at_top"
    by (force intro: Lim_transform_eventually) 
  moreover have "((?h  of_real)  fds_nth f 1 * exp (-fds_nth (fds_ln l f) 1)) at_top"
    unfolding o_def using conv_abscissa (fds_ln l f)   and conv_abscissa f  
    by (intro tendsto_intros tendsto_eval_fds_Re_at_top) (auto simp: filterlim_ident)
  ultimately have "c = fds_nth f 1 * exp (-fds_nth (fds_ln l f) 1)"
    by (rule tendsto_unique)
  with c[OF Re s > s0] and l and nz show ?thesis
    by (simp add: exp_minus field_simps)
qed

lemma fds_ln_completely_multiplicative:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "completely_multiplicative_function (fds_nth f)"
  assumes "fds_nth f 1  0"
  shows   "fds_ln l f = fds (λn. if n = 1 then l else fds_nth f n * mangoldt n /R ln n)"
proof -
  have "fds_ln l f = fds_integral l (fds_deriv f / f)"
    by (simp add: fds_ln_def)
  also have "fds_deriv f = -fds (λn. fds_nth f n * mangoldt n) * f"
    by (intro completely_multiplicative_fds_deriv' assms)
  also have " / f = -fds (λn. fds_nth f n * mangoldt n) * (f * inverse f)"
    by (simp add: divide_fds_def)
  also from assms have "f * inverse f = 1"
    by (simp add: fds_right_inverse)
  also have "fds_integral l (- fds (λn. fds_nth f n * mangoldt n) * 1) = 
               fds (λn. if n = 1 then l else fds_nth f n * mangoldt n /R ln n)"
    by (simp add: fds_integral_def cong: if_cong)
  finally show ?thesis .
qed

lemma eval_fds_ln_completely_multiplicative_strong:
  fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds" and g :: "nat  'a"
  defines "h  fds (λn. fds_nth (fds_ln l f) n * g n)"
  assumes "fds_abs_converges h s"
  assumes "completely_multiplicative_function (fds_nth f)" and "fds_nth f 1  0"
  shows  "(λ(p,k). (fds_nth f p / nat_power p s) ^ Suc k * g (p ^ Suc k) / of_nat (Suc k))
            abs_summable_on ({p. prime p} × UNIV)" (is ?th1)
    and  "eval_fds h s = l * g 1 + (a(p, k){p. prime p}×UNIV.
            (fds_nth f p / nat_power p s) ^ Suc k * g (p ^ Suc k) / of_nat (Suc k))" (is ?th2)
proof -
  let ?P = "{p::nat. prime p}"
  interpret f: completely_multiplicative_function "fds_nth f" by fact
  from assms have *: "(λn. fds_nth h n / nat_power n s) abs_summable_on UNIV"
    by (auto simp: abs_summable_on_nat_iff' fds_abs_converges_def)
  have eq: "h = fds (λn. if n = 1 then l * g 1 else fds_nth f n * g n * mangoldt n /R ln (real n))"
    using fds_ln_completely_multiplicative [OF assms(3), of l] 
    by (simp add: h_def fds_eq_iff)

  note *
  also have "(λn. fds_nth h n / nat_power n s) abs_summable_on UNIV 
          (λx. if x = Suc 0 then l * g 1 else fds_nth f x * g x * mangoldt x /R ln (real x) /
                nat_power x s) abs_summable_on {1}  Collect primepow"
    using eq by (intro abs_summable_on_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
  finally have sum1: "(λx. if x = Suc 0 then l * g 1 else 
                        fds_nth f x * g x * mangoldt x /R ln (real x) / nat_power x s)
                      abs_summable_on Collect primepow"
    by (rule abs_summable_on_subset) auto
  also have "?this  (λx. fds_nth f x * g x * mangoldt x /R ln (real x) / nat_power x s) 
                         abs_summable_on Collect primepow" 
    by (intro abs_summable_on_cong) (insert primepow_gt_Suc_0, auto)
  also have "  (λ(p,k). fds_nth f (p ^ Suc k) * g (p ^ Suc k) * mangoldt (p ^ Suc k)
                 /R ln (real (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 "  ?th1"
    by (intro abs_summable_on_cong)
       (auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat 
          nat_power_power_left divide_simps scaleR_conv_of_real simp del: power_Suc)
  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  {1}  {n. primepow n}.
        if n = 1 then l * g 1 else fds_nth f n * g n * mangoldt n /R ln (real n) /  nat_power n s)"
    by (intro infsetsum_cong_neutral) (auto simp: eq fds_nth_fds mangoldt_def)
  also have " = l * g 1 + (an | primepow n.
         if n = 1 then l * g 1 else fds_nth f n * g n * mangoldt n /R ln (real n) / nat_power n s)"
    (is "_ = _ + ?x") using sum1 primepow_gt_Suc_0 by (subst infsetsum_Un_disjoint) auto
  also have "?x =
    (anCollect primepow. fds_nth f n * g n * mangoldt n /R ln (real n) / nat_power n s)"
    (is "_ = infsetsum ?f _") by (intro infsetsum_cong refl) (insert primepow_gt_Suc_0, auto)
  also have " = (a(p,k)(?P × UNIV). fds_nth f (p ^ Suc k) * g (p ^ Suc k) *
                    mangoldt (p ^ Suc k) /R ln (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 * g (p ^ Suc k) / of_nat (Suc k))"
    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 scaleR_conv_of_real simp del: power_Suc)
  finally show ?th2 .
qed    

lemma eval_fds_ln_completely_multiplicative:
  fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds"
  assumes "completely_multiplicative_function (fds_nth f)" and "fds_nth f 1  0"
  assumes "s  1 > abs_conv_abscissa (fds_deriv f / f)"
  shows  "(λ(p,k). (fds_nth f p / nat_power p s) ^ Suc k / of_nat (Suc k))
            abs_summable_on ({p. prime p} × UNIV)" (is ?th1)
    and  "eval_fds (fds_ln l f) s =
                  l + (a(p, k){p. prime p}×UNIV.
                        (fds_nth f p / nat_power p s) ^ Suc k / of_nat (Suc k))" (is ?th2)
proof -
  from assms have "fds_abs_converges (fds_ln l f) s"
    by (intro fds_abs_converges_ln) (auto intro!: fds_abs_converges_mult intro: fds_abs_converges)
  hence "fds_abs_converges (fds (λn. fds_nth (fds_ln l f) n * 1)) s"
    by simp
  from eval_fds_ln_completely_multiplicative_strong [OF this assms(1,2)] show ?th1 ?th2 
    by simp_all
qed

subsection ‹Exponential and logarithm›

lemma summable_fds_exp_aux:
  assumes "fds_nth f' 1 = (0 :: 'a :: real_normed_algebra_1)"
  shows   "summable (λk. fds_nth (f' ^ k) n /R fact k)"
proof (rule summable_finite)
  fix k assume "k  {..n}"
  hence "n < k" by simp
  also have " < 2 ^ k"
    by (rule less_exp)
  finally have "fds_nth (f' ^ k) n = 0"
    using assms by (intro fds_nth_power_eq_0) auto
  thus "fds_nth (f' ^ k) n /R fact k = 0" by simp
qed auto

lemma
  fixes f :: "'a :: dirichlet_series fds"
  assumes "fds_abs_converges f s"
  shows   fds_abs_converges_exp: "fds_abs_converges (fds_exp f) s"
  and     eval_fds_exp: "eval_fds (fds_exp f) s = exp (eval_fds f s)"
proof -
  have conv: "fds_abs_converges (fds_exp f) s" and ev: "eval_fds (fds_exp f) s = exp (eval_fds f s)"
    if "fds_abs_converges f s" and [simp]: "fds_nth f (Suc 0) = 0" for f
  proof -
    have [simp]: "fds (λn. if n = Suc 0 then 0 else fds_nth f n) = f"
      by (intro fds_eqI) simp_all
    have  "(λ(k,n). fds_nth (f ^ k) n / fact k / nat_power n s) abs_summable_on (UNIV × {1..})"
    proof (subst abs_summable_on_Sigma_iff, safe, goal_cases)
      case (3 k)
      from that have "fds_abs_converges (f ^ k) s" by (intro fds_abs_converges_power)
      hence "(λn. fds_nth (f ^ k) n / nat_power n s * inverse (fact k)) abs_summable_on {1..}"
        unfolding fds_abs_converges_altdef by (intro abs_summable_on_cmult_left)
      thus ?case by (simp add: field_simps)
    next
      case 4
      show ?case unfolding abs_summable_on_nat_iff'
      proof (rule summable_comparison_test_ev[OF always_eventually[OF allI]])
        fix k :: nat
        from that have *: "fds_abs_converges (fds_norm (f ^ k)) (s  1)"
          by (auto simp: fds_abs_converges_power)
        have "(an{1..}. norm (fds_nth (f ^ k) n / fact k / nat_power n s)) =
                (an{1..}. fds_nth (fds_norm (f ^ k)) n / nat_power n (s  1) / fact k)" 
          (is "?S = _") by (intro infsetsum_cong) (simp_all add: norm_divide norm_mult norm_nat_power)
        also have " = (an{1..}. fds_nth (fds_norm (f ^ k)) n / nat_power n (s  1)) /R fact k"
          (is "_ = ?S' /R _") using * unfolding fds_abs_converges_altdef
          by (subst infsetsum_cdiv) (auto simp: abs_summable_on_nat_iff scaleR_conv_of_real divide_simps)
        also have "?S' = eval_fds (fds_norm (f ^ k)) (s  1)"
          using * unfolding fds_abs_converges_altdef eval_fds_def
          by (subst infsetsum_nat) (auto intro!: suminf_cong)
        finally have eq: "?S =  /R fact k" .
        note eq
        also have "?S  0" by (intro infsetsum_nonneg) auto
        hence "?S = norm (norm ?S)" by simp
        also have "eval_fds (fds_norm (f ^ k)) (s  1)  eval_fds (fds_norm f) (s  1) ^ k"
          using that by (intro eval_fds_norm_power_le) auto
        finally show "norm (norm (an{1..}. norm (fds_nth (f ^ k) n / fact k / nat_power n s))) 
                        eval_fds (fds_norm f) (s  1) ^ k /R fact k" 
          by (simp add: divide_right_mono)
      next
        from exp_converges[of "eval_fds (fds_norm f) (s  1)"]
        show "summable (λx. eval_fds (fds_norm f) (s  1) ^ x /R fact x)"
          by (simp add: sums_iff)
      qed
    qed auto
    hence summable:
      "(λ(n,k). fds_nth (f ^ k) n / fact k / nat_power n s) abs_summable_on {1..} × UNIV"
      by (subst abs_summable_on_Times_swap) (simp add: case_prod_unfold)
  
    have summable': "(λk. fds_nth (f ^ k) n / fact k) abs_summable_on UNIV" for n
      using abs_summable_on_cmult_left[of "nat_power n s",
              OF abs_summable_on_Sigma_project2 [OF summable, of n]] by (cases "n = 0") simp_all
  
    have "(λn. ak. fds_nth (f ^ k) n / fact k / nat_power n s) abs_summable_on {1..}"
      using summable by (rule abs_summable_on_Sigma_project1') auto
    also have "?this  (λn. (k. fds_nth (f ^ k) n / fact k) * inverse (nat_power n s)) 
                           abs_summable_on {1..}"
    proof (intro abs_summable_on_cong refl, goal_cases)
      case (1 n)
      hence "(ak. fds_nth (f ^ k) n / fact k / nat_power n s) =
              (ak. fds_nth (f ^ k) n / fact k) * inverse (nat_power n s)"
        using summable'[of n]
        by (subst infsetsum_cmult_left [symmetric]) (auto simp: field_simps)
      also have "(ak. fds_nth (f ^ k) n / fact k) = (k. fds_nth (f ^ k) n / fact k)"
        using summable'[of n] 1 by (intro abs_summable_on_cong refl infsetsum_nat') auto
      finally show ?case .
    qed
    finally show "fds_abs_converges (fds_exp f) s"
      by (simp add: fds_exp_def fds_nth_fds' abs_summable_on_Sigma_iff scaleR_conv_of_real 
                    fds_abs_converges_altdef field_simps)
  
    have "eval_fds (fds_exp f) s = (n. (k. fds_nth (f ^ k) n /R fact k) / nat_power n s)"
      by (simp add: fds_exp_def eval_fds_def fds_nth_fds')
    also have " = (n. (ak. fds_nth (f ^ k) n /R fact k) / nat_power n s)"
    proof (intro suminf_cong, goal_cases)
      case (1 n)
      show ?case
      proof (cases "n = 0")
        case False
        have "(k. fds_nth (f ^ k) n /R fact k) = (ak. fds_nth (f ^ k) n /R fact k)"
          using summable'[of n] False
          by (intro infsetsum_nat' [symmetric]) (auto simp: scaleR_conv_of_real field_simps)
        thus ?thesis by simp
      qed simp_all
    qed
    also have " = (an. (ak. fds_nth (f ^ k) n /R fact k) / nat_power n s)"
    proof (intro infsetsum_nat' [symmetric], goal_cases)
      case 1
      have *: "UNIV - {Suc 0..} = {0}" by auto
      have "(λx. ay. fds_nth (f ^ y) x / fact y / nat_power x s) abs_summable_on {1..}"
        by (intro abs_summable_on_Sigma_project1'[OF summable]) auto
      also have "?this  (λx. (ay. fds_nth (f ^ y) x / fact y) * inverse (nat_power x s)) 
                    abs_summable_on {1..}"
        using summable' by (intro abs_summable_on_cong refl, subst infsetsum_cmult_left [symmetric])
                           (auto simp: field_simps)
      also have "  (λx. (ay. fds_nth (f ^ y) x /R fact y) / (nat_power x s)) 
                    abs_summable_on {1..}" by (simp add: field_simps scaleR_conv_of_real)
      finally show ?case by (rule abs_summable_on_finite_diff) (use * in auto)
    qed
    also have " = (an. (ak. fds_nth (f ^ k) n /R fact k * inverse (nat_power n s)))"
      using summable' by (subst infsetsum_cmult_left) (auto simp: field_simps scaleR_conv_of_real)
    also have " = (an{1..}. (ak. fds_nth (f ^ k) n /R fact k * inverse (nat_power n s)))"
      by (intro infsetsum_cong_neutral) (auto simp: Suc_le_eq)
    also have " = (ak. an{1..}. fds_nth (f ^ k) n / nat_power n s /R fact k)" using summable 
      by (subst infsetsum_swap) (auto simp: field_simps scaleR_conv_of_real case_prod_unfold)
    also have " = (ak. (an{1..}. fds_nth (f ^ k) n / nat_power n s) /R fact k)"
      by (subst infsetsum_scaleR_right) simp
    also have " = (ak. eval_fds f s ^ k /R fact k)"
    proof (intro infsetsum_cong refl, goal_cases)
      case (1 k)
      have *: "fds_abs_converges (f ^ k) s" by (intro fds_abs_converges_power that)
      have "(an{1..}. fds_nth (f ^ k) n / nat_power n s) =
              (an. fds_nth (f ^ k) n / nat_power n s)"
        by (intro infsetsum_cong_neutral) (auto simp: Suc_le_eq)
      also have " = eval_fds (f ^ k) s" using * unfolding eval_fds_def 
        by (intro infsetsum_nat') (auto simp: fds_abs_converges_def abs_summable_on_nat_iff')
      also from that have " = eval_fds f s ^ k" by (simp add: eval_fds_power)
      finally show ?case by simp
    qed
    also have " = (k. eval_fds f s ^ k /R fact k)"
      using exp_converges[of "norm (eval_fds f s)"]
      by (intro infsetsum_nat') (auto simp: abs_summable_on_nat_iff' sums_iff field_simps norm_power)
    also have " = exp (eval_fds f s)" by (simp add: exp_def)
    finally show "eval_fds (fds_exp f) s = exp (eval_fds f s)" .
  qed
  
  define f' where "f' = f - fds_const (fds_nth f 1)"
  have *: "fds_abs_converges (fds_exp f') s" 
    by (auto simp: f'_def intro!: fds_abs_converges_diff conv assms)
  have "fds_abs_converges (fds_const (exp (fds_nth f 1)) * fds_exp f') s"
    unfolding f'_def
    by (intro fds_abs_converges_mult conv fds_abs_converges_diff assms) auto
  thus "fds_abs_converges (fds_exp f) s" unfolding f'_def
    by (simp add: fds_exp_times_fds_nth_0)
  have "eval_fds (fds_exp f) s = eval_fds (fds_const (exp (fds_nth f 1)) * fds_exp f') s"
    by (simp add: f'_def fds_exp_times_fds_nth_0)
  also have " = exp (fds_nth f (Suc 0)) * eval_fds (fds_exp f') s" using *
    using assms by (subst eval_fds_mult) (simp_all)
  also have " = exp (eval_fds f s)" using ev[of f'] assms unfolding f'_def
    by (auto simp: fds_abs_converges_diff eval_fds_diff fds_abs_converges_imp_converges exp_diff)
  finally show "eval_fds (fds_exp f) s = exp (eval_fds f s)" .
qed

lemma fds_exp_add:
  fixes f :: "'a :: dirichlet_series fds"
  shows   "fds_exp (f + g) = fds_exp f * fds_exp g"
proof (rule fds_eqI_truncate)
  fix m :: nat assume m: "m > 0"
  let ?T = "fds_truncate m"
  have "?T (fds_exp (f + g)) = ?T (fds_exp (?T f + ?T g))"
    by (simp add: fds_truncate_exp fds_truncate_add_strong [symmetric])
  also have "fds_exp (?T f + ?T g) = fds_exp (?T f) * fds_exp (?T g)"
  proof (rule eval_fds_eqD)
    have "fds_abs_converges (fds_exp (?T f + ?T g)) 0"
      by (intro fds_abs_converges_exp fds_abs_converges_add) auto
    thus "conv_abscissa (fds_exp (?T f + ?T g)) < "
      using conv_abscissa_PInf_iff by blast
    hence "fds_abs_converges (fds_exp (fds_truncate m f) * fds_exp (fds_truncate m g)) 0"
      by (intro fds_abs_converges_mult fds_abs_converges_exp) auto
    thus "conv_abscissa (fds_exp (fds_truncate m f) * fds_exp (fds_truncate m g)) < "
      using conv_abscissa_PInf_iff by blast
    show "frequently (λs. eval_fds (fds_exp (fds_truncate m f + fds_truncate m g)) s =
                          eval_fds (fds_exp (fds_truncate m f) * fds_exp (fds_truncate m g)) s)
            ((λs. s  1) going_to at_top)"
      by (auto simp: eval_fds_add eval_fds_mult eval_fds_exp fds_abs_converges_add 
                     fds_abs_converges_exp exp_add)
  qed
  also have "?T  = ?T (fds_exp f * fds_exp g)"
    by (subst fds_truncate_mult [symmetric], subst (1 2) fds_truncate_exp)
       (simp add: fds_truncate_mult)
  finally show "?T (fds_exp (f + g)) = " .
qed

lemma fds_exp_minus:
  fixes f :: "'a :: dirichlet_series fds"
  shows   "fds_exp (-f) = inverse (fds_exp f)"
proof (rule fds_right_inverse_unique)
  have "fds_exp f * fds_exp (- f) = fds_exp (f + (-f))"
    by (subst fds_exp_add) simp_all
  also have "f + (-f) = 0" by simp
  also have "fds_exp  = 1" by simp
  finally show "fds_exp f * fds_exp (-f) = 1" .
qed

lemma abs_conv_abscissa_exp: 
  fixes f :: "'a :: dirichlet_series fds"
  shows "abs_conv_abscissa (fds_exp f)  abs_conv_abscissa f"
  by (intro abs_conv_abscissa_mono fds_abs_converges_exp)

lemma fds_deriv_exp [simp]:
  fixes f :: "'a :: dirichlet_series fds"
  shows   "fds_deriv (fds_exp f) = fds_exp f * fds_deriv f"
proof (rule fds_eqI_truncate)
  fix m :: nat assume m: "m > 0"
  let ?T = "fds_truncate m"
  have "abs_conv_abscissa (fds_deriv (?T f)) = -"
    by (simp add: abs_conv_abscissa_deriv)

  have "?T (fds_deriv (fds_exp f)) = ?T (fds_deriv (fds_exp (?T f)))"
    by (simp add: fds_truncate_deriv fds_truncate_exp)
  also have "fds_deriv (fds_exp (?T f)) = fds_exp (?T f) * fds_deriv (?T f)"
  proof (rule eval_fds_eqD)
    note abscissa = conv_le_abs_conv_abscissa abs_conv_abscissa_exp
    note abscissa' = abscissa[THEN le_less_trans]
    have "fds_abs_converges (fds_deriv (fds_exp (fds_truncate m f))) 0"
      by (intro fds_abs_converges )
         (auto simp: abs_conv_abscissa_deriv intro: le_less_trans[OF abs_conv_abscissa_exp])
    thus "conv_abscissa (fds_deriv (fds_exp (fds_truncate m f))) < "
      using conv_abscissa_PInf_iff by blast
    have "fds_abs_converges (fds_exp (fds_truncate m f) * fds_deriv (fds_truncate m f)) 0"
      by (intro fds_abs_converges_mult fds_abs_converges_exp)
         (auto intro: fds_abs_converges simp add: fds_truncate_deriv [symmetric])
    thus "conv_abscissa (fds_exp (fds_truncate m f) * fds_deriv (fds_truncate m f)) < "
      using conv_abscissa_PInf_iff by blast
    show "F s in (λs. s  1) going_to at_top.
            eval_fds (fds_deriv (fds_exp (?T f))) s =
            eval_fds (fds_exp (?T f) * fds_deriv (?T f)) s"
    proof (intro always_eventually eventually_frequently allI, goal_cases)
      case (2 s)
      have "eval_fds (fds_deriv (fds_exp (?T f))) s =
              deriv (eval_fds (fds_exp (?T f))) s"
        by (auto simp: eval_fds_exp eval_fds_mult fds_abs_converges_mult fds_abs_converges_exp
                  fds_abs_converges eval_fds_deriv abscissa')
      also have "eval_fds (fds_exp (?T f)) = (λs. exp (eval_fds (?T f) s))"
        by (intro ext eval_fds_exp) auto
      also have "deriv   = (λs. exp (eval_fds (?T f) s) * deriv (eval_fds (?T f)) s)"
        by (auto intro!: DERIV_imp_deriv derivative_eq_intros simp: eval_fds_deriv)
      also have " = eval_fds (fds_exp (?T f) * fds_deriv (?T f))"
        by (auto simp: eval_fds_exp eval_fds_mult fds_abs_converges_mult fds_abs_converges_exp
                       fds_abs_converges eval_fds_deriv abs_conv_abscissa_deriv)
      finally show ?case .
    qed auto
  qed
  also have "?T  = ?T (fds_exp f * fds_deriv f)"
    by (subst fds_truncate_mult [symmetric])
       (simp add: fds_truncate_exp fds_truncate_deriv [symmetric], simp add: fds_truncate_mult)
  finally show "?T (fds_deriv (fds_exp f)) = " .
qed

lemma fds_exp_ln_strong:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "fds_nth f (Suc 0)  0"
  shows   "fds_exp (fds_ln l f) = fds_const (exp l / fds_nth f (Suc 0)) * f"
proof -
  let ?c = "exp l / fds_nth f (Suc 0)"
  have "f * fds_const ?c = f * (fds_exp (-fds_ln l f) * fds_exp (fds_ln l f)) * fds_const ?c" 
    (is "_ = _ * (?g * ?h) * _") by (subst fds_exp_add [symmetric]) simp
  also have " = fds_const ?c * (f * ?g) * ?h" by (simp add: mult_ac)
  also have "f * ?g = fds_const (inverse ?c)"
  proof (rule fds_deriv_eq_imp_eq)
    have "fds_deriv (f * fds_exp (-fds_ln l f)) = 
            fds_exp (- fds_ln l f) * fds_deriv f * (1 - f / f)"
      by (simp add: divide_fds_def algebra_simps)
    also from assms have "f / f = 1" by (simp add: divide_fds_def fds_right_inverse)
    finally show "fds_deriv (f * fds_exp (-fds_ln l f)) = fds_deriv (fds_const (inverse ?c))" 
      by simp
  qed (insert assms, auto simp: exp_minus field_simps)
  also have "fds_const ?c * fds_const (inverse ?c) = 1"
    using assms by (subst fds_const_mult [symmetric]) (simp add: divide_simps)
  finally show ?thesis by (simp add: mult_ac)
qed

lemma fds_exp_ln [simp]:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "exp l = fds_nth f (Suc 0)"
  shows   "fds_exp (fds_ln l f) = f"
  using assms by (subst fds_exp_ln_strong) auto

lemma fds_ln_exp [simp]:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "l = fds_nth f (Suc 0)"
  shows   "fds_ln l (fds_exp f) = f"
proof (rule fds_deriv_eq_imp_eq)
  have "fds_deriv (fds_ln l (fds_exp f)) = fds_deriv f * (fds_exp f / fds_exp f)"
    by (simp add: algebra_simps divide_fds_def)
  also have "fds_exp f / fds_exp f = 1" by (simp add: divide_fds_def fds_right_inverse)
  finally show "fds_deriv (fds_ln l (fds_exp f)) = fds_deriv f" by simp
qed (insert assms, auto simp: field_simps)


subsection ‹Euler products›

lemma fds_euler_product_LIMSEQ:
  fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds"
  assumes "multiplicative_function (fds_nth f)" and "fds_abs_converges f s"
  shows   "(λn. pn. if prime p then i. fds_nth f (p ^ i) / nat_power (p ^ i) s else 1)  
             eval_fds f s"
  unfolding eval_fds_def
proof (rule euler_product_LIMSEQ)
  show "multiplicative_function (λn. fds_nth f n / nat_power n s)"
    by (rule multiplicative_function_divide_nat_power) fact+
qed (insert assms, auto simp: fds_abs_converges_def)

lemma fds_euler_product_LIMSEQ':
  fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds"
  assumes "completely_multiplicative_function (fds_nth f)" and "fds_abs_converges f s"
  shows   "(λn. pn. if prime p then inverse (1 - fds_nth f p / nat_power p s) else 1)  
             eval_fds f s"
  unfolding eval_fds_def
proof (rule euler_product_LIMSEQ')
  show "completely_multiplicative_function (λn. fds_nth f n / nat_power n s)"
    by (rule completely_multiplicative_function_divide_nat_power) fact+
qed (insert assms, auto simp: fds_abs_converges_def)

lemma fds_abs_convergent_euler_product:
  fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds"
  assumes "multiplicative_function (fds_nth f)" and "fds_abs_converges f s"
  shows   "abs_convergent_prod 
             (λp. if prime p then i. fds_nth f (p ^ i) / nat_power (p ^ i) s else 1)"
  unfolding eval_fds_def
proof (rule abs_convergent_euler_product)
  show "multiplicative_function (λn. fds_nth f n / nat_power n s)"
    by (rule multiplicative_function_divide_nat_power) fact+
qed (insert assms, auto simp: fds_abs_converges_def)

lemma fds_abs_convergent_euler_product':
  fixes f :: "'a :: {nat_power, real_normed_field, banach, second_countable_topology} fds"
  assumes "completely_multiplicative_function (fds_nth f)" and "fds_abs_converges f s"
  shows   "abs_convergent_prod 
             (λp. if prime p then inverse (1 - fds_nth f p / nat_power p s) else 1)"
  unfolding eval_fds_def
proof (rule abs_convergent_euler_product')
  show "completely_multiplicative_function (λn. fds_nth f n / nat_power n s)"
    by (rule completely_multiplicative_function_divide_nat_power) fact+
qed (insert assms, auto simp: fds_abs_converges_def)

lemma fds_abs_convergent_zero_iff:
  fixes f :: "'a :: {nat_power_field, real_normed_field, banach, second_countable_topology} fds"
  assumes "completely_multiplicative_function (fds_nth f)"
  assumes "fds_abs_converges f s"
  shows   "eval_fds f s = 0  (p. prime p  fds_nth f p = nat_power p s)"
proof -
  let ?g = "λp. if prime p then inverse (1 - fds_nth f p / nat_power p s) else 1" 
  have lim: "(λn. pn. ?g p)  eval_fds f s"
    by (intro fds_euler_product_LIMSEQ' assms)
  have conv: "convergent_prod ?g"
    by (intro abs_convergent_prod_imp_convergent_prod fds_abs_convergent_euler_product' assms)

  {
    assume "eval_fds f s = 0"
    from convergent_prod_to_zero_iff[OF conv] and this and lim
      have "p. prime p  fds_nth f p = nat_power p s" 
      by (auto split: if_splits)
  } moreover {
    assume "p. prime p  fds_nth f p = nat_power p s"
    then obtain p where "prime p" "fds_nth f p = nat_power p s" by blast
    moreover from this have "nat_power p s  0" 
      by (intro nat_power_nonzero) (auto simp: prime_gt_0_nat)
    ultimately have "(λn. pn. ?g p)  0"
      using convergent_prod_to_zero_iff[OF conv]
      by (auto intro!: exI[of _ p] split: if_splits)
    from tendsto_unique[OF _ lim this] have "eval_fds f s = 0"
      by simp
  }
  ultimately show ?thesis by blast
qed

lemma 
  fixes s :: "'a :: {nat_power_normed_field,banach,euclidean_space}"
  assumes "s  1 > 1"
  shows   euler_product_fds_zeta: 
            "(λn. pn. if prime p then inverse (1 - 1 / nat_power p s) else 1)
                 eval_fds fds_zeta s" (is ?th1)
  and     eval_fds_zeta_nonzero: "eval_fds fds_zeta s  0"
proof -
  have *: "completely_multiplicative_function (fds_nth fds_zeta)"
    by standard auto
  have lim: "(λn. pn. if prime p then inverse (1 - fds_nth fds_zeta p / nat_power p s) else 1) 
           eval_fds fds_zeta s" (is "filterlim ?g _ _")
    using assms by (intro fds_euler_product_LIMSEQ' * fds_abs_summable_zeta)
  also have "?g = (λn. pn. if prime p then inverse (1 - 1 / nat_power p s) else 1)"
    by (intro ext prod.cong refl) (auto simp: fds_zeta_def fds_nth_fds)
  finally show ?th1 .

  {
    fix p :: nat assume "prime p"
    from this have "p > 1" by (simp add: prime_gt_Suc_0_nat)
    hence "norm (nat_power p s) = real p powr (s  1)" 
      by (simp add: norm_nat_power)
    also have " > real p powr 0" using assms and p > 1 
      by (intro powr_less_mono) auto
    finally have "nat_power p s  1"
      using p > 1 by auto
  }
  hence **: "p. prime p  fds_nth fds_zeta p = nat_power p s"
    by (auto simp: fds_zeta_def fds_nth_fds)
  show "eval_fds fds_zeta s  0"
    using assms * ** by (subst fds_abs_convergent_zero_iff) simp_all
qed

lemma fds_primepow_subseries_euler_product_cm:
  fixes f :: "'a :: dirichlet_series fds"
  assumes "completely_multiplicative_function (fds_nth f)" "prime p"
  assumes "s  1 > abs_conv_abscissa f"
  shows   "eval_fds (fds_primepow_subseries p f) s = 1 / (1 - fds_nth f p / nat_power p s)"
proof -
  let ?f = "(λn. pan. if prime pa then inverse (1 - fds_nth (fds_primepow_subseries p f) pa /
                 nat_power pa s) else 1)"
  have "sequentially  bot" by simp
  moreover have "?f  eval_fds (fds_primepow_subseries p f) s" 
    by (intro fds_euler_product_LIMSEQ' completely_multiplicative_function_only_pows assms
          fds_abs_converges_subseries) (insert assms, auto intro!: fds_abs_converges)
  moreover have "eventually (λn. ?f n = 1 / (1 - fds_nth f p / nat_power p s)) at_top"
    using eventually_ge_at_top[of p]
  proof eventually_elim
    case (elim n)
    have "(pan. if prime pa then inverse (1 - fds_nth (fds_primepow_subseries p f) pa /
              nat_power pa s) else 1) = 
          (qn. if q = p then inverse (1 - fds_nth f p / nat_power p s) else 1)" using prime p
      by (intro prod.cong) (auto simp: fds_nth_subseries prime_prime_factors)
    also have " = 1 / (1 - fds_nth f p / nat_power p s)"
      using elim by (subst prod.delta) (auto simp: divide_simps)
    finally show ?case .
  qed
  hence "?f  1 / (1 - fds_nth f p / nat_power p s)" by (rule tendsto_eventually)
  ultimately show ?thesis by (rule tendsto_unique)
qed


subsection ‹Non-negative Dirichlet series›

lemma nonneg_Reals_sum: "(x. x  A  f x  0)  sum f A  0"
  by (induction A rule: infinite_finite_induct) auto

locale nonneg_dirichlet_series =
  fixes f :: "'a :: dirichlet_series fds"
  assumes nonneg_coeffs_aux: "n > 0  fds_nth f n  0"
begin

lemma nonneg_coeffs: "fds_nth f n  0"
  using nonneg_coeffs_aux[of n] by (cases "n = 0") auto

end

lemma nonneg_dirichlet_series_0 [simp,intro]: "nonneg_dirichlet_series 0"
  by standard (auto simp: zero_fds_def)

lemma nonneg_dirichlet_series_1 [simp,intro]: "nonneg_dirichlet_series 1"
  by standard (auto simp: one_fds_def)

lemma nonneg_dirichlet_series_const [simp,intro]: 
  "c  0  nonneg_dirichlet_series (fds_const c)"
  by standard (auto simp: fds_const_def)

lemma nonneg_dirichlet_series_add [intro]:
  assumes "nonneg_dirichlet_series f" "nonneg_dirichlet_series g"
  shows   "nonneg_dirichlet_series (f + g)"
proof -
  interpret f: nonneg_dirichlet_series f by fact
  interpret g: nonneg_dirichlet_series g by fact
  show ?thesis
    by standard (auto intro!: nonneg_Reals_add_I f.nonneg_coeffs g.nonneg_coeffs)
qed

lemma nonneg_dirichlet_series_mult [intro]:
  assumes "nonneg_dirichlet_series f" "nonneg_dirichlet_series g"
  shows   "nonneg_dirichlet_series (f * g)"
proof -
  interpret f: nonneg_dirichlet_series f by fact
  interpret g: nonneg_dirichlet_series g by fact
  show ?thesis
    by standard (auto intro!: nonneg_Reals_sum nonneg_Reals_mult_I f.nonneg_coeffs g.nonneg_coeffs 
                      simp: fds_nth_mult dirichlet_prod_def)
qed

lemma nonneg_dirichlet_series_power [intro]:
  assumes "nonneg_dirichlet_series f"
  shows   "nonneg_dirichlet_series (f ^ n)"
  using assms by (induction n) auto

context nonneg_dirichlet_series
begin

lemma nonneg_exp [intro]: "nonneg_dirichlet_series (fds_exp f)"
proof
  fix n :: nat assume "n > 0"
  define c where "c = exp (fds_nth f (Suc 0))"
  define f' where "f' = fds (λn. if n = Suc 0 then 0 else fds_nth f n)"
  from nonneg_coeffs[of 1] obtain c' where "fds_nth f (Suc 0) = of_real c'"
    by (auto elim!: nonneg_Reals_cases)
  hence "c = of_real (exp c')" by (simp add: c_def exp_of_real)
  hence c: "c  0" by simp
  have less: "n < 2 ^ k" if "n < k" for k
  proof -
    have "n < k" by fact
    also have " < 2 ^ k"
      by (rule less_exp)
    finally show ?thesis .
  qed
  have nonneg_power: "fds_nth (f' ^ k) n  0" for k
  proof -
    have "nonneg_dirichlet_series f'"
      by standard (insert nonneg_coeffs, auto simp: f'_def)
    interpret nonneg_dirichlet_series "f' ^ k"
      by (intro nonneg_dirichlet_series_power) fact+
    from nonneg_coeffs[of n] show ?thesis .
  qed
  hence "fds_nth (fds_exp f) n = c * (k. fds_nth (f' ^ k) n /R fact k)"
    by (simp add: fds_exp_def fds_nth_fds' f'_def c_def)
  also have "(k. fds_nth (f' ^ k) n /R fact k) = (kn. fds_nth (f' ^ k) n /R fact k)"
    by (intro suminf_finite) (auto intro!: fds_nth_power_eq_0 less simp: f'_def not_le)
  also have "c *   0" unfolding scaleR_conv_of_real
    by (intro nonneg_Reals_mult_I nonneg_Reals_sum nonneg_power, unfold nonneg_Reals_of_real_iff )
       (auto simp: c)
  finally show "fds_nth (fds_exp f) n  0" .
qed

end

lemma nonneg_dirichlet_series_lnD: 
  assumes "nonneg_dirichlet_series (fds_ln l f)" "exp l = fds_nth f (Suc 0)"
  shows   "nonneg_dirichlet_series f"
proof -
  from assms have "nonneg_dirichlet_series (fds_exp (fds_ln l f))"
    by (intro nonneg_dirichlet_series.nonneg_exp)
  thus ?thesis using assms by simp
qed

context nonneg_dirichlet_series
begin

lemma fds_of_real_norm: "fds_of_real (fds_norm f) = f"
proof (rule fds_eqI)
  fix n :: nat assume n: "n > 0"
  show "fds_nth (fds_of_real (fds_norm f)) n = fds_nth f n"
    using nonneg_coeffs[of n] by (auto elim!: nonneg_Reals_cases)
qed

end

(* TODO: Simplify proof *)
lemma pringsheim_landau_aux:
  fixes c :: real and f :: "complex fds"
  assumes "nonneg_dirichlet_series f"
  assumes abscissa: "c  abs_conv_abscissa f"
  assumes g: "s. s  A  Re s > c  g s = eval_fds f s"
  assumes "g holomorphic_on A" "open A" "c  A"
  shows   "x. x < c  fds_abs_converges f (of_real x)"
proof -
  interpret nonneg_dirichlet_series f by fact
  define a where "a = 1 + c"

  define g' where "g' = (λs. if s  {s. Re s > c} then eval_fds f s else g s)"

  ― ‹We can find some $\varepsilon > 0$ such that the Dirichlet series can be continued
      analytically in a ball of radius $1 + \varepsilon$ around $a$.›
  from open A c  A obtain δ where δ: "δ > 0" "ball c δ  A"
    by (auto simp: open_contains_ball)
  define ε where "ε = sqrt (1 + δ^2) - 1"
  from δ have ε: "ε > 0" by (simp add: ε_def)

  have ball_a_subset: "ball a (1 + ε)  {s. Re s > c}  A"
  proof (intro subsetI)
    fix s :: complex assume s: "s  ball a (1 + ε)"
    define x y where "x = Re s" and "y = Im s"
    have [simp]: "s = x + 𝗂 * y" by (simp add: complex_eq_iff x_def y_def)
    show "s  {s. Re s > c}  A"
    proof (cases "Re s  c")
      case True
      hence "(c - x)2 + y2  (1 + c - x)2 + y2 - 1"
        by (simp add: power2_eq_square algebra_simps)
      also from s have "(1 + c - x)2 + y2 - 1 < δ2"
        by (auto simp: dist_norm cmod_def a_def ε_def)
      finally have "sqrt ((c - x)2 + y2) < δ" using δ
        by (intro real_less_lsqrt) auto
      hence "s  ball c δ" by (auto simp: dist_norm cmod_def)
      also have "  A" by fact
      finally show ?thesis ..
    qed auto
  qed

  have holo: "g' holomorphic_on ball a (1 + ε)" unfolding g'_def
  proof (intro holomorphic_on_subset[OF _ ball_a_subset] holomorphic_on_If_Un)
    have "conv_abscissa f  abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa)
    also have "  ereal c" by fact
    finally have*:  "conv_abscissa f  ereal c" .
    show "eval_fds f holomorphic_on {s. c < Re s}"
      by (intro holomorphic_intros) (auto intro: le_less_trans[OF *])
  qed (insert assms, auto intro!: holomorphic_intros open_halfspace_Re_gt)

  define f' where "f' = fds_norm f"
  have f_f': "f = fds_of_real f'" by (simp add: f'_def fds_of_real_norm)
  have f'_nonneg: "fds_nth f' n  0" for n
    using nonneg_coeffs[of n] by (auto elim!: nonneg_Reals_cases simp: f'_def)

  have deriv: "(λn. (deriv ^^ n) g' a) = (λn. eval_fds ((fds_deriv ^^ n) f) a)"
  proof
    fix n :: nat
    have ev: "eventually (λs. s  {s. Re s > c}) (nhds (complex_of_real a))"
      by (intro eventually_nhds_in_open open_halfspace_Re_gt) (auto simp: a_def)
    have "(deriv ^^ n) g' a = (deriv ^^ n) (eval_fds f) a"
      by (intro higher_deriv_cong_ev refl eventually_mono[OF ev]) (auto simp: g'_def)
    also have " = eval_fds ((fds_deriv ^^ n) f) a"
    proof (intro eval_fds_higher_deriv [symmetric])
      have "conv_abscissa f  abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa)
      also have "  ereal c" by (rule assms)
      also have " < a" by (simp add: a_def)
      finally show "conv_abscissa f < ereal (complex_of_real a  1)" by simp
    qed
    finally show "(deriv ^^ n) g' a = eval_fds ((fds_deriv ^^ n) f) a" .
  qed

  have nth_deriv_conv: "fds_abs_converges ((fds_deriv ^^ n) f) (of_real a)" for n
    by (intro fds_abs_converges)
       (auto simp: abs_conv_abscissa_higher_deriv a_def intro!: le_less_trans[OF abscissa])

  have nth_deriv_eq: "(fds_deriv ^^ n) f = fds (λk. (-1) ^ n * fds_nth f k * ln (real k) ^ n)" for n
  proof -
    have "fds_nth ((fds_deriv ^^ n) f) k = (-1) ^ n * fds_nth f k * ln (real k) ^ n" for k
      by (induction n) (simp_all add: fds_deriv_def fds_eq_iff fds_nth_fds' scaleR_conv_of_real)
    thus ?thesis by (intro fds_eqI) simp_all
  qed

  have deriv': "(λn. eval_fds ((fds_deriv ^^ n) f) (complex_of_real a)) =
      (λn. (- 1) ^ n * complex_of_real (ak. fds_nth f' k * ln (real k) ^ n / real k powr a))"
  proof
    fix n
    have "eval_fds ((fds_deriv ^^ n) f) (of_real a) = 
                 (ak. fds_nth ((fds_deriv ^^ n) f) k / of_nat k powr complex_of_real a)"
      using nth_deriv_conv by (subst eval_fds_altdef) auto
    hence "eval_fds ((fds_deriv ^^ n) f) (of_real a) = 
                 (ak. (- 1) ^ n *R (fds_nth f k * ln (real k) ^ n / k powr a))"
      by (simp add: nth_deriv_eq fds_nth_fds' powr_Reals_eq scaleR_conv_of_real algebra_simps)
    also have " = (- 1) ^ n * (ak. of_real (fds_nth f' k * ln (real k) ^ n / k powr a))"
      by (subst infsetsum_scaleR_right) (simp_all add: scaleR_conv_of_real f_f')
    also have " = (- 1) ^ n * of_real (ak. fds_nth f' k * ln (real k) ^ n / k powr a)"
      by (subst infsetsum_of_real) (rule refl)
    finally show "eval_fds ((fds_deriv ^^ n) f) (complex_of_real a) =
      (- 1) ^ n * complex_of_real (ak. fds_nth f' k * ln (real k) ^ n / real k powr a)" .
  qed

  define s :: complex where "s = c - ε / 2"
  have s: "Re s < c" using assms δ by (simp_all add: s_def ε_def field_simps)
  have "s  ball a (1 + ε)" using s by (simp add: a_def dist_norm cmod_def s_def)
  from holomorphic_power_series[OF holo this]
    have sums: "(λn. (deriv ^^ n) g' a / fact n * (s - a) ^ n) sums g' s" by simp
  also note deriv
  also have "s - a = -of_real (1 + ε / 2)" by (simp add: s_def a_def)
  also have "(λn.  ^ n) = (λn. of_real ((-1) ^ n * (1 + ε / 2) ^ n))"
    by (intro ext) (subst power_minus, auto)
  also have "(λn. eval_fds ((fds_deriv ^^ n) f) a / fact n *  n) =
               (λn. of_real ((-1) ^ n * eval_fds ((fds_deriv ^^ n) f') a / fact n * (1+ε/2) ^ n))"
    using nth_deriv_conv by (simp add: f_f' fds_abs_converges_imp_converges mult_ac)
  finally have "summable " by (simp add: sums_iff)
  hence summable: "summable (λn. (-1)^n * eval_fds ((fds_deriv ^^ n) f') a / fact n * (1+ε/2)^n)"
    by (subst (asm) summable_of_real_iff)

  have "(λ(n,k). (-1)^n * fds_nth f k * ln (real k) ^ n / (real k powr a) * ((s-a) ^ n / fact n))
          abs_summable_on (UNIV × UNIV)"
  proof (subst abs_summable_on_Sigma_iff, safe, goal_cases)
    case (3 n)
    from nth_deriv_conv[of n] show ?case
      unfolding fds_abs_converges_altdef'
      by (intro abs_summable_on_cmult_left) (simp add: nth_deriv_eq fds_nth_fds' powr_Reals_eq)
  next
    case 4
    have nth_deriv_f_f': "(fds_deriv ^^ n) f = fds_of_real ((fds_deriv ^^ n) f')" for n
      by (induction n) (auto simp: f'_def fds_of_real_norm)
    have norm_nth_deriv_f: "norm (fds_nth ((fds_deriv ^^ n) f) k) = 
                                 (-1) ^ n * of_real (fds_nth ((fds_deriv ^^ n) f') k)" for n k
    proof (induction n)
      case (Suc n)
      thus ?case by (cases k) (auto simp: f_f' fds_nth_deriv scaleR_conv_of_real norm_mult)
    qed (auto simp: f'_nonneg f_f')

    note summable
    also have "(λn. (-1)^n * eval_fds ((fds_deriv ^^ n) f') a / fact n * (1+ε/2)^n) =
               (λn. ak. norm ((- 1) ^ n * fds_nth f k * ln (real k) ^ n /
                    (real k powr a) * ((s - a) ^ n / fact n)))" (is "_ = ?h")
    proof (rule ext, goal_cases)
      case (1 n)
      have "(ak. norm ((- 1) ^ n * fds_nth f k * ln (real k) ^ n /
                    (real k powr a) * ((s - a) ^ n / fact n))) =
            (norm ((s - a) ^ n / fact n) * (-1) ^ n) *R 
              (ak. (-1) ^ n * norm (fds_nth ((fds_deriv ^^ n) f) k / real k powr a))" (is "_ = _ *R ?S")
        by (subst infsetsum_scaleR_right [symmetric])
           (auto simp: norm_mult norm_divide norm_power mult_ac nth_deriv_eq fds_nth_fds')
      also have "?S = (ak. fds_nth ((fds_deriv ^^ n) f') k / real k powr a)"
        by (intro infsetsum_cong) (auto simp: norm_mult norm_divide norm_power norm_nth_deriv_f)
      also have " = eval_fds ((fds_deriv ^^ n) f') a"
        using nth_deriv_conv[of n] by (subst eval_fds_altdef) (auto simp: f'_def nth_deriv_f_f')
      also have "(norm ((s - a) ^ n / fact n) * (- 1) ^ n) *R eval_fds ((fds_deriv ^^ n) f') a =
                  (-1) ^ n * eval_fds ((fds_deriv ^^ n) f') a / fact n * norm (s - a) ^ n"
        by (simp add: norm_divide norm_power)
      also have s_a: "s - a = -of_real (1 + ε / 2)" by (simp add: s_def a_def)
      have "norm (s - a) = 1 + ε / 2" unfolding s_a norm_minus_cancel norm_of_real using ε by simp
      finally show ?case ..
    qed
    also have "?h n  0" for n by (intro infsetsum_nonneg) auto
    hence "?h = (λn. norm (?h n))" by simp
    finally show ?case unfolding abs_summable_on_nat_iff' .
  qed auto
  hence "(λ(k,n). (-1)^n * fds_nth f k * ln (real k) ^ n / (real k powr a) * ((s-a) ^ n / fact n))
          abs_summable_on (UNIV × UNIV)"
    by (subst (asm) abs_summable_on_Times_swap) (simp add: case_prod_unfold)
  hence "(λk. an. (- 1) ^ n * fds_nth f k * ln (real k) ^ n / (k powr a) *
           ((s - a) ^ n / fact n)) abs_summable_on UNIV" (is "?h abs_summable_on _")
    by (rule abs_summable_on_Sigma_project1') auto
  also have "?this  (λk. fds_nth f k / nat_power k s) abs_summable_on UNIV"
  proof (intro abs_summable_on_cong refl, goal_cases)
    case (1 k)
    have "?h k = (fds_nth f' k / k powr a) *R (an. (-ln (real k) * (s - a)) ^ n / fact n)"
      by (subst infsetsum_scaleR_right [symmetric], rule infsetsum_cong) 
         (simp_all add: scaleR_conv_of_real f_f' power_minus' power_mult_distrib divide_simps)
    also have "(an. (-ln (real k) * (s - a)) ^ n / fact n) = exp (-ln (real k) * (s - a))"
      using exp_converges[of "-ln k * (s - a)"] exp_converges[of "norm (-ln k * (s - a))"]
      by (subst infsetsum_nat') (auto simp: abs_summable_on_nat_iff' sums_iff scaleR_conv_of_real
                                            divide_simps norm_divide norm_mult norm_power)
    also have "(fds_nth f' k / k powr a) *R  = fds_nth f k / nat_power k s"
      by (auto simp: scaleR_conv_of_real f_f' powr_def exp_minus
                     field_simps exp_of_real [symmetric] exp_diff)
    finally show ?case .
  qed
  finally have "fds_abs_converges f s"
    by (simp add: fds_abs_converges_def abs_summable_on_nat_iff')
  thus ?thesis by (intro exI[of _ "(c - ε / 2)"]) (auto simp: s_def a_def ε)
qed

theorem pringsheim_landau:
  fixes c :: real and f :: "complex fds"
  assumes "nonneg_dirichlet_series f"
  assumes abscissa: "abs_conv_abscissa f = c"
  assumes g: "s. s  A  Re s > c  g s = eval_fds f s"
  assumes "g holomorphic_on A" "open A" "c  A"
  shows   False
proof -
  have "x<c. fds_abs_converges f (complex_of_real x)"
    by (rule pringsheim_landau_aux[where g = g and A = A]) (insert assms, auto)
  then obtain x where x: "x < c" "fds_abs_converges f (complex_of_real x)" by blast
  hence "abs_conv_abscissa f  complex_of_real x  1" 
    unfolding abs_conv_abscissa_def 
    by (intro Inf_lower) (auto simp: image_iff intro!: exI[of _ "of_real x"])
  also have " < abs_conv_abscissa f" using assms x by simp
  finally show False by simp
qed    

corollary entire_continuation_imp_abs_conv_abscissa_MInfty:
  assumes "nonneg_dirichlet_series f"
  assumes c: "c  abs_conv_abscissa f"
  assumes g: "s. Re s > c  g s = eval_fds f s"
  assumes holo: "g holomorphic_on UNIV"
  shows   "abs_conv_abscissa f = -"
proof (rule ccontr)
  assume "abs_conv_abscissa f  -"
  with c obtain a where abscissa [simp]: "abs_conv_abscissa f = ereal a"
    by (cases "abs_conv_abscissa f") auto
  show False
  proof (rule pringsheim_landau[OF assms(1) abscissa _ holo])
    fix s assume s: "Re s > a"
    show "g s = eval_fds f s"
    proof (rule sym, rule analytic_continuation_open[of _ _ _ g])
      show "g holomorphic_on {s. Re s > a}" by (rule holomorphic_on_subset[OF holo]) auto
      from assms show "{s. Re s > c}  {s. Re s > a}" by auto
    next
      have "conv_abscissa f  abs_conv_abscissa f" by (rule conv_le_abs_conv_abscissa)
      also have " = ereal a" by simp
      finally show "eval_fds f holomorphic_on {s. Re s > a}"
        by (intro holomorphic_intros) (auto intro: le_less_trans)
    qed (insert assms s, auto intro!: exI[of _ "of_real (c + 1)"] 
           open_halfspace_Re_gt convex_connected convex_halfspace_Re_gt)
  qed auto
qed



subsection ‹Convergence of the $\zeta$ and M\"{o}bius $\mu$ series›

lemma fds_abs_summable_zeta_real_iff [simp]:
  "fds_abs_converges fds_zeta s  s > (1 :: real)"
proof -
  have "fds_abs_converges fds_zeta s  summable (λn. real n powr -s)"
    unfolding fds_abs_converges_def
    by (intro summable_cong always_eventually)
       (auto simp: fds_nth_zeta powr_minus divide_simps)
  also have "  s > 1" by (simp add: summable_real_powr_iff)
  finally show ?thesis .
qed

lemma fds_abs_summable_zeta_real: "s > (1 :: real)  fds_abs_converges fds_zeta s"
  by simp

lemma fds_abs_converges_moebius_mu_real: 
  assumes "s > (1 :: real)"
  shows   "fds_abs_converges (fds moebius_mu) s"
  unfolding fds_abs_converges_def
proof (rule summable_comparison_test, intro exI allI impI)
  fix n :: nat
  show "norm (norm (fds_nth (fds moebius_mu) n / nat_power n s))  n powr (-s)"
    by (simp add: powr_minus divide_simps abs_moebius_mu_le)
next
  from assms show "summable (λn. real n powr -s)" by (simp add: summable_real_powr_iff)
qed


subsection ‹Application to the M\"{o}bius $\mu$ function›

lemma inverse_squares_sums': "(λn. 1 / real n ^ 2) sums (pi ^ 2 / 6)"
  using inverse_squares_sums sums_Suc_iff[of "λn. 1 / real n ^ 2" "pi^2 / 6"] by simp

lemma norm_summable_moebius_over_square: 
  "summable (λn. norm (moebius_mu n / real n ^ 2))"
proof (subst summable_Suc_iff [symmetric], rule summable_comparison_test)
  show "summable (λn. 1 / real (Suc n) ^ 2)"
    using inverse_squares_sums by (simp add: sums_iff)
qed (auto simp del: of_nat_Suc simp: field_simps abs_moebius_mu_le)

lemma summable_moebius_over_square:
  "summable (λn. moebius_mu n / real n ^ 2)"
  using norm_summable_moebius_over_square by (rule summable_norm_cancel)

lemma moebius_over_square_sums: "(λn. moebius_mu n / n2) sums (6 / pi2)"
proof -
  have "1 = eval_fds (1 :: real fds) 2" by simp
  also have "(1 :: real fds) = fds_zeta * fds moebius_mu" 
    by (rule fds_zeta_times_moebius_mu [symmetric])
  also have "eval_fds  2 = eval_fds fds_zeta 2 * eval_fds (fds moebius_mu) 2"
    by (intro eval_fds_mult fds_abs_converges_moebius_mu_real) simp_all
  also have " = pi ^ 2 / 6 * (n. moebius_mu n / (real n)2)"
    using inverse_squares_sums' by (simp add: eval_fds_at_numeral suminf_fds_zeta_aux sums_iff)
  finally have "(n. moebius_mu n / (real n)2) = 6 / pi ^ 2" by (simp add: field_simps)
  with summable_moebius_over_square show ?thesis by (simp add: sums_iff)
qed

end