Theory Perron_Formula

theory Perron_Formula
imports
  "PNT_Remainder_Library"
  "PNT_Subsummable"
begin
unbundle pnt_syntax

section ‹Perron's formula›

text ‹This version of Perron's theorem is referenced to:
  ‹Perron's Formula and the Prime Number Theorem for Automorphic L-Functions, Jianya Liu, Y. Ye››

text ‹A contour integral estimation lemma that will be used
  both in proof of Perron's formula and the prime number theorem.›

lemma perron_aux_3':
  fixes f :: "complex ⇒ complex" and a b B T :: real
  assumes Ha: "0 < a" and Hb: "0 < b" and hT: "0 < T"
    and Hf: "⋀t. t ∈ {-T..T} ⟹ ∥f (Complex b t)∥ ≤ B"
    and Hf': "(λs. f s * a powr s / s) contour_integrable_on (linepath (Complex b (-T)) (Complex b T))"
  shows "∥1 / (2 * pi * 𝗂) * contour_integral (linepath (Complex b (-T)) (Complex b T)) (λs. f s * a powr s / s)∥
       ≤ B * a powr b * ln (1 + T / b)"
proof -
  define path where "path ≡ linepath (Complex b (-T)) (Complex b T)"
  define t' where "t' t ≡ Complex (Re (Complex b (-T))) t" for t
  define g where "g t ≡ f (Complex b t) * a powr (Complex b t) / Complex b t * 𝗂" for t
  have "∥f (Complex b 0)∥ ≤ B" using hT by (auto intro: Hf [of 0])
  hence hB: "0 ≤ B" using hT by (smt (verit) norm_ge_zero)
  have "((λt. f (t' t) * a powr (t' t) / (t' t) * 𝗂)
        has_integral contour_integral path (λs. f s * a powr s / s)) {Im (Complex b (-T))..Im (Complex b T)}"
    unfolding t'_def using hT
    by (intro integral_linepath_same_Re, unfold path_def)
       (auto intro: has_contour_integral_integral Hf')
  hence h_int: "(g has_integral contour_integral path (λs. f s * a powr s / s)) {-T..T}"
    unfolding g_def t'_def by auto
  hence int: "g integrable_on {-T..T}" by (rule has_integral_integrable)
  have "contour_integral path (λs. f s * a powr s / s) = integral {-T..T} g"
    using h_int by (rule integral_unique [symmetric])
  also have "∥…∥ ≤ integral {-T..T} (λt. 2 * B * a powr b / (b + ¦t¦))"
  proof (rule integral_norm_bound_integral, goal_cases)
    case 1 from int show ?case .
    case 2 show ?case
      by (intro integrable_continuous_interval continuous_intros)
         (use Hb in auto)
  next
    fix t assume *: "t ∈ {-T..T}"
    have "(b + ¦t¦)⇧2 - 4 * (b⇧2 + t⇧2) = - 3 * (b - ¦t¦)⇧2 + - 4 * b * ¦t¦"
      by (simp add: field_simps power2_eq_square)
    also have "… ≤ 0" using Hb by (intro add_nonpos_nonpos) auto
    finally have "(b + ¦t¦)⇧2 - 4 * (b⇧2 + t⇧2) ≤ 0" .
    hence "b + ¦t¦ ≤ 2 * ∥Complex b t∥"
      unfolding cmod_def by (auto intro: power2_le_imp_le)
    hence "a powr b / ∥Complex b t∥ ≤ a powr b / ((b + ¦t¦) / 2)"
      using Hb by (intro divide_left_mono) (auto intro!: mult_pos_pos)
    hence "a powr b / ∥Complex b t∥ * ∥f (Complex b t)∥ ≤ a powr b / ((b + ¦t¦) / 2) * B"
      by (insert Hf [OF *], rule mult_mono) (use Hb in auto)
    thus "∥g t∥ ≤ 2 * B * a powr b / (b + ¦t¦)"
      unfolding g_def
      by (auto simp add: norm_mult norm_divide)
         (subst norm_powr_real_powr, insert Ha, auto simp add: mult_ac)
  qed
  also have "… = 2 * B * a powr b * integral {-T..T} (λt. 1 / (b + ¦t¦))"
    by (subst divide_inverse, subst integral_mult_right) (simp add: inverse_eq_divide)
  also have "… = 4 * B * a powr b * integral {0..T} (λt. 1 / (b + ¦t¦))"
  proof -
    let ?f = "λt. 1 / (b + ¦t¦)"
    have "integral {-T..0} ?f + integral {0..T} ?f = integral {-T..T} ?f"
      by (intro Henstock_Kurzweil_Integration.integral_combine
                integrable_continuous_interval continuous_intros)
         (use Hb hT in auto)
    moreover have "integral {-T..-0} (λt. ?f (-t)) = integral {0..T} ?f"
      by (rule Henstock_Kurzweil_Integration.integral_reflect_real)
    hence "integral {-T..0} ?f = integral {0..T} ?f" by auto
    ultimately show ?thesis by auto
  qed
  also have "… = 4 * B * a powr b * ln (1 + T / b)"
  proof -
    have "((λt. 1 / (b + ¦t¦)) has_integral (ln (b + T) - ln (b + 0))) {0..T}"
    proof (rule fundamental_theorem_of_calculus, goal_cases)
      case 1 show ?case using hT by auto
    next
      fix x assume *: "x ∈ {0..T}"
      have "((λx. ln (b + x)) has_real_derivative 1 / (b + x) * (0 + 1)) (at x within {0..T})"
        by (intro derivative_intros) (use Hb * in auto)
      thus "((λx. ln (b + x)) has_vector_derivative 1 / (b + ¦x¦)) (at x within {0..T})"
        using * by (subst has_real_derivative_iff_has_vector_derivative [symmetric]) auto
    qed
    moreover have "ln (b + T) - ln (b + 0) = ln (1 + T / b)"
      using Hb hT by (simp add: ln_div field_simps)
    ultimately show ?thesis by auto
  qed
  finally have "∥1 / (2 * pi * 𝗂) * contour_integral path (λs. f s * a powr s / s)∥
    ≤ 1 / (2*pi) * 4 * B * a powr b * ln (1 + T / b)"
    by (simp add: norm_divide norm_mult field_simps)
  also have "… ≤ 1 * B * a powr b * ln (1 + T / b)"
  proof -
    have "1 / (2*pi) * 4 ≤ 1" using pi_gt3 by auto
    thus ?thesis by (intro mult_right_mono) (use hT Hb hB in auto)
  qed
  finally show ?thesis unfolding path_def by auto
qed

locale perron_locale =
  fixes b B H T x :: real and f :: "complex fds"
  assumes Hb: "0 < b" and hT: "b ≤ T"
    and Hb': "abs_conv_abscissa f < b"
    and hH: "1 < H" and hH': "b + 1 ≤ H" and Hx: "0 < x"
    and hB: "(∑`n ≥ 1. ∥fds_nth f n∥ / n nat_powr b) ≤ B"
begin
definition r where "r a ≡
  if a ≠ 1 then min (1 / (2 * T * ¦ln a¦)) (2 + ln (T / b))
  else (2 + ln (T / b))"
definition path where "path ≡ linepath (Complex b (-T)) (Complex b T)"
definition img_path where "img_path ≡ path_image path"
definition σ⇩a where "σ⇩a ≡ abs_conv_abscissa f"
definition region where "region = {n :: nat. x - x / H ≤ n ∧ n ≤ x + x / H}"
definition F where "F (a :: real) ≡
  1 / (2 * pi * 𝗂) * contour_integral path (λs. a powr s / s) - (if 1 ≤ a then 1 else 0)"
definition F' where "F' (n :: nat) ≡ F (x / n)"

lemma hT': "0 < T" using Hb hT by auto
lemma cond: "0 < b" "b ≤ T" "0 < T" using Hb hT hT' by auto

lemma perron_integrable:
  assumes "(0 :: real) < a"
  shows "(λs. a powr s / s) contour_integrable_on (linepath (Complex b (-T)) (Complex b T))"
using cond assms
by (intro contour_integrable_continuous_linepath continuous_intros)
   (auto simp add: closed_segment_def legacy_Complex_simps field_simps)

lemma perron_aux_1':
  fixes U :: real
  assumes hU: "0 < U" and Ha: "1 < a"
  shows "∥F a∥ ≤ 1 / pi * a powr b / (T * ¦ln a¦) + a powr -U * T / (pi * U)"
proof -
  define f where "f ≡ λs :: complex. a powr s / s"
  note assms' = cond assms this
  define P⇩1 where "P⇩1 ≡ linepath (Complex (-U) (-T)) (Complex b (-T))"
  define P⇩2 where "P⇩2 ≡ linepath (Complex b (-T)) (Complex b T)"
  define P⇩3 where "P⇩3 ≡ linepath (Complex b T) (Complex (-U) T)"
  define P⇩4 where "P⇩4 ≡ linepath (Complex (-U) T) (Complex (-U) (-T))"
  define P where "P ≡ P⇩1 +++ P⇩2 +++ P⇩3 +++ P⇩4"
  define I⇩1 I⇩2 I⇩3 I⇩4 where
    "I⇩1 ≡ contour_integral P⇩1 f" and "I⇩2 ≡ contour_integral P⇩2 f" and
    "I⇩3 ≡ contour_integral P⇩3 f" and "I⇩4 ≡ contour_integral P⇩4 f"
  define rpath where "rpath ≡ rectpath (Complex (-U) (-T)) (Complex b T)"
  note P_defs = P_def P⇩1_def P⇩2_def P⇩3_def P⇩4_def
  note I_defs = I⇩1_def I⇩2_def I⇩3_def I⇩4_def
  have 1: "⋀A B x. A ⊆ B ⟹ x ∉ A ⟹ A ⊆ B - {x}" by auto
  have "path_image (rectpath (Complex (- U) (- T)) (Complex b T))
        ⊆ cbox (Complex (- U) (- T)) (Complex b T) - {0}"
    using assms'
    by (intro 1 path_image_rectpath_subset_cbox)
       (auto simp add: path_image_rectpath)
  moreover have "0 ∈ box (Complex (- U) (- T)) (Complex b T)"
    using assms' by (simp add: mem_box Basis_complex_def)
  ultimately have
    "((λs. a powr s / (s - 0)) has_contour_integral
      2 * pi * 𝗂 * winding_number rpath 0 * a powr (0 :: complex)) rpath"
    "winding_number rpath 0 = 1"
    unfolding rpath_def
    by (intro Cauchy_integral_formula_convex_simple
              [where S = "cbox (Complex (-U) (-T)) (Complex b T)"])
       (auto intro!: assms' holomorphic_on_powr_right winding_number_rectpath
             simp add: mem_box Basis_complex_def)
  hence "(f has_contour_integral 2 * pi * 𝗂) rpath" unfolding f_def using Ha by auto
  hence 2: "(f has_contour_integral 2 * pi * 𝗂) P"
    unfolding rpath_def P_defs rectpath_def Let_def by simp
  hence "f contour_integrable_on P" by (intro has_contour_integral_integrable) (use 2 in auto)
  hence 3: "f contour_integrable_on P⇩1" "f contour_integrable_on P⇩2"
           "f contour_integrable_on P⇩3" "f contour_integrable_on P⇩4" unfolding P_defs by auto
  from 2 have "I⇩1 + I⇩2 + I⇩3 + I⇩4 = 2 * pi * 𝗂" unfolding P_defs I_defs by (rule has_chain_integral_chain_integral4)
  hence "I⇩2 - 2 * pi * 𝗂 = - (I⇩1 + I⇩3 + I⇩4)" by (simp add: field_simps)
  hence "∥I⇩2 - 2 * pi * 𝗂∥ = ∥- (I⇩1 + I⇩3 + I⇩4)∥" by auto
  also have "… = ∥I⇩1 + I⇩3 + I⇩4∥" by (rule norm_minus_cancel)
  also have "… ≤ ∥I⇩1 + I⇩3∥ + ∥I⇩4∥" by (rule norm_triangle_ineq)
  also have "… ≤ ∥I⇩1∥ + ∥I⇩3∥ + ∥I⇩4∥" using norm_triangle_ineq by auto
  finally have *: "∥I⇩2 - 2 * pi * 𝗂∥ ≤ ∥I⇩1∥ + ∥I⇩3∥ + ∥I⇩4∥" .
  have I⇩2_val: "∥I⇩2 / (2 * pi * 𝗂) - 1∥ ≤ 1 / (2*pi) * (∥I⇩1∥ + ∥I⇩3∥ + ∥I⇩4∥)"
  proof -
    have "I⇩2 - 2 * pi * 𝗂 = (I⇩2 / (2 * pi * 𝗂) - 1) * (2 * pi * 𝗂)" by (auto simp add: field_simps)
    hence "∥I⇩2 - 2 * pi * 𝗂∥ = ∥(I⇩2 / (2 * pi * 𝗂) - 1) * (2 * pi * 𝗂)∥" by auto
    also have "… = ∥I⇩2 / (2 * pi * 𝗂) - 1∥ * (2*pi)" by (auto simp add: norm_mult)
    finally have "∥I⇩2 / (2 * pi * 𝗂) - 1∥ = 1 / (2*pi) * ∥I⇩2 - 2 * pi * 𝗂∥" by auto
    also have "… ≤ 1 / (2*pi) * (∥I⇩1∥ + ∥I⇩3∥ + ∥I⇩4∥)"
      using * by (subst mult_le_cancel_left_pos) auto
    finally show ?thesis .
  qed
  define Q where "Q t ≡ linepath (Complex (-U) t) (Complex b t)" for t
  define g where "g t ≡ contour_integral (Q t) f" for t
  have Q_1: "(f has_contour_integral I⇩1) (Q (-T))"
    using 3(1) unfolding P⇩1_def I⇩1_def Q_def
    by (rule has_contour_integral_integral)
  have Q_2: "(f has_contour_integral -I⇩3) (Q T)"
    using 3(3) unfolding P⇩3_def I⇩3_def Q_def
    by (subst contour_integral_reversepath [symmetric],
        auto intro!: has_contour_integral_integral)
       (subst contour_integrable_reversepath_eq [symmetric], auto)
  have subst_I⇩1_I⇩3: "I⇩1 = g (- T)" "I⇩3 = - g T"
    using Q_1 Q_2 unfolding g_def by (auto simp add: contour_integral_unique)
  have g_bound: "∥g t∥ ≤ a powr b / (T * ¦ln a¦)"
    when Ht: "¦t¦ = T" for t
  proof -
    have "(f has_contour_integral g t) (Q t)" proof -
      consider "t = T" | "t = -T" using Ht by fastforce
      hence "f contour_integrable_on Q t" using Q_1 Q_2 by (metis has_contour_integral_integrable)
      thus ?thesis unfolding g_def by (rule has_contour_integral_integral)
    qed
    hence "((λx. a powr (x + Im (Complex (-U) t) * 𝗂) / (x + Im (Complex (-U) t) * 𝗂)) has_integral (g t))
          {Re (Complex (-U) t) .. Re (Complex b t)}"
      unfolding Q_def f_def
      by (subst has_contour_integral_linepath_same_Im_iff [symmetric])
         (use hU Hb in auto)
    hence *: "((λx. a powr (x + t * 𝗂) / (x + t * 𝗂)) has_integral g t) {-U..b}" by auto
    hence "∥g t∥ = ∥integral {-U..b} (λx. a powr (x + t * 𝗂) / (x + t * 𝗂))∥" by (auto simp add: integral_unique)
    also have "… ≤ integral {-U..b} (λx. a powr x / T)"
    proof (rule integral_norm_bound_integral)
      show "(λx. a powr (x + t * 𝗂) / (x + t * 𝗂)) integrable_on {-U..b}" using * by auto
      have "(λx. a powr x / (of_real T)) integrable_on {-U..b}"
        by (intro iffD2 [OF integrable_on_cdivide_iff] powr_integrable) (use hU Ha Hb hT' in auto)
      thus "(λx. a powr x / T) integrable_on {-U..b}" by auto
    next
      fix x assume "x ∈ {-U..b}"
      have "∥a powr (x + t * 𝗂)∥ = Re a powr Re (x + t * 𝗂)" by (rule norm_powr_real_powr) (use Ha in auto)
      also have "… = a powr x" by auto
      finally have *: "∥a powr (x + t * 𝗂)∥ = a powr x" .
      have "T = ¦Im (x + t * 𝗂)¦" using Ht by auto
      also have "… ≤ ∥x + t * 𝗂∥" by (rule abs_Im_le_cmod)
      finally have "T ≤ ∥x + t * 𝗂∥" .
      with * show "∥a powr (x + t * 𝗂) / (x + t * 𝗂)∥ ≤ a powr x / T"
        by (subst norm_divide) (rule frac_le, use assms' in auto)
    qed
    also have "… = integral {-U..b} (λx. a powr x) / T" by auto
    also have "… ≤ a powr b / (T * ¦ln a¦)"
    proof -
      have "integral {-U..b} (λx. a powr x) ≤ a powr b / ¦ln a¦"
        by (rule powr_integral_bound_gt_1) (use hU Ha Hb in auto)
      thus ?thesis using hT' by (auto simp add: field_simps)
    qed
    finally show ?thesis .
  qed
  have "∥I⇩4∥ ≤ a powr -U / U * ∥Complex (- U) (- T) - Complex (- U) T∥"
  proof -
    have "f contour_integrable_on P⇩4" by (rule 3)
    moreover have "0 ≤ a powr - U / U" using hU by auto
    moreover have "∥f z∥ ≤ a powr - U / U"
      when *: "z ∈ closed_segment (Complex (- U) T) (Complex (- U) (- T))" for z
    proof -
      from * have Re_z: "Re z = - U"
        unfolding closed_segment_def
        by (auto simp add: legacy_Complex_simps field_simps)
      hence "U = ¦Re z¦" using hU by auto
      also have "… ≤ ∥z∥" by (rule abs_Re_le_cmod)
      finally have zmod: "U ≤ ∥z∥" .
      have "∥f z∥ = ∥a powr z∥ / ∥z∥" unfolding f_def by (rule norm_divide)
      also have "… ≤ a powr - U / U"
        by (subst norm_powr_real_powr, use Ha in auto)
           (rule frac_le, use hU Re_z zmod in auto)
      finally show ?thesis .
    qed
    ultimately show ?thesis unfolding I⇩4_def P⇩4_def by (rule contour_integral_bound_linepath)
  qed
  also have "… = a powr -U / U * (2 * T)"
  proof -
    have "sqrt ((2 * T)⇧2) = ¦2 * T¦" by (rule real_sqrt_abs)
    thus ?thesis using hT' by (auto simp add: field_simps legacy_Complex_simps)
  qed
  finally have I⇩4_bound: "∥I⇩4∥ ≤ a powr -U / U * (2 * T)" .
  have "∥I⇩2 / (2 * pi * 𝗂) - 1∥ ≤ 1 / (2*pi) * (∥g (- T)∥ + ∥- g T∥ + ∥I⇩4∥)"
    using I⇩2_val subst_I⇩1_I⇩3 by auto
  also have "… ≤ 1 / (2*pi) * (2 * a powr b / (T * ¦ln a¦) + a powr -U / U * (2*T))"
  proof -
    have "∥g T∥ ≤ a powr b / (T * ¦ln a¦)"
         "∥g (- T)∥ ≤ a powr b / (T * ¦ln a¦)"
      using hT' by (auto intro: g_bound)
    hence "∥g (- T)∥ + ∥- g T∥ + ∥I⇩4∥ ≤ 2 * a powr b / (T * ¦ln a¦) + a powr -U / U * (2*T)"
      using I⇩4_bound by auto
    thus ?thesis by (auto simp add: field_simps)
  qed
  also have "… = 1 / pi * a powr b / (T * ¦ln a¦) + a powr -U * T / (pi * U)"
    using hT' by (auto simp add: field_simps)
  finally show ?thesis
    using Ha unfolding I⇩2_def P⇩2_def f_def F_def path_def by auto
qed

lemma perron_aux_1:
  assumes Ha: "1 < a"
  shows "∥F a∥ ≤ 1 / pi * a powr b / (T * ¦ln a¦)" (is "_ ≤ ?x")
proof -
  let ?y = "λU :: real. a powr -U * T / (pi * U)"
  have "((λU :: real. ?x) ⤏ ?x) at_top" by auto
  moreover have "((λU. ?y U) ⤏ 0) at_top" using Ha by real_asymp
  ultimately have "((λU. ?x + ?y U) ⤏ ?x + 0) at_top" by (rule tendsto_add)
  hence "((λU. ?x + ?y U) ⤏ ?x) at_top" by auto
  moreover have "∥F a∥ ≤ ?x + ?y U" when hU: "0 < U" for U
    by (subst perron_aux_1' [OF hU Ha], standard)
  hence "∀⇩F U in at_top. ∥F a∥ ≤ ?x + ?y U"
    by (rule eventually_at_top_linorderI')
  ultimately show ?thesis
    by (intro tendsto_lowerbound) auto
qed

lemma perron_aux_2':
  fixes U :: real
  assumes hU: "0 < U" "b < U" and Ha: "0 < a ∧ a < 1"
  shows "∥F a∥ ≤ 1 / pi * a powr b / (T * ¦ln a¦) + a powr U * T / (pi * U)"
proof -
  define f where "f ≡ λs :: complex. a powr s / s"
  note assms' = cond assms hU
  define P⇩1 where "P⇩1 ≡ linepath (Complex b (-T)) (Complex U (-T))"
  define P⇩2 where "P⇩2 ≡ linepath (Complex U (-T)) (Complex U T)"
  define P⇩3 where "P⇩3 ≡ linepath (Complex U T) (Complex b T)"
  define P⇩4 where "P⇩4 ≡ linepath (Complex b T) (Complex b (-T))"
  define P where "P ≡ P⇩1 +++ P⇩2 +++ P⇩3 +++ P⇩4"
  define I⇩1 I⇩2 I⇩3 I⇩4 where
    "I⇩1 ≡ contour_integral P⇩1 f" and "I⇩2 ≡ contour_integral P⇩2 f" and
    "I⇩3 ≡ contour_integral P⇩3 f" and "I⇩4 ≡ contour_integral P⇩4 f"
  define rpath where "rpath ≡ rectpath (Complex b (- T)) (Complex U T)"
  note P_defs = P_def P⇩1_def P⇩2_def P⇩3_def P⇩4_def
  note I_defs = I⇩1_def I⇩2_def I⇩3_def I⇩4_def
  have "path_image (rectpath (Complex b (- T)) (Complex U T)) ⊆ cbox (Complex b (- T)) (Complex U T)"
    by (intro path_image_rectpath_subset_cbox) (use assms' in auto)
  moreover have "0 ∉ cbox (Complex b (- T)) (Complex U T)"
    using Hb unfolding cbox_def by (auto simp add: Basis_complex_def)
  ultimately have "((λs. a powr s / (s - 0)) has_contour_integral 0) rpath"
    unfolding rpath_def
    by (intro Cauchy_theorem_convex_simple
              [where S = "cbox (Complex b (- T)) (Complex U T)"])
       (auto intro!: holomorphic_on_powr_right holomorphic_on_divide)
  hence "(f has_contour_integral 0) rpath" unfolding f_def using Ha by auto
  hence 1: "(f has_contour_integral 0) P" unfolding rpath_def P_defs rectpath_def Let_def by simp
  hence "f contour_integrable_on P" by (intro has_contour_integral_integrable) (use 1 in auto)
  hence 2: "f contour_integrable_on P⇩1" "f contour_integrable_on P⇩2"
           "f contour_integrable_on P⇩3" "f contour_integrable_on P⇩4" unfolding P_defs by auto
  from 1 have "I⇩1 + I⇩2 + I⇩3 + I⇩4 = 0" unfolding P_defs I_defs by (rule has_chain_integral_chain_integral4)
  hence "I⇩4 = - (I⇩1 + I⇩2 + I⇩3)" by (metis neg_eq_iff_add_eq_0)
  hence "∥I⇩4∥ = ∥- (I⇩1 + I⇩2 + I⇩3)∥" by auto
  also have "… = ∥I⇩1 + I⇩2 + I⇩3∥" by (rule norm_minus_cancel)
  also have "… ≤ ∥I⇩1 + I⇩2∥ + ∥I⇩3∥" by (rule norm_triangle_ineq)
  also have "… ≤ ∥I⇩1∥ + ∥I⇩2∥ + ∥I⇩3∥" using norm_triangle_ineq by auto
  finally have "∥I⇩4∥ ≤ ∥I⇩1∥ + ∥I⇩2∥ + ∥I⇩3∥" .
  hence I⇩4_val: "∥I⇩4 / (2 * pi * 𝗂)∥ ≤ 1 / (2*pi) * (∥I⇩1∥ + ∥I⇩2∥ + ∥I⇩3∥)"
    by (auto simp add: norm_divide norm_mult field_simps)
  define Q where "Q t ≡ linepath (Complex b t) (Complex U t)" for t
  define g where "g t ≡ contour_integral (Q t) f" for t
  have Q_1: "(f has_contour_integral I⇩1) (Q (-T))"
    using 2(1) unfolding P⇩1_def I⇩1_def Q_def
    by (rule has_contour_integral_integral)
  have Q_2: "(f has_contour_integral -I⇩3) (Q T)"
    using 2(3) unfolding P⇩3_def I⇩3_def Q_def
    by (subst contour_integral_reversepath [symmetric],
        auto intro!: has_contour_integral_integral)
       (subst contour_integrable_reversepath_eq [symmetric], auto)
  have subst_I⇩1_I⇩3: "I⇩1 = g (- T)" "I⇩3 = - g T"
    using Q_1 Q_2 unfolding g_def by (auto simp add: contour_integral_unique)
  have g_bound: "∥g t∥ ≤ a powr b / (T * ¦ln a¦)"
    when Ht: "¦t¦ = T" for t
  proof -
    have "(f has_contour_integral g t) (Q t)" proof -
      consider "t = T" | "t = -T" using Ht by fastforce
      hence "f contour_integrable_on Q t" using Q_1 Q_2 by (metis has_contour_integral_integrable)
      thus ?thesis unfolding g_def by (rule has_contour_integral_integral)
    qed
    hence "((λx. a powr (x + Im (Complex b t) * 𝗂) / (x + Im (Complex b t) * 𝗂)) has_integral (g t))
          {Re (Complex b t) .. Re (Complex U t)}"
      unfolding Q_def f_def
      by (subst has_contour_integral_linepath_same_Im_iff [symmetric])
         (use assms' in auto)
    hence *: "((λx. a powr (x + t * 𝗂) / (x + t * 𝗂)) has_integral g t) {b..U}" by auto
    hence "∥g t∥ = ∥integral {b..U} (λx. a powr (x + t * 𝗂) / (x + t * 𝗂))∥" by (auto simp add: integral_unique)
    also have "… ≤ integral {b..U} (λx. a powr x / T)"
    proof (rule integral_norm_bound_integral)
      show "(λx. a powr (x + t * 𝗂) / (x + t * 𝗂)) integrable_on {b..U}" using * by auto
      have "(λx. a powr x / (of_real T)) integrable_on {b..U}"
        by (intro iffD2 [OF integrable_on_cdivide_iff] powr_integrable) (use assms' in auto)
      thus "(λx. a powr x / T) integrable_on {b..U}" by auto
    next
      fix x assume "x ∈ {b..U}"
      have "∥a powr (x + t * 𝗂)∥ = Re a powr Re (x + t * 𝗂)" by (rule norm_powr_real_powr) (use Ha in auto)
      also have "… = a powr x" by auto
      finally have 1: "∥a powr (x + t * 𝗂)∥ = a powr x" .
      have "T = ¦Im (x + t * 𝗂)¦" using Ht by auto
      also have "… ≤ ∥x + t * 𝗂∥" by (rule abs_Im_le_cmod)
      finally have 2: "T ≤ ∥x + t * 𝗂∥" .
      from 1 2 show "∥a powr (x + t * 𝗂) / (x + t * 𝗂)∥ ≤ a powr x / T"
        by (subst norm_divide) (rule frac_le, use hT' in auto)
    qed
    also have "… = integral {b..U} (λx. a powr x) / T" by auto
    also have "… ≤ a powr b / (T * ¦ln a¦)"
    proof -
      have "integral {b..U} (λx. a powr x) ≤ a powr b / ¦ln a¦"
        by (rule powr_integral_bound_lt_1) (use assms' in auto)
      thus ?thesis using hT' by (auto simp add: field_simps)
    qed
    finally show ?thesis .
  qed
  have "∥I⇩2∥ ≤ a powr U / U * ∥Complex U T - Complex U (- T)∥"
  proof -
    have "f contour_integrable_on P⇩2" by (rule 2)
    moreover have "0 ≤ a powr U / U" using hU by auto
    moreover have "∥f z∥ ≤ a powr U / U"
      when *: "z ∈ closed_segment (Complex U (- T)) (Complex U T)" for z
    proof -
      from * have Re_z: "Re z = U"
        unfolding closed_segment_def
        by (auto simp add: legacy_Complex_simps field_simps)
      hence "U = ¦Re z¦" using hU by auto
      also have "… ≤ ∥z∥" by (rule abs_Re_le_cmod)
      finally have zmod: "U ≤ ∥z∥" .
      have "∥f z∥ = ∥a powr z∥ / ∥z∥" unfolding f_def by (rule norm_divide)
      also have "… ≤ a powr U / U"
        by (subst norm_powr_real_powr, use Ha in auto)
           (rule frac_le, use hU Re_z zmod in auto)
      finally show ?thesis .
    qed
    ultimately show ?thesis unfolding I⇩2_def P⇩2_def by (rule contour_integral_bound_linepath)
  qed
  also have "… ≤ a powr U / U * (2 * T)"
  proof -
    have "sqrt ((2 * T)⇧2) = ¦2 * T¦" by (rule real_sqrt_abs)
    thus ?thesis using hT' by (simp add: field_simps legacy_Complex_simps)
  qed
  finally have I⇩2_bound: "∥I⇩2∥ ≤ a powr U / U * (2 * T)" .
  have "∥I⇩4 / (2 * pi * 𝗂)∥ ≤ 1 / (2*pi) * (∥g (- T)∥ + ∥I⇩2∥ + ∥- g T∥)"
    using I⇩4_val subst_I⇩1_I⇩3 by auto
  also have "… ≤ 1 / (2*pi) * (2 * a powr b / (T * ¦ln a¦) + a powr U / U * (2*T))"
  proof -
    have "∥g T∥ ≤ a powr b / (T * ¦ln a¦)"
         "∥g (- T)∥ ≤ a powr b / (T * ¦ln a¦)"
      using hT' by (auto intro: g_bound)
    hence "∥g (- T)∥ + ∥- g T∥ + ∥I⇩2∥ ≤ 2 * a powr b / (T * ¦ln a¦) + a powr U / U * (2*T)"
      using I⇩2_bound by auto
    thus ?thesis by (auto simp add: field_simps)
  qed
  also have "… = 1 / pi * a powr b / (T * ¦ln a¦) + a powr U * T / (pi * U)"
    using hT' by (auto simp add: field_simps)
  finally have "∥1 / (2 * pi * 𝗂) * contour_integral (reversepath P⇩4) f∥
    ≤ 1 / pi * a powr b / (T * ¦ln a¦) + a powr U * T / (pi * U)"
    unfolding I⇩4_def P⇩4_def by (subst contour_integral_reversepath) auto
  thus ?thesis using Ha unfolding I⇩4_def P⇩4_def f_def F_def path_def by auto
qed

lemma perron_aux_2:
  assumes Ha: "0 < a ∧ a < 1"
  shows "∥F a∥ ≤ 1 / pi * a powr b / (T * ¦ln a¦)" (is "_ ≤ ?x")
proof -
  let ?y = "λU :: real. a powr U * T / (pi * U)"
  have "((λU :: real. ?x) ⤏ ?x) at_top" by auto
  moreover have "((λU. ?y U) ⤏ 0) at_top" using Ha by real_asymp
  ultimately have "((λU. ?x + ?y U) ⤏ ?x + 0) at_top" by (rule tendsto_add)
  hence "((λU. ?x + ?y U) ⤏ ?x) at_top" by auto
  moreover have "∥F a∥ ≤ ?x + ?y U" when hU: "0 < U" "b < U" for U
    by (subst perron_aux_2' [OF hU Ha], standard)
  hence "∀⇩F U in at_top. ∥F a∥ ≤ ?x + ?y U"
    by (rule eventually_at_top_linorderI') (use Hb in auto)
  ultimately show ?thesis
    by (intro tendsto_lowerbound) auto
qed

lemma perron_aux_3:
  assumes Ha: "0 < a"
  shows "∥1 / (2 * pi * 𝗂) * contour_integral path (λs. a powr s / s)∥ ≤ a powr b * ln (1 + T / b)"
proof -
  have "∥1 / (2 * pi * 𝗂) * contour_integral (linepath (Complex b (-T)) (Complex b T)) (λs. 1 * a powr s / s)∥
       ≤ 1 * a powr b * ln (1 + T / b)"
    by (rule perron_aux_3') (auto intro: Ha cond perron_integrable)
  thus ?thesis unfolding path_def by auto
qed

lemma perron_aux':
  assumes Ha: "0 < a"
  shows "∥F a∥ ≤ a powr b * r a"
proof -
  note assms' = assms cond
  define P where "P ≡ 1 / (2 * pi * 𝗂) * contour_integral path (λs. a powr s / s)"
  have lm_1: "1 + ln (1 + T / b) ≤ 2 + ln (T / b)"
  proof -
    have "1 ≤ T / b" using hT Hb by auto
    hence "1 + T / b ≤ 2 * (T / b)" by auto
    hence "ln (1 + T / b) ≤ ln 2 + ln (T / b)"
      by (subst ln_mult_pos [symmetric]) auto
    thus ?thesis using ln_2_less_1 by auto
  qed
  have *: "∥F a∥ ≤ a powr b * (2 + ln (T / b))"
  proof (cases "1 ≤ a")
    assume Ha': "1 ≤ a"
    have "∥P - 1∥ ≤ ∥P∥ + 1" by (simp add: norm_triangle_le_diff)
    also have "… ≤ a powr b * ln (1 + T / b) + 1"
    proof -
      have "∥P∥ ≤ a powr b * ln (1 + T / b)"
        unfolding P_def by (intro perron_aux_3 assms')
      thus ?thesis by auto
    qed
    also have "… ≤ a powr b * (2 + ln (T / b))"
    proof -
      have "1 = a powr 0" using Ha' by auto
      also have "a powr 0 ≤ a powr b" using Ha' Hb by (intro powr_mono) auto
      finally have "a powr b * ln (1 + T / b) + 1 ≤ a powr b * (1 + ln (1 + T / b))"
        by (auto simp add: algebra_simps)
      also have "… ≤ a powr b * (2 + ln (T / b))" using Ha' lm_1 by auto
      finally show ?thesis .
    qed
    finally show ?thesis using Ha' unfolding F_def P_def by auto
  next
    assume Ha': "¬ 1 ≤ a"
    hence "∥P∥ ≤ a powr b * ln (1 + T / b)"
      unfolding P_def by (intro perron_aux_3 assms')
    also have "… ≤ a powr b * (2 + ln (T / b))"
      by (rule mult_left_mono) (use lm_1 in auto)
    finally show ?thesis using Ha' unfolding F_def P_def by auto
  qed
  consider "0 < a ∧ a ≠ 1" | "a = 1" using Ha by linarith
  thus ?thesis proof cases
    define c where "c = 1 / 2 * a powr b / (T * ¦ln a¦)"
    assume Ha': "0 < a ∧ a ≠ 1"
    hence "(0 < a ∧ a < 1) ∨ a > 1" by auto
    hence "∥F a∥ ≤ 1 / pi * a powr b / (T * ¦ln a¦)"
      using perron_aux_1 perron_aux_2 by auto
    also have "… ≤ c" unfolding c_def
      using Ha' hT' pi_gt3 by (auto simp add: field_simps)
    finally have "∥F a∥ ≤ c" .
    hence "∥F a∥ ≤ min c (a powr b * (2 + ln (T / b)))" using * by auto
    also have "… = a powr b * r a"
      unfolding r_def c_def using Ha' by auto (subst min_mult_distrib_left, auto)
    finally show ?thesis using Ha' unfolding P_def by auto
  next
    assume Ha': "a = 1"
    with * show ?thesis unfolding r_def by auto
  qed
qed

lemma r_bound:
  assumes Hn: "1 ≤ n"
  shows "r (x / n) ≤ H / T + (if n ∈ region then 2 + ln (T / b) else 0)"
proof (cases "n ∈ region")
  assume *: "n ∉ region"
  then consider "n < x - x / H" | "x + x / H < n" unfolding region_def by auto
  hence "1 / ¦ln (x / n)¦ ≤ 2 * H"
  proof cases
    have hH': "1 / (1 - 1 / H) > 1" using hH by auto
    case 1 hence "x / n > x / (x - x / H)"
      using Hx hH Hn by (intro divide_strict_left_mono) auto
    also have "x / (x - x / H) = 1 / (1 - 1 / H)"
      using Hx hH by (auto simp add: field_simps)
    finally have xn: "x / n > 1 / (1 - 1 / H)" .
    moreover have xn': "x / n > 1" using xn hH' by linarith
    ultimately have "¦ln (x / n)¦ > ln (1 / (1 - 1 / H))"
      using hH Hx Hn by auto
    hence "1 / ¦ln (x / n)¦ < 1 / ln (1 / (1 - 1 / H))"
      using xn' hH' by (intro divide_strict_left_mono mult_pos_pos ln_gt_zero) auto
    also have "… ≤ H" proof -
      have "ln (1 - 1 / H) ≤ - (1 / H)"
        using hH by (intro ln_one_minus_pos_upper_bound) auto
      hence "-1 / ln (1 - 1 / H) ≤ -1 / (- (1 / H))"
        using hH by (intro divide_left_mono_neg) (auto intro: divide_neg_pos)
      also have "... = H" by auto
      finally show ?thesis
        by (subst (2) inverse_eq_divide [symmetric])
           (subst ln_inverse, use hH in auto)
    qed
    finally show ?thesis using hH by auto
  next
    case 2 hence "x / n < x / (x + x / H)"
      using Hx hH Hn by (auto intro!: divide_strict_left_mono mult_pos_pos add_pos_pos)
    also have "… = 1 / (1 + 1 / H)"
    proof -
      have "0 < x + x * H" using Hx hH by (auto intro: add_pos_pos)
      thus ?thesis using Hx hH by (auto simp add: field_simps)
    qed
    finally have xn: "x / n < 1 / (1 + 1 / H)" .
    also have hH': "… < 1" using hH by (auto simp add: field_simps)
    finally have xn': "0 < x / n ∧ x / n < 1" using Hx Hn by auto
    have "1 / ¦ln (x / n)¦ = -1 / ln (x / n)"
      using xn' by (auto simp add: field_simps)
    also have "… ≤ 2 * H" proof -
      have "ln (x / n) < ln (1 / (1 + 1 / H))"
        using xn xn' by (subst ln_less_cancel_iff) (blast, linarith)
      also have "… = - ln (1 + 1 / H)"
        by (simp add: divide_inverse ln_inverse)
      also have "… ≤ - 1 / (2 * H)"
      proof -
        have "- ln (1 + 1 / H) = ln (inverse (1 + 1 / H))"
          by (simp add: ln_inverse)
        also have "… = ln (1 - 1 / (H + 1))"
          using hH by (auto simp: field_simps)
        also have "… ≤ - (1 / (H + 1))"
          using hH by (auto intro: ln_one_minus_pos_upper_bound)
        also have "… ≤ - 1 / (2 * H)"
          using hH by (auto simp: field_simps)
        finally show ?thesis .
      qed
      finally have "-1 / ln (x / n) ≤ -1 / (-1 / (2 * H))"
        by (intro divide_left_mono_neg) (insert xn' hH, auto simp add: field_simps)
      thus ?thesis by auto
    qed
    finally show ?thesis .
  qed
  hence "(1 / ¦ln (x / n)¦) / (2 * T) ≤ (2 * H) / (2 * T)"
    using hT' by (intro divide_right_mono) auto
  hence "1 / (2 * T * ¦ln (x / n)¦) ≤ H / T"
    by (simp add: field_simps)
  moreover have "x / n ≠ 1" using * hH unfolding region_def by auto
  ultimately show ?thesis unfolding r_def using * by auto
next
  assume *: "n ∈ region"
  moreover have "2 + ln (T / b) ≤ H / T + (2 + ln (T / b))"
    using hH hT' by auto
  ultimately show ?thesis unfolding r_def by auto
qed

lemma perron_aux:
  assumes Hn: "0 < n"
  shows "∥F' n∥ ≤ 1 / n nat_powr b * (x powr b * H / T)
    + (if n ∈ region then 3 * (2 + ln (T / b)) else 0)" (is "?P ≤ ?Q")
proof -
  have "∥F (x / n)∥ ≤ (x / n) powr b * r (x / n)"
    by (rule perron_aux') (use Hx Hn in auto)
  also have "… ≤ (x / n) powr b * (H / T + (if n ∈ region then 2 + ln (T / b) else 0))"
    by (intro mult_left_mono r_bound) (use Hn in auto)
  also have "… ≤ ?Q"
  proof -
    have *: "(x / n) powr b * (H / T) = 1 / n nat_powr b * (x powr b * H / T)"
      using Hx Hn by (subst powr_divide) (auto simp add: field_simps)
    moreover have "(x / n) powr b * (H / T + (2 + ln (T / b)))
      ≤ 1 / n nat_powr b * (x powr b * H / T) + 3 * (2 + ln (T / b))"
      when Hn': "n ∈ region"
    proof -
      have "(x / n) powr b ≤ 3"
      proof -
        have "x - x / H ≤ n" using Hn' unfolding region_def by auto
        moreover have "x / H < x / 1" using hH Hx by (intro divide_strict_left_mono) auto
        ultimately have "x / n ≤ x / (x - x / H)"
          using Hx hH Hn by (intro divide_left_mono mult_pos_pos) auto
        also have "… = 1 + 1 / (H - 1)"
          using Hx hH by (auto simp add: field_simps)
        finally have "(x / n) powr b ≤ (1 + 1 / (H - 1)) powr b"
          using Hx Hn Hb by (intro powr_mono2) auto
        also have "… ≤ exp (b / (H - 1))"
        proof -
          have "ln (1 + 1 / (H - 1)) ≤ 1 / (H - 1)"
            using hH by (intro ln_add_one_self_le_self) auto
          hence "b * ln (1 + 1 / (H - 1)) ≤ b * (1 / (H - 1))"
            using Hb by (intro mult_left_mono) auto
          thus ?thesis unfolding powr_def by auto
        qed
        also have "… ≤ exp 1" using Hb hH' by auto
        also have "… ≤ 3" by (rule exp_le)
        finally show ?thesis .
      qed
      moreover have "0 ≤ ln (T / b)" using hT Hb by (auto intro!: ln_ge_zero)
      ultimately show ?thesis using hT
        by (subst ring_distribs, subst *, subst add_le_cancel_left)
           (intro mult_right_mono, auto intro!: add_nonneg_nonneg)
    qed
    ultimately show ?thesis by auto
  qed
  finally show ?thesis unfolding F'_def .
qed

definition a where "a n ≡ fds_nth f n"

lemma finite_region: "finite region"
  unfolding region_def by (subst nat_le_real_iff) auto

lemma zero_notin_region: "0 ∉ region"
  unfolding region_def using hH Hx by (auto simp add: field_simps)

lemma path_image_conv:
  assumes "s ∈ img_path"
  shows "conv_abscissa f < s ∙ 1"
proof -
  from assms have "Re s = b"
    unfolding img_path_def path_def
    by (auto simp add: closed_segment_def legacy_Complex_simps field_simps)
  thus ?thesis using Hb' conv_le_abs_conv_abscissa [of f] by auto
qed

lemma converge_on_path:
  assumes "s ∈ img_path"
  shows "fds_converges f s"
  by (intro fds_converges path_image_conv assms)

lemma summable_on_path:
  assumes "s ∈ img_path"
  shows "(λn. a n / n nat_powr s) subsummable {1..}"
  unfolding a_def by (intro eval_fds_complex_subsum(2) converge_on_path assms)

lemma zero_notin_path:
  shows "0 ∉ closed_segment (Complex b (- T)) (Complex b T)"
  using Hb unfolding img_path_def path_def
  by (auto simp add: closed_segment_def legacy_Complex_simps field_simps)

lemma perron_bound:
  "∥∑`n ≥ 1. a n * F' n∥ ≤ x powr b * H * B / T
    + 3 * (2 + ln (T / b)) * (∑n∈region. ∥a n∥)"
proof -
  define M where "M ≡ 3 * (2 + ln (T / b))"
  have sum_1: "(λn. ∥a n / n nat_powr (b :: complex)∥) subsummable {1..}"
    unfolding a_def
    by (fold nat_power_complex_def)
       (fastforce intro: Hb' fds_abs_subsummable fds_abs_converges)
  hence sum_2: "(λn. ∥a n∥ * 1 / n nat_powr b) subsummable {1..}"
  proof -
    have "∥a n / n nat_powr (b :: complex)∥ = ∥a n∥ * 1 / n nat_powr b" for n
      by (auto simp add: norm_divide field_simps norm_powr_real_powr')
    thus ?thesis using sum_1 by auto
  qed
  hence sum_3: "(λn. ∥a n∥ * 1 / n nat_powr b * (x powr b * H / T)) subsummable {1..}"
    by (rule subsummable_mult2)
  moreover have sum_4: "(λn. if n ∈ region then M * ∥a n∥ else 0) subsummable {1..}"
    by (intro has_subsum_summable, rule has_subsum_If_finite)
       (insert finite_region, auto)
  moreover have "∥a n * F' n∥
    ≤ ∥a n∥ * 1 / n nat_powr b * (x powr b * H / T)
    + (if n ∈ region then M * ∥a n∥ else 0)" (is "?x' ≤ ?x")
    when "n ∈ {1..}" for n
  proof -
    have "∥a n * F' n∥ ≤ ∥a n∥ *
      (1 / n nat_powr b * (x powr b * H / T) + (if n ∈ region then M else 0))"
      unfolding M_def
      by (subst norm_mult)
         (intro mult_left_mono perron_aux, use that in auto)
    also have "… = ?x" by (simp add: field_simps)
    finally show ?thesis .
  qed
  ultimately have "∥∑`n ≥ 1. a n * F' n∥
    ≤ (∑`n ≥ 1. ∥a n∥ * 1 / n nat_powr b * (x powr b * H / T)
    + (if n ∈ region then M * ∥a n∥ else 0))"
    by (intro subsum_norm_bound subsummable_add)
  also have "… ≤ x powr b * H * B / T + M * (∑n∈region. ∥a n∥)"
  proof -
    have "(∑`n ≥ 1. (if n ∈ region then M * ∥a n∥ else 0))
        = (∑n ∈ region ∩ {1..}. M * ∥a n∥)"
      by (intro subsumI [symmetric] has_subsum_If_finite_set finite_region)
    also have "… = M * (∑n∈region. ∥a n∥)"
    proof -
      have "region ∩ {1..} = region"
        using zero_notin_region zero_less_iff_neq_zero by (auto intro: Suc_leI)
      thus ?thesis by (subst sum_distrib_left) (use zero_notin_region in auto)
    qed
    also have
      "(∑`n ≥ 1. ∥a n∥ * 1 / n nat_powr b * (x powr b * H / T))
      ≤ x powr b * H * B / T"
      by (subst subsum_mult2, rule sum_2, insert hB hH hT', fold a_def)
         (auto simp add: field_simps, subst (1) mult.commute, auto intro: mult_right_mono)
    ultimately show ?thesis
      by (subst subsum_add [symmetric]) ((rule sum_3 sum_4)+, auto)
  qed
  finally show ?thesis unfolding M_def .
qed

lemma perron:
  "(λs. eval_fds f s * x powr s / s) contour_integrable_on path"
  "∥sum_upto a x - 1 / (2 * pi * 𝗂) * contour_integral path (λs. eval_fds f s * x powr s / s)∥
    ≤ x powr b * H * B / T + 3 * (2 + ln (T / b)) * (∑n∈region. ∥a n∥)"
proof (goal_cases)
  define g where "g s ≡ eval_fds f s * x powr s / s" for s :: complex
  define h where "h s n ≡ a n / n nat_powr s * (x powr s / s)" for s :: complex and n :: nat
  define G where "G n ≡ contour_integral path (λs. (x / n) powr s / s)" for n :: nat
  define H where "H n ≡ 1 / (2 * pi * 𝗂) * G n" for n :: nat
  have h_integrable: "(λs. h s n) contour_integrable_on path" when "0 < n" for n
    using Hb Hx unfolding path_def h_def
    by (intro contour_integrable_continuous_linepath continuous_intros)
       (use that zero_notin_path in auto)
  have "contour_integral path g = contour_integral path (λs. ∑`n ≥ 1. h s n)"
  proof (rule contour_integral_eq, fold img_path_def)
    fix s assume *: "s ∈ img_path"
    hence "g s = (∑`n ≥ 1. a n / n nat_powr s) * (x powr s / s)"
      unfolding g_def a_def
      by (subst eval_fds_complex_subsum) (auto intro!: converge_on_path)
    also have "… = (∑`n ≥ 1. a n / n nat_powr s * (x powr s / s))"
      by (intro subsum_mult2 [symmetric] summable) (intro summable_on_path *)
    finally show "g s = (∑`n ≥ 1. h s n)" unfolding h_def .
  qed
  also have
    sum_1: "(λn. contour_integral path (λs. h s n)) subsummable {1..}"
    and "… = (∑`n ≥ 1. contour_integral path (λs. h s n))"
  proof (goal_cases)
    have "((λN. contour_integral path (λs. sum (h s) {1..N}))
      ⤏ contour_integral path (λs. subsum (h s) {1..})) at_top"
    proof (rule contour_integral_uniform_limit)
      show "valid_path path" unfolding path_def by auto
      show "sequentially ≠ bot" by auto
    next
      fix t :: real
      show "∥vector_derivative path (at t)∥ ≤ sqrt (4 * T⇧2)"
        unfolding path_def by (auto simp add: legacy_Complex_simps)
    next
      from path_image_conv
      have *: "uniformly_convergent_on img_path (λN s. ∑n≤N. fds_nth f n / nat_power n s)"
        by (intro uniformly_convergent_eval_fds) (unfold path_def img_path_def, auto)
      have *: "uniformly_convergent_on img_path (λN s. ∑n = 1..N. a n / n nat_powr s)"
      proof -
        have "(∑n≤N. fds_nth f n / nat_power n s) = (∑n = 1..N. a n / n nat_powr s)" for N s
        proof -
          have "(∑n≤N. fds_nth f n / nat_power n s) = (∑n≤N. a n / n nat_powr s)"
            unfolding a_def nat_power_complex_def by auto
          also have "… = (∑n∈{..N} - {0}. a n / n nat_powr s)"
            by (subst sum_diff1) auto
          also have "… = (∑n = 1..N. a n / n nat_powr s)"
          proof -
            have "{..N} - {0} = {1..N}" by auto
            thus ?thesis by auto
          qed
          finally show ?thesis by auto
        qed
        thus ?thesis using * by auto
      qed
      hence "uniform_limit img_path
        (λN s. ∑n = 1..N. a n / n nat_powr s)
        (λs. ∑`n ≥ 1. a n / n nat_powr s) at_top"
      proof -
        have "uniform_limit img_path
          (λN s. ∑n = 1..N. a n / n nat_powr s)
          (λs. lim (λN. ∑n = 1..N. a n / n nat_powr s)) at_top"
          using * by (subst (asm) uniformly_convergent_uniform_limit_iff)
        moreover have "lim (λN. ∑n = 1..N. a n / n nat_powr s) = (∑`n ≥ 1. a n / n nat_powr s)" for s
          by (rule subsum_ge_limit)
        ultimately show ?thesis by auto
      qed
      moreover have "bounded ((λs. subsum (λn. a n / n nat_powr s) {1..}) ` img_path)" (is "bounded ?A")
      proof -
        have "bounded (eval_fds f ` img_path)"
          by (intro compact_imp_bounded compact_continuous_image continuous_on_eval_fds)
             (use path_image_conv img_path_def path_def in auto)
        moreover have "… = ?A"
          unfolding a_def by (intro image_cong refl eval_fds_complex_subsum(1) converge_on_path)
        ultimately show ?thesis by auto
      qed
      moreover have "0 ∉ closed_segment (Complex b (- T)) (Complex b T)"
        using Hb by (auto simp: closed_segment_def legacy_Complex_simps algebra_simps)
      hence "bounded ((λs. x powr s / s) ` img_path)"
        unfolding img_path_def path_def using Hx Hb
        by (intro compact_imp_bounded compact_continuous_image continuous_intros) auto
      ultimately have "uniform_limit img_path
        (λN s. (∑n = 1..N. a n / n nat_powr s) * (x powr s / s))
        (λs. (∑`n ≥ 1. a n / n nat_powr s) * (x powr s / s)) at_top" (is ?P)
        by (intro uniform_lim_mult uniform_limit_const)
      moreover have "?P = uniform_limit (path_image path)
        (λN s. sum (h s) {1..N}) (λs. subsum (h s) {1..}) at_top" (is "?P = ?Q")
        unfolding h_def
        by (fold img_path_def, rule uniform_limit_cong', subst sum_distrib_right [symmetric], rule refl)
           (subst subsum_mult2, intro summable_on_path, auto)
      ultimately show ?Q by blast
    next
      from h_integrable
      show "∀⇩F N in at_top. (λs. sum (h s) {1..N}) contour_integrable_on path"
        unfolding h_def by (intro eventuallyI contour_integrable_sum) auto
    qed
    hence *: "has_subsum (λn. contour_integral path (λs. h s n)) {1..} (contour_integral path (λs. subsum (h s) {1..}))"
      using h_integrable by (subst (asm) contour_integral_sum) (auto intro: has_subsum_ge_limit)
    case 1 from * show ?case unfolding h_def by (intro has_subsum_summable)
    case 2 from * show ?case unfolding h_def by (rule subsumI)
  qed
  note this(2) also have
    sum_2: "(λn. a n * G n) subsummable {1..}"
    and "… = (∑`n ≥ 1. a n * G n)"
  proof (goal_cases)
    have *: "a n * G n = contour_integral path (λs. h s n)" when Hn: "n ∈ {1..}" for n :: nat
    proof -
      have "(λs. (x / n) powr s / s) contour_integrable_on path"
        unfolding path_def by (rule perron_integrable) (use Hn Hx hT in auto)
      moreover have "contour_integral path (λs. h s n) = contour_integral path (λs. a n * ((x / n) powr s / s))"
      proof (intro contour_integral_cong refl)
        fix s :: complex
        have "(x / n) powr s * n powr s = ((x / n :: complex) * n) powr s"
          by (rule powr_times_real [symmetric]) (use Hn Hx in auto)
        also have "… = x powr s" using Hn by auto
        finally have "(x / n) powr s = x powr s / n powr s" using Hn by (intro eq_divide_imp) auto
        thus "h s n = a n * ((x / n) powr s / s)" unfolding h_def by (auto simp add: field_simps)
      qed
      ultimately show ?thesis unfolding G_def by (subst (asm) contour_integral_lmul) auto
    qed
    case 1 show ?case by (subst subsummable_cong) (use * sum_1 in auto)
    case 2 show ?case by (intro subsum_cong * [symmetric])
  qed
  note this(2) finally have
    "1 / (2 * pi * 𝗂) * contour_integral path g = (∑`n ≥ 1. a n * G n) * (1 / (2 * pi * 𝗂))" by auto
  also have
    sum_3: "(λn. a n * G n * (1 / (2 * pi * 𝗂))) subsummable {1..}"
    and "… = (∑`n ≥ 1. a n * G n * (1 / (2 * pi * 𝗂)))"
    by (intro subsummable_mult2 subsum_mult2 [symmetric] sum_2)+
  note this(2) also have
    sum_4: "(λn. a n * H n) subsummable {1..}"
    and "… = (∑`n ≥ 1. a n * H n)"
    unfolding H_def using sum_3 by auto
  note this(2) also have
    "… - (∑`n ≥ 1. if n ≤ x then a n else 0)
      = (∑`n ≥ 1. a n * H n - (if n ≤ x then a n else 0))"
    using sum_4
    by (rule subsum_minus(1), unfold subsummable_def)
       (auto simp add: if_if_eq_conj nat_le_real_iff)
  moreover have "(∑`n ≥ 1. if n ≤ x then a n else 0) = sum_upto a x"
  proof -
    have "(∑`n ≥ 1. if n ≤ x then a n else 0) = (∑n :: nat|n ∈ {1..} ∧ n ≤ x. a n)"
      by (intro subsumI [symmetric] has_subsum_If_finite) (auto simp add: nat_le_real_iff)
    also have "… = sum_upto a x"
    proof -
      have "{n :: nat. n ∈ {1..} ∧ n ≤ x} = {n. 0 < n ∧ n ≤ x}" by auto
      thus ?thesis unfolding sum_upto_def by auto
    qed
    finally show ?thesis .
  qed
  moreover have "(∑`n ≥ 1. a n * H n - (if n ≤ x then a n else 0)) = (∑`n ≥ 1. a n * F' n)"
    unfolding F_def F'_def G_def H_def by (rule subsum_cong) (auto simp add: algebra_simps)
  ultimately have result: "∥sum_upto a x - 1 / (2 * pi * 𝗂) * contour_integral path g∥ = ∥∑`n ≥ 1. a n * F' n∥"
    by (subst norm_minus_commute) auto
  case 1 show ?case
  proof -
    have "closed_segment (Complex b (- T)) (Complex b T) ⊆ {s. conv_abscissa f < ereal (s ∙ 1)}"
      using path_image_conv unfolding img_path_def path_def by auto
    thus ?thesis unfolding path_def
      by (intro contour_integrable_continuous_linepath continuous_intros)
         (use Hx zero_notin_path in auto)
  qed
  case 2 show ?case using perron_bound result unfolding g_def by linarith
qed
end

theorem perron_formula:
  fixes b B H T x :: real and f :: "complex fds"
  assumes Hb: "0 < b" and hT: "b ≤ T"
    and Hb': "abs_conv_abscissa f < b"
    and hH: "1 < H" and hH': "b + 1 ≤ H" and Hx: "0 < x"
    and hB: "(∑`n ≥ 1. ∥fds_nth f n∥ / n nat_powr b) ≤ B"
  shows "(λs. eval_fds f s * x powr s / s) contour_integrable_on (linepath (Complex b (-T)) (Complex b T))"
        "∥sum_upto (fds_nth f) x - 1 / (2 * pi * 𝗂) *
          contour_integral (linepath (Complex b (-T)) (Complex b T)) (λs. eval_fds f s * x powr s / s)∥
         ≤ x powr b * H * B / T + 3 * (2 + ln (T / b)) * (∑n | x - x / H ≤ n ∧ n ≤ x + x / H. ∥fds_nth f n∥)"
proof (goal_cases)
  interpret z: perron_locale using assms unfolding perron_locale_def by auto
  case 1 show ?case using z.perron(1) unfolding z.path_def .
  case 2 show ?case using z.perron(2) unfolding z.path_def z.region_def z.a_def .
qed

theorem perron_asymp:
  fixes b x :: real
  assumes b: "b > 0" "ereal b > abs_conv_abscissa f"
  assumes x: "0 < x" "x ∉ ℕ"
  defines "L ≡ (λT. linepath (Complex b (-T)) (Complex b T))"
  shows   "((λT. contour_integral (L T) (λs. eval_fds f s * of_real x powr s / s))
               ⤏ 2 * pi * 𝗂 * sum_upto (λn. fds_nth f n) x) at_top"
proof -
  define R where "R = (λH. {n. x - x / H ≤ real n ∧ real n ≤ x + x / H})"
  have R_altdef: "R H = {n. dist (of_nat n) x ≤ x / H}" for H
    unfolding R_def by (intro Collect_cong) (auto simp: dist_norm)
  obtain H where H: "H > 1" "H ≥ b + 1" "R H = (if x ∈ ℕ then {nat ⌊x⌋} else {})"
  proof (cases "x ∈ ℕ")
    case True thus ?thesis using x by auto
  next
    case False
    define d where "d = setdist {x} ℕ"
    have "0 ∈ (ℕ :: real set)" by auto
    hence "(ℕ :: real set) ≠ {}" by blast
    hence "d > 0"
      unfolding d_def using False by (subst setdist_gt_0_compact_closed) auto
    define H where "H = Max {2, b + 1, 2 * x / d}"
    have H: "H ≥ 2" "H ≥ b + 1" "H ≥ 2 * x / d"
      unfolding H_def by (rule Max.coboundedI; simp)+
    
    show ?thesis
    proof (rule that[of H])
      have "n ∉ R H" for n :: nat
      proof -
        have "x / H ≤ x / (2 * x / d)"
          using H x ‹d > 0› 
          by (intro divide_left_mono) (auto intro!: mult_pos_pos)
        also have "… < d"
          using x ‹d > 0› by simp
        also have "d ≤ dist (of_nat n) x"
          unfolding d_def by (subst dist_commute, rule setdist_le_dist) auto
        finally show "n ∉ R H"
          by (auto simp: R_altdef)
      qed
      thus "R H = (if x ∈ ℕ then {nat ⌊x⌋} else {})"
        using False by auto
    qed (use H in auto)
  qed

  define g where "g = (λs. eval_fds f s * of_real x powr s / s)"
  define I where "I = (λT. contour_integral (L T) g)"
  define c where "c = 2 * pi * 𝗂"
  define A where "A = sum_upto (fds_nth f)"
  define B where "B = subsum (λn. norm (fds_nth f n) / n nat_powr b) {0⇩+..}"
  define X where "X = (if x ∈ ℤ then {nat ⌊x⌋} else {})"
  
  have norm_le: "norm (A x - I T / c) ≤ x powr b * H * B / T" if T: "T ≥ b" for T
  proof -
    interpret perron_locale b B H T x f
      by standard (use b T x H(1,2) in ‹auto simp: B_def›)
    from perron
    have "norm (A x - I T / c) ≤ x powr b * H * B / T
        + 3 * (∑n∈R H. norm (fds_nth f n)) * (2 + ln (T / b))"
      by (simp add: I_def A_def g_def a_def local.path_def L_def c_def R_def 
                    region_def algebra_simps)
    also have "(∑n∈R H. norm (fds_nth f n)) = 0"
      using x H by auto
    finally show "norm (A x - I T / c) ≤ x powr b * H * B / T"
      by simp
  qed
  have "eventually (λT. norm (A x - I T / c) ≤ x powr b * H * B / T) at_top"
    using eventually_ge_at_top[of b] by eventually_elim (use norm_le in auto)
  moreover have "((λT. x powr b * H * B / T) ⤏ 0) at_top"
    by real_asymp
  ultimately have lim: "((λT. A x - I T / c) ⤏ 0) at_top"
    using Lim_null_comparison by fast
  have "((λT. -c * (A x - I T / c) + c * A x) ⤏ -c * 0 + c * A x) at_top"
    by (rule tendsto_intros lim)+
  also have "(λT. -c * (A x - I T / c) + c * A x) = I"
    by (simp add: algebra_simps c_def)
  finally show ?thesis
    by (simp add: c_def A_def I_def g_def)
qed

unbundle no pnt_syntax

end