Theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
section ‹Bounds on partial sums of the $\zeta$ function›
theory Partial_Zeta_Bounds
imports
Euler_MacLaurin.Euler_MacLaurin_Landau
Zeta_Function.Zeta_Function
Prime_Number_Theorem.Prime_Number_Theorem_Library
Prime_Distribution_Elementary_Library
begin
text ‹
We employ Euler--MacLaurin's summation formula to obtain asymptotic estimates
for the partial sums of the Riemann $\zeta(s)$ function for fixed real $a$, i.\,e.\ the function
\[f(n) = \sum_{k=1}^n k^{-s}\ .\]
We distinguish various cases. The case $s = 1$ is simply the Harmonic numbers and is
treated apart from the others.
›
lemma harm_asymp_equiv: "sum_upto (λn. 1 / n) ∼[at_top] ln"
proof -
have "sum_upto (λn. n powr -1) ∼[at_top] (λx. ln (⌊x⌋ + 1))"
proof (rule asymp_equiv_sandwich)
have "eventually (λx. sum_upto (λn. n powr -1) x ∈ {ln (⌊x⌋ + 1)..ln ⌊x⌋ + 1}) at_top"
using eventually_ge_at_top[of 1]
proof eventually_elim
case (elim x)
have "sum_upto (λn. real n powr -1) x = harm (nat ⌊x⌋)"
unfolding sum_upto_altdef harm_def by (intro sum.cong) (auto simp: field_simps powr_minus)
also have "… ∈ {ln (⌊x⌋ + 1)..ln ⌊x⌋ + 1}"
using elim harm_le[of "nat ⌊x⌋"] ln_le_harm[of "nat ⌊x⌋"]
by (auto simp: le_nat_iff le_floor_iff)
finally show ?case by simp
qed
thus "eventually (λx. sum_upto (λn. n powr -1) x ≥ ln (⌊x⌋ + 1)) at_top"
"eventually (λx. sum_upto (λn. n powr -1) x ≤ ln ⌊x⌋ + 1) at_top"
by (eventually_elim; simp)+
qed real_asymp+
also have "… ∼[at_top] ln" by real_asymp
finally show ?thesis by (simp add: powr_minus field_simps)
qed
lemma
fixes s :: real
assumes s: "s > 0" "s ≠ 1"
shows zeta_partial_sum_bigo_pos:
"(λn. (∑k=1..n. real k powr -s) - real n powr (1 - s) / (1 - s) - Re (zeta s))
∈ O(λx. real x powr -s)"
and zeta_partial_sum_bigo_pos':
"(λn. ∑k=1..n. real k powr -s) =o
(λn. real n powr (1 - s) / (1 - s) + Re (zeta s)) +o O(λx. real x powr -s)"
proof -
define F where "F = (λx. x powr (1 - s) / (1 - s))"
define f where "f = (λx. x powr -s)"
define f' where "f' = (λx. -s * x powr (-s-1))"
define z where "z = Re (zeta s)"
interpret euler_maclaurin_nat' F f "(!) [f, f']" 1 0 z "{}"
proof
have "(λb. (∑k=1..b. real k powr -s) - real b powr (1 - s) / (1 - s) - real b powr -s / 2)
⇢ Re (zeta s) - 0"
proof (intro tendsto_diff)
let ?g = "λb. (∑i<b. complex_of_real (real i + 1) powr - complex_of_real s) -
of_nat b powr (1 - complex_of_real s) / (1 - complex_of_real s)"
have "∀⇩F b in at_top. Re (?g b) = (∑k=1..b. real k powr -s) - real b powr (1 - s) / (1 - s)"
using eventually_ge_at_top[of 1]
proof eventually_elim
case (elim b)
have "(∑k=1..b. real k powr -s) = (∑k<b. real (Suc k) powr -s) "
by (intro sum.reindex_bij_witness[of _ Suc "λn. n - 1"]) auto
also have "… - real b powr (1 - s) / (1 - s) = Re (?g b)"
by (auto simp: powr_Reals_eq add_ac)
finally show ?case ..
qed
moreover have "(λb. Re (?g b)) ⇢ Re (zeta s)"
using hurwitz_zeta_critical_strip[of "of_real s" 1] s
by (intro tendsto_intros) (simp add: zeta_def)
ultimately show "(λb. (∑k=1..b. real k powr -s) - real b powr (1 - s) / (1 - s)) ⇢ Re (zeta s)"
by (blast intro: Lim_transform_eventually)
qed (use s in real_asymp)
thus "(λb. (∑k = 1..b. f (real k)) - F (real b) -
(∑i<2 * 0 + 1. (bernoulli' (Suc i) / fact (Suc i)) *⇩R ([f, f'] ! i) (real b)))
⇢ z" by (simp add: f_def F_def z_def)
qed (use ‹s ≠ 1› in
‹auto intro!: derivative_eq_intros continuous_intros
simp flip: has_real_derivative_iff_has_vector_derivative
simp: F_def f_def f'_def nth_Cons split: nat.splits›)
{
fix n :: nat assume n: "n ≥ 1"
have "(∑k=1..n. real k powr -s) =
n powr (1 - s) / (1 - s) + z + 1/2 * n powr -s -
EM_remainder 1 f' (int n)"
using euler_maclaurin_strong_nat'[of n] n by (simp add: F_def f_def)
} note * = this
have "(λn. (∑k=1..n. real k powr -s) - n powr (1 - s) / (1 - s) - z) ∈
Θ(λn. 1/2 * n powr -s - EM_remainder 1 f' (int n))"
using * by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of 1]]) auto
also have "(λn. 1/2 * n powr -s - EM_remainder 1 f' (int n)) ∈ O(λn. n powr -s)"
proof (intro sum_in_bigo)
have "(λx. norm (EM_remainder 1 f' (int x))) ∈ O(λx. real x powr - s)"
proof (rule EM_remainder_strong_bigo_nat[where a = 1 and Y = "{}"])
fix x :: real assume "x ≥ 1"
show "norm (f' x) ≤ s * x powr (-s-1)"
using s by (simp add: f'_def)
next
from s show "((λx. x powr -s) ⤏ 0) at_top" by real_asymp
qed (auto simp: f'_def intro!: continuous_intros derivative_eq_intros)
thus "(λx. EM_remainder 1 f' (int x)) ∈ O(λx. real x powr -s)"
by simp
qed real_asymp+
finally show "(λn. (∑k=1..n. real k powr -s) - real n powr (1 - s) / (1 - s) - z)
∈ O(λx. real x powr -s)" .
thus"(λn. ∑k=1..n. real k powr -s) =o
(λn. real n powr (1 - s) / (1 - s) + z) +o O(λx. real x powr -s)"
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def algebra_simps)
qed
lemma zeta_tail_bigo:
fixes s :: real
assumes s: "s > 1"
shows "(λn. Re (hurwitz_zeta (real n + 1) s)) ∈ O(λx. real x powr (1 - s))"
proof -
have [simp]: "complex_of_real (Re (zeta s)) = zeta s"
using zeta_real[of s] by (auto elim!: Reals_cases)
from s have s': "s > 0" "s ≠ 1" by auto
have "(λn. -Re (hurwitz_zeta (real n + 1) s) - real n powr (1 - s) / (1 - s)
+ real n powr (1 - s) / (1 - s))
∈ O(λx. real x powr (1 - s))"
proof (rule sum_in_bigo)
have "(λn. -Re (hurwitz_zeta (real n + 1) s) - real n powr (1 - s) / (1 - s)) =
(λn. (∑k=1..n. real k powr -s) - real n powr (1 - s) / (1 - s) - Re (zeta s))"
(is "?lhs = ?rhs")
proof
fix n :: nat
have "hurwitz_zeta (1 + real n) s = zeta s - (∑k<n. real (Suc k) powr -s)"
by (subst hurwitz_zeta_shift) (use assms in ‹auto simp: zeta_def powr_Reals_eq›)
also have "(∑k<n. real (Suc k) powr -s) = (∑k=1..n. real k powr -s)"
by (rule sum.reindex_bij_witness[of _ "λk. k - 1" Suc]) auto
finally show "?lhs n = ?rhs n" by (simp add: add_ac)
qed
also have "… ∈ O(λx. real x powr (-s))"
by (rule zeta_partial_sum_bigo_pos) (use s in auto)
also have "(λx. real x powr (-s)) ∈ O(λx. real x powr (1-s))"
by real_asymp
finally show "(λn. -Re (hurwitz_zeta (real n + 1) s) - real n powr (1 - s) / (1 - s)) ∈ …" .
qed (use s in real_asymp)
thus ?thesis by simp
qed
lemma zeta_tail_bigo':
fixes s :: real
assumes s: "s > 1"
shows "(λn. Re (hurwitz_zeta (real n) s)) ∈ O(λx. real x powr (1 - s))"
proof -
have "(λn. Re (hurwitz_zeta (real n) s)) ∈ Θ(λn. Re (hurwitz_zeta (real (n - 1) + 1) s))"
by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of 1]])
(auto simp: of_nat_diff)
also have "(λn. Re (hurwitz_zeta (real (n - 1) + 1) s)) ∈ O(λx. real (x - 1) powr (1 - s))"
by (rule landau_o.big.compose[OF zeta_tail_bigo[OF assms]]) real_asymp
also have "(λx. real (x - 1) powr (1 - s)) ∈ O(λx. real x powr (1 - s))"
by real_asymp
finally show ?thesis .
qed
lemma
fixes s :: real
assumes s: "s > 0"
shows zeta_partial_sum_bigo_neg:
"(λn. (∑i=1..n. real i powr s) - n powr (1 + s) / (1 + s)) ∈ O(λn. n powr s)"
and zeta_partial_sum_bigo_neg':
"(λn. (∑i=1..n. real i powr s)) =o (λn. n powr (1 + s) / (1 + s)) +o O(λn. n powr s)"
proof -
define F where "F = (λx. x powr (1 + s) / (1 + s))"
define f where "f = (λx. x powr s)"
define f' where "f' = (λx. s * x powr (s - 1))"
have "(∑i=1..n. f (real i)) - F n =
1 / 2 - F 1 + f n / 2 + EM_remainder' 1 f' 1 (real n)" if n: "n ≥ 1" for n
proof -
have "(∑i∈{1<..n}. f (real i)) - integral {real 1..real n} f =
(∑k<1. (bernoulli' (Suc k) / fact (Suc k)) *⇩R (([f, f'] ! k) (real n) -
([f, f'] ! k) (real 1))) + EM_remainder' 1 ([f, f'] ! 1) (real 1) (real n)"
by (rule euler_maclaurin_strong_raw_nat[where Y = "{}"])
(use ‹s > 0› ‹n ≥ 1› in
‹auto intro!: derivative_eq_intros continuous_intros
simp flip: has_real_derivative_iff_has_vector_derivative
simp: F_def f_def f'_def nth_Cons split: nat.splits›)
also have "(∑i∈{1<..n}. f (real i)) = (∑i∈insert 1 {1<..n}. f (real i)) - f 1"
using n by (subst sum.insert) auto
also from n have "insert 1 {1<..n} = {1..n}" by auto
finally have "(∑i=1..n. f (real i)) - F n = f 1 + (integral {1..real n} f - F n) +
(f (real n) - f 1) / 2 + EM_remainder' 1 f' 1 (real n)" by simp
hence "(∑i=1..n. f (real i)) - F n = 1 / 2 + (integral {1..real n} f - F n) +
f (real n) / 2 + EM_remainder' 1 f' 1 (real n)"
using s by (simp add: f_def diff_divide_distrib)
also have "(f has_integral (F (real n) - F 1)) {1..real n}" using assms n
by (intro fundamental_theorem_of_calculus)
(auto simp flip: has_real_derivative_iff_has_vector_derivative simp: F_def f_def
intro!: derivative_eq_intros continuous_intros)
hence "integral {1..real n} f - F n = - F 1"
by (simp add: has_integral_iff)
also have "1 / 2 + (-F 1) + f (real n) / 2 = 1 / 2 - F 1 + f n / 2"
by simp
finally show ?thesis .
qed
hence "(λn. (∑i=1..n. f (real i)) - F n) ∈
Θ(λn. 1 / 2 - F 1 + f n / 2 + EM_remainder' 1 f' 1 (real n))"
by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of 1]])
also have "(λn. 1 / 2 - F 1 + f n / 2 + EM_remainder' 1 f' 1 (real n))
∈ O(λn. real n powr s)"
unfolding F_def f_def
proof (intro sum_in_bigo)
have "(λx. integral {1..real x} (λt. pbernpoly 1 t *⇩R f' t)) ∈ O(λn. 1 / s * real n powr s)"
proof (intro landau_o.big.compose[OF integral_bigo])
have "(λx. pbernpoly 1 x * f' x) ∈ O(λx. 1 * x powr (s - 1))"
by (intro landau_o.big.mult pbernpoly_bigo) (auto simp: f'_def)
thus "(λx. pbernpoly 1 x *⇩R f' x) ∈ O(λx. x powr (s - 1))"
by simp
from s show "filterlim (λa. 1 / s * a powr s) at_top at_top" by real_asymp
next
fix a' x :: real assume "a' ≥ 1" "a' ≤ x"
thus "(λa. pbernpoly 1 a *⇩R f' a) integrable_on {a'..x}"
by (intro integrable_EM_remainder') (auto intro!: continuous_intros simp: f'_def)
qed (use s in ‹auto intro!: filterlim_real_sequentially continuous_intros derivative_eq_intros›)
thus "(λx. EM_remainder' 1 f' 1 (real x)) ∈ O(λn. real n powr s)"
using ‹s > 0› by (simp add: EM_remainder'_def)
qed (use ‹s > 0› in real_asymp)+
finally show "(λn. (∑i=1..n. real i powr s) - n powr (1 + s) / (1 + s)) ∈ O(λn. n powr s)"
by (simp add: f_def F_def)
thus "(λn. (∑i=1..n. real i powr s)) =o (λn. n powr (1 + s) / (1 + s)) +o O(λn. n powr s)"
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def algebra_simps)
qed
lemma zeta_partial_sum_le_pos:
assumes "s > 0" "s ≠ 1"
defines "z ≡ Re (zeta (complex_of_real s))"
shows "∃c>0. ∀x≥1. ¦sum_upto (λn. n powr -s) x - (x powr (1-s) / (1-s) + z)¦ ≤ c * x powr -s"
proof (rule sum_upto_asymptotics_lift_nat_real)
show "(λn. (∑k = 1..n. real k powr - s) - (real n powr (1 - s) / (1 - s) + z))
∈ O(λn. real n powr - s)"
using zeta_partial_sum_bigo_pos[OF assms(1,2)] unfolding z_def
by (simp add: algebra_simps)
from assms have "s < 1 ∨ s > 1" by linarith
thus "(λn. real n powr (1 - s) / (1 - s) + z - (real (Suc n) powr (1 - s) / (1 - s) + z))
∈ O(λn. real n powr - s)"
by standard (use ‹s > 0› in ‹real_asymp+›)
show "(λn. real n powr - s) ∈ O(λn. real (Suc n) powr - s)"
by real_asymp
show "mono_on {1..} (λa. a powr - s) ∨ mono_on {1..} (λx. - (x powr - s))"
using assms by (intro disjI2) (auto intro!: mono_onI powr_mono2')
from assms have "s < 1 ∨ s > 1" by linarith
hence "mono_on {1..} (λa. a powr (1 - s) / (1 - s) + z)"
proof
assume "s < 1"
thus ?thesis using ‹s > 0›
by (intro mono_onI powr_mono2 divide_right_mono add_right_mono) auto
next
assume "s > 1"
thus ?thesis
by (intro mono_onI le_imp_neg_le add_right_mono divide_right_mono_neg powr_mono2') auto
qed
thus "mono_on {1..} (λa. a powr (1 - s) / (1 - s) + z) ∨
mono_on {1..} (λx. - (x powr (1 - s) / (1 - s) + z))" by blast
qed auto
lemma zeta_partial_sum_le_pos':
assumes "s > 0" "s ≠ 1"
defines "z ≡ Re (zeta (complex_of_real s))"
shows "∃c>0. ∀x≥1. ¦sum_upto (λn. n powr -s) x - x powr (1-s) / (1-s)¦ ≤ c"
proof -
have "∃c>0. ∀x≥1. ¦sum_upto (λn. n powr -s) x - x powr (1-s) / (1-s)¦ ≤ c * 1"
proof (rule sum_upto_asymptotics_lift_nat_real)
have "(λn. (∑k = 1..n. real k powr - s) - (real n powr (1 - s) / (1 - s) + z))
∈ O(λn. real n powr - s)"
using zeta_partial_sum_bigo_pos[OF assms(1,2)] unfolding z_def
by (simp add: algebra_simps)
also have "(λn. real n powr -s) ∈ O(λn. 1)"
using assms by real_asymp
finally have "(λn. (∑k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - z)
∈ O(λn. 1)" by (simp add: algebra_simps)
hence "(λn. (∑k = 1..n. real k powr - s) - real n powr (1 - s) / (1 - s) - z + z) ∈ O(λn. 1)"
by (rule sum_in_bigo) auto
thus "(λn. (∑k = 1..n. real k powr - s) - (real n powr (1 - s) / (1 - s))) ∈ O(λn. 1)"
by simp
from assms have "s < 1 ∨ s > 1" by linarith
thus "(λn. real n powr (1 - s) / (1 - s) - (real (Suc n) powr (1 - s) / (1 - s))) ∈ O(λn. 1)"
by standard (use ‹s > 0› in ‹real_asymp+›)
show "mono_on {1..} (λa. 1) ∨ mono_on {1..} (λx::real. -1 :: real)"
using assms by (intro disjI2) (auto intro!: mono_onI powr_mono2')
from assms have "s < 1 ∨ s > 1" by linarith
hence "mono_on {1..} (λa. a powr (1 - s) / (1 - s))"
proof
assume "s < 1"
thus ?thesis using ‹s > 0›
by (intro mono_onI powr_mono2 divide_right_mono add_right_mono) auto
next
assume "s > 1"
thus ?thesis
by (intro mono_onI le_imp_neg_le add_right_mono divide_right_mono_neg powr_mono2') auto
qed
thus "mono_on {1..} (λa. a powr (1 - s) / (1 - s)) ∨
mono_on {1..} (λx. - (x powr (1 - s) / (1 - s)))" by blast
qed auto
thus ?thesis by simp
qed
lemma zeta_partial_sum_le_pos'':
assumes "s > 0" "s ≠ 1"
shows "∃c>0. ∀x≥1. ¦sum_upto (λn. n powr -s) x¦ ≤ c * x powr max 0 (1 - s)"
proof -
from zeta_partial_sum_le_pos'[OF assms] obtain c where
c: "c > 0" "⋀x. x ≥ 1 ⟹ ¦sum_upto (λx. real x powr - s) x - x powr (1 - s) / (1 - s)¦ ≤ c"
by auto
{
fix x :: real assume x: "x ≥ 1"
have "¦sum_upto (λx. real x powr - s) x¦ ≤ ¦x powr (1 - s) / (1 - s)¦ + c"
using c(1) c(2)[OF x] x by linarith
also have "¦x powr (1 - s) / (1 - s)¦ = x powr (1 - s) / ¦1 - s¦"
using assms by simp
also have "… ≤ x powr max 0 (1 - s) / ¦1 - s¦"
using x by (intro divide_right_mono powr_mono) auto
also have "c = c * x powr 0" using x by simp
also have "c * x powr 0 ≤ c * x powr max 0 (1 - s)"
using c(1) x by (intro mult_left_mono powr_mono) auto
also have "x powr max 0 (1 - s) / ¦1 - s¦ + c * x powr max 0 (1 - s) =
(1 / ¦1 - s¦ + c) * x powr max 0 (1 - s)"
by (simp add: algebra_simps)
finally have "¦sum_upto (λx. real x powr - s) x¦ ≤ (1 / ¦1 - s¦ + c) * x powr max 0 (1 - s)"
by simp
}
moreover have "(1 / ¦1 - s¦ + c) > 0"
using c assms by (intro add_pos_pos divide_pos_pos) auto
ultimately show ?thesis by blast
qed
lemma zeta_partial_sum_le_pos_bigo:
assumes "s > 0" "s ≠ 1"
shows "(λx. sum_upto (λn. n powr -s) x) ∈ O(λx. x powr max 0 (1 - s))"
proof -
from zeta_partial_sum_le_pos''[OF assms] obtain c
where "∀x≥1. ¦sum_upto (λn. n powr -s) x¦ ≤ c * x powr max 0 (1 - s)" by auto
thus ?thesis
by (intro bigoI[of _ c] eventually_mono[OF eventually_ge_at_top[of 1]]) auto
qed
lemma zeta_partial_sum_01_asymp_equiv:
assumes "s ∈ {0<..<1}"
shows "sum_upto (λn. n powr -s) ∼[at_top] (λx. x powr (1 - s) / (1 - s))"
proof -
from zeta_partial_sum_le_pos'[of s] assms obtain c where
c: "c > 0" "∀x≥1. ¦sum_upto (λx. real x powr -s) x - x powr (1 - s) / (1 - s)¦ ≤ c" by auto
hence "(λx. sum_upto (λx. real x powr -s) x - x powr (1 - s) / (1 - s)) ∈ O(λ_. 1)"
by (intro bigoI[of _ c] eventually_mono[OF eventually_ge_at_top[of 1]]) auto
also have "(λ_. 1) ∈ o(λx. x powr (1 - s) / (1 - s))"
using assms by real_asymp
finally show ?thesis
by (rule smallo_imp_asymp_equiv)
qed
lemma zeta_partial_sum_gt_1_asymp_equiv:
fixes s :: real
assumes "s > 1"
defines "ζ ≡ Re (zeta s)"
shows "sum_upto (λn. n powr -s) ∼[at_top] (λx. ζ)"
proof -
have [simp]: "ζ ≠ 0"
using assms zeta_Re_gt_1_nonzero[of s] zeta_real[of s] by (auto elim!: Reals_cases)
from zeta_partial_sum_le_pos[of s] assms obtain c where
c: "c > 0" "∀x≥1. ¦sum_upto (λx. real x powr -s) x - (x powr (1 - s) / (1 - s) + ζ)¦ ≤
c * x powr -s" by (auto simp: ζ_def)
hence "(λx. sum_upto (λx. real x powr -s) x - ζ - x powr (1 - s) / (1 - s)) ∈ O(λx. x powr -s)"
by (intro bigoI[of _ c] eventually_mono[OF eventually_ge_at_top[of 1]]) auto
also have "(λx. x powr -s) ∈ o(λ_. 1)"
using ‹s > 1› by real_asymp
finally have "(λx. sum_upto (λx. real x powr -s) x - ζ - x powr (1 - s) / (1 - s) +
x powr (1 - s) / (1 - s)) ∈ o(λ_. 1)"
by (rule sum_in_smallo) (use ‹s > 1› in real_asymp)
thus ?thesis by (simp add: smallo_imp_asymp_equiv)
qed
lemma zeta_partial_sum_pos_bigtheta:
assumes "s > 0" "s ≠ 1"
shows "sum_upto (λn. n powr -s) ∈ Θ(λx. x powr max 0 (1 - s))"
proof (cases "s > 1")
case False
thus ?thesis
using asymp_equiv_imp_bigtheta[OF zeta_partial_sum_01_asymp_equiv[of s]] assms
by (simp add: max_def)
next
case True
have [simp]: "Re (zeta s) ≠ 0"
using True zeta_Re_gt_1_nonzero[of s] zeta_real[of s] by (auto elim!: Reals_cases)
show ?thesis
using True asymp_equiv_imp_bigtheta[OF zeta_partial_sum_gt_1_asymp_equiv[of s]]
by (simp add: max_def)
qed
lemma zeta_partial_sum_le_neg:
assumes "s > 0"
shows "∃c>0. ∀x≥1. ¦sum_upto (λn. n powr s) x - x powr (1 + s) / (1 + s)¦ ≤ c * x powr s"
proof (rule sum_upto_asymptotics_lift_nat_real)
show "(λn. (∑k = 1..n. real k powr s) - (real n powr (1 + s) / (1 + s)))
∈ O(λn. real n powr s)"
using zeta_partial_sum_bigo_neg[OF assms(1)] by (simp add: algebra_simps)
show "(λn. real n powr (1 + s) / (1 + s) - (real (Suc n) powr (1 + s) / (1 + s)))
∈ O(λn. real n powr s)"
using assms by real_asymp
show "(λn. real n powr s) ∈ O(λn. real (Suc n) powr s)"
by real_asymp
show "mono_on {1..} (λa. a powr s) ∨ mono_on {1..} (λx. - (x powr s))"
using assms by (intro disjI1) (auto intro!: mono_onI powr_mono2)
show "mono_on {1..} (λa. a powr (1 + s) / (1 + s)) ∨
mono_on {1..} (λx. - (x powr (1 + s) / (1 + s)))"
using assms by (intro disjI1 divide_right_mono powr_mono2 mono_onI) auto
qed auto
lemma zeta_partial_sum_neg_asymp_equiv:
assumes "s > 0"
shows "sum_upto (λn. n powr s) ∼[at_top] (λx. x powr (1 + s) / (1 + s))"
proof -
from zeta_partial_sum_le_neg[of s] assms obtain c where
c: "c > 0" "∀x≥1. ¦sum_upto (λx. real x powr s) x - x powr (1 + s) / (1 + s)¦ ≤ c * x powr s"
by auto
hence "(λx. sum_upto (λx. real x powr s) x - x powr (1 + s) / (1 + s)) ∈ O(λx. x powr s)"
by (intro bigoI[of _ c] eventually_mono[OF eventually_ge_at_top[of 1]]) auto
also have "(λx. x powr s) ∈ o(λx. x powr (1 + s) / (1 + s))"
using assms by real_asymp
finally show ?thesis
by (rule smallo_imp_asymp_equiv)
qed
end