(* 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: "∃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 - ― ‹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" "∀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 ― ‹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 "∃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 ― ‹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. ∀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› (* 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 "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 (* 4.9 *) 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 (* 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