# 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 = (∑p←primes_upto (nat ⌊x⌋). f p)"
proof -
have "(∑p←primes_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⌋<..nat⌊b⌋} ⟹ ¬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"

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"

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'})"
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"

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)"
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)"
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)"

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
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 -
(∑n∈real - {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 + (∑n∈real - {2<..x}. ind prime n * ln n)))) {2..x}"
by (simp add: π_def prime_sum_upto_altdef1 algebra_simps)
also have "π 2 * ln 2 + (∑n∈real - {2<..x}. ind prime n * ln n) =
(∑n∈insert 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) -
(∑n∈real - {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) -
(∑n∈real - {2<..x}. b n * (1 / ln (real n))) =
θ x * (1 / ln x) - (∑n∈insert 2 (real - {2<..x}). b n * (1 / ln (real n)))"
by (subst sum.insert) (auto simp: b_def eval_θ)
also have "(∑n∈insert 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 -
(∑n∈real - {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 - (∑n∈real - {2<..x}. b n * real n) =
𝔐 x * x - (∑n∈insert 2 (real - {2<..x}). b n * real n)"
by (subst sum.insert) (auto simp: eval_𝔐 b_def)
also have "(∑n∈insert 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 / t⇧2) 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) -
(∑n∈real - {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) - (∑n∈real - {2<..x}. b n * (-1 / real n)) =
-(θ x / x - (∑n∈insert 2 (real - {2<..x}). b n / real n))"
by (subst sum.insert) (auto simp: eval_θ b_def sum_negf)
also have "(∑n∈insert 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
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⌋})"
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 "… ≤ (∑i≤n. 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)"
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)"
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"
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
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"
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"
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)))"
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