Theory Prime_Distribution_Elementary.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)"
          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)) = (iinsert 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. 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
    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. 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
      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. 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)"
      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 "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
    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. 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