Theory Prime_Distribution_Elementary.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 "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