Theory PNT_with_Remainder

theory PNT_with_Remainder
imports
  "Relation_of_PNTs"
  "Zeta_Zerofree"
  "Perron_Formula"
begin
unbundle pnt_notation

section ‹Estimation of the order of $\frac{\zeta'(s)}{\zeta(s)}$›

notation primes_psi ("ψ")

lemma zeta_div_bound':
  assumes "1 + exp (- 4 * ln (14 + 4 * t)) ≤ σ"
    and "13 / 22 ≤ t"
    and "z ∈ cball (Complex σ t) (1 / 2)"
  shows "∥zeta z / zeta (Complex σ t)∥ ≤ exp (12 * ln (14 + 4 * t))"
proof -
  interpret z: zeta_bound_param_2
    "λt. 1 / 2" "λt. 4 * ln (12 + 2 * max 0 t)" t σ t
    unfolding zeta_bound_param_1_def zeta_bound_param_2_def
              zeta_bound_param_1_axioms_def zeta_bound_param_2_axioms_def
    using assms by (auto intro: classical_zeta_bound.zeta_bound_param_axioms)
  show ?thesis using z.zeta_div_bound assms(2) assms(3)
    unfolding z.s_def z.r_def by auto
qed

lemma zeta_div_bound:
  assumes "1 + exp (- 4 * ln (14 + 4 * ¦t¦)) ≤ σ"
    and "13 / 22 ≤ ¦t¦"
    and "z ∈ cball (Complex σ t) (1 / 2)"
  shows "∥zeta z / zeta (Complex σ t)∥ ≤ exp (12 * ln (14 + 4 * ¦t¦))"
proof (cases "0 ≤ t")
  case True with assms(2) have "13 / 22 ≤ t" by auto
  thus ?thesis using assms by (auto intro: zeta_div_bound')
next
  case False with assms(2) have Ht: "t ≤ - 13 / 22" by auto
  moreover have 1: "Complex σ (- t) = cnj (Complex σ t)" by (auto simp add: legacy_Complex_simps)
  ultimately have "∥zeta (cnj z) / zeta (Complex σ (- t))∥ ≤ exp (12 * ln (14 + 4 * (- t)))"
    using assms(1) assms(3)
    by (intro zeta_div_bound', auto simp add: dist_complex_def)
       (subst complex_cnj_diff [symmetric], subst complex_mod_cnj)
  thus ?thesis using Ht by (subst (asm) 1) (simp add: norm_divide)
qed

definition C⇩2 where "C⇩2 ≡ 319979520 :: real"

lemma C⇩2_gt_zero: "0 < C⇩2" unfolding C⇩2_def by auto

lemma logderiv_zeta_order_estimate':
"∀⇩F t in (abs going_to at_top).
  ∀σ. 1 - 1 / 7 * C⇩1 / ln (¦t¦ + 3) ≤ σ
  ⟶ ∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2"
proof -
  define F where "F :: real filter ≡ abs going_to at_top"
  define r where "r t ≡ C⇩1 / ln (¦t¦ + 3)" for t :: real
  define s where "s σ t ≡ Complex (σ + 2 / 7 * r t) t" for σ t
  have r_nonneg: "0 ≤ r t" for t unfolding PNT_const_C⇩1_def r_def by auto
  have "∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2"
    when h: "1 - 1 / 7 * r t ≤ σ"
            "exp (- 4 * ln (14 + 4 * ¦t¦)) ≤ 1 / 7 * r t"
            "8 / 7 * r t ≤ ¦t¦"
            "8 / 7 * r t ≤ 1 / 2"
            "13 / 22 ≤ ¦t¦" for σ t
  proof -
    have "∥logderiv zeta (Complex σ t)∥ ≤ 8 * (12 * ln (14 + 4 * ¦t¦)) / (8 / 7 * r t)"
    proof (rule lemma_3_9_beta1' [where ?s = "s σ t"], goal_cases)
      case 1 show ?case unfolding PNT_const_C⇩1_def r_def by auto
      case 2 show ?case by auto
      have notin_ball: "1 ∉ ball (s σ t) (8 / 7 * r t)"
      proof -
        note h(3)
        also have "¦t¦ = ¦Im (Complex (σ + 2 / 7 * r t) t - 1)¦" by auto
        also have "… ≤ ∥Complex (σ + 2 / 7 * r t) t - 1∥" by (rule abs_Im_le_cmod)
        finally show ?thesis
          unfolding s_def by (auto simp add: dist_complex_def)
      qed
      case 3 show ?case by (intro holomorphic_zeta notin_ball)
      case 6 show ?case
        using r_nonneg unfolding s_def
        by (auto simp add: dist_complex_def legacy_Complex_simps)
      fix z assume Hz: "z ∈ ball (s σ t) (8 / 7 * r t)"
      show "zeta z ≠ 0"
      proof (rule ccontr)
        assume "¬ zeta z ≠ 0"
        hence zero: "zeta (Complex (Re z) (Im z)) = 0" by auto
        have "r t ≤ C⇩1 / ln (¦Im z¦ + 2)"
        proof -
          have "∥s σ t - z∥ < 1"
            using Hz h(4) by (auto simp add: dist_complex_def)
          hence "¦t - Im z¦ < 1"
            using abs_Im_le_cmod [of "s σ t - z"]
            unfolding s_def by (auto simp add: legacy_Complex_simps)
          hence "¦Im z¦ < ¦t¦ + 1" by auto
          thus ?thesis unfolding r_def
            by (intro divide_left_mono mult_pos_pos)
               (subst ln_le_cancel_iff, use C⇩1_gt_zero in auto)
        qed
        also have "… ≤ 1 - Re z"
          using notin_ball Hz by (intro zeta_nonzero_region zero) auto
        also have "… < 1 - Re (s σ t) + 8 / 7 * r t"
        proof -
          have "Re (s σ t - z) ≤ ¦Re (s σ t - z)¦" by auto
          also have "… < 8 / 7 * r t"
            using Hz abs_Re_le_cmod [of "s σ t - z"]
            by (auto simp add: dist_complex_def)
          ultimately show ?thesis by auto
        qed
        also have "… = 1 - σ + 6 / 7 * r t" unfolding s_def by auto
        also have "… ≤ r t" using h(1) by auto
        finally show False by auto
      qed
      from Hz have "z ∈ cball (s σ t) (1 / 2)"
        using h(4) by auto
      thus "∥zeta z / zeta (s σ t)∥ ≤ exp (12 * ln (14 + 4 * ¦t¦))"
        using h(1) h(2) unfolding s_def
        by (intro zeta_div_bound h(5)) auto
    qed
    also have "… = 84 / r t * ln (14 + 4 * ¦t¦)"
      by (auto simp add: field_simps)
    also have "… ≤ 336 / C⇩1 * ln (¦t¦ + 2) * ln (¦t¦ + 3)"
    proof - 
      have "84 / r t * ln (14 + 4 * ¦t¦) ≤ 84 / r t * (4 * ln (¦t¦ + 2))"
        using r_nonneg by (intro mult_left_mono mult_right_mono ln_bound_1) auto
      thus ?thesis unfolding r_def by (simp add: mult_ac)
    qed
    also have "… ≤ 336 / C⇩1 * (ln (¦t¦ + 3))⇧2"
      unfolding power2_eq_square
      by (simp add: mult_ac, intro divide_right_mono mult_right_mono)
         (subst ln_le_cancel_iff, use C⇩1_gt_zero in auto)
    also have "… = C⇩2 * (ln (¦t¦ + 3))⇧2"
      unfolding PNT_const_C⇩1_def C⇩2_def by auto
    finally show ?thesis .
  qed
  hence
    "∀⇩F t in F.
        exp (- 4 * ln (14 + 4 * ¦t¦)) ≤ 1 / 7 * r t
    ⟶ 8 / 7 * r t ≤ ¦t¦
    ⟶ 8 / 7 * r t ≤ 1 / 2
    ⟶ 13 / 22 ≤ ¦t¦
    ⟶ (∀σ. 1 - 1 / 7 * r t ≤ σ
      ⟶ ∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2)"
    by (blast intro: eventuallyI)
  moreover have "∀⇩F t in F. exp (- 4 * ln (14 + 4 * ¦t¦)) ≤ 1 / 7 * r t"
    unfolding F_def r_def PNT_const_C⇩1_def
    by (rule eventually_going_toI) real_asymp
  moreover have "∀⇩F t in F. 8 / 7 * r t ≤ ¦t¦"
    unfolding F_def r_def PNT_const_C⇩1_def
    by (rule eventually_going_toI) real_asymp
  moreover have "∀⇩F t in F. 8 / 7 * r t ≤ 1 / 2"
    unfolding F_def r_def PNT_const_C⇩1_def
    by (rule eventually_going_toI) real_asymp
  moreover have "∀⇩F t in F. 13 / 22 ≤ ¦t¦"
    unfolding F_def by (rule eventually_going_toI) real_asymp
  ultimately have
    "∀⇩F t in F. (∀σ. 1 - 1 / 7 * r t ≤ σ
      ⟶ ∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2)"
    by eventually_elim blast
  thus ?thesis unfolding F_def r_def by auto
qed

definition C⇩3 where
"C⇩3 ≡ SOME T. 0 < T ∧
  (∀t. T ≤ ¦t¦ ⟶
    (∀σ. 1 - 1 / 7 * C⇩1 / ln (¦t¦ + 3) ≤ σ
     ⟶ ∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2))"

lemma C⇩3_prop:
  "0 < C⇩3 ∧
  (∀t. C⇩3 ≤ ¦t¦ ⟶
    (∀σ. 1 - 1 / 7 * C⇩1 / ln (¦t¦ + 3) ≤ σ
    ⟶ ∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2))"
proof -
  obtain T' where hT:
  "⋀t. T' ≤ ¦t¦ ⟹
    (∀σ. 1 - 1 / 7 * C⇩1 / ln (¦t¦ + 3) ≤ σ
     ⟶ ∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2)"
    using logderiv_zeta_order_estimate'
      [unfolded going_to_def, THEN rev_iffD1,
      OF eventually_filtercomap_at_top_linorder] by blast
  define T where "T ≡ max 1 T'"
  show ?thesis unfolding C⇩3_def
    by (rule someI [of _ T]) (unfold T_def, use hT in auto)
qed

lemma C⇩3_gt_zero: "0 < C⇩3" using C⇩3_prop by blast

lemma logderiv_zeta_order_estimate:
  assumes "1 - 1 / 7 * C⇩1 / ln (¦t¦ + 3) ≤ σ" "C⇩3 ≤ ¦t¦"
  shows "∥logderiv zeta (Complex σ t)∥ ≤ C⇩2 * (ln (¦t¦ + 3))⇧2"
  using assms C⇩3_prop by blast

definition zeta_zerofree_region
  where "zeta_zerofree_region ≡ {s. s ≠ 1 ∧ 1 - C⇩1 / ln (¦Im s¦ + 2) < Re s}"
definition logderiv_zeta_region
  where "logderiv_zeta_region ≡ {s. C⇩3 ≤ ¦Im s¦ ∧ 1 - 1 / 7 * C⇩1 / ln (¦Im s¦ + 3) ≤ Re s}"
definition zeta_strip_region
  where "zeta_strip_region σ T ≡ {s. s ≠ 1 ∧ σ ≤ Re s ∧ ¦Im s¦ ≤ T}"
definition zeta_strip_region'
  where "zeta_strip_region' σ T ≡ {s. s ≠ 1 ∧ σ ≤ Re s ∧ C⇩3 ≤ ¦Im s¦ ∧ ¦Im s¦ ≤ T}"

lemma strip_in_zerofree_region:
  assumes "1 - C⇩1 / ln (T + 2) < σ"
  shows "zeta_strip_region σ T ⊆ zeta_zerofree_region"
proof
  fix s assume Hs: "s ∈ zeta_strip_region σ T"
  hence Hs': "s ≠ 1" "σ ≤ Re s" "¦Im s¦ ≤ T" unfolding zeta_strip_region_def by auto
  from this(3) have "C⇩1 / ln (T + 2) ≤ C⇩1 / ln (¦Im s¦ + 2)"
    using C⇩1_gt_zero by (intro divide_left_mono mult_pos_pos) auto
  thus "s ∈ zeta_zerofree_region" using Hs' assms unfolding zeta_zerofree_region_def by auto
qed

lemma strip_in_logderiv_zeta_region:
  assumes "1 - 1 / 7 * C⇩1 / ln (T + 3) ≤ σ"
  shows "zeta_strip_region' σ T ⊆ logderiv_zeta_region"
proof
  fix s assume Hs: "s ∈ zeta_strip_region' σ T"
  hence Hs': "s ≠ 1" "σ ≤ Re s" "C⇩3 ≤ ¦Im s¦" "¦Im s¦ ≤ T" unfolding zeta_strip_region'_def by auto
  from this(4) have "C⇩1 / (7 * ln (T + 3)) ≤ C⇩1 / (7 * ln (¦Im s¦ + 3))"
    using C⇩1_gt_zero by (intro divide_left_mono mult_pos_pos) auto
  thus "s ∈ logderiv_zeta_region" using Hs' assms unfolding logderiv_zeta_region_def by auto
qed

lemma strip_condition_imp:
  assumes "0 ≤ T" "1 - 1 / 7 * C⇩1 / ln (T + 3) ≤ σ"
  shows "1 - C⇩1 / ln (T + 2) < σ"
proof -
  have "ln (T + 2) ≤ 7 * ln (T + 2)" using assms(1) by auto
  also have "… < 7 * ln (T + 3)" using assms(1) by auto
  finally have "C⇩1 / (7 * ln (T + 3)) < C⇩1 / ln (T + 2)"
    using C⇩1_gt_zero assms(1) by (intro divide_strict_left_mono mult_pos_pos) auto
  thus ?thesis using assms(2) by auto
qed

lemma zeta_zerofree_region:
  assumes "s ∈ zeta_zerofree_region"
  shows "zeta s ≠ 0"
  using zeta_nonzero_region [of "Re s" "Im s"] assms
  unfolding zeta_zerofree_region_def by auto

lemma logderiv_zeta_region_estimate:
  assumes "s ∈ logderiv_zeta_region"
  shows "∥logderiv zeta s∥ ≤ C⇩2 * (ln (¦Im s¦ + 3))⇧2"
  using logderiv_zeta_order_estimate [of "Im s" "Re s"] assms
  unfolding logderiv_zeta_region_def by auto

definition C⇩4 :: real where "C⇩4 ≡ 1 / 6666241"

lemma C⇩4_prop:
  "∀⇩F x in at_top. C⇩4 / ln x ≤ C⇩1 / (7 * ln (x + 3))"
  unfolding PNT_const_C⇩1_def C⇩4_def by real_asymp

lemma C⇩4_gt_zero: "0 < C⇩4" unfolding C⇩4_def by auto

definition C⇩5_prop where
"C⇩5_prop C⇩5 ≡
  0 < C⇩5 ∧ (∀⇩F x in at_top. (∀t. ¦t¦ ≤ x
    ⟶ ∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩5 * (ln x)⇧2))"

lemma logderiv_zeta_bound_vertical':
  "∃C⇩5. C⇩5_prop C⇩5"
proof -
  define K where "K ≡ cbox (Complex 0 (-C⇩3)) (Complex 2 C⇩3)"
  define Γ where "Γ ≡ {s ∈ K. zeta' s = 0}"
  have "zeta' not_zero_on K"
    unfolding not_zero_on_def K_def using C⇩3_gt_zero
    by (intro bexI [where x = 2])
       (auto simp add: zeta_eq_zero_iff_zeta' zeta_2 in_cbox_complex_iff)
  hence fin: "finite Γ"
    unfolding Γ_def K_def
    by (auto intro!: convex_connected analytic_compact_finite_zeros zeta'_analytic)
  define α where "α ≡ if Γ = {} then 0 else (1 + Max (Re ` Γ)) / 2"
  define K' where "K' ≡ cbox (Complex α (-C⇩3)) (Complex 1 C⇩3)"
  have Hα: "α ∈ {0..<1}"
  proof (cases "Γ = {}")
    case True thus ?thesis unfolding α_def by auto
  next
    case False hence hΓ: "Γ ≠ {}" .
    moreover have "Re a < 1" if Ha: "a ∈ Γ" for a
    proof (rule ccontr)
      assume "¬ Re a < 1" hence "1 ≤ Re a" by auto
      hence "zeta' a ≠ 0" by (subst zeta'_eq_zero_iff) (use zeta_Re_ge_1_nonzero in auto)
      thus False using Ha unfolding Γ_def by auto
    qed
    moreover have "∃a∈Γ. 0 ≤ Re a"
    proof -
      from hΓ have "∃a. a ∈ Γ" by auto
      moreover have "⋀a. a ∈ Γ ⟹ 0 ≤ Re a"
        unfolding Γ_def K_def by (auto simp add: in_cbox_complex_iff)
      ultimately show ?thesis by auto
    qed
    ultimately have "0 ≤ Max (Re ` Γ)" "Max (Re ` Γ) < 1"
      using fin by (auto simp add: Max_ge_iff)
    thus ?thesis unfolding α_def using hΓ by auto
  qed
  have nonzero: "zeta' z ≠ 0" when "z ∈ K'" for z
  proof (rule ccontr)
    assume "¬ zeta' z ≠ 0"
    moreover have "K' ⊆ K" unfolding K'_def K_def
      by (rule subset_box_imp) (insert Hα, simp add: Basis_complex_def)
    ultimately have Hz: "z ∈ Γ" unfolding Γ_def using that by auto
    hence "Re z ≤ Max (Re ` Γ)" using fin by (intro Max_ge) auto
    also have "… < α"
    proof -
      from Hz have "Γ ≠ {}" by auto
      thus ?thesis using Hα unfolding α_def by auto
    qed
    finally have "Re z < α" .
    moreover from ‹z ∈ K'› have "α ≤ Re z"
      unfolding K'_def by (simp add: in_cbox_complex_iff)
    ultimately show False by auto
  qed
  hence "logderiv zeta' analytic_on K'" by (intro analytic_intros)
  moreover have "compact K'" unfolding K'_def by auto
  ultimately have "bounded ((logderiv zeta') ` K')"
    by (intro analytic_imp_holomorphic holomorphic_on_imp_continuous_on
        compact_imp_bounded compact_continuous_image)
  from this [THEN rev_iffD1, OF bounded_pos]
  obtain M where
    hM: "⋀s. s ∈ K' ⟹ ∥logderiv zeta' s∥ ≤ M" by auto
  have "(λt. C⇩2 * (ln (t + 3))⇧2) ∈ O(λx. (ln x)⇧2)" using C⇩2_gt_zero by real_asymp
  then obtain γ where
    Hγ: "∀⇩F x in at_top. ∥C⇩2 * (ln (x + 3))⇧2∥ ≤ γ * ∥(ln x)⇧2∥"
    unfolding bigo_def by auto
  define C⇩5 where "C⇩5 ≡ max 1 γ"
  have C⇩5_gt_zero: "0 < C⇩5" unfolding C⇩5_def by auto
  have "∀⇩F x in at_top. γ * (ln x)⇧2 ≤ C⇩5 * (ln x)⇧2"
    by (intro eventuallyI mult_right_mono) (unfold C⇩5_def, auto)
  with Hγ have hC⇩5: "∀⇩F x in at_top. C⇩2 * (ln (x + 3))⇧2 ≤ C⇩5 * (ln x)⇧2"
    by eventually_elim (use C⇩2_gt_zero in auto)
  have "∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩5 * (ln x)⇧2"
    when h: "C⇩3 ≤ ¦t¦" "¦t¦ ≤ x" "1 < x"
            "C⇩4 / ln x ≤ C⇩1 / (7 * ln (x + 3))"
            "C⇩2 * (ln (x + 3))⇧2 ≤ C⇩5 * (ln x)⇧2" for x t
  proof -
    have "Re (Complex (1 - C⇩4 / ln x) t) ≠ Re 1" using C⇩4_gt_zero h(3) by auto
    hence "Complex (1 - C⇩4 / ln x) t ≠ 1" by metis
    hence "Complex (1 - C⇩4 / ln x) t ∈ zeta_strip_region' (1 - C⇩4 / ln x) x"
      unfolding zeta_strip_region'_def using h(1) h(2) by auto
    moreover hence "1 - 1 / 7 * C⇩1 / ln (x + 3) ≤ 1 - C⇩4 / ln x" using h(4) by auto
    ultimately have "∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩2 * (ln (¦Im (Complex (1 - C⇩4 / ln x) t)¦ + 3))⇧2"
      using strip_in_logderiv_zeta_region [where ?σ = "1 - C⇩4 / ln x" and ?T = x]
      by (intro logderiv_zeta_region_estimate) auto
    also have "… ≤ C⇩2 * (ln (x + 3))⇧2"
      by (intro mult_left_mono, subst power2_le_iff_abs_le)
         (use C⇩2_gt_zero h(2) h(3) in auto)
    also have "… ≤ C⇩5 * (ln x)⇧2" by (rule h(5))
    finally show ?thesis .
  qed
  hence "∀⇩F x in at_top. ∀t. C⇩3 ≤ ¦t¦ ⟶ ¦t¦ ≤ x
    ⟶ 1 < x ⟶ C⇩4 / ln x ≤ C⇩1 / (7 * ln (x + 3))
    ⟶ C⇩2 * (ln (x + 3))⇧2 ≤ C⇩5 * (ln x)⇧2
    ⟶ ∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩5 * (ln x)⇧2"
    by (intro eventuallyI) blast
  moreover have "∀⇩F x in at_top. (1 :: real) < x" by auto
  ultimately have 1: "∀⇩F x in at_top. ∀t. C⇩3 ≤ ¦t¦ ⟶ ¦t¦ ≤ x
    ⟶ ∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩5 * (ln x)⇧2"
    using C⇩4_prop hC⇩5 by eventually_elim blast
  define f where "f x ≡ 1 - C⇩4 / ln x" for x
  define g where "g x t ≡ Complex (f x) t" for x t
  let ?P = "λx t. ∥logderiv zeta (g x t)∥ ≤ M + ln x / C⇩4"
  have "α < 1" using Hα by auto
  hence "∀⇩F x in at_top. α ≤ f x" unfolding f_def using C⇩4_gt_zero by real_asymp
  moreover have f_lt_1: "∀⇩F x in at_top. f x < 1" unfolding f_def using C⇩4_gt_zero by real_asymp
  ultimately have "∀⇩F x in at_top. ∀t. ¦t¦ ≤ C⇩3 ⟶ g x t ∈ K' - {1}"
    unfolding g_def K'_def by eventually_elim (auto simp add: in_cbox_complex_iff legacy_Complex_simps)
  moreover have "∥logderiv zeta (g x t)∥ ≤ M + 1 / (1 - f x)"
    when h: "g x t ∈ K' - {1}" "f x < 1" for x t
  proof -
    from h(1) have ne_1: "g x t ≠ 1" by auto
    hence "∥logderiv zeta (g x t)∥ = ∥logderiv zeta' (g x t) - 1 / (g x t - 1)∥"
      using h(1) nonzero
      by (subst logderiv_zeta_eq_zeta')
         (auto simp add: zeta_eq_zero_iff_zeta' [symmetric])
    also have "… ≤ ∥logderiv zeta' (g x t)∥ + ∥1 / (g x t - 1)∥" by (rule norm_triangle_ineq4)
    also have "… ≤ M + 1 / (1 - f x)"
    proof -
      have "∥logderiv zeta' (g x t)∥ ≤ M" using that by (auto intro: hM)
      moreover have "¦Re (g x t - 1)¦ ≤ ∥g x t - 1∥" by (rule abs_Re_le_cmod)
      hence "∥1 / (g x t - 1)∥ ≤ 1 / (1 - f x)"
        using ne_1 h(2)
        by (auto simp add: norm_divide g_def
                 intro!: divide_left_mono mult_pos_pos)
      ultimately show ?thesis by auto
    qed
    finally show ?thesis .
  qed
  hence "∀⇩F x in at_top. ∀t. f x < 1
    ⟶ g x t ∈ K' - {1} 
    ⟶ ∥logderiv zeta (g x t)∥ ≤ M + 1 / (1 - f x)" by auto
  ultimately have "∀⇩F x in at_top. ∀t. ¦t¦ ≤ C⇩3 ⟶ ∥logderiv zeta (g x t)∥ ≤ M + 1 / (1 - f x)"
    using f_lt_1 by eventually_elim blast
  hence "∀⇩F x in at_top. ∀t. ¦t¦ ≤ C⇩3 ⟶ ∥logderiv zeta (g x t)∥ ≤ M + ln x / C⇩4" unfolding f_def by auto
  moreover have "∀⇩F x in at_top. M + ln x / C⇩4 ≤ C⇩5 * (ln x)⇧2" using C⇩4_gt_zero C⇩5_gt_zero by real_asymp
  ultimately have 2: "∀⇩F x in at_top. ∀t. ¦t¦ ≤ C⇩3 ⟶ ∥logderiv zeta (g x t)∥ ≤ C⇩5 * (ln x)⇧2" by eventually_elim auto
  show ?thesis
  proof (unfold C⇩5_prop_def, intro exI conjI)
    show "0 < C⇩5" by (rule C⇩5_gt_zero)+
    have "∀⇩F x in at_top. ∀t. C⇩3 ≤ ¦t¦ ∨ ¦t¦ ≤ C⇩3"
      by (rule eventuallyI) auto
    with 1 2 show "∀⇩F x in at_top. ∀t. ¦t¦ ≤ x ⟶ ∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩5 * (ln x)⇧2"
      unfolding f_def g_def by eventually_elim blast
  qed
qed

definition C⇩5 where "C⇩5 ≡ SOME C⇩5. C⇩5_prop C⇩5"

lemma
  C⇩5_gt_zero: "0 < C⇩5" (is ?prop_1) and
  logderiv_zeta_bound_vertical:
    "∀⇩F x in at_top. ∀t. ¦t¦ ≤ x
      ⟶ ∥logderiv zeta (Complex (1 - C⇩4 / ln x) t)∥ ≤ C⇩5 * (ln x)⇧2" (is ?prop_2)
proof -
  have "C⇩5_prop C⇩5" unfolding C⇩5_def
    by (rule someI_ex) (rule logderiv_zeta_bound_vertical')
  thus ?prop_1 ?prop_2 unfolding C⇩5_prop_def by auto
qed

section ‹Deducing prime number theorem using Perron's formula›

locale prime_number_theorem =
  fixes c ε :: real
  assumes Hc: "0 < c" and Hc': "c * c < 2 * C⇩4" and Hε: "0 < ε" "2 * ε < c"
begin
notation primes_psi ("ψ")
definition H where "H x ≡ exp (c / 2 * (ln x) powr (1 / 2))" for x :: real
definition T where "T x ≡ exp (c * (ln x) powr (1 / 2))" for x :: real
definition a where "a x ≡ 1 - C⇩4 / (c * (ln x) powr (1 / 2))" for x :: real
definition b where "b x ≡ 1 + 1 / (ln x)" for x :: real
definition B where "B x ≡ 5 / 4 * ln x" for x :: real
definition f where "f x s ≡ x powr s / s * logderiv zeta s" for x :: real and s :: complex
definition R where "R x ≡
  x powr (b x) * H x * B x / T x + 3 * (2 + ln (T x / b x))
  * (∑n | x - x / H x ≤ n ∧ n ≤ x + x / H x. ∥fds_nth (fds mangoldt_complex) n∥)" for x :: real
definition Rc' where "Rc' ≡ O(λx. x * exp (- (c / 2 - ε) * ln x powr (1 / 2)))"
definition Rc where "Rc ≡ O(λx. x * exp (- (c / 2 - 2 * ε) * ln x powr (1 / 2)))"
definition z⇩1 where "z⇩1 x ≡ Complex (a x) (- T x)" for x
definition z⇩2 where "z⇩2 x ≡ Complex (b x) (- T x)" for x
definition z⇩3 where "z⇩3 x ≡ Complex (b x) (T x)" for x
definition z⇩4 where "z⇩4 x ≡ Complex (a x) (T x)" for x
definition rect where "rect x ≡ cbox (z⇩1 x) (z⇩3 x)" for x
definition rect' where "rect' x ≡ rect x - {1}" for x
definition P⇩t where "P⇩t x t ≡ linepath (Complex (a x) t) (Complex (b x) t)" for x t
definition P⇩1 where "P⇩1 x ≡ linepath (z⇩1 x) (z⇩4 x)" for x
definition P⇩2 where "P⇩2 x ≡ linepath (z⇩2 x) (z⇩3 x)" for x
definition P⇩3 where "P⇩3 x ≡ P⇩t x (- T x)" for x
definition P⇩4 where "P⇩4 x ≡ P⇩t x (T x)" for x
definition P⇩r where "P⇩r x ≡ rectpath (z⇩1 x) (z⇩3 x)" for x

lemma Rc_eq_rem_est:
  "Rc = rem_est (c / 2 - 2 * ε) (1 / 2) 0"
proof -
  have *: "∀⇩F x :: real in at_top. 0 < ln (ln x)" by real_asymp
  show ?thesis unfolding Rc_def rem_est_def
    by (rule landau_o.big.cong) (use * in eventually_elim, auto)
qed

lemma residue_f:
  "residue (f x) 1 = - x"
proof -
  define A where "A ≡ box (Complex 0 (- 1 / 2)) (Complex 2 (1 / 2))"
  have hA: "0 ∉ A" "1 ∈ A" "open A"
    unfolding A_def by (auto simp add: mem_box Basis_complex_def)
  have "zeta' s ≠ 0" when "s ∈ A" for s
  proof -
    have "s ≠ 1 ⟹ zeta s ≠ 0"
      using that unfolding A_def
      by (intro zeta_nonzero_small_imag)
         (auto simp add: mem_box Basis_complex_def)
    thus ?thesis by (subst zeta'_eq_zero_iff) auto
  qed
  hence h: "(λs. x powr s / s * logderiv zeta' s) holomorphic_on A"
    by (intro holomorphic_intros) (use hA in auto)
  have h': "(λs. x powr s / (s * (s - 1))) holomorphic_on A - {1}"
    by (auto intro!: holomorphic_intros) (use hA in auto)
  have s_ne_1: "∀⇩F s :: complex in at 1. s ≠ 1"
    by (subst eventually_at_filter) auto
  moreover have "∀⇩F s in at 1. zeta s ≠ 0"
    by (intro non_zero_neighbour_pole is_pole_zeta)
  ultimately have "∀⇩F s in at 1. logderiv zeta s = logderiv zeta' s - 1 / (s - 1)"
    by eventually_elim (rule logderiv_zeta_eq_zeta')
  moreover have
    "f x s = x powr s / s * logderiv zeta' s - x powr s / s / (s - 1)"
    when "logderiv zeta s = logderiv zeta' s - 1 / (s - 1)" "s ≠ 0" "s ≠ 1" for s :: complex
    unfolding f_def by (subst that(1)) (insert that, auto simp add: field_simps)
  hence "∀⇩F s :: complex in at 1. s ≠ 0 ⟶ s ≠ 1
    ⟶ logderiv zeta s = logderiv zeta' s - 1 / (s - 1)
    ⟶ f x s = x powr s / s * logderiv zeta' s - x powr s / s / (s - 1)"
    by (intro eventuallyI) blast
  moreover have "∀⇩F s :: complex in at 1. s ≠ 0"
    by (subst eventually_at_topological)
       (intro exI [of _ "UNIV - {0}"], auto)
  ultimately have "∀⇩F s :: complex in at 1. f x s = x powr s / s * logderiv zeta' s - x powr s / s / (s - 1)"
    using s_ne_1 by eventually_elim blast
  hence "residue (f x) 1 = residue (λs. x powr s / s * logderiv zeta' s - x powr s / s / (s - 1)) 1"
    by (intro residue_cong refl)
  also have "… = residue (λs. x powr s / s * logderiv zeta' s) 1 - residue (λs. x powr s / s / (s - 1)) 1"
    by (subst residue_diff [where ?s = A]) (use h h' hA in auto)
  also have "… = - x"
  proof -
    have "residue (λs. x powr s / s * logderiv zeta' s) 1 = 0"
      by (rule residue_holo [where ?s = A]) (use hA h in auto)
    moreover have "residue (λs. x powr s / s / (s - 1)) 1 = (x :: complex) powr 1 / 1"
      by (rule residue_simple [where ?s = A]) (use hA in ‹auto intro!: holomorphic_intros›)
    ultimately show ?thesis by auto
  qed
  finally show ?thesis .
qed

lemma rect_in_strip:
  "rect x - {1} ⊆ zeta_strip_region (a x) (T x)"
  unfolding rect_def zeta_strip_region_def z⇩1_def z⇩3_def
  by (auto simp add: in_cbox_complex_iff)

lemma rect_in_strip':
  "{s ∈ rect x. C⇩3 ≤ ¦Im s¦} ⊆ zeta_strip_region' (a x) (T x)"
  unfolding rect_def zeta_strip_region'_def z⇩1_def z⇩3_def
  using C⇩3_gt_zero by (auto simp add: in_cbox_complex_iff)

lemma
  rect'_in_zerofree: "∀⇩F x in at_top. rect' x ⊆ zeta_zerofree_region" and
  rect_in_logderiv_zeta: "∀⇩F x in at_top. {s ∈ rect x. C⇩3 ≤ ¦Im s¦} ⊆ logderiv_zeta_region"
proof (goal_cases)
  case 1 have
    "∀⇩F x in at_top. C⇩4 / ln x ≤ C⇩1 / (7 * ln (x + 3))" by (rule C⇩4_prop)
  moreover have "LIM x at_top. exp (c * (ln x) powr (1 / 2)) :> at_top" using Hc by real_asymp
  ultimately have h:
   "∀⇩F x in at_top. C⇩4 / ln (exp (c * (ln x) powr (1 / 2)))
    ≤ C⇩1 / (7 * ln (exp (c * (ln x) powr (1 / 2)) + 3))" (is "eventually ?P _")
    by (rule eventually_compose_filterlim)
  moreover have
    "?P x ⟹ zeta_strip_region (a x) (T x) ⊆ zeta_zerofree_region"
    (is "_ ⟹ ?Q") for x unfolding T_def a_def
    by (intro strip_in_zerofree_region strip_condition_imp) auto
  hence "∀⇩F x in at_top. ?P x ⟶ ?Q x" by (intro eventuallyI) blast
  ultimately show ?case unfolding rect'_def by eventually_elim (use rect_in_strip in auto)
  case 2 from h have
    "?P x ⟹ zeta_strip_region' (a x) (T x) ⊆ logderiv_zeta_region"
    (is "_ ⟹ ?Q") for x unfolding T_def a_def
    by (intro strip_in_logderiv_zeta_region) auto
  hence "∀⇩F x in at_top. ?P x ⟶ ?Q x" by (intro eventuallyI) blast
  thus ?case using h by eventually_elim (use rect_in_strip' in auto)
qed

lemma zeta_nonzero_in_rect:
  "∀⇩F x in at_top. ∀s. s ∈ rect' x ⟶ zeta s ≠ 0"
  using rect'_in_zerofree by eventually_elim (use zeta_zerofree_region in auto)

lemma zero_notin_rect: "∀⇩F x in at_top. 0 ∉ rect' x"
proof -
  have "∀⇩F x in at_top. C⇩4 / (c * (ln x) powr (1 / 2)) < 1"
    using Hc by real_asymp
  thus ?thesis
    unfolding rect'_def rect_def z⇩1_def z⇩4_def T_def a_def
    by eventually_elim (simp add: in_cbox_complex_iff)
qed

lemma f_analytic:
  "∀⇩F x in at_top. f x analytic_on rect' x"
  using zeta_nonzero_in_rect zero_notin_rect unfolding f_def
  by eventually_elim (intro analytic_intros, auto simp: rect'_def)

lemma path_image_in_rect_1:
  assumes "0 ≤ T x ∧ a x ≤ b x"
  shows "path_image (P⇩1 x) ⊆ rect x ∧ path_image (P⇩2 x) ⊆ rect x"
  unfolding P⇩1_def P⇩2_def rect_def z⇩1_def z⇩2_def z⇩3_def z⇩4_def
  by (simp, intro conjI closed_segment_subset)
     (insert assms, auto simp add: in_cbox_complex_iff)

lemma path_image_in_rect_2:
  assumes "0 ≤ T x ∧ a x ≤ b x ∧ t ∈ {-T x..T x}"
  shows "path_image (P⇩t x t) ⊆ rect x"
  unfolding P⇩t_def rect_def z⇩1_def z⇩3_def
  by (simp, intro conjI closed_segment_subset)
     (insert assms, auto simp add: in_cbox_complex_iff)

definition path_in_rect' where
"path_in_rect' x ≡
  path_image (P⇩1 x) ⊆ rect' x ∧ path_image (P⇩2 x) ⊆ rect' x ∧
  path_image (P⇩3 x) ⊆ rect' x ∧ path_image (P⇩4 x) ⊆ rect' x"

lemma path_image_in_rect':
  assumes "0 < T x ∧ a x < 1 ∧ 1 < b x"
  shows "path_in_rect' x"
proof -
  have "path_image (P⇩1 x) ⊆ rect x ∧ path_image (P⇩2 x) ⊆ rect x"
    by (rule path_image_in_rect_1) (use assms in auto)
  moreover have "path_image (P⇩3 x) ⊆ rect x" "path_image (P⇩4 x) ⊆ rect x"
    unfolding P⇩3_def P⇩4_def
    by (intro path_image_in_rect_2, (use assms in auto)[1])+
  moreover have
    "1 ∉ path_image (P⇩1 x) ∧ 1 ∉ path_image (P⇩2 x) ∧
     1 ∉ path_image (P⇩3 x) ∧ 1 ∉ path_image (P⇩4 x)"
    unfolding P⇩1_def P⇩2_def P⇩3_def P⇩4_def P⇩t_def z⇩1_def z⇩2_def z⇩3_def z⇩4_def using assms
    by (auto simp add: closed_segment_def legacy_Complex_simps field_simps)
  ultimately show ?thesis unfolding path_in_rect'_def rect'_def by blast
qed

lemma asymp_1:
  "∀⇩F x in at_top. 0 < T x ∧ a x < 1 ∧ 1 < b x"
  unfolding T_def a_def b_def
  by (intro eventually_conj, insert Hc C⇩4_gt_zero) (real_asymp)+

lemma f_continuous_on:
  "∀⇩F x in at_top. ∀A⊆rect' x. continuous_on A (f x)"
  using f_analytic
  by (eventually_elim, safe)
     (intro holomorphic_on_imp_continuous_on analytic_imp_holomorphic,
      elim analytic_on_subset)

lemma contour_integrability:
  "∀⇩F x in at_top.
    f x contour_integrable_on P⇩1 x ∧ f x contour_integrable_on P⇩2 x ∧
    f x contour_integrable_on P⇩3 x ∧ f x contour_integrable_on P⇩4 x"
proof -
  have "∀⇩F x in at_top. path_in_rect' x"
    using asymp_1 by eventually_elim (rule path_image_in_rect')
  thus ?thesis using f_continuous_on
    unfolding P⇩1_def P⇩2_def P⇩3_def P⇩4_def P⇩t_def path_in_rect'_def
    by eventually_elim
       (intro conjI contour_integrable_continuous_linepath,
        fold z⇩1_def z⇩2_def z⇩3_def z⇩4_def, auto)
qed

lemma contour_integral_rectpath':
  assumes "f x analytic_on (rect' x)" "0 < T x ∧ a x < 1 ∧ 1 < b x"
  shows "contour_integral (P⇩r x) (f x) = - 2 * pi * 𝗂 * x"
proof -
  define z where "z ≡ (1 + b x) / 2"
  have Hz: "z ∈ box (z⇩1 x) (z⇩3 x)"
    unfolding z⇩1_def z⇩3_def z_def using assms(2)
    by (auto simp add: mem_box Basis_complex_def)
  have Hz': "z ≠ 1" unfolding z_def using assms(2) by auto
  have "connected (rect' x)"
  proof -
    have box_nonempty: "box (z⇩1 x) (z⇩3 x) ≠ {}" using Hz by auto
    hence "aff_dim (closure (box (z⇩1 x) (z⇩3 x))) = 2"
      by (subst closure_aff_dim, subst aff_dim_open) auto
    thus ?thesis
      unfolding rect'_def using box_nonempty
      by (subst (asm) closure_box)
         (auto intro: connected_punctured_convex simp add: rect_def)
  qed
  moreover have Hz'': "z ∈ rect' x"
    unfolding rect'_def rect_def using box_subset_cbox Hz Hz' by auto
  ultimately obtain T where hT:
    "f x holomorphic_on T" "open T" "rect' x ⊆ T" "connected T"
    using analytic_on_holomorphic_connected assms(1) by (metis dual_order.refl)
  define U where "U ≡ T ∪ box (z⇩1 x) (z⇩3 x)"
  have one_in_box: "1 ∈ box (z⇩1 x) (z⇩3 x)"
    unfolding z⇩1_def z⇩3_def z_def using assms(2) by (auto simp add: mem_box Basis_complex_def)
  have "contour_integral (P⇩r x) (f x) = 2 * pi * 𝗂 *
    (∑s∈{1}. winding_number (P⇩r x) s * residue (f x) s)"
  proof (rule Residue_theorem)
    show "finite {1}" "valid_path (P⇩r x)" "pathfinish (P⇩r x) = pathstart (P⇩r x)"
      unfolding P⇩r_def by auto
    show "open U" unfolding U_def using hT(2) by auto
    show "connected U" unfolding U_def
      by (intro connected_Un hT(4) convex_connected)
         (use Hz Hz'' hT(3) in auto)
    have "f x holomorphic_on box (z⇩1 x) (z⇩3 x) - {1}"
      by (rule holomorphic_on_subset, rule analytic_imp_holomorphic, rule assms(1))
         (unfold rect'_def rect_def, use box_subset_cbox in auto)
    hence "f x holomorphic_on ((T - {1}) ∪ (box (z⇩1 x) (z⇩3 x) - {1}))"
      by (intro holomorphic_on_Un) (use hT(1) hT(2) in auto)
    moreover have "… = U - {1}" unfolding U_def by auto
    ultimately show "f x holomorphic_on U - {1}" by auto
    have Hz: "Re (z⇩1 x) ≤ Re (z⇩3 x)" "Im (z⇩1 x) ≤ Im (z⇩3 x)"
      unfolding z⇩1_def z⇩3_def using assms(2) by auto
    have "path_image (P⇩r x) = rect x - box (z⇩1 x) (z⇩3 x)"
      unfolding rect_def P⇩r_def
      by (intro path_image_rectpath_cbox_minus_box Hz)
    thus "path_image (P⇩r x) ⊆ U - {1}"
      using one_in_box hT(3) U_def unfolding rect'_def by auto
    have hU': "rect x ⊆ U"
      using hT(3) one_in_box unfolding U_def rect'_def by auto
    show "∀z. z ∉ U ⟶ winding_number (P⇩r x) z = 0"
      using Hz P⇩r_def hU' rect_def winding_number_rectpath_outside by fastforce
  qed
  also have "… = - 2 * pi * 𝗂 * x" unfolding P⇩r_def
    by (simp add: residue_f, subst winding_number_rectpath, auto intro: one_in_box)
  finally show ?thesis .
qed

lemma contour_integral_rectpath:
  "∀⇩F x in at_top. contour_integral (P⇩r x) (f x) = - 2 * pi * 𝗂 * x"
  using f_analytic asymp_1 by eventually_elim (rule contour_integral_rectpath')

lemma valid_paths:
  "valid_path (P⇩1 x)" "valid_path (P⇩2 x)" "valid_path (P⇩3 x)" "valid_path (P⇩4 x)"
  unfolding P⇩1_def P⇩2_def P⇩3_def P⇩4_def P⇩t_def by auto

lemma integral_rectpath_split:
  assumes "f x contour_integrable_on P⇩1 x ∧ f x contour_integrable_on P⇩2 x ∧
           f x contour_integrable_on P⇩3 x ∧ f x contour_integrable_on P⇩4 x"
  shows "contour_integral (P⇩3 x) (f x) + contour_integral (P⇩2 x) (f x)
       - contour_integral (P⇩4 x) (f x) - contour_integral (P⇩1 x) (f x) = contour_integral (P⇩r x) (f x)"
proof -
  define Q⇩1 where "Q⇩1 ≡ linepath (z⇩3 x) (z⇩4 x)"
  define Q⇩2 where "Q⇩2 ≡ linepath (z⇩4 x) (z⇩1 x)"
  have Q_eq: "Q⇩1 = reversepath (P⇩4 x)" "Q⇩2 = reversepath (P⇩1 x)"
    unfolding Q⇩1_def Q⇩2_def P⇩1_def P⇩4_def P⇩t_def by (fold z⇩3_def z⇩4_def) auto
  hence "contour_integral Q⇩1 (f x) = - contour_integral (P⇩4 x) (f x)"
        "contour_integral Q⇩2 (f x) = - contour_integral (P⇩1 x) (f x)"
    by (auto intro: contour_integral_reversepath valid_paths)
  moreover have "contour_integral (P⇩3 x +++ P⇩2 x +++ Q⇩1 +++ Q⇩2) (f x)
       = contour_integral (P⇩3 x) (f x) + contour_integral (P⇩2 x) (f x)
       + contour_integral Q⇩1 (f x) + contour_integral Q⇩2 (f x)"
  proof -
    have 1: "pathfinish (P⇩2 x) = pathstart (Q⇩1 +++ Q⇩2)" "pathfinish Q⇩1 = pathstart Q⇩2"
      unfolding P⇩2_def Q⇩1_def Q⇩2_def by auto
    have 2: "valid_path Q⇩1" "valid_path Q⇩2" unfolding Q⇩1_def Q⇩2_def by auto
    have 3: "f x contour_integrable_on P⇩1 x" "f x contour_integrable_on P⇩2 x"
            "f x contour_integrable_on P⇩3 x" "f x contour_integrable_on P⇩4 x"
            "f x contour_integrable_on Q⇩1" "f x contour_integrable_on Q⇩2"
      using assms by (auto simp add: Q_eq intro: contour_integrable_reversepath valid_paths)
    show ?thesis by (subst contour_integral_join |
      auto intro: valid_paths valid_path_join contour_integrable_joinI 1 2 3)+
  qed
  ultimately show ?thesis
    unfolding P⇩r_def z⇩1_def z⇩3_def rectpath_def
    by (simp add: Let_def, fold P⇩t_def P⇩3_def z⇩1_def z⇩2_def z⇩3_def z⇩4_def)
       (fold P⇩2_def Q⇩1_def Q⇩2_def, auto)
qed

lemma P⇩2_eq:
  "∀⇩F x in at_top. contour_integral (P⇩2 x) (f x) + 2 * pi * 𝗂 * x
  = contour_integral (P⇩1 x) (f x) - contour_integral (P⇩3 x) (f x) + contour_integral (P⇩4 x) (f x)"
proof -
  have "∀⇩F x in at_top. contour_integral (P⇩3 x) (f x) + contour_integral (P⇩2 x) (f x)
      - contour_integral (P⇩4 x) (f x) - contour_integral (P⇩1 x) (f x) = - 2 * pi * 𝗂 * x"
    using contour_integrability contour_integral_rectpath asymp_1 f_analytic
    by eventually_elim (metis integral_rectpath_split)
  thus ?thesis by (auto simp add: field_simps)
qed

lemma estimation_P⇩1:
  "(λx. ∥contour_integral (P⇩1 x) (f x)∥) ∈ Rc"
proof -
  define r where "r x ≡
    C⇩5 * (c * (ln x) powr (1 / 2))⇧2 * x powr a x * ln (1 + T x / a x)" for x
  note logderiv_zeta_bound_vertical
  moreover have "LIM x at_top. T x :> at_top"
    unfolding T_def using Hc by real_asymp
  ultimately have "∀⇩F x in at_top. ∀t. ¦t¦ ≤ T x
    ⟶ ∥logderiv zeta (Complex (1 - C⇩4 / ln (T x)) t)∥ ≤ C⇩5 * (ln (T x))⇧2"
    unfolding a_def by (rule eventually_compose_filterlim)
  hence "∀⇩F x in at_top. ∀t. ¦t¦ ≤ T x
    ⟶ ∥logderiv zeta (Complex (a x) t)∥ ≤ C⇩5 * (c * (ln x) powr (1 / 2))⇧2"
    unfolding a_def T_def by auto
  moreover have "∀⇩F x in at_top. (f x) contour_integrable_on (P⇩1 x)"
    using contour_integrability by eventually_elim auto
  hence "∀⇩F x in at_top. (λs. logderiv zeta s * x powr s / s) contour_integrable_on (P⇩1 x)"
     unfolding f_def by eventually_elim (auto simp add: field_simps)
  moreover have "∀⇩F x :: real in at_top. 0 < x" by auto
  moreover have "∀⇩F x in at_top. 0 < a x" unfolding a_def using Hc by real_asymp
  ultimately have "∀⇩F x in at_top.
    ∥1 / (2 * pi * 𝗂) * contour_integral (P⇩1 x) (λs. logderiv zeta s * x powr s / s)∥ ≤ r x"
    unfolding r_def P⇩1_def z⇩1_def z⇩4_def using asymp_1
    by eventually_elim (rule perron_aux_3', auto)
  hence "∀⇩F x in at_top. ∥1 / (2 * pi * 𝗂) * contour_integral (P⇩1 x) (f x)∥ ≤ r x"
    unfolding f_def by eventually_elim (auto simp add: mult_ac)
  hence "(λx. ∥1 / (2 * pi * 𝗂) * contour_integral (P⇩1 x) (f x)∥) ∈ O(r)"
    unfolding f_def by (rule eventually_le_imp_bigo')
  moreover have "r ∈ Rc"
  proof -
    define r⇩1 where "r⇩1 x ≡ C⇩5 * c⇧2 * ln x * ln (1 + T x / a x)" for x
    define r⇩2 where "r⇩2 x ≡ exp (a x * ln x)" for x
    have "r⇩1 ∈ O(λx. (ln x)⇧2)"
      unfolding r⇩1_def T_def a_def using Hc C⇩5_gt_zero by real_asymp
    moreover have "r⇩2 ∈ Rc'"
    proof -
      have 1: "∥r⇩2 x∥ ≤ x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2))"
        when h: "0 < x" "0 < ln x" for x
      proof -
        have "a x * ln x = ln x + - C⇩4 / c * (ln x) powr (1 / 2)"
          unfolding a_def using h(2) Hc
          by (auto simp add: field_simps powr_add [symmetric] frac_eq_eq)
        hence "r⇩2 x = exp (…)" unfolding r⇩2_def by blast
        also have "… = x * exp (- C⇩4 / c * (ln x) powr (1 / 2))"
          by (subst exp_add) (use h(1) in auto)
        also have "… ≤ x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2))"
          by (intro mult_left_mono, subst exp_le_cancel_iff, intro mult_right_mono)
             (use Hc Hc' Hε C⇩4_gt_zero h in ‹auto simp: field_simps intro: add_increasing2›)
        finally show ?thesis unfolding r⇩2_def by auto
      qed
      have "∀⇩F x in at_top. ∥r⇩2 x∥ ≤ x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2))"
        using ln_asymp_pos x_asymp_pos by eventually_elim (rule 1)
      thus ?thesis unfolding Rc'_def by (rule eventually_le_imp_bigo)
    qed
    ultimately have "(λx. r⇩1 x * r⇩2 x)
      ∈ O(λx. (ln x)⇧2 * (x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2))))"
      unfolding Rc'_def by (rule landau_o.big.mult)
    moreover have "(λx. (ln x)⇧2 * (x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2)))) ∈ Rc"
      unfolding Rc_def using Hc Hε
      by (real_asymp simp add: field_simps)
    ultimately have "(λx. r⇩1 x * r⇩2 x) ∈ Rc"
      unfolding Rc_def by (rule landau_o.big_trans)
    moreover have "∀⇩F x in at_top. r x = r⇩1 x * r⇩2 x"
      using ln_ln_asymp_pos ln_asymp_pos x_asymp_pos
      unfolding r_def r⇩1_def r⇩2_def a_def powr_def power2_eq_square
      by (eventually_elim) (simp add: field_simps exp_add [symmetric])
    ultimately show ?thesis unfolding Rc_def
      using landau_o.big.ev_eq_trans2 by auto
  qed
  ultimately have "(λx. ∥1 / (2 * pi * 𝗂) * contour_integral (P⇩1 x) (f x)∥) ∈ Rc"
    unfolding Rc_def by (rule landau_o.big_trans)
  thus ?thesis unfolding Rc_def by (simp add: norm_divide)
qed

lemma estimation_P⇩t':
  assumes h:
    "1 < x ∧ max 1 C⇩3 ≤ T x" "a x < 1 ∧ 1 < b x"
    "{s ∈ rect x. C⇩3 ≤ ¦Im s¦} ⊆ logderiv_zeta_region"
    "f x contour_integrable_on P⇩3 x ∧ f x contour_integrable_on P⇩4 x"
    and Ht: "¦t¦ = T x"
  shows "∥contour_integral (P⇩t x t) (f x)∥ ≤ C⇩2 * exp 1 * x / T x * (ln (T x + 3))⇧2 * (b x - a x)"
proof -
  consider "t = T x" | "t = - T x" using Ht by fastforce
  hence "f x contour_integrable_on P⇩t x t"
    using Ht h(4) unfolding P⇩t_def P⇩3_def P⇩4_def by cases auto
  moreover have "∥f x s∥ ≤ exp 1 * x / T x * (C⇩2 * (ln (T x + 3))⇧2)"
    when "s ∈ closed_segment (Complex (a x) t) (Complex (b x) t)" for s
  proof -
    have Hs: "s ∈ path_image (P⇩t x t)" using that unfolding P⇩t_def by auto
    have "path_image (P⇩t x t) ⊆ rect x"
      by (rule path_image_in_rect_2) (use h(2) Ht in auto)
    moreover have Hs': "Re s ≤ b x" "Im s = t"
    proof -
      have "u ≤ 1 ⟹ (1 - u) * a x ≤ (1 - u) * b x" for u
        using h(2) by (intro mult_left_mono) auto
      thus "Re s ≤ b x" "Im s = t"
        using that h(2) unfolding closed_segment_def
        by (auto simp add: legacy_Complex_simps field_simps)
    qed
    hence "C⇩3 ≤ ¦Im s¦" using h(1) Ht by auto
    ultimately have "s ∈ logderiv_zeta_region" using Hs h(3) by auto
    hence "∥logderiv zeta s∥ ≤ C⇩2 * (ln (¦Im s¦ + 3))⇧2"
      by (rule logderiv_zeta_region_estimate)
    also have "… = C⇩2 * (ln (T x + 3))⇧2" using Hs'(2) Ht by auto
    also have "∥x powr s / s∥ ≤ exp 1 * x / T x"
    proof -
      have "∥x powr s∥ = Re x powr Re s" using h(1) by (intro norm_powr_real_powr) auto
      also have "… = x powr Re s" by auto
      also have "… ≤ x powr b x" by (intro powr_mono Hs') (use h(1) in auto)
      also have "… = exp 1 * x"
        using h(1) unfolding powr_def b_def by (auto simp add: field_simps exp_add)
      finally have "∥x powr s∥ ≤ exp 1 * x" .
      moreover have "T x ≤ ∥s∥" using abs_Im_le_cmod [of s] Hs'(2) h(1) Ht by auto
      hence 1: "∥x powr s∥ / ∥s∥ ≤ ∥x powr s∥ / T x"
        using h(1) by (intro divide_left_mono mult_pos_pos) auto
      ultimately have "… ≤ exp 1 * x / T x"
        by (intro divide_right_mono) (use h(1) in auto)
      thus ?thesis using 1 by (subst norm_divide) linarith
    qed
    ultimately show ?thesis unfolding f_def
      by (subst norm_mult, intro mult_mono, auto)
         (metis norm_ge_zero order.trans)
  qed
  ultimately have "∥contour_integral (P⇩t x t) (f x)∥
    ≤ exp 1 * x / T x * (C⇩2 * (ln (T x + 3))⇧2) * ∥Complex (b x) t - Complex (a x) t∥"
    unfolding P⇩t_def
    by (intro contour_integral_bound_linepath)
       (use C⇩2_gt_zero h(1) in auto)
  also have "… = C⇩2 * exp 1 * x / T x * (ln (T x + 3))⇧2 * (b x - a x)"
    using h(2) by (simp add: legacy_Complex_simps)
  finally show ?thesis .
qed

lemma estimation_P⇩t:
  "(λx. ∥contour_integral (P⇩3 x) (f x)∥) ∈ Rc ∧
   (λx. ∥contour_integral (P⇩4 x) (f x)∥) ∈ Rc"
proof -
  define r where "r x ≡ C⇩2 * exp 1 * x / T x * (ln (T x + 3))⇧2 * (b x - a x)" for x
  define p where "p x ≡ ∥contour_integral (P⇩3 x) (f x)∥ ≤ r x ∧ ∥contour_integral (P⇩4 x) (f x)∥ ≤ r x" for x
  have "∀⇩F x in at_top. 1 < x ∧ max 1 C⇩3 ≤ T x"
    unfolding T_def by (rule eventually_conj) (simp, use Hc in real_asymp)
  hence "∀⇩F x in at_top. ∀t. ¦t¦ = T x ⟶ ∥contour_integral (P⇩t x t) (f x)∥ ≤ r x" (is "eventually ?P _")
    unfolding r_def using asymp_1 rect_in_logderiv_zeta contour_integrability
    by eventually_elim (use estimation_P⇩t' in blast)
  moreover have "⋀x. ?P x ⟹ 0 < T x ⟹ p x"
    unfolding p_def P⇩3_def P⇩4_def by auto
  hence "∀⇩F x in at_top. ?P x ⟶ 0 < T x ⟶ p x"
    by (intro eventuallyI) blast
  ultimately have "∀⇩F x in at_top. p x" using asymp_1 by eventually_elim blast
  hence "∀⇩F x in at_top.
    ∥∥contour_integral (P⇩3 x) (f x)∥∥ ≤ 1 * ∥r x∥ ∧
    ∥∥contour_integral (P⇩4 x) (f x)∥∥ ≤ 1 * ∥r x∥"
    unfolding p_def by eventually_elim auto
  hence "(λx. ∥contour_integral (P⇩3 x) (f x)∥) ∈ O(r) ∧ (λx. ∥contour_integral (P⇩4 x) (f x)∥) ∈ O(r)"
    by (subst (asm) eventually_conj_iff, blast)+
  moreover have "r ∈ Rc"
    unfolding r_def Rc_def a_def b_def T_def using Hc Hε
    by (real_asymp simp add: field_simps)
  ultimately show ?thesis
    unfolding Rc_def using landau_o.big_trans by blast
qed

lemma Re_path_P⇩2:
  "⋀z. z ∈ path_image (P⇩2 x) ⟹ Re z = b x"
  unfolding P⇩2_def z⇩2_def z⇩3_def
  by (auto simp add: closed_segment_def legacy_Complex_simps field_simps)

lemma estimation_P⇩2:
  "(λx. ∥1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x) + x∥) ∈ Rc"
proof -
  define r where "r x ≡ ∥contour_integral (P⇩1 x) (f x)∥ +
    ∥contour_integral (P⇩3 x) (f x)∥ + ∥contour_integral (P⇩4 x) (f x)∥" for x
  have [simp]: "∥a - b + c∥ ≤ ∥a∥ + ∥b∥ + ∥c∥" for a b c :: complex
    using adhoc_norm_triangle norm_triangle_ineq4 by blast
  have "∀⇩F x in at_top. ∥contour_integral (P⇩2 x) (f x) + 2 * pi * 𝗂 * x∥ ≤ r x"
    unfolding r_def using P⇩2_eq by eventually_elim auto
  hence "(λx. ∥contour_integral (P⇩2 x) (f x) + 2 * pi * 𝗂 * x∥) ∈ O(r)"
    by (rule eventually_le_imp_bigo')
  moreover have "r ∈ Rc"
    using estimation_P⇩1 estimation_P⇩t
    unfolding r_def Rc_def by (intro sum_in_bigo) auto
  ultimately have "(λx. ∥contour_integral (P⇩2 x) (f x) + 2 * pi * 𝗂 * x∥) ∈ Rc"
    unfolding Rc_def by (rule landau_o.big_trans)
  hence "(λx. ∥1 / (2 * pi * 𝗂) * (contour_integral (P⇩2 x) (f x) + 2 * pi * 𝗂 * x)∥) ∈ Rc"
    unfolding Rc_def by (auto simp add: norm_mult norm_divide)
  thus ?thesis by (auto simp add: algebra_simps)
qed

lemma estimation_R:
  "R ∈ Rc"
proof -
  define Γ where "Γ x ≡ {n :: nat. x - x / H x ≤ n ∧ n ≤ x + x / H x}" for x
  have 1: "(λx. x powr b x * H x * B x / T x) ∈ Rc"
    unfolding b_def H_def B_def T_def Rc_def using Hc Hε
    by (real_asymp simp add: field_simps)
  have "∥∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥∥ ≤ (2 * x / H x + 1) * ln (x + x / H x)"
    when h: "0 < x - x / H x" "0 < x / H x" "0 ≤ ln (x + x / H x)" for x
  proof -
    have "∥∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥∥ = (∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥)"
      by simp (subst abs_of_nonneg, auto intro: sum_nonneg)
    also have "… = sum mangoldt_real (Γ x)"
      by (subst norm_fds_mangoldt_complex) (rule refl)
    also have "… ≤ card (Γ x) * ln (x + x / H x)"
    proof (rule sum_bounded_above)
      fix n assume "n ∈ Γ x"
      hence Hn: "0 < n" "n ≤ x + x / H x" unfolding Γ_def using h by auto
      hence "mangoldt_real n ≤ ln n" by (intro mangoldt_le)
      also have "… ≤ ln (x + x / H x)" using Hn by auto
      finally show "mangoldt_real n ≤ ln (x + x / H x)" .
    qed
    also have "… ≤ (2 * x / H x + 1) * ln (x + x / H x)"
    proof -
      have Γ_eq: "Γ x = {nat ⌈x - x / H x⌉..<nat (⌊x + x / H x⌋ + 1)}"
        unfolding Γ_def by (subst nat_le_real_iff) (subst nat_ceiling_le_eq [symmetric], auto)
      moreover have "nat (⌊x + x / H x⌋ + 1) = ⌊x + x / H x⌋ + 1" using h(1) h(2) by auto
      moreover have "nat ⌈x - x / H x⌉ = ⌈x - x / H x⌉" using h(1) by auto
      moreover have "⌊x + x / H x⌋ ≤ x + x / H x" by (rule floor_le)
      moreover have "⌈x - x / H x⌉ ≥ x - x / H x" by (rule ceil_ge)
      ultimately have "(nat (⌊x + x / H x⌋ + 1) :: real) - nat ⌈x - x / H x⌉ ≤ 2 * x / H x + 1" by linarith
      hence "card (Γ x) ≤ 2 * x / H x + 1" using h(2) by (subst Γ_eq) (auto simp add: of_nat_diff_real)
      thus ?thesis using h(3) by (rule mult_right_mono)
    qed
    finally show ?thesis .
  qed
  hence "∀⇩F x in at_top.
    0 < x - x / H x ⟶ 0 < x / H x ⟶ 0 ≤ ln (x + x / H x)
    ⟶ ∥∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥∥ ≤ (2 * x / H x + 1) * ln (x + x / H x)"
    by (intro eventuallyI) blast
  moreover have "∀⇩F x in at_top. 0 < x - x / H x" unfolding H_def using Hc Hε by real_asymp
  moreover have "∀⇩F x in at_top. 0 < x / H x" unfolding H_def using Hc Hε  by real_asymp
  moreover have "∀⇩F x in at_top. 0 ≤ ln (x + x / H x)" unfolding H_def using Hc Hε by real_asymp
  ultimately have "∀⇩F x in at_top. ∥∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥∥ ≤ (2 * x / H x + 1) * ln (x + x / H x)"
    by eventually_elim blast
  hence "(λx. ∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥) ∈ O(λx. (2 * x / H x + 1) * ln (x + x / H x))"
    by (rule eventually_le_imp_bigo)
  moreover have "(λx. (2 * x / H x + 1) * ln (x + x / H x)) ∈ Rc'"
    unfolding Rc'_def H_def using Hc Hε
    by (real_asymp simp add: field_simps)
  ultimately have "(λx. ∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥) ∈ Rc'"
    unfolding Rc'_def by (rule landau_o.big_trans)
  hence "(λx. 3 * (2 + ln (T x / b x)) * (∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥))
      ∈ O(λx. 3 * (2 + ln (T x / b x)) * (x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2))))"
    unfolding Rc'_def by (intro landau_o.big.mult_left) auto
  moreover have "(λx. 3 * (2 + ln (T x / b x)) * (x * exp (- (c / 2 - ε) * (ln x) powr (1 / 2)))) ∈ Rc"
    unfolding Rc_def T_def b_def using Hc Hε by (real_asymp simp add: field_simps)
  ultimately have 2: "(λx. 3 * (2 + ln (T x / b x)) * (∑n∈Γ x. ∥fds_nth (fds mangoldt_complex) n∥)) ∈ Rc"
    unfolding Rc_def by (rule landau_o.big_trans)
  from 1 2 show ?thesis unfolding Rc_def R_def Γ_def by (rule sum_in_bigo)
qed

lemma perron_psi:
  "∀⇩F x in at_top. ∥ψ x + 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x)∥ ≤ R x"
proof -
  have Hb: "∀⇩F x in at_top. 1 < b x" unfolding b_def by real_asymp
  hence "∀⇩F x in at_top. 0 < b x" by eventually_elim auto
  moreover have "∀⇩F x in at_top. b x ≤ T x" unfolding b_def T_def using Hc by real_asymp
  moreover have "∀⇩F x in at_top. abs_conv_abscissa (fds mangoldt_complex) < ereal (b x)"
  proof -
    have "abs_conv_abscissa (fds mangoldt_complex) ≤ 1" by (rule abs_conv_abscissa_mangoldt)
    hence "∀⇩F x in at_top. 1 < b x ⟶ abs_conv_abscissa (fds mangoldt_complex) < ereal (b x)"
      by (auto intro: eventuallyI
               simp add: le_ereal_less one_ereal_def)
    thus ?thesis using Hb by (rule eventually_mp)
  qed
  moreover have "∀⇩F x in at_top. 2 ≤ H x" unfolding H_def using Hc by real_asymp
  moreover have "∀⇩F x in at_top. b x + 1 ≤ H x" unfolding b_def H_def using Hc by real_asymp
  moreover have "∀⇩F x :: real in at_top. 2 ≤ x" by auto
  moreover have "∀⇩F x in at_top.
    (∑`n≥1. ∥fds_nth (fds mangoldt_complex) n∥ / n nat_powr b x) ≤ B x"
    (is "eventually ?P ?F")
  proof -
    have "?P x" when Hb: "1 < b x ∧ b x ≤ 23 / 20" for x
    proof -
      have "(∑`n≥1. ∥fds_nth (fds mangoldt_complex) n∥ / n nat_powr (b x))
          = (∑`n≥1. mangoldt_real n / n nat_powr (b x))"
        by (subst norm_fds_mangoldt_complex) (rule refl)
      also have "… = - Re (logderiv zeta (b x))"
      proof -
        have "((λn. mangoldt_real n * n nat_powr (-b x) * cos (0 * ln (real n)))
            has_sum Re (- deriv zeta (Complex (b x) 0) / zeta (Complex (b x) 0))) {1..}"
          by (intro sums_Re_logderiv_zeta) (use Hb in auto)
        moreover have "Complex (b x) 0 = b x" by (rule complex_eqI) auto
        moreover have "Re (- deriv zeta (b x) / zeta (b x)) = - Re (logderiv zeta (b x))"
          unfolding logderiv_def by auto
        ultimately have "((λn. mangoldt_real n * n nat_powr (-b x)) has_sum
                         - Re (logderiv zeta (b x))) {1..}" by auto
        hence "- Re (logderiv zeta (b x)) = (∑`n≥1. mangoldt_real n * n nat_powr (-b x))"
          by (intro has_sum_imp_has_subsum subsumI)
        also have "… = (∑`n≥1. mangoldt_real n / n nat_powr (b x))"
          by (intro subsum_cong) (auto simp add: powr_minus_divide)
        finally show ?thesis by auto
      qed
      also have "… ≤ ¦Re (logderiv zeta (b x))¦" by auto
      also have "… ≤ ∥logderiv zeta (b x)∥" by (rule abs_Re_le_cmod)
      also have "… ≤ 5 / 4 * (1 / (b x - 1))"
        by (rule logderiv_zeta_bound) (use Hb in auto)
      also have "… = B x" unfolding b_def B_def by auto
      finally show ?thesis .
    qed
    hence "∀⇩F x in at_top. 1 < b x ∧ b x ≤ 23 / 20 ⟶ ?P x" by auto
    moreover have "∀⇩F x in at_top. b x ≤ 23 / 20" unfolding b_def by real_asymp
    ultimately show ?thesis using Hb by eventually_elim auto
  qed
  ultimately have "∀⇩F x in at_top.
    ∥sum_upto (fds_nth (fds mangoldt_complex)) x - 1 / (2 * pi * 𝗂)
      * contour_integral (P⇩2 x) (λs. eval_fds (fds mangoldt_complex) s * x powr s / s)∥ ≤ R x"
    unfolding R_def P⇩2_def z⇩2_def z⇩3_def
    by eventually_elim (rule perron_formula(2))
  moreover have "∀⇩F x in at_top. sum_upto (fds_nth (fds mangoldt_complex)) x = ψ x" for x :: real
    unfolding primes_psi_def sum_upto_def by auto
  moreover have
     "contour_integral (P⇩2 x) (λs. eval_fds (fds mangoldt_complex) s * x powr s / s)
    = contour_integral (P⇩2 x) (λs. - (x powr s / s * logderiv zeta s))"
    when "1 < b x" for x
  proof (rule contour_integral_eq, goal_cases)
    case (1 s)
    hence "Re s = b x" by (rule Re_path_P⇩2)
    hence "eval_fds (fds mangoldt_complex) s = - deriv zeta s / zeta s"
      by (intro eval_fds_mangoldt) (use that in auto)
    thus ?case unfolding logderiv_def by (auto simp add: field_simps)
  qed
  hence "∀⇩F x in at_top. 1 < b x ⟶
      contour_integral (P⇩2 x) (λs. eval_fds (fds mangoldt_complex) s * x powr s / s)
    = contour_integral (P⇩2 x) (λs. - (x powr s / s * logderiv zeta s))"
    using Hb by (intro eventuallyI) blast
  ultimately have "∀⇩F x in at_top.
    ∥ψ x - 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (λs. - (x powr s / s * logderiv zeta s))∥ ≤ R x"
    using Hb by eventually_elim auto
  thus ?thesis unfolding f_def
    by eventually_elim (auto simp add: contour_integral_neg)
qed

lemma estimation_perron_psi:
  "(λx. ∥ψ x + 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x)∥) ∈ Rc"
proof -
  have "(λx. ∥ψ x + 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x)∥) ∈ O(R)"
    by (intro eventually_le_imp_bigo' perron_psi)
  moreover have "R ∈ Rc" by (rule estimation_R)
  ultimately show ?thesis unfolding Rc_def by (rule landau_o.big_trans)
qed

theorem prime_number_theorem:
  "PNT_3 (c / 2 - 2 * ε) (1 / 2) 0"
proof -
  define r where "r x ≡
      ∥ψ x + 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x)∥
    + ∥1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x) + x∥" for x
  have "∥ψ x - x∥ ≤ r x" for x
  proof -
    have "∥ψ x - x∥ = ∥(ψ x :: complex) - x∥"
      by (fold dist_complex_def, simp add: dist_real_def)
    also have "… ≤ ∥ψ x - - 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x)∥
      + ∥x - - 1 / (2 * pi * 𝗂) * contour_integral (P⇩2 x) (f x)∥"
      by (fold dist_complex_def, rule dist_triangle2)
    finally show ?thesis unfolding r_def by (simp add: add_ac)
  qed
  hence "(λx. ψ x - x) ∈ O(r)" by (rule le_imp_bigo)
  moreover have "r ∈ Rc"
    unfolding r_def Rc_def
    by (intro sum_in_bigo, fold Rc_def)
       (rule estimation_perron_psi, rule estimation_P⇩2)
  ultimately show ?thesis unfolding PNT_3_def
    by (subst Rc_eq_rem_est [symmetric], unfold Rc_def)
       (rule landau_o.big_trans)
qed

no_notation primes_psi ("ψ")
end

unbundle prime_counting_notation

theorem prime_number_theorem:
  shows "(λx. π x - Li x) ∈ O(λx. x * exp (- 1 / 3653 * (ln x) powr (1 / 2)))"
proof -
  define c :: real where "c ≡ 1 / 1826"
  define ε :: real where "ε ≡ 1 / 26681512"
  interpret z: prime_number_theorem c ε
    unfolding c_def ε_def by standard (auto simp: C⇩4_def)
  have "PNT_3 (c / 2 - 2 * ε) (1 / 2) 0" by (rule z.prime_number_theorem)
  hence "PNT_1 (c / 2 - 2 * ε) (1 / 2) 0" by (auto intro: PNT_3_imp_PNT_1)
  thus "(λx. π x - Li x) ∈ O(λx. x * exp (- 1 / 3653 * (ln x) powr (1 / 2)))"
    unfolding PNT_1_def rem_est_def c_def ε_def
    by (rule landau_o.big.ev_eq_trans1, use ln_ln_asymp_pos in eventually_elim)
       (auto intro: eventually_at_top_linorderI [of 1] simp: powr_half_sqrt)
qed

hide_const (open) C⇩3 C⇩4 C⇩5
unbundle no_prime_counting_notation
unbundle no_pnt_notation
end