(* 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" 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 - (* TODO: Tedious Landau sum reasoning *) from assms have "((λx. π x / (x / ln x)) ⤏ 1) at_top" by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto hence "((λx. ln (π x / (x / ln x))) ⤏ ln 1) at_top" by (rule tendsto_ln) auto also have "?this ⟷ ((λx. ln (π x) - ln x + ln (ln x)) ⤏ 0) at_top" by (intro filterlim_cong eventually_mono[OF eventually_gt_at_top[of 2]]) (auto simp: ln_div field_simps ln_mult π_pos) finally have "(λx. ln (π x) - ln x + ln (ln x)) ∈ o(λ_. 1)" by (intro smalloI_tendsto) auto also have "(λ_::real. 1 :: real) ∈ o(λx. ln x)" by real_asymp finally have "(λx. ln (π x) - ln x + ln (ln x) - ln (ln x)) ∈ o(λx. ln x)" by (rule sum_in_smallo) real_asymp+ thus *: "(λx. ln (π x)) ∼[at_top] ln" by (simp add: asymp_equiv_altdef) qed lemma PNT1_imp_PNT2: assumes "π ∼[at_top] (λx. x / ln x)" shows "(λx. π x * ln (π x)) ∼[at_top] (λx. x)" proof - have "(λx. π x * ln (π x)) ∼[at_top] (λx. x / ln x * ln x)" by (intro asymp_equiv_intros assms PNT1_imp_PNT1') also have "… ∼[at_top] (λx. x)" by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 1]]) (auto simp: field_simps) finally show "(λx. π x * ln (π x)) ∼[at_top] (λx. x)" by simp qed lemma PNT2_imp_PNT3: assumes "(λx. π x * ln (π x)) ∼[at_top] (λx. x)" shows "nth_prime ∼[at_top] (λn. n * ln n)" proof - have "(λn. nth_prime n) ∼[at_top] (λn. π (nth_prime n) * ln (π (nth_prime n)))" using assms by (rule asymp_equiv_symI [OF asymp_equiv_compose']) (auto intro!: filterlim_compose[OF filterlim_real_sequentially nth_prime_at_top]) also have "… = (λn. real (Suc n) * ln (real (Suc n)))" by (simp add: add_ac) also have "… ∼[at_top] (λn. real n * ln (real n))" by real_asymp finally show "nth_prime ∼[at_top] (λn. n * ln n)" . qed lemma PNT3_imp_PNT2: assumes "nth_prime ∼[at_top] (λn. n * ln n)" shows "(λx. π x * ln (π x)) ∼[at_top] (λx. x)" proof (rule asymp_equiv_symI, rule asymp_equiv_sandwich_real) show "eventually (λx. x ∈ {real (nth_prime (nat ⌊π x⌋ - 1))..real (nth_prime (nat ⌊π x⌋))}) at_top" using eventually_ge_at_top[of 2] proof eventually_elim case (elim x) with nth_prime_partition''[of x] show ?case by auto qed next have "(λx. real (nth_prime (nat ⌊π x⌋ - 1))) ∼[at_top