Theory Shapiro_Tauberian
section ‹Shapiro's Tauberian Theorem›
theory Shapiro_Tauberian
imports
More_Dirichlet_Misc
Prime_Number_Theorem.Prime_Counting_Functions
Prime_Distribution_Elementary_Library
begin
subsection ‹Proof›
text ‹
Given an arithmeticla function $a(n)$, Shapiro's Tauberian theorem relates the sum
$\sum_{n\leq x} a(n)$ to the weighted sums $\sum_{n\leq x} a(n) \lfloor\frac{x}{n}\rfloor$
and $\sum_{n\leq x} a(n)/n$.
More precisely, it shows that if $\sum_{n\leq x} a(n) \lfloor\frac{x}{n}\rfloor = x\ln x + O(x)$,
then:
▪ $\sum_{n\leq x} \frac{a(n)}{n} = \ln x + O(1)$
▪ $\sum_{n\leq x} a(n) \leq Bx$ for some constant $B\geq 0$ and all $x\geq 0$
▪ $\sum_{n\leq x} a(n) \geq Cx$ for some constant $C>0$ and all $x\geq 1/C$
›
locale shapiro_tauberian =
fixes a :: "nat ⇒ real" and A S T :: "real ⇒ real"
defines "A ≡ sum_upto (λn. a n / n)"
defines "S ≡ sum_upto a"
defines "T ≡ (λx. dirichlet_prod' a floor x)"
assumes a_nonneg: "⋀n. n > 0 ⟹ a n ≥ 0"
assumes a_asymptotics: "(λx. T x - x * ln x) ∈ O(λx. x)"
begin
lemma fin: "finite X" if "X ⊆ {n. real n ≤ x}" for X x
by (rule finite_subset[of _ "{..nat ⌊x⌋}"]) (use that in ‹auto simp: le_nat_iff le_floor_iff›)
lemma S_mono: "S x ≤ S y" if "x ≤ y" for x y
unfolding S_def sum_upto_def using that by (intro sum_mono2 fin[of _ y] a_nonneg) auto
lemma split:
fixes f :: "nat ⇒ real"
assumes "α ∈ {0..1}"
shows "sum_upto f x = sum_upto f (α*x) + (∑n | n > 0 ∧ real n ∈ {α*x<..x}. f n)"
proof (cases "x > 0")
case False
hence *: "{n. n > 0 ∧ real n ≤ x} = {}" "{n. n > 0 ∧ real n ∈ {α*x<..x}} = {}"
using mult_right_mono[of α 1 x] assms by auto
have "α * x ≤ 0"
using False assms by (intro mult_nonneg_nonpos) auto
hence **: "{n. n > 0 ∧ real n ≤ α * x} = {}"
by auto
show ?thesis
unfolding sum_upto_def * ** by auto
next
case True
have "sum_upto f x = (∑n | n > 0 ∧ real n ≤ x. f n)"
by (simp add: sum_upto_def)
also have "{n. n > 0 ∧ real n ≤ x} =
{n. n > 0 ∧ real n ≤ α*x} ∪ {n. n > 0 ∧ real n ∈ {α*x<..x}}"
using assms True mult_right_mono[of α 1 x] by (force intro: order_trans)
also have "(∑n∈…. f n) = sum_upto f (α*x) + (∑n | n > 0 ∧ real n ∈ {α*x<..x}. f n)"
by (subst sum.union_disjoint) (auto intro: fin simp: sum_upto_def)
finally show ?thesis .
qed
lemma S_diff_T_diff: "S x - S (x / 2) ≤ T x - 2 * T (x / 2)"
proof -
note fin = fin[of _ x]
have T_diff_eq:
"T x - 2 * T (x / 2) = sum_upto (λn. a n * (⌊x / n⌋ - 2 * ⌊x / (2 * n)⌋)) (x / 2) +
(∑n | n > 0 ∧ real n ∈ {x/2<..x}. a n * ⌊x / n⌋)"
unfolding T_def dirichlet_prod'_def
by (subst split[where α = "1/2"])
(simp_all add: sum_upto_def sum_subtractf ring_distribs
sum_distrib_left sum_distrib_right mult_ac)
have "S x - S (x / 2) = (∑n | n > 0 ∧ real n ∈ {x/2<..x}. a n)"
unfolding S_def by (subst split[where α = "1 / 2"]) (auto simp: sum_upto_def)
also have "… = (∑n | n > 0 ∧ real n ∈ {x/2<..x}. a n * ⌊x / n⌋)"
proof (intro sum.cong)
fix n assume "n ∈ {n. n > 0 ∧ real n ∈ {x/2<..x}}"
hence "x / n ≥ 1" "x / n < 2" by (auto simp: field_simps)
hence "⌊x / n⌋ = 1" by linarith
thus "a n = a n * ⌊x / n⌋" by simp
qed auto
also have "… = 0 + …" by simp
also have "0 ≤ sum_upto (λn. a n * (⌊x / n⌋ - 2 * ⌊x / (2 * n)⌋)) (x / 2)"
unfolding sum_upto_def
proof (intro sum_nonneg mult_nonneg_nonneg a_nonneg)
fix n assume "n ∈ {n. n > 0 ∧ real n ≤ x / 2}"
hence "x / real n ≥ 2" by (auto simp: field_simps)
thus "real_of_int (⌊x / n⌋ - 2 * ⌊x / (2 * n)⌋) ≥ 0"
using le_mult_floor[of 2 "x / (2 * n)"] by (simp add: mult_ac)
qed auto
also have "… + (∑n | n > 0 ∧ real n ∈ {x/2<..x}. a n * ⌊x / n⌋) = T x - 2 * T (x / 2)"
using T_diff_eq ..
finally show "S x - S (x / 2) ≤ T x - 2 * T (x / 2)" by simp
qed
lemma
shows diff_bound_strong: "∃c≥0. ∀x≥0. x * A x - T x ∈ {0..c*x}"
and asymptotics: "(λx. A x - ln x) ∈ O(λ_. 1)"
and upper: "∃c≥0. ∀x≥0. S x ≤ c * x"
and lower: "∃c>0. ∀x≥1/c. S x ≥ c * x"
and bigtheta: "S ∈ Θ(λx. x)"
proof -
have "(λx. S x - S (x / 2)) ∈ O(λx. T x - 2 * T (x / 2))"
proof (rule le_imp_bigo_real)
show "eventually (λx. S x - S (x / 2) ≥ 0) at_top"
using eventually_ge_at_top[of 0]
proof eventually_elim
case (elim x)
thus ?case using S_mono[of "x / 2" x] by simp
qed
next
show "eventually (λx. S x - S (x / 2) ≤ 1 * (T x - 2 * T (x / 2))) at_top"
using S_diff_T_diff by simp
qed auto
also have "(λx. T x - 2 * T (x / 2)) ∈ O(λx. x)"
proof -
have "(λx. T x - 2 * T (x / 2)) =
(λx. (T x - x * ln x) - 2 * (T (x / 2) - (x / 2) * ln (x / 2))
+ x * (ln x - ln (x / 2)))" by (simp add: algebra_simps)
also have "… ∈ O(λx. x)"
proof (rule sum_in_bigo, rule sum_in_bigo)
show "(λx. T x - x * ln x) ∈ O(λx. x)" by (rule a_asymptotics)
next
have "(λx. T (x / 2) - (x / 2) * ln (x / 2)) ∈ O(λx. x / 2)"
using a_asymptotics by (rule landau_o.big.compose) real_asymp+
thus "(λx. 2 * (T (x / 2) - x / 2 * ln (x / 2))) ∈ O(λx. x)"
unfolding cmult_in_bigo_iff by (subst (asm) landau_o.big.cdiv) auto
qed real_asymp+
finally show ?thesis .
qed
finally have S_diff_bigo: "(λx. S x - S (x / 2)) ∈ O(λx. x)" .
obtain c1 where c1: "c1 ≥ 0" "⋀x. x ≥ 0 ⟹ S x ≤ c1 * x"
proof -
from S_diff_bigo have "(λn. S (real n) - S (real n / 2)) ∈ O(λn. real n)"
by (rule landau_o.big.compose) real_asymp
from natfun_bigoE[OF this, of 1] obtain c
where "c > 0" "∀n≥1. ¦S (real n) - S (real n / 2)¦ ≤ c * real n" by auto
hence c: "S (real n) - S (real n / 2) ≤ c * real n" if "n ≥ 1" for n
using S_mono[of "real n" "2 * real n"] that by auto
have c_twopow: "S (2 ^ Suc n / 2) - S (2 ^ n / 2) ≤ c * 2 ^ n" for n
using c[of "2 ^ n"] by simp
have S_twopow_le: "S (2 ^ k) ≤ 2 * c * 2 ^ k" for k
proof -
have [simp]: "{0<..Suc 0} = {1}" by auto
have "(∑r<Suc k. S (2 ^ Suc r / 2) - S (2 ^ r / 2)) ≤ (∑r<Suc k. c * 2 ^ r)"
by (intro sum_mono c_twopow)
also have "(∑r<Suc k. S (2 ^ Suc r / 2) - S (2 ^ r / 2)) = S (2 ^ k)"
by (subst sum_lessThan_telescope) (auto simp: S_def sum_upto_altdef)
also have "(∑r<Suc k. c * 2 ^ r) = c * (∑r<Suc k. 2 ^ r)"
unfolding sum_distrib_left ..
also have "(∑r<Suc k. 2 ^ r :: real) = 2^Suc k - 1"
by (subst geometric_sum) auto
also have "c * … ≤ c * 2 ^ Suc k"
using ‹c > 0› by (intro mult_left_mono) auto
finally show "S (2 ^ k) ≤ 2 * c * 2 ^ k" by simp
qed
have S_le: "S x ≤ 4 * c * x" if "x ≥ 0" for x
proof (cases "x ≥ 1")
case False
with that have "x ∈ {0..<1}" by auto
thus ?thesis using ‹c > 0› by (auto simp: S_def sum_upto_altdef)
next
case True
hence x: "x ≥ 1" by simp
define n where "n = nat ⌊log 2 x⌋"
have "2 powr real n ≤ 2 powr (log 2 x)"
unfolding n_def using x by (intro powr_mono) auto
hence ge: "2 ^ n ≤ x" using x by (subst (asm) powr_realpow) auto
have "2 powr real (Suc n) > 2 powr (log 2 x)"
unfolding n_def using x by (intro powr_less_mono) linarith+
hence less: "2 ^ (Suc n) > x" using x by (subst (asm) powr_realpow) auto
have "S x ≤ S (2 ^ Suc n)"
using less by (intro S_mono) auto
also have "… ≤ 2 * c * 2 ^ Suc n"
by (intro S_twopow_le)
also have "… = 4 * c * 2 ^ n"
by simp
also have "… ≤ 4 * c * x"
by (intro mult_left_mono ge) (use x ‹c > 0› in auto)
finally show "S x ≤ 4 * c * x" .
qed
with that[of "4 * c"] and ‹c > 0› show ?thesis by auto
qed
thus "∃c≥0. ∀x≥0. S x ≤ c * x" by auto
have a_strong: "x * A x - T x ∈ {0..c1 * x}" if x: "x ≥ 0" for x
proof -
have "sum_upto (λn. a n * frac (x / n)) x ≤ sum_upto (λn. a n * 1) x" unfolding sum_upto_def
by (intro sum_mono mult_left_mono a_nonneg) (auto intro: less_imp_le frac_lt_1)
also have "… = S x" unfolding S_def by simp
also from x have "… ≤ c1 * x" by (rule c1)
finally have "sum_upto (λn. a n * frac (x / n)) x ≤ c1 * x" .
moreover have "sum_upto (λn. a n * frac (x / n)) x ≥ 0"
unfolding sum_upto_def by (intro sum_nonneg mult_nonneg_nonneg a_nonneg) auto
ultimately have "sum_upto (λn. a n * frac (x / n)) x ∈ {0..c1*x}" by auto
also have "sum_upto (λn. a n * frac (x / n)) x = x * A x - T x"
by (simp add: T_def A_def sum_upto_def sum_subtractf frac_def algebra_simps
sum_distrib_left sum_distrib_right dirichlet_prod'_def)
finally show ?thesis .
qed
thus "∃c≥0. ∀x≥0. x * A x - T x ∈ {0..c*x}"
using ‹c1 ≥ 0› by (intro exI[of _ c1]) auto
hence "(λx. x * A x - T x) ∈ O(λx. x)"
using a_strong ‹c1 ≥ 0›
by (intro le_imp_bigo_real[of c1] eventually_mono[OF eventually_ge_at_top[of 1]]) auto
from this and a_asymptotics have "(λx. (x * A x - T x) + (T x - x * ln x)) ∈ O(λx. x)"
by (rule sum_in_bigo)
hence "(λx. x * (A x - ln x)) ∈ O(λx. x * 1)"
by (simp add: algebra_simps)
thus bigo: "(λx. A x - ln x) ∈ O(λx. 1)"
by (subst (asm) landau_o.big.mult_cancel_left) auto
define R where "R = (λx. A x - ln x)"
obtain M where M: "⋀x. x ≥ 1 ⟹ ¦R x¦ ≤ M"
proof -
have "(λn. R (real n)) ∈ O(λ_. 1)"
using bigo unfolding R_def by (rule landau_o.big.compose) real_asymp
from natfun_bigoE[OF this, of 0] obtain M where M: "M > 0" "⋀n. ¦R (real n)¦ ≤ M"
by auto
have "¦R x¦ ≤ M + ln 2" if x: "x ≥ 1" for x
proof -
define n where "n = nat ⌊x⌋"
have "¦R x - R (real n)¦ = ln (x / n)"
using x by (simp add: R_def A_def sum_upto_altdef n_def ln_div)
also {
have "x ≤ real n + 1"
unfolding n_def by linarith
also have "1 ≤ real n"
using x unfolding n_def by simp
finally have "ln (x / n) ≤ ln 2"
using x by (simp add: field_simps)
}
finally have "¦R x¦ ≤ ¦R (real n)¦ + ln 2"
by linarith
also have "¦R (real n)¦ ≤ M"
by (rule M)
finally show "¦R x¦ ≤ M + ln 2" by simp
qed
with that[of "M + ln 2"] show ?thesis by blast
qed
have "M ≥ 0" using M[of 1] by simp
have A_diff_ge: "A x - A (α*x) ≥ -ln α - 2 * M"
if α: "α ∈ {0<..<1}" and "x ≥ 1 / α" for x α :: real
proof -
from that have "1 < inverse α * 1" by (simp add: field_simps)
also have "… ≤ inverse α * (α * x)"
using ‹x ≥ 1 / α› and α by (intro mult_left_mono) (auto simp: field_simps)
also from α have "… = x" by simp
finally have "x > 1" .
note x = this ‹x >= 1 / α›
have "-ln α - M - M ≤ -ln α - ¦R x¦ - ¦R (α*x)¦"
using x α by (intro diff_mono M) (auto simp: field_simps)
also have "… ≤ -ln α + R x - R (α*x)"
by linarith
also have "… = A x - A (α*x)"
using α x by (simp add: R_def ln_mult)
finally show "A x - A (α*x) ≥ -ln α - 2 * M" by simp
qed
define α where "α = exp (-2*M-1)"
have "α ∈ {0<..<1}"
using ‹M ≥ 0› by (auto simp: α_def)
have S_ge: "S x ≥ α * x" if x: "x ≥ 1 / α" for x
proof -
have "1 = -ln α - 2 * M"
by (simp add: α_def)
also have "… ≤ A x - A (α*x)"
by (intro A_diff_ge) fact+
also have "… = (∑n | n > 0 ∧ real n ∈ {α*x<..x}. a n / n)"
unfolding A_def using ‹α ∈ {0<..<1}› by (subst split[where α = α]) auto
also have "… ≤ (∑n | n > 0 ∧ real n ∈ {α*x<..x}. a n / (α*x))"
using x ‹α ∈ {0<..<1}› by (intro sum_mono divide_left_mono a_nonneg) auto
also have "… = (∑n | n > 0 ∧ real n ∈ {α*x<..x}. a n) / (α*x)"
by (simp add: sum_divide_distrib)
also have "… ≤ S x / (α*x)"
using x ‹α ∈ {0<..<1}› unfolding S_def sum_upto_def
by (intro divide_right_mono sum_mono2 a_nonneg) (auto simp: field_simps)
finally show "S x ≥ α * x"
using ‹α ∈ {0<..<1}› x by (simp add: field_simps)
qed
thus "∃c>0. ∀x≥1/c. S x ≥ c * x"
using ‹α ∈ {0<..<1}› by (intro exI[of _ α]) auto
have S_nonneg: "S x ≥ 0" for x
unfolding S_def sum_upto_def by (intro sum_nonneg a_nonneg) auto
have "eventually (λx. ¦S x¦ ≥ α * ¦x¦) at_top"
using eventually_ge_at_top[of "max 0 (1 / α)"]
proof eventually_elim
case (elim x)
with S_ge[of x] elim show ?case by auto
qed
hence "S ∈ Ω(λx. x)"
using ‹α ∈ {0<..<1}› by (intro landau_omega.bigI[of α]) auto
moreover have "S ∈ O(λx. x)"
proof (intro bigoI eventually_mono[OF eventually_ge_at_top[of 0]])
fix x :: real assume "x ≥ 0"
thus "norm (S x) ≤ c1 * norm x"
using c1(2)[of x] by (auto simp: S_nonneg)
qed
ultimately show "S ∈ Θ(λx. x)"
by (intro bigthetaI)
qed
end
subsection ‹Applications to the Chebyshev functions›
text ‹
We can now apply Shapiro's Tauberian theorem to \<^term>‹ψ› and \<^term>‹θ›.
›
lemma dirichlet_prod_mangoldt1_floor_bigo:
includes prime_counting_notation
shows "(λx. dirichlet_prod' (λn. ind prime n * ln n) floor x - x * ln x) ∈ O(λx. x)"
proof -
define R where "R = (λx. sum_upto (λi. ind prime i * ln i * frac (x / i)) x)"
have *: "R x ∈ {0..ln 4 * x}" if "x ≥ 1" for x
proof -
have "R x ≤ θ x"
unfolding R_def prime_sum_upto_altdef1 sum_upto_def θ_def
by (intro sum_mono) (auto simp: ind_def less_imp_le[OF frac_lt_1] dest!: prime_gt_1_nat)
also have "… < ln 4 * x"
by (rule θ_upper_bound) fact+
finally have "R x ≤ ln 4 * x" by auto
moreover have "R x ≥ 0" unfolding R_def sum_upto_def
by (intro sum_nonneg mult_nonneg_nonneg) (auto simp: ind_def)
ultimately show ?thesis by auto
qed
have "eventually (λx. ¦R x¦ ≤ ln 4 * ¦x¦) at_top"
using eventually_ge_at_top[of 1] by eventually_elim (use * in auto)
hence "R ∈ O(λx. x)" by (intro landau_o.bigI[of "ln 4"]) auto
have "(λx. dirichlet_prod' (λn. ind prime n * ln n) floor x - x * ln x) =
(λx. x * (𝔐 x - ln x) - R x)"
by (auto simp: primes_M_def dirichlet_prod'_def prime_sum_upto_altdef1 sum_upto_def
frac_def sum_subtractf sum_distrib_left sum_distrib_right algebra_simps R_def)
also have "… ∈ O(λx. x)"
proof (rule sum_in_bigo)
have "(λx. x * (𝔐 x - ln x)) ∈ O(λx. x * 1)"
by (intro landau_o.big.mult mertens_bounded) auto
thus "(λx. x * (𝔐 x - ln x)) ∈ O(λx. x)" by simp
qed fact+
finally show ?thesis .
qed
lemma dirichlet_prod'_mangoldt_floor_asymptotics:
"(λx. dirichlet_prod' mangoldt floor x - x * ln x + x) ∈ O(ln)"
proof -
have "dirichlet_prod' mangoldt floor = (λx. sum_upto ln x)"
unfolding sum_upto_ln_conv_sum_upto_mangoldt dirichlet_prod'_def
by (intro sum_upto_cong' ext) auto
hence "(λx. dirichlet_prod' mangoldt floor x - x * ln x + x) = (λx. sum_upto ln x - x * ln x + x)"
by simp
also have "… ∈ O(ln)"
by (rule sum_upto_ln_stirling_weak_bigo)
finally show "(λx. dirichlet_prod' mangoldt (λx. real_of_int ⌊x⌋) x - x * ln x + x) ∈ O(ln)" .
qed
interpretation ψ: shapiro_tauberian mangoldt "sum_upto (λn. mangoldt n / n)" primes_psi
"dirichlet_prod' mangoldt floor"
proof unfold_locales
have "dirichlet_prod' mangoldt floor = (λx. sum_upto ln x)"
unfolding sum_upto_ln_conv_sum_upto_mangoldt dirichlet_prod'_def
by (intro sum_upto_cong' ext) auto
hence "(λx. dirichlet_prod' mangoldt floor x - x * ln x + x) = (λx. sum_upto ln x - x * ln x + x)"
by simp
also have "… ∈ O(ln)"
by (rule sum_upto_ln_stirling_weak_bigo)
also have "ln ∈ O(λx::real. x)" by real_asymp
finally have "(λx. dirichlet_prod' mangoldt (λx. real_of_int ⌊x⌋) x - x * ln x + x - x)
∈ O(λx. x)" by (rule sum_in_bigo) auto
thus "(λx. dirichlet_prod' mangoldt (λx. real_of_int ⌊x⌋) x - x * ln x) ∈ O(λx. x)" by simp
qed (simp_all add: primes_psi_def mangoldt_nonneg)
thm ψ.asymptotics ψ.upper ψ.lower
interpretation θ: shapiro_tauberian "λn. ind prime n * ln n"
"sum_upto (λn. ind prime n * ln n / n)" primes_theta "dirichlet_prod' (λn. ind prime n * ln n) floor"
proof unfold_locales
fix n :: nat show "ind prime n * ln n ≥ 0"
by (auto simp: ind_def dest: prime_gt_1_nat)
next
show "(λx. dirichlet_prod' (λn. ind prime n * ln n) floor x - x * ln x) ∈ O(λx. x)"
by (rule dirichlet_prod_mangoldt1_floor_bigo)
qed (simp_all add: primes_theta_def mangoldt_nonneg prime_sum_upto_altdef1[abs_def])
thm θ.asymptotics θ.upper θ.lower
lemma sum_upto_ψ_x_over_n_asymptotics:
"(λx. sum_upto (λn. primes_psi (x / n)) x - x * ln x + x) ∈ O(ln)"
and sum_upto_θ_x_over_n_asymptotics:
"(λx. sum_upto (λn. primes_theta (x / n)) x - x * ln x) ∈ O(λx. x)"
using dirichlet_prod_mangoldt1_floor_bigo dirichlet_prod'_mangoldt_floor_asymptotics
by (simp_all add: dirichlet_prod'_floor_conv_sum_upto primes_theta_def
primes_psi_def prime_sum_upto_altdef1)
end