Theory Prime_Counting_Functions
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"
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 -
(∑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
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 "… ≤ (∑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)"
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 -
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]
(λx. real (nat ⌊π x⌋ - 1) * ln (real (nat ⌊π x⌋ - 1)))"
by (rule asymp_equiv_compose'[OF _ π_at_top], rule asymp_equiv_compose'[OF assms]) real_asymp
also have "… ∼[at_top] (λx. π x * ln (π x))"
by (rule asymp_equiv_compose'[OF _ π_at_top]) real_asymp
finally show "(λx. real (nth_prime (nat ⌊π x⌋ - 1))) ∼[at_top] (λx. π x * ln (π x))" .
next
have "(λx. real (nth_prime (nat ⌊π x⌋))) ∼[at_top]
(λx. real (nat ⌊π x⌋) * ln (real (nat ⌊π x⌋)))"
by (rule asymp_equiv_compose'[OF _ π_at_top], rule asymp_equiv_compose'[OF assms]) real_asymp
also have "… ∼[at_top] (λx. π x * ln (π x))"
by (rule asymp_equiv_compose'[OF _ π_at_top]) real_asymp
finally show "(λx. real (nth_prime (nat ⌊π x⌋))) ∼[at_top] (λx. π x * ln (π x))" .
qed
lemma PNT2_imp_PNT1:
assumes "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
shows "(λx. ln (π x)) ∼[at_top] (λx. ln x)"
and "π ∼[at_top] (λx. x / ln x)"
proof -
have ev: "eventually (λx. π x > 0) at_top"
"eventually (λx. ln (π x) > 0) at_top"
"eventually (λx. ln (ln (π x)) > 0) at_top"
by (rule eventually_compose_filterlim[OF _ π_at_top], real_asymp)+
let ?f = "λx. 1 + ln (ln (π x)) / ln (π x) - ln x / ln (π x)"
have "((λx. ln (π x) * ?f x) ⤏ ln 1) at_top"
proof (rule Lim_transform_eventually)
from assms have "((λx. π x * ln (π x) / x) ⤏ 1) at_top"
by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto
then show "((λx. ln (π x * ln (π x) / x)) ⤏ ln 1) at_top"
by (rule tendsto_ln) auto
show "∀⇩F x in at_top. ln (π x * ln (π x) / x) = ln (π x) * ?f x"
using eventually_gt_at_top[of 0] ev
by eventually_elim (simp add: field_simps ln_mult ln_div)
qed
moreover have "((λx. 1 / ln (π x)) ⤏ 0) at_top"
by (rule filterlim_compose[OF _ π_at_top]) real_asymp
ultimately have "((λx. ln (π x) * ?f x * (1 / ln (π x))) ⤏ ln 1 * 0) at_top"
by (rule tendsto_mult)
moreover have "eventually (λx. ln (π x) * ?f x * (1 / ln (π x)) = ?f x) at_top"
using ev by eventually_elim auto
ultimately have "(?f ⤏ ln 1 * 0) at_top"
by (rule Lim_transform_eventually)
hence "((λx. 1 + ln (ln (π x)) / ln (π x) - ?f x) ⤏ 1 + 0 - ln 1 * 0) at_top"
by (intro tendsto_intros filterlim_compose[OF _ π_at_top]) (real_asymp | simp)+
hence "((λx. ln x / ln (π x)) ⤏ 1) at_top"
by simp
thus *: "(λx. ln (π x)) ∼[at_top] (λx. ln x)"
by (rule asymp_equiv_symI[OF asymp_equivI'])
have "eventually (λx. π x = π x * ln (π x) / ln (π x)) at_top"
using ev by eventually_elim auto
hence "π ∼[at_top] (λx. π x * ln (π x) / ln (π x))"
by (rule asymp_equiv_refl_ev)
also from assms and * have "(λx. π x * ln (π x) / ln (π x)) ∼[at_top] (λx. x / ln x)"
by (rule asymp_equiv_intros)
finally show "π ∼[at_top] (λx. x / ln x)" .
qed
lemma PNT4_imp_PNT5:
assumes "θ ∼[at_top] (λx. x)"
shows "ψ ∼[at_top] (λx. x)"
proof -
define r where "r = (λx. ψ x - θ x)"
have "r ∈ O(λx. ln x * sqrt x)"
unfolding r_def by (fact ψ_minus_θ_bigo)
also have "(λx::real. ln x * sqrt x) ∈ o(λx. x)"
by real_asymp
finally have r: "r ∈ o(λx. x)" .
have "(λx. θ x + r x) ∼[at_top] (λx. x)"
using assms r by (subst asymp_equiv_add_right) auto
thus ?thesis by (simp add: r_def)
qed
lemma PNT4_imp_PNT1:
assumes "θ ∼[at_top] (λx. x)"
shows "π ∼[at_top] (λx. x / ln x)"
proof -
have "(λx. (π x - θ x / ln x) + ((θ x - x) / ln x)) ∈ o(λx. x / ln x)"
proof (rule sum_in_smallo)
have "(λx. π x - θ x / ln x) ∈ O(λx. x / ln x ^ 2)"
by (rule π_θ_bigo)
also have "(λx. x / ln x ^ 2) ∈ o(λx. x / ln x :: real)"
by real_asymp
finally show "(λx. π x - θ x / ln x) ∈ o(λx. x / ln x)" .
next
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
thus "(λx. (θ x - x) / ln x) ∈ o(λx. x / ln x)"
by (intro landau_o.small.divide_right asymp_equiv_imp_diff_smallo assms)
qed
thus ?thesis by (simp add: diff_divide_distrib asymp_equiv_altdef)
qed
lemma PNT1_imp_PNT4:
assumes "π ∼[at_top] (λx. x / ln x)"
shows "θ ∼[at_top] (λx. x)"
proof -
have "θ ∼[at_top] (λx. π x * ln x)"
proof (rule smallo_imp_asymp_equiv)
have "(λx. θ x - π x * ln x) ∈ Θ(λx. - ((π x - θ x / ln x) * ln x))"
by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 1]])
(auto simp: field_simps)
also have "(λx. - ((π x - θ x / ln x) * ln x)) ∈ O(λx. x / (ln x)⇧2 * ln x)"
unfolding landau_o.big.uminus_in_iff by (intro landau_o.big.mult_right π_θ_bigo)
also have "(λx::real. x / (ln x)⇧2 * ln x) ∈ o(λx. x / ln x * ln x)"
by real_asymp
also have "(λx. x / ln x * ln x) ∈ Θ(λx. π x * ln x)"
by (intro asymp_equiv_imp_bigtheta asymp_equiv_intros asymp_equiv_symI[OF assms])
finally show "(λx. θ x - π x * ln x) ∈ o(λx. π x * ln x)" .
qed
also have "… ∼[at_top] (λx. x / ln x * ln x)"
by (intro asymp_equiv_intros assms)
also have "… ∼[at_top] (λx. x)"
by real_asymp
finally show ?thesis .
qed
lemma PNT5_imp_PNT4:
assumes "ψ ∼[at_top] (λx. x)"
shows "θ ∼[at_top] (λx. x)"
proof -
define r where "r = (λx. θ x - ψ x)"
have "(λx. ψ x - θ x) ∈ O(λx. ln x * sqrt x)"
by (fact ψ_minus_θ_bigo)
also have "(λx. ψ x - θ x) = (λx. -r x)"
by (simp add: r_def)
finally have "r ∈ O(λx. ln x * sqrt x)"
by simp
also have "(λx::real. ln x * sqrt x) ∈ o(λx. x)"
by real_asymp
finally have r: "r ∈ o(λx. x)" .
have "(λx. ψ x + r x) ∼[at_top] (λx. x)"
using assms r by (subst asymp_equiv_add_right) auto
thus ?thesis by (simp add: r_def)
qed
subsection ‹The asymptotic form of Mertens' First Theorem›
text ‹
Mertens' first theorem states that $\mathfrak{M}(x) - \ln x$ is bounded, i.\,e.\
$\mathfrak{M}(x) = \ln x + O(1)$.
With some work, one can also show some absolute bounds for $|\mathfrak{M}(x) - \ln x|$, and we
will, in fact, do this later. However, this asymptotic form is somewhat easier to obtain and it is
(as we shall see) enough to prove the Prime Number Theorem, so we prove the weak form here first
for the sake of a smoother presentation.
First of all, we need a very weak version of Stirling's formula for the logarithm of
the factorial, namely:
\[\ln(\lfloor x\rfloor!) = \sum\limits_{n\leq x} \ln x = x \ln x + O(x)\]
We show this using summation by parts.
›
lemma stirling_weak:
assumes x: "x ≥ 1"
shows "sum_upto ln x ∈ {x * ln x - x - ln x + 1 .. x * ln x}"
proof (cases "x = 1")
case True
have "{0<..Suc 0} = {1}" by auto
with True show ?thesis by (simp add: sum_upto_altdef)
next
case False
with assms have x: "x > 1" by simp
have "((λt. sum_upto (λ_. 1) t * (1 / t)) has_integral
sum_upto (λ_. 1) x * ln x - sum_upto (λ_. 1) 1 * ln 1 -
(∑n∈real -` {1<..x}. 1 * ln (real n))) {1..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)
hence "((λt. real (nat ⌊t⌋) / t) has_integral
real (nat ⌊x⌋) * ln x - (∑n∈real -` {1<..x}. ln (real n))) {1..x}"
by (simp add: sum_upto_altdef)
also have "(∑n∈real -` {1<..x}. ln (real n)) = sum_upto ln x" unfolding sum_upto_def
by (intro sum.mono_neutral_left)
(auto intro!: finite_subset[OF _ finite_vimage_real_of_nat_greaterThanAtMost[of 0 x]])
finally have *: "((λt. real (nat ⌊t⌋) / t) has_integral ⌊x⌋ * ln x - sum_upto ln x) {1..x}"
using x by simp
have "0 ≤ real_of_int ⌊x⌋ * ln x - sum_upto (λn. ln (real n)) x"
using * by (rule has_integral_nonneg) auto
also have "… ≤ x * ln x - sum_upto ln x"
using x by (intro diff_mono mult_mono) auto
finally have upper: "sum_upto ln x ≤ x * ln x" by simp
have "(x - 1) * ln x - x + 1 ≤ ⌊x⌋ * ln x - x + 1"
using x by (intro diff_mono mult_mono add_mono) auto
also have "((λt. 1) has_integral (x - 1)) {1..x}"
using has_integral_const_real[of "1::real" 1 x] x by simp
from * and this have "⌊x⌋ * ln x - sum_upto ln x ≤ x - 1"
by (rule has_integral_le) auto
hence "⌊x⌋ * ln x - x + 1 ≤ sum_upto ln x"
by simp
finally have "sum_upto ln x ≥ x * ln x - x - ln x + 1"
by (simp add: algebra_simps)
with upper show ?thesis by simp
qed
lemma stirling_weak_bigo: "(λx::real. sum_upto ln x - x * ln x) ∈ O(λx. x)"
proof -
have "(λx. sum_upto ln x - x * ln x) ∈ O(λx. -(sum_upto ln x - x * ln x))"
by (subst landau_o.big.uminus) auto
also have "(λx. -(sum_upto ln x - x * ln x)) ∈ O(λx. x + ln x - 1)"
proof (intro le_imp_bigo_real[of 2] eventually_mono[OF eventually_ge_at_top[of 1]], goal_cases)
case (2 x)
thus ?case using stirling_weak[of x] by (auto simp: algebra_simps)
next
case (3 x)
thus ?case using stirling_weak[of x] by (auto simp: algebra_simps)
qed auto
also have "(λx. x + ln x - 1) ∈ O(λx::real. x)" by real_asymp
finally show ?thesis .
qed
lemma floor_floor_div_eq:
fixes x :: real and d :: nat
assumes "x ≥ 0"
shows "⌊nat ⌊x⌋ / real d⌋ = ⌊x / real d⌋"
proof -
have "⌊nat ⌊x⌋ / real_of_int (int d)⌋ = ⌊x / real_of_int (int d)⌋" using assms
by (subst (1 2) floor_divide_real_eq_div) auto
thus ?thesis by simp
qed
text ‹
The key to showing Mertens' first theorem is the function
\[h(x) := \sum\limits_{n \leq x} \frac{\Lambda(d)}{d}\]
where $\Lambda$ is the Mangoldt function, which is equal to $\ln p$ for any prime power
$p^k$ and $0$ otherwise. As we shall see, $h(x)$ is a good approximation for $\mathfrak M(x)$,
as the difference between them is bounded by a constant.
›
lemma sum_upto_mangoldt_over_id_minus_phi_bounded:
"(λx. sum_upto (λd. mangoldt d / real d) x - 𝔐 x) ∈ O(λ_. 1)"
proof -
define f where "f = (λd. mangoldt d / real d)"
define C where "C = (∑p. ln (real (p + 1)) * (1 / real (p * (p - 1))))"
have summable: "summable (λp::nat. ln (p + 1) * (1 / (p * (p - 1))))"
proof (rule summable_comparison_test_bigo)
show "summable (λp. norm (p powr (-3/2)))"
by (simp add: summable_real_powr_iff)
qed real_asymp
have diff_bound: "sum_upto f x - 𝔐 x ∈ {0..C}" if x: "x ≥ 4" for x
proof -
define S where "S = {(p, i). prime p ∧ 0 < i ∧ real (p ^ i) ≤ x}"
define S' where "S' = (SIGMA p:{2..nat ⌊root 2 x⌋}. {2..nat ⌊log 2 x⌋})"
have "S ⊆ {..nat ⌊x⌋} × {..nat ⌊log 2 x⌋}" unfolding S_def
using x primepows_le_subset[of x 1] by (auto simp: Suc_le_eq)
hence "finite S" by (rule finite_subset) auto
note fin = finite_subset[OF _ this, unfolded S_def]
have "sum_upto f x = (∑(p, i)∈S. ln (real p) / real (p ^ i))" unfolding S_def
by (intro sum_upto_primepows) (auto simp: f_def mangoldt_non_primepow)
also have "S = {p. prime p ∧ p ≤ x} × {1} ∪ {(p, i). prime p ∧ 1 < i ∧ real (p ^ i) ≤ x}"
by (auto simp: S_def not_less le_Suc_eq not_le intro!: Suc_lessI)
also have "(∑(p,i)∈…. ln (real p) / real (p ^ i)) =
(∑(p, i) ∈ {p. prime p ∧ of_nat p ≤ x} × {1}. ln (real p) / real (p ^ i)) +
(∑(p, i) | prime p ∧ real (p ^ i) ≤ x ∧ i > 1. ln (real p) / real (p ^ i))"
(is "_ = ?S1 + ?S2")
by (subst sum.union_disjoint[OF fin fin]) (auto simp: conj_commute case_prod_unfold)
also have "?S1 = 𝔐 x"
by (subst sum.cartesian_product [symmetric]) (auto simp: primes_M_def prime_sum_upto_def)
finally have eq: "sum_upto f x - 𝔐 x = ?S2" by simp
have "?S2 ≤ (∑(p, i)∈S'. ln (real p) / real (p ^ i))"
using primepows_le_subset[of x 2] x unfolding case_prod_unfold of_nat_power
by (intro sum_mono2 divide_nonneg_pos zero_less_power)
(auto simp: eval_nat_numeral Suc_le_eq S'_def subset_iff dest: prime_gt_1_nat)+
also have "… = (∑p=2..nat ⌊sqrt x⌋. ln p * (∑i∈{2..nat ⌊log 2 x⌋}. (1 / real p) ^ i))"
by (simp add: S'_def sum.Sigma case_prod_unfold
sum_distrib_left sqrt_def field_simps)
also have "… ≤ (∑p=2..nat ⌊sqrt x⌋. ln p * (1 / (p * (p - 1))))"
unfolding sum_upto_def
proof (intro sum_mono, goal_cases)
case (1 p)
from x have "nat ⌊log 2 x⌋ ≥ 2"
by (auto simp: le_nat_iff' le_log_iff)
hence "(∑i∈{2..nat ⌊log 2 x⌋}. (1 / real p) ^ i) =
((1 / p)⇧2 - (1 / p) ^ nat ⌊log 2 x⌋ / p) / (1 - 1 / p)" using 1
by (subst sum_gp) (auto dest!: prime_gt_1_nat simp: field_simps power2_eq_square)
also have "… ≤ ((1 / p) ^ 2 - 0) / (1 - 1 / p)"
using 1 by (intro divide_right_mono diff_mono power_mono)
(auto simp: field_simps dest: prime_gt_0_nat)
also have "… = 1 / (p * (p - 1))"
by (auto simp: divide_simps power2_eq_square dest: prime_gt_0_nat)
finally show ?case
using 1 by (intro mult_left_mono) (auto dest: prime_gt_0_nat)
qed
also have "… ≤ (∑p=2..nat ⌊sqrt x⌋. ln (p + 1) * (1 / (p * (p - 1))))"
by (intro sum_mono mult_mono) auto
also have "… ≤ C" unfolding C_def
by (intro sum_le_suminf summable) auto
finally have "?S2 ≤ C" by simp
moreover have "?S2 ≥ 0" by (intro sum_nonneg) (auto dest: prime_gt_0_nat)
ultimately show ?thesis using eq by simp
qed
from diff_bound[of 4] have "C ≥ 0" by auto
with diff_bound show "(λx. sum_upto f x - 𝔐 x) ∈ O(λ_. 1)"
by (intro le_imp_bigo_real[of C] eventually_mono[OF eventually_ge_at_top[of 4]]) auto
qed
text ‹
Next, we show that our $h(x)$ itself is close to $\ln x$, i.\,e.:
\[\sum\limits_{n \leq x} \frac{\Lambda(d)}{d} = \ln x + O(1)\]
›
lemma sum_upto_mangoldt_over_id_asymptotics:
"(λx. sum_upto (λd. mangoldt d / real d) x - ln x) ∈ O(λ_. 1)"
proof -
define r where "r = (λn::real. sum_upto (λd. mangoldt d * (n / d - real_of_int ⌊n / d⌋)) n)"
have r: "r ∈ O(ψ)"
proof (intro landau_o.bigI[of 1] eventually_mono[OF eventually_ge_at_top[of 0]])
fix x :: real assume x: "x ≥ 0"
have eq: "{1..nat ⌊x⌋} = {0<..nat ⌊x⌋}" by auto
hence "r x ≥ 0" unfolding r_def sum_upto_def
by (intro sum_nonneg mult_nonneg_nonneg mangoldt_nonneg)
(auto simp: floor_le_iff)
moreover have "x / real d ≤ 1 + real_of_int ⌊x / real d⌋" for d by linarith
hence "r x ≤ sum_upto (λd. mangoldt d * 1) x" unfolding sum_upto_altdef eq r_def using x
by (intro sum_mono mult_mono mangoldt_nonneg)
(auto simp: less_imp_le[OF frac_lt_1] algebra_simps)
ultimately show "norm (r x) ≤ 1 * norm (ψ x)" by (simp add: ψ_def)
qed auto
also have "ψ ∈ O(λx. x)" by (fact ψ_bigo)
finally have r: "r ∈ O(λx. x)" .
define r' where "r' = (λx::real. sum_upto ln x - x * ln x)"
have r'_bigo: "r' ∈ O(λx. x)"
using stirling_weak_bigo unfolding r'_def .
have ln_fact: "ln (fact n) = (∑d=1..n. ln d)" for n
by (induction n) (simp_all add: ln_mult)
hence r': "sum_upto ln n = n * ln n + r' n" for n :: real
unfolding r'_def sum_upto_altdef by (auto intro!: sum.cong)
have "eventually (λn. sum_upto (λd. mangoldt d / d) n - ln n = r' n / n + r n / n) at_top"
using eventually_gt_at_top
proof eventually_elim
fix x :: real assume x: "x > 0"
have "sum_upto ln x = sum_upto (λn. mangoldt n * real (nat ⌊x / n⌋)) x"
unfolding sum_upto_ln_conv_sum_upto_mangoldt ..
also have "… = sum_upto (λd. mangoldt d * (x / d)) x - r x"
unfolding sum_upto_def by (simp add: algebra_simps sum_subtractf r_def sum_upto_def)
also have "sum_upto (λd. mangoldt d * (x / d)) x = x * sum_upto (λd. mangoldt d / d) x"
unfolding sum_upto_def by (subst sum_distrib_left) (simp add: field_simps)
finally have "x * sum_upto (λd. mangoldt d / real d) x = r' x + r x + x * ln x"
by (simp add: r' algebra_simps)
thus "sum_upto (λd. mangoldt d / d) x - ln x = r' x / x + r x / x"
using x by (simp add: field_simps)
qed
hence "(λx. sum_upto (λd. mangoldt d / d) x - ln x) ∈ Θ(λx. r' x / x + r x / x)"
by (rule bigthetaI_cong)
also have "(λx. r' x / x + r x / x) ∈ O(λ_. 1)"
by (intro sum_in_bigo) (insert r r'_bigo, auto simp: landau_divide_simps)
finally show ?thesis .
qed
text ‹
Combining these two gives us Mertens' first theorem.
›
theorem mertens_bounded: "(λx. 𝔐 x - ln x) ∈ O(λ_. 1)"
proof -
define f where "f = sum_upto (λd. mangoldt d / d)"
have "(λx. (f x - ln x) - (f x - 𝔐 x)) ∈ O(λ_. 1)"
using sum_upto_mangoldt_over_id_asymptotics
sum_upto_mangoldt_over_id_minus_phi_bounded
unfolding f_def by (rule sum_in_bigo)
thus ?thesis by simp
qed
lemma primes_M_bigo: "𝔐 ∈ O(λx. ln x)"
proof -
have "(λx. 𝔐 x - ln x) ∈ O(λ_. 1)"
by (rule mertens_bounded)
also have "(λ_::real. 1) ∈ O(λx. ln x)"
by real_asymp
finally have "(λx. 𝔐 x - ln x + ln x) ∈ O(λx. ln x)"
by (rule sum_in_bigo) auto
thus ?thesis by simp
qed
unbundle no_prime_counting_notation
end