# Theory Shapiro_Tauberian

(*
File:    Shapiro_Tauberian.thy
Author:  Manuel Eberl, TU München

Shapiro's Tauberian theorem
(see Section 4.6 of Apostol's Introduction to Analytic Number Theory)
*)
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: "c0. x0. x * A x - T x  {0..c*x}"
and asymptotics:       "(λx. A x - ln x)  O(λ_. 1)"
and upper:             "c0. x0. S x  c * x"
and lower:             "c>0. x1/c. S x  c * x"
and bigtheta:          "S  Θ(λx. x)"
proof -
― ‹We first prove the third case, i.\,e.\ the upper bound for S›.›
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" "n1. ¦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 "c0. x0. S x  c * x" by auto

― ‹The asymptotics of A› follows from this immediately:›
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 "c0. x0. 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

― ‹It remains to show the lower bound for S›.›
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. x1/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›

(* 3.16 *)
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 -
― ‹This is a perhaps somewhat roundabout way of proving this statement. We show this using
the asymptotics of 𝔐›: $\mathfrak{M}(x) = \ln x + O(1)$

We proved this before (which was a bit of work, but not that much).
Apostol, on the other hand, shows the following statement first and then deduces the
asymptotics of 𝔐› with Shapiro's Tauberian theorem instead. This might save a bit of
work, but it is probably negligible.›
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
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

(* 4.9 *)
interpretation ψ: shapiro_tauberian mangoldt "sum_upto (λn. mangoldt n / n)" primes_psi

proof unfold_locales
have
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

(* 4.10 *)
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

(* 4.11 *)
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