Theory Newman_Ingham_Tauberian

(*
  File:     Newman_Ingham_Tauberian.thy
  Author:   Manuel Eberl (TU München)

  A proof of Newman's "analytic theorem", originally stated by Ingham
*)
section ‹Ingham's Tauberian Theorem›
theory Newman_Ingham_Tauberian
imports
  "HOL-Real_Asymp.Real_Asymp"
  Prime_Number_Theorem_Library
begin

text ‹
  In his proof of the Prime Number Theorem, Newman~cite"newman1998analytic" uses a Tauberian 
  theorem that was first proven by Ingham. Newman gives a nice and straightforward proof of this
  theorem based on contour integration. This section will be concerned with proving this theorem.
  
  This Tauberian theorem is probably the part of the Newman's proof of the Prime Number Theorem
  where most of the ``heavy lifting'' is done. Its purpose is to extend the summability of a 
  Dirichlet series with bounded coefficients from the region $\mathfrak{R}(s)>1$ to 
  $\mathfrak{R}(s)\geq 1$.

  In order to show it, we first require a number of auxiliary bounding lemmas.
›
lemma newman_ingham_aux1:
  fixes R :: real and z :: complex
  assumes R: "R > 0" and z : "norm z = R"
  shows   "norm (1 / z + z / R2) = 2 * ¦Re z¦ / R2"
proof -
  from z and R have [simp]: "z  0" by auto
  have "1 / z + z / R2 = (R2 + z2) * (1 / R2 / z)" using R
    by (simp add: field_simps power2_eq_square)
  also have "norm  = norm (R2 + z2) / R ^ 3"
    by (simp add: numeral_3_eq_3 z norm_divide norm_mult power2_eq_square)
  also have "R2 + z2 = z * (z + cnj z)" using complex_norm_square[of z]
    by (simp add: z power2_eq_square algebra_simps)
  also have "norm  = 2 * ¦Re z¦ * R"
    by (subst complex_add_cnj) (simp_all add: z norm_mult)
  also have " / R ^ 3 = 2 * ¦Re z¦ / R2"
    using R by (simp add: field_simps numeral_3_eq_3 power2_eq_square)
  finally show ?thesis .
qed

lemma newman_ingham_aux2:
  fixes m :: nat and w z :: complex
  assumes "1  m" "1  Re w" "0 < Re z" and f: "n. 1  n  norm (f n)  C"
  shows "norm (n=1..m. f n / n powr (w - z))  C * (m powr Re z) * (1 / m + 1 / Re z)"
proof -
  have [simp]: "C  0" by (rule order.trans[OF _ f[of 1]]) auto
  have "norm (n=1..m. f n / n powr (w - z))  (n=1..m. C / n powr (1 - Re z))"
    by (rule sum_norm_le)
       (insert assms, auto simp: norm_divide norm_powr_real_powr intro!: frac_le assms powr_mono)
  also have " = C * (n=1..m. n powr (Re z - 1))"
    by (subst sum_distrib_left) (simp_all add: powr_diff)
  also have "  C * (m powr Re z * (1 / Re z + 1 / m))"
    using zeta_partial_sum_le'[of "Re z" m] assms by (intro mult_left_mono) auto
  finally show ?thesis by (simp add: mult_ac add_ac)
qed

lemma hurwitz_zeta_real_bound_aux:
  fixes a x :: real
  assumes ax: "a > 0" "x > 1"
  shows "(i. (a + real (Suc i)) powr (-x))  a powr (1 - x) / (x - 1)"
proof (rule decreasing_sum_le_integral, goal_cases)
  have "((λt. (a + t) powr -x) has_integral -(a powr (-x + 1)) / (-x + 1)) (interior {0..})"
    using powr_has_integral_at_top[of 0 a "-x"] using ax by (simp add: interior_real_atLeast)
  also have "-(a powr (- x + 1)) / (- x + 1) = a powr (1 - x) / (x - 1)"
    using ax by (simp add: field_simps)
  finally show "((λt. (a + t) powr -x) has_integral a powr (1 - x) / (x - 1)) {0..}"
    by (subst (asm) has_integral_interior) auto
qed (insert ax, auto intro!: powr_mono2')


text ‹
  Given a function that is analytic on some vertical line segment, we can find a rectangle
  around that line segment on which the function is also analytic.
›
lemma analytic_on_axis_extend:
  fixes y1 y2 x :: real
  defines "S  {z. Re z = x  Im z  {y1..y2}}"
  assumes "y1  y2"
  assumes "f analytic_on S"
  obtains x1 x2 :: real where "x1 < x" "x2 > x" "f analytic_on cbox (Complex x1 y1) (Complex x2 y2)"
proof -
  define C where "C = {box a b |a b z. f analytic_on box a b  z  box a b  z  S}"
  have "S = cbox (Complex x y1) (Complex x y2)"
    by (auto simp: S_def in_cbox_complex_iff)
  also have "compact " by simp
  finally have 1: "compact S" .

  have 2: "S  C"
  proof (intro subsetI)
    fix z assume "z  S"
    from f analytic_on S and this obtain a b where "z  box a b" "f analytic_on box a b"
      by (blast elim: analytic_onE_box)
    with z  S show "z  C" unfolding C_def by blast
  qed

  have 3: "open X" if "X  C" for X using that by (auto simp: C_def)
  from compactE[OF 1 2 3] obtain T where T: "T  C" "finite T" "S  T"
    by blast

  define x1 where "x1 = Max (insert (x - 1) ((λX. x + (Inf (Re ` X) - x) / 2) ` T))"
  define x2 where "x2 = Min (insert (x + 1) ((λX. x + (Sup (Re ` X) - x) / 2) ` T))"

  have *: "x + (Inf (Re ` X) - x) / 2 < x  x + (Sup (Re ` X) - x) / 2 > x" if "X  T" for X
  proof -
    from that and T obtain a b s where [simp]: "X = box a b" and s: "s  box a b" "s  S"
      by (force simp: C_def)
    hence le: "Re a < Re b" "Im a < Im b" by (auto simp: in_box_complex_iff)
    show ?thesis using le s
      unfolding X = box a b Re_image_box[OF le] Im_image_box[OF le]
      by (auto simp: S_def in_box_complex_iff)
  qed
  from * T have "x1 < x" unfolding x1_def by (subst Max_less_iff) auto
  from * T have "x2 > x" unfolding x2_def by (subst Min_gr_iff) auto

  have "f analytic_on (T)"
    using T by (subst analytic_on_Union) (auto simp: C_def)
  moreover have "z  T" if "z  cbox (Complex x1 y1) (Complex x2 y2)" for z
  proof -
    from that have "Complex x (Im z)  S"
      by (auto simp: in_cbox_complex_iff S_def)
    with T obtain X where X: "X  T" "Complex x (Im z)  X"
      by auto
    with T obtain a b where [simp]: "X = box a b" by (auto simp: C_def)
    from X have le: "Re a < Re b" "Im a < Im b" by (auto simp: in_box_complex_iff)

    from that have "Re z  x2" by (simp add: in_cbox_complex_iff)
    also have "  x + (Sup (Re ` X) - x) / 2"
      unfolding x2_def by (rule Min.coboundedI)(use T X in auto)
    also have " = (x + Re b) / 2"
      using le unfolding X = box a b Re_image_box[OF le] by (simp add: field_simps)
    also have " < (Re b + Re b) / 2"
      using X by (intro divide_strict_right_mono add_strict_right_mono)
                 (auto simp: in_box_complex_iff)
    also have " = Re b" by simp
    finally have [simp]: "Re z < Re b" .

    have "Re a = (Re a + Re a) / 2" by simp
    also have " < (x + Re a) / 2"
      using X by (intro divide_strict_right_mono add_strict_right_mono)
                 (auto simp: in_box_complex_iff)
    also have " = x + (Inf (Re ` X) - x) / 2"
      using le unfolding X = box a b Re_image_box[OF le] by (simp add: field_simps)
    also have "  x1" unfolding x1_def by (rule Max.coboundedI)(use T X in auto)
    also have "  Re z" using that by (simp add: in_cbox_complex_iff)
    finally have [simp]: "Re z > Re a" .

    from X have "z  X" by (simp add: in_box_complex_iff)
    with T X show ?thesis by blast
  qed
  hence "cbox (Complex x1 y1) (Complex x2 y2)  T" by blast
  ultimately have "f analytic_on cbox (Complex x1 y1) (Complex x2 y2)"
    by (rule analytic_on_subset)

  with x1 < x and x2 > x and that[of x1 x2] show ?thesis by blast
qed


text ‹
  We will now prove the theorem. The precise setting is this:
  Consider a Dirichlet series $F(s) = \sum a_n n^{-s}$ with bounded coefficients. Clearly,
  this converges to an analytic function $f(s)$ on $\{s\mid \mathfrak R(s)>1\}$.

  If $f(s)$ is analytic on the larger set $\{s\mid \mathfrak R(s)\geq 1\}$, $F$ converges
  to $f(s)$ for all $\mathfrak R(s) \geq 1$.

  The proof follows Newman's argument very closely, but some of the precise bounds we use
  are a bit different from his. Also, like Harrison, we choose a combination of a semicircle
  and a rectangle as our contour, whereas Newman uses a circle with a vertical cut-off. The result
  of the Residue theorem is the same in both cases, but the bounding of the contributions of the
  different parts is somewhat different.

  The reason why we picked Harrison's contour over Newman's is because we could not understand how
  his bounding of the different contributions fits to his contour, and it seems likely that this
  is also the reason why Harrison altered the contour in the first place.
›
lemma Newman_Ingham_1:
  fixes F :: "complex fds" and f :: "complex  complex"
  assumes coeff_bound:   "fds_nth F  O(λ_. 1)"
  assumes f_analytic:    "f analytic_on {s. Re s  1}"
  assumes F_conv_f:      "s. Re s > 1  eval_fds F s = f s"
  assumes w:             "Re w  1"
  shows   "fds_converges F w" and "eval_fds F w = f w"
proof -
  ― ‹We get a bound on our coefficients and call it C›.›
  obtain C where C: "C  1" "n. norm (fds_nth F n)  C"
    using natfun_bigo_1E[OF coeff_bound, where lb = 1] by blast
  write contour_integral ("∮[_]")

  ― ‹We show convergence directly by showing that the difference between the 
      partial sums and the limit vanishes.›
  have "(λN. eval_fds (fds_truncate N F) w)  f w"
    unfolding tendsto_iff dist_norm norm_minus_commute[of "eval_fds F s" for F s]
  proof safe
    fix ε :: real assume ε: "ε > 0"
    ― ‹We choose an integration radius that is big enough for the error to be sufficiently small.›
    define R where "R = max 1 (3 * C / ε)"
    have R: "R  3 * C / ε" "R  1" by (auto simp: R_def)

    ― ‹Next, we extend the analyticity of f (w + z)› to the left of the complex plane
        within a thin rectangle that is at least as high as the circle.›
    obtain l where l: "l > 0"
      "(λz. f (w + z)) analytic_on {s. Re s > 0  Im s  {-R-1<..<R+1}  Re s > -l}"
    proof -
      have f_analytic': "(λz. f (w + z)) analytic_on {s. Re s  0}"
        by (rule analytic_on_compose_gen[OF _ f_analytic, unfolded o_def])
           (insert w, auto intro: analytic_intros)
      hence "(λz. f (w + z)) analytic_on {s. Re s = 0  Im s  {-R-1..R+1}}"
        by (rule analytic_on_subset) auto
      from analytic_on_axis_extend[OF _ this] obtain x1 x2 where x12: 
        "x1 < 0" "x2 > 0" "(λz. f (w + z)) analytic_on cbox (Complex x1 (-R-1)) (Complex x2 (R+1))"
        using R  1 by auto
      from this(3) have "(λz. f (w + z)) analytic_on {s. Re s  {x1..0}  Im s  {-R-1..R+1}}"
        by (rule analytic_on_subset) (insert x12, auto simp: in_cbox_complex_iff)
      with f_analytic' have "(λz. f (w + z)) analytic_on
                               ({s. Re s  0}  {s. Re s  {x1..0}  Im s  {-R-1..R+1}})"
        by (subst analytic_on_Un) auto
      hence "(λz. f (w + z)) analytic_on {s. Re s > 0  Im s  {-R-1<..<R+1}  Re s > x1}"
        by (rule analytic_on_subset) auto
      with x1 < 0 and that[of "-x1"] show ?thesis by auto
    qed

    ― ‹The function f (w + z)› is now analytic on the open box $(-l; R+1) + i(-R+1; R+1)$.
        We call this region X›.›
    define X where "X = box (Complex (-l) (-R-1)) (Complex (R+1) (R+1))"
    have [simp, intro]: "open X" "convex X" by (simp_all add: X_def open_box)
    from R l have [simp]: "0  X" by (auto simp: X_def in_box_complex_iff)
    have analytic: "(λz. f (w + z)) analytic_on X"
      by (rule analytic_on_subset[OF l(2)]) (auto simp: X_def in_box_complex_iff)
    note f_analytic' [analytic_intros] = analytic_on_compose_gen[OF _ analytic, unfolded o_def]
    note f_holo [holomorphic_intros] =
      holomorphic_on_compose_gen[OF _ analytic_imp_holomorphic[OF analytic], unfolded o_def]
    note f_cont [continuous_intros] = continuous_on_compose2[OF 
      holomorphic_on_imp_continuous_on[OF analytic_imp_holomorphic[OF analytic]]]

    ― ‹We now pick a smaller closed box X'› inside the big open box X›. This is because
        we need a compact set for the next step. our integration path still lies entirely
        within X'›, and since X'› is compact, f (w + z)› is bounded on it,
        so we obtain such a bound and call it M›.›
    define δ where "δ = min (1/2) (l/2)"
    from l have δ: "δ > 0" "δ  1/2" "δ < l" by (auto simp: δ_def)
    define X' where "X' = cbox (Complex (-δ) (-R)) (Complex R R)"
    have "X'  X" unfolding X'_def X_def using l(1) R δ
      by (intro subset_box_imp) (auto simp: Basis_complex_def)
    have [intro]: "compact X'" by (simp add: X'_def)
    moreover have "continuous_on X' (λz. f (w + z))"
      using w X'  X by (auto intro!: continuous_intros)
    ultimately obtain M where M: "M  0" "z. z  X'  norm (f (w + z))  M"
      using continuous_on_compact_bound by blast

    ― ‹Our objective is now to show that the difference between the N›-th partial sum
        and the limit is below a certain bound (depending on N›) which tends to 0› 
        for N → ∞›. We use the following bound:›
    define bound where
      "bound = (λN::nat. (2*C/R + C/N + 3*M / (pi*R*ln N) + 3*R*M / (δ*pi * N powr δ)))"
    have "2 * C / R < ε" using M(1) R C(1) δ(1) ε
      by (auto simp: field_simps)
    ― ‹Evidently this is below @{term ε} for sufficiently large N›.›
    hence "eventually (λN::nat. bound N < ε) at_top"
      using M(1) R C(1) δ(1) ε unfolding bound_def by real_asymp

    ― ‹It now only remains to show that the difference is indeed less than the claimed bound.›
    thus "eventually (λN. norm (f w - eval_fds (fds_truncate N F) w) < ε) at_top"
      using eventually_gt_at_top[of 1]
    proof eventually_elim
      case (elim N)
      note N = this

      ― ‹Like Harrison (and unlike Newman), our integration path Γ› consists of a semicircle A›
          of radius R› in the right-halfplane and a box of width δ› and height 2R› on
          the left halfplane. The latter consists of three straight lines, which we call B1›
          to B3›.›
      define A where "A = part_circlepath 0 R (-pi/2) (pi/2)"
      define B2 where "B2 = linepath (Complex (-δ) R) (Complex (-δ) (-R))"
      define B1 where "B1 = linepath (R * 𝗂) (R * 𝗂 - δ)"
      define B3 where "B3 = linepath (-R * 𝗂 - δ) (-R * 𝗂)"
      define Γ where "Γ = A +++ B1 +++ B2 +++ B3"

      ― ‹We first need to show some basic facts about the geometry of our integration path.›
      have [simp, intro]:
        "path A" "path B1" "path B3" "path B2"
        "valid_path A" "valid_path B1" "valid_path B3" "valid_path B2"
        "arc A" "arc B1" "arc B3" "arc B2"
        "pathstart A = -𝗂 * R" "pathfinish A = 𝗂 * R"
        "pathstart B1 = 𝗂 * R" "pathfinish B1 = R * 𝗂 - δ"
        "pathstart B3 = -R * 𝗂 - δ" "pathfinish B3 = -𝗂 * R"
        "pathstart B2 = R * 𝗂 - δ" "pathfinish B2 = -R * 𝗂 - δ" using R δ
        by (simp_all add: A_def B1_def B3_def exp_eq_polar B2_def Complex_eq arc_part_circlepath)
      hence [simp, intro]: "valid_path Γ" 
        by (simp add: Γ_def A_def B1_def B3_def B2_def exp_eq_polar Complex_eq)
      hence [simp, intro]: "path Γ" using valid_path_imp_path by blast
      have [simp]: "pathfinish Γ = pathstart Γ" by (simp add: Γ_def exp_eq_polar)
    
      have image_B2: "path_image B2 = {s. Re s = -δ  Im s  {-R..R}}"
        using R by (auto simp: closed_segment_same_Re closed_segment_eq_real_ivl B2_def)
      have image_B1: "path_image B1 = {s. Re s  {-δ..0}  Im s = R}"
       and image_B3: "path_image B3 = {s. Re s  {-δ..0}  Im s = -R}"
        using δ by (auto simp: B1_def B3_def closed_segment_same_Im closed_segment_eq_real_ivl)
      have image_A: "path_image A = {s. Re s  0  norm s = R}"
        unfolding A_def using R by (subst path_image_semicircle_Re_ge) auto
      also have "z    z  X' - {0}" for z
        using complex_Re_le_cmod[of z] abs_Im_le_cmod[of z] δ R
        by (auto simp: X'_def in_cbox_complex_iff)
      hence "{s. Re s  0  norm s = R}  X' - {0}" by auto
      finally have "path_image B2  X' - {0}" "path_image A  X' - {0}"
           "path_image B1  X' - {0}" "path_image B3  X' - {0}" using δ > 0
        by (auto simp: X'_def in_cbox_complex_iff image_B2 image_B1 image_B3)
      note path_images = this X'  X

      ― ‹Γ› is a simple path, which, combined with its simple geometric shape, makes
          reasoning about its winding numbers trivial.›
      from R have "simple_path A" unfolding A_def
        by (subst simple_path_part_circlepath) auto
      have "simple_path Γ" unfolding Γ_def
      proof (intro simple_path_join_loop subsetI arc_join, goal_cases)
        fix z assume z: "z  path_image A  path_image (B1 +++ B2 +++ B3)"
        with image_A have "Re z  0" "norm z = R" by auto
        with z R δ show "z  {pathstart A, pathstart (B1 +++ B2 +++ B3)}"
          by (auto simp: path_image_join image_B1 image_B2 image_B3 complex_eq_iff)
      qed (insert R, auto simp: image_B1 image_B3 path_image_join image_B2 complex_eq_iff)
    
      ― ‹We define the integrands in the same fashion as Newman:›
      define g where "g = (λz::complex. f (w + z) * N powr z * (1 / z + z / R2))"
      define S where "S = eval_fds (fds_truncate N F)"
      define g_S where "g_S = (λz::complex. S (w + z) * N powr z * (1 / z + z / R2))"
      define rem where "rem = (λz::complex. f z - S z)"
      define g_rem where "g_rem = (λz::complex. rem (w + z) * N powr z * (1 / z + z / R2))"

      have g_holo: "g holomorphic_on X - {0}" unfolding g_def
        by (auto intro!: holomorphic_intros analytic_imp_holomorphic'[OF analytic])

      have rem_altdef: "rem z = eval_fds (fds_remainder N F) z" if "Re z > 1" for z
      proof -
      have abscissa: "abs_conv_abscissa F  1"
        using assms by (intro bounded_coeffs_imp_abs_conv_abscissa_le_1)
                       (simp_all add: natfun_bigo_iff_Bseq)
        from assms and that have "f z = eval_fds F z" by auto
        also have "F = fds_truncate N F + fds_remainder N F" 
          by (rule fds_truncate_plus_remainder [symmetric])
        also from that have "eval_fds  z = S z + eval_fds (fds_remainder N F) z" unfolding S_def
          by (subst eval_fds_add) (auto intro!: fds_abs_converges_imp_converges 
                                                fds_abs_converges[OF le_less_trans[OF abscissa]])
        finally show ?thesis by (simp add: rem_def)
      qed

      ― ‹We now come to the first application of the residue theorem along the path Γ›:›
      have "∮[Γ] g = 2 * pi * 𝗂 * winding_number Γ 0 * residue g 0"
      proof (subst Residue_theorem)
        show "g holomorphic_on X - {0}" by fact
        show "path_image Γ  X - {0}" using path_images
          by (auto simp: Γ_def path_image_join)
        thus "z. z  X  winding_number Γ z = 0"
          by (auto intro!: simply_connected_imp_winding_number_zero[of X]
                           convex_imp_simply_connected)
      qed (insert path_images, auto intro: convex_connected)
      also have "winding_number Γ 0 = 1"
      proof (rule simple_closed_path_winding_number_pos)
        from R δ have "g{A, B1, B2, B3}. Re (winding_number g 0) > 0"
          unfolding A_def B1_def B2_def B3_def
          by (auto intro!: winding_number_linepath_pos_lt winding_number_part_circlepath_pos_less)
        hence "valid_path Γ  0  path_image Γ  Re (winding_number Γ 0) > 0"
          unfolding Γ_def using path_images(1-4) by (intro winding_number_join_pos_combined') auto
        thus "Re (winding_number Γ 0) > 0" by simp
      qed (insert path_images simple_path Γ, auto simp: Γ_def path_image_join)
      also have "residue g 0 = f w"
      proof -
        have "g = (λz::complex. f (w + z) * N powr z * (1 + z2 / R2) / z)"
          by (auto simp: g_def divide_simps fun_eq_iff power2_eq_square
                   simp del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
        moreover from N have "residue  0 = f w"
          by (subst residue_simple'[of X])
             (auto intro!: holomorphic_intros analytic_imp_holomorphic[OF analytic])
        ultimately show ?thesis by (simp only:)
      qed
      finally have "2 * pi * 𝗂 * f w = ∮[Γ] g" by simp
      also have " = ∮[A] g + ∮[B2] g + ∮[B1] g + ∮[B3] g" unfolding Γ_def
        by (subst contour_integral_join, (insert path_images,
            auto intro!: contour_integral_join contour_integrable_holomorphic_simple g_holo)[4])+
           (simp_all add: add_ac)
      finally have integral1: "2 * pi * 𝗂 * f w = ∮[A] g + ∮[B2] g + ∮[B1] g + ∮[B3] g" .

      ― ‹Next, we apply the residue theorem along a circle of radius R› to another
          integrand that is related to the partial sum:›
      have "∮[circlepath 0 R] g_S = 2 * pi * 𝗂 * residue g_S 0"
      proof (subst Residue_theorem)
        show "g_S holomorphic_on UNIV - {0}"
          by (auto simp: g_S_def S_def intro!: holomorphic_intros)
      qed (insert R, auto simp: winding_number_circlepath_centre)
      also have "residue g_S 0 = S w"
      proof -
        have "g_S = (λz::complex. S (w + z) * N powr z * (1 + z2 / R2) / z)"
          by (auto simp: g_S_def divide_simps fun_eq_iff power2_eq_square
                   simp del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
        moreover from N have "residue  0 = S w"
          by (subst residue_simple'[of X])
             (auto intro!: holomorphic_intros simp: S_def)
        ultimately show ?thesis by (simp only:)
      qed
      finally have "2 * pi * 𝗂 * S w = ∮[circlepath 0 R] g_S" ..

      ― ‹We split this integral into integrals along two semicircles in the left and right
          half-plane, respectively:›
      also have " = ∮[part_circlepath 0 R (-pi/2) (3*pi/2)] g_S"
      proof (rule Cauchy_theorem_homotopic_loops)
        show "homotopic_loops (-{0}) (circlepath 0 R)
                (part_circlepath 0 R (- pi / 2) (3 * pi / 2))" unfolding circlepath_def using R
          by (intro homotopic_loops_part_circlepath[where k = 1]) auto
      qed (auto simp: g_S_def S_def intro!: holomorphic_intros)
      also have " = ∮[A +++ -A] g_S"
      proof (rule Cauchy_theorem_homotopic_paths)
        have *: "-A = part_circlepath 0 R (pi/2) (3*pi/2)" unfolding A_def
          by (intro part_circlepath_mirror[where k = 0]) auto
        from R show "homotopic_paths (-{0}) (part_circlepath 0 R (-pi/2) (3*pi/2)) (A +++ -A)"
          unfolding * unfolding A_def
          by (intro homotopic_paths_part_circlepath) (auto dest!: in_path_image_part_circlepath)
      qed (auto simp: g_S_def S_def A_def exp_eq_polar intro!: holomorphic_intros)
      also have " = ∮[A] g_S + ∮[-A] g_S" using R
        by (intro contour_integral_join contour_integrable_holomorphic_simple[of _ "-{0}"])
           (auto simp: A_def g_S_def S_def path_image_mirror dest!: in_path_image_part_circlepath
                 intro!: holomorphic_intros)
      also have "∮[-A] g_S = -∮[A] (λx. g_S (-x))"
        by (simp add: A_def contour_integral_mirror contour_integral_neg)
      finally have integral2: "2 * pi * 𝗂 * S w = ∮[A] g_S - ∮[A] (λx. g_S (-x))"
        by simp

      ― ‹Next, we show a small bounding lemma that we will need for the final estimate:›
      have circle_bound: "norm (1 / z + z / R2)  2 / R" if [simp]: "norm z = R" for z :: complex
      proof -
        have "norm (1 / z + z / R2)  1 / R + 1 / R"
          by (intro order.trans[OF norm_triangle_ineq] add_mono)
             (insert R, simp_all add: norm_divide norm_mult power2_eq_square)
        thus ?thesis by simp
      qed

      ― ‹The next bound differs somewhat from Newman's, but it works just as well.
          Its purpose is to bound the contribution of the two short horizontal line segments.›
      have B12_bound: "norm (integral {- δ..0} (λx. g (x + R' * 𝗂)))  3 * M / R / ln N"
        (is "?I  _") if "¦R'¦ = R" for R' 
      proof -
        have "?I  integral {-δ..0} (λx. 3 * M / R * N powr x)"
        proof (rule integral_norm_bound_integral)
          fix x assume x: "x  {-δ..0}"
          define z where "z = x + 𝗂 * R'"
          from R that have [simp]: "z  0" "Re z = x" "Im z = R'"
            by (auto simp: z_def complex_eq_iff)
          from x R that have "z  X'" by (auto simp: z_def X'_def in_cbox_complex_iff)
          from x R that have "norm z  δ + R"
            by (intro order.trans[OF cmod_le add_mono]) auto
      
          hence "norm (1 / z + z / R2)  1 / R + (δ / R + 1) / R"
            using R that abs_Im_le_cmod[of z]
            by (intro order.trans[OF norm_triangle_ineq add_mono])
               (auto simp: norm_divide norm_mult power2_eq_square field_simps )
          also have "δ / R  1" using δ R by auto
          finally have "norm (1 / z + z / R2)  3 / R"
            using R by (simp add: divide_right_mono)
          hence "norm (g z)  M * N powr x * (3 / R)"
            unfolding g_def norm_mult using M  0 z  X'
            by (intro mult_mono mult_nonneg_nonneg M) (auto simp: norm_powr_real_powr)
          thus "norm (g (x + R' * 𝗂))  3 * M / R * N powr x" by (simp add: mult_ac z_def)
        qed (insert N R l that δ, auto intro!: integrable_continuous_real continuous_intros
                                  simp: g_def X_def complex_eq_iff in_box_complex_iff)
        also have " = 3 * M / R * integral {-δ..0} (λx. N powr x)" by simp
        also have "((λx. N powr x) has_integral (N powr 0 / ln N - N powr (-δ) / ln N)) {-δ..0}"
          using δ N
          by (intro fundamental_theorem_of_calculus)
             (auto simp: has_real_derivative_iff_has_vector_derivative [symmetric] powr_def
                   intro!: derivative_eq_intros)
        hence "integral {-δ..0} (λx. N powr x) = 1 / ln (real N) - real N powr - δ / ln (real N)"
          using N by (simp add: has_integral_iff)
        also have "  1 / ln (real N)" using N by simp
        finally show ?thesis using M R by (simp add: mult_left_mono divide_right_mono)
      qed

      ― ‹We combine the two results from the residue theorem and obtain an integral
          representation of the difference between the partial sums and the limit:›
      have "2 * pi * 𝗂 * (f w - S w) =
              ∮[A] g - ∮[A] g_S + ∮[A] (λx. g_S (-x)) + ∮[B1] g + ∮[B3] g + ∮[B2] g"
        unfolding ring_distribs integral1 integral2 by (simp add: algebra_simps)
      also have "∮[A] g - ∮[A] g_S = ∮[A] (λx. g x - g_S x)" using path_images
        by (intro contour_integral_diff [symmetric])
           (auto intro!: contour_integrable_holomorphic_simple[of _ "X - {0}"] holomorphic_intros
                 simp: g_S_def g_holo S_def)
      also have " = ∮[A] g_rem"
        by (simp add: g_rem_def g_def g_S_def algebra_simps rem_def)
      finally have "2 * pi * 𝗂 * (f w - S w) =
                      ∮[A] g_rem + ∮[A] (λx. g_S (- x)) + ∮[B1] g + ∮[B3] g + ∮[B2] g" .

      ― ‹We now bound each of these integrals individually:›
      also have "norm   2 * C * pi / R  +  2 * C * pi * (1 / N + 1 / R)  +  3 * M / R / ln N  +
                             3 * M / R / ln N  +  6 * R * M * N powr (-δ) / δ"
      proof (rule order.trans[OF norm_triangle_ineq] add_mono)+
        have "∮[B1] g = -∮[reversepath B1] g" by (simp add: contour_integral_reversepath)
        also have "∮[reversepath B1] g = integral {-δ..0} (λx. g (x + R * 𝗂))"
          unfolding B1_def reversepath_linepath using δ
          by (subst contour_integral_linepath_same_Im) auto
        also have "norm (-) = norm " by simp
        also have "  3 * M / R / ln N" using R by (intro B12_bound) auto
        finally show "norm (∮[B1] g)  " .
      next
        have "∮[B3] g = integral {-δ..0} (λx. g (x + (-R) * 𝗂))" unfolding B3_def using δ
          by (subst contour_integral_linepath_same_Im) auto
        also have "norm   3 * M / R / ln N" using R by (intro B12_bound) auto
        finally show "norm (∮[B3] g)  " .
      next
        have "norm (∮[B2] g)  M * N powr (-δ) * (3 / δ) *
                norm (Complex (- δ) (-R) - Complex (- δ) R)" unfolding B2_def
        proof ((rule contour_integral_bound_linepath; (fold B2_def)?), goal_cases)
          case (3 z)
          from 3 δ R have [simp]: "z  0" and Re_z: "Re z = -δ" and Im_z: "Im z  {-R..R}"
            by (auto simp: closed_segment_same_Re closed_segment_eq_real_ivl)
          from 3 have "z  X'" using R δ path_images by (auto simp: B2_def)
          from 3 δ R have "norm z  sqrt (δ^2 + R^2)" unfolding cmod_def using Re_z Im_z
            by (intro real_sqrt_le_mono add_mono) (auto simp: power2_le_iff_abs_le)
          from power_mono[OF this, of 2] have norm_sqr: "norm z ^ 2  δ2 + R2" by simp
    
          have "norm (1 / z + z / R2)  (1 + (norm z)2 / R2) / δ"
            unfolding add_divide_distrib using δ R abs_Re_le_cmod[of z]
            by (intro order.trans[OF norm_triangle_ineq] add_mono)
               (auto simp: norm_divide norm_mult field_simps power2_eq_square Re_z)
          also have "  (1 + (1 + δ2 / R2)) / δ" using δ R z  X' norm_sqr unfolding X'_def
            by (intro divide_right_mono add_left_mono)
               (auto simp: field_simps in_cbox_complex_iff intro!: power_mono)
          also have "δ2 / R2  1"
            using δ R by (auto simp: field_simps intro!: power_mono)
          finally have "norm (1 / z + z / R2)  3 / δ" using δ by(simp add: divide_right_mono)
          with z  X' show "norm (g z)  M * N powr (-δ) * (3 / δ)" unfolding g_def norm_mult
            by (intro mult_mono mult_nonneg_nonneg M) (auto simp: norm_powr_real_powr Re_z)
        qed (insert path_images M δ, auto intro!: contour_integrable_holomorphic_simple[OF g_holo])
        thus "norm (∮[B2] g)  6 * R * M * N powr (-δ) / δ"
          using R by (simp add: field_simps cmod_def real_sqrt_mult)
      next
        have "norm (∮[A] (λx. g_S (- x)))  (2 * C / (real N * R) + 2 * C / R2) * 
                                R * ((pi/2) - (-pi/2))" unfolding A_def
        proof ((rule contour_integral_bound_part_circlepath_strong[where k = "{R * 𝗂, -R*𝗂}"];
               (fold A_def)?), goal_cases)
          case (6 z)
          hence [simp]: "z  0" and "norm z = R" using R
            by (auto simp: A_def dest!: in_path_image_part_circlepath)
          from 6 have "Re z  0"
            using norm z = R by (auto simp: cmod_def abs_if complex_eq_iff split: if_splits)
          with 6 have "Re z > 0" using image_A by auto
          have "S (w - z) = (k = 1..N. fds_nth F k / of_nat k powr (w - z))"
            by (simp add: S_def eval_fds_truncate)
          also have "norm   C * N powr Re z * (1 / N + 1 / Re z)"
            using Re z > 0 w N by (intro newman_ingham_aux2 C) auto
          finally have "norm (S (w - z))  " .
          hence "norm (g_S (-z)) 
                   (C * N powr (Re z) * (1 / N + 1 / Re z)) * N powr (-Re z) * (2 * Re z / R2)"
            unfolding g_S_def norm_mult 
            using newman_ingham_aux1[OF _ norm z = R] Re z > 0 C  1 R
            by (intro mult_mono mult_nonneg_nonneg circle_bound)
               (auto simp: norm_powr_real_powr norm_uminus_minus)
          also have " = 2 * C * (Re z / N + 1) / R2" using R N Re z > 0
            by (simp add: powr_minus algebra_simps)
          also have "  2 * C / (N * R) + 2 * C / R2" unfolding add_divide_distrib ring_distribs
            using R N abs_Re_le_cmod[of z] norm z = R Re z > 0 C  1
            by (intro add_mono) (auto simp: power2_eq_square field_simps mult_mono)
          finally show ?case .
        qed (insert R N image_A C, auto intro!: contour_integrable_holomorphic_simple[of _ "-{0}"]
                                                holomorphic_intros simp: g_S_def S_def)
        also have " = 2 * C * pi * (1 / N + 1 / R)" using R N
          by (simp add: power2_eq_square field_simps)
        finally show "norm (∮[A] (λx. g_S (- x)))  " .
      next
        have "norm (∮[A] g_rem)  (2 * C / R2) * R * ((pi/2) - (-pi/2))" unfolding A_def
        proof ((rule contour_integral_bound_part_circlepath_strong[where k = "{R * 𝗂, -R*𝗂}"];
               (fold A_def)?), goal_cases)
          case (6 z)
          hence [simp]: "z  0" and "norm z = R" using R
            by (auto simp: A_def dest!: in_path_image_part_circlepath)
          from 6 have "Re z  0"
            using norm z = R by (auto simp: cmod_def abs_if complex_eq_iff split: if_splits)
          with 6 have "Re z > 0" using image_A by auto
    
          have summable: "summable (λn. C * (1 / (Suc n + N) powr (Re w + Re z)))"
            using summable_hurwitz_zeta_real[of "Re w + Re z" "Suc N"] Re z > 0 w
            unfolding powr_minus by (intro summable_mult) (auto simp: field_simps)
          have "rem (w + z) = (n. fds_nth F (Suc n + N) / (Suc n + N) powr (w + z))"
            using Re z > 0 w by (simp add: rem_altdef eval_fds_remainder)
          also have "norm   (n. C / (Suc n + N) powr Re (w + z))" using summable
            by (intro norm_suminf_le)
               (auto simp: norm_divide norm_powr_real_powr intro!: divide_right_mono C)
          also have " = (n. C * (Suc n + N) powr -Re (w + z))"
            unfolding powr_minus by (simp add: field_simps)
          also have " = C * (n. (Suc n + N) powr -Re (w + z))"
            using summable_hurwitz_zeta_real[of "Re w + Re z" "Suc N"] Re z > 0 w
            by (subst suminf_mult) (auto simp: add_ac)
          also have "(n. (Suc n + N) powr -Re (w + z)) 
                       N powr (1 - Re (w + z)) / (Re (w + z) - 1)"
            using Re z > 0 w N hurwitz_zeta_real_bound_aux[of N "Re (w + z)"]
            by (auto simp: add_ac)
          also have "  N powr -Re z / Re z"
            using w N Re z > 0 by (intro frac_le powr_mono) auto
          finally have "norm (rem (w + z))  C / (Re z * N powr Re z)"
            using C by (simp add: mult_left_mono mult_right_mono powr_minus field_simps)
          hence "norm (g_rem z)  (C / (Re z * N powr Re z)) * N powr (Re z) * (2 * Re z / R2)"
            unfolding g_rem_def norm_mult
            using newman_ingham_aux1[OF _ norm z = R] R Re z > 0 C
            by (intro mult_mono mult_nonneg_nonneg circle_bound)
               (auto simp: norm_powr_real_powr norm_uminus_minus)
          also have " = 2 * C / R2" using R N Re z > 0
            by (simp add: powr_minus field_simps)
          finally show ?case .
        next
          show "g_rem contour_integrable_on A" using path_images
            by (auto simp: g_rem_def rem_def S_def
                     intro!: contour_integrable_holomorphic_simple[of _ "X-{0}"] holomorphic_intros)
        qed (insert R N C, auto)
        also have "(2 * C / R2) * R * ((pi/2) - (-pi/2)) = 2 * C * pi / R"
          using R by (simp add: power2_eq_square field_simps)
        finally show "norm (∮[A] g_rem)  " .
      qed
      also have " = 4*C*pi/R + 2*C*pi/N + 6*M/R / ln N + 6*R*M*N powr - δ / δ"
        by (simp add: algebra_simps)
      also have " = 2*pi * (2*C/R + C/N + 3*M / (pi*R*ln N) + 3*R*M / (δ*pi * N powr δ))"
        by (simp add: field_simps powr_minus )
      also have "norm (2 * pi * 𝗂 * (f w - S w)) = 2 * pi * norm (f w - S w)"
        by (simp add: norm_mult)
      finally have "norm (f w - S w)  bound N" by (simp add: bound_def)
      also have "bound N < ε" by fact
      finally show "norm (f w - S w) < ε" .
    qed
  qed
  thus "fds_converges F w"
    by (auto simp: fds_converges_altdef2 intro: convergentI)
  thus "eval_fds F w = f w"
    using (λN. eval_fds (fds_truncate N F) w)  f w
    by (intro tendsto_unique[OF _ tendsto_eval_fds_truncate]) auto
qed

text ‹
  The theorem generalises in a trivial way; we can replace the requirement that the
  coefficients of $f(s)$ be $O(1)$ by $O(n^{\sigma-1})$ for some $\sigma\in\mathbb{R}$, then
  $f(s)$ converges for $\mathfrak{R}(s)>\sigma$. If it can be analytically continued to
  $\mathfrak{R}(s)\geq\sigma$, it is also convergent there.
›
theorem Newman_Ingham:
  fixes F :: "complex fds" and f :: "complex  complex"
  assumes coeff_bound:   "fds_nth F  O(λn. n powr of_real (σ - 1))"
  assumes f_analytic:    "f analytic_on {s. Re s  σ}"
  assumes F_conv_f:      "s. Re s > σ  eval_fds F s = f s"
  assumes w:             "Re w  σ"
  shows   "fds_converges F w" and "eval_fds F w = f w"
proof -
  define F' where "F' = fds_shift (-of_real (σ - 1)) F"
  define f' where "f' = f  (λs. s + of_real (σ - 1))"

  have "fds_nth F' = (λn. fds_nth F n * of_nat n powr -of_real(σ - 1))"
    by (auto simp: fun_eq_iff F'_def)
  also have "  O(λn. of_nat n powr of_real (σ - 1) * of_nat n powr -of_real(σ - 1))"
    by (intro landau_o.big.mult_right assms)
  also have "(λn. of_nat n powr of_real (σ - 1) * of_nat n powr -of_real (σ - 1))  Θ(λ_. 1)"
    by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 0]])
       (auto simp: powr_minus powr_diff)
  finally have bigo: "fds_nth F'  O(λ_. 1)" .

  from f_analytic have analytic: "f' analytic_on {s. Re s  1}" unfolding f'_def
    by (intro analytic_on_compose_gen[OF _ f_analytic]) (auto intro!: analytic_intros)

  have F'_f: "eval_fds F' s = f' s" if "Re s > 1" for s
    using assms that by (auto simp: F'_def f'_def algebra_simps)

  have w': "1  Re (w - of_real (σ - 1))"
    using w by simp
  
  have 1: "fds_converges F' (w - of_real (σ - 1))"
    using bigo analytic F'_f w' by (rule Newman_Ingham_1)
  thus "fds_converges F w" by (auto simp: F'_def)

  have 2: "eval_fds F' (w - of_real (σ - 1)) = f' (w - of_real (σ - 1))"
    using bigo analytic F'_f w' by (rule Newman_Ingham_1)
  thus "eval_fds F w = f w"
    using assms by (simp add: F'_def f'_def)
qed

end