Theory Prime_Counting_Functions

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

  Definitions and basic properties of prime-counting functions like pi, theta, and psi
*)
section ‹Prime-Counting Functions›
theory Prime_Counting_Functions
  imports Prime_Number_Theorem_Library
begin

text ‹
  We will now define the basic prime-counting functions π›, θ›, and ψ›. Additionally, we 
  shall define a function M that is related to Mertens' theorems and Newman's proof of the
  Prime Number Theorem. Most of the results in this file are not actually required to prove 
  the Prime Number Theorem, but are still nice to have.
›

subsection ‹Definitions›

definition prime_sum_upto :: "(nat  'a)  real  'a :: semiring_1" where
  "prime_sum_upto f x = (p | prime p  real p  x. f p)"

lemma prime_sum_upto_altdef1:
  "prime_sum_upto f x = sum_upto (λp. ind prime p * f p) x"
  unfolding sum_upto_def prime_sum_upto_def
  by (intro sum.mono_neutral_cong_left finite_subset[OF _ finite_Nats_le_real[of x]])
     (auto dest: prime_gt_1_nat simp: ind_def)

lemma prime_sum_upto_altdef2:
  "prime_sum_upto f x = (p | prime p  p  nat x. f p)"
  unfolding sum_upto_altdef prime_sum_upto_altdef1
  by (intro sum.mono_neutral_cong_right) (auto simp: ind_def dest: prime_gt_1_nat)

lemma prime_sum_upto_altdef3:
  "prime_sum_upto f x = (pprimes_upto (nat x). f p)"
proof -
  have "(pprimes_upto (nat x). f p) = (p | prime p  p  nat x. f p)"
    by (subst sum_list_distinct_conv_sum_set) (auto simp: set_primes_upto conj_commute)
  thus ?thesis by (simp add: prime_sum_upto_altdef2)
qed

lemma prime_sum_upto_eqI:
  assumes "a  b" "k. k  {nat a<..natb}  ¬prime k"
  shows   "prime_sum_upto f a = prime_sum_upto f b"
proof -
  have *: "k  nat a" if "k  nat b" "prime k" for k
    using that assms(2)[of k] by (cases "k  nat a") auto
  from assms(1) have "nat a  nat b" by linarith
  hence "(p | prime p  p  nat a. f p) = (p | prime p  p  nat b. f p)"
    using assms by (intro sum.mono_neutral_left) (auto dest: *)
  thus ?thesis by (simp add: prime_sum_upto_altdef2)
qed

lemma prime_sum_upto_eqI':
  assumes "a'  nat a" "a  b" "nat b  b'" "k. k  {a'<..b'}  ¬prime k"
  shows   "prime_sum_upto f a = prime_sum_upto f b"
  by (rule prime_sum_upto_eqI) (use assms in auto)

lemmas eval_prime_sum_upto = prime_sum_upto_altdef3[unfolded primes_upto_sieve]

lemma of_nat_prime_sum_upto: "of_nat (prime_sum_upto f x) = prime_sum_upto (λp. of_nat (f p)) x"
  by (simp add: prime_sum_upto_def)

lemma prime_sum_upto_mono:
  assumes "n. n > 0  f n  (0::real)" "x  y"
  shows   "prime_sum_upto f x  prime_sum_upto f y"
  using assms unfolding prime_sum_upto_altdef1 sum_upto_altdef
  by (intro sum_mono2) (auto simp: le_nat_iff' le_floor_iff ind_def)

lemma prime_sum_upto_nonneg:
  assumes "n. n > 0  f n  (0 :: real)"
  shows   "prime_sum_upto f x  0"
  unfolding prime_sum_upto_altdef1 sum_upto_altdef
  by (intro sum_nonneg) (auto simp: ind_def assms)

lemma prime_sum_upto_eq_0:
  assumes "x < 2"
  shows   "prime_sum_upto f x = 0"
proof -
  from assms have "nat x = 0  nat x = 1" by linarith
  thus ?thesis by (auto simp: eval_prime_sum_upto)
qed

lemma measurable_prime_sum_upto [measurable]:
  fixes f :: "'a  nat  real"
  assumes [measurable]: "y. (λt. f t y)  M M borel"
  assumes [measurable]: "x  M M borel"
  shows "(λt. prime_sum_upto (f t) (x t))  M M borel"
  unfolding prime_sum_upto_altdef1 by measurable

text ‹
  The following theorem breaks down a sum over all prime powers no greater than
  fixed bound into a nicer form.
›
lemma sum_upto_primepows:
  fixes f :: "nat  'a :: comm_monoid_add"
  assumes "n. ¬primepow n  f n = 0" "p i. prime p  i > 0  f (p ^ i) = g p i"
  shows   "sum_upto f x = ((p, i) | prime p  i > 0  real (p ^ i)  x. g p i)"
proof -
  let ?d = aprimedivisor
  have g: "g (?d n) (multiplicity (?d n) n) = f n" if "primepow n" for n using that 
      by (subst assms(2) [symmetric])
         (auto simp: primepow_decompose aprimedivisor_prime_power primepow_gt_Suc_0
               intro!: aprimedivisor_nat multiplicity_aprimedivisor_gt_0_nat)
  have "sum_upto f x = (n | primepow n  real n  x. f n)"
    unfolding sum_upto_def using assms
    by (intro sum.mono_neutral_cong_right) (auto simp: primepow_gt_0_nat)
  also have " = ((p, i) | prime p  i > 0  real (p ^ i)  x. g p i)" (is "_ = sum _ ?S")
    by (rule sum.reindex_bij_witness[of _ "λ(p,i). p ^ i" "λn. (?d n, multiplicity (?d n) n)"])
       (auto simp: aprimedivisor_prime_power primepow_decompose primepow_gt_Suc_0 g
             simp del: of_nat_power intro!: aprimedivisor_nat multiplicity_aprimedivisor_gt_0_nat)
  finally show ?thesis .
qed


definition primes_pi    where "primes_pi = prime_sum_upto (λp. 1 :: real)"
definition primes_theta where "primes_theta = prime_sum_upto (λp. ln (real p))"
definition primes_psi   where "primes_psi = sum_upto (mangoldt :: nat  real)"
definition primes_M     where "primes_M = prime_sum_upto (λp. ln (real p) / real p)"

text ‹
  Next, we define some nice optional notation for these functions.
›

bundle prime_counting_notation
begin

notation primes_pi    ("π")
notation primes_theta ("θ")
notation primes_psi   ("ψ")
notation primes_M     ("𝔐")

end

bundle no_prime_counting_notation
begin

no_notation primes_pi    ("π")
no_notation primes_theta ("θ")
no_notation primes_psi   ("ψ")
no_notation primes_M     ("𝔐")

end

(*<*)
unbundle prime_counting_notation
(*>*)

lemmas π_def = primes_pi_def
lemmas θ_def = primes_theta_def
lemmas ψ_def = primes_psi_def

lemmas eval_π = primes_pi_def[unfolded eval_prime_sum_upto]
lemmas eval_θ = primes_theta_def[unfolded eval_prime_sum_upto]
lemmas eval_𝔐 = primes_M_def[unfolded eval_prime_sum_upto]


subsection ‹Basic properties›

text ‹
  The proofs in this section are mostly taken from Apostol~cite"apostol1976analytic".
›

lemma measurable_π [measurable]: "π  borel M borel"
  and measurable_θ [measurable]: "θ  borel M borel"
  and measurable_ψ [measurable]: "ψ  borel M borel"
  and measurable_primes_M [measurable]: "𝔐  borel M borel"
  unfolding primes_M_def π_def θ_def ψ_def by measurable

lemma π_eq_0 [simp]: "x < 2  π x = 0"
  and θ_eq_0 [simp]: "x < 2  θ x = 0"
  and primes_M_eq_0 [simp]: "x < 2  𝔐 x = 0"
  unfolding primes_pi_def primes_theta_def primes_M_def
  by (rule prime_sum_upto_eq_0; simp)+

lemma π_nat_cancel [simp]: "π (nat x) = π x"
  and θ_nat_cancel [simp]: "θ (nat x) = θ x"
  and primes_M_nat_cancel [simp]: "𝔐 (nat x) = 𝔐 x"
  and ψ_nat_cancel [simp]: "ψ (nat x) = ψ x"
  and π_floor_cancel [simp]: "π (of_int y) = π y"
  and θ_floor_cancel [simp]: "θ (of_int y) = θ y"
  and primes_M_floor_cancel [simp]: "𝔐 (of_int y) = 𝔐 y"
  and ψ_floor_cancel [simp]: "ψ (of_int y) = ψ y"
  by (simp_all add: π_def θ_def ψ_def primes_M_def prime_sum_upto_altdef2 sum_upto_altdef)

lemma π_nonneg [intro]: "π x  0"
  and θ_nonneg [intro]: "θ x  0"
  and primes_M_nonneg [intro]: "𝔐 x  0"
  unfolding primes_pi_def primes_theta_def primes_M_def
  by (rule prime_sum_upto_nonneg; simp)+

lemma π_mono [intro]: "x  y  π x  π y"
  and θ_mono [intro]: "x  y  θ x  θ y"
  and primes_M_mono [intro]: "x  y  𝔐 x  𝔐 y"
  unfolding primes_pi_def primes_theta_def primes_M_def
  by (rule prime_sum_upto_mono; simp)+

lemma π_pos_iff: "π x > 0  x  2"
proof
  assume x: "x  2"
  show "π x > 0"
    by (rule less_le_trans[OF _ π_mono[OF x]]) (auto simp: eval_π)
next
  assume "π x > 0"
  hence "¬(x < 2)" by auto
  thus "x  2" by simp
qed

lemma π_pos: "x  2  π x > 0"
  by (simp add: π_pos_iff)

lemma ψ_eq_0 [simp]:
  assumes "x < 2"
  shows   "ψ x = 0"
proof -
  from assms have "nat x  1" by linarith
  hence "mangoldt n = (0 :: real)" if "n  {0<..nat x}" for n
    using that by (auto simp: mangoldt_def dest!: primepow_gt_Suc_0)
  thus ?thesis unfolding ψ_def sum_upto_altdef by (intro sum.neutral) auto
qed

lemma ψ_nonneg [intro]: "ψ x  0"
  unfolding ψ_def sum_upto_def by (intro sum_nonneg mangoldt_nonneg)

lemma ψ_mono: "x  y  ψ x  ψ y"
  unfolding ψ_def sum_upto_def by (intro sum_mono2 mangoldt_nonneg) auto


subsection ‹The $n$-th prime number›

text ‹
  Next we define the $n$-th prime number, where counting starts from 0. In traditional
  mathematics, it seems that counting usually starts from 1, but it is more natural to
  start from 0 in HOL and the asymptotics of the function are the same.
›
definition nth_prime :: "nat  nat" where
  "nth_prime n = (THE p. prime p  card {q. prime q  q < p} = n)"

lemma finite_primes_less [intro]: "finite {q::nat. prime q  q < p}"
  by (rule finite_subset[of _ "{..<p}"]) auto

lemma nth_prime_unique_aux:
  fixes p p' :: nat
  assumes "prime p"  "card {q. prime q  q < p} = n"
  assumes "prime p'" "card {q. prime q  q < p'} = n"
  shows   "p = p'"
  using assms
proof (induction p p' rule: linorder_wlog)
  case (le p p')
  have "finite {q. prime q  q < p'}" by (rule finite_primes_less)
  moreover from le have "{q. prime q  q < p}  {q. prime q  q < p'}"
    by auto
  moreover from le have "card {q. prime q  q < p} = card {q. prime q  q < p'}"
    by simp
  ultimately have "{q. prime q  q < p} = {q. prime q  q < p'}"
    by (rule card_subset_eq)
  with prime p have "¬(p < p')" by blast
  with p  p' show "p = p'" by auto
qed auto

lemma π_smallest_prime_beyond:
  "π (real (smallest_prime_beyond m)) = π (real (m - 1)) + 1"
proof (cases m)
  case 0
  have "smallest_prime_beyond 0 = 2"
    by (rule smallest_prime_beyond_eq) (auto dest: prime_gt_1_nat)
  with 0 show ?thesis by (simp add: eval_π)
next
  case (Suc n) 
  define n' where "n' = smallest_prime_beyond (Suc n)"
  have "n < n'"
    using smallest_prime_beyond_le[of "Suc n"] unfolding n'_def by linarith
  have "prime n'" by (simp add: n'_def)
  have "n'  p" if "prime p" "p > n" for p
    using that smallest_prime_beyond_smallest[of p "Suc n"] by (auto simp: n'_def)
  note n' = n < n' prime n' this

  have "π (real n') = real (card {p. prime p  p  n'})"
    by (simp add: π_def prime_sum_upto_def)
  also have "Suc n  n'" unfolding n'_def by (rule smallest_prime_beyond_le)
  hence "{p. prime p  p  n'} = {p. prime p  p  n}  {p. prime p  p  {n<..n'}}"
    by auto
  also have "real (card ) = π (real n) + real (card {p. prime p  p  {n<..n'}})"
    by (subst card_Un_disjoint) (auto simp: π_def prime_sum_upto_def)
  also have "{p. prime p  p  {n<..n'}} = {n'}"
    using n' by (auto intro: antisym)
  finally show ?thesis using Suc by (simp add: n'_def)
qed

lemma π_inverse_exists: "n. π (real n) = real m"
proof (induction m)
  case 0
  show ?case by (intro exI[of _ 0]) auto
next
  case (Suc m)
  from Suc.IH obtain n where n: "π (real n) = real m"
    by auto
  hence "π (real (smallest_prime_beyond (Suc n))) = real (Suc m)"
    by (subst π_smallest_prime_beyond) auto
  thus ?case by blast
qed

lemma nth_prime_exists: "p::nat. prime p  card {q. prime q  q < p} = n"
proof -
  from π_inverse_exists[of n] obtain m where "π (real m) = real n" by blast
  hence card: "card {q. prime q  q  m} = n"
    by (auto simp: π_def prime_sum_upto_def)

  define p where "p = smallest_prime_beyond (Suc m)"
  have "m < p" using smallest_prime_beyond_le[of "Suc m"] unfolding p_def by linarith
  have "prime p" by (simp add: p_def)
  have "p  q" if "prime q" "q > m" for q
    using smallest_prime_beyond_smallest[of q "Suc m"] that by (simp add: p_def)
  note p = m < p prime p this

  have "{q. prime q  q < p} = {q. prime q  q  m}"
  proof safe
    fix q assume "prime q" "q < p"
    hence "¬(q > m)" using p(1,2) p(3)[of q] by auto
    thus "q  m" by simp
  qed (insert p, auto)
  also have "card  = n" by fact
  finally show ?thesis using prime p by blast
qed

lemma nth_prime_exists1: "∃!p::nat. prime p  card {q. prime q  q < p} = n"
  by (intro ex_ex1I nth_prime_exists) (blast intro: nth_prime_unique_aux)

lemma prime_nth_prime [intro]:    "prime (nth_prime n)"
  and card_less_nth_prime [simp]: "card {q. prime q  q < nth_prime n} = n"
  using theI'[OF nth_prime_exists1[of n]] by (simp_all add: nth_prime_def)

lemma card_le_nth_prime [simp]: "card {q. prime q  q  nth_prime n} = Suc n"
proof -
  have "{q. prime q  q  nth_prime n} = insert (nth_prime n) {q. prime q  q < nth_prime n}"
    by auto
  also have "card  = Suc n" by simp
  finally show ?thesis .
qed

lemma π_nth_prime [simp]: "π (real (nth_prime n)) = real n + 1"
  by (simp add: π_def prime_sum_upto_def)

lemma nth_prime_eqI:
  assumes "prime p" "card {q. prime q  q < p} = n"
  shows   "nth_prime n = p"
  unfolding nth_prime_def
  by (rule the1_equality[OF nth_prime_exists1]) (use assms in auto)

lemma nth_prime_eqI':
  assumes "prime p" "card {q. prime q  q  p} = Suc n"
  shows   "nth_prime n = p"
proof (rule nth_prime_eqI)
  have "{q. prime q  q  p} = insert p {q. prime q  q < p}"
    using assms by auto
  also have "card  = Suc (card {q. prime q  q < p})"
    by simp
  finally show "card {q. prime q  q < p} = n" using assms by simp
qed (use assms in auto)

lemma nth_prime_eqI'':
  assumes "prime p" "π (real p) = real n + 1"
  shows   "nth_prime n = p"
proof (rule nth_prime_eqI')
  have "real (card {q. prime q  q  p}) = π (real p)"
    by (simp add: π_def prime_sum_upto_def)
  also have " = real (Suc n)" by (simp add: assms)
  finally show "card {q. prime q  q  p} = Suc n"
    by (simp only: of_nat_eq_iff)
qed fact+

lemma nth_prime_0 [simp]: "nth_prime 0 = 2"
  by (intro nth_prime_eqI) (auto dest: prime_gt_1_nat)

lemma nth_prime_Suc: "nth_prime (Suc n) = smallest_prime_beyond (Suc (nth_prime n))"
  by (rule nth_prime_eqI'') (simp_all add: π_smallest_prime_beyond)

lemmas nth_prime_code [code] = nth_prime_0 nth_prime_Suc

lemma strict_mono_nth_prime: "strict_mono nth_prime"
proof (rule strict_monoI_Suc)
  fix n :: nat
  have "Suc (nth_prime n)  smallest_prime_beyond (Suc (nth_prime n))" by simp
  also have " = nth_prime (Suc n)" by (simp add: nth_prime_Suc)
  finally show "nth_prime n < nth_prime (Suc n)" by simp
qed

lemma nth_prime_le_iff [simp]: "nth_prime m  nth_prime n  m  n"
  using strict_mono_less_eq[OF strict_mono_nth_prime] by blast

lemma nth_prime_less_iff [simp]: "nth_prime m < nth_prime n  m < n"
  using strict_mono_less[OF strict_mono_nth_prime] by blast

lemma nth_prime_eq_iff [simp]: "nth_prime m = nth_prime n  m = n"
  using strict_mono_eq[OF strict_mono_nth_prime] by blast

lemma nth_prime_ge_2: "nth_prime n  2"
  using nth_prime_le_iff[of 0 n] by (simp del: nth_prime_le_iff)

lemma nth_prime_lower_bound: "nth_prime n  Suc (Suc n)"
proof -
  have "n = card {q. prime q  q < nth_prime n}"
    by simp
  also have "  card {2..<nth_prime n}"
    by (intro card_mono) (auto dest: prime_gt_1_nat)
  also have " = nth_prime n - 2" by simp
  finally show ?thesis using nth_prime_ge_2[of n] by linarith
qed

lemma nth_prime_at_top: "filterlim nth_prime at_top at_top"
proof (rule filterlim_at_top_mono)
  show "filterlim (λn::nat. n + 2) at_top at_top" by real_asymp
qed (auto simp: nth_prime_lower_bound)

lemma π_at_top: "filterlim π at_top at_top"
  unfolding filterlim_at_top
proof safe
  fix C :: real
  define x0 where "x0 = real (nth_prime (nat max 0 C))"
  show "eventually (λx. π x  C) at_top"
    using eventually_ge_at_top
  proof eventually_elim
    fix x assume "x  x0"
    have "C  real (nat max 0 C + 1)" by linarith
    also have "real (nat max 0 C + 1) = π x0"
      unfolding x0_def by simp
    also have "  π x" by (rule π_mono) fact
    finally show "π x  C" .
  qed
qed

text‹
  An unbounded, strictly increasing sequence $a_n$ partitions $[a_0; \infty)$ into
  segments of the form $[a_n; a_{n+1})$.
›
lemma strict_mono_sequence_partition:
  assumes "strict_mono (f :: nat  'a :: {linorder, no_top})"
  assumes "x  f 0"
  assumes "filterlim f at_top at_top"
  shows   "k. x  {f k..<f (Suc k)}"
proof -
  define k where "k = (LEAST k. f (Suc k) > x)"
  {
    obtain n where "x  f n"
      using assms by (auto simp: filterlim_at_top eventually_at_top_linorder)
    also have "f n < f (Suc n)"
      using assms by (auto simp: strict_mono_Suc_iff)
    finally have "n. f (Suc n) > x" by auto
  }
  from LeastI_ex[OF this] have "x < f (Suc k)"
    by (simp add: k_def)
  moreover have "f k  x"
  proof (cases k)
    case (Suc k')
    have "k  k'" if "f (Suc k') > x"
      using that unfolding k_def by (rule Least_le)
    with Suc show "f k  x" by (cases "f k  x") (auto simp: not_le)
  qed (use assms in auto)
  ultimately show ?thesis by auto
qed

lemma nth_prime_partition:
  assumes "x  2"
  shows   "k. x  {nth_prime k..<nth_prime (Suc k)}"
  using strict_mono_sequence_partition[OF strict_mono_nth_prime, of x] assms nth_prime_at_top
  by simp

lemma nth_prime_partition':
  assumes "x  2"
  shows   "k. x  {real (nth_prime k)..<real (nth_prime (Suc k))}"
  by (rule strict_mono_sequence_partition)
     (auto simp: strict_mono_Suc_iff assms
           intro!: filterlim_real_sequentially filterlim_compose[OF _ nth_prime_at_top])

lemma between_nth_primes_imp_nonprime:
  assumes "n > nth_prime k" "n < nth_prime (Suc k)"
  shows   "¬prime n"
  using assms by (metis Suc_leI not_le nth_prime_Suc smallest_prime_beyond_smallest)

lemma nth_prime_partition'':
  assumes "x  (2 :: real)"
  shows "x  {real (nth_prime (nat π x - 1))..<real (nth_prime (nat π x))}"
proof -
  obtain n where n: "x  {nth_prime n..<nth_prime (Suc n)}"
    using nth_prime_partition' assms by auto
  have "π (nth_prime n) = π x"
    unfolding π_def using between_nth_primes_imp_nonprime n
    by (intro prime_sum_upto_eqI) (auto simp: le_nat_iff le_floor_iff)
  hence "real n = π x - 1"
    by simp
  hence n_eq: "n = nat π x - 1" "Suc n = nat π x"
    by linarith+
  with n show ?thesis 
    by simp
qed


subsection ‹Relations between different prime-counting functions›

text ‹
  The ψ› function can be expressed as a sum of θ›.
›
lemma ψ_altdef:
  assumes "x > 0"
  shows   "ψ x = sum_upto (λm. prime_sum_upto ln (root m x)) (log 2 x)" (is "_ = ?rhs")
proof -
  have finite: "finite {p. prime p  real p  y}" for y
    by (rule finite_subset[of _ "{..nat y}"]) (auto simp: le_nat_iff' le_floor_iff)
  define S where "S = (SIGMA i:{i. 0 < i  real i  log 2 x}. {p. prime p  real p  root i x})"
  have "ψ x = ((p, i) | prime p  0 < i  real (p ^ i)  x. ln (real p))"  unfolding ψ_def
    by (subst sum_upto_primepows[where g = "λp i. ln (real p)"])
       (auto simp: case_prod_unfold mangoldt_non_primepow)
  also have " = ((i, p) | prime p  0 < i  real (p ^ i)  x. ln (real p))"
    by (intro sum.reindex_bij_witness[of _ "λ(x,y). (y,x)" "λ(x,y). (y,x)"]) auto
  also have "{(i, p). prime p  0 < i  real (p ^ i)  x} = S"
    unfolding S_def
  proof safe
    fix i p :: nat assume ip: "i > 0" "real i  log 2 x" "prime p" "real p  root i x"
    hence "real (p ^ i)  root i x ^ i" unfolding of_nat_power by (intro power_mono) auto
    with ip assms show "real (p ^ i)  x" by simp
  next
    fix i p assume ip: "prime p" "i > 0" "real (p ^ i)  x"
    from ip have "2 ^ i  p ^ i" by (intro power_mono) (auto dest: prime_gt_1_nat)
    also have "  x" using ip by simp
    finally show "real i  log 2 x"
      using assms by (simp add: le_log_iff powr_realpow)
    have "root i (real p ^ i)  root i x" using ip assms
      by (subst real_root_le_iff) auto
    also have "root i (real p ^ i) = real p"
      using assms ip by (subst real_root_pos2) auto
    finally show "real p  root i x" .
  qed
  also have "((i,p)S. ln p) = sum_upto (λm. prime_sum_upto ln (root m x)) (log 2 x)"
    unfolding sum_upto_def prime_sum_upto_def S_def using finite by (subst sum.Sigma) auto
  finally show ?thesis .
qed

lemma ψ_conv_θ_sum: "x > 0  ψ x = sum_upto (λm. θ (root m x)) (log 2 x)"
  by (simp add: ψ_altdef θ_def)

lemma ψ_minus_θ:
  assumes x: "x  2"
  shows   "ψ x - θ x = (i | 2  i  real i  log 2 x. θ (root i x))"
proof -
  have finite: "finite {i. 2  i  real i  log 2 x}"
    by (rule finite_subset[of _ "{2..nat log 2 x}"]) (auto simp: le_nat_iff' le_floor_iff)
  have "ψ x = (i | 0 < i  real i  log 2 x. θ (root i x))" using x
    by (simp add: ψ_conv_θ_sum sum_upto_def)
  also have "{i. 0 < i  real i  log 2 x} = insert 1 {i. 2  i  real i  log 2 x}" using x
    by (auto simp: le_log_iff)
  also have "(i. θ (root i x)) - θ x =
               (i | 2  i  real i  log 2 x. θ (root i x))" using finite
    by (subst sum.insert) auto
  finally show ?thesis .
qed

text ‹
  The following theorems use summation by parts to relate different prime-counting functions to
  one another with an integral as a remainder term.
›
lemma θ_conv_π_integral:
  assumes "x  2"
  shows   "((λt. π t / t) has_integral (π x * ln x - θ x)) {2..x}"
proof (cases "x = 2")
  case False
  note [intro] = finite_vimage_real_of_nat_greaterThanAtMost
  from False and assms have x: "x > 2" by simp
  have "((λt. sum_upto (ind prime) t * (1 / t)) has_integral
          sum_upto (ind prime) x * ln x - sum_upto (ind prime) 2 * ln 2 -
          (nreal -` {2<..x}. ind prime n * ln (real n))) {2..x}" using x
    by (intro partial_summation_strong[where X = "{}"])
       (auto intro!: continuous_intros derivative_eq_intros
             simp flip: has_real_derivative_iff_has_vector_derivative)
  hence "((λt. π t / t) has_integral (π x * ln x -
           (π 2 * ln 2 + (nreal -` {2<..x}. ind prime n * ln n)))) {2..x}"
    by (simp add: π_def prime_sum_upto_altdef1 algebra_simps)
  also have "π 2 * ln 2 + (nreal -` {2<..x}. ind prime n * ln n) =
               (ninsert 2 (real -` {2<..x}). ind prime n * ln n)"
    by (subst sum.insert) (auto simp: eval_π)
  also have " = θ x" unfolding θ_def prime_sum_upto_def using x
    by (intro sum.mono_neutral_cong_right) (auto simp: ind_def dest: prime_gt_1_nat)
  finally show ?thesis .
qed (auto simp: has_integral_refl eval_π eval_θ)

lemma π_conv_θ_integral:
  assumes "x  2"
  shows   "((λt. θ t / (t * ln t ^ 2)) has_integral (π x - θ x / ln x)) {2..x}"
proof (cases "x = 2")
  case False
  define b where "b = (λp. ind prime p * ln (real p))"
  note [intro] = finite_vimage_real_of_nat_greaterThanAtMost
  from False and assms have x: "x > 2" by simp
  have "((λt. -(sum_upto b t * (-1 / (t * (ln t)2)))) has_integral
          -(sum_upto b x * (1 / ln x) - sum_upto b 2 * (1 / ln 2) -
              (nreal -` {2<..x}. b n * (1 / ln (real n))))) {2..x}" using x
    by (intro has_integral_neg partial_summation_strong[where X = "{}"])
       (auto intro!: continuous_intros derivative_eq_intros
             simp flip: has_real_derivative_iff_has_vector_derivative simp add: power2_eq_square)
  also have "sum_upto b = θ"
    by (simp add: θ_def b_def prime_sum_upto_altdef1 fun_eq_iff)
  also have "θ x * (1 / ln x) - θ 2 * (1 / ln 2) - 
                   (nreal -` {2<..x}. b n * (1 / ln (real n))) =
               θ x * (1 / ln x) - (ninsert 2 (real -` {2<..x}). b n * (1 / ln (real n)))"
    by (subst sum.insert) (auto simp: b_def eval_θ)
  also have "(ninsert 2 (real -` {2<..x}). b n * (1 / ln (real n))) = π x" using x
    unfolding π_def prime_sum_upto_altdef1 sum_upto_def
  proof (intro sum.mono_neutral_cong_left ballI, goal_cases)
    case (3 p)
    hence "p = 1" by auto
    thus ?case by auto
  qed (auto simp: b_def)
  finally show ?thesis by simp
qed (auto simp: has_integral_refl eval_π eval_θ)

lemma integrable_weighted_θ:
  assumes "2  a" "a  x"
  shows   "((λt. θ t / (t * ln t ^ 2)) integrable_on {a..x})"
proof (cases "a < x")
  case True
  hence "((λt. θ t * (1 / (t * ln t ^ 2))) integrable_on {a..x})" using assms
    unfolding θ_def prime_sum_upto_altdef1
    by (intro partial_summation_integrable_strong[where X = "{}" and f = "λx. -1 / ln x"])
       (auto simp flip: has_real_derivative_iff_has_vector_derivative
             intro!: derivative_eq_intros continuous_intros simp: power2_eq_square field_simps)
  thus ?thesis by simp
qed (insert has_integral_refl[of _ a] assms, auto simp: has_integral_iff)

lemma θ_conv_𝔐_integral:
  assumes "x  2"
  shows  "(𝔐 has_integral (𝔐 x * x - θ x)) {2..x}"
proof (cases "x = 2")
  case False
  with assms have x: "x > 2" by simp
  define b :: "nat  real" where "b = (λp. ind prime p * ln p / p)"
  note [intro] = finite_vimage_real_of_nat_greaterThanAtMost
  have prime_le_2: "p = 2" if "p  2" "prime p" for p :: nat
    using that by (auto simp: prime_nat_iff)

  have "((λt. sum_upto b t * 1) has_integral sum_upto b x * x - sum_upto b 2 * 2 -
          (nreal -` {2<..x}. b n * real n)) {2..x}" using x
    by (intro partial_summation_strong[of "{}"])
       (auto simp flip: has_real_derivative_iff_has_vector_derivative
             intro!: derivative_eq_intros continuous_intros)
  also have "sum_upto b = 𝔐"
    by (simp add: fun_eq_iff primes_M_def b_def prime_sum_upto_altdef1)
  also have "𝔐 x * x - 𝔐 2 * 2 - (nreal -` {2<..x}. b n * real n) =
               𝔐 x * x - (ninsert 2 (real -` {2<..x}). b n * real n)"
    by (subst sum.insert) (auto simp: eval_𝔐 b_def)
  also have "(ninsert 2 (real -` {2<..x}). b n * real n) = θ x"
    unfolding θ_def prime_sum_upto_def using x
    by (intro sum.mono_neutral_cong_right) (auto simp: b_def ind_def not_less prime_le_2)
  finally show ?thesis by simp
qed (auto simp: eval_θ eval_𝔐)

lemma 𝔐_conv_θ_integral:
  assumes "x  2"
  shows  "((λt. θ t / t2) has_integral (𝔐 x - θ x / x)) {2..x}"
proof (cases "x = 2")
  case False
  with assms have x: "x > 2" by simp
  define b :: "nat  real" where "b = (λp. ind prime p * ln p)"
  note [intro] = finite_vimage_real_of_nat_greaterThanAtMost
  have prime_le_2: "p = 2" if "p  2" "prime p" for p :: nat
    using that by (auto simp: prime_nat_iff)

  have "((λt. sum_upto b t * (1 / t^2)) has_integral
          sum_upto b x * (-1 / x) - sum_upto b 2 * (-1 / 2) -
          (nreal -` {2<..x}. b n * (-1 / real n))) {2..x}" using x
    by (intro partial_summation_strong[of "{}"])
       (auto simp flip: has_real_derivative_iff_has_vector_derivative simp: power2_eq_square
             intro!: derivative_eq_intros continuous_intros)
  also have "sum_upto b = θ"
    by (simp add: fun_eq_iff θ_def b_def prime_sum_upto_altdef1)
  also have "θ x * (-1 / x) - θ 2 * (-1 / 2) - (nreal -` {2<..x}. b n * (-1 / real n)) =
               -(θ x / x - (ninsert 2 (real -` {2<..x}). b n / real n))"
    by (subst sum.insert) (auto simp: eval_θ b_def sum_negf)
  also have "(ninsert 2 (real -` {2<..x}). b n / real n) = 𝔐 x"
    unfolding primes_M_def prime_sum_upto_def using x
    by (intro sum.mono_neutral_cong_right) (auto simp: b_def ind_def not_less prime_le_2)
  finally show ?thesis by simp
qed (auto simp: eval_θ eval_𝔐)

lemma integrable_primes_M: "𝔐 integrable_on {x..y}" if "2  x" for x y :: real
proof -
  have "(λx. 𝔐 x * 1) integrable_on {x..y}" if "2  x" "x < y" for x y :: real
    unfolding primes_M_def prime_sum_upto_altdef1 using that
    by (intro partial_summation_integrable_strong[where X = "{}" and f = "λx. x"])
       (auto simp flip: has_real_derivative_iff_has_vector_derivative
             intro!: derivative_eq_intros continuous_intros)
  thus ?thesis using that has_integral_refl(2)[of 𝔐 x] by (cases x y rule: linorder_cases) auto
qed


subsection ‹Bounds›

lemma θ_upper_bound_coarse:
  assumes "x  1"
  shows   "θ x  x * ln x"
proof -
  have "θ x  sum_upto (λ_. ln x) x" unfolding θ_def prime_sum_upto_altdef1 sum_upto_def
    by (intro sum_mono) (auto simp: ind_def)
  also have "  real_of_int x * ln x" using assms
    by (simp add: sum_upto_altdef)
  also have "  x * ln x" using assms by (intro mult_right_mono) auto
  finally show ?thesis .
qed

lemma θ_le_ψ: "θ x  ψ x"
proof (cases "x  2")
  case False
  hence "nat x = 0  nat x = 1" by linarith
  thus ?thesis by (auto simp: eval_θ)
next
  case True
  hence "ψ x - θ x = (i | 2  i  real i  log 2 x. θ (root i x))"
    by (rule ψ_minus_θ)
  also have "  0" by (intro sum_nonneg) auto
  finally show ?thesis by simp
qed

lemma π_upper_bound_coarse:
  assumes "x  0"
  shows   "π x  x / 3 + 2"
proof -
  have "{p. prime p  p  nat x}  {2, 3}  {p. p  1  odd p  ¬3 dvd p  p  nat x}"
    using primes_dvd_imp_eq[of "2 :: nat"] primes_dvd_imp_eq[of "3 :: nat"] by auto
  also have "  {2, 3}  ((λk. 6*k+1) ` {0<..<nat (x+5)/6}  (λk. 6*k+5) ` {..<nat (x+1)/6})"
    (is "_  ?lhs  _  ?rhs")
  proof (intro Un_mono subsetI)
    fix p :: nat assume "p  ?lhs"
    hence p: "p  1" "odd p" "¬3 dvd p" "p  nat x" by auto
    from p (1-3) have "(k. k > 0  p = 6 * k + 1  p = 6 * k + 5)" by presburger
    then obtain k where "k > 0  p = 6 * k + 1  p = 6 * k + 5" by blast
    hence "p = 6 * k + 1  k > 0  k < nat (x+5)/6  p = 6*k+5  k < nat (x+1)/6"
      unfolding add_divide_distrib using p(4) by linarith
    thus "p  ?rhs" by auto
  qed
  finally have subset: "{p. prime p  p  nat x}  " (is "_  ?A") .

  have "π x = real (card {p. prime p  p  nat x})"
    by (simp add: π_def prime_sum_upto_altdef2)
  also have "card {p. prime p  p  nat x}  card ?A"
    by (intro card_mono subset) auto
  also have "  2 + (nat (x+5)/6 - 1 + nat (x+1)/6)"
    by (intro order.trans[OF card_Un_le] add_mono order.trans[OF card_image_le]) auto
  also have "  x / 3 + 2"
    using assms unfolding add_divide_distrib by (cases "x  1", linarith, simp)
  finally show ?thesis by simp
qed

lemma le_numeral_iff: "m  numeral n  m = numeral n  m  pred_numeral n"
  using numeral_eq_Suc by presburger

text ‹
  The following nice proof for the upper bound $\theta(x) \leq \ln 4 \cdot x$ is taken
  from Otto Forster's lecture notes on Analytic Number Theory~cite"forsteranalytic".
›
lemma prod_primes_upto_less:
  defines "F  (λn. ({p::nat. prime p  p  n}))"
  shows   "n > 0  F n < 4 ^ n"
proof (induction n rule: less_induct)
  case (less n)
  have "n = 0  n = 1  n = 2  n = 3  even n  n  4  odd n  n  4"
    by presburger
  then consider "n = 0" | "n = 1" | "n = 2" | "n = 3" | "even n" "n  4" | "odd n" "n  4"
    by metis
  thus ?case
  proof cases
    assume [simp]: "n = 1"
    have *: "{p. prime p  p  Suc 0} = {}" by (auto dest: prime_gt_1_nat)
    show ?thesis by (simp add: F_def *)
  next
    assume [simp]: "n = 2"
    have *: "{p. prime p  p  2} = {2 :: nat}"
      by (auto simp: le_numeral_iff dest: prime_gt_1_nat)
    thus ?thesis by (simp add: F_def *)
  next
    assume [simp]: "n = 3"
    have *: "{p. prime p  p  3} = {2, 3 :: nat}"
      by (auto simp: le_numeral_iff dest: prime_gt_1_nat)
    thus ?thesis by (simp add: F_def *)
  next
    assume n: "even n" "n  4"
    from n have "F (n - 1) < 4 ^ (n - 1)" by (intro less.IH) auto
    also have "prime p  p  n  prime p  p  n - 1" for p
      using n prime_odd_nat[of n] by (cases "p = n") auto
    hence "F (n - 1) = F n" by (simp add: F_def)
    also have "4 ^ (n - 1)  (4 ^ n :: nat)" by (intro power_increasing) auto
    finally show ?case .
  next
    assume n: "odd n" "n  4"
    then obtain k where k_eq: "n = Suc (2 * k)" by (auto elim: oddE)
    from n have k: "k  2" unfolding k_eq by presburger
    have prime_dvd: "p dvd (n choose k)" if p: "prime p" "p  {k+1<..n}" for p
    proof -
      from p k n have "p dvd pochhammer (k + 2) k"
        unfolding pochhammer_prod
        by (subst prime_dvd_prod_iff)
           (auto intro!: bexI[of _ "p - k - 2"] simp: k_eq numeral_2_eq_2 Suc_diff_Suc)
      also have "pochhammer (real (k + 2)) k = real ((n choose k) * fact k)"
        by (simp add: binomial_gbinomial gbinomial_pochhammer' k_eq field_simps)
      hence "pochhammer (k + 2) k = (n choose k) * fact k"
        unfolding pochhammer_of_nat of_nat_eq_iff .
      finally show "p dvd (n choose k)" using p
        by (auto simp: prime_dvd_fact_iff prime_dvd_mult_nat)
    qed

    have "{p. prime p  p  {k+1<..n}} dvd (n choose k)"
    proof (rule multiplicity_le_imp_dvd, goal_cases)
      case (2 p)
      thus ?case
      proof (cases "p  {k+1<..n}")
        case False
        hence "multiplicity p ({p. prime p  p  {k+1<..n}}) = 0" using 2
          by (subst prime_elem_multiplicity_prod_distrib) (auto simp: prime_multiplicity_other)
        thus ?thesis by auto
      next
        case True
        hence "multiplicity p ({p. prime p  p  {k+1<..n}}) =
                 sum (multiplicity p) {p. prime p  Suc k < p  p  n}" using 2
          by (subst prime_elem_multiplicity_prod_distrib) auto
        also have " = sum (multiplicity p) {p}" using True 2
        proof (intro sum.mono_neutral_right ballI)
          fix q :: nat assume "q  {p. prime p  Suc k < p  p  n} - {p}"
          thus "multiplicity p q = 0" using 2
            by (cases "p = q") (auto simp: prime_multiplicity_other)
        qed auto
        also have " = 1" using 2 by simp
        also have "1  multiplicity p (n choose k)"
          using prime_dvd[of p] 2 True by (intro multiplicity_geI) auto
        finally show ?thesis .
      qed
    qed auto
    hence "{p. prime p  p  {k+1<..n}}  (n choose k)"
      by (intro dvd_imp_le) (auto simp: k_eq)
    also have " = 1 / 2 * (i{k, Suc k}. n choose i)"
      using central_binomial_odd[of n] by (simp add: k_eq)
    also have "(i{k, Suc k}. n choose i) < (i{0, k, Suc k}. n choose i)"
      using k by simp
    also have "  (in. n choose i)"
      by (intro sum_mono2) (auto simp: k_eq)
    also have " = (1 + 1) ^ n"
      using binomial[of 1 1 n] by simp
    also have "1 / 2 *  = real (4 ^ k)"
      by (simp add: k_eq power_mult)
    finally have less: "({p. prime p  p  {k + 1<..n}}) < 4 ^ k"
      unfolding of_nat_less_iff by simp

    have "F n = F (Suc k) * ({p. prime p  p  {k+1<..n}})" unfolding F_def
      by (subst prod.union_disjoint [symmetric]) (auto intro!: prod.cong simp: k_eq)
    also have " < 4 ^ Suc k * 4 ^ k" using n
      by (intro mult_strict_mono less less.IH) (auto simp: k_eq)
    also have " = 4 ^ (Suc k + k)"
      by (simp add: power_add)
    also have "Suc k + k = n" by (simp add: k_eq)
    finally show ?case .
  qed (insert less.prems, auto)
qed

lemma θ_upper_bound:
  assumes x: "x  1"
  shows   "θ x < ln 4 * x"
proof -
  have "4 powr (θ x / ln 4) = (p | prime p  p  nat x. 4 powr (log 4 (real p)))"
    by (simp add: θ_def powr_sum prime_sum_upto_altdef2 sum_divide_distrib log_def)
  also have " = (p | prime p  p  nat x. real p)"
    by (intro prod.cong) (auto dest: prime_gt_1_nat)
  also have " = real (p | prime p  p  nat x. p)"
    by simp
  also have "(p | prime p  p  nat x. p) < 4 ^ nat x"
    using x by (intro prod_primes_upto_less) auto
  also have " = 4 powr real (nat x)"
    using x by (subst powr_realpow) auto
  also have "  4 powr x"
    using x by (intro powr_mono) auto
  finally have "4 powr (θ x / ln 4) < 4 powr x"
    by simp
  thus "θ x < ln 4 * x"
    by (subst (asm) powr_less_cancel_iff) (auto simp: field_simps)
qed

lemma θ_bigo: "θ  O(λx. x)"
  by (intro le_imp_bigo_real[of "ln 4"] eventually_mono[OF eventually_ge_at_top[of 1]]
            less_imp_le[OF θ_upper_bound]) auto

lemma ψ_minus_θ_bound:
  assumes x: "x  2"
  shows   "ψ x - θ x  2 * ln x * sqrt x"
proof -
  have "ψ x - θ x = (i | 2  i  real i  log 2 x. θ (root i x))" using x
    by (rule ψ_minus_θ)
  also have "  (i | 2  i  real i  log 2 x. ln 4 * root i x)"
    using x by (intro sum_mono less_imp_le[OF θ_upper_bound]) auto
  also have "  (i | 2  i  real i  log 2 x. ln 4 * root 2 x)" using x
    by (intro sum_mono mult_mono) (auto simp: le_log_iff powr_realpow intro!: real_root_decreasing)
  also have " = card {i. 2  i  real i  log 2 x} * ln 4 * sqrt x"
    by (simp add: sqrt_def)
  also have "{i. 2  i  real i  log 2 x} = {2..nat log 2 x}"
    by (auto simp: le_nat_iff' le_floor_iff)
  also have "log 2 x  1" using x by (simp add: le_log_iff)
  hence "real (nat log 2 x - 1)  log 2 x" using x by linarith
  hence "card {2..nat log 2 x}  log 2 x" by simp
  also have "ln (2 * 2 :: real) = 2 * ln 2" by (subst ln_mult) auto
  hence "log 2 x * ln 4 * sqrt x = 2 * ln x * sqrt x" using x
    by (simp add: ln_sqrt log_def power2_eq_square field_simps)
  finally show ?thesis using x by (simp add: mult_right_mono)
qed

lemma ψ_minus_θ_bigo: "(λx. ψ x - θ x)  O(λx. ln x * sqrt x)"
proof (intro bigoI[of _ "2"] eventually_mono[OF eventually_ge_at_top[of 2]])
  fix x :: real assume "x  2"
  thus "norm (ψ x - θ x)  2 * norm (ln x * sqrt x)"
    using ψ_minus_θ_bound[of x] θ_le_ψ[of x] by simp
qed

lemma ψ_bigo: "ψ  O(λx. x)"
proof -
  have "(λx. ψ x - θ x)  O(λx. ln x * sqrt x)"
    by (rule ψ_minus_θ_bigo)
  also have "(λx. ln x * sqrt x)  O(λx. x)"
    by real_asymp
  finally have "(λx. ψ x - θ x + θ x)  O(λx. x)"
    by (rule sum_in_bigo) (fact θ_bigo)
  thus ?thesis by simp
qed

text ‹
  We shall now attempt to get some more concrete bounds on the difference
  between $\pi(x)$ and $\theta(x)/\ln x$ These will be essential in showing the Prime
  Number Theorem later.

  We first need some bounds on the integral
  \[\int\nolimits_2^x \frac{1}{\ln^2 t}\,\mathrm{d}t\]
  in order to bound the contribution of the remainder term. This integral actually has an
  antiderivative in terms of the logarithmic integral $\textrm{li}(x)$, but since we do not have a
  formalisation of it in Isabelle, we will instead use the following ad-hoc bound given by Apostol:
›
lemma integral_one_over_log_squared_bound:
  assumes x: "x  4"
  shows   "integral {2..x} (λt. 1 / ln t ^ 2)  sqrt x / ln 2 ^ 2 + 4 * x / ln x ^ 2"
proof -
  from x have "x * 1  x ^ 2" unfolding power2_eq_square by (intro mult_left_mono) auto
  with x have x': "2  sqrt x" "sqrt x  x"
    by (auto simp: real_sqrt_le_iff' intro!: real_le_rsqrt)
  have "integral {2..x} (λt. 1 / ln t ^ 2) =
          integral {2..sqrt x} (λt. 1 / ln t ^ 2) + integral {sqrt x..x} (λt. 1 / ln t ^ 2)"
    (is "_ = ?I1 + ?I2") using x x'
    by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] integrable_continuous_real)
       (auto intro!: continuous_intros)
  also have "?I1  integral {2..sqrt x} (λ_. 1 / ln 2 ^ 2)" using x
    by (intro integral_le integrable_continuous_real divide_left_mono
              power_mono continuous_intros) auto
  also have "  sqrt x / ln 2 ^ 2" using x' by (simp add: field_simps)
  also have "?I2  integral {sqrt x..x} (λt. 1 / ln (sqrt x) ^ 2)" using x'
    by (intro integral_le integrable_continuous_real divide_left_mono
              power_mono continuous_intros) auto
  also have "  4 * x / ln x ^ 2" using x' by (simp add: ln_sqrt field_simps)
  finally show ?thesis by simp
qed

lemma integral_one_over_log_squared_bigo:
  "(λx::real. integral {2..x} (λt. 1 / ln t ^ 2))  O(λx. x / ln x ^ 2)"
proof -
  define ub where "ub = (λx::real. sqrt x / ln 2 ^ 2 + 4 * x / ln x ^ 2)"
  have "eventually (λx. ¦integral {2..x} (λt. 1 / (ln t)2)¦  ¦ub x¦) at_top"
    using eventually_ge_at_top[of 4]
  proof eventually_elim
    case (elim x)
    hence "¦integral {2..x} (λt. 1 / ln t ^ 2)¦ = integral {2..x} (λt. 1 / ln t ^ 2)"
      by (intro abs_of_nonneg integral_nonneg integrable_continuous_real continuous_intros) auto
    also have "  ¦ub x¦"
      using integral_one_over_log_squared_bound[of x] elim by (simp add: ub_def)
    finally show ?case .
  qed
  hence "(λx. integral {2..x} (λt. 1 / (ln t)2))  O(ub)"
    by (intro landau_o.bigI[of 1]) auto
  also have "ub  O(λx. x / ln x ^ 2)" unfolding ub_def by real_asymp
  finally show ?thesis .
qed

lemma π_θ_bound:
  assumes "x  (4 :: real)"
  defines "ub  2 / ln 2 * sqrt x + 8 * ln 2 * x / ln x ^ 2"
  shows   "π x - θ x / ln x  {0..ub}"
proof -
  define r where "r = (λx. integral {2..x} (λt. θ t / (t * ln t ^ 2)))"
  have integrable: "(λt. c / ln t ^ 2) integrable_on {2..x}" for c
    by (intro integrable_continuous_real continuous_intros) auto

  have "r x  integral {2..x} (λt. ln 4 / ln t ^ 2)" unfolding r_def
    using integrable_weighted_θ[of 2 x] integrable[of "ln 4"] assms less_imp_le[OF θ_upper_bound]
    by (intro integral_le divide_right_mono) (auto simp: field_simps)
  also have " = ln 4 * integral {2..x} (λt. 1 / ln t ^ 2)"
    using integrable[of 1] by (subst integral_mult) auto
  also have "  ln 4 * (sqrt x / ln 2 ^ 2 + 4 * x / ln x ^ 2)"
    using assms by (intro mult_left_mono integral_one_over_log_squared_bound) auto
  also have "ln (4 :: real) = 2 * ln 2"
    using ln_realpow[of 2 2] by simp
  also have " * (sqrt x / ln 2 ^ 2 + 4 * x / ln x ^ 2) = ub"
    using assms by (simp add: field_simps power2_eq_square ub_def)
  finally have "r x  " .
  moreover have "r x  0" unfolding r_def using assms
    by (intro integral_nonneg integrable_weighted_θ divide_nonneg_pos) auto
  ultimately have "r x  {0..ub}" by auto
  with π_conv_θ_integral[of x] assms(1) show ?thesis
    by (simp add: r_def has_integral_iff)
qed

text ‹
  The following statement already indicates that the asymptotics of π› and θ›
  are very closely related, since through it, $\pi(x) \sim x / \ln x$ and $\theta(x) \sim x$
  imply each other.
›
lemma π_θ_bigo: "(λx. π x - θ x / ln x)  O(λx. x / ln x ^ 2)"
proof -
  define ub where "ub = (λx. 2 / ln 2 * sqrt x + 8 * ln 2 * x / ln x ^ 2)"
  have "(λx. π x - θ x / ln x)  O(ub)"
  proof (intro le_imp_bigo_real[of 1] eventually_mono[OF eventually_ge_at_top])
    fix x :: real assume "x  4"
    from π_θ_bound[OF this] show "π x - θ x / ln x  0" and "π x - θ x / ln x  1 * ub x"
      by (simp_all add: ub_def)
  qed auto
  also have "ub  O(λx. x / ln x ^ 2)"
    unfolding ub_def by real_asymp
  finally show ?thesis .
qed

text ‹
  As a foreshadowing of the Prime Number Theorem, we can already show
  the following upper bound on $\pi(x)$:
›
lemma π_upper_bound:
  assumes "x  (4 :: real)"
  shows   "π x < ln 4 * x / ln x  +  8 * ln 2 * x / ln x ^ 2  +  2 / ln 2 * sqrt x"
proof -
  define ub where "ub = 2 / ln 2 * sqrt x + 8 * ln 2 * x / ln x ^ 2"
  have "π x  θ x / ln x + ub"
    using π_θ_bound[of x] assms unfolding ub_def by simp
  also from assms have "θ x / ln x < ln 4 * x / ln x"
    by (intro θ_upper_bound divide_strict_right_mono) auto
  finally show ?thesis
    using assms by (simp add: algebra_simps ub_def)
qed

lemma π_bigo: "π  O(λx. x / ln x)"
proof -
  have "(λx. π x - θ x / ln x)  O(λx. x / ln x ^ 2)"
    by (fact π_θ_bigo)
  also have "(λx::real. x / ln x ^ 2)  O(λx. x / ln x)"
    by real_asymp
  finally have "(λx. π x - θ x / ln x)  O(λx. x / ln x)" .
  moreover have "eventually (λx::real. ln x > 0) at_top" by real_asymp
  hence "eventually (λx::real. ln x  0) at_top" by eventually_elim auto
  hence "(λx. θ x / ln x)  O(λx. x / ln x)"
    using θ_bigo by (intro landau_o.big.divide_right)
  ultimately have "(λx. π x - θ x / ln x + θ x / ln x)  O(λx. x / ln x)"
    by (rule sum_in_bigo)
  thus ?thesis by simp
qed


subsection ‹Equivalence of various forms of the Prime Number Theorem›

text ‹
  In this section, we show that the following forms of the Prime Number Theorem are
  all equivalent:
     $\pi(x) \sim x / \ln x$
     $\pi(x) \ln \pi(x) \sim x$
     $p_n \sim n \ln n$
     $\vartheta(x) \sim x$
     $\psi(x) \sim x$

  We show the following implication chains:
     (1) → (2) → (3) → (2) → (1)›
     (1) → (4) → (1)›
     (4) → (5) → (4)›

  All of these proofs are taken from Apostol's book.
›

lemma PNT1_imp_PNT1':
  assumes "π ∼[at_top] (λx. x / ln x)"
  shows   "(λx. ln (π x)) ∼[at_top] ln"
proof -
  (* TODO: Tedious Landau sum reasoning *)
  from assms have "((λx. π x / (x / ln x))  1) at_top"
    by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto
  hence "((λx. ln (π x / (x / ln x)))  ln 1) at_top"
    by (rule tendsto_ln) auto
  also have "?this  ((λx. ln (π x) - ln x + ln (ln x))  0) at_top"
    by (intro filterlim_cong eventually_mono[OF eventually_gt_at_top[of 2]])
       (auto simp: ln_div field_simps ln_mult π_pos)
  finally have "(λx. ln (π x) - ln x + ln (ln x))  o(λ_. 1)"
    by (intro smalloI_tendsto) auto
  also have "(λ_::real. 1 :: real)  o(λx. ln x)"
    by real_asymp
  finally have "(λx. ln (π x) - ln x + ln (ln x) - ln (ln x))  o(λx. ln x)"
    by (rule sum_in_smallo) real_asymp+
  thus *: "(λx. ln (π x)) ∼[at_top] ln"
    by (simp add: asymp_equiv_altdef)
qed

lemma PNT1_imp_PNT2:
  assumes "π ∼[at_top] (λx. x / ln x)"
  shows   "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
proof -
  have "(λx. π x * ln (π x)) ∼[at_top] (λx. x / ln x * ln x)"
    by (intro asymp_equiv_intros assms PNT1_imp_PNT1')
  also have " ∼[at_top] (λx. x)"
    by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 1]])
       (auto simp: field_simps)
  finally show "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
    by simp
qed

lemma PNT2_imp_PNT3:
  assumes "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
  shows   "nth_prime ∼[at_top] (λn. n * ln n)"
proof -
  have "(λn. nth_prime n) ∼[at_top] (λn. π (nth_prime n) * ln (π (nth_prime n)))"
    using assms
    by (rule asymp_equiv_symI [OF asymp_equiv_compose'])
       (auto intro!: filterlim_compose[OF filterlim_real_sequentially nth_prime_at_top])
  also have " = (λn. real (Suc n) * ln (real (Suc n)))"
    by (simp add: add_ac)
  also have " ∼[at_top] (λn. real n * ln (real n))"
    by real_asymp
  finally show "nth_prime ∼[at_top] (λn. n * ln n)" .
qed

lemma PNT3_imp_PNT2:
  assumes "nth_prime ∼[at_top] (λn. n * ln n)"
  shows   "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
proof (rule asymp_equiv_symI, rule asymp_equiv_sandwich_real)
  show "eventually (λx. x  {real (nth_prime (nat π x - 1))..real (nth_prime (nat π x))})
          at_top"
    using eventually_ge_at_top[of 2]
  proof eventually_elim
    case (elim x)
    with nth_prime_partition''[of x] show ?case by auto
  qed
next
  have "(λx. real (nth_prime (nat π x - 1))) ∼[at_top