# Theory Partial_Zeta_Bounds

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

Asymptotic bounds on sums over k^(-s) for k=1..n, for fixed s and variable n.
*)
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

(* TODO: This does not necessarily require the full complex zeta function. *)

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)"
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
)

{
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
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
)
also have "(i{1<..n}. f (real i)) = (iinsert 1 {1<..n}. f (real i)) - f 1"
using n by (subst sum.insert) auto
also from n have  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"
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 )
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)"
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. x1. ¦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

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. x1. ¦sum_upto (λn. n powr -s) x - x powr (1-s) / (1-s)¦  c"
proof -
have "c>0. x1. ¦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
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. x1. ¦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)"
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 "x1. ¦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" "x1. ¦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" "x1. ¦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
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]]
qed

lemma zeta_partial_sum_le_neg:
assumes "s > 0"
shows   "c>0. x1. ¦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" "x1. ¦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