Theory PNT_Consequences
section ‹Consequences of the Prime Number Theorem›
theory PNT_Consequences
imports
Elementary_Prime_Bounds
Prime_Number_Theorem.Mertens_Theorems
Prime_Number_Theorem.Prime_Counting_Functions
Moebius_Mu_Sum
Lcm_Nat_Upto
Primorial
Primes_Omega
begin
text ‹
In this section, we will define a locale that assumes the Prime Number Theorem in order to
explore some of its elementary consequences.
›
unbundle prime_counting_syntax
locale prime_number_theorem =
assumes prime_number_theorem [asymp_equiv_intros]: "π ∼[at_top] (λx. x / ln x)"
begin
corollary θ_asymptotics [asymp_equiv_intros]: "θ ∼[at_top] (λx. x)"
using prime_number_theorem by (rule PNT1_imp_PNT4)
corollary ψ_asymptotics [asymp_equiv_intros]: "ψ ∼[at_top] (λx. x)"
using θ_asymptotics PNT4_imp_PNT5 by simp
corollary ln_π_asymptotics [asymp_equiv_intros]: "(λx. ln (π x)) ∼[at_top] ln"
using prime_number_theorem PNT1_imp_PNT1' by simp
corollary π_ln_π_asymptotics: "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
using prime_number_theorem PNT1_imp_PNT2 by simp
corollary nth_prime_asymptotics [asymp_equiv_intros]:
"(λn. real (nth_prime n)) ∼[at_top] (λn. real n * ln (real n))"
using π_ln_π_asymptotics PNT2_imp_PNT3 by simp
corollary moebius_mu_smallo: "sum_upto moebius_mu ∈ o(λx. x)"
using PNT_implies_sum_moebius_mu_sublinear ψ_asymptotics by simp
lemma ln_θ_asymptotics:
includes prime_counting_syntax
shows "(λx. ln (θ x) - ln x) ∈ o(λ_. 1)"
proof -
have [simp]: "θ 2 = ln 2"
by (simp add: eval_θ)
have θ_pos: "θ x > 0" if "x ≥ 2" for x
proof -
have "0 < ln (2 :: real)" by simp
also have "… ≤ θ x"
using θ_mono[OF that] by simp
finally show ?thesis .
qed
have nz: "eventually (λx. θ x ≠ 0 ∨ x ≠ 0) at_top"
using eventually_gt_at_top[of 0] by eventually_elim auto
have "filterlim (λx. θ x / x) (nhds 1) at_top"
using asymp_equivD_strong[OF θ_asymptotics nz] .
hence "filterlim (λx. ln (θ x / x)) (nhds (ln 1)) at_top"
by (rule tendsto_ln) auto
also have "?this ⟷ filterlim (λx. ln (θ x) - ln x) (nhds 0) at_top"
by (intro filterlim_cong eventually_mono[OF eventually_ge_at_top[of 2]])
(auto simp: ln_divide_pos θ_pos)
finally show "(λx. ln (θ x) - ln x) ∈ o(λx. 1)"
by (intro smalloI_tendsto) auto
qed
lemma ln_θ_asymp_equiv [asymp_equiv_intros]:
includes prime_counting_syntax
shows "(λx. ln (θ x)) ∼[at_top] ln"
proof (rule smallo_imp_asymp_equiv)
have "(λx. ln (θ x) - ln x) ∈ o(λ_. 1)" by (rule ln_θ_asymptotics)
also have "(λ_. 1) ∈ O(λx::real. ln x)" by real_asymp
finally show "(λx. ln (θ x) - ln x) ∈ o(ln)" .
qed
lemma ln_nth_prime_asymptotics:
"(λn. ln (nth_prime n) - (ln n + ln (ln n))) ∈ o(λ_. 1)"
proof -
have "filterlim (λn. ln (nth_prime n / (n * ln n))) (nhds (ln 1)) at_top"
by (intro tendsto_ln asymp_equivD_strong[OF nth_prime_asymptotics])
(auto intro!: eventually_mono[OF eventually_gt_at_top[of 1]])
also have "?this ⟷ filterlim (λn. ln (nth_prime n) - (ln n + ln (ln n))) (nhds 0) at_top"
using prime_gt_0_nat[OF prime_nth_prime]
by (intro filterlim_cong refl eventually_mono[OF eventually_gt_at_top[of 1]])
(auto simp: field_simps ln_mult ln_div)
finally show ?thesis by (intro smalloI_tendsto) auto
qed
lemma ln_nth_prime_asymp_equiv [asymp_equiv_intros]:
"(λn. ln (nth_prime n)) ∼[at_top] ln"
proof -
have "(λn. ln (nth_prime n) - (ln n + ln (ln n))) ∈ o(ln)"
using ln_nth_prime_asymptotics by (rule landau_o.small.trans) real_asymp
hence "(λn. ln (nth_prime n) - (ln n + ln (ln n)) + ln (ln n)) ∈ o(ln)"
by (rule sum_in_smallo) real_asymp
thus ?thesis by (intro smallo_imp_asymp_equiv) auto
qed
text ‹
The following versions use a little less notation.
›
corollary prime_number_theorem': "((λx. π x / (x / ln x)) ⤏ 1) at_top"
using prime_number_theorem
by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto
corollary prime_number_theorem'':
"(λx. card {p. prime p ∧ real p ≤ x}) ∼[at_top] (λx. x / ln x)"
proof -
have "π = (λx. card {p. prime p ∧ real p ≤ x})"
by (intro ext) (simp add: π_def prime_sum_upto_def)
with prime_number_theorem show ?thesis by simp
qed
corollary prime_number_theorem''':
"(λn. card {p. prime p ∧ p ≤ n}) ∼[at_top] (λn. real n / ln (real n))"
proof -
have "(λn. card {p. prime p ∧ real p ≤ real n}) ∼[at_top] (λn. real n / ln (real n))"
using prime_number_theorem''
by (rule asymp_equiv_compose') (simp add: filterlim_real_sequentially)
thus ?thesis by simp
qed
end
subsection ‹Existence of primes in intervals›
text ‹
For fixed ‹ε›, The interval $(x; \varepsilon x]$ contains a prime number for any sufficiently
large ‹x›. This proof was taken from A.\,J. Hildebrand's lecture notes~\<^cite>‹"hildebrand_ant"›.
›
lemma (in prime_number_theorem) prime_in_interval_exists:
fixes c :: real
assumes "c > 1"
shows "eventually (λx. ∃p. prime p ∧ real p ∈ {x<..c*x}) at_top"
proof -
from ‹c > 1› have "(λx. π (c * x) / π x) ∼[at_top] (λx. ((c * x) / ln (c * x)) / (x / ln x))"
by (intro asymp_equiv_intros asymp_equiv_compose'[OF prime_number_theorem]) real_asymp+
also have "… ∼[at_top] (λx. c)"
using ‹c > 1› by real_asymp
finally have "(λx. π (c * x) / π x) ∼[at_top] (λa. c)" by simp
hence "((λx. π (c * x) / π x) ⤏ c) at_top"
by (rule asymp_equivD_const)
from this and ‹c > 1› have "eventually (λx. π (c * x) / π x > 1) at_top"
by (rule order_tendstoD)
moreover have "eventually (λx. π x > 0) at_top"
using π_at_top by (auto simp: filterlim_at_top_dense)
ultimately show ?thesis using eventually_gt_at_top[of 1]
proof eventually_elim
case (elim x)
define P where "P = {p. prime p ∧ real p ∈ {x<..c*x}}"
from elim and ‹c > 1› have "1 * x < c * x" by (intro mult_strict_right_mono) auto
hence "x < c * x" by simp
have "P = {p. prime p ∧ real p ≤ c * x} - {p. prime p ∧ real p ≤ x}"
by (auto simp: P_def)
also have "card … = card {p. prime p ∧ real p ≤ c * x} - card {p. prime p ∧ real p ≤ x}"
using ‹x < c * x› by (subst card_Diff_subset) (auto intro: finite_primes_le)
also have "real … = π (c * x) - π x"
using π_mono[of x "c * x"] ‹x < c * x›
by (subst of_nat_diff) (auto simp: primes_pi_def prime_sum_upto_def)
finally have "real (card P) = π (c * x) - π x" by simp
moreover have "π (c * x) - π x > 0"
using elim by (auto simp: field_simps)
ultimately have "real (card P) > 0" by linarith
hence "card P > 0" by simp
hence "P ≠ {}" by (intro notI) simp
thus ?case by (auto simp: P_def)
qed
qed
text ‹
The set of rationals whose numerator and denominator are primes is
dense in $\mathbb{R}_{{}>0}$.
›
lemma (in prime_number_theorem) prime_fractions_dense:
fixes α ε :: real
assumes "α > 0" and "ε > 0"
obtains p q :: nat where "prime p" and "prime q" and "dist (real p / real q) α < ε"
proof -
define ε' where "ε' = ε / 2"
from assms have "ε' > 0" by (simp add: ε'_def)
have "eventually (λx. ∃p. prime p ∧ real p ∈ {x<..(1 + ε' / α) * x}) at_top"
using assms ‹ε' > 0› by (intro prime_in_interval_exists) (auto simp: field_simps)
then obtain x0 where x0: "⋀x. x ≥ x0 ⟹ ∃p. prime p ∧ real p ∈ {x<..(1 + ε' / α) * x}"
by (auto simp: eventually_at_top_linorder)
have "∃q. prime q ∧ q > nat ⌊x0 / α⌋" by (rule bigger_prime)
then obtain q where "prime q" "q > nat ⌊x0 / α⌋" by blast
hence "real q ≥ x0 / α" by linarith
with ‹α > 0› have "α * real q ≥ x0" by (simp add: field_simps)
hence "∃p. prime p ∧ real p ∈ {α * real q<..(1 + ε' / α) * (α * real q)}"
by (intro x0)
then obtain p where p: "prime p" "real p > α * real q" "real p ≤ (1 + ε' / α) * (α * real q)"
using assms by auto
from p ‹prime q› have "real p / real q ≤ (1 + ε' / α) * α"
using assms by (auto simp: field_simps dest: prime_gt_0_nat)
also have "… = α + ε'"
using assms by (simp add: field_simps)
finally have "real p / real q ≤ α + ε'" .
moreover from p ‹prime q› have "real p / real q > α" "real p / real q ≤ (1 + ε' / α) * α"
using assms by (auto simp: field_simps dest: prime_gt_0_nat)
ultimately have "dist (real p / real q) α ≤ ε'"
by (simp add: dist_norm)
also have "… < ε"
using ‹ε > 0› by (simp add: ε'_def)
finally show ?thesis using ‹prime p› ‹prime q› that[of p q] by blast
qed
subsection ‹The logarithm of the primorial›
text ‹
The PNT directly implies the asymptotics of the logarithm of the primorial function:
›
context prime_number_theorem
begin
lemma ln_primorial_asymp_equiv [asymp_equiv_intros]:
"(λx. ln (primorial x)) ∼[at_top] (λx. x)"
by (auto simp: ln_primorial θ_asymptotics)
lemma ln_ln_primorial_asymp_equiv [asymp_equiv_intros]:
"(λx. ln (ln (primorial x))) ∼[at_top] (λx. ln x)"
by (auto simp: ln_primorial ln_θ_asymp_equiv)
lemma ln_primorial'_asymp_equiv [asymp_equiv_intros]:
"(λk. ln (primorial' k)) ∼[at_top] (λk. k * ln k)"
and ln_ln_primorial'_asymp_equiv [asymp_equiv_intros]:
"(λk. ln (ln (primorial' k))) ∼[at_top] (λk. ln k)"
and ln_over_ln_ln_primorial'_asymp_equiv:
"(λk. ln (primorial' k) / ln (ln (primorial' k))) ∼[at_top] (λk. k)"
proof -
have lim1: "filterlim (λk. real (nth_prime (k - 1))) at_top at_top"
by (rule filterlim_compose[OF filterlim_real_sequentially]
filterlim_compose[OF nth_prime_at_top])+ real_asymp
have lim2: "filterlim (λk::nat. k - 1) at_top at_top"
by real_asymp
have "(λk. ln (primorial' k)) ∼[at_top] (λn. ln (primorial (nth_prime (n - 1))))"
by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 0]])
(auto simp: primorial'_conv_primorial)
also have "… ∼[at_top] (λn. nth_prime (n - 1))"
by (intro asymp_equiv_compose'[OF _ lim1] asymp_equiv_intros)
also have "… ∼[at_top] (λn. real (n - 1) * ln (real (n - 1)))"
by (intro asymp_equiv_compose'[OF _ lim2] asymp_equiv_intros)
also have "… ∼[at_top] (λn. n * ln n)" by real_asymp
finally show 1: "(λk. ln (primorial' k)) ∼[at_top] (λk. k * ln k)" .
have "(λk. ln (ln (primorial' k))) ∼[at_top] (λn. ln (ln (primorial (nth_prime (n - 1)))))"
by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 0]])
(auto simp: primorial'_conv_primorial)
also have "… ∼[at_top] (λn. ln (nth_prime (n - 1)))"
by (intro asymp_equiv_compose'[OF _ lim1] asymp_equiv_intros)
also have "… ∼[at_top] (λn. ln (real (n - 1)))"
by (intro asymp_equiv_compose'[OF _ lim2] asymp_equiv_intros)
also have "… ∼[at_top] (λn. ln n)" by real_asymp
finally show 2: "(λk. ln (ln (primorial' k))) ∼[at_top] (λk. ln k)" .
have "(λk. ln (primorial' k) / ln (ln (primorial' k))) ∼[at_top] (λk. (k * ln k) / ln k)"
by (intro asymp_equiv_intros 1 2)
also have "… ∼[at_top] (λk. k)" by real_asymp
finally show "(λk. ln (primorial' k) / ln (ln (primorial' k))) ∼[at_top] (λk. k)" .
qed
end
subsection ‹Consequences of the asymptotics of ‹ψ› and ‹θ››
text ‹
Next, we will show some consequences of $\psi(x)\sim x$ and $\vartheta(x)\sim x$. To this
end, we first show generically that any function $g = e^{x + o(x)}$ is $o(c^n)$ if $c > e$ and
$\omega(c^n)$ if $c < e$.
›
locale exp_asymp_equiv_linear =
fixes f g :: "real ⇒ real"
assumes f_asymp_equiv: "f ∼[at_top] (λx. x)"
assumes g: "eventually (λx. g x = exp (f x)) F"
begin
lemma
fixes ε :: real assumes "ε > 0"
shows smallo: "g ∈ o(λx. exp ((1 + ε) * x))"
and smallomega: "g ∈ ω(λx. exp ((1 - ε) * x))"
proof -
have "(λx. exp (f x) / exp ((1 + ε) * x)) ∈ Θ(λx. exp (((f x - x) / x - ε) * x))"
by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 1]])
(simp_all add: divide_simps ring_distribs flip: exp_add exp_diff)
also have "((λx. exp (((f x - x) / x - ε) * x)) ⤏ 0) at_top"
proof (intro filterlim_compose[OF exp_at_bot] filterlim_tendsto_neg_mult_at_bot)
have smallo: "(λx. f x - x) ∈ o(λx. x)"
using f_asymp_equiv by (rule asymp_equiv_imp_diff_smallo)
show "((λx. (f x - x) / x - ε) ⤏ 0 - ε) at_top"
by (intro tendsto_diff smalloD_tendsto[OF smallo] tendsto_const)
qed (use ‹ε > 0› in ‹auto simp: filterlim_ident›)
hence "(λx. exp (((f x - x) / x - ε) * x)) ∈ o(λ_. 1)"
by (intro smalloI_tendsto) auto
finally have "(λx. exp (f x)) ∈ o(λx. exp ((1 + ε) * x))"
by (simp add: landau_divide_simps)
also have "?this ⟷ g ∈ o(λx. exp ((1 + ε) * x))"
using g by (intro landau_o.small.in_cong) (simp add: eq_commute)
finally show "g ∈ o(λx. exp ((1 + ε) * x))" .
next
have "(λx. exp (f x) / exp ((1 - ε) * x)) ∈ Θ(λx. exp (((f x - x) / x + ε) * x))"
by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 1]])
(simp add: ring_distribs flip: exp_add exp_diff)
also have "filterlim (λx. exp (((f x - x) / x + ε) * x)) at_top at_top"
proof (intro filterlim_compose[OF exp_at_top] filterlim_tendsto_pos_mult_at_top)
have smallo: "(λx. f x - x) ∈ o(λx. x)"
using f_asymp_equiv by (rule asymp_equiv_imp_diff_smallo)
show "((λx. (f x - x) / x + ε) ⤏ 0 + ε) at_top"
by (intro tendsto_add smalloD_tendsto[OF smallo] tendsto_const)
qed (use ‹ε > 0› in ‹auto simp: filterlim_ident›)
hence "(λx. exp (((f x - x) / x + ε) * x)) ∈ ω(λ_. 1)"
by (simp add: filterlim_at_top_iff_smallomega)
finally have "(λx. exp (f x)) ∈ ω(λx. exp ((1 - ε) * x))"
by (simp add: landau_divide_simps)
also have "?this ⟷ g ∈ ω(λx. exp ((1 - ε) * x))"
using g by (intro landau_omega.small.in_cong) (simp add: eq_commute)
finally show "g ∈ ω(λx. exp ((1 - ε) * x))" .
qed
lemma smallo':
fixes c :: real assumes "c > exp 1"
shows "g ∈ o(λx. c powr x)"
proof -
have "c > 0" by (rule le_less_trans[OF _ assms]) auto
from ‹c > 0› assms have "exp 1 < exp (ln c)"
by (subst exp_ln) auto
hence "ln c > 1" by (subst (asm) exp_less_cancel_iff)
hence "g ∈ o(λx. exp ((1 + (ln c - 1)) * x))"
using assms by (intro smallo) auto
also have "(λx. exp ((1 + (ln c - 1)) * x)) = (λx. c powr x)"
using ‹c > 0› by (simp add: powr_def mult_ac)
finally show ?thesis .
qed
lemma smallomega':
fixes c :: real assumes "c ∈ {0<..<exp 1}"
shows "g ∈ ω(λx. c powr x)"
proof -
from assms have "exp 1 > exp (ln c)"
by (subst exp_ln) auto
hence "ln c < 1" by (subst (asm) exp_less_cancel_iff)
hence "g ∈ ω(λx. exp ((1 - (1 - ln c)) * x))"
using assms by (intro smallomega) auto
also have "(λx. exp ((1 - (1 - ln c)) * x)) = (λx. c powr x)"
using assms by (simp add: powr_def mult_ac)
finally show ?thesis .
qed
end
text ‹
The primorial fulfils $x\# = e^{\vartheta(x)}$ and is therefore one example of this.
›
context prime_number_theorem
begin
sublocale primorial: exp_asymp_equiv_linear θ "λx. real (primorial x)"
using θ_asymptotics by unfold_locales (simp_all add: ln_primorial [symmetric])
end
text ‹
The LCM of the first ‹n› natural numbers is equal to $e^{\psi(n)}$ and is
therefore another example.
›
context prime_number_theorem
begin
sublocale Lcm_upto: exp_asymp_equiv_linear ψ "λx. real (Lcm {1..nat ⌊x⌋})"
using ψ_asymptotics by unfold_locales (simp_all flip: Lcm_upto_real_conv_ψ)
end
subsection ‹Bounds on the prime ‹ω› function›
text ‹
Next, we will examine the asymptotic behaviour of the prime ‹ω› function $\omega(n)$,
i.\,e.\ the number of distinct prime factors of ‹n›. These proofs are again taken from
A.\,J. Hildebrand's lecture notes~\<^cite>‹"hildebrand_ant"›.
›
lemma ln_gt_1:
assumes "x > (3 :: real)"
shows "ln x > 1"
proof -
have "x > exp 1"
using exp_le assms by linarith
hence "ln x > ln (exp 1)" using assms by (subst ln_less_cancel_iff) auto
thus ?thesis by simp
qed
lemma (in prime_number_theorem) primes_omega_primorial'_asymp_equiv:
"(λk. primes_omega (primorial' k)) ∼[at_top]
(λk. ln (primorial' k) / ln (ln (primorial' k)))"
using ln_over_ln_ln_primorial'_asymp_equiv by (simp add: asymp_equiv_sym)
text ‹
The number of distinct prime factors of ‹n› has maximal order $\ln n / \ln\ln n$:
›
theorem (in prime_number_theorem)
limsup_primes_omega: "limsup (λn. primes_omega n / (ln n / ln (ln n))) = 1"
proof (intro antisym)
have "(λk. primes_omega (primorial' k) / (ln (primorial' k) / ln (ln (primorial' k)))) ⇢ 1"
using primes_omega_primorial'_asymp_equiv
by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]]) auto
hence "limsup ((λn. primes_omega n / (ln n / ln (ln n))) ∘ primorial') = ereal 1"
by (intro lim_imp_Limsup tendsto_ereal) simp_all
hence "1 = limsup ((λn. ereal (primes_omega n / (ln n / ln (ln n)))) ∘ primorial')"
by (simp add: o_def)
also have "… ≤ limsup (λn. primes_omega n / (ln n / ln (ln n)))"
using strict_mono_primorial' by (rule limsup_subseq_mono)
finally show "limsup (λn. primes_omega n / (ln n / ln (ln n))) ≥ 1" .
next
show "limsup (λn. primes_omega n / (ln n / ln (ln n))) ≤ 1"
unfolding Limsup_le_iff
proof safe
fix C' :: ereal assume C': "C' > 1"
from ereal_dense2[OF this] obtain C where C: "C > 1" "ereal C < C'" by auto
have "(λk. primes_omega (primorial' k) / (ln (primorial' k) / ln (ln (primorial' k)))) ⇢ 1"
(is "filterlim ?f _ _") using primes_omega_primorial'_asymp_equiv
by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]]) auto
from order_tendstoD(2)[OF this C(1)]
have "eventually (λk. ?f k < C) at_top" .
then obtain k0 where k0: "⋀k. k ≥ k0 ⟹ ?f k < C" by (auto simp: eventually_at_top_linorder)
have "eventually (λn::nat. max 3 k0 / (ln n / ln (ln n)) < C) at_top"
using ‹C > 1› by real_asymp
hence "eventually (λn. primes_omega n / (ln n / ln (ln n)) ≤ C) at_top"
using eventually_gt_at_top[of "primorial' (max k0 3)"]
proof eventually_elim
case (elim n)
define k where "k = primes_omega n"
define m where "m = primorial' k"
have "primorial' 3 ≤ primorial' (max k0 3)"
by (subst strict_mono_less_eq[OF strict_mono_primorial']) auto
also have "… < n" by fact
finally have "n > 30" by simp
show ?case
proof (cases "k ≥ max 3 k0")
case True
hence "m ≥ 30"
using strict_mono_less_eq[OF strict_mono_primorial', of 3 k] by (simp add: m_def k_def)
have "exp 1 ^ 3 ≤ (3 ^ 3 :: real)"
using exp_le by (intro power_mono) auto
also have "… < m" using ‹m ≥ 30› by simp
finally have "ln (exp 1 ^ 3) < ln m"
using ‹m ≥ 30› by (subst ln_less_cancel_iff) auto
hence "ln m > 3" by (subst (asm) ln_realpow) auto
have "primorial' (primes_omega n) ≤ n"
using ‹n > 30› by (intro primorial'_primes_omega_le) auto
hence "m ≤ n" unfolding m_def k_def using elim
by (auto simp: max_def)
hence "primes_omega n / (ln n / ln (ln n)) ≤ k / (ln m / ln (ln m))"
unfolding k_def using elim ‹m ≥ 30› ln_gt_1[of n] ‹ln m > 3›
by (intro frac_le[of "primes_omega n"] divide_ln_mono mult_pos_pos divide_pos_pos) auto
also have "… = ?f k"
by (simp add: k_def m_def)
also have "… < C"
by (intro k0) (use True in ‹auto simp: k_def›)
finally show ?thesis by simp
next
case False
hence "primes_omega n / (ln n / ln (ln n)) ≤ max 3 k0 / (ln n / ln (ln n))"
using elim ln_gt_1[of n] ‹n > 30›
by (intro divide_right_mono divide_nonneg_pos) (auto simp: k_def)
also have "… < C"
using elim by simp
finally show ?thesis by simp
qed
qed
thus "eventually (λn. ereal (primes_omega n / (ln n / ln (ln n))) < C') at_top"
by eventually_elim (rule le_less_trans[OF _ C(2)], auto)
qed
qed
subsection ‹Bounds on the divisor function›
text ‹
In this section, we shall examine the growth of the divisor function $\sigma_0(n)$.
In particular, we will show that $\sigma_0(n) < 2^{c\ln n / \ln\ln n}$ for all sufficiently
large ‹n› if $c > 1$ and $\sigma_0(n) > 2^{c\ln n / \ln\ln n}$ for infinitely many ‹n›
if $c < 1$.
An equivalent statement is that $\ln(\sigma_0(n))$ has maximal order
$\ln 2 \cdot \ln n / \ln\ln n$.
Following Apostol's somewhat didactic approach, we first show a generic bounding lemma for
$\sigma_0$ that depends on some function ‹f› that we will specify later.
›
lemma divisor_count_bound_gen:
fixes f :: "nat ⇒ real"
assumes "eventually (λn. f n ≥ 2) at_top"
defines "c ≡ (8 / ln 2 :: real)"
defines "g ≡ (λn. (ln n + c * f n * ln (ln n)) / (ln (f n)))"
shows "eventually (λn. divisor_count n < 2 powr g n) at_top"
proof -
include prime_counting_syntax
have "eventually (λn::nat. 1 + log 2 n ≤ ln n ^ 2) at_top" by real_asymp
thus "eventually (λn. divisor_count n < 2 powr g n) at_top"
using eventually_gt_at_top[of 2] assms(1)
proof eventually_elim
fix n :: nat
assume n: "n > 2" and "f n ≥ 2" and "1 + log 2 n ≤ ln n ^ 2"
define Pr where [simp]: "Pr = prime_factors n"
define Pr1 where [simp]: "Pr1 = {p∈Pr. p < f n}"
define Pr2 where [simp]: "Pr2 = {p∈Pr. p ≥ f n}"
have "exp 1 < real n"
using e_less_272 ‹n > 2› by linarith
hence "ln (exp 1) < ln (real n)"
using ‹n > 2› by (subst ln_less_cancel_iff) auto
hence "ln (ln n) > ln (ln (exp 1))"
by (subst ln_less_cancel_iff) auto
hence "ln (ln n) > 0" by simp
define S2 where "S2 = (∑p∈Pr2. multiplicity p n)"
have "f n ^ S2 = (∏p∈Pr2. f n ^ multiplicity p n)"
by (simp add: S2_def power_sum)
also have "… ≤ (∏p∈Pr2. real p ^ multiplicity p n)"
using ‹f n ≥ 2› by (intro prod_mono conjI power_mono) auto
also from ‹n > 2› have "… ≤ (∏p∈Pr. real p ^ multiplicity p n)"
by (intro prod_mono2 one_le_power) (auto simp: in_prime_factors_iff dest: prime_gt_0_nat)
also have "… = n"
using ‹n > 2› by (subst prime_factorization_nat[of n]) auto
finally have "f n ^ S2 ≤ n" .
hence "ln (f n ^ S2) ≤ ln n"
using n ‹f n ≥ 2› by (subst ln_le_cancel_iff) auto
hence "S2 ≤ ln n / ln (f n)"
using ‹f n ≥ 2› by (simp add: field_simps ln_realpow)
have le_twopow: "Suc a ≤ 2 ^ a" for a :: nat by (induction a) auto
have "(∏p∈Pr2. Suc (multiplicity p n)) ≤ (∏p∈Pr2. 2 ^ multiplicity p n)"
by (intro prod_mono conjI le_twopow) auto
also have "… = 2 ^ S2"
by (simp add: S2_def power_sum)
also have "… = 2 powr real S2"
by (subst powr_realpow) auto
also have "… ≤ 2 powr (ln n / ln (f n))"
by (intro powr_mono ‹S2 ≤ ln n / ln (f n)›) auto
finally have bound2: "real (∏p∈Pr2. Suc (multiplicity p n)) ≤ 2 powr (ln n / ln (f n))"
by simp
have multiplicity_le: "multiplicity p n ≤ log 2 n" if p: "p ∈ Pr" for p
proof -
from p have "2 ^ multiplicity p n ≤ p ^ multiplicity p n"
by (intro power_mono) (auto simp: in_prime_factors_iff dest: prime_gt_1_nat)
also have "… = (∏p∈{p}. p ^ multiplicity p n)" by simp
also from p have "(∏p∈{p}. p ^ multiplicity p n) ≤ (∏p∈Pr. p ^ multiplicity p n)"
by (intro dvd_imp_le prod_dvd_prod_subset)
(auto simp: in_prime_factors_iff dest: prime_gt_0_nat)
also have "… = n"
using n by (subst prime_factorization_nat[of n]) auto
finally have "2 ^ multiplicity p n ≤ n" .
hence "log 2 (2 ^ multiplicity p n) ≤ log 2 n"
using n by (subst log_le_cancel_iff) auto
thus "multiplicity p n ≤ log 2 n"
by (subst (asm) log_nat_power) auto
qed
have "(∏p∈Pr1. Suc (multiplicity p n)) = exp (∑p∈Pr1. ln (multiplicity p n + 1))"
by (simp add: exp_sum)
also have "(∑p∈Pr1. ln (multiplicity p n + 1)) ≤ (∑p∈Pr1. 2 * ln (ln n))"
proof (intro sum_mono)
fix p assume p: "p ∈ Pr1"
have "ln (multiplicity p n + 1) ≤ ln (1 + log 2 n)"
using p multiplicity_le[of p] by (subst ln_le_cancel_iff) auto
also have "… ≤ ln (ln n ^ 2)"
using ‹n > 2› ‹1 + log 2 n ≤ ln n ^ 2›
by (subst ln_le_cancel_iff) (auto intro: add_pos_nonneg)
also have "… = 2 * ln (ln n)"
using ‹n > 2› by (simp add: ln_realpow)
finally show "ln (multiplicity p n + 1) ≤ 2 * ln (ln n)" .
qed
also have "… = 2 * ln (ln n) * card Pr1"
by simp
also have "finite {p. prime p ∧ real p ≤ f n}"
by (rule finite_subset[of _ "{..nat ⌊f n⌋}"]) (auto simp: le_nat_iff le_floor_iff)
hence "card Pr1 ≤ card {p. prime p ∧ real p ≤ f n}"
by (intro card_mono) auto
also have "real … = π (f n)"
by (simp add: primes_pi_def prime_sum_upto_def)
also have "… < 4 * (f n / ln (f n))"
using ‹f n ≥ 2› by (intro π_upper_bound'') auto
also have "exp (2 * ln (ln (real n)) * (4 * (f n / ln (f n)))) =
2 powr (c * f n * ln (ln n) / ln (f n))"
by (simp add: powr_def c_def)
finally have bound1: "(∏p∈Pr1. Suc (multiplicity p n)) <
2 powr (c * f n * ln (ln (real n)) / ln (f n))"
using ‹ln (ln n) > 0› by (simp add: mult_strict_left_mono)
have "divisor_count n = (∏p∈Pr. Suc (multiplicity p n))"
using n by (subst divisor_count.prod_prime_factors') auto
also have "Pr = Pr1 ∪ Pr2" by auto
also have "real (∏p∈…. Suc (multiplicity p n)) =
real ((∏p∈Pr1. Suc (multiplicity p n)) * (∏p∈Pr2. Suc (multiplicity p n)))"
by (subst prod.union_disjoint) auto
also have "… < 2 powr (c * f n * ln (ln (real n)) / ln (f n)) * 2 powr (ln n / ln (f n))"
unfolding of_nat_mult
by (intro mult_less_le_imp_less bound1 bound2) (auto intro!: prod_nonneg prod_pos)
also have "… = 2 powr g n"
by (simp add: g_def add_divide_distrib powr_add)
finally show "real (divisor_count n) < 2 powr g n" .
qed
qed
text ‹
Now, Apostol explains that one can choose $f(n) := \ln n / (\ln\ln n) ^ 2$ to obtain
the desired bound.
›
proposition divisor_count_upper_bound:
fixes ε :: real
assumes "ε > 0"
shows "eventually (λn. divisor_count n < 2 powr ((1 + ε) * ln n / ln (ln n))) at_top"
proof -
define c :: real where "c = 8 / ln 2"
define f :: "nat ⇒ real" where "f = (λn. ln n / (ln (ln n)) ^ 2)"
define g where "g = (λn. (ln n + c * f n * ln (ln n)) / (ln (f n)))"
have "eventually (λn. divisor_count n < 2 powr g n) at_top"
unfolding g_def c_def f_def by (rule divisor_count_bound_gen) real_asymp+
moreover have "eventually (λn. 2 powr g n < 2 powr ((1 + ε) * ln n / ln (ln n))) at_top"
using ‹ε > 0› unfolding g_def c_def f_def by real_asymp
ultimately show "eventually (λn. divisor_count n < 2 powr ((1 + ε) * ln n / ln (ln n))) at_top"
by eventually_elim (rule less_trans)
qed
text ‹
Next, we will examine the `worst case'. Since any prime factor of ‹n› with multiplicity
‹k› contributes a factor of $k + 1$, it is intuitively clear that $\sigma_0(n)$ is
largest w.\,r.\,t.\ ‹n› if it is a product of small distinct primes.
We show that indeed, if $n := x\#$ (where $x\#$ denotes the primorial), we have
$\sigma_0(n) = 2^{\pi(x)}$, which, by the Prime Number Theorem, indeed
exceeds $c \ln n / \ln\ln n$.
›
theorem (in prime_number_theorem) divisor_count_primorial_gt:
assumes "ε > 0"
defines "h ≡ primorial"
shows "eventually (λx. divisor_count (h x) > 2 powr ((1 - ε) * ln (h x) / ln (ln (h x)))) at_top"
proof -
have "(λx. (1 - ε) * ln (h x) / ln (ln (h x))) ∼[at_top] (λx. (1 - ε) * θ x / ln (θ x))"
by (simp add: h_def ln_primorial)
also have "… ∼[at_top] (λx. (1 - ε) * x / ln x)"
by (intro asymp_equiv_intros θ_asymptotics ln_θ_asymp_equiv)
finally have *: "(λx. (1 - ε) * ln (h x) / ln (ln (h x))) ∼[at_top] (λx. (1 - ε) * x / ln x)"
by simp
have "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - (1 - ε) * x / ln x) ∈ o(λx. (1 - ε) * x / ln x)"
using asymp_equiv_imp_diff_smallo[OF *] by simp
also have "?this ⟷ (λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - x / ln x + ε * x / ln x)
∈ o(λx. (1 - ε) * x / ln x)"
by (intro landau_o.small.in_cong eventually_mono[OF eventually_gt_at_top[of 1]])
(auto simp: field_simps)
also have "(λx. (1 - ε) * x / ln x) ∈ O(λx. x / ln x)"
by real_asymp
finally have "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - x / ln x + ε * x / ln x)
∈ o(λx. x / ln x)" .
hence "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - x / ln x + ε * x / ln x - (π x - x / ln x))
∈ o(λx. x / ln x)"
by (intro sum_in_smallo[OF _ asymp_equiv_imp_diff_smallo] prime_number_theorem)
hence "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - π x + ε * (x / ln x)) ∈ o(λx. ε * (x / ln x))"
using ‹ε > 0› by (subst landau_o.small.cmult) (simp_all add: algebra_simps)
hence "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - π x) ∼[at_top] (λx. -ε * (x / ln x))"
by (intro smallo_imp_asymp_equiv) auto
hence "eventually (λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - π x < 0 ⟷
-ε * (x / ln x) < 0) at_top"
by (rule asymp_equiv_eventually_neg_iff)
moreover have "eventually (λx. -ε * (x / ln x) < 0) at_top"
using ‹ε > 0› by real_asymp
ultimately have "eventually (λx. (1 - ε) * ln (h x) / ln (ln (h x)) < π x) at_top"
by eventually_elim simp
thus "eventually (λx. divisor_count (h x) > 2 powr ((1 - ε) * ln (h x) / ln (ln (h x)))) at_top"
proof eventually_elim
case (elim x)
hence "2 powr ((1 - ε) * ln (h x) / ln (ln (h x))) < 2 powr π x"
by (intro powr_less_mono) auto
thus ?case by (simp add: divisor_count_primorial h_def)
qed
qed
text ‹
Since $h(x)\longrightarrow\infty$, this gives us our infinitely many values of ‹n›
that exceed the bound.
›
corollary (in prime_number_theorem) divisor_count_lower_bound:
assumes "ε > 0"
shows "frequently (λn. divisor_count n > 2 powr ((1 - ε) * ln n / ln (ln n))) at_top"
proof -
define h where "h = primorial"
have "eventually (λn. divisor_count n > 2 powr ((1 - ε) * ln n / ln (ln n)))
(filtermap h at_top)"
using divisor_count_primorial_gt[OF assms] by (simp add: eventually_filtermap h_def)
hence "frequently (λn. divisor_count n > 2 powr ((1 - ε) * ln n / ln (ln n)))
(filtermap h at_top)"
by (intro eventually_frequently) (auto simp: filtermap_bot_iff)
moreover from this and primorial_at_top
have "filtermap h at_top ≤ at_top" by (simp add: filterlim_def h_def)
ultimately show ?thesis
by (rule frequently_mono_filter)
qed
text ‹
A different formulation that is not quite as tedious to prove is this one:
›
lemma (in prime_number_theorem) ln_divisor_count_primorial'_asymp_equiv:
"(λk. ln (divisor_count (primorial' k))) ∼[at_top]
(λk. ln 2 * ln (primorial' k) / ln (ln (primorial' k)))"
proof -
have "(λk. ln 2 * (ln (primorial' k) / ln (ln (primorial' k)))) ∼[at_top] (λk. ln 2 * k)"
by (intro asymp_equiv_intros ln_over_ln_ln_primorial'_asymp_equiv)
also have "… ∼[at_top] (λk. ln (divisor_count (primorial' k)))"
by (simp add: ln_realpow mult_ac)
finally show ?thesis by (simp add: asymp_equiv_sym mult_ac)
qed
text ‹
It follows that the maximal order of the divisor function is $\ln 2 \cdot \ln n /\ln \ln n$.
›
theorem (in prime_number_theorem) limsup_divisor_count:
"limsup (λn. ln (divisor_count n) * ln (ln n) / ln n) = ln 2"
proof (intro antisym)
let ?h = "primorial'"
have "2 ^ k = (1 :: real) ⟷ k = 0" for k :: nat
using power_eq_1_iff[of "2::real" k] by auto
hence "(λk. ln (divisor_count (?h k)) / (ln 2 * ln (?h k) / ln (ln (?h k)))) ⇢ 1"
using ln_divisor_count_primorial'_asymp_equiv
by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]])
(auto simp: power_eq_1_iff)
hence "(λk. ln (divisor_count (?h k)) / (ln 2 * ln (?h k) / ln (ln (?h k))) * ln 2) ⇢ 1 * ln 2"
by (rule tendsto_mult) auto
hence "(λk. ln (divisor_count (?h k)) / (ln (?h k) / ln (ln (?h k)))) ⇢ ln 2"
by simp
hence "limsup ((λn. ln (divisor_count n) * ln (ln n) / ln n) ∘ primorial') = ereal (ln 2)"
by (intro lim_imp_Limsup tendsto_ereal) simp_all
hence "ln 2 = limsup ((λn. ereal (ln (divisor_count n) * ln (ln n) / ln n)) ∘ primorial')"
by (simp add: o_def)
also have "… ≤ limsup (λn. ln (divisor_count n) * ln (ln n) / ln n)"
using strict_mono_primorial' by (rule limsup_subseq_mono)
finally show "limsup (λn. ln (divisor_count n) * ln (ln n) / ln n) ≥ ln 2" .
next
show "limsup (λn. ln (divisor_count n) * ln (ln n) / ln n) ≤ ln 2"
unfolding Limsup_le_iff
proof safe
fix C' assume "C' > ereal (ln 2)"
from ereal_dense2[OF this] obtain C where C: "C > ln 2" "ereal C < C'" by auto
define ε where "ε = (C / ln 2) - 1"
from C have "ε > 0" by (simp add: ε_def)
have "eventually (λn::nat. ln (ln n) > 0) at_top" by real_asymp
hence "eventually (λn. ln (divisor_count n) * ln (ln n) / ln n < C) at_top"
using divisor_count_upper_bound[OF ‹ε > 0›] eventually_gt_at_top[of 1]
proof eventually_elim
case (elim n)
hence "ln (divisor_count n) < ln (2 powr ((1 + ε) * ln n / ln (ln n)))"
by (subst ln_less_cancel_iff) auto
also have "… = (1 + ε) * ln 2 * ln n / ln (ln n)"
by (simp add: ln_powr)
finally have "ln (divisor_count n) * ln (ln n) / ln n < (1 + ε) * ln 2"
using elim by (simp add: field_simps)
also have "… = C" by (simp add: ε_def)
finally show ?case .
qed
thus "eventually (λn. ereal (ln (divisor_count n) * ln (ln n) / ln n) < C') at_top"
by eventually_elim (rule less_trans[OF _ C(2)], auto)
qed
qed
subsection ‹Mertens' Third Theorem›
text ‹
In this section, we will show that
\[\prod_{p\leq x} \left(1 - \frac{1}{p}\right) =
\frac{C}{\ln x} + O\left(\frac{1}{\ln^2 x}\right)\]
with explicit bounds for the factor in the `Big-O'. Here, ‹C› is the following constant:
›
definition third_mertens_const :: real where
"third_mertens_const =
exp (-(∑p::nat. if prime p then -ln (1 - 1 / real p) - 1 / real p else 0) - meissel_mertens)"
text ‹
This constant is actually equal to $e^{-\gamma}$ where $\gamma$ is the Euler--Mascheroni
constant, but showing this is quite a bit of work, which we shall not do here.
›
lemma third_mertens_const_pos: "third_mertens_const > 0"
by (simp add: third_mertens_const_def)
theorem
defines "C ≡ third_mertens_const"
shows mertens_third_theorem_strong:
"eventually (λx. ¦(∏p | prime p ∧ real p ≤ x. 1 - 1 / p) - C / ln x¦ ≤
10 * C / ln x ^ 2) at_top"
and mertens_third_theorem:
"(λx. (∏p | prime p ∧ real p ≤ x. 1 - 1 / p) - C / ln x) ∈ O(λx. 1 / ln x ^ 2)"
proof -
define Pr where "Pr = (λx. {p. prime p ∧ real p ≤ x})"
define a :: "nat ⇒ real"
where "a = (λp. if prime p then -ln (1 - 1 / real p) - 1 / real p else 0)"
define B where "B = suminf a"
have C_eq: "C = exp (-B - meissel_mertens)"
by (simp add: B_def a_def third_mertens_const_def C_def)
have fin: "finite (Pr x)" for x
by (rule finite_subset[of _ "{..nat ⌊x⌋}"]) (auto simp: Pr_def le_nat_iff le_floor_iff)
define S where "S = (λx. (∑p∈Pr x. ln (1 - 1 / p)))"
define R where "R = (λx. S x + ln (ln x) + (B + meissel_mertens))"
have exp_S: "exp (S x) = (∏p∈Pr x. (1 - 1 / p))" for x
proof -
have "exp (S x) = (∏p∈Pr x. exp (ln (1 - 1 / p)))"
by (simp add: S_def exp_sum fin)
also have "… = (∏p∈Pr x. (1 - 1 / p))"
by (intro prod.cong) (auto simp: Pr_def dest: prime_gt_1_nat)
finally show ?thesis .
qed
have a_nonneg: "a n ≥ 0" for n
proof (cases "prime n")
case True
hence "ln (1 - 1 / n) ≤ -(1 / n)"
by (intro ln_one_minus_pos_upper_bound) (auto dest: prime_gt_1_nat)
thus ?thesis by (auto simp: a_def)
qed (auto simp: a_def)
have "summable a"
proof (rule summable_comparison_test_bigo)
have "a ∈ O(λn. -ln (1 - 1 / n) - 1 / n)"
by (intro bigoI[of _ 1]) (auto simp: a_def)
also have "(λn::nat. -ln (1 - 1 / n) - 1 / n) ∈ O(λn. 1 / n ^ 2)"
by real_asymp
finally show "a ∈ O(λn. 1 / real n ^ 2)" .
next
show "summable (λn. norm (1 / real n ^ 2))"
using inverse_power_summable[of 2] by (simp add: field_simps)
qed
have "eventually (λn. a n ≤ 1 / n - 1 / Suc n) at_top"
proof -
have "eventually (λn::nat. -ln (1 - 1 / n) - 1 / n ≤ 1 / n - 1 / Suc n) at_top"
by real_asymp
thus ?thesis using eventually_gt_at_top[of 1]
by eventually_elim (auto simp: a_def of_nat_diff field_simps)
qed
hence "eventually (λm. ∀n≥m. a n ≤ 1 / n - 1 / Suc n) at_top"
by (rule eventually_all_ge_at_top)
hence "eventually (λx. ∀n≥nat ⌊x⌋. a n ≤ 1 / n - 1 / Suc n) at_top"
by (rule eventually_compose_filterlim)
(intro filterlim_compose[OF filterlim_nat_sequentially] filterlim_floor_sequentially)
hence "eventually (λx. B - sum_upto a x ≤ 1 / x) at_top"
using eventually_ge_at_top[of "1::real"]
proof eventually_elim
case (elim x)
have a_le: "a n ≤ 1 / real n - 1 / real (Suc n)" if "real n ≥ x" for n
proof -
from that and ‹x ≥ 1› have "n ≥ nat ⌊x⌋" by linarith
with elim and that show ?thesis by auto
qed
define m where "m = Suc (nat ⌊x⌋)"
have telescope: "(λn. 1 / (n + m) - 1 / (Suc n + m)) sums (1 / real (0 + m) - 0)"
by (intro telescope_sums') real_asymp
have "B - (∑n<m. a n) = (∑n. a (n + m))"
unfolding B_def sum_upto_altdef m_def using ‹summable a›
by (subst suminf_split_initial_segment[of _ "Suc (nat ⌊x⌋)"]) auto
also have "(∑n<m. a n) = sum_upto a x"
unfolding m_def sum_upto_altdef by (intro sum.mono_neutral_right) (auto simp: a_def)
also have "(∑n. a (n + m)) ≤ (∑n. 1 / (n + m) - 1 / (Suc n + m))"
proof (intro suminf_le allI)
show "summable (λn. a (n + m))"
by (rule summable_ignore_initial_segment) fact+
next
show "summable (λn. 1 / (n + m) - 1 / (Suc n + m))"
using telescope by (rule sums_summable)
next
fix n :: nat
have "x ≤ n + m" unfolding m_def using ‹x ≥ 1› by linarith
thus "a (n + m) ≤ 1 / (n + m) - 1 / (Suc n + m)"
using a_le[of "n + m"] ‹x ≥ 1› by simp
qed
also have "… = 1 / m"
using telescope by (simp add: sums_iff)
also have "x ≤ m" "m > 0"
unfolding m_def using ‹x ≥ 1› by linarith+
hence "1 / m ≤ 1 / x"
using ‹x ≥ 1› by (intro divide_left_mono) (auto simp: m_def)
finally show ?case .
qed
moreover have "eventually (λx::real. 1 / x ≤ 1 / ln x) at_top" by real_asymp
ultimately have "eventually (λx. B - sum_upto a x ≤ 1 / ln x) at_top"
by eventually_elim (rule order.trans)
hence "eventually (λx. ¦R x¦ ≤ 5 / ln x) at_top"
using eventually_ge_at_top[of 2]
proof eventually_elim
case (elim x)
have "¦(B - sum_upto a x) - (prime_sum_upto (λp. 1 / p) x - ln (ln x) - meissel_mertens)¦ ≤
1 / ln x + 4 / ln x"
proof (intro order.trans[OF abs_triangle_ineq4 add_mono])
show "¦prime_sum_upto (λp. 1 / real p) x - ln (ln x) - meissel_mertens¦ ≤ 4 / ln x"
by (intro mertens_second_theorem ‹x ≥ 2›)
have "sum_upto a x ≤ B"
unfolding B_def sum_upto_def by (intro sum_le_suminf ‹summable a› a_nonneg ballI) auto
thus "¦B - sum_upto a x¦ ≤ 1 / ln x"
using elim by linarith
qed
also have "sum_upto a x = prime_sum_upto (λp. -ln (1 - 1 / p) - 1 / p) x"
unfolding sum_upto_def prime_sum_upto_altdef1 a_def by (intro sum.cong allI) auto
also have "… = -S x - prime_sum_upto (λp. 1 / p) x"
by (simp add: a_def S_def Pr_def prime_sum_upto_def sum_subtractf sum_negf)
finally show "¦R x¦ ≤ 5 / ln x"
by (simp add: R_def)
qed
moreover have "eventually (λx::real. ¦5 / ln x¦ < 1 / 2) at_top" by real_asymp
ultimately have "eventually (λx. exp (R x) - 1 ∈ {-5 / ln x..10 / ln x}) at_top"
using eventually_gt_at_top[of 1]
proof eventually_elim
case (elim x)
have "exp (R x) ≤ exp (5 / ln x)"
using elim by simp
also have "… ≤ 1 + 10 / ln x"
using real_exp_bound_lemma[of "5 / ln x"] elim by (simp add: abs_if split: if_splits)
finally have le: "exp (R x) ≤ 1 + 10 / ln x" .
have "1 + (-5 / ln x) ≤ exp (-5 / ln x)"
by (rule exp_ge_add_one_self)
also have "exp (-5 / ln x) ≤ exp (R x)"
using elim by simp
finally have "exp (R x) ≥ 1 - 5 / ln x" by simp
with le show ?case by simp
qed
thus "eventually (λx. ¦(∏p∈Pr x. 1 - 1 / real p) - C / ln x¦ ≤ 10 * C / ln x ^ 2) at_top"
using eventually_gt_at_top[of "exp 1"] eventually_gt_at_top[of 1]
proof eventually_elim
case (elim x)
have "¦exp (R x) - 1¦ ≤ 10 / ln x"
using elim by (simp add: abs_if)
from elim have "¦exp (S x) - C / ln x¦ = C / ln x * ¦exp (R x) - 1¦"
by (simp add: R_def exp_add C_eq exp_diff exp_minus field_simps)
also have "… ≤ C / ln x * (10 / ln x)"
using elim by (intro mult_left_mono) (auto simp: C_eq)
finally show ?case by (simp add: exp_S power2_eq_square mult_ac)
qed
thus "(λx. (∏p∈Pr x. 1 - 1 / real p) - C / ln x) ∈ O(λx. 1 / ln x ^ 2)"
by (intro bigoI[of _ "10 * C"]) auto
qed
lemma mertens_third_theorem_asymp_equiv:
"(λx. (∏p | prime p ∧ real p ≤ x. 1 - 1 / real p)) ∼[at_top]
(λx. third_mertens_const / ln x)"
by (rule smallo_imp_asymp_equiv[OF landau_o.big_small_trans[OF mertens_third_theorem]])
(use third_mertens_const_pos in real_asymp)
text ‹
We now show an equivalent version where $\prod_{p\leq x} (1 - 1 / p)$ is replaced
by $\prod_{i=1}^k (1 - 1 / p_i)$:
›
lemma mertens_third_convert:
assumes "n > 0"
shows "(∏k<n. 1 - 1 / real (nth_prime k)) =
(∏p | prime p ∧ p ≤ nth_prime (n - 1). 1 - 1 / p)"
proof -
have "primorial' n = primorial (nth_prime (n - 1))"
using assms by (simp add: primorial'_conv_primorial)
also have "real (totient …) =
primorial' n * (∏p | prime p ∧ p ≤ nth_prime (n - 1). 1 - 1 / p)"
using assms by (subst totient_primorial) (auto simp: primorial'_conv_primorial)
finally show ?thesis
by (simp add: totient_primorial')
qed
lemma (in prime_number_theorem) mertens_third_theorem_asymp_equiv':
"(λn. (∏k<n. 1 - 1 / nth_prime k)) ∼[at_top] (λx. third_mertens_const / ln x)"
proof -
have lim: "filterlim (λn. real (nth_prime (n - 1))) at_top at_top"
by (intro filterlim_compose[OF filterlim_real_sequentially]
filterlim_compose[OF nth_prime_at_top]) real_asymp
have "(λn. (∏k<n. 1 - 1 / nth_prime k)) ∼[at_top]
(λn. (∏p | prime p ∧ real p ≤ real (nth_prime (n - 1)). 1 - 1 / p))"
by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 0]])
(subst mertens_third_convert, auto)
also have "… ∼[at_top] (λn. third_mertens_const / ln (real (nth_prime (n - 1))))"
by (intro asymp_equiv_compose'[OF mertens_third_theorem_asymp_equiv lim])
also have "… ∼[at_top] (λn. third_mertens_const / ln (real (n - 1)))"
by (intro asymp_equiv_intros asymp_equiv_compose'[OF ln_nth_prime_asymp_equiv]) real_asymp
also have "… ∼[at_top] (λn. third_mertens_const / ln (real n))"
using third_mertens_const_pos by real_asymp
finally show ?thesis .
qed
subsection ‹Bounds on Euler's totient function›
text ‹
Similarly to the divisor function, we will show that $\varphi(n)$ has minimal order
$C n / \ln\ln n$.
The first part is to show the lower bound:
›
theorem totient_lower_bound:
fixes ε :: real
assumes "ε > 0"
defines "C ≡ third_mertens_const"
shows "eventually (λn. totient n > (1 - ε) * C * n / ln (ln n)) at_top"
proof -
include prime_counting_syntax
define f :: "nat ⇒ nat" where "f = (λn. card {p∈prime_factors n. p > ln n})"
define lb1 where "lb1 = (λn::nat. (∏p | prime p ∧ real p ≤ ln n. 1 - 1 / p))"
define lb2 where "lb2 = (λn::nat. (1 - 1 / ln n) powr (ln n / ln (ln n)))"
define lb1' where "lb1' = (λn::nat. C / ln (ln n) - 10 * C / ln (ln n) ^ 2)"
have "eventually (λn::nat. 1 + log 2 n ≤ ln n ^ 2) at_top" by real_asymp
hence "eventually (λn. totient n / n ≥ lb1 n * lb2 n) at_top"
using eventually_gt_at_top[of 2]
proof eventually_elim
fix n :: nat
assume n: "n > 2" and "1 + log 2 n ≤ ln n ^ 2"
define Pr where [simp]: "Pr = prime_factors n"
define Pr1 where [simp]: "Pr1 = {p∈Pr. p ≤ ln n}"
define Pr2 where [simp]: "Pr2 = {p∈Pr. p > ln n}"
have "exp 1 < real n"
using e_less_272 ‹n > 2› by linarith
hence "ln (exp 1) < ln (real n)"
using ‹n > 2› by (subst ln_less_cancel_iff) auto
hence "1 < ln n" by simp
hence "ln (ln n) > ln (ln (exp 1))"
by (subst ln_less_cancel_iff) auto
hence "ln (ln n) > 0" by simp
have "ln n ^ f n ≤ (∏p∈Pr2. ln n)"
by (simp add: f_def)
also have "… ≤ real (∏p∈Pr2. p)" unfolding of_nat_prod
by (intro prod_mono) (auto dest: prime_gt_1_nat simp: in_prime_factors_iff)
also {
have "(∏p∈Pr2. p) dvd (∏p∈Pr2. p ^ multiplicity p n)"
by (intro prod_dvd_prod dvd_power) (auto simp: prime_factors_multiplicity)
also have "… dvd (∏p∈Pr. p ^ multiplicity p n)"
by (intro prod_dvd_prod_subset2) auto
also have "… = n"
using ‹n > 2› by (subst (2) prime_factorization_nat[of n]) auto
finally have "(∏p∈Pr2. p) ≤ n"
using ‹n > 2› by (intro dvd_imp_le) auto
}
finally have "ln (ln n ^ f n) ≤ ln n"
using ‹n > 2› by (subst ln_le_cancel_iff) auto
also have "ln (ln n ^ f n) = f n * ln (ln n)"
using ‹n > 2› by (subst ln_realpow) auto
finally have f_le: "f n ≤ ln n / ln (ln n)"
using ‹ln (ln n) > 0› by (simp add: field_simps)
have "(1 - 1 / ln n) powr (ln n / ln (ln n)) ≤ (1 - 1 / ln n) powr (real (f n))"
using ‹n > 2› and ‹ln n > 1› by (intro powr_mono' f_le) auto
also have "… = (∏p∈Pr2. 1 - 1 / ln n)"
using ‹n > 2› and ‹ln n > 1› by (subst powr_realpow) (auto simp: f_def)
also have "… ≤ (∏p∈Pr2. 1 - 1 / p)"
using ‹n > 2› and ‹ln n > 1›
by (intro prod_mono conjI diff_mono divide_left_mono) (auto dest: prime_gt_1_nat)
finally have bound2: "(∏p∈Pr2. 1 - 1 / p) ≥ lb2 n" unfolding lb2_def .
have "(∏p | prime p ∧ real p ≤ ln n. inverse (1 - 1 / p)) ≥ (∏p∈Pr1. inverse (1 - 1 / p))"
using ‹n > 2› by (intro prod_mono2) (auto intro: finite_primes_le dest: prime_gt_1_nat simp: in_prime_factors_iff field_simps)
hence "inverse (∏p | prime p ∧ real p ≤ ln n. 1 - 1 / p) ≥ inverse (∏p∈Pr1. 1 - 1 / p)"
by (subst (1 2) prod_inversef [symmetric]) auto
hence bound1: "(∏p∈Pr1. 1 - 1 / p) ≥ lb1 n" unfolding lb1_def
by (rule inverse_le_imp_le)
(auto intro!: prod_pos simp: in_prime_factors_iff dest: prime_gt_1_nat)
have "lb1 n * lb2 n ≤ (∏p∈Pr1. 1 - 1 / p) * (∏p∈Pr2. 1 - 1 / p)"
by (intro mult_mono bound1 bound2 prod_nonneg ballI)
(auto simp: in_prime_factors_iff lb1_def lb2_def dest: prime_gt_1_nat)
also have "… = (∏p∈Pr1 ∪ Pr2. 1 - 1 / p)"
by (subst prod.union_disjoint) auto
also have "Pr1 ∪ Pr2 = Pr" by auto
also have "(∏p∈Pr. 1 - 1 / p) = totient n / n"
using n by (subst totient_formula2) auto
finally show "real (totient n) / real n ≥ lb1 n * lb2 n"
by (simp add: lb1_def lb2_def)
qed
moreover have "eventually (λn. ¦lb1 n - C / ln (ln n)¦ ≤ 10 * C / ln (ln n) ^ 2) at_top"
unfolding lb1_def C_def using mertens_third_theorem_strong
by (rule eventually_compose_filterlim) real_asymp
moreover have "eventually (λn. (1 - ε) * C / ln (ln n) < lb1' n * lb2 n) at_top"
unfolding lb1'_def lb2_def C_def using third_mertens_const_pos ‹ε > 0› by real_asymp
ultimately show "eventually (λn. totient n > (1 - ε) * C * n / ln (ln n)) at_top"
using eventually_gt_at_top[of 0]
proof eventually_elim
case (elim n)
have "(1 - ε) * C / ln (ln n) < lb1' n * lb2 n" by fact
also have "lb1' n ≤ lb1 n"
unfolding lb1'_def using elim by linarith
hence "lb1' n * lb2 n ≤ lb1 n * lb2 n"
by (intro mult_right_mono) (auto simp: lb2_def)
also have "… ≤ totient n / n" by fact
finally show "totient n > (1 - ε) * C * n / (ln (ln n))"
using ‹n > 0› by (simp add: field_simps)
qed
qed
text ‹
Next, we examine the `worst case' of $\varphi(n)$ where ‹n› is the primorial of $x$.
In this case, we have $\varphi(n) < c n / \ln\ln n$ for any $c > C$ for all sufficiently
large $n$.
›
theorem (in prime_number_theorem) totient_primorial_less:
fixes ε :: real
defines "C ≡ third_mertens_const" and "h ≡ primorial"
assumes "ε > 0"
shows "eventually (λx. totient (h x) < (1 + ε) * C * h x / ln (ln (h x))) at_top"
proof -
have "C > 0" by (simp add: C_def third_mertens_const_pos)
have "(λx. (1 + ε) * C / ln (ln (h x))) ∼[at_top] (λx. (1 + ε) * C / ln (θ x))"
by (simp add: ln_primorial h_def)
also have "… ∼[at_top] (λx. (1 + ε) * C / ln x)"
by (intro asymp_equiv_intros ln_θ_asymp_equiv)
finally have "(λx. (1 + ε) * C / ln (ln (h x)) - (1 + ε) * C / ln x) ∈ o(λx. (1 + ε) * C / ln x)"
by (rule asymp_equiv_imp_diff_smallo)
also have "(λx. (1 + ε) * C / ln x) ∈ O(λx. 1 / ln x)"
by real_asymp
also have "(λx. (1 + ε) * C / ln (ln (h x)) - (1 + ε) * C / ln x) =
(λx. (1 + ε) * C / ln (ln (h x)) - C / ln x - ε * C / ln x)"
by (simp add: algebra_simps fun_eq_iff add_divide_distrib)
finally have "(λx. (1 + ε) * C / ln (ln (h x)) - C / ln x - ε * C / ln x) ∈ o(λx. 1 / ln x)" .
hence "(λx. (1 + ε) * C / ln (ln (h x)) - C / ln x - ε * C / ln x -
((∏p∈{p. prime p ∧ real p ≤ x}. 1 - 1 / real p) - C / ln x)) ∈ o(λx. 1 / ln x)"
unfolding C_def
by (rule sum_in_smallo[OF _ landau_o.big_small_trans[OF mertens_third_theorem]]) real_asymp+
hence "(λx. ((1 + ε) * C / ln (ln (h x)) - (∏p∈{p. prime p ∧ real p ≤ x}. 1 - 1 / real p)) -
(ε * C / ln x)) ∈ o(λx. 1 / ln x)"
by (simp add: algebra_simps)
also have "(λx. 1 / ln x) ∈ O(λx. ε * C / ln x)"
using ‹ε > 0› by (simp add: landau_divide_simps C_def third_mertens_const_def)
finally have "(λx. (1 + ε) * C / ln (ln (h x)) - (∏p | prime p ∧ real p ≤ x. 1 - 1 / p))
∼[at_top] (λx. ε * C / ln x)"
by (rule smallo_imp_asymp_equiv)
hence "eventually (λx. (1 + ε) * C / ln (ln (h x)) - (∏p | prime p ∧ real p ≤ x. 1 - 1 / p) > 0
⟷ ε * C / ln x > 0) at_top"
by (rule asymp_equiv_eventually_pos_iff)
moreover have "eventually (λx. ε * C / ln x > 0) at_top"
using ‹ε > 0› ‹C > 0› by real_asymp
ultimately have "eventually (λx. (1 + ε) * C / ln (ln (h x)) >
(∏p | prime p ∧ real p ≤ x. 1 - 1 / p)) at_top"
by eventually_elim auto
thus ?thesis
proof eventually_elim
case (elim x)
have "h x > 0" by (auto simp: h_def primorial_def intro!: prod_pos dest: prime_gt_0_nat)
have "h x * ((1 + ε) * C / ln (ln (h x))) > totient (h x)"
using elim primorial_pos[of x] unfolding h_def totient_primorial
by (intro mult_strict_left_mono) auto
thus ?case by (simp add: mult_ac)
qed
qed
text ‹
It follows that infinitely many values of ‹n› exceed $c n / \ln (\ln n)$ when ‹c› is chosen
larger than ‹C›.
›
corollary (in prime_number_theorem) totient_upper_bound:
assumes "ε > 0"
defines "C ≡ third_mertens_const"
shows "frequently (λn. totient n < (1 + ε) * C * n / ln (ln n)) at_top"
proof -
define h where "h = primorial"
have "eventually (λn. totient n < (1 + ε) * C * n / ln (ln n)) (filtermap h at_top)"
using totient_primorial_less[OF assms(1)] by (simp add: eventually_filtermap C_def h_def)
hence "frequently (λn. totient n < (1 + ε) * C * n / ln (ln n)) (filtermap h at_top)"
by (intro eventually_frequently) (auto simp: filtermap_bot_iff)
moreover from this and primorial_at_top
have "filtermap h at_top ≤ at_top" by (simp add: filterlim_def h_def)
ultimately show ?thesis
by (rule frequently_mono_filter)
qed
text ‹
Again, the following alternative formulation is somewhat nicer to prove:
›
lemma (in prime_number_theorem) totient_primorial'_asymp_equiv:
"(λk. totient (primorial' k)) ∼[at_top] (λk. third_mertens_const * primorial' k / ln k)"
proof -
let ?C = third_mertens_const
have "(λk. totient (primorial' k)) ∼[at_top] (λk. primorial' k * (∏i<k. 1 - 1 / nth_prime i))"
by (subst totient_primorial') auto
also have "… ∼[at_top] (λk. primorial' k * (?C / ln k))"
by (intro asymp_equiv_intros mertens_third_theorem_asymp_equiv')
finally show ?thesis by (simp add: algebra_simps)
qed
lemma (in prime_number_theorem) totient_primorial'_asymp_equiv':
"(λk. totient (primorial' k)) ∼[at_top]
(λk. third_mertens_const * primorial' k / ln (ln (primorial' k)))"
proof -
let ?C = third_mertens_const
have "(λk. totient (primorial' k)) ∼[at_top] (λk. third_mertens_const * primorial' k / ln k)"
by (rule totient_primorial'_asymp_equiv)
also have "… ∼[at_top] (λk. third_mertens_const * primorial' k / ln (ln (primorial' k)))"
by (intro asymp_equiv_intros asymp_equiv_symI[OF ln_ln_primorial'_asymp_equiv])
finally show ?thesis .
qed
text ‹
All in all, $\varphi(n)$ has minimal order $cn / \ln\ln n$:
›
theorem (in prime_number_theorem)
liminf_totient: "liminf (λn. totient n * ln (ln n) / n) = third_mertens_const"
(is "_ = ereal ?c")
proof (intro antisym)
have "(λk. totient (primorial' k) / (?c * primorial' k / ln (ln (primorial' k)))) ⇢ 1"
using totient_primorial'_asymp_equiv'
by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]]) auto
hence "(λk. totient (primorial' k) / (?c * primorial' k / ln (ln (primorial' k))) * ?c)
⇢ 1 * ?c" by (intro tendsto_mult) auto
hence "(λk. totient (primorial' k) / (primorial' k / ln (ln (primorial' k)))) ⇢ ?c"
using third_mertens_const_pos by simp
hence "liminf ((λn. totient n * ln (ln n) / n) ∘ primorial') = ereal ?c"
by (intro lim_imp_Liminf tendsto_ereal) simp_all
hence "?c = liminf ((λn. ereal (totient n * ln (ln n) / n)) ∘ primorial')"
by (simp add: o_def)
also have "… ≥ liminf (λn. totient n * ln (ln n) / n)"
using strict_mono_primorial' by (rule liminf_subseq_mono)
finally show "liminf (λn. totient n * ln (ln n) / n) ≤ ?c" .
next
show "liminf (λn. totient n * ln (ln n) / n) ≥ ?c"
unfolding le_Liminf_iff
proof safe
fix C' assume "C' < ereal ?c"
from ereal_dense2[OF this] obtain C where C: "C < ?c" "ereal C > C'" by auto
define ε where "ε = 1 - C / ?c"
from C have "ε > 0" using third_mertens_const_pos by (simp add: ε_def)
have "eventually (λn::nat. ln (ln n) > 0) at_top" by real_asymp
hence "eventually (λn. totient n * ln (ln n) / n > C) at_top"
using totient_lower_bound[OF ‹ε > 0›] eventually_gt_at_top[of 1]
proof eventually_elim
case (elim n)
hence "totient n * ln (ln n) / n > (1 - ε) * ?c"
by (simp add: field_simps)
also have "(1 - ε) * ?c = C"
using third_mertens_const_pos by (simp add: field_simps ε_def)
finally show ?case .
qed
thus "eventually (λn. ereal (totient n * ln (ln n) / n) > C') at_top"
by eventually_elim (rule less_trans[OF C(2)], auto)
qed
qed
unbundle no prime_counting_syntax
end