Session Zeta_Function

Theory Zeta_Library

section ‹Various preliminary material›
theory Zeta_Library
imports
  "HOL-Complex_Analysis.Complex_Analysis"
  "HOL-Real_Asymp.Real_Asymp"
  "Dirichlet_Series.Dirichlet_Series_Analysis"
begin

subsection ‹Facts about limits›

lemma at_within_altdef:
  "at x within A = (INF S{S. open S  x  S}. principal (S  (A - {x})))"
  unfolding at_within_def nhds_def inf_principal [symmetric]
    by (subst INF_inf_distrib [symmetric]) (auto simp: INF_constant)

lemma tendsto_at_left_realI_sequentially:
  fixes f :: "real  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_left c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_left c)"
proof -
  obtain A where A: "decseq A" "open (A n)" "y  A n" "nhds y = (INF n. principal (A n))" for n
    by (rule nhds_countable[of y]) (rule that)

  have "m. d<c. x{d<..<c}. f x  A m"
  proof (rule ccontr)
    assume "¬ (m. d<c. x{d<..<c}. f x  A m)"
    then obtain m where **: "d. d < c  x{d<..<c}. f x  A m"
      by auto
    have "X. n. (f (X n)  A m  X n < c)  X (Suc n) > c - max 0 ((c - X n) / 2)"
    proof (intro dependent_nat_choice, goal_cases)
      case 1
      from **[of "c - 1"] show ?case by auto
    next
      case (2 x n)
      with **[of "c - max 0 (c - x) / 2"] show ?case by force
    qed
    then obtain X where X: "n. f (X n)  A m" "n. X n < c" "n. X (Suc n) > c - max 0 ((c - X n) / 2)"
      by auto
    have X_ge: "X n  c - (c - X 0) / 2 ^ n" for n
    proof (induction n)
      case (Suc n)
      have "c - (c - X 0) / 2 ^ Suc n = c - (c - (c - (c - X 0) / 2 ^ n)) / 2"
        by simp
      also have "c - (c - (c - (c - X 0) / 2 ^ n)) / 2  c - (c - X n) / 2"
        by (intro diff_left_mono divide_right_mono Suc diff_right_mono) auto
      also have " = c - max 0 ((c - X n) / 2)"
        using X[of n] by (simp add: max_def)
      also have " < X (Suc n)"
        using X[of n] by simp
      finally show ?case by linarith
    qed auto

    have "X  c"
    proof (rule tendsto_sandwich)
      show "eventually (λn. X n  c) sequentially"
        using X by (intro always_eventually) (auto intro!: less_imp_le)
      show "eventually (λn. X n  c - (c - X 0) / 2 ^ n) sequentially"
        using X_ge by (intro always_eventually) auto
    qed real_asymp+
    hence "filterlim X (at_left c) sequentially"
      by (rule tendsto_imp_filterlim_at_left)
         (use X in auto intro!: always_eventually less_imp_le›)
    from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
      by auto
  qed

  then obtain d where d: "d m < c" "x  {d m<..<c}  f x  A m" for m x
    by metis
  have ***: "at_left c = (INF S{S. open S  c  S}. principal (S  {..<c}))"
    by (simp add: at_within_altdef)
  from d show ?thesis
    unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {d m<..}"]) auto
qed

lemma
  shows at_right_PInf [simp]: "at_right ( :: ereal) = bot"
    and at_left_MInf [simp]: "at_left (- :: ereal) = bot"
proof -
  have "{(::ereal)<..} = {}" "{..<-(::ereal)} = {}"
    by auto
  thus "at_right ( :: ereal) = bot" "at_left (- :: ereal) = bot"
    by (simp_all add: at_within_def)
qed

lemma tendsto_at_left_erealI_sequentially:
  fixes f :: "ereal  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_left c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_left c)"
proof (cases c)
  case [simp]: PInf
  have "((λx. f (ereal x))  y) at_top" using assms
    by (intro tendsto_at_topI_sequentially assms)
       (simp_all flip: ereal_tendsto_simps add: o_def filterlim_at)
  thus ?thesis
    by (simp add: at_left_PInf filterlim_filtermap)
next
  case [simp]: MInf
  thus ?thesis by auto
next
  case [simp]: (real c')
  have "((λx. f (ereal x))  y) (at_left c')"
  proof (intro tendsto_at_left_realI_sequentially assms)
    fix X assume *: "filterlim X (at_left c') sequentially"
    show "filterlim (λn. ereal (X n)) (at_left c) sequentially"
      by (rule filterlim_compose[OF _ *])
         (simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_left)
  qed
  thus ?thesis
    by (simp add: at_left_ereal filterlim_filtermap)
qed

lemma tendsto_at_right_realI_sequentially:
  fixes f :: "real  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_right c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_right c)"
proof -
  obtain A where A: "decseq A" "open (A n)" "y  A n" "nhds y = (INF n. principal (A n))" for n
    by (rule nhds_countable[of y]) (rule that)

  have "m. d>c. x{c<..<d}. f x  A m"
  proof (rule ccontr)
    assume "¬ (m. d>c. x{c<..<d}. f x  A m)"
    then obtain m where **: "d. d > c  x{c<..<d}. f x  A m"
      by auto
    have "X. n. (f (X n)  A m  X n > c)  X (Suc n) < c + max 0 ((X n - c) / 2)"
    proof (intro dependent_nat_choice, goal_cases)
      case 1
      from **[of "c + 1"] show ?case by auto
    next
      case (2 x n)
      with **[of "c + max 0 (x - c) / 2"] show ?case by force
    qed
    then obtain X where X: "n. f (X n)  A m" "n. X n > c" "n. X (Suc n) < c + max 0 ((X n - c) / 2)"
      by auto
    have X_le: "X n  c + (X 0 - c) / 2 ^ n" for n
    proof (induction n)
      case (Suc n)
      have "X (Suc n) < c + max 0 ((X n - c) / 2)"
        by (intro X) 
      also have " = c + (X n - c) / 2"
        using X[of n] by (simp add: field_simps max_def)
      also have "  c + (c + (X 0 - c) / 2 ^ n - c) / 2"
        by (intro add_left_mono divide_right_mono Suc diff_right_mono) auto
      also have " = c + (X 0 - c) / 2 ^ Suc n"
        by simp
      finally show ?case by linarith
    qed auto

    have "X  c"
    proof (rule tendsto_sandwich)
      show "eventually (λn. X n  c) sequentially"
        using X by (intro always_eventually) (auto intro!: less_imp_le)
      show "eventually (λn. X n  c + (X 0 - c) / 2 ^ n) sequentially"
        using X_le by (intro always_eventually) auto
    qed real_asymp+
    hence "filterlim X (at_right c) sequentially"
      by (rule tendsto_imp_filterlim_at_right)
         (use X in auto intro!: always_eventually less_imp_le›)
    from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
      by auto
  qed

  then obtain d where d: "d m > c" "x  {c<..<d m}  f x  A m" for m x
    by metis
  have ***: "at_right c = (INF S{S. open S  c  S}. principal (S  {c<..}))"
    by (simp add: at_within_altdef)
  from d show ?thesis
    unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {..<d m}"]) auto
qed

lemma tendsto_at_right_erealI_sequentially:
  fixes f :: "ereal  'b::first_countable_topology"
  assumes *: "X. filterlim X (at_right c) sequentially  (λn. f (X n))  y"
  shows "(f  y) (at_right c)"
proof (cases c)
  case [simp]: MInf
  have "((λx. f (-ereal x))  y) at_top" using assms
   by (intro tendsto_at_topI_sequentially assms)
      (simp_all flip: uminus_ereal.simps ereal_tendsto_simps add: o_def filterlim_at)
  thus ?thesis
    by (simp add: at_right_MInf filterlim_filtermap at_top_mirror)
next
  case [simp]: PInf
  thus ?thesis by auto
next
  case [simp]: (real c')
  have "((λx. f (ereal x))  y) (at_right c')"
  proof (intro tendsto_at_right_realI_sequentially assms)
    fix X assume *: "filterlim X (at_right c') sequentially"
    show "filterlim (λn. ereal (X n)) (at_right c) sequentially"
      by (rule filterlim_compose[OF _ *])
         (simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_right)
  qed
  thus ?thesis
    by (simp add: at_right_ereal filterlim_filtermap)
qed

proposition analytic_continuation':
  assumes hol: "f holomorphic_on S" "g holomorphic_on S"
      and "open S" and "connected S"
      and "U  S" and "ξ  S"
      and "ξ islimpt U"
      and fU0 [simp]: "z. z  U  f z = g z"
      and "w  S"
    shows "f w = g w"
  using analytic_continuation[OF holomorphic_on_diff[OF hol] assms(3-7) _ assms(9)] assms(8)
  by simp


subsection ‹Various facts about integrals›

lemma continuous_on_imp_set_integrable_cbox:
  fixes h :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes "continuous_on (cbox a b) h"
  shows   "set_integrable lborel (cbox a b) h"
proof -
  from assms have "h absolutely_integrable_on cbox a b"
    by (rule absolutely_integrable_continuous)
  moreover have "(λx. indicat_real (cbox a b) x *R h x)  borel_measurable borel"
    by (rule borel_measurable_continuous_on_indicator) (use assms in auto)
  ultimately show ?thesis
    unfolding set_integrable_def using assms by (subst (asm) integrable_completion) auto
qed

lemma set_nn_integral_cong:
  assumes "M = M'" "A = B" "x. x  space M  A  f x = g x"
  shows   "set_nn_integral M A f = set_nn_integral M' B g"
  using assms unfolding assms(1,2) by (intro nn_integral_cong) (auto simp: indicator_def)

lemma set_integrable_bound:
  fixes f :: "'a  'b::{banach, second_countable_topology}"
    and g :: "'a  'c::{banach, second_countable_topology}"
  assumes "set_integrable M A f" "set_borel_measurable M A g"
  assumes "AE x in M. x  A  norm (g x)  norm (f x)"
  shows   "set_integrable M A g"
  unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
  from assms(1) show "integrable M (λx. indicator A x *R f x)"
    by (simp add: set_integrable_def)
  from assms(2) show "(λx. indicat_real A x *R g x)  borel_measurable M"
    by (simp add: set_borel_measurable_def)
  from assms(3) show "AE x in M. norm (indicat_real A x *R g x)  norm (indicat_real A x *R f x)"
    by eventually_elim (simp add: indicator_def)
qed

(* TODO replace version in library. Better name? *)
lemma nn_integral_has_integral_lebesgue:
  fixes f :: "'a::euclidean_space  real"
  assumes nonneg: "x. x  Ω  0  f x" and I: "(f has_integral I) Ω"
  shows "integralN lborel (λx. indicator Ω x * f x) = I"
proof -
  from I have "(λx. indicator Ω x *R f x)  lebesgue M borel"
    by (rule has_integral_implies_lebesgue_measurable)
  then obtain f' :: "'a  real"
    where [measurable]: "f'  borel M borel" and eq: "AE x in lborel. indicator Ω x * f x = f' x"
    by (auto dest: completion_ex_borel_measurable_real)

  from I have "((λx. abs (indicator Ω x * f x)) has_integral I) UNIV"
    using nonneg by (simp add: indicator_def of_bool_def if_distrib[of "λx. x * f y" for y] cong: if_cong)
  also have "((λx. abs (indicator Ω x * f x)) has_integral I) UNIV  ((λx. abs (f' x)) has_integral I) UNIV"
    using eq by (intro has_integral_AE) auto
  finally have "integralN lborel (λx. abs (f' x)) = I"
    by (rule nn_integral_has_integral_lborel[rotated 2]) auto
  also have "integralN lborel (λx. abs (f' x)) = integralN lborel (λx. abs (indicator Ω x * f x))"
    using eq by (intro nn_integral_cong_AE) auto
  also have "(λx. abs (indicator Ω x * f x)) = (λx. indicator Ω x * f x)"
    using nonneg by (auto simp: indicator_def fun_eq_iff)
  finally show ?thesis .
qed


subsection ‹Uniform convergence of integrals›

lemma has_absolute_integral_change_of_variables_1':
  fixes f :: "real  real" and g :: "real  real"
  assumes S: "S  sets lebesgue"
    and der_g: "x. x  S  (g has_field_derivative g' x) (at x within S)"
    and inj: "inj_on g S"
  shows "(λx. ¦g' x¦ *R f(g x)) absolutely_integrable_on S 
           integral S (λx. ¦g' x¦ *R f(g x)) = b
      f absolutely_integrable_on (g ` S)  integral (g ` S) f = b"
proof -
  have "(λx. ¦g' x¦ *R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S 
           integral S (λx. ¦g' x¦ *R vec (f(g x))) = (vec b :: real ^ 1)
          (λx. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) 
           integral (g ` S) (λx. vec (f x)) = (vec b :: real ^ 1)"
    using assms unfolding has_field_derivative_iff_has_vector_derivative
    by (intro has_absolute_integral_change_of_variables_1 assms) auto
  thus ?thesis
    by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
qed

lemma set_nn_integral_lborel_eq_integral:
  fixes f::"'a::euclidean_space  real"
  assumes "set_borel_measurable borel A f"
  assumes "x. x  A  0  f x" "(+xA. f x lborel) < "
  shows "(+xA. f x lborel) = integral A f"
proof -
  have eq: "(+xA. f x lborel) = (+x. ennreal (indicator A x * f x) lborel)"
    by (intro nn_integral_cong) (auto simp: indicator_def)
  also have " = integral UNIV (λx. indicator A x * f x)"
    using assms eq by (intro nn_integral_lborel_eq_integral)
                      (auto simp: indicator_def set_borel_measurable_def)
  also have "integral UNIV (λx. indicator A x * f x) = integral A (λx. indicator A x * f x)"
    by (rule integral_spike_set) (auto intro: empty_imp_negligible)
 
  also have " = integral A f"
    by (rule integral_cong) (auto simp: indicator_def)
  finally show ?thesis .
qed

lemma nn_integral_has_integral_lebesgue':
  fixes f :: "'a::euclidean_space  real"
  assumes nonneg: "x. x  Ω  0  f x" and I: "(f has_integral I) Ω"
  shows "integralN lborel (λx. ennreal (f x) * indicator Ω x) = ennreal I"
proof -
  have "integralN lborel (λx. ennreal (f x) * indicator Ω x) =
        integralN lborel (λx. ennreal (indicator Ω x * f x))"
    by (intro nn_integral_cong) (auto simp: indicator_def)
  also have " = ennreal I"
    using assms by (intro nn_integral_has_integral_lebesgue)
  finally show ?thesis .
qed

lemma uniform_limit_set_lebesgue_integral:
  fixes f :: "'a  'b :: euclidean_space  'c :: {banach, second_countable_topology}"
  assumes "set_integrable lborel X' g"
  assumes [measurable]: "X'  sets borel"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel X' (f y)"
  assumes "y. y  Y  (AE tX' in lborel. norm (f y t)  g t)"
  assumes "eventually (λx. X x  sets borel  X x  X') F"
  assumes "filterlim (λx. set_lebesgue_integral lborel (X x) g)
             (nhds (set_lebesgue_integral lborel X' g)) F"
  shows "uniform_limit Y
           (λx y. set_lebesgue_integral lborel (X x) (f y))
           (λy. set_lebesgue_integral lborel X' (f y)) F"
proof (rule uniform_limitI, goal_cases)
  case (1 ε)
  have integrable_g: "set_integrable lborel U g"
    if "U  sets borel" "U  X'" for U
    by (rule set_integrable_subset[OF assms(1)]) (use that in auto)
  have "eventually (λx. dist (set_lebesgue_integral lborel (X x) g)
                             (set_lebesgue_integral lborel X' g) < ε) F"
    using ε > 0 assms by (auto simp: tendsto_iff)
  from this show ?case using ‹eventually (λ_. _  _) F
  proof eventually_elim
    case (elim x)
    hence [measurable]:"X x  sets borel" and "X x  X'" by auto
    have integrable: "set_integrable lborel U (f y)"
      if "y  Y" "U  sets borel" "U  X'" for y U
      apply (rule set_integrable_subset)
        apply (rule set_integrable_bound[OF assms(1)])
         apply (use assms(3) that in simp add: set_borel_measurable_def›)
      using assms(4)[OF y  Y] apply eventually_elim apply force
      using that apply simp_all
      done
    show ?case
    proof
      fix y assume "y  Y"
      have "dist (set_lebesgue_integral lborel (X x) (f y))
                 (set_lebesgue_integral lborel X' (f y)) =
            norm (set_lebesgue_integral lborel X' (f y) -
                  set_lebesgue_integral lborel (X x) (f y))"
        by (simp add: dist_norm norm_minus_commute)
      also have "set_lebesgue_integral lborel X' (f y) -
                    set_lebesgue_integral lborel (X x) (f y) =
                 set_lebesgue_integral lborel (X' - X x) (f y)"
        unfolding set_lebesgue_integral_def
        apply (subst Bochner_Integration.integral_diff [symmetric])
        unfolding set_integrable_def [symmetric]
          apply (rule integrable; (fact | simp))
         apply (rule integrable; fact)
        apply (intro Bochner_Integration.integral_cong)
         apply (use X x  X' in auto simp: indicator_def›)
        done
      also have "norm   (tX'-X x. norm (f y t) lborel)"
        by (intro set_integral_norm_bound integrable) (fact | simp)+
      also have "AE tX' - X x in lborel. norm (f y t)  g t"
        using assms(4)[OF y  Y] by eventually_elim auto
      with y  Y have "(tX'-X x. norm (f y t) lborel)  (tX'-X x. g t lborel)"
        by (intro set_integral_mono_AE set_integrable_norm integrable integrable_g) auto
      also have " = (tX'. g t lborel) - (tX x. g t lborel)"
        unfolding set_lebesgue_integral_def
        apply (subst Bochner_Integration.integral_diff [symmetric])
        unfolding set_integrable_def [symmetric]
          apply (rule integrable_g; (fact | simp))
         apply (rule integrable_g; fact)
        apply (intro Bochner_Integration.integral_cong)
         apply (use X x  X' in auto simp: indicator_def›)
        done
      also have "  dist (tX x. g t lborel) (tX'. g t lborel)"
        by (simp add: dist_norm)
      also have " < ε" by fact
      finally show "dist (set_lebesgue_integral lborel (X x) (f y))
                         (set_lebesgue_integral lborel X' (f y)) < ε" .
    qed
  qed
qed

lemma integral_dominated_convergence_at_right:
  fixes s :: "real  'a  'b::{banach, second_countable_topology}" and w :: "'a  real"
    and f :: "'a  'b" and M and c :: real
  assumes "f  borel_measurable M" "t. s t  borel_measurable M" "integrable M w"
  assumes lim: "AE x in M. ((λi. s i x)  f x) (at_right c)"
  assumes bound: "F i in at_right c. AE x in M. norm (s i x)  w x"
  shows "((λt. integralL M (s t))  integralL M f) (at_right c)"
proof (rule tendsto_at_right_realI_sequentially)
  fix X :: "nat  real" assume X: "filterlim X (at_right c) sequentially"
  from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
  obtain N where w: "n. N  n  AE x in M. norm (s (X n) x)  w x"
    by (auto simp: eventually_sequentially)

  show "(λn. integralL M (s (X n)))  integralL M f"
  proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
    show "AE x in M. norm (s (X (n + N)) x)  w x" for n
      by (rule w) auto
    show "AE x in M. (λn. s (X (n + N)) x)  f x"
      using lim
    proof eventually_elim
      fix x assume "((λi. s i x)  f x) (at_right c)"
      then show "(λn. s (X (n + N)) x)  f x"
        by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
    qed
  qed fact+
qed

lemma integral_dominated_convergence_at_left:
  fixes s :: "real  'a  'b::{banach, second_countable_topology}" and w :: "'a  real"
    and f :: "'a  'b" and M and c :: real
  assumes "f  borel_measurable M" "t. s t  borel_measurable M" "integrable M w"
  assumes lim: "AE x in M. ((λi. s i x)  f x) (at_left c)"
  assumes bound: "F i in at_left c. AE x in M. norm (s i x)  w x"
  shows "((λt. integralL M (s t))  integralL M f) (at_left c)"
proof (rule tendsto_at_left_realI_sequentially)
  fix X :: "nat  real" assume X: "filterlim X (at_left c) sequentially"
  from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
  obtain N where w: "n. N  n  AE x in M. norm (s (X n) x)  w x"
    by (auto simp: eventually_sequentially)

  show "(λn. integralL M (s (X n)))  integralL M f"
  proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
    show "AE x in M. norm (s (X (n + N)) x)  w x" for n
      by (rule w) auto
    show "AE x in M. (λn. s (X (n + N)) x)  f x"
      using lim
    proof eventually_elim
      fix x assume "((λi. s i x)  f x) (at_left c)"
      then show "(λn. s (X (n + N)) x)  f x"
        by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
    qed
  qed fact+
qed

lemma uniform_limit_interval_integral_right:
  fixes f :: "'a  real  'c :: {banach, second_countable_topology}"
  assumes "interval_lebesgue_integrable lborel a b g"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel (einterval a b) (f y)"
  assumes "y. y  Y  (AE teinterval a b in lborel. norm (f y t)  g t)"
  assumes "a < b"
  shows   "uniform_limit Y (λb' y. LBINT t=a..b'. f y t) (λy. LBINT t=a..b. f y t) (at_left b)"
proof (cases "Y = {}")
  case False
  have g_nonneg: "AE teinterval a b in lborel. g t  0"
  proof -
    from Y  {} obtain y where "y  Y" by auto
    from assms(3)[OF this] show ?thesis 
      by eventually_elim (auto elim: order.trans[rotated])
  qed

  have ev: "eventually (λb'. b'  {a<..<b}) (at_left b)"
    using a < b by (intro eventually_at_leftI)
  with a < b have "?thesis  uniform_limit Y (λb' y. teinterval a (min b b'). f y t lborel)
                                  (λy. teinterval a b. f y t lborel) (at_left b)"
    by (intro filterlim_cong arg_cong2[where f = uniformly_on])
       (auto simp: interval_lebesgue_integral_def fun_eq_iff min_def
             intro!: eventually_mono[OF ev])
  also have 
  proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
    show "F b' in at_left b. einterval a (min b b')  sets borel 
                              einterval a (min b b')  einterval a b"
      using ev by eventually_elim (auto simp: einterval_def)
  next
    show "((λb'. set_lebesgue_integral lborel (einterval a (min b b')) g) 
            set_lebesgue_integral lborel (einterval a b) g) (at_left b)"
      unfolding set_lebesgue_integral_def
    proof (intro tendsto_at_left_erealI_sequentially integral_dominated_convergence)
      have *: "set_borel_measurable borel (einterval a b) g"
        using assms(1) less_imp_le[OF a < b]
        by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
      show "(λx. indicat_real (einterval a b) x *R g x)  borel_measurable lborel"
        using * by (simp add: set_borel_measurable_def)
      fix X :: "nat  ereal" and n :: nat
      have "set_borel_measurable borel (einterval a (min b (X n))) g"
        by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
      thus "(λx. indicat_real (einterval a (min b (X n))) x *R g x)  borel_measurable lborel"
        by (simp add: set_borel_measurable_def)
    next
      fix X :: "nat  ereal"
      assume X: "filterlim X (at_left b) sequentially"
      show "AE x in lborel. (λn. indicat_real (einterval a (min b (X n))) x *R g x)
                indicat_real (einterval a b) x *R g x"
      proof (rule AE_I2)
        fix x :: real
        have "(λt. indicator (einterval a (min b (X t))) x :: real) 
                indicator (einterval a b) x"
        proof (cases "x  einterval a b")
          case False
          hence "x  einterval a (min b (X t))"for t by (auto simp: einterval_def)
          with False show ?thesis by (simp add: indicator_def)
        next
          case True
          with a < b have "eventually (λt. t  {max a x<..<b}) (at_left b)"
            by (intro eventually_at_leftI[of "ereal x"]) (auto simp: einterval_def min_def)
          from this and X have "eventually (λt. X t  {max a x<..<b}) sequentially"
            by (rule eventually_compose_filterlim)
          hence "eventually (λt. indicator (einterval a (min b (X t))) x = (1 :: real)) sequentially"
            by eventually_elim (use True in auto simp: indicator_def einterval_def›)
          from tendsto_eventually[OF this] and True show ?thesis
            by (simp add: indicator_def)
        qed
        thus "(λn. indicat_real (einterval a (min b (X n))) x *R g x)
                  indicat_real (einterval a b) x *R g x" by (intro tendsto_intros)
      qed
    next
      fix X :: "nat  ereal" and n :: nat
      show "AE x in lborel. norm (indicator (einterval a (min b (X n))) x *R g x) 
              indicator (einterval a b) x *R g x"
        using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
    qed (use assms less_imp_le[OF a < b] in 
         auto simp: interval_lebesgue_integrable_def set_integrable_def›) 
  qed (use assms in auto simp: interval_lebesgue_integrable_def›)
  finally show ?thesis .
qed auto

lemma uniform_limit_interval_integral_left:
  fixes f :: "'a  real  'c :: {banach, second_countable_topology}"
  assumes "interval_lebesgue_integrable lborel a b g"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel (einterval a b) (f y)"
  assumes "y. y  Y  (AE teinterval a b in lborel. norm (f y t)  g t)"
  assumes "a < b"
  shows   "uniform_limit Y (λa' y. LBINT t=a'..b. f y t) (λy. LBINT t=a..b. f y t) (at_right a)"
proof (cases "Y = {}")
  case False
  have g_nonneg: "AE teinterval a b in lborel. g t  0"
  proof -
    from Y  {} obtain y where "y  Y" by auto
    from assms(3)[OF this] show ?thesis 
      by eventually_elim (auto elim: order.trans[rotated])
  qed

  have ev: "eventually (λb'. b'  {a<..<b}) (at_right a)"
    using a < b by (intro eventually_at_rightI)
  with a < b have "?thesis  uniform_limit Y (λa' y. teinterval (max a a') b. f y t lborel)
                                  (λy. teinterval a b. f y t lborel) (at_right a)"
    by (intro filterlim_cong arg_cong2[where f = uniformly_on])
       (auto simp: interval_lebesgue_integral_def fun_eq_iff max_def
             intro!: eventually_mono[OF ev])
  also have 
  proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
    show "F a' in at_right a. einterval (max a a') b  sets borel 
                              einterval (max a a') b  einterval a b"
      using ev by eventually_elim (auto simp: einterval_def)
  next
    show "((λa'. set_lebesgue_integral lborel (einterval (max a a') b) g) 
            set_lebesgue_integral lborel (einterval a b) g) (at_right a)"
      unfolding set_lebesgue_integral_def
    proof (intro tendsto_at_right_erealI_sequentially integral_dominated_convergence)
      have *: "set_borel_measurable borel (einterval a b) g"
        using assms(1) less_imp_le[OF a < b]
        by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
      show "(λx. indicat_real (einterval a b) x *R g x)  borel_measurable lborel"
        using * by (simp add: set_borel_measurable_def)
      fix X :: "nat  ereal" and n :: nat
      have "set_borel_measurable borel (einterval (max a (X n)) b) g"
        by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
      thus "(λx. indicat_real (einterval (max a (X n)) b) x *R g x)  borel_measurable lborel"
        by (simp add: set_borel_measurable_def)
    next
      fix X :: "nat  ereal"
      assume X: "filterlim X (at_right a) sequentially"
      show "AE x in lborel. (λn. indicat_real (einterval (max a (X n)) b) x *R g x)
                indicat_real (einterval a b) x *R g x"
      proof (rule AE_I2)
        fix x :: real
        have "(λt. indicator (einterval (max a (X t)) b) x :: real) 
                indicator (einterval a b) x"
        proof (cases "x  einterval a b")
          case False
          hence "x  einterval (max a (X t)) b"for t by (auto simp: einterval_def)
          with False show ?thesis by (simp add: indicator_def)
        next
          case True
          with a < b have "eventually (λt. t  {a<..<x}) (at_right a)"
            by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def)
          from this and X have "eventually (λt. X t  {a<..<x}) sequentially"
            by (rule eventually_compose_filterlim)
          hence "eventually (λt. indicator (einterval (max a (X t)) b) x = (1 :: real)) sequentially"
            by eventually_elim (use True in auto simp: indicator_def einterval_def›)
          from tendsto_eventually[OF this] and True show ?thesis
            by (simp add: indicator_def)
        qed
        thus "(λn. indicat_real (einterval (max a (X n)) b) x *R g x)
                  indicat_real (einterval a b) x *R g x" by (intro tendsto_intros)
      qed
    next
      fix X :: "nat  ereal" and n :: nat
      show "AE x in lborel. norm (indicator (einterval (max a (X n)) b) x *R g x) 
              indicator (einterval a b) x *R g x"
        using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
    qed (use assms less_imp_le[OF a < b] in 
         auto simp: interval_lebesgue_integrable_def set_integrable_def›) 
  qed (use assms in auto simp: interval_lebesgue_integrable_def›)
  finally show ?thesis .
qed auto

lemma uniform_limit_interval_integral_sequentially:
  fixes f :: "'a  real  'c :: {banach, second_countable_topology}"
  assumes "interval_lebesgue_integrable lborel a b g"
  assumes [measurable]: "y. y  Y  set_borel_measurable borel (einterval a b) (f y)"
  assumes "y. y  Y  (AE teinterval a b in lborel. norm (f y t)  g t)"
  assumes a': "filterlim a' (at_right a) sequentially"
  assumes b': "filterlim b' (at_left b) sequentially"
  assumes "a < b"
  shows   "uniform_limit Y (λn y. LBINT t=a' n..b' n. f y t)
             (λy. LBINT t=a..b. f y t) sequentially"
proof (cases "Y = {}")
  case False
  have g_nonneg: "AE teinterval a b in lborel. g t  0"
  proof -
    from Y  {} obtain y where "y  Y" by auto
    from assms(3)[OF this] show ?thesis 
      by eventually_elim (auto elim: order.trans[rotated])
  qed

  have ev: "eventually (λn. a < a' n  a' n < b' n  b' n < b) sequentially"
  proof -
    from ereal_dense2[OF a < b] obtain t where t: "a < ereal t" "ereal t < b" by blast
    from t have "eventually (λn. a' n  {a<..<t}) sequentially"
      by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal t"])
    moreover from t have "eventually (λn. b' n  {t<..<b}) sequentially"
      by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal t"])
    ultimately show "eventually (λn. a < a' n  a' n < b' n  b' n < b) sequentially"
      by eventually_elim auto
  qed

  have "?thesis  uniform_limit Y (λn y. teinterval (max a (a' n)) (min b (b' n)). f y t lborel)
                      (λy. teinterval a b. f y t lborel) sequentially" using a < b
    by (intro filterlim_cong arg_cong2[where f = uniformly_on])
       (auto simp: interval_lebesgue_integral_def fun_eq_iff min_def max_def
             intro!: eventually_mono[OF ev])
  also have 
  proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases)
    show "F n in sequentially. einterval (max a (a' n)) (min b (b' n))  sets borel 
                                einterval (max a (a' n)) (min b (b' n))  einterval a b"
      using ev by eventually_elim (auto simp: einterval_def)
  next
    show "((λn. set_lebesgue_integral lborel (einterval (max a (a' n)) (min b (b' n))) g) 
            set_lebesgue_integral lborel (einterval a b) g) sequentially"
      unfolding set_lebesgue_integral_def
    proof (intro integral_dominated_convergence)
      have *: "set_borel_measurable borel (einterval a b) g"
        using assms(1) less_imp_le[OF a < b]
        by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def)
      show "(λx. indicat_real (einterval a b) x *R g x)  borel_measurable lborel"
        using * by (simp add: set_borel_measurable_def)
      fix n :: nat
      have "set_borel_measurable borel (einterval (max a (a' n)) (min b (b' n))) g"
        by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def)
      thus "(λx. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *R g x)  borel_measurable lborel"
        by (simp add: set_borel_measurable_def)
    next
      show "AE x in lborel. (λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *R g x)
                indicat_real (einterval a b) x *R g x"
      proof (rule AE_I2)
        fix x :: real
        have "(λt. indicator (einterval (max a (a' t)) (min b (b' t))) x :: real) 
                indicator (einterval a b) x"
        proof (cases "x  einterval a b")
          case False
          hence "x  einterval (max a (a' t)) (min b (b' t))"for t
            by (auto simp: einterval_def)
          with False show ?thesis by (simp add: indicator_def)
        next
          case True
          with a < b have "eventually (λt. t  {a<..<x}) (at_right a)"
            by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def)

          have "eventually (λn. x  {a' n<..<b' n}) sequentially"
          proof -
            have "eventually (λn. a' n  {a<..<x}) sequentially" using True
              by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal x"])
                 (auto simp: einterval_def)
            moreover have "eventually (λn. b' n  {x<..<b}) sequentially" using True
              by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal x"])
                 (auto simp: einterval_def)
            ultimately show "eventually (λn. x  {a' n<..<b' n}) sequentially"
              by eventually_elim auto
          qed
          hence "eventually (λt. indicator (einterval (max a (a' t)) (min b (b' t))) x = (1 :: real)) sequentially"
            by eventually_elim (use True in auto simp: indicator_def einterval_def›)
          from tendsto_eventually[OF this] and True show ?thesis
            by (simp add: indicator_def)
        qed
        thus "(λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *R g x)
                  indicat_real (einterval a b) x *R g x" by (intro tendsto_intros)
      qed
    next
      fix X :: "nat  ereal" and n :: nat
      show "AE x in lborel. norm (indicator (einterval (max a (a' n)) (min b (b' n))) x *R g x) 
              indicator (einterval a b) x *R g x"
        using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def)
    qed (use assms less_imp_le[OF a < b] in 
         auto simp: interval_lebesgue_integrable_def set_integrable_def›) 
  qed (use assms in auto simp: interval_lebesgue_integrable_def›)
  finally show ?thesis .
qed auto

lemma interval_lebesgue_integrable_combine:
  assumes "interval_lebesgue_integrable lborel A B f"
  assumes "interval_lebesgue_integrable lborel B C f"
  assumes "set_borel_measurable borel (einterval A C) f"
  assumes "A  B" "B  C"
  shows   "interval_lebesgue_integrable lborel A C f"
proof -
  have meas: "set_borel_measurable borel (einterval A B  einterval B C) f"
    by (rule set_borel_measurable_subset[OF assms(3)]) (use assms in auto simp: einterval_def›)
  have "set_integrable lborel (einterval A B  einterval B C) f"
    using assms by (intro set_integrable_Un) (auto simp: interval_lebesgue_integrable_def)
  also have "?this  set_integrable lborel (einterval A C) f"
  proof (cases "B  {, -}")
    case True
    with assms have "einterval A B  einterval B C = einterval A C"
      by (auto simp: einterval_def)
    thus ?thesis by simp
  next
    case False
    then obtain B' where [simp]: "B = ereal B'"
      by (cases B) auto
    have "indicator (einterval A C) x = (indicator (einterval A B  einterval B C) x :: real)"
      if "x  B'" for x using assms(4,5) that
      by (cases A; cases C) (auto simp: einterval_def indicator_def)
    hence "{x  space lborel. indicat_real (einterval A B  einterval B C) x *R f x 
              indicat_real (einterval A C) x *R f x}  {B'}" by force
    thus ?thesis unfolding set_integrable_def using meas assms
      by (intro integrable_cong_AE AE_I[of _ _ "{B'}"])
         (simp_all add: set_borel_measurable_def)
  qed
  also have "  ?thesis"
    using order.trans[OF assms(4,5)] by (simp add: interval_lebesgue_integrable_def)
  finally show ?thesis .
qed

lemma interval_lebesgue_integrable_bigo_right:
  fixes A B :: real
  fixes f :: "real  real"
  assumes "f  O[at_left B](g)"
  assumes cont: "continuous_on {A..<B} f"
  assumes meas: "set_borel_measurable borel {A<..<B} f"
  assumes "interval_lebesgue_integrable lborel A B g"
  assumes "A < B"
  shows   "interval_lebesgue_integrable lborel A B f"
proof -
  from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x)  c * norm (g x)) (at_left B)"
    by (elim landau_o.bigE)
  then obtain B' where B': "B' < B" "x. x  {B'<..<B}  norm (f x)  c * norm (g x)"
    using A < B by (auto simp: Topological_Spaces.eventually_at_left[of A])

  show ?thesis
  proof (rule interval_lebesgue_integrable_combine)
    show "interval_lebesgue_integrable lborel A (max A B') f"
      using B' assms
      by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto
    show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f"
      using assms by simp
    have meas': "set_borel_measurable borel {max A B'<..<B} f"
      by (rule set_borel_measurable_subset[OF meas]) auto
    have "set_integrable lborel {max A B'<..<B} f"
    proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]])
      have "set_integrable lborel {A<..<B} (λx. c * g x)"
        using assms by (simp add: interval_lebesgue_integrable_def)
      thus "set_integrable lborel {max A B'<..<B} (λx. c * g x)"
        by (rule set_integrable_subset) auto
    next
      fix x assume "x  {max A B'<..<B}"
      hence "norm (f x)  c * norm (g x)"
        by (intro B') auto
      also have "  norm (c * g x)"
        unfolding norm_mult by (intro mult_right_mono) auto
      finally show  "norm (f x)  norm (c * g x)" .
    qed (use meas' in simp_all add: set_borel_measurable_def›)
    thus "interval_lebesgue_integrable lborel (ereal (max A B')) (ereal B) f"
      unfolding interval_lebesgue_integrable_def einterval_eq_Icc using B' < B assms by simp
  qed (use B' assms in auto)
qed

lemma interval_lebesgue_integrable_bigo_left:
  fixes A B :: real
  fixes f :: "real  real"
  assumes "f  O[at_right A](g)"
  assumes cont: "continuous_on {A<..B} f"
  assumes meas: "set_borel_measurable borel {A<..<B} f"
  assumes "interval_lebesgue_integrable lborel A B g"
  assumes "A < B"
  shows   "interval_lebesgue_integrable lborel A B f"
proof -
  from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x)  c * norm (g x)) (at_right A)"
    by (elim landau_o.bigE)
  then obtain A' where A': "A' > A" "x. x  {A<..<A'}  norm (f x)  c * norm (g x)"
    using A < B by (auto simp: Topological_Spaces.eventually_at_right[of A])

  show ?thesis
  proof (rule interval_lebesgue_integrable_combine)
    show "interval_lebesgue_integrable lborel (min B A') B f"
      using A' assms
      by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto
    show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f"
      using assms by simp
    have meas': "set_borel_measurable borel {A<..<min B A'} f"
      by (rule set_borel_measurable_subset[OF meas]) auto
    have "set_integrable lborel {A<..<min B A'} f"
    proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]])
      have "set_integrable lborel {A<..<B} (λx. c * g x)"
        using assms by (simp add: interval_lebesgue_integrable_def)
      thus "set_integrable lborel {A<..<min B A'} (λx. c * g x)"
        by (rule set_integrable_subset) auto
    next
      fix x assume "x  {A<..<min B A'}"
      hence "norm (f x)  c * norm (g x)"
        by (intro A') auto
      also have "  norm (c * g x)"
        unfolding norm_mult by (intro mult_right_mono) auto
      finally show  "norm (f x)  norm (c * g x)" .
    qed (use meas' in simp_all add: set_borel_measurable_def›)
    thus "interval_lebesgue_integrable lborel (ereal A) (ereal (min B A')) f"
      unfolding interval_lebesgue_integrable_def einterval_eq_Icc using A' > A assms by simp
  qed (use A' assms in auto)
qed


subsection ‹Other material›

(* TODO: Library *)
lemma summable_comparison_test_bigo:
  fixes f :: "nat  real"
  assumes "summable (λn. norm (g n))" "f  O(g)"
  shows   "summable f"
proof -
  from f  O(g) obtain C where C: "eventually (λx. norm (f x)  C * norm (g x)) at_top"
    by (auto elim: landau_o.bigE)
  thus ?thesis
    by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
qed

lemma fps_expansion_cong:
  assumes "eventually (λx. g x = h x) (nhds x)"
  shows   "fps_expansion g x = fps_expansion h x"
proof -
  have "(deriv ^^ n) g x = (deriv ^^ n) h x" for n
    by (intro higher_deriv_cong_ev assms refl)
  thus ?thesis by (simp add: fps_expansion_def)
qed

lemma fps_expansion_eq_zero_iff:
  assumes "g holomorphic_on ball z r" "r > 0"
  shows   "fps_expansion g z = 0  (zball z r. g z = 0)"
proof
  assume *: "zball z r. g z = 0"
  have "eventually (λw. w  ball z r) (nhds z)"
    using assms by (intro eventually_nhds_in_open) auto
  hence "eventually (λz. g z = 0) (nhds z)"
    by eventually_elim (use * in auto)
  hence "fps_expansion g z = fps_expansion (λ_. 0) z"
    by (intro fps_expansion_cong)
  thus "fps_expansion g z = 0"
    by (simp add: fps_expansion_def fps_zero_def)
next
  assume *: "fps_expansion g z = 0"
  have "g w = 0" if "w  ball z r" for w
    by (rule holomorphic_fun_eq_0_on_ball[OF assms(1) that])
       (use * in auto simp: fps_expansion_def fps_eq_iff›)
  thus "wball z r. g w = 0" by blast
qed

lemma fds_nth_higher_deriv:
  "fds_nth ((fds_deriv ^^ k) F) = (λn. (-1) ^ k * of_real (ln n) ^ k * fds_nth F n)"
  by (induction k) (auto simp: fds_nth_deriv fun_eq_iff simp flip: scaleR_conv_of_real)

lemma binomial_n_n_minus_one [simp]: "n > 0  n choose (n - Suc 0) = n"
  by (cases n) auto

lemma has_field_derivative_complex_powr_right:
  "w  0  ((λz. w powr z) has_field_derivative Ln w * w powr z) (at z within A)"
  by (rule DERIV_subset, rule has_field_derivative_powr_right) auto

lemmas has_field_derivative_complex_powr_right' =
  has_field_derivative_complex_powr_right[THEN DERIV_chain2]

end

Theory Zeta_Function

(*
    File:      Zeta_Function.thy
    Author:    Manuel Eberl, TU München
*)
section ‹The Hurwitz and Riemann $\zeta$ functions›
theory Zeta_Function
imports
  "Euler_MacLaurin.Euler_MacLaurin"
  "Bernoulli.Bernoulli_Zeta"
  "Dirichlet_Series.Dirichlet_Series_Analysis"
  "Winding_Number_Eval.Winding_Number_Eval"
  "HOL-Real_Asymp.Real_Asymp"
  Zeta_Library
begin

subsection ‹Preliminary facts›

(* TODO Move once Landau symbols are in the distribution *)
lemma holomorphic_on_extend:
  assumes "f holomorphic_on S - {ξ}" "ξ  interior S" "f  O[at ξ](λ_. 1)"
  shows   "(g. g holomorphic_on S  (zS - {ξ}. g z = f z))"
  by (subst holomorphic_on_extend_bounded) (insert assms, auto elim!: landau_o.bigE)

lemma removable_singularities:
  assumes "finite X" "X  interior S" "f holomorphic_on (S - X)"
  assumes "z. z  X  f  O[at z](λ_. 1)"
  shows   "g. g holomorphic_on S  (zS-X. g z = f z)"
  using assms
proof (induction arbitrary: f rule: finite_induct)
  case empty
  thus ?case by auto
next
  case (insert z0 X f)
  from insert.prems and insert.hyps have z0: "z0  interior (S - X)"
    by (auto simp: interior_diff finite_imp_closed)
  hence "g. g holomorphic_on (S - X)  (zS - X - {z0}. g z = f z)"
    using insert.prems insert.hyps by (intro holomorphic_on_extend) auto
  then obtain g where g: "g holomorphic_on (S - X)" "zS - X - {z0}. g z = f z" by blast
  have "h. h holomorphic_on S  (zS - X. h z = g z)"
  proof (rule insert.IH)
    fix z0' assume z0': "z0'  X"
    hence "eventually (λz. z  interior S - (X - {z0'}) - {z0}) (nhds z0')"
      using insert.prems insert.hyps
      by (intro eventually_nhds_in_open open_Diff finite_imp_closed) auto
    hence ev: "eventually (λz. z  S - X - {z0}) (at z0')"
      unfolding eventually_at_filter 
      by eventually_elim (insert z0' insert.hyps interior_subset[of S], auto)
    have "g  Θ[at z0'](f)"
      by (intro bigthetaI_cong eventually_mono[OF ev]) (insert g, auto)
    also have "f  O[at z0'](λ_. 1)"
      using z0' by (intro insert.prems) auto
    finally show "g  " .
  qed (insert insert.prems g, auto)
  then obtain h where "h holomorphic_on S" "zS - X. h z = g z" by blast
  with g have "h holomorphic_on S" "zS - insert z0 X. h z = f z" by auto
  thus ?case by blast
qed

lemma continuous_imp_bigo_1:
  assumes "continuous (at x within A) f"
  shows   "f  O[at x within A](λ_. 1)"
proof (rule bigoI_tendsto)
  from assms show "((λx. f x / 1)  f x) (at x within A)"
    by (auto simp: continuous_within)
qed auto

lemma taylor_bigo_linear:
  assumes "f field_differentiable at x0 within A"
  shows   "(λx. f x - f x0)  O[at x0 within A](λx. x - x0)"
proof -
  from assms obtain f' where "(f has_field_derivative f') (at x0 within A)"
    by (auto simp: field_differentiable_def)
  hence "((λx. (f x - f x0) / (x - x0))  f') (at x0 within A)"
    by (auto simp: has_field_derivative_iff)
  thus ?thesis by (intro bigoI_tendsto[where c = f']) (auto simp: eventually_at_filter)
qed
(* END TODO *)

(* TODO Move? *)
lemma powr_add_minus_powr_asymptotics:
  fixes a z :: complex 
  shows "((λz. ((1 + z) powr a - 1) / z)  a) (at 0)"
proof (rule Lim_transform_eventually)
  have "eventually (λz::complex. z  ball 0 1 - {0}) (at 0)"
    using eventually_at_ball'[of 1 "0::complex" UNIV] by (simp add: dist_norm)
  thus "eventually (λz. (n. (a gchoose (Suc n)) * z ^ n) = ((1 + z) powr a - 1) / z) (at 0)"
  proof eventually_elim
    case (elim z)
    hence "(λn. (a gchoose n) * z ^ n) sums (1 + z) powr a"
      by (intro gen_binomial_complex) auto
    hence "(λn. (a gchoose (Suc n)) * z ^ (Suc n)) sums ((1 + z) powr a - 1)"
      by (subst sums_Suc_iff) simp_all
    also have "(λn. (a gchoose (Suc n)) * z ^ (Suc n)) = (λn. z * ((a gchoose (Suc n)) * z ^ n))"
      by (simp add: algebra_simps)
    finally have "(λn. (a gchoose (Suc n)) * z ^ n) sums (((1 + z) powr a - 1) / z)"
      by (rule sums_mult_D) (use elim in auto)
    thus ?case by (simp add: sums_iff)
  qed
next
  have "conv_radius (λn. a gchoose (n + 1)) = conv_radius (λn. a gchoose n)"
    using conv_radius_shift[of "λn. a gchoose n" 1] by simp
  hence "continuous_on (cball 0 (1/2)) (λz. n. (a gchoose (Suc n)) * (z - 0) ^ n)"
    using conv_radius_gchoose[of a] by (intro powser_continuous_suminf) (simp_all)
  hence "isCont (λz. n. (a gchoose (Suc n)) * z ^ n) 0"
    by (auto intro: continuous_on_interior)
  thus "(λz. n. (a gchoose Suc n) * z ^ n) 0 a"
    by (auto simp: isCont_def)
qed

lemma complex_powr_add_minus_powr_asymptotics:
  fixes s :: complex
  assumes a: "a > 0" and s: "Re s < 1"
  shows "filterlim (λx. of_real (x + a) powr s - of_real x powr s) (nhds 0) at_top"
proof (rule Lim_transform_eventually)
  show "eventually (λx. ((1 + of_real (a / x)) powr s - 1) / of_real (a / x) * 
                            of_real x powr (s - 1) * a = 
                          of_real (x + a) powr s - of_real x powr s) at_top"
    (is "eventually (λx. ?f x / ?g x * ?h x * _ = _) _") using eventually_gt_at_top[of a]
  proof eventually_elim
    case (elim x)
    have "?f x / ?g x * ?h x * a = ?f x * (a * ?h x / ?g x)" by simp
    also have "a * ?h x / ?g x = of_real x powr s"
      using elim a by (simp add: powr_diff)
    also have "?f x *  = of_real (x + a) powr s - of_real x powr s"
      using a elim by (simp add: algebra_simps powr_times_real [symmetric])
    finally show ?case .
  qed

  have "filterlim (λx. complex_of_real (a / x)) (nhds (complex_of_real 0)) at_top"
    by (intro tendsto_of_real real_tendsto_divide_at_top[OF tendsto_const] filterlim_ident)
  hence "filterlim (λx. complex_of_real (a / x)) (at 0) at_top"
    using a by (intro filterlim_atI) auto
  hence "((λx. ?f x / ?g x * ?h x * a)  s * 0 * a) at_top" using s
    by (intro tendsto_mult filterlim_compose[OF powr_add_minus_powr_asymptotics]
              tendsto_const tendsto_neg_powr_complex_of_real filterlim_ident) auto
  thus "((λx. ?f x / ?g x * ?h x * a)  0) at_top" by simp
qed
(* END TODO *)

lemma summable_zeta:
  assumes "Re s > 1"
  shows   "summable (λn. of_nat (Suc n) powr -s)"
proof -
  have "summable (λn. exp (complex_of_real (ln (real (Suc n))) * - s))" (is "summable ?f")
    by (subst summable_Suc_iff, rule summable_complex_powr_iff) (use assms in auto)
  also have "?f = (λn. of_nat (Suc n) powr -s)"
    by (simp add: powr_def algebra_simps del: of_nat_Suc)
  finally show ?thesis .
qed

lemma summable_zeta_real:
  assumes "x > 1"
  shows   "summable (λn. real (Suc n) powr -x)"
proof -
  have "summable (λn. of_nat (Suc n) powr -complex_of_real x)"
    using assms by (intro summable_zeta) simp_all
  also have "(λn. of_nat (Suc n) powr -complex_of_real x) = (λn. of_real (real (Suc n) powr -x))"
    by (subst powr_Reals_eq) simp_all
  finally show ?thesis
    by (subst (asm) summable_complex_of_real)
qed

lemma summable_hurwitz_zeta:
  assumes "Re s > 1" "a > 0"
  shows   "summable (λn. (of_nat n + of_real a) powr -s)"
proof -
  have "summable (λn. (of_nat (Suc n) + of_real a) powr -s)"
  proof (rule summable_comparison_test' [OF summable_zeta_real [OF assms(1)]] )
    fix n :: nat
    have "norm ((of_nat (Suc n) + of_real a) powr -s) = (real (Suc n) + a) powr - Re s"
      (is "?N = _") using assms by (simp add: norm_powr_real_powr)
    also have "  real (Suc n) powr -Re s"
      using assms by (intro powr_mono2') auto
    finally show "?N  " .
  qed
  thus ?thesis by (subst (asm) summable_Suc_iff)
qed

lemma summable_hurwitz_zeta_real:
  assumes "x > 1" "a > 0"
  shows   "summable (λn. (real n + a) powr -x)"
proof -
  have "summable (λn. (of_nat n + of_real a) powr -complex_of_real x)"
    using assms by (intro summable_hurwitz_zeta) simp_all
  also have "(λn. (of_nat n + of_real a) powr -complex_of_real x) = 
               (λn. of_real ((real n + a) powr -x))"
    using assms by (subst powr_Reals_eq) simp_all
  finally show ?thesis
    by (subst (asm) summable_complex_of_real)
qed



subsection ‹Definitions›

text ‹
  We use the Euler--MacLaurin summation formula to express $\zeta(s,a) - \frac{a^{1-s}}{s-1}$ as
  a polynomial plus some remainder term, which is an integral over a function of 
  order $O(-1-2n-\mathfrak{R}(s))$. It is then clear that this integral converges uniformly
  to an analytic function in $s$ for all $s$ with $\mathfrak{R}(s) > -2n$.
›
definition pre_zeta_aux :: "nat  real  complex  complex" where
  "pre_zeta_aux N a s = a powr - s / 2 +
    (i=1..N. (bernoulli (2 * i) / fact (2 * i)) *R (pochhammer s (2*i - 1) * 
                 of_real a powr (- s - of_nat (2*i - 1)))) +
    EM_remainder (Suc (2*N)) 
      (λx. -(pochhammer s (Suc (2*N)) * of_real (x + a) powr (- 1 - 2*N - s))) 0"

text ‹
  By iterating the above construction long enough, we can extend this to the entire
  complex plane.
›
definition pre_zeta :: "real  complex  complex" where
  "pre_zeta a s = pre_zeta_aux (nat (1 - Re s / 2)) a s"

text ‹
  We can then obtain the Hurwitz $\zeta$ function by adding back the pole at 1.
  Note that it is not necessary to trust that this somewhat complicated definition is,
  in fact, the correct one, since we will later show that this Hurwitz zeta function
  fulfils
  \[\zeta(s,a) = \sum_{n=0}^\infty \frac{1}{(n + a)^s}\]
  and is analytic on $\mathbb{C}\setminus \{1\}$, which uniquely defines the function
  due to analytic continuation. It is therefore obvious that any alternative definition
  that is analytic on $\mathbb{C}\setminus \{1\}$ and satisfies the above equation 
  must be equal to our Hurwitz $\zeta$ function.
›
definition hurwitz_zeta :: "real  complex  complex" where
  "hurwitz_zeta a s = (if s = 1 then 0 else pre_zeta a s + of_real a powr (1 - s) / (s - 1))"

text ‹
  The Riemann $\zeta$ function is simply the Hurwitz $\zeta$ function with $a = 1$.
›
definition zeta :: "complex  complex" where
  "zeta = hurwitz_zeta 1"


text ‹
  We define the $\zeta$ functions as 0 at their poles. To avoid confusion, these facts
  are not added as simplification rules by default.
›
lemma hurwitz_zeta_1: "hurwitz_zeta c 1 = 0"
  by (simp add: hurwitz_zeta_def)

lemma zeta_1: "zeta 1 = 0"
  by (simp add: zeta_def hurwitz_zeta_1)

lemma zeta_minus_pole_eq: "s  1  zeta s - 1 / (s - 1) = pre_zeta 1 s"
  by (simp add: zeta_def hurwitz_zeta_def)


context
begin

private lemma holomorphic_pre_zeta_aux':
  assumes "a > 0" "bounded U" "open U" "U  {s. Re s > σ}" and σ: "σ > - 2 * real n"
  shows   "pre_zeta_aux n a holomorphic_on U" unfolding pre_zeta_aux_def
proof (intro holomorphic_intros)
  define C :: real where "C = max 0 (Sup ((λs. norm (pochhammer s (Suc (2 * n)))) ` closure U))"
  have "compact (closure U)" 
    using assms by (auto simp: compact_eq_bounded_closed)
  hence "compact ((λs. norm (pochhammer s (Suc (2 * n)))) ` closure U)"
    by (rule compact_continuous_image [rotated]) (auto intro!: continuous_intros)
  hence "bounded ((λs. norm (pochhammer s (Suc (2 * n)))) ` closure U)"
    by (simp add: compact_eq_bounded_closed)
  hence C: "cmod (pochhammer s (Suc (2 * n)))  C" if "s  U" for s
    using that closure_subset[of U] unfolding C_def 
    by (intro max.coboundedI2 cSup_upper bounded_imp_bdd_above) (auto simp: image_iff)
  have C' [simp]: "C  0" by (simp add: C_def)

  let ?g = "λ(x::real). C * (x + a) powr (- 1 - 2 * of_nat n - σ)"
  let ?G = "λ(x::real). C / (- 2 * of_nat n - σ) * (x + a) powr (- 2 * of_nat n - σ)"  
  define poch' where "poch' = deriv (λz::complex. pochhammer z (Suc (2 * n)))"
  have [derivative_intros]:
    "((λz. pochhammer z (Suc (2 * n))) has_field_derivative poch' z) (at z within A)" 
    for z :: complex and A unfolding poch'_def
    by (rule holomorphic_derivI [OF holomorphic_pochhammer [of _ UNIV]]) auto
  have A: "continuous_on A poch'" for A unfolding poch'_def 
    by (rule continuous_on_subset[OF _ subset_UNIV], 
        intro holomorphic_on_imp_continuous_on holomorphic_deriv)
        (auto intro: holomorphic_pochhammer) 
  note [continuous_intros] = continuous_on_compose2[OF this _ subset_UNIV]

  define f' where "f' = (λz t. - (poch' z * complex_of_real (t + a) powr (- 1 - 2 * of_nat n - z) -
                          Ln (complex_of_real (t + a)) * complex_of_real (t + a) powr 
                            (- 1 - 2 * of_nat n - z) * pochhammer z (Suc (2 * n))))"

  show "(λz. EM_remainder (Suc (2 * n)) (λx. - (pochhammer z (Suc (2 * n)) *
                  complex_of_real (x + a) powr (- 1 - 2 * of_nat n - z))) 0) holomorphic_on
    U" unfolding pre_zeta_aux_def
  proof (rule holomorphic_EM_remainder[of _ ?G ?g _ _ f'], goal_cases)
    case (1 x)
    show ?case
      by (insert 1 σ a > 0, rule derivative_eq_intros refl | simp)+
         (auto simp: field_simps powr_diff powr_add powr_minus)
  next
    case (2 z t x)
    note [derivative_intros] = has_field_derivative_powr_right [THEN DERIV_chain2]
    show ?case
      by (insert 2 σ a > 0, (rule derivative_eq_intros refl | (simp add: add_eq_0_iff; fail))+)
         (simp add: f'_def)
  next
    case 3
    hence *: "complex_of_real x + complex_of_real a  0" if "x  0" for x
      using nonpos_Reals_of_real_iff[of "x+a", unfolded of_real_add] that a > 0 by auto
    show ?case using a > 0 and * unfolding f'_def
      by (auto simp: case_prod_unfold add_eq_0_iff intro!: continuous_intros)
  next
    case (4 b c z e)
    have "- 2 * real n < σ" by (fact σ)
    also from 4 assms have "σ < Re z" by auto
    finally show ?case using assms 4
      by (intro integrable_continuous_real continuous_intros) (auto simp: add_eq_0_iff)
  next
    case (5 t x s)
    thus ?case using a > 0
      by (intro integrable_EM_remainder') (auto intro!: continuous_intros simp: add_eq_0_iff)
  next
    case 6
    from σ have "(λy. C / (-2 * real n - σ) * (a + y) powr (-2 * real n - σ))  0"
      by (intro tendsto_mult_right_zero tendsto_neg_powr
            filterlim_real_sequentially filterlim_tendsto_add_at_top [OF tendsto_const]) auto
    thus ?case unfolding convergent_def by (auto simp: add_ac)
  next
    case 7
    show ?case 
    proof (intro eventually_mono [OF eventually_ge_at_top[of 1]] ballI)
      fix x :: real and s :: complex assume x: "x  1" and s: "s  U"
      have "norm (- (pochhammer s (Suc (2 * n)) * of_real (x + a) powr (- 1 - 2 * of_nat n - s))) =
              norm (pochhammer s (Suc (2 * n))) * (x + a) powr (-1 - 2 * of_nat n - Re s)"
        (is "?N = _") using 7 a > 0 x by (simp add: norm_mult norm_powr_real_powr)
      also have "  ?g x"
        using 7 assms x s a > 0 by (intro mult_mono C powr_mono) auto
      finally show "?N  ?g x" .
    qed
  qed (insert assms, auto)
qed (insert assms, auto)

lemma analytic_pre_zeta_aux:
  assumes "a > 0"
  shows   "pre_zeta_aux n a analytic_on {s. Re s > - 2 * real n}"
  unfolding analytic_on_def
proof
  fix s assume s: "s  {s. Re s > - 2 * real n}"
  define σ where "σ = (Re s - 2 * real n) / 2"
  with s have σ: "σ > - 2 * real n" 
    by (simp add: σ_def field_simps)
  from s have s': "s  {s. Re s > σ}"
    by (auto simp: σ_def field_simps)

  have "open {s. Re s > σ}"
    by (rule open_halfspace_Re_gt)
  with s' obtain ε where "ε > 0" "ball s ε  {s. Re s > σ}"
    unfolding open_contains_ball by blast
  with σ have "pre_zeta_aux n a holomorphic_on ball s ε"
    by (intro holomorphic_pre_zeta_aux' [OF assms, of _ σ]) auto
  with ε > 0 show "e>0. pre_zeta_aux n a holomorphic_on ball s e"
    by blast
qed
end

context
  fixes s :: complex and N :: nat and ζ :: "complex  complex" and a :: real
  assumes s: "Re s > 1" and a: "a > 0"
  defines "ζ  (λs. n. (of_nat n + of_real a) powr -s)"
begin

interpretation ζ: euler_maclaurin_nat'
  "λx. of_real (x + a) powr (1 - s) / (1 - s)" "λx. of_real (x + a) powr -s" 
  "λn x. (-1) ^ n * pochhammer s n * of_real (x + a) powr -(s + n)" 
  0 N "ζ s" "{}"
proof (standard, goal_cases)
  case 2
  show ?case by (simp add: powr_minus field_simps)
next
  case (3 k)
  have "complex_of_real x + complex_of_real a = 0  x = -a" for x
    by (simp only: of_real_add [symmetric] of_real_eq_0_iff add_eq_0_iff2)
  with a s show ?case
    by (intro continuous_intros) (auto simp: add_nonneg_nonneg)
next
  case (4 k x)
  with a have "0 < x + a" by simp
  hence *: "complex_of_real x + complex_of_real a  0"
    using nonpos_Reals_of_real_iff[of "x+a", unfolded of_real_add] by auto
  have **: "pochhammer z (Suc n) = - pochhammer z n * (-z - of_nat n :: complex)" for z n
    by (simp add: pochhammer_rec' field_simps)
  show "((λx. (- 1) ^ k * pochhammer s k * of_real (x + a) powr - (s + of_nat k)) 
          has_vector_derivative (- 1) ^ Suc k * pochhammer s (Suc k) *
            of_real (x + a) powr - (s + of_nat (Suc k))) (at x)"
    by (insert 4 *, (rule has_vector_derivative_real_field derivative_eq_intros refl | simp)+)
       (auto simp: divide_simps powr_add powr_diff powr_minus **)
next
  case 5
  with s a show ?case 
    by (auto intro!: continuous_intros simp: minus_equation_iff add_eq_0_iff)
next
  case (6 x)
  with a have "0 < x + a" by simp
  hence *: "complex_of_real x + complex_of_real a  0"
    using nonpos_Reals_of_real_iff[of "x+a", unfolded of_real_add] by auto
  show ?case unfolding of_real_add
    by (insert 6 s *, (rule has_vector_derivative_real_field derivative_eq_intros refl | 
          force simp add: minus_equation_iff)+)
next
  case 7
  from s a have "(λk. (of_nat k + of_real a) powr -s) sums ζ s"
    unfolding ζ_def by (intro summable_sums summable_hurwitz_zeta) auto
  hence 1: "(λb. (k=0..b. (of_nat k + of_real a) powr -s))  ζ s"
    by (simp add: sums_def')

  {
    fix z assume "Re z < 0"
    hence "((λb. (a + real b) powr Re z)  0) at_top"
      by (intro tendsto_neg_powr filterlim_tendsto_add_at_top filterlim_real_sequentially) auto    
    also have "(λb. (a + real b) powr Re z) = (λb. norm ((of_nat b + a) powr z))"
      using a by (subst norm_powr_real_powr) (auto simp: add_ac)
    finally have "((λb. (of_nat b + a) powr z)  0) at_top" 
      by (subst (asm) tendsto_norm_zero_iff) simp
  } note * = this
  have "(λb. (of_nat b + a) powr (1 - s) / (1 - s))  0 / (1 - s)"
    using s by (intro tendsto_divide tendsto_const *) auto
  hence 2: "(λb. (of_nat b + a) powr (1 - s) / (1 - s))  0"
    by simp

  have "(λb. (i<2 * N + 1. (bernoulli' (Suc i) / fact (Suc i)) *R
             ((- 1) ^ i * pochhammer s i * (of_nat b + a) powr -(s + of_nat i))))
           (i<2 * N + 1. (bernoulli' (Suc i) / fact (Suc i)) *R 
                   ((- 1) ^ i * pochhammer s i * 0))"
    using s by (intro tendsto_intros *) auto
  hence 3: "(λb. (i<2 * N + 1. (bernoulli' (Suc i) / fact (Suc i)) *R
              ((- 1) ^ i * pochhammer s i * (of_nat b + a) powr -(s + of_nat i))))  0" 
    by simp

  from tendsto_diff[OF tendsto_diff[OF 1 2] 3]
  show ?case by simp
qed simp_all

text ‹
  The pre-$\zeta$ functions agree with the infinite sum that is used to define the $\zeta$
  function for $\mathfrak{R}(s)>1$.
›
lemma pre_zeta_aux_conv_zeta:
  "pre_zeta_aux N a s = ζ s + a powr (1 - s) / (1 - s)"
proof -
  let ?R = "(i=1..N. ((bernoulli (2*i) / fact (2*i)) *R pochhammer s (2*i - 1) * of_real a powr (-s - (2*i-1))))"
  let ?S = "EM_remainder (Suc (2 * N)) (λx. - (pochhammer s (Suc (2*N)) *
              of_real (x + a) powr (- 1 - 2 * of_nat N - s))) 0"
  from ζ.euler_maclaurin_strong_nat'[OF le_refl, simplified]
  have "of_real a powr -s = a powr (1 - s) / (1 - s) + ζ s + a powr -s / 2 + (-?R) - ?S"
    unfolding sum_negf [symmetric] by (simp add: scaleR_conv_of_real pre_zeta_aux_def mult_ac)
  thus ?thesis unfolding pre_zeta_aux_def 
    (* TODO: Field_as_Ring causes some problems with field_simps vs. div_mult_self *)
    by (simp add: field_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
qed

end


text ‹
  Since all of the partial pre-$\zeta$ functions are analytic and agree in the halfspace with 
  $\mathfrak R(s)>0$, they must agree in their entire domain.
›
lemma pre_zeta_aux_eq:
  assumes "m  n" "a > 0" "Re s > -2 * real m"
  shows   "pre_zeta_aux m a s = pre_zeta_aux n a s"
proof -
  have "pre_zeta_aux n a s - pre_zeta_aux m a s = 0"
  proof (rule analytic_continuation[of "λs. pre_zeta_aux n a s - pre_zeta_aux m a s"])
    show "(λs. pre_zeta_aux n a s - pre_zeta_aux m a s) holomorphic_on {s. Re s > -2 * real m}"
      using assms by (intro holomorphic_intros analytic_imp_holomorphic 
                        analytic_on_subset[OF analytic_pre_zeta_aux]) auto
  next
    fix s assume "s  {s. Re s > 1}"
    with a > 0 show "pre_zeta_aux n a s - pre_zeta_aux m a s = 0"
      by (simp add: pre_zeta_aux_conv_zeta)
  next
    have "2  {s. Re s > 1}" by simp
    also have " = interior "
      by (intro interior_open [symmetric] open_halfspace_Re_gt)
    finally show "2 islimpt {s. Re s > 1}"
      by (rule interior_limit_point)
  next
    show "connected {s. Re s > -2 * real m}"
      using convex_halfspace_gt[of "-2 * real m" "1::complex"]
      by (intro convex_connected) auto
  qed (insert assms, auto simp: open_halfspace_Re_gt)
  thus ?thesis by simp
qed

lemma pre_zeta_aux_eq':
  assumes "a > 0" "Re s > -2 * real m" "Re s > -2 * real n"
  shows   "pre_zeta_aux m a s = pre_zeta_aux n a s"
proof (cases m n rule: linorder_cases)
  case less
  with assms show ?thesis by (intro pre_zeta_aux_eq) auto
next
  case greater
  with assms show ?thesis by (subst eq_commute, intro pre_zeta_aux_eq) auto
qed auto

lemma pre_zeta_aux_eq_pre_zeta:
  assumes "Re s > -2 * real n" and "a > 0"
  shows   "pre_zeta_aux n a s = pre_zeta a s"
  unfolding pre_zeta_def
proof (intro pre_zeta_aux_eq')
  from assms show "- 2 * real (nat (1 - Re s / 2)) < Re s"
    by linarith
qed (insert assms, simp_all)

text ‹
  This means that the idea of iterating that construction infinitely does yield
  a well-defined entire function.
›
lemma analytic_pre_zeta: 
  assumes "a > 0"
  shows   "pre_zeta a analytic_on A"
  unfolding analytic_on_def
proof
  fix s assume "s  A"
  let ?B = "{s'. Re s' > of_int Re s - 1}"
  have s: "s  ?B" by simp linarith?
  moreover have "open ?B" by (rule open_halfspace_Re_gt)
  ultimately obtain ε where ε: "ε > 0" "ball s ε  ?B"
    unfolding open_contains_ball by blast
  define C where "C = ball s ε"

  note analytic = analytic_on_subset[OF analytic_pre_zeta_aux]
  have "pre_zeta_aux (nat - Re s + 2) a holomorphic_on C"
  proof (intro analytic_imp_holomorphic analytic subsetI assms, goal_cases)
    case (1 w)
    with ε have "w  ?B" by (auto simp: C_def)
    thus ?case by (auto simp: ceiling_minus)
  qed
  also have "?this  pre_zeta a holomorphic_on C"
  proof (intro holomorphic_cong refl pre_zeta_aux_eq_pre_zeta assms)
    fix w assume "w  C"
    with ε have w: "w  ?B" by (auto simp: C_def)
    thus " - 2 * real (nat - Re s + 2) < Re w"
      by (simp add: ceiling_minus)
  qed
  finally show "e>0. pre_zeta a holomorphic_on ball s e"
    using ε > 0 unfolding C_def by blast
qed

lemma holomorphic_pre_zeta [holomorphic_intros]:
  "f holomorphic_on A  a > 0  (λz. pre_zeta a (f z)) holomorphic_on A"
  using holomorphic_on_compose [OF _ analytic_imp_holomorphic [OF analytic_pre_zeta], of f]
  by (simp add: o_def)

corollary continuous_on_pre_zeta:
  "a > 0  continuous_on A (pre_zeta a)"
  by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto

corollary continuous_on_pre_zeta' [continuous_intros]:
  "continuous_on A f  a > 0  continuous_on A (λx. pre_zeta a (f x))"
  using continuous_on_compose2 [OF continuous_on_pre_zeta, of a A f "f ` A"]
  by (auto simp: image_iff)

corollary continuous_pre_zeta [continuous_intros]:
  "a > 0  continuous (at s within A) (pre_zeta a)"
  by (rule continuous_within_subset[of _ UNIV])
     (insert continuous_on_pre_zeta[of a UNIV], 
      auto simp: continuous_on_eq_continuous_at open_Compl)

corollary continuous_pre_zeta' [continuous_intros]:
  "a > 0  continuous (at s within A) f 
     continuous (at s within A) (λs. pre_zeta a (f s))"
  using continuous_within_compose3[OF continuous_pre_zeta, of a s A f] by auto


text ‹
  It is now obvious that $\zeta$ is holomorphic everywhere except 1, where it has a 
  simple pole with residue 1, which we can simply read off.
›
theorem holomorphic_hurwitz_zeta: 
  assumes "a > 0" "1  A"
  shows   "hurwitz_zeta a holomorphic_on A"
proof -
  have "(λs. pre_zeta a s + complex_of_real a powr (1 - s) / (s - 1)) holomorphic_on A"
    using assms by (auto intro!: holomorphic_intros)
  also from assms have "?this  ?thesis"
    by (intro holomorphic_cong) (auto simp: hurwitz_zeta_def)
  finally show ?thesis .
qed

corollary holomorphic_hurwitz_zeta' [holomorphic_intros]:
  assumes "f holomorphic_on A" and "a > 0" and "z. z  A  f z  1"
  shows   "(λx. hurwitz_zeta a (f x)) holomorphic_on A"
proof -
  have "hurwitz_zeta a  f holomorphic_on A" using assms
    by (intro holomorphic_on_compose_gen[of _ _ _ "f ` A"] holomorphic_hurwitz_zeta assms) auto
  thus ?thesis by (simp add: o_def)
qed

theorem holomorphic_zeta: "1  A zeta holomorphic_on A"
  unfolding zeta_def by (auto intro: holomorphic_intros)

corollary holomorphic_zeta' [holomorphic_intros]:
  assumes "f holomorphic_on A" and "z. z  A  f z  1"
  shows   "(λx. zeta (f x)) holomorphic_on A"
  using assms unfolding zeta_def by (auto intro: holomorphic_intros)

corollary analytic_hurwitz_zeta: 
  assumes "a > 0" "1  A"
  shows   "hurwitz_zeta a analytic_on A"
proof -
  from assms(1) have "hurwitz_zeta a holomorphic_on -{1}"
    by (rule holomorphic_hurwitz_zeta) auto
  also have "?this  hurwitz_zeta a analytic_on -{1}"
    by (intro analytic_on_open [symmetric]) auto
  finally show ?thesis by (rule analytic_on_subset) (insert assms, auto)
qed

corollary analytic_zeta: "1  A  zeta analytic_on A"
  unfolding zeta_def by (rule analytic_hurwitz_zeta) auto

corollary continuous_on_hurwitz_zeta:
  "a > 0  1  A  continuous_on A (hurwitz_zeta a)"
  by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto

corollary continuous_on_hurwitz_zeta' [continuous_intros]:
  "continuous_on A f  a > 0  (x. x  A  f x  1)  
     continuous_on A (λx. hurwitz_zeta a (f x))"
  using continuous_on_compose2 [OF continuous_on_hurwitz_zeta, of a "f ` A" A f]
  by (auto simp: image_iff)

corollary continuous_on_zeta: "1  A  continuous_on A zeta"
  by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto

corollary continuous_on_zeta' [continuous_intros]:
  "continuous_on A f  (x. x  A  f x  1)  
     continuous_on A (λx. zeta (f x))"
  using continuous_on_compose2 [OF continuous_on_zeta, of "f ` A" A f]
  by (auto simp: image_iff)

corollary continuous_hurwitz_zeta [continuous_intros]:
  "a > 0  s  1  continuous (at s within A) (hurwitz_zeta a)"
  by (rule continuous_within_subset[of _ UNIV])
     (insert continuous_on_hurwitz_zeta[of a "-{1}"], 
      auto simp: continuous_on_eq_continuous_at open_Compl)

corollary continuous_hurwitz_zeta' [continuous_intros]:
  "a > 0  f s  1  continuous (at s within A) f 
     continuous (at s within A) (λs. hurwitz_zeta a (f s))"
  using continuous_within_compose3[OF continuous_hurwitz_zeta, of a f s A] by auto

corollary continuous_zeta [continuous_intros]:
  "s  1  continuous (at s within A) zeta"
  unfolding zeta_def by (intro continuous_intros) auto

corollary continuous_zeta' [continuous_intros]:
  "f s  1  continuous (at s within A) f  continuous (at s within A) (λs. zeta (f s))"
  unfolding zeta_def by (intro continuous_intros) auto

corollary field_differentiable_at_zeta:
  assumes "s  1"
  shows "zeta field_differentiable at s"
proof -
  have "zeta holomorphic_on (- {1})" using holomorphic_zeta by force
  moreover have "open (-{1} :: complex set)" by (intro open_Compl) auto
  ultimately show ?thesis using assms
    by (auto simp add: holomorphic_on_open open_halfspace_Re_gt open_Diff field_differentiable_def)
qed

theorem is_pole_hurwitz_zeta:
  assumes "a > 0"
  shows   "is_pole (hurwitz_zeta a) 1"
proof -
  from assms have "continuous_on UNIV (pre_zeta a)"
    by (intro holomorphic_on_imp_continuous_on analytic_imp_holomorphic analytic_pre_zeta)
  hence "isCont (pre_zeta a) 1"
    by (auto simp: continuous_on_eq_continuous_at)
  hence *: "pre_zeta a 1 pre_zeta a 1"
    by (simp add: isCont_def)
  from assms have "isCont (λs. complex_of_real a powr (1 - s)) 1"
    by (intro isCont_powr_complex) auto
  with assms have **: "(λs. complex_of_real a powr (1 - s)) 1 1" 
    by (simp add: isCont_def)
  have "(λs::complex. s - 1) 1 1 - 1" by (intro tendsto_intros)
  hence "filterlim (λs::complex. s - 1) (at 0) (at 1)"
    by (auto simp: filterlim_at eventually_at_filter)
  hence ***: "filterlim (λs :: complex. a powr (1 - s) / (s - 1)) at_infinity (at 1)"
    by (intro filterlim_divide_at_infinity [OF **]) auto
  have "is_pole (λs. pre_zeta a s + complex_of_real a powr (1 - s) / (s - 1)) 1"
    unfolding is_pole_def hurwitz_zeta_def by (rule tendsto_add_filterlim_at_infinity * ***)+
  also have "?this  ?thesis" unfolding is_pole_def
    by (intro filterlim_cong refl) (auto simp: eventually_at_filter hurwitz_zeta_def)
  finally show ?thesis .
qed

corollary is_pole_zeta: "is_pole zeta 1"
  unfolding zeta_def by (rule is_pole_hurwitz_zeta) auto

theorem zorder_hurwitz_zeta: 
  assumes "a > 0"
  shows   "zorder (hurwitz_zeta a) 1 = -1"
proof (rule zorder_eqI[of UNIV])
  fix w :: complex assume "w  UNIV" "w  1"
  thus "hurwitz_zeta a w = (pre_zeta a w * (w - 1) + a powr (1 - w)) * (w - 1) powr (of_int (-1))"
    apply (subst (1) powr_of_int)
    by (auto simp add: hurwitz_zeta_def field_simps)
qed (insert assms, auto intro!: holomorphic_intros)

corollary zorder_zeta: "zorder zeta 1 = - 1"
  unfolding zeta_def by (rule zorder_hurwitz_zeta) auto

theorem residue_hurwitz_zeta: 
  assumes "a > 0"
  shows   "residue (hurwitz_zeta a) 1 = 1"
proof -
  note holo = analytic_imp_holomorphic[OF analytic_pre_zeta]
  have "residue (hurwitz_zeta a) 1 = residue (λz. pre_zeta a z + a powr (1 - z) / (z - 1)) 1"
    by (intro residue_cong) (auto simp: eventually_at_filter hurwitz_zeta_def)
  also have " = residue (λz. a powr (1 - z) / (z - 1)) 1" using assms
    by (subst residue_add [of UNIV])
       (auto intro!: holomorphic_intros holo intro: residue_holo[of UNIV, OF _ _ holo])
  also have " = complex_of_real a powr (1 - 1)"
    using assms by (intro residue_simple [of UNIV]) (auto intro!: holomorphic_intros)
  also from assms have " = 1" by simp
  finally show ?thesis .
qed

corollary residue_zeta: "residue zeta 1 = 1"
  unfolding zeta_def by (rule residue_hurwitz_zeta) auto

lemma zeta_bigo_at_1: "zeta  O[at 1 within A](λx. 1 / (x - 1))"
proof -
  have "zeta  Θ[at 1 within A](λs. pre_zeta 1 s + 1 / (s - 1))"
    by (intro bigthetaI_cong) (auto simp: eventually_at_filter zeta_def hurwitz_zeta_def)
  also have "(λs. pre_zeta 1 s + 1 / (s - 1))  O[at 1 within A](λs. 1 / (s - 1))"
  proof (rule sum_in_bigo)
    have "continuous_on UNIV (pre_zeta 1)"
      by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto
    hence "isCont (pre_zeta 1) 1" by (auto simp: continuous_on_eq_continuous_at)
    hence "continuous (at 1 within A) (pre_zeta 1)"
      by (rule continuous_within_subset) auto
    hence "pre_zeta 1  O[at 1 within A](λ_. 1)"
      by (intro continuous_imp_bigo_1) auto
    also have ev: "eventually (λs. s  ball 1 1  s  1  s  A) (at 1 within A)"
      by (intro eventually_at_ball') auto
    have "(λ_. 1)  O[at 1 within A](λs. 1 / (s - 1))"
      by (intro landau_o.bigI[of 1] eventually_mono[OF ev]) 
         (auto simp: eventually_at_filter norm_divide dist_norm norm_minus_commute field_simps)
    finally show "pre_zeta 1  O[at 1 within A](λs. 1 / (s - 1))" .
  qed simp_all
  finally show ?thesis .
qed

theorem
  assumes "a > 0" "Re s > 1"
  shows hurwitz_zeta_conv_suminf: "hurwitz_zeta a s = (n. (of_nat n + of_real a) powr -s)"
  and   sums_hurwitz_zeta: "(λn. (of_nat n + of_real a) powr -s) sums hurwitz_zeta a s"
proof -
  from assms have [simp]: "s  1" by auto
  from assms have "hurwitz_zeta a s = pre_zeta_aux 0 a s + of_real a powr (1 - s) / (s - 1)"
    by (simp add: hurwitz_zeta_def pre_zeta_def)
  also from assms have "pre_zeta_aux 0 a s = (n. (of_nat n + of_real a) powr -s) + 
                          of_real a powr (1 - s) / (1 - s)"
    by (intro pre_zeta_aux_conv_zeta)
  also have " + a powr (1 - s) / (s - 1) = 
               (n. (of_nat n + of_real a) powr -s) + a powr (1 - s) * (1 / (1 - s) + 1 / (s - 1))"
    by (simp add: algebra_simps)
  also have "1 / (1 - s) + 1 / (s - 1) = 0" 
    by (simp add: divide_simps)
  finally show "hurwitz_zeta a s = (n. (of_nat n + of_real a) powr -s)" by simp
  moreover have "(λn. (of_nat n + of_real a) powr -s) sums (n. (of_nat n + of_real a) powr -s)"
    by (intro summable_sums summable_hurwitz_zeta assms)
  ultimately show "(λn. (of_nat n + of_real a) powr -s) sums hurwitz_zeta a s" 
    by simp
qed

corollary
  assumes "Re s > 1"
  shows zeta_conv_suminf: "zeta s = (n. of_nat (Suc n) powr -s)"
  and   sums_zeta: "(λn. of_nat (Suc n) powr -s) sums zeta s"
  using hurwitz_zeta_conv_suminf[of 1 s] sums_hurwitz_zeta[of 1 s] assms 
  by (simp_all add: zeta_def add_ac)

corollary
  assumes "n > 1"
  shows zeta_nat_conv_suminf: "zeta (of_nat n) = (k. 1 / of_nat (Suc k) ^ n)"
  and   sums_zeta_nat: "(λk. 1 / of_nat (Suc k) ^ n) sums zeta (of_nat n)"
proof -
  have "(λk. of_nat (Suc k) powr -of_nat n) sums zeta (of_nat n)"
    using assms by (intro sums_zeta) auto
  also have "(λk. of_nat (Suc k) powr -of_nat n) = (λk. 1 / of_nat (Suc k) ^ n :: complex)"
    by (simp add: powr_minus divide_simps del: of_nat_Suc)
  finally show "(λk. 1 / of_nat (Suc k) ^ n) sums zeta (of_nat n)" .
  thus "zeta (of_nat n) = (k. 1 / of_nat (Suc k) ^ n)" by (simp add: sums_iff)
qed

lemma pre_zeta_aux_cnj [simp]: 
  assumes "a > 0"
  shows   "pre_zeta_aux n a (cnj z) = cnj (pre_zeta_aux n a z)"
proof -
  have "cnj (pre_zeta_aux n a z) = 
          of_real a powr -cnj z / 2 + (x=1..n. (bernoulli (2 * x) / fact (2 * x)) *R
            a powr (-cnj z - (2*x-1)) * pochhammer (cnj z) (2*x-1)) + EM_remainder (2*n+1)
          (λx. -(pochhammer (cnj z) (Suc (2 * n)) * 
                  cnj (of_real (x + a) powr (-1 - 2 * of_nat n - z)))) 0"
    (is "_ = _ + ?A + ?B") unfolding pre_zeta_aux_def complex_cnj_add using assms
    by (subst EM_remainder_cnj [symmetric]) 
       (auto intro!: continuous_intros simp: cnj_powr add_eq_0_iff mult_ac)
  also have "?B = EM_remainder (2*n+1)
        (λx. -(pochhammer (cnj z) (Suc (2 * n)) * of_real (x + a) powr (-1 - 2 * of_nat n - cnj z))) 0"
    using assms by (intro EM_remainder_cong) (auto simp: cnj_powr)
  also have "of_real a powr -cnj z / 2 + ?A +  = pre_zeta_aux n a (cnj z)"
    by (simp add: pre_zeta_aux_def mult_ac)
  finally show ?thesis ..
qed

lemma pre_zeta_cnj [simp]: "a > 0  pre_zeta a (cnj z) = cnj (pre_zeta a z)"
  by (simp add: pre_zeta_def)

lemma hurwitz_zeta_cnj [simp]: "a > 0  hurwitz_zeta a (cnj z) = cnj (hurwitz_zeta a z)"
proof -
  assume "a > 0"
  moreover have "cnj z = 1  z = 1" by (simp add: complex_eq_iff)
  ultimately show ?thesis by (auto simp: hurwitz_zeta_def cnj_powr)
qed

lemma zeta_cnj [simp]: "zeta (cnj z) = cnj (zeta z)"
  by (simp add: zeta_def)

corollary hurwitz_zeta_real: "a > 0  hurwitz_zeta a (of_real x)  "
  using hurwitz_zeta_cnj [of a "of_real x"] by (simp add: Reals_cnj_iff del: zeta_cnj)

corollary zeta_real: "zeta (of_real x)  "
  unfolding zeta_def by (rule hurwitz_zeta_real) auto

corollary zeta_real': "z    zeta z  "
  by (elim Reals_cases) (auto simp: zeta_real)


subsection ‹Connection to Dirichlet series›

lemma eval_fds_zeta: "Re s > 1  eval_fds fds_zeta s = zeta s"
  using sums_zeta [of s] by (intro eval_fds_eqI) (auto simp: powr_minus divide_simps)

theorem euler_product_zeta:
  assumes "Re s > 1"
  shows   "(λn. pn. if prime p then inverse (1 - 1 / of_nat p powr s) else 1)  zeta s"
  using euler_product_fds_zeta[of s] assms unfolding nat_power_complex_def 
  by (simp add: eval_fds_zeta)

corollary euler_product_zeta':
  assumes "Re s > 1"
  shows   "(λn. p | prime p  p  n. inverse (1 - 1 / of_nat p powr s))  zeta s"
proof -
  note euler_product_zeta [OF assms]
  also have "(λn. pn. if prime p then inverse (1 - 1 / of_nat p powr s) else 1) =
               (λn. p | prime p  p  n. inverse (1 - 1 / of_nat p powr s))"
    by (intro ext prod.mono_neutral_cong_right refl) auto
  finally show ?thesis .
qed

theorem zeta_Re_gt_1_nonzero: "Re s > 1  zeta s  0"
  using eval_fds_zeta_nonzero[of s] by (simp add: eval_fds_zeta)

theorem tendsto_zeta_Re_going_to_at_top: "(zeta  1) (Re going_to at_top)"
proof (rule Lim_transform_eventually)
  have "eventually (λx::real. x > 1) at_top"
    by (rule eventually_gt_at_top)
  hence "eventually (λs. Re s > 1) (Re going_to at_top)"
    by blast
  thus "eventually (λz. eval_fds fds_zeta z = zeta z) (Re going_to at_top)"
    by eventually_elim (simp add: eval_fds_zeta)
next
  have "conv_abscissa (fds_zeta :: complex fds)  1"
  proof (rule conv_abscissa_leI)
    fix c' assume "ereal c' > 1"
    thus "s. s  1 = c'  fds_converges fds_zeta (s::complex)"
      by (auto intro!: exI[of _ "of_real c'"])
  qed
  hence "(eval_fds fds_zeta  fds_nth fds_zeta 1) (Re going_to at_top)"
    by (intro tendsto_eval_fds_Re_going_to_at_top') auto
  thus "(eval_fds fds_zeta  1) (Re going_to at_top)" by simp
qed

lemma conv_abscissa_zeta [simp]: "conv_abscissa (fds_zeta :: complex fds) = 1"
  and abs_conv_abscissa_zeta [simp]: "abs_conv_abscissa (fds_zeta :: complex fds) = 1"
proof -
  let ?z = "fds_zeta :: complex fds"
  have A: "conv_abscissa ?z  1"
  proof (intro conv_abscissa_geI)
    fix c' assume "ereal c' < 1"
    hence "¬summable (λn. real n powr -c')"
      by (subst summable_real_powr_iff) auto
    hence "¬summable (λn. of_real (real n powr -c') :: complex)"
      by (subst summable_of_real_iff)
    also have "summable (λn. of_real (real n powr -c') :: complex)  
                 fds_converges fds_zeta (of_real c' :: complex)"
      unfolding fds_converges_def
      by (intro summable_cong eventually_mono [OF eventually_gt_at_top[of 0]])
         (simp add: fds_nth_zeta powr_Reals_eq powr_minus divide_simps)
    finally show "s::complex. s  1 = c'  ¬fds_converges fds_zeta s"
      by (intro exI[of _ "of_real c'"]) auto
  qed

  have B: "abs_conv_abscissa ?z  1"
  proof (intro abs_conv_abscissa_leI)
    fix c' assume "1 < ereal c'"
    thus "s::complex. s  1 = c'  fds_abs_converges fds_zeta s"
      by (intro exI[of _ "of_real c'"]) auto
  qed

  have "conv_abscissa ?z  abs_conv_abscissa ?z"
    by (rule conv_le_abs_conv_abscissa)
  also note B
  finally show "conv_abscissa ?z = 1" using A by (intro antisym)

  note A
  also have "conv_abscissa ?z  abs_conv_abscissa ?z"
    by (rule conv_le_abs_conv_abscissa)
  finally show "abs_conv_abscissa ?z = 1" using B by (intro antisym)
qed

theorem deriv_zeta_sums:
  assumes s: "Re s > 1"
  shows "(λn. -of_real (ln (real (Suc n))) / of_nat (Suc n) powr s) sums deriv zeta s"
proof -
  from s have "fds_converges (fds_deriv fds_zeta) s"
    by (intro fds_converges_deriv) simp_all
  with s have "(λn. -of_real (ln (real (Suc n))) / of_nat (Suc n) powr s) sums
                  deriv (eval_fds fds_zeta) s"
    unfolding fds_converges_altdef
    by (simp add: fds_nth_deriv scaleR_conv_of_real eval_fds_deriv eval_fds_zeta)
  also from s have "eventually (λs. s  {s. Re s > 1}) (nhds s)"
    by (intro eventually_nhds_in_open) (auto simp: open_halfspace_Re_gt)
  hence "eventually (λs. eval_fds fds_zeta s = zeta s) (nhds s)"
    by eventually_elim (auto simp: eval_fds_zeta)
  hence "deriv (eval_fds fds_zeta) s = deriv zeta s"
    by (intro deriv_cong_ev refl)
  finally show ?thesis .
qed

theorem inverse_zeta_sums:
  assumes s: "Re s > 1"
  shows   "(λn. moebius_mu (Suc n) / of_nat (Suc n) powr s) sums inverse (zeta s)"
proof -
  have "fds_converges (fds moebius_mu) s"
    using assms by (auto intro!: fds_abs_converges_moebius_mu)
  hence "(λn. moebius_mu (Suc n) / of_nat (Suc n) powr s) sums eval_fds (fds moebius_mu) s"
    by (simp add: fds_converges_altdef)
  also have "fds moebius_mu = inverse (fds_zeta :: complex fds)"
    by (rule fds_moebius_inverse_zeta)
  also from s have "eval_fds  s = inverse (zeta s)"
    by (subst eval_fds_inverse)
       (auto simp: fds_moebius_inverse_zeta [symmetric] eval_fds_zeta 
             intro!: fds_abs_converges_moebius_mu)
  finally show ?thesis .
qed

text ‹
  The following gives an extension of the $\zeta$ functions to the critical strip.
›
lemma hurwitz_zeta_critical_strip:
  fixes s :: complex and a :: real
  defines "S  (λn. i<n. (of_nat i + a) powr - s)"
  defines "I'  (λn. of_nat n powr (1 - s) / (1 - s))"
  assumes "Re s > 0" "s  1" and "a > 0"
  shows   "(λn. S n - I' n)  hurwitz_zeta a s"
proof -
  from assms have [simp]: "s  1" by auto
  let ?f = "λx. of_real (x + a) powr -s"
  let ?fs = "λn x. (-1) ^ n * pochhammer s n * of_real (x + a) powr (-s - of_nat n)"
  have minus_commute: "-a - b = -b - a" for a b :: complex by (simp add: algebra_simps)
  define I where "I = (λn. (of_nat n + a) powr (1 - s) / (1 - s))"
  define R where "R = (λn. EM_remainder' 1 (?fs 1) (real 0) (real n))"
  define R_lim where "R_lim = EM_remainder 1 (?fs 1) 0"
  define C where "C = - (a powr -s / 2)"
  define D where "D = (λn. (1/2) * (of_real (a + real n) powr - s))"
  define D' where "D' = (λn. of_real (a + real n) powr - s)"
  define C' where "C' = a powr (1 - s) / (1 - s)"
  define C'' where "C'' = of_real a powr - s"
  {
    fix n :: nat assume n: "n > 0"
    have "((λx. of_real (x + a) powr -s) has_integral (of_real (real n + a) powr (1-s) / (1 - s) - 
            of_real (0 + a) powr (1 - s) / (1 - s))) {0..real n}" using n assms 
      by (intro fundamental_theorem_of_calculus)
         (auto intro!: continuous_intros has_vector_derivative_real_field derivative_eq_intros
               simp: complex_nonpos_Reals_iff)
    hence I: "((λx. of_real (x + a) powr -s) has_integral (I n - C')) {0..n}"
      by (auto simp: divide_simps C'_def I_def)
    have "(i{0<..n}. ?f (real i)) - integral {real 0..real n} ?f =
            (k<1. (bernoulli' (Suc k) / fact (Suc k)) *R (?fs k (real n) - ?fs k (real 0))) + R n" 
      using n assms unfolding R_def
      by (intro euler_maclaurin_strong_raw_nat[where Y = "{0}"])
         (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_field
               simp: pochhammer_rec' algebra_simps complex_nonpos_Reals_iff add_eq_0_iff)
    also have "(k<1. (bernoulli' (Suc k) / fact (Suc k)) *R (?fs k (real n) - ?fs k (real 0))) = 
                  ((n + a) powr - s - a powr - s) / 2"
      by (simp add: lessThan_nat_numeral scaleR_conv_of_real numeral_2_eq_2 [symmetric])
    also have " = C + D n" by (simp add: C_def D_def field_simps)
    also have "integral {real 0..real n} (λx. complex_of_real (x + a) powr - s) = I n - C'"
      using I by (simp add: has_integral_iff)
    also have "(i{0<..n}. of_real (real i + a) powr - s) = 
                 (i=0..n. of_real (real i + a) powr - s) - of_real a powr -s"
      using assms by (subst sum.head) auto
    also have "(i=0..n. of_real (real i + a) powr - s) = S n + of_real (real n + a) powr -s"
      unfolding S_def by (subst sum.last_plus) (auto simp: atLeast0LessThan)
    finally have "C - C' + C'' - D' n + D n + R n + (I n - I' n) = S n - I' n"
      by (simp add: algebra_simps S_def D'_def C''_def)
  }
  hence ev: "eventually (λn. C - C' + C'' - D' n + D n + R n + (I n - I' n) = S n - I' n) at_top"
    by (intro eventually_mono[OF eventually_gt_at_top[of 0]]) auto

  have [simp]: "-1 - s = -s - 1" by simp
  {
    let ?C = "norm (pochhammer s 1)"
    have "R  R_lim" unfolding R_def R_lim_def of_nat_0
    proof (subst of_int_0 [symmetric], rule tendsto_EM_remainder)
      show "eventually (λx. norm (?fs 1 x)  ?C * (x + a) powr (-Re s - 1)) at_top"
        using eventually_ge_at_top[of 0]
        by eventually_elim (insert assms, auto simp: norm_mult norm_powr_real_powr)
    next
      fix x assume x: "x  real_of_int 0"
      have [simp]: "-numeral n - (x :: real) = -x - numeral n" for x n by (simp add: algebra_simps)
      show "((λx. ?C / (-Re s) * (x + a) powr (-Re s)) has_real_derivative 
              ?C * (x + a) powr (- Re s - 1)) (at x within {real_of_int 0..})"
        using assms x by (auto intro!: derivative_eq_intros)
    next
      have "(λy. ?C / (- Re s) * (a + real y) powr (- Re s))  0"
        by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_real_sequentially
                  filterlim_tendsto_add_at_top[OF tendsto_const]) (use assms in auto)
      thus "convergent (λy. ?C / (- Re s) * (real y + a) powr (- Re s))"
        by (auto simp: add_ac convergent_def)
    qed (intro integrable_EM_remainder' continuous_intros, insert assms, auto simp: add_eq_0_iff)
  }
  moreover have "(λn. I n - I' n)  0"
  proof -
    have "(λn. (complex_of_real (real n + a) powr (1 - s) - 
                 of_real (real n) powr (1 - s)) / (1 - s))  0 / (1 - s)" 
      using assms(3-5) by (intro filterlim_compose[OF _ filterlim_real_sequentially]
                             tendsto_divide complex_powr_add_minus_powr_asymptotics) auto
    thus "(λn. I n - I' n)  0" by (simp add: I_def I'_def divide_simps)
  qed
  ultimately have "(λn. C - C' + C'' - D' n + D n + R n + (I n - I' n)) 
                      C - C' + C'' - 0 + 0 + R_lim + 0"
    unfolding D_def D'_def using assms
    by (intro tendsto_add tendsto_diff tendsto_const tendsto_mult_right_zero
              tendsto_neg_powr_complex_of_real filterlim_tendsto_add_at_top 
              filterlim_real_sequentially) auto
  also have "C - C' + C'' - 0 + 0 + R_lim + 0 = 
               (a powr - s / 2) + a powr (1 - s) / (s - 1) + R_lim"
    by (simp add: C_def C'_def C''_def field_simps)
  also have " = hurwitz_zeta a s"
    using assms by (simp add: hurwitz_zeta_def pre_zeta_def pre_zeta_aux_def
                              R_lim_def scaleR_conv_of_real)
  finally have "(λn. C - C' + C'' - D' n + D n + R n + (I n - I' n))  hurwitz_zeta a s" .
  with ev show ?thesis
    by (blast intro: Lim_transform_eventually)
qed

lemma zeta_critical_strip:
  fixes s :: complex and a :: real
  defines "S  (λn. i=1..n. (of_nat i) powr - s)"
  defines "I  (λn. of_nat n powr (1 - s) / (1 - s))"
  assumes s: "Re s > 0" "s  1"
  shows   "(λn. S n - I n)  zeta s"
proof -
  from hurwitz_zeta_critical_strip[OF s zero_less_one]
    have "(λn. (i<n. complex_of_real (Suc i) powr - s) -
            of_nat n powr (1 - s) / (1 - s))  hurwitz_zeta 1 s" by (simp add: add_ac)
  also have "(λn. (i<n. complex_of_real (Suc i) powr -s)) = (λn. (i=1..n. of_nat i powr -s))"
    by (intro ext sum.reindex_bij_witness[of _ "λx. x - 1" Suc]) auto
  finally show ?thesis by (simp add: zeta_def S_def I_def)
qed


subsection ‹The non-vanishing of $\zeta$ for $\mathfrak{R}(s) \geq 1$›

text ‹
  This proof is based on a sketch by Newman~\cite{newman1998analytic}, which was previously
  formalised in HOL Light by Harrison~\cite{harrison2009pnt}, albeit in a much more concrete
  and low-level style.

  Our aim here is to reproduce Newman's proof idea cleanly and on the same high level of
  abstraction.
›
theorem zeta_Re_ge_1_nonzero:
  fixes s assumes "Re s  1" "s  1"
  shows "zeta s  0"
proof (cases "Re s > 1")
  case False
  define a where "a = -Im s"
  from False assms have s [simp]: "s = 1 - 𝗂 * a" and a: "a  0"
    by (auto simp: complex_eq_iff a_def)
  show ?thesis
  proof
    assume "zeta s = 0"
    hence zero: "zeta (1 - 𝗂 * a) = 0" by simp
    with zeta_cnj[of "1 - 𝗂 * a"] have zero': "zeta (1 + 𝗂 * a) = 0" by simp

    ― ‹We define the function $Q(s) = \zeta(s)^2\zeta(s+ia)\zeta(s-ia)$ and its Dirichlet series.
        The objective will be to show that this function is entire and its Dirichlet series
        converges everywhere. Of course, $Q(s)$ has singularities at $1$ and $1\pm ia$, so we 
        need to show they can be removed.›
    define Q Q_fds
      where "Q = (λs. zeta s ^ 2 * zeta (s + 𝗂 * a) * zeta (s - 𝗂 * a))"
        and "Q_fds = fds_zeta ^ 2 * fds_shift (𝗂 * a) fds_zeta * fds_shift (-𝗂 * a) fds_zeta"  
    let ?sings = "{1, 1 + 𝗂 * a, 1 - 𝗂 * a}"
 
    ― ‹We show that @{term Q} is locally bounded everywhere. This is the case because the
        poles of $\zeta(s)$ cancel with the zeros of $\zeta(s\pm ia)$ and vice versa.
        This boundedness is then enough to show that @{term Q} has only removable singularities.›
    have Q_bigo_1: "Q  O[at s](λ_. 1)" for s
    proof -
      have Q_eq: "Q = (λs. (zeta s * zeta (s + 𝗂 * a)) * (zeta s * zeta (s - 𝗂 * a)))"
        by (simp add: Q_def power2_eq_square mult_ac)

      ― ‹The singularity of $\zeta(s)$ at 1 gets cancelled by the zero of $\zeta(s-ia)$:›
      have bigo1: "(λs. zeta s * zeta (s - 𝗂 * a))  O[at 1](λ_. 1)"
        if "zeta (1 - 𝗂 * a) = 0" "a  0" for a :: real
      proof -
        have "(λs. zeta (s - 𝗂 * a) - zeta (1 - 𝗂 * a))  O[at 1](λs. s - 1)"
          using that
          by (intro taylor_bigo_linear holomorphic_on_imp_differentiable_at[of _ "-{1 + 𝗂 * a}"]
                    holomorphic_intros) (auto simp: complex_eq_iff)
        hence "(λs. zeta s * zeta (s - 𝗂 * a))  O[at 1](λs. 1 / (s - 1) * (s - 1))" 
          using that by (intro landau_o.big.mult zeta_bigo_at_1) simp_all
        also have "(λs. 1 / (s - 1) * (s - 1))  Θ[at 1](λ_. 1)"
          by (intro bigthetaI_cong) (auto simp: eventually_at_filter)
        finally show ?thesis .
      qed

      ― ‹The analogous result for $\zeta(s) \zeta(s+ia)$:›
      have bigo1': "(λs. zeta s * zeta (s + 𝗂 * a))  O[at 1](λ_. 1)"
        if "zeta (1 - 𝗂 * a) = 0" "a  0" for a :: real
        using bigo1[of  "-a"] that zeta_cnj[of "1 - 𝗂 * a"] by simp

      ― ‹The singularity of $\zeta(s-ia)$ gets cancelled by the zero of $\zeta(s)$:›
      have bigo2: "(λs. zeta s * zeta (s - 𝗂 * a))  O[at (1 + 𝗂 * a)](λ_. 1)"
        if "zeta (1 - 𝗂 * a) = 0" "a  0" for a :: real
      proof -
        have "(λs. zeta s * zeta (s - 𝗂 * a))  O[filtermap (λs. s + 𝗂 * a) (at 1)](λ_. 1)"
          using bigo1'[of a] that by (simp add: mult.commute landau_o.big.in_filtermap_iff)
        also have "filtermap (λs. s + 𝗂 * a) (at 1) = at (1 + 𝗂 * a)"
          using filtermap_at_shift[of "-𝗂 * a" 1] by simp
        finally show ?thesis .
      qed

      ― ‹Again, the analogous result for $\zeta(s) \zeta(s+ia)$:›
      have bigo2': "(λs. zeta s * zeta (s + 𝗂 * a))  O[at (1 - 𝗂 * a)](λ_. 1)"
        if "zeta (1 - 𝗂 * a) = 0" "a  0" for a :: real
        using bigo2[of "-a"] that zeta_cnj[of "1 - 𝗂 * a"] by simp

      ― ‹Now the final case distinction to show $Q(s)\in O(1)$ for all $s\in\mathbb{C}$:›
      consider "s = 1" | "s = 1 + 𝗂 * a" | "s = 1 - 𝗂 * a" | "s  ?sings" by blast
      thus ?thesis
      proof cases
        case 1
        thus ?thesis unfolding Q_eq using zero zero' a
          by (auto intro: bigo1 bigo1' landau_o.big.mult_in_1)
      next
        case 2
        from a have "isCont (λs. zeta s * zeta (s + 𝗂 * a)) (1 + 𝗂 * a)"
          by (auto intro!: continuous_intros)
        with 2 show ?thesis unfolding Q_eq using zero zero' a
          by (auto intro: bigo2 landau_o.big.mult_in_1 continuous_imp_bigo_1)
      next
        case 3
        from a have "isCont (λs. zeta s * zeta (s - 𝗂 * a)) (1 - 𝗂 * a)"
          by (auto intro!: continuous_intros)
        with 3 show ?thesis unfolding Q_eq using zero zero' a
          by (auto intro: bigo2' landau_o.big.mult_in_1 continuous_imp_bigo_1)
      qed (auto intro!: continuous_imp_bigo_1 continuous_intros simp: Q_def complex_eq_iff)
    qed
  
    ― ‹Thus, we can remove the singularities from @{term Q} and extend it to an entire function.›
    have "Q'. Q' holomorphic_on UNIV  (zUNIV - ?sings. Q' z = Q z)"
      by (intro removable_singularities Q_bigo_1)
         (auto simp: Q_def complex_eq_iff intro!: holomorphic_intros)
    then obtain Q' where Q': "Q' holomorphic_on UNIV" "z. z  ?sings  Q' z = Q z" by blast

    ― ‹@{term Q'} constitutes an analytic continuation of the Dirichlet series of @{term Q}.›
    have eval_Q_fds: "eval_fds Q_fds s = Q' s" if "Re s > 1" for s
    proof -
      have "eval_fds Q_fds s = Q s" using that
        by (simp add: Q_fds_def Q_def eval_fds_mult eval_fds_power fds_abs_converges_mult 
                      fds_abs_converges_power eval_fds_zeta)
      also from that have " = Q' s" by (subst Q') auto
      finally show ?thesis .
    qed
  
    ― ‹Since $\zeta(s)$ and $\zeta(s\pm ia)$ are completely multiplicative Dirichlet series,
        the logarithm of their product can be rewritten into the following nice form:›
    have ln_Q_fds_eq: 
      "fds_ln 0 Q_fds = fds (λk. of_real (2 * mangoldt k / ln k * (1 + cos (a * ln k))))"
    proof -
      note simps = fds_ln_mult[where l' = 0 and l'' = 0] fds_ln_power[where l' = 0]
                   fds_ln_prod[where l' = "λ_. 0"]
      have "fds_ln 0 Q_fds = 2 * fds_ln 0 fds_zeta + fds_shift (𝗂 * a) (fds_ln 0 fds_zeta) + 
                               fds_shift (-𝗂 * a) (fds_ln 0 fds_zeta)"
        by (auto simp: Q_fds_def simps)
      also have "completely_multiplicative_function (fds_nth (fds_zeta :: complex fds))"
        by standard auto
      hence "fds_ln (0 :: complex) fds_zeta = fds (λn. mangoldt n /R ln (real n))"
        by (subst fds_ln_completely_multiplicative) (auto simp: fds_eq_iff)
      also have "2 *  + fds_shift (𝗂 * a)  + fds_shift (-𝗂 * a)  = 
                   fds (λk. of_real (2 * mangoldt k / ln k * (1 + cos (a * ln k))))"
        (is "?a = ?b")
      proof (intro fds_eqI, goal_cases)
        case (1 n)
        then consider "n = 1" | "n > 1" by force
        hence "fds_nth ?a n = mangoldt n / ln (real n) * (2 + (n powr (𝗂 * a) + n powr (-𝗂 * a)))"
          by cases (auto simp: field_simps scaleR_conv_of_real numeral_fds)
        also have "n powr (𝗂 * a) + n powr (-𝗂 * a) = 2 * cos (of_real (a * ln n))"
          using 1 by (subst cos_exp_eq) (simp_all add: powr_def algebra_simps)
        also have "mangoldt n / ln (real n) * (2 + ) = 
                     of_real (2 * mangoldt n / ln n * (1 + cos (a * ln n)))"
          by (subst cos_of_real) simp_all
        finally show ?case by (simp add: fds_nth_fds')
      qed
      finally show ?thesis .
    qed
    ― ‹It is then obvious that this logarithm series has non-negative real coefficients.›
    also have "nonneg_dirichlet_series "
    proof (standard, goal_cases)
      case (1 n)
      from cos_ge_minus_one[of "a * ln n"] have "1 + cos (a * ln (real n))  0" by linarith
      thus ?case using 1
        by (cases "n = 0")
           (auto simp: complex_nonneg_Reals_iff fds_nth_fds' mangoldt_nonneg
                 intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
    qed
    ― ‹Therefore, the original series also has non-negative real coefficients.›
    finally have nonneg: "nonneg_dirichlet_series Q_fds"
      by (rule nonneg_dirichlet_series_lnD) (auto simp: Q_fds_def)
  
    ― ‹By the Pringsheim--Landau theorem, a Dirichlet series with non-negative coefficnets that 
        can be analytically continued to the entire complex plane must converge everywhere, i.\,e.\ 
        its abscissa of (absolute) convergence is $-\infty$:›
    have abscissa_Q_fds: "abs_conv_abscissa Q_fds  1"
      unfolding Q_fds_def by (auto intro!: abs_conv_abscissa_mult_leI abs_conv_abscissa_power_leI)
    with nonneg and eval_Q_fds and Q' holomorphic_on UNIV›
      have abscissa: "abs_conv_abscissa Q_fds = -"
        by (intro entire_continuation_imp_abs_conv_abscissa_MInfty[where c = 1 and g = Q'])
           (auto simp: one_ereal_def)
  
    ― ‹This now leads to a contradiction in a very obvious way. If @{term Q_fds} is
        absolutely convergent, then the subseries corresponding to powers of 2 (\i.e.
        we delete all summands $a_n / n ^ s$ where $n$ is not a power of 2 from the sum) is
        also absolutely convergent. We denote this series with $R$.›
    define R_fds where "R_fds = fds_primepow_subseries 2 Q_fds"
    have "conv_abscissa R_fds  abs_conv_abscissa R_fds" by (rule conv_le_abs_conv_abscissa)
    also have "abs_conv_abscissa R_fds  abs_conv_abscissa Q_fds"
      unfolding R_fds_def by (rule abs_conv_abscissa_restrict)
    also have " = -" by (simp add: abscissa)
    finally have abscissa': "conv_abscissa R_fds = -" by simp
  
    ― ‹Since $\zeta(s)$ and $\zeta(s \pm ia)$ have an Euler product expansion for 
        $\mathfrak{R}(s) > 1$, we have
          \[R(s) = (1 - 2^{-s})^-2 (1 - 2^{-s+ia})^{-1} (1 - 2^{-s-ia})^{-1}\]
        there, and since $R$ converges everywhere and the right-hand side is holomorphic for
        $\mathfrak{R}(s) > 0$, the equation is also valid for all $s$ with $\mathfrak{R}(s) > 0$
        by analytic continuation.›
    have eval_R: "eval_fds R_fds s = 
                   1 / ((1 - 2 powr -s) ^ 2 * (1 - 2 powr (-s + 𝗂 * a)) * (1 - 2 powr (-s - 𝗂 * a)))"
      (is "_ = ?f s") if "Re s > 0" for s
    proof -
      show ?thesis
      proof (rule analytic_continuation_open[where f = "eval_fds R_fds"])
        show "?f holomorphic_on {s. Re s > 0}"
          by (intro holomorphic_intros) (auto simp: powr_def exp_eq_1 Ln_Reals_eq)
      next
        fix z assume z: "z  {s. Re s > 1}"
        have [simp]: "completely_multiplicative_function (fds_nth fds_zeta)" by standard auto
        thus "eval_fds R_fds z = ?f z" using z
          by (simp add: R_fds_def Q_fds_def eval_fds_mult eval_fds_power fds_abs_converges_mult 
                fds_abs_converges_power fds_primepow_subseries_euler_product_cm divide_simps
                powr_minus powr_diff powr_add fds_abs_summable_zeta)
      qed (insert that abscissa', auto intro!: exI[of _ 2] convex_connected open_halfspace_Re_gt
                                               convex_halfspace_Re_gt holomorphic_intros)
    qed
  
    ― ‹We now clearly have a contradiction: $R(s)$, being entire, is continuous everywhere,
        while the function on the right-hand side clearly has a pole at $0$.›
    show False
    proof (rule not_tendsto_and_filterlim_at_infinity)
      have "((λb. (1-2 powr - b)2 * (1 - 2 powr (-b+𝗂*a)) * (1 - 2 powr (-b-𝗂*a)))  0) 
              (at 0 within {s. Re s > 0})"
        (is "filterlim ?f' _ _") by (intro tendsto_eq_intros) (auto)
      moreover have "eventually (λs. s  {s. Re s > 0}) (at 0 within {s. Re s > 0})"
        by (auto simp: eventually_at_filter)
      hence "eventually (λs. ?f' s  0) (at 0 within {s. Re s > 0})"
        by eventually_elim (auto simp: powr_def exp_eq_1 Ln_Reals_eq)
      ultimately have "filterlim ?f' (at 0) (at 0 within {s. Re s > 0})" by (simp add: filterlim_at)
      hence "filterlim ?f at_infinity (at 0 within {s. Re s > 0})" (is ?lim)
        by (intro filterlim_divide_at_infinity[OF tendsto_const]
                     tendsto_mult_filterlim_at_infinity) auto
      also have ev: "eventually (λs. Re s > 0) (at 0 within {s. Re s > 0})"
        by (auto simp: eventually_at intro!: exI[of _ 1])
      have "?lim  filterlim (eval_fds R_fds) at_infinity (at 0 within {s. Re s > 0})"
        by (intro filterlim_cong refl eventually_mono[OF ev]) (auto simp: eval_R)
      finally show  .
    next
      have "continuous (at 0 within {s. Re s > 0}) (eval_fds R_fds)"
        by (intro continuous_intros) (auto simp: abscissa')
      thus "((eval_fds R_fds  eval_fds R_fds 0)) (at 0 within {s. Re s > 0})"
        by (auto simp: continuous_within)
    next
      have "0  {s. Re s  0}" by simp
      also have "{s. Re s  0} = closure {s. Re s > 0}"
        using closure_halfspace_gt[of "1::complex" 0] by (simp add: inner_commute)
      finally have "0  " .
      thus "at 0 within {s. Re s > 0}  bot"
        by (subst at_within_eq_bot_iff) auto
    qed
  qed
qed (fact zeta_Re_gt_1_nonzero)


subsection ‹Special values of the $\zeta$ functions›

theorem hurwitz_zeta_neg_of_nat: 
  assumes "a > 0"
  shows   "hurwitz_zeta a (-of_nat n) = -bernpoly (Suc n) a / of_nat (Suc n)"
proof -
  have "-of_nat n  (1::complex)" by (simp add: complex_eq_iff)
  hence "hurwitz_zeta a (-of_nat n) = 
           pre_zeta a (-of_nat n) + a powr real (Suc n) / (-of_nat (Suc n))"
    unfolding zeta_def hurwitz_zeta_def using assms by (simp add: powr_of_real [symmetric])
  also have "a powr real (Suc n) / (-of_nat (Suc n)) = - (a powr real (Suc n) / of_nat (Suc n))"
    by (simp add: divide_simps del: of_nat_Suc)
  also have "a powr real (Suc n) = a ^ Suc n"
    using assms by (intro powr_realpow)
  also have "pre_zeta a (-of_nat n) = pre_zeta_aux (Suc n) a (- of_nat n)"
    using assms by (intro pre_zeta_aux_eq_pre_zeta [symmetric]) auto
  also have " = of_real a powr of_nat n / 2 +
                    (i = 1..Suc n. (bernoulli (2 * i) / fact (2 * i)) *R
                       (pochhammer (- of_nat n) (2 * i - 1) *
                       of_real a powr (of_nat n - of_nat (2 * i - 1)))) +
                    EM_remainder (Suc (2 * Suc n)) (λx. - (pochhammer (- of_nat n)
                      (2*n+3) * of_real (x + a) powr (- of_nat n - 3))) 0"
    (is "_ = ?B + sum (λn. ?f (2 * n)) _ + _") 
    unfolding pre_zeta_aux_def by (simp add: add_ac eval_nat_numeral)
  also have "?B = of_real (a ^ n) / 2" 
    using assms by (subst powr_Reals_eq) (auto simp: powr_realpow)
  also have "pochhammer (-of_nat n :: complex) (2*n+3) = 0"
    by (subst pochhammer_eq_0_iff) auto
  finally have "hurwitz_zeta a (-of_nat n) = 
                  - (a ^ Suc n / of_nat (Suc n)) + (a ^ n / 2 + sum (λn. ?f (2 * n)) {1..Suc n})"
    by simp

  also have "sum (λn. ?f (2 * n)) {1..Suc n} = sum ?f ((*) 2 ` {1..Suc n})"
    by (intro sum.reindex_bij_witness[of _ "λi. i div 2" "λi. 2*i"]) auto
  also have " = (i=2..2*n+2. ?f i)"
  proof (intro sum.mono_neutral_left ballI, goal_cases)
    case (3 i)
    hence "odd i" "i  1" by (auto elim!: evenE)
    thus ?case by (simp add: bernoulli_odd_eq_0)
  qed auto
  also have " = (i=2..Suc n. ?f i)"
  proof (intro sum.mono_neutral_right ballI, goal_cases)
    case (3 i)
    hence "pochhammer (-of_nat n :: complex) (i - 1) = 0"
      by (subst pochhammer_eq_0_iff) auto
    thus ?case by simp
  qed auto
  also have " = (i=Suc 1..Suc n. -of_real (real (Suc n choose i) * bernoulli i * 
                     a ^ (Suc n - i)) / of_nat (Suc n))"
    (is "sum ?lhs _ = sum ?f _")
  proof (intro sum.cong, goal_cases)
    case (2 i)
    hence "of_nat n - of_nat (i - 1) = (of_nat (Suc n - i) :: complex)"
      by (auto simp: of_nat_diff)
    also have "of_real a powr  = of_real (a ^ (Suc n - i))"
      using 2 assms by (subst powr_nat) auto
    finally have A: "of_real a powr (of_nat n - of_nat (i - 1)) = " .
    have "pochhammer (-of_nat n) (i - 1) = complex_of_real (pochhammer (-real n) (i - 1))"
      by (simp add: pochhammer_of_real [symmetric])
    also have "pochhammer (-real n) (i - 1) = pochhammer (-of_nat (Suc n)) i / (-1 - real n)"
      using 2 by (subst (2) pochhammer_rec_if) auto
    also have "-1 - real n = -real (Suc n)" by simp
    finally have B: "pochhammer (-of_nat n) (i - 1) = 
                    -complex_of_real (pochhammer (-real (Suc n)) i / real (Suc n))"
      by (simp del: of_nat_Suc)
    have "?lhs i = -complex_of_real (bernoulli i * pochhammer (-real (Suc n)) i / fact i * 
                      a ^ (Suc n - i)) / of_nat (Suc n)"
      by (simp only: A B) (simp add: scaleR_conv_of_real)
    also have "bernoulli i * pochhammer (-real (Suc n)) i / fact i =
                 (real (Suc n) gchoose i) * bernoulli i" using 2
      by (subst gbinomial_pochhammer) (auto simp: minus_one_power_iff bernoulli_odd_eq_0)
    also have "real (Suc n) gchoose i = Suc n choose i"
      by (subst binomial_gbinomial) auto
    finally show ?case by simp
  qed auto
  also have "a ^ n / 2 + sum ?f {Suc 1..Suc n} = sum ?f {1..Suc n}"
    by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: scaleR_conv_of_real del: of_nat_Suc)
  also have "-(a ^ Suc n / of_nat (Suc n)) + sum ?f {1..Suc n} = sum ?f {0..Suc n}"
    by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: scaleR_conv_of_real)
  also have " = - bernpoly (Suc n) a / of_nat (Suc n)"
    unfolding sum_negf sum_divide_distrib [symmetric] by (simp add: bernpoly_def atLeast0AtMost)
  finally show ?thesis .
qed

lemma hurwitz_zeta_0 [simp]: "a > 0  hurwitz_zeta a 0 = 1 / 2 - a"
  using hurwitz_zeta_neg_of_nat[of a 0] by (simp add: bernpoly_def)

lemma zeta_0 [simp]: "zeta 0 = -1 / 2"
  by (simp add: zeta_def)

theorem zeta_neg_of_nat: 
  "zeta (-of_nat n) = -of_real (bernoulli' (Suc n)) / of_nat (Suc n)"
  unfolding zeta_def by (simp add: hurwitz_zeta_neg_of_nat bernpoly_1')

corollary zeta_trivial_zero:
  assumes "even n" "n  0"
  shows   "zeta (-of_nat n) = 0"
  using zeta_neg_of_nat[of n] assms by (simp add: bernoulli'_odd_eq_0)

theorem zeta_even_nat: 
  "zeta (2 * of_nat n) = 
     of_real ((-1) ^ Suc n * bernoulli (2 * n) * (2 * pi) ^ (2 * n) / (2 * fact (2 * n)))"
proof (cases "n = 0")
  case False
  hence "(λk. 1 / of_nat (Suc k) ^ (2 * n)) sums zeta (of_nat (2 * n))"
    by (intro sums_zeta_nat) auto
  from sums_unique2 [OF this nat_even_power_sums_complex] False show ?thesis by simp
qed (insert zeta_neg_of_nat[of 0], simp_all)

corollary zeta_even_numeral: 
  "zeta (numeral (Num.Bit0 n)) = of_real
     ((- 1) ^ Suc (numeral n) * bernoulli (numeral (num.Bit0 n)) *
     (2 * pi) ^ numeral (num.Bit0 n) / (2 * fact (numeral (num.Bit0 n))))" (is "_ = ?rhs")
proof -
  have *: "(2 * numeral n :: nat) = numeral (Num.Bit0 n)"
    by (subst numeral.numeral_Bit0, subst mult_2, rule refl)
  have "numeral (Num.Bit0 n) = (2 * numeral n :: complex)"
    by (subst numeral.numeral_Bit0, subst mult_2, rule refl)
  also have " = 2 * of_nat (numeral n)" by (simp only: of_nat_numeral of_nat_mult)
  also have "zeta  = ?rhs" by (subst zeta_even_nat) (simp only: *)
  finally show ?thesis .
qed

corollary zeta_neg_even_numeral [simp]: "zeta (-numeral (Num.Bit0 n)) = 0"
proof -
  have "-numeral (Num.Bit0 n) = (-of_nat (numeral (Num.Bit0 n)) :: complex)"
    by simp
  also have "zeta  = 0"
  proof (rule zeta_trivial_zero)
    have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
      by (subst numeral.numeral_Bit0, subst mult_2, rule refl)
    also have "even " by (rule dvd_triv_left)
    finally show "even (numeral (Num.Bit0 n) :: nat)" .
  qed auto
  finally show ?thesis .
qed

corollary zeta_neg_numeral:
  "zeta (-numeral n) = 
     -of_real (bernoulli' (numeral (Num.inc n)) / numeral (Num.inc n))"
proof -
  have "-numeral n = (- of_nat (numeral n) :: complex)" 
    by simp
  also have "zeta  = -of_real (bernoulli' (numeral (Num.inc n)) / numeral (Num.inc n))"
    by (subst zeta_neg_of_nat) (simp add: numeral_inc)
  finally show ?thesis .
qed

corollary zeta_neg1: "zeta (-1) = - 1 / 12"
  using zeta_neg_of_nat[of 1] by (simp add: eval_bernoulli)

corollary zeta_neg3: "zeta (-3) = 1 / 120"
  by (simp add: zeta_neg_numeral)

corollary zeta_neg5: "zeta (-5) = - 1 / 252"
  by (simp add: zeta_neg_numeral)

corollary zeta_2: "zeta 2 = pi ^ 2 / 6"
  by (simp add: zeta_even_numeral)

corollary zeta_4: "zeta 4 = pi ^ 4 / 90"
  by (simp add: zeta_even_numeral fact_num_eq_if)

corollary zeta_6: "zeta 6 = pi ^ 6 / 945"
  by (simp add: zeta_even_numeral fact_num_eq_if)

corollary zeta_8: "zeta 8 = pi ^ 8 / 9450"
  by (simp add: zeta_even_numeral fact_num_eq_if)


subsection ‹Integral relation between $\Gamma$ and $\zeta$ function›

lemma
  assumes z: "Re z > 0" and a: "a > 0"
  shows   Gamma_hurwitz_zeta_aux_integral: 
            "Gamma z / (of_nat n + of_real a) powr z = 
               (s{0<..}. (s powr (z - 1) / exp ((n+a) * s)) lebesgue)"
    and   Gamma_hurwitz_zeta_aux_integrable:
            "set_integrable lebesgue {0<..} (λs. s powr (z - 1) / exp ((n+a) * s))"
proof -
  note integrable = absolutely_integrable_Gamma_integral' [OF z]
  let ?INT = "set_lebesgue_integral lebesgue {0<..} :: (real  complex)  complex"
  let ?INT' = "set_lebesgue_integral lebesgue {0<..} :: (real  real)  real"

  have meas1: "set_borel_measurable lebesgue {0<..} 
                 (λx. of_real x powr (z - 1) / of_real (exp ((n+a) * x)))"
    unfolding set_borel_measurable_def
    by (intro measurable_completion, subst measurable_lborel2, 
        intro borel_measurable_continuous_on_indicator) (auto intro!: continuous_intros)
  show integrable1: "set_integrable lebesgue {0<..} 
                       (λs. s powr (z - 1) / exp ((n+a) * s))"
    using assms by (intro absolutely_integrable_Gamma_integral) auto
  from assms have pos: "0 < real n + a" by (simp add: add_nonneg_pos)
  hence "complex_of_real 0  of_real (real n + a)" by (simp only: of_real_eq_iff)
  also have "complex_of_real (real n + a) = of_nat n + of_real a" by simp
  finally have nz: "  0" by auto

  have "((λt. complex_of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0<..}"
    by (rule Gamma_integral_complex') fact+
  hence "Gamma z = ?INT (λt. t powr (z - 1) / of_real (exp t))"
    using set_lebesgue_integral_eq_integral(2) [OF integrable] 
    by (simp add: has_integral_iff exp_of_real)
  also have "lebesgue = density (distr lebesgue lebesgue (λt. (real n+a) * t)) 
                          (λx. ennreal (real n+a))"
    using lebesgue_real_scale[of "real n + a"] pos by auto
  also have "set_lebesgue_integral  {0<..} (λt. of_real t powr (z - 1) / of_real (exp t)) = 
               set_lebesgue_integral (distr lebesgue lebesgue (λt. (real n + a) * t)) {0<..}
                 (λt. (real n + a) * t powr (z - 1) / exp t)" using integrable pos
    unfolding set_lebesgue_integral_def
    by (subst integral_density) (simp_all add: exp_of_real algebra_simps scaleR_conv_of_real set_integrable_def)
  also have " = ?INT (λs. (n + a) * (of_real (n+a) * of_real s) powr (z - 1) / 
                    of_real (exp ((n+a) * s)))"
    unfolding set_lebesgue_integral_def
  proof (subst integral_distr)
    show "(*) (real n + a)  lebesgue M lebesgue"
      using lebesgue_measurable_scaling[of "real n + a", where ?'a = real]
      unfolding real_scaleR_def .
  next
    have "(λx. (n+a) * (indicator {0<..} x *R (of_real x powr (z - 1) / of_real (exp x)))) 
              lebesgue M borel" 
      using integrable unfolding set_integrable_def by (intro borel_measurable_times) simp_all
    thus "(λx. indicator {0<..} x *R
           (complex_of_real (real n + a) * complex_of_real x powr (z - 1) / exp x))
     borel_measurable lebesgue" by simp
  qed (intro Bochner_Integration.integral_cong refl, insert pos, 
       auto simp: indicator_def zero_less_mult_iff)
  also have " = ?INT (λs. ((n+a) powr z) * (s powr (z - 1) / exp ((n+a) * s)))" using pos
    by (intro set_lebesgue_integral_cong refl allI impI, simp, subst powr_times_real)
       (auto simp: powr_diff)
  also have " = (n + a) powr z * ?INT (λs. s powr (z - 1) / exp ((n+a) * s))"
    unfolding set_lebesgue_integral_def
    by (subst integral_mult_right_zero [symmetric]) simp_all
  finally show "Gamma z / (of_nat n + of_real a) powr z = 
                  ?INT (λs. s powr (z - 1) / exp ((n+a) * s))" 
    using nz by (auto simp add: field_simps)
qed

lemma
  assumes x: "x > 0" and "a > 0"
  shows   Gamma_hurwitz_zeta_aux_integral_real: 
            "Gamma x / (real n + a) powr x = 
               set_lebesgue_integral lebesgue {0<..} 
               (λs. s powr (x - 1) / exp ((real n + a) * s))"
    and   Gamma_hurwitz_zeta_aux_integrable_real:
            "set_integrable lebesgue {0<..} (λs. s powr (x - 1) / exp ((real n + a) * s))"
proof -
  show "set_integrable lebesgue {0<..} (λs. s powr (x - 1) / exp ((real n + a) * s))"
    using absolutely_integrable_Gamma_integral[of "of_real x" "real n + a"]
    unfolding set_integrable_def
  proof (rule Bochner_Integration.integrable_bound, goal_cases)
    case 3
    have "set_integrable lebesgue {0<..} (λxa. complex_of_real xa powr (of_real x - 1) / 
              of_real (exp ((n + a) * xa)))"
      using assms by (intro Gamma_hurwitz_zeta_aux_integrable) auto
    also have "?this  integrable lebesgue
                 (λs. complex_of_real (indicator {0<..} s *R (s powr (x - 1) / (exp ((n+a) * s)))))"
      unfolding set_integrable_def
      by (intro Bochner_Integration.integrable_cong refl) (auto simp: powr_Reals_eq indicator_def)
    finally have "set_integrable lebesgue {0<..} (λs. s powr (x - 1) / exp ((n+a) * s))"
      unfolding set_integrable_def complex_of_real_integrable_eq .
    thus ?case
      by (simp add: set_integrable_def)
  qed (insert assms, auto intro!: AE_I2 simp: indicator_def norm_divide norm_powr_real_powr)
  from Gamma_hurwitz_zeta_aux_integral[of "of_real x" a n] and assms
    have "of_real (Gamma x / (real n + a) powr x) = set_lebesgue_integral lebesgue {0<..} 
            (λs. complex_of_real s powr (of_real x - 1) / of_real (exp ((n+a) * s)))" (is "_ = ?I")
      by (auto simp: Gamma_complex_of_real powr_Reals_eq)
  also have "?I = lebesgue_integral lebesgue
                    (λs. of_real (indicator {0<..} s *R (s powr (x - 1) / exp ((n+a) * s))))"
    unfolding set_lebesgue_integral_def
    using assms by (intro Bochner_Integration.integral_cong refl) 
                   (auto simp: indicator_def powr_Reals_eq)
  also have " = of_real (set_lebesgue_integral lebesgue {0<..} 
                    (λs. s powr (x - 1) / exp ((n+a) * s)))"
    unfolding set_lebesgue_integral_def
    by (rule Bochner_Integration.integral_complex_of_real)
  finally show "Gamma x / (real n + a) powr x = set_lebesgue_integral lebesgue {0<..} 
                  (λs. s powr (x - 1) / exp ((real n + a) * s))"
    by (subst (asm) of_real_eq_iff)
qed

theorem
  assumes "Re z > 1" and "a > (0::real)"
  shows   Gamma_times_hurwitz_zeta_integral: "Gamma z * hurwitz_zeta a z =
            (x{0<..}. (of_real x powr (z - 1) * of_real (exp (-a*x) / (1 - exp (-x)))) lebesgue)"
    and   Gamma_times_hurwitz_zeta_integrable:
            "set_integrable lebesgue {0<..} 
               (λx. of_real x powr (z - 1) * of_real (exp (-a*x) / (1 - exp (-x))))"
proof -
  from assms have z: "Re z > 0" by simp
  let ?INT = "set_lebesgue_integral lebesgue {0<..} :: (real  complex)  complex"
  let ?INT' = "set_lebesgue_integral lebesgue {0<..} :: (real  real)  real"

  have 1: "complex_set_integrable lebesgue {0<..} 
            (λx. of_real x powr (z - 1) / of_real (exp ((real n + a) * x)))" for n
      by (rule Gamma_hurwitz_zeta_aux_integrable) (use assms in simp_all)
  have 2: "summable (λn. norm (indicator {0<..} s *R (of_real s powr (z - 1) / 
             of_real (exp ((n + a) * s)))))" for s
  proof (cases "s > 0")
    case True
    hence "summable (λn. norm (of_real s powr (z - 1)) * exp (-a * s) * exp (-s) ^ n)"
      using assms by (intro summable_mult summable_geometric) simp_all
    with True show ?thesis
      by (simp add: norm_mult norm_divide exp_add exp_diff
                    exp_minus field_simps exp_of_nat_mult [symmetric])
  qed simp_all
  have 3: "summable (λn. x. norm (indicator {0<..} x *R (complex_of_real x powr (z - 1) /
                            complex_of_real (exp ((n + a) * x)))) lebesgue)"
  proof -
    have "summable (λn. Gamma (Re z) * (real n + a) powr -Re z)"
      using assms by (intro summable_mult summable_hurwitz_zeta_real) simp_all
    also have "?this  summable (λn. ?INT' (λs. norm (of_real s powr (z - 1) / 
                                       of_real (exp ((n+a) * s)))))"
    proof (intro summable_cong always_eventually allI, goal_cases)
      case (1 n)
      have "Gamma (Re z) * (real n + a) powr -Re z = Gamma (Re z) / (real n + a) powr Re z"
        by (subst powr_minus) (simp_all add: field_simps)
      also from assms have " = (x{0<..}. (x powr (Re z-1) / exp ((n+a) * x)) lebesgue)"
        by (subst Gamma_hurwitz_zeta_aux_integral_real) simp_all
      also have " = (xa{0<..}. norm (of_real xa powr (z-1) / of_real (exp ((n+a) * xa)))
                         lebesgue)"
        unfolding set_lebesgue_integral_def
        by (intro Bochner_Integration.integral_cong refl)
          (auto simp: indicator_def norm_divide norm_powr_real_powr)
      finally show ?case .
    qed
    finally show ?thesis
      by (simp add: set_lebesgue_integral_def)
  qed

  have sum_eq: "(n. indicator {0<..} s *R (of_real s powr (z - 1) / of_real (exp ((n+a) * s)))) = 
                   indicator {0<..} s *R (of_real s powr (z - 1) * 
                     of_real (exp (-a * s) / (1 - exp (-s))))" for s
  proof (cases "s > 0")
    case True
    hence "(n. indicator {0..} s *R (of_real s powr (z - 1) / of_real (exp ((n+a) * s)))) =
             (n. of_real s powr (z - 1) * of_real (exp (-a * s)) * of_real (exp (-s)) ^ n)"
      by (intro suminf_cong) 
         (auto simp: exp_add exp_minus exp_of_nat_mult [symmetric] field_simps of_real_exp)
    also have "(n. of_real s powr (z - 1) * of_real (exp (-a * s)) * of_real (exp (-s)) ^ n) =
                 of_real s powr (z - 1) * of_real (exp (-a * s)) * (n. of_real (exp (-s)) ^ n)"
      using True by (intro suminf_mult summable_geometric) simp_all
    also have "(n. complex_of_real (exp (-s)) ^ n) = 1 / (1 - of_real (exp (-s)))"
      using True by (intro suminf_geometric) auto
    also have "of_real s powr (z - 1) * of_real (exp (-a * s)) *  = 
                 of_real s powr (z - 1) * of_real (exp (-a * s) / (1 - exp (-s)))" using a > 0
      by (auto simp add: divide_simps exp_minus)
    finally show ?thesis using True by simp
  qed simp_all

  show "set_integrable lebesgue {0<..} 
          (λx. of_real x powr (z - 1) * of_real (exp (-a*x) / (1 - exp (-x))))"
    using 1 unfolding sum_eq [symmetric] set_integrable_def 
    by (intro integrable_suminf[OF _ AE_I2] 2 3)

  have "(λn. ?INT (λs. s powr (z - 1) / exp ((n+a) * s))) sums lebesgue_integral lebesgue
            (λs. n. indicator {0<..} s *R (s powr (z - 1) / exp ((n+a) * s)))" (is "?A sums ?B")
    using 1 unfolding set_lebesgue_integral_def set_integrable_def
    by (rule sums_integral[OF _ AE_I2[OF 2] 3])
  also have "?A = (λn. Gamma z * (n + a) powr -z)"
    using assms by (subst Gamma_hurwitz_zeta_aux_integral [symmetric]) 
                   (simp_all add: powr_minus divide_simps)
  also have "?B = ?INT (λs. of_real s powr (z - 1) * of_real (exp (-a * s) / (1 - exp (-s))))"
    unfolding sum_eq set_lebesgue_integral_def ..
  finally have "(λn. Gamma z * (of_nat n + of_real a) powr -z) sums
                  ?INT (λx. of_real x powr (z - 1) * of_real (exp (-a * x) / (1 - exp (-x))))" 
    by simp
  moreover have "(λn. Gamma z * (of_nat n + of_real a) powr -z) sums (Gamma z * hurwitz_zeta a z)"
    using assms by (intro sums_mult sums_hurwitz_zeta) simp_all
  ultimately show "Gamma z * hurwitz_zeta a z = 
                     (x{0<..}. (of_real x powr (z - 1) * 
                        of_real (exp (-a * x) / (1 - exp (-x)))) lebesgue)"
    by (rule sums_unique2 [symmetric])
qed

corollary
  assumes "Re z > 1"
  shows   Gamma_times_zeta_integral: "Gamma z * zeta z =
            (x{0<..}. (of_real x powr (z - 1) / of_real (exp x - 1)) lebesgue)" (is ?th1)
    and   Gamma_times_zeta_integrable:
            "set_integrable lebesgue {0<..} 
               (λx. of_real x powr (z - 1) / of_real (exp x - 1))" (is ?th2)
proof -
  have *: "(λx. indicator {0<..} x *R (of_real x powr (z - 1) * 
                of_real (exp (-x) / (1 - exp (-x))))) =
             (λx. indicator {0<..} x *R (of_real x powr (z - 1) / of_real (exp x - 1)))"
    by (intro ext) (simp add: field_simps exp_minus indicator_def)
  from Gamma_times_hurwitz_zeta_integral [OF assms zero_less_one] and *
    show ?th1 by (simp add: zeta_def set_lebesgue_integral_def)
  from Gamma_times_hurwitz_zeta_integrable [OF assms zero_less_one] and *
    show ?th2 by (simp add: zeta_def set_integrable_def)
qed

corollary hurwitz_zeta_integral_Gamma_def:
  assumes "Re z > 1" "a > 0"
  shows   "hurwitz_zeta a z = 
             rGamma z * (x{0<..}. (of_real x powr (z - 1) * 
               of_real (exp (-a * x) / (1 - exp (-x)))) lebesgue)"
proof -
  from assms have "Gamma z  0" 
    by (subst Gamma_eq_zero_iff) (auto elim!: nonpos_Ints_cases)
  with Gamma_times_hurwitz_zeta_integral [OF assms] show ?thesis
    by (simp add: rGamma_inverse_Gamma field_simps)
qed

corollary zeta_integral_Gamma_def:
  assumes "Re z > 1"
  shows   "zeta z =
             rGamma z * (x{0<..}. (of_real x powr (z - 1) / of_real (exp x - 1)) lebesgue)"
proof -
  from assms have "Gamma z  0" 
    by (subst Gamma_eq_zero_iff) (auto elim!: nonpos_Ints_cases)
  with Gamma_times_zeta_integral [OF assms] show ?thesis
    by (simp add: rGamma_inverse_Gamma field_simps)
qed

lemma Gamma_times_zeta_has_integral:
  assumes "Re z > 1"
  shows   "((λx. x powr (z - 1) / (of_real (exp x) - 1)) has_integral (Gamma z * zeta z)) {0<..}"
    (is "(?f has_integral _) _")
proof -
  have "(?f has_integral set_lebesgue_integral lebesgue {0<..} ?f) {0<..}"
    using Gamma_times_zeta_integrable[OF assms]
    by (intro has_integral_set_lebesgue) auto
  also have "set_lebesgue_integral lebesgue {0<..} ?f = Gamma z * zeta z"
    using Gamma_times_zeta_integral[OF assms] by simp
  finally show ?thesis .
qed

lemma Gamma_times_zeta_has_integral_real:
  fixes z :: real
  assumes "z > 1"
  shows   "((λx. x powr (z - 1) / (exp x - 1)) has_integral (Gamma z * Re (zeta z))) {0<..}"
proof -
  from assms have *: "Re (of_real z) > 1" by simp
  have "((λx. Re (complex_of_real x powr (complex_of_real z - 1)) / (exp x - 1)) has_integral
           Gamma z * Re (zeta (complex_of_real z))) {0<..}"
    using has_integral_linear[OF Gamma_times_zeta_has_integral[OF *] bounded_linear_Re] 
    by (simp add: o_def Gamma_complex_of_real)
  also have "?this  ?thesis"
    using assms by (intro has_integral_cong) (auto simp: powr_Reals_eq)
  finally show ?thesis .
qed

lemma Gamma_integral_real':
  assumes x: "x > (0 :: real)"
  shows   "((λt. t powr (x - 1) / exp t) has_integral Gamma x) {0<..}"
  using Gamma_integral_real[OF assms] by (subst has_integral_closure [symmetric]) auto


subsection ‹An analytic proof of the infinitude of primes›

text ‹
  We can now also do an analytic proof of the infinitude of primes.
›
lemma primes_infinite_analytic: "infinite {p :: nat. prime p}"
proof
  ― ‹Suppose the set of primes were finite.›
  define P :: "nat set" where "P = {p. prime p}"
  assume fin: "finite P"

  ― ‹Then the Euler product form of the $\zeta$ function ranges over a finite set,
      and since each factor is holomorphic in the positive real half-space, 
      the product is, too.›
  define zeta' :: "complex  complex" 
    where "zeta' = (λs. (pP. inverse (1 - 1 / of_nat p powr s)))"
  have holo: "zeta' holomorphic_on A" if "A  {s. Re s > 0}" for A
  proof -
    {
      fix p :: nat and s :: complex assume p: "p  P" and s: "s  A"
      from p have p': "real p > 1" 
        by (subst of_nat_1 [symmetric], subst of_nat_less_iff) (simp add: prime_gt_Suc_0_nat P_def)
      have "norm (of_nat p powr s) = real p powr Re s"
        by (simp add: norm_powr_real_powr)
      also have " > real p powr 0" using p p' s that
        by (subst powr_less_cancel_iff) (auto simp: prime_gt_1_nat)
      finally have "of_nat p powr s  1" using p by (auto simp: P_def)
    }
    thus ?thesis by (auto simp: zeta'_def P_def intro!: holomorphic_intros)
  qed

  ― ‹Since the Euler product expansion of $\zeta(s)$ is valid for all $s$ with
      real value at least 1, and both $\zeta(s)$ and the Euler product must 
      be equal in the positive real half-space punctured at 1 by analytic
      continuation.›
  have eq: "zeta s = zeta' s" if "Re s > 0" "s  1" for s
  proof (rule analytic_continuation_open[of "{s. Re s > 1}" "{s. Re s > 0} - {1}" zeta zeta'])
    fix s assume s: "s  {s. Re s > 1}"
    let ?f = "(λn. pn. if prime p then inverse (1 - 1 / of_nat p powr s) else 1)"
    have "eventually (λn. ?f n = zeta' s) sequentially"
      using eventually_ge_at_top[of "Max P"]
    proof eventually_elim
      case (elim n)
      have "P  {}" by (auto simp: P_def intro!: exI[of _ 2])
      with elim have "P  {..n}" using fin by auto
      thus ?case unfolding zeta'_def
        by (intro prod.mono_neutral_cong_right) (auto simp: P_def)
    qed
    moreover from s have "?f  zeta s" by (intro euler_product_zeta) auto
    ultimately have "(λ_. zeta' s)  zeta s"
      by (blast intro: Lim_transform_eventually)
    thus "zeta s = zeta' s" by (simp add: LIMSEQ_const_iff)
  qed (auto intro!: exI[of _ 2] open_halfspace_Re_gt connected_open_delete convex_halfspace_Re_gt 
         holomorphic_intros holo that intro: convex_connected)

  ― ‹However, since the Euler product is holomorphic on the entire positive real
      half-space, it cannot have a pole at 1, while $\zeta(s)$ does have a pole
      at 1. Since they are equal in the punctured neighbourhood of 1, this is
      a contradiction.›
  have ev: "eventually (λs. s  {s. Re s > 0} - {1}) (at 1)"
    by (auto simp: eventually_at_filter intro!: open_halfspace_Re_gt
               eventually_mono[OF eventually_nhds_in_open[of "{s. Re s > 0}"]])
  have "¬is_pole zeta' 1"
    by (rule not_is_pole_holomorphic [of "{s. Re s > 0}"]) (auto intro!: holo open_halfspace_Re_gt)
  also have "is_pole zeta' 1  is_pole zeta 1" unfolding is_pole_def
    by (intro filterlim_cong refl eventually_mono [OF ev] eq [symmetric]) auto
  finally show False using is_pole_zeta by contradiction
qed


subsection ‹The periodic zeta function›

text ‹
  The periodic zeta function $F(s, q)$ (as described e.\,g.\ by Apostol~\cite{apostol1976analytic} 
  is related to the Hurwitz zeta function. It is periodic in q› with period 1 and it can be 
  represented by a Dirichlet series that is absolutely convergent for $\mathfrak{R}(s) > 1$.
   If q ∉ ℤ›, it furthermore convergent for $\mathfrak{R}(s) > 0$.

  It is clear that for integer q›, we have $F(s, q) = F(s, 0) = \zeta(s)$. Moreover, for
  non-integer q›, $F(s, q)$ can be analytically continued to an entire function.
›
definition fds_perzeta :: "real  complex fds" where
  "fds_perzeta q = fds (λm. exp (2 * pi * 𝗂 * m * q))"

text ‹
  The definition of the periodic zeta function on the full domain is a bit unwieldy.
  The precise reasoning for this definition will be given later, and, in any case, it
  is probably more instructive to look at the derived ``alternative'' definitions later.
›
definition perzeta :: "real  complex  complex" where
  "perzeta q' s =
     (if q'   then zeta s
      else let q = frac q' in
        if s = 0 then 𝗂 / (2 * pi) * (pre_zeta q 1 - pre_zeta (1 - q) 1 + 
                                             ln (1 - q) - ln q + pi * 𝗂)
        else if s   then eval_fds (fds_perzeta q) s 
        else complex_of_real (2 * pi) powr (s - 1) * 𝗂 * Gamma (1 - s) *
               (𝗂 powr (-s) * hurwitz_zeta q (1 - s) -
                𝗂 powr s * hurwitz_zeta (1 - q) (1 - s)))"

interpretation fds_perzeta: periodic_fun_simple' fds_perzeta
  by standard (simp_all add: fds_perzeta_def exp_add ring_distribs exp_eq_polar
                             cis_mult [symmetric] cis_multiple_2pi)

interpretation perzeta: periodic_fun_simple' perzeta
proof -
  have [simp]: "n + 1    n  " for n :: real
    by (simp flip: frac_eq_0_iff add: frac.plus_1)
  show "periodic_fun_simple' perzeta"
    by standard (auto simp: fun_eq_iff perzeta_def Let_def frac.plus_1)
qed

lemma perzeta_frac [simp]: "perzeta (frac q) = perzeta q"
  by (auto simp: perzeta_def fun_eq_iff Let_def)

lemma fds_perzeta_frac [simp]: "fds_perzeta (frac q) = fds_perzeta q"
  using fds_perzeta.plus_of_int[of "frac q" "q"] by (simp add: frac_def)

lemma abs_conv_abscissa_perzeta: "abs_conv_abscissa (fds_perzeta q)  1"
proof (rule abs_conv_abscissa_leI)
  fix c assume c: "ereal c > 1"
  hence "summable (λn. n powr -c)"
    by (simp add: summable_real_powr_iff)
  also have "?this  fds_abs_converges (fds_perzeta q) (of_real c)" unfolding fds_abs_converges_def
    by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of 0]])
       (auto simp: norm_divide norm_powr_real_powr fds_perzeta_def powr_minus field_simps)
  finally show "s. s  1 = c  fds_abs_converges (fds_perzeta q) s"
    by (intro exI[of _ "of_real c"]) auto
qed

lemma conv_abscissa_perzeta: "conv_abscissa (fds_perzeta q)  1"
  by (rule order.trans[OF conv_le_abs_conv_abscissa abs_conv_abscissa_perzeta])

lemma fds_perzeta__left_0 [simp]: "fds_perzeta 0 = fds_zeta"
  by (simp add: fds_perzeta_def fds_zeta_def)

lemma perzeta_0_left [simp]: "perzeta 0 s = zeta s"
  by (simp add: perzeta_def eval_fds_zeta)

lemma perzeta_int: "q    perzeta q = zeta"
  by (simp add: perzeta_def fun_eq_iff)

lemma fds_perzeta_int: "q    fds_perzeta q = fds_zeta"
  by (auto simp: fds_perzeta.of_int elim!: Ints_cases)

lemma sums_fds_perzeta:
  assumes "Re s > 1"
  shows   "(λm. exp (2 * pi * 𝗂 * Suc m * q) / of_nat (Suc m) powr s) sums
             eval_fds (fds_perzeta q) s"
proof -
  have "conv_abscissa (fds_perzeta q)  1" by (rule conv_abscissa_perzeta)
  also have " < ereal (Re s)"  using assms by (simp add: one_ereal_def)
  finally have "fds_converges (fds_perzeta q) s" by (intro fds_converges) auto
  hence "(λn. fds_nth (fds_perzeta q) (Suc n) / nat_power (Suc n) s) sums
           eval_fds (fds_perzeta q) s" by (subst sums_Suc_iff) (auto simp: fds_converges_iff)
  thus ?thesis by (simp add: fds_perzeta_def)
qed

lemma sum_tendsto_fds_perzeta:
  assumes "Re s > 1"
  shows   "(λn. k{0<..n}. exp (2 * real k * pi * q * 𝗂) * of_nat k powr - s)
               eval_fds (fds_perzeta q) s"
proof -
  have "(λm. exp (2 * pi * 𝗂 * Suc m * q) / of_nat (Suc m) powr s) sums eval_fds (fds_perzeta q) s"
    by (intro sums_fds_perzeta assms)
  hence "(λn. k<n. exp (2 * real (Suc k) * pi * q * 𝗂) * of_nat (Suc k) powr -s) 
           eval_fds (fds_perzeta q) s"
    (is "filterlim ?f _ _") by (simp add: sums_def powr_minus field_simps)
  also have "?f = (λn. k{0<..n}. exp (2 * real k * pi * q * 𝗂) * of_nat k powr -s)"
    by (intro ext sum.reindex_bij_betw sum.reindex_bij_witness[of _ "λn. n - 1" Suc]) auto
  finally show ?thesis by simp
qed

text ‹
  Using the geometric series, it is easy to see that the Dirichlet series for $F(s, q)$
  has bounded partial sums for non-integer q›, so it must converge for any s› with
  $\mathfrak{R}(s) > 0$.
›
lemma conv_abscissa_perzeta':
  assumes "q  "
  shows   "conv_abscissa (fds_perzeta q)  0"
proof (rule conv_abscissa_leI)
  fix c :: real assume c: "ereal c > 0"
  have "fds_converges (fds_perzeta q) (of_real c)"
  proof (rule bounded_partial_sums_imp_fps_converges)
    define ω where "ω = exp (2 * pi * 𝗂 * q)"
    have [simp]: "norm ω = 1" by (simp add: ω_def)
    define M where "M = 2 / norm (1 - ω)"
    from q   have "ω  1"
      by (auto simp: ω_def exp_eq_1)
    hence "M > 0" by (simp add: M_def)
  
    show "Bseq (λn. kn. fds_nth (fds_perzeta q) k / nat_power k 0)"
      unfolding Bseq_def
    proof (rule exI, safe)
      fix n :: nat
      show "norm (kn. fds_nth (fds_perzeta q) k / nat_power k 0)  M"
      proof (cases "n = 0")
        case False
        have "(kn. fds_nth (fds_perzeta q) k / nat_power k 0) =
                (k{1..1 + (n - 1)}. ω ^ k)" using False
          by (intro sum.mono_neutral_cong_right)
             (auto simp: fds_perzeta_def fds_nth_fds exp_of_nat_mult [symmetric] mult_ac ω_def)
        also have " = ω * (1 - ω ^ n) / (1 - ω)" using ω  1 and False
          by (subst sum_gp_offset) simp
        also have "norm   1 * (norm (1::complex) + norm (ω ^ n)) / norm (1 - ω)"
          unfolding norm_mult norm_divide
          by (intro mult_mono divide_right_mono norm_triangle_ineq4) auto
        also have " = M" by (simp add: M_def norm_power)
        finally show ?thesis .
      qed (use M > 0 in simp_all)
    qed fact+
  qed (insert c, auto)
  thus "s. s  1 = c  fds_converges (fds_perzeta q) s"
    by (intro exI[of _ "of_real c"]) auto
qed

lemma fds_perzeta_one_half: "fds_perzeta (1 / 2) = fds (λn. (-1) ^ n)"
  using Complex.DeMoivre[of pi]
  by (intro fds_eqI) (auto simp: fds_perzeta_def exp_eq_polar mult_ac)

lemma perzeta_one_half_1 [simp]: "perzeta (1 / 2) 1 = -ln 2"
proof (rule sums_unique2)
  have *: "(1 / 2 :: real)  "
    using fraction_not_in_ints[of 2 1] by auto
  have "fds_converges (fds_perzeta (1 / 2)) 1"
    by (rule fds_converges, rule le_less_trans, rule conv_abscissa_perzeta') (use * in auto)
  hence "(λn. (-1) ^ Suc n / Suc n) sums eval_fds (fds_perzeta (1 / 2)) 1"
    unfolding fds_converges_altdef by (simp add: fds_perzeta_one_half)
  also from * have "eval_fds (fds_perzeta (1 / 2)) 1 = perzeta (1 / 2) 1"
    by (simp add: perzeta_def)
  finally show "(λn. -complex_of_real ((-1) ^ n / Suc n)) sums perzeta (1 / 2) 1"
    by simp
  hence "(λn. -complex_of_real ((-1) ^ n / Suc n)) sums -of_real (ln 2)"
    by (intro sums_minus sums_of_real alternating_harmonic_series_sums)
  thus "(λn. -complex_of_real ((-1) ^ n / Suc n)) sums -(ln 2)"
    by (simp flip: Ln_of_real)
qed


subsection ‹Hurwitz's formula›

text ‹
  We now move on to prove Hurwitz's formula relating the Hurwitz zeta function and the
  periodic zeta function. We mostly follow Apostol's proof, although we do make some small
  changes in order to make the proof more amenable to Isabelle's complex analysis library.
 
  The big difference is that Apostol integrates along a circle with a slit, where the two
  sides of the slit lie on different branches of the integrand. This makes sense when looking
  as the integrand as a Riemann surface, but we do not have a notion of Riemann surfaces in
  Isabelle.

  It is therefore much easier to simply cut the circle into an upper and a lower half. In fact,
  the integral on the lower half can be reduced to the one on the upper half easily by
  symmetry, so we really only need to handle the integral on the upper half. The integration
  contour that we will use is therefore a semi-annulus in the upper half of the complex plane,
  centred around the origin.

  Now, first of all, we prove the existence of an important improper integral 
  that we will need later.
›
(* TODO: Move *)
lemma set_integrable_bigo:
  fixes f g :: "real  'a :: {banach, real_normed_field, second_countable_topology}"
  assumes "f  O(λx. g x)" and "set_integrable lborel {a..} g"
  assumes "b. b  a  set_integrable lborel {a..<b} f"
  assumes [measurable]: "set_borel_measurable borel {a..} f"
  shows   "set_integrable lborel {a..} f"
proof -
  from assms(1) obtain C x0 where C: "C > 0" "x. x  x0  norm (f x)  C * norm (g x)"
    by (fastforce elim!: landau_o.bigE simp: eventually_at_top_linorder)
  define x0' where "x0' = max a x0"

  have "set_integrable lborel {a..<x0'} f"
    by (intro assms) (auto simp: x0'_def)
  moreover have "set_integrable lborel {x0'..} f" unfolding set_integrable_def
  proof (rule Bochner_Integration.integrable_bound)
    from assms(2) have "set_integrable lborel {x0'..} g"
      by (rule set_integrable_subset) (auto simp: x0'_def)
    thus "integrable lborel (λx. C *R (indicator {x0'..} x *R g x))" unfolding set_integrable_def
      by (intro integrable_scaleR_right) (simp add: abs_mult norm_mult)
  next
    from assms(4) have "set_borel_measurable borel {x0'..} f"
      by (rule set_borel_measurable_subset) (auto simp: x0'_def)
    thus "(λx. indicator {x0'..} x *R f x)  borel_measurable lborel"
      by (simp add: set_borel_measurable_def)
  next
    show "AE x in lborel. norm (indicator {x0'..} x *R f x)
                             norm (C *R (indicator {x0'..} x *R g x))"
      using C by (intro AE_I2) (auto simp: abs_mult indicator_def x0'_def)
  qed
  ultimately have "set_integrable lborel ({a..<x0'}  {x0'..}) f"
    by (rule set_integrable_Un) auto
  also have "{a..<x0'}  {x0'..} = {a..}" by (auto simp: x0'_def)
  finally show ?thesis .
qed

lemma set_integrable_Gamma_hurwitz_aux2_real:
  fixes s a :: real
  assumes "r > 0" and "a > 0"
  shows "set_integrable lborel {r..} (λx. x powr s * (exp (-a * x)) / (1 - exp (-x)))"
    (is "set_integrable _ _ ?g")
proof (rule set_integrable_bigo)
  have "(λx. exp (-(a/2) * x)) integrable_on {r..}" using assms
    by (intro integrable_on_exp_minus_to_infinity) auto
  hence "set_integrable lebesgue {r..} (λx. exp (-(a/2) * x))"
    by (intro nonnegative_absolutely_integrable) simp_all
  thus "set_integrable lborel {r..} (λx. exp (-(a/2) * x))"
    by (simp add: set_integrable_def integrable_completion)
next
  fix y :: real
  have "set_integrable lborel {r..y} ?g" using assms
    by (intro borel_integrable_atLeastAtMost') (auto intro!: continuous_intros)
  thus "set_integrable lborel {r..<y} ?g"
    by (rule set_integrable_subset) auto
next
  from assms show "?g  O(λx. exp (-(a/2) * x))"
    by real_asymp
qed (auto simp: set_borel_measurable_def)

lemma set_integrable_Gamma_hurwitz_aux2:
  fixes s :: complex and a :: real
  assumes "r > 0" and "a > 0"
  shows   "set_integrable lborel {r..} (λx. x powr -s * (exp (- a * x)) / (1 - exp (- x)))"
             (is "set_integrable _ _ ?g")
proof -
  have "set_integrable lborel {r..} (λx. x powr -Re s * (exp (-a * x)) / (1 - exp (-x)))" 
    (is "set_integrable _ _ ?g'")
    by (rule set_integrable_Gamma_hurwitz_aux2_real) (use assms in auto)
  also have "?this  integrable lborel (λx. indicator {r..} x *R ?g' x)"
    by (simp add: set_integrable_def)
  also have "(λx. indicator {r..} x *R ?g' x) = (λx. norm (indicator {r..} x *R ?g x))" using assms
    by (auto simp: indicator_def norm_mult norm_divide norm_powr_real_powr fun_eq_iff
                   exp_of_real exp_minus norm_inverse in_Reals_norm power2_eq_square divide_simps)
  finally show ?thesis unfolding set_integrable_def
    by (subst (asm) integrable_norm_iff) auto
qed

lemma closed_neg_Im_slit: "closed {z. Re z = 0  Im z  0}"
proof -
  have "closed ({z. Re z = 0}  {z. Im z  0})"
    by (intro closed_Int closed_halfspace_Re_eq closed_halfspace_Im_le)
  also have "{z. Re z = 0}  {z. Im z  0} = {z. Re z = 0  Im z  0}" by blast
  finally show ?thesis .
qed


text ‹
  We define tour semi-annulus path. When this path is mirrored into the lower half of the complex
  plane and subtracted from the original path and the outer radius tends to ∞›, this becomes a
  Hankel contour extending to -∞›.
›
definition hankel_semiannulus :: "real  nat  real  complex" where
 "hankel_semiannulus r N = (let R = (2 * N + 1) * pi in
    part_circlepath 0 R 0 pi +++                  ―‹Big half circle›
    linepath (of_real (-R)) (of_real (-r)) +++    ―‹Line on the negative real axis›
    part_circlepath 0 r pi 0 +++                  ―‹Small half circle›
    linepath (of_real r) (of_real R))             ―‹Line on the positive real axis›" 

lemma path_hankel_semiannulus [simp, intro]: "path (hankel_semiannulus r R)"
  and valid_path_hankel_semiannulus [simp, intro]: "valid_path (hankel_semiannulus r R)"
  and pathfinish_hankel_semiannulus [simp, intro]:
        "pathfinish (hankel_semiannulus r R) = pathstart (hankel_semiannulus r R)"
  by (simp_all add: hankel_semiannulus_def Let_def)


text ‹
  We set the stage for an application of the Residue Theorem. We define a function
  \[f(s, z) = z^{-s} \frac{\exp(az)}{1-\exp(-z)}\ ,\]
  which will be the integrand. However, the principal branch of $z^{-s}$ has a branch cut
  along the non-positive real axis, which is bad because a part of our integration path also
  lies on the non-positive real axis. We therefore choose a slightly different branch of $z^{-s}$
  by moving the logarithm branch along by $90^{\circ}$ so that the branch cut lies on the
  non-positive imaginary axis instead.
›
context
  fixes a :: real
  fixes f :: "complex  complex  complex"
    and g :: "complex  real  complex"
    and h :: "real  complex  real  complex"
    and Res :: "complex  nat  complex" 
    and Ln' :: "complex  complex"
    and F :: "real  complex  complex"
  assumes a: "a  {0<..1}"

  ―‹Our custom branch of the logarithm›
  defines "Ln'  (λz. ln (-𝗂 * z) + 𝗂 * pi / 2)"

  ―‹The integrand›
  defines "f  (λs z. exp (Ln' z * (-s) + of_real a * z) / (1 - exp z))"

  ―‹The integrand on the negative real axis›
  defines "g  (λs x. complex_of_real x powr -s * of_real (exp (-a*x)) / of_real (1 - exp (-x)))"

  ―‹The integrand on the circular arcs›
  defines "h  (λr s t. r * 𝗂 * cis t * exp (a * (r * cis t) - (ln r + 𝗂 * t) * s) /
                        (1 - exp (r * cis t)))"

  ―‹The interesting part of the residues›
  defines "Res  (λs k. exp (of_real (2 * real k * pi * a) * 𝗂) *
                            of_real (2 * real k * pi) powr (-s))"

  ―‹The periodic zeta function (at least on $\mathfrak{R}(s) > 1$ half-plane)›
  defines "F  (λq. eval_fds (fds_perzeta q))"
begin

text ‹
  First, some basic properties of our custom branch of the logarithm:
›
lemma Ln'_i: "Ln' 𝗂 = 𝗂 * pi / 2"
  by (simp add: Ln'_def)

lemma Ln'_of_real_pos:
  assumes "x > 0"
  shows   "Ln' (of_real x) = of_real (ln x)"
proof -
  have "Ln' (of_real x) = Ln (of_real x * (-𝗂)) + 𝗂 * pi / 2"
    by (simp add: Ln'_def mult_ac)
  also have " = of_real (ln x)" using assms
    by (subst Ln_times_of_real) (auto simp: Ln_of_real)
  finally show ?thesis .
qed

lemma Ln'_of_real_neg:
  assumes "x < 0"
  shows   "Ln' (of_real x) = of_real (ln (-x)) + 𝗂 * pi"
proof -
  have "Ln' (of_real x) = Ln (of_real (-x) * 𝗂) + 𝗂 * pi / 2"
    by (simp add: Ln'_def mult_ac)
  also have " = of_real (ln (-x)) + 𝗂 * pi" using assms
    by (subst Ln_times_of_real) (auto simp: Ln_Reals_eq)
  finally show ?thesis .
qed

lemma Ln'_times_of_real:
  "Ln' (of_real x * z) = of_real (ln x) + Ln' z" if "x > 0" "z  0" for z x
proof -
  have "Ln' (of_real x * z) = Ln (of_real x * (- 𝗂 * z)) + 𝗂 * pi / 2"
    by (simp add: Ln'_def mult_ac)
  also have " = of_real (ln x) + Ln' z"
    using that by (subst Ln_times_of_real) (auto simp: Ln'_def Ln_of_real)
  finally show ?thesis .
qed

lemma Ln'_cis:
  assumes "t  {-pi / 2<..3 / 2 * pi}"
  shows   "Ln' (cis t) = 𝗂 * t"
proof -
  have "exp (𝗂 * pi / 2) = 𝗂" by (simp add: exp_eq_polar)
  hence "Ln (- (𝗂 * cis t)) = 𝗂 * (t - pi / 2)" using assms
    by (intro Ln_unique) (auto simp: algebra_simps exp_diff cis_conv_exp)
  thus ?thesis by (simp add: Ln'_def algebra_simps)
qed

text ‹
  Next, we show that the line and circle integrals are holomorphic using Leibniz's rule:
›
lemma contour_integral_part_circlepath_h:
  assumes r: "r > 0"
  shows   "contour_integral (part_circlepath 0 r 0 pi) (f s) = integral {0..pi} (h r s)"
proof -
  have "contour_integral (part_circlepath 0 r 0 pi) (f s) = 
          integral {0..pi} (λt. f s (r * cis t) * r * 𝗂 * cis t)"
    by (simp add: contour_integral_part_circlepath_eq)
  also have "integral {0..pi} (λt. f s (r * cis t) * r * 𝗂 * cis t) = integral {0..pi} (h r s)"
  proof (intro integral_cong)
    fix t assume t: "t  {0..pi}"
    have "-(pi / 2) < 0" by simp
    also have "0  t" using t by simp
    finally have "t  {-(pi/2)<..3/2*pi}" using t by auto
    thus "f s (r * cis t) * r * 𝗂 * cis t = h r s t"
      using r by (simp add: f_def Ln'_times_of_real Ln'_cis h_def Ln_Reals_eq)
  qed
  finally show ?thesis .
qed

lemma integral_g_holomorphic:
  assumes "b > 0"
  shows   "(λs. integral {b..c} (g</