Session Prime_Distribution_Elementary

Theory Prime_Distribution_Elementary_Library

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

  Various auxiliary material, much of which should probably be moved somewhere else
  eventually.
*)
section ‹Auxiliary material›
theory Prime_Distribution_Elementary_Library
imports
  Zeta_Function.Zeta_Function
  Prime_Number_Theorem.Prime_Counting_Functions
  Stirling_Formula.Stirling_Formula
begin

lemma divisor_count_pos [intro]: "n > 0  divisor_count n > 0"
  by (auto simp: divisor_count_def intro!: Nat.gr0I)

lemma divisor_count_eq_0_iff [simp]: "divisor_count n = 0  n = 0"
  by (cases "n = 0") auto

lemma divisor_count_pos_iff [simp]: "divisor_count n > 0  n > 0"
  by (cases "n = 0") auto

lemma smallest_prime_beyond_eval:
  "prime n  smallest_prime_beyond n = n"
  "¬prime n  smallest_prime_beyond n = smallest_prime_beyond (Suc n)"
proof -
  assume "prime n"
  thus "smallest_prime_beyond n = n"
    by (rule smallest_prime_beyond_eq) auto
next
  assume "¬prime n"
  show "smallest_prime_beyond n = smallest_prime_beyond (Suc n)"
  proof (rule antisym)
    show "smallest_prime_beyond n  smallest_prime_beyond (Suc n)"
      by (rule smallest_prime_beyond_smallest)
         (auto intro: order.trans[OF _ smallest_prime_beyond_le])
  next
    have "smallest_prime_beyond n  n"
      using prime_smallest_prime_beyond[of n] ¬prime n by metis
    hence "smallest_prime_beyond n > n"
      using smallest_prime_beyond_le[of n] by linarith
    thus "smallest_prime_beyond n  smallest_prime_beyond (Suc n)"
      by (intro smallest_prime_beyond_smallest) auto
  qed
qed

lemma nth_prime_numeral:
  "nth_prime (numeral n) = smallest_prime_beyond (Suc (nth_prime (pred_numeral n)))"
  by (subst nth_prime_Suc[symmetric]) auto

lemmas nth_prime_eval = smallest_prime_beyond_eval nth_prime_Suc nth_prime_numeral

lemma nth_prime_1 [simp]: "nth_prime (Suc 0) = 3"
  by (simp add: nth_prime_eval)

lemma nth_prime_2 [simp]: "nth_prime 2 = 5"
  by (simp add: nth_prime_eval)

lemma nth_prime_3 [simp]: "nth_prime 3 = 7"
  by (simp add: nth_prime_eval)

(* TODO: copied from afp-devel; delete in AFP 2019 *)
lemma strict_mono_sequence_partition:
  assumes "strict_mono (f :: nat  'a :: {linorder, no_top})"
  assumes "x  f 0"
  assumes "filterlim f at_top at_top"
  shows   "k. x  {f k..<f (Suc k)}"
proof -
  define k where "k = (LEAST k. f (Suc k) > x)"
  {
    obtain n where "x  f n"
      using assms by (auto simp: filterlim_at_top eventually_at_top_linorder)
    also have "f n < f (Suc n)"
      using assms by (auto simp: strict_mono_Suc_iff)
    finally have "n. f (Suc n) > x" by auto
  }
  from LeastI_ex[OF this] have "x < f (Suc k)"
    by (simp add: k_def)
  moreover have "f k  x"
  proof (cases k)
    case (Suc k')
    have "k  k'" if "f (Suc k') > x"
      using that unfolding k_def by (rule Least_le)
    with Suc show "f k  x" by (cases "f k  x") (auto simp: not_le)
  qed (use assms in auto)
  ultimately show ?thesis by auto
qed

lemma nth_prime_partition:
  assumes "x  2"
  shows   "k. x  {nth_prime k..<nth_prime (Suc k)}"
  using strict_mono_sequence_partition[OF strict_mono_nth_prime, of x] assms nth_prime_at_top
  by simp

lemma nth_prime_partition':
  assumes "x  2"
  shows   "k. x  {real (nth_prime k)..<real (nth_prime (Suc k))}"
  by (rule strict_mono_sequence_partition)
     (auto simp: strict_mono_Suc_iff assms
           intro!: filterlim_real_sequentially filterlim_compose[OF _ nth_prime_at_top])

lemma between_nth_primes_imp_nonprime:
  assumes "n > nth_prime k" "n < nth_prime (Suc k)"
  shows   "¬prime n"
  using assms by (metis Suc_leI not_le nth_prime_Suc smallest_prime_beyond_smallest)

lemma nth_prime_partition'':
  includes prime_counting_notation
  assumes "x  (2 :: real)"
  shows "x  {real (nth_prime (nat π x - 1))..<real (nth_prime (nat π x))}"
proof -
  obtain n where n: "x  {nth_prime n..<nth_prime (Suc n)}"
    using nth_prime_partition' assms by auto
  have "π (nth_prime n) = π x"
    unfolding π_def using between_nth_primes_imp_nonprime n
    by (intro prime_sum_upto_eqI) (auto simp: le_nat_iff le_floor_iff)
  hence "real n = π x - 1"
    by simp
  hence n_eq: "n = nat π x - 1" "Suc n = nat π x"
    by linarith+
  with n show ?thesis 
    by simp
qed
(* END TODO *)

(* TODO: Move *)
lemma asymp_equivD_strong:
  assumes "f ∼[F] g" "eventually (λx. f x  0  g x  0) F"
  shows   "((λx. f x / g x)  1) F"
proof -
  from assms(1) have "((λx. if f x = 0  g x = 0 then 1 else f x / g x)  1) F"
    by (rule asymp_equivD)
  also have "?this  ?thesis"
    by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
  finally show ?thesis .
qed

lemma hurwitz_zeta_shift:
  fixes s :: complex
  assumes "a > 0" and "s  1"
  shows   "hurwitz_zeta (a + real n) s = hurwitz_zeta a s - (k<n. (a + real k) powr -s)"
proof (rule analytic_continuation_open[where f = "λs. hurwitz_zeta (a + real n) s"])
  fix s assume s: "s  {s. Re s > 1}"
  have "(λk. (a + of_nat (k + n)) powr -s) sums hurwitz_zeta (a + real n) s"
    using sums_hurwitz_zeta[of "a + real n" s] s assms by (simp add: add_ac)
  moreover have "(λk. (a + of_nat k) powr -s) sums hurwitz_zeta a s"
    using sums_hurwitz_zeta[of a s] s assms by (simp add: add_ac)
  hence "(λk. (a + of_nat (k + n)) powr -s) sums
            (hurwitz_zeta a s - (k<n. (a + of_nat k) powr -s))"
    by (rule sums_split_initial_segment)
  ultimately show "hurwitz_zeta (a + real n) s = hurwitz_zeta a s - (k<n. (a + real k) powr -s)"
    by (simp add: sums_iff)
next
  show "connected (-{1::complex})"
    by (rule connected_punctured_universe) auto
qed (use assms in auto intro!: holomorphic_intros open_halfspace_Re_gt exI[of _ 2])

lemma pbernpoly_bigo: "pbernpoly n  O(λ_. 1)"
proof -
  from bounded_pbernpoly[of n] obtain c where "x. norm (pbernpoly n x)  c"
    by auto
  thus ?thesis by (intro bigoI[of _ c]) auto
qed

lemma harm_le: "n  1  harm n  ln n + 1"
  using euler_mascheroni_sequence_decreasing[of 1 n]
  by (simp add: harm_expand)

lemma sum_upto_1 [simp]: "sum_upto f 1 = f 1"
proof -
  have "{0<..Suc 0} = {1}" by auto
  thus ?thesis by (simp add: sum_upto_altdef)
qed

(* TODO: replace original *)
lemma sum_upto_cong' [cong]:
  "(n. n > 0  real n  x  f n = f' n)  x = x'  sum_upto f x = sum_upto f' x'"
  unfolding sum_upto_def by (intro sum.cong) auto

lemma finite_primes_le: "finite {p. prime p  real p  x}"
  by (rule finite_subset[of _ "{..nat x}"]) (auto simp: le_nat_iff le_floor_iff)

lemma frequently_filtermap: "frequently P (filtermap f F) = frequently (λn. P (f n)) F"
  by (auto simp: frequently_def eventually_filtermap)

lemma frequently_mono_filter: "frequently P F  F  F'  frequently P F'"
  using filter_leD[of F F' "λx. ¬P x"] by (auto simp: frequently_def)

lemma π_at_top: "filterlim primes_pi at_top at_top"
  unfolding filterlim_at_top
proof safe
  fix C :: real
  define x0 where "x0 = real (nth_prime (nat max 0 C))"
  show "eventually (λx. primes_pi x  C) at_top"
    using eventually_ge_at_top
  proof eventually_elim
    fix x assume "x  x0"
    have "C  real (nat max 0 C + 1)" by linarith
    also have "real (nat max 0 C + 1) = primes_pi x0"
      unfolding x0_def by simp
    also have "  primes_pi x" by (rule π_mono) fact
    finally show "primes_pi x  C" .
  qed
qed

lemma sum_upto_ln_stirling_weak_bigo: "(λx. sum_upto ln x - x * ln x + x)  O(ln)"
proof -
  let ?f = "λx. x * ln x - x + ln (2 * pi * x) / 2"
  have "ln (fact n) - (n * ln n - n + ln (2 * pi * n) / 2)  {0..1/(12*n)}" if "n > 0" for n :: nat
    using ln_fact_bounds[OF that] by (auto simp: algebra_simps)
  hence "(λn. ln (fact n) - ?f n)  O(λn. 1 / real n)"
    by (intro bigoI[of _ "1/12"] eventually_mono[OF eventually_gt_at_top[of 0]]) auto
  hence "(λx. ln (fact (nat x)) - ?f (nat x))  O(λx. 1 / real (nat x))"
    by (rule landau_o.big.compose)
       (intro filterlim_compose[OF filterlim_nat_sequentially] filterlim_floor_sequentially)
  also have "(λx. 1 / real (nat x))  O(λx::real. ln x)" by real_asymp
  finally have "(λx. ln (fact (nat x)) - ?f (nat x) + (?f (nat x) - ?f x))  O(λx. ln x)"
    by (rule sum_in_bigo) real_asymp
  hence "(λx. ln (fact (nat x)) - ?f x)  O(λx. ln x)"
    by (simp add: algebra_simps)
  hence "(λx. ln (fact (nat x)) - ?f x + ln (2 * pi * x) / 2)  O(λx. ln x)"
    by (rule sum_in_bigo) real_asymp
  thus ?thesis by (simp add: sum_upto_ln_conv_ln_fact algebra_simps)
qed


subsection ‹Various facts about Dirichlet series›

lemma fds_mangoldt':
  "fds mangoldt = fds_zeta * fds_deriv (fds moebius_mu)"
proof -
  have "fds mangoldt = (fds moebius_mu * fds (λn. of_real (ln (real n)) :: 'a))"
    (is "_ = ?f") by (subst fds_mangoldt) auto
  also have " = fds_zeta * fds_deriv (fds moebius_mu)"
  proof (intro fds_eqI)
    fix n :: nat assume n: "n > 0"
    have "fds_nth ?f n = (d | d dvd n. moebius_mu d * of_real (ln (real (n div d))))"
      by (auto simp: fds_eq_iff fds_nth_mult dirichlet_prod_def)
    also have " = (d | d dvd n. moebius_mu d * of_real (ln (real n / real d)))"
      by (intro sum.cong) (auto elim!: dvdE simp: ln_mult split: if_splits)
    also have " = (d | d dvd n. moebius_mu d * of_real (ln n - ln d))"
      using n by (intro sum.cong refl) (subst ln_div, auto elim!: dvdE)
    also have " = of_real (ln n) * (d | d dvd n. moebius_mu d) -
                      (d | d dvd n. of_real (ln d) * moebius_mu d)"
      by (simp add: sum_subtractf sum_distrib_left sum_distrib_right algebra_simps)
    also have "of_real (ln n) * (d | d dvd n. moebius_mu d) = 0"
      by (subst sum_moebius_mu_divisors') auto
    finally show "fds_nth ?f n = fds_nth (fds_zeta * fds_deriv (fds moebius_mu) :: 'a fds) n"
      by (simp add: fds_nth_mult dirichlet_prod_altdef1 fds_nth_deriv sum_negf scaleR_conv_of_real)
  qed
  finally show ?thesis .
qed

lemma sum_upto_divisor_sum1:
  "sum_upto (λn. d | d dvd n. f d :: real) x = sum_upto (λn. f n * floor (x / n)) x"
proof -
  have "sum_upto (λn. d | d dvd n. f d :: real) x =
          sum_upto (λn. f n * real (nat (floor (x / n)))) x"
    using sum_upto_dirichlet_prod[of f "λ_. 1" x]
    by (simp add: dirichlet_prod_def sum_upto_altdef)
  also have " = sum_upto (λn. f n * floor (x / n)) x"
    unfolding sum_upto_def by (intro sum.cong) auto
  finally show ?thesis .
qed

lemma sum_upto_divisor_sum2:
  "sum_upto (λn. d | d dvd n. f d :: real) x = sum_upto (λn. sum_upto f (x / n)) x"
  using sum_upto_dirichlet_prod[of "λ_. 1" f x] by (simp add: dirichlet_prod_altdef1)

lemma sum_upto_moebius_times_floor_linear:
  "sum_upto (λn. moebius_mu n * x / real n) x = (if x  1 then 1 else 0)"
proof -
  have "real_of_int (sum_upto (λn. moebius_mu n * x / real n) x) =
          sum_upto (λn. moebius_mu n * of_int x / real n) x"
    by (simp add: sum_upto_def)
  also have " = sum_upto (λn. d | d dvd n. moebius_mu d :: real) x"
    using sum_upto_divisor_sum1[of moebius_mu x] by auto
  also have " = sum_upto (λn. if n = 1 then 1 else 0) x"
    by (intro sum_upto_cong sum_moebius_mu_divisors' refl)
  also have " = real_of_int (if x  1 then 1 else 0)"
    by (auto simp: sum_upto_def)
  finally show ?thesis unfolding of_int_eq_iff .
qed

lemma ln_fact_conv_sum_mangoldt:
  "sum_upto (λn. mangoldt n * x / real n) x = ln (fact (nat x))"
proof -
  have "sum_upto (λn. mangoldt n * of_int x / real n) x =
          sum_upto (λn. d | d dvd n. mangoldt d :: real) x"
    using sum_upto_divisor_sum1[of mangoldt x] by auto
  also have " = sum_upto (λn. of_real (ln (real n))) x"
    by (intro sum_upto_cong mangoldt_sum refl) auto
  also have " = (n{0<..nat x}. ln n)"
    by (simp add: sum_upto_altdef)
  also have " = ln ({0<..nat x})"
    unfolding of_nat_prod by (subst ln_prod) auto
  also have "{0<..nat x} = {1..nat x}" by auto
  also have " = fact (nat x)"
    by (simp add: fact_prod)
  finally show ?thesis by simp
qed


subsection ‹Facts about prime-counting functions›

lemma abs_π [simp]: "¦primes_pi x¦ = primes_pi x"
  by (subst abs_of_nonneg) auto

lemma π_less_self:
  includes prime_counting_notation
  assumes "x > 0"
  shows   "π x < x"
proof -
  have "π x  (n{1<..nat x}. 1)"
    unfolding π_def prime_sum_upto_altdef2 by (intro sum_mono2) (auto dest: prime_gt_1_nat)
  also have " = real (nat x - 1)"
    using assms by simp
  also have " < x" using assms by linarith
  finally show ?thesis .
qed

lemma π_le_self':
  includes prime_counting_notation
  assumes "x  1"
  shows   "π x  x - 1"
proof -
  have "π x  (n{1<..nat x}. 1)"
    unfolding π_def prime_sum_upto_altdef2 by (intro sum_mono2) (auto dest: prime_gt_1_nat)
  also have " = real (nat x - 1)"
    using assms by simp
  also have "  x - 1" using assms by linarith
  finally show ?thesis .
qed

lemma π_le_self:
  includes prime_counting_notation
  assumes "x  0"
  shows   "π x  x"
  using π_less_self[of x] assms by (cases "x = 0") auto

subsection ‹Strengthening `Big-O' bounds›

text ‹
  The following two statements are crucial: They allow us to strengthen a `Big-O' statement
  for $n\to\infty$ or $x\to\infty$ to a bound for ‹all› $n\geq n_0$ or all $x\geq x_0$ under
  some mild conditions.

  This allows us to use all the machinery of asymptotics in Isabelle and still get a bound
  that is applicable over the full domain of the function in the end. This is important because
  Newman often shows that $f(x) \in O(g(x))$ and then writes
  \[\sum_{n\leq x} f(\frac{x}{n}) = \sum_{n\leq x} O(g(\frac{x}{n}))\]
  which is not easy to justify otherwise.
›
lemma natfun_bigoE:
  fixes f :: "nat  _"
  assumes bigo: "f  O(g)" and nz: "n. n  n0  g n  0"
  obtains c where "c > 0" "n. n  n0  norm (f n)  c * norm (g n)"
proof -
  from bigo obtain c where c: "c > 0" "eventually (λn. norm (f n)  c * norm (g n)) at_top"
    by (auto elim: landau_o.bigE)
  then obtain n0' where n0': "n. n  n0'  norm (f n)  c * norm (g n)"
    by (auto simp: eventually_at_top_linorder)
  define c' where "c' = Max ((λn. norm (f n) / norm (g n)) ` (insert n0 {n0..<n0'}))"
  have "norm (f n)  max 1 (max c c') * norm (g n)" if "n  n0" for n
  proof (cases "n  n0'")
    case False
    with that have "norm (f n) / norm (g n)  c'"
      unfolding c'_def by (intro Max.coboundedI) auto
    also have "  max 1 (max c c')" by simp
    finally show ?thesis using nz[of n] that by (simp add: field_simps)
  next
    case True
    hence "norm (f n)  c * norm (g n)" by (rule n0')
    also have "  max 1 (max c c') * norm (g n)"
      by (intro mult_right_mono) auto
    finally show ?thesis .
  qed
  with that[of "max 1 (max c c')"] show ?thesis by auto
qed

lemma bigoE_bounded_real_fun:
  fixes f g :: "real  real"
  assumes "f  O(g)"
  assumes "x. x  x0  ¦g x¦  cg" "cg > 0"
  assumes "b. b  x0  bounded (f ` {x0..b})"
  shows   "c>0. xx0. ¦f x¦  c * ¦g x¦"
proof -
  from assms(1) obtain c where c: "c > 0" "eventually (λx. ¦f x¦  c * ¦g x¦) at_top"
    by (elim landau_o.bigE) auto
  then obtain b where b: "x. x  b  ¦f x¦  c * ¦g x¦"
    by (auto simp: eventually_at_top_linorder)
  have "bounded (f ` {x0..max x0 b})" by (intro assms) auto
  then obtain C where C: "x. x  {x0..max x0 b}  ¦f x¦  C"
    unfolding bounded_iff by fastforce

  define c' where "c' = max c (C / cg)"
  have "¦f x¦  c' * ¦g x¦" if "x  x0" for x
  proof (cases "x  b")
    case False
    then have "¦f x¦  C"
      using C that by auto
    with False have "¦f x¦ / ¦g x¦  C / cg"
      by (meson abs_ge_zero assms frac_le landau_omega.R_trans that)
    also have "  c'" by (simp add: c'_def)
    finally show "¦f x¦  c' * ¦g x¦"
      using that False assms(2)[of x] assms(3) by (auto simp add: divide_simps split: if_splits)
  next
    case True
    hence "¦f x¦  c * ¦g x¦" by (intro b) auto
    also have "  c' * ¦g x¦" by (intro mult_right_mono) (auto simp: c'_def)
    finally show ?thesis .
  qed
  moreover from c(1) have "c' > 0" by (auto simp: c'_def)
  ultimately show ?thesis by blast
qed

lemma sum_upto_asymptotics_lift_nat_real_aux:
  fixes f :: "nat  real" and g :: "real  real"
  assumes bigo: "(λn. (k=1..n. f k) - g (real n))  O(λn. h (real n))"
  assumes g_bigo_self: "(λn. g (real n) - g (real (Suc n)))  O(λn. h (real n))"
  assumes h_bigo_self: "(λn. h (real n))  O(λn. h (real (Suc n)))"
  assumes h_pos: "x. x  1  h x > 0"
  assumes mono_g: "mono_on g {1..}  mono_on (λx. - g x) {1..}"
  assumes mono_h: "mono_on h {1..}  mono_on (λx. - h x) {1..}"
  shows   "c>0. x1. sum_upto f x - g x  c * h x"
proof -
  have h_nz: "h (real n)  0" if "n  1" for n
    using h_pos[of n] that by simp

  from natfun_bigoE[OF bigo h_nz] obtain c1 where
    c1: "c1 > 0" "n. n  1  norm ((k=1..n. f k) - g (real n))  c1 * norm (h (real n))"
    by auto
  from natfun_bigoE[OF g_bigo_self h_nz] obtain c2 where
    c2: "c2 > 0" "n. n  1  norm (g (real n) - g (real (Suc n)))  c2 * norm (h (real n))"
    by auto
  from natfun_bigoE[OF h_bigo_self h_nz] obtain c3 where
    c3: "c3 > 0" "n. n  1  norm (h (real n))  c3 * norm (h (real (Suc n)))"
    by auto

  {
    fix x :: real assume x: "x  1"
    define n where "n = nat x"
    from x have n: "n  1" unfolding n_def by linarith

    have "(k = 1..n. f k) - g x  (c1 + c2) * h (real n)" using mono_g
    proof
      assume mono: "mono_on (λx. -g x) {1..}"
      from x have "x  real (Suc n)"
        unfolding n_def by linarith
      hence "(k=1..n. f k) - g x  (k=1..n. f k) - g n + (g n - g (Suc n))"
        using mono_onD[OF mono, of x "real (Suc n)"] x by auto
      also have "  norm ((k=1..n. f k) - g n) + norm (g n - g (Suc n))"
        by simp
      also have "  c1 * norm (h n) + c2 * norm (h n)"
        using n by (intro add_mono c1 c2) auto
      also have " = (c1 + c2) * h n"
        using h_pos[of "real n"] n by (simp add: algebra_simps)
      finally show ?thesis .
    next
      assume mono: "mono_on g {1..}"
      have "(k=1..n. f k) - g x  (k=1..n. f k) - g n"
        using x by (intro diff_mono mono_onD[OF mono]) (auto simp: n_def)
      also have "  c1 * h (real n)"
        using c1(2)[of n] n h_pos[of n] by simp
      also have "  (c1 + c2) * h (real n)"
        using c2 h_pos[of n] n by (intro mult_right_mono) auto
      finally show ?thesis .
    qed
    also have "(c1 + c2) * h (real n)  (c1 + c2) * (1 + c3) * h x"
      using mono_h
    proof
      assume mono: "mono_on (λx. -h x) {1..}"
      have "(c1 + c2) * h (real n)  (c1 + c2) * (c3 * h (real (Suc n)))"
        using c3(2)[of n] n h_pos[of n] h_pos[of "Suc n"] c1(1) c2(1)
        by (intro mult_left_mono) (auto)
      also have " = (c1 + c2) * c3 * h (real (Suc n))"
        by (simp add: mult_ac)
      also have "  (c1 + c2) * (1 + c3) * h (real (Suc n))"
        using c1(1) c2(1) c3(1) h_pos[of "Suc n"] by (intro mult_left_mono mult_right_mono) auto
      also from x have "x  real (Suc n)"
        unfolding n_def by linarith
      hence "(c1 + c2) * (1 + c3) * h (real (Suc n))  (c1 + c2) * (1 + c3) * h x"
        using c1(1) c2(1) c3(1) mono_onD[OF mono, of x "real (Suc n)"] x
        by (intro mult_left_mono) (auto simp: n_def)
      finally show "(c1 + c2) * h (real n)  (c1 + c2) * (1 + c3) * h x" .
    next
      assume mono: "mono_on h {1..}"
      have "(c1 + c2) * h (real n) = 1 * ((c1 + c2) * h (real n))" by simp
      also have "  (1 + c3) * ((c1 + c2) * h (real n))"
        using c1(1) c2(1) c3(1) h_pos[of n] x n by (intro mult_right_mono) auto
      also have " = (1 + c3) * (c1 + c2) * h (real n)"
        by (simp add: mult_ac)
      also have "  (1 + c3) * (c1 + c2) * h x"
        using x c1(1) c2(1) c3(1) h_pos[of n] n
        by (intro mult_left_mono mono_onD[OF mono]) (auto simp: n_def)
      finally show "(c1 + c2) * h (real n)  (c1 + c2) * (1 + c3) * h x"
        by (simp add: mult_ac)
    qed
    also have "(k = 1..n. f k) = sum_upto f x"
      unfolding sum_upto_altdef n_def by (intro sum.cong) auto
    finally have "sum_upto f x - g x  (c1 + c2) * (1 + c3) * h x" .
  }
  moreover have "(c1 + c2) * (1 + c3) > 0"
    using c1(1) c2(1) c3(1) by (intro mult_pos_pos add_pos_pos) auto
  ultimately show ?thesis by blast
qed

lemma sum_upto_asymptotics_lift_nat_real:
  fixes f :: "nat  real" and g :: "real  real"
  assumes bigo: "(λn. (k=1..n. f k) - g (real n))  O(λn. h (real n))"
  assumes g_bigo_self: "(λn. g (real n) - g (real (Suc n)))  O(λn. h (real n))"
  assumes h_bigo_self: "(λn. h (real n))  O(λn. h (real (Suc n)))"
  assumes h_pos: "x. x  1  h x > 0"
  assumes mono_g: "mono_on g {1..}  mono_on (λx. - g x) {1..}"
  assumes mono_h: "mono_on h {1..}  mono_on (λx. - h x) {1..}"
  shows   "c>0. x1. ¦sum_upto f x - g x¦  c * h x"
proof -
  have "c>0. x1. sum_upto f x - g x  c * h x"
    by (intro sum_upto_asymptotics_lift_nat_real_aux assms)
  then obtain c1 where c1: "c1 > 0" "x. x  1  sum_upto f x - g x  c1 * h x"
    by auto

  have "(λn. -(g (real n) - g (real (Suc n))))  O(λn. h (real n))"
    by (subst landau_o.big.uminus_in_iff) fact
  also have "(λn. -(g (real n) - g (real (Suc n)))) = (λn. g (real (Suc n)) - g (real n))"
    by simp
  finally have "(λn. g (real (Suc n)) - g (real n))  O(λn. h (real n))" .
  moreover {
    have "(λn. -((k=1..n. f k) - g (real n)))  O(λn. h (real n))"
      by (subst landau_o.big.uminus_in_iff) fact
    also have "(λn. -((k=1..n. f k) - g (real n))) =
                 (λn. (k=1..n. -f k) + g (real n))" by (simp add: sum_negf)
    finally have "(λn. (k=1..n. - f k) + g (real n))  O(λn. h (real n))" .
  }
  ultimately have "c>0. x1. sum_upto (λn. -f n) x - (-g x)  c * h x" using mono_g
    by (intro sum_upto_asymptotics_lift_nat_real_aux assms) (simp_all add: disj_commute)
  then obtain c2 where c2: "c2 > 0" "x. x  1  sum_upto (λn. - f n) x + g x  c2 * h x"
    by auto

  {
    fix x :: real assume x: "x  1"
    have "sum_upto f x - g x  max c1 c2 * h x"
      using h_pos[of x] x by (intro order.trans[OF c1(2)] mult_right_mono) auto
    moreover have "sum_upto (λn. -f n) x + g x  max c1 c2 * h x"
      using h_pos[of x] x by (intro order.trans[OF c2(2)] mult_right_mono) auto
    hence "-(sum_upto f x - g x)  max c1 c2 * h x"
      by (simp add: sum_upto_def sum_negf)
    ultimately have "¦sum_upto f x - g x¦  max c1 c2 * h x" by linarith
  }
  moreover from c1(1) c2(1) have "max c1 c2 > 0" by simp
  ultimately show ?thesis by blast
qed

lemma (in factorial_semiring) primepow_divisors_induct [case_names zero unit factor]:
  assumes "P 0" "x. is_unit x  P x"
          "p k x. prime p  k > 0  ¬p dvd x  P x  P (p ^ k * x)"
  shows   "P x"
proof -
  have "finite (prime_factors x)" by simp
  thus ?thesis
  proof (induction "prime_factors x" arbitrary: x rule: finite_induct)
    case empty
    hence "prime_factors x = {}" by metis
    hence "prime_factorization x = {#}" by simp
    thus ?case using assms(1,2) by (auto simp: prime_factorization_empty_iff)
  next
    case (insert p A x)
    define k where "k = multiplicity p x"
    have "k > 0" using insert.hyps
      by (auto simp: prime_factors_multiplicity k_def)
    have p: "p  prime_factors x" using insert.hyps by auto
    from p have "x  0" "¬is_unit p" by (auto simp: in_prime_factors_iff)

    from multiplicity_decompose'[OF this] obtain y where y: "x = p ^ k * y" "¬p dvd y"
      by (auto simp: k_def)
    have "prime_factorization x = replicate_mset k p + prime_factorization y"
      using p k > 0 y unfolding y
      by (subst prime_factorization_mult)
         (auto simp: prime_factorization_prime_power in_prime_factors_iff)
    moreover from y p have "p  prime_factors y"
      by (auto simp: in_prime_factors_iff)
    ultimately have "prime_factors y = prime_factors x - {p}"
      by auto
    also have " = A"
      using insert.hyps by auto
    finally have "P y" using insert by auto
    thus "P x"
      unfolding y using y k > 0 p by (intro assms(3)) (auto simp: in_prime_factors_iff)
  qed
qed

end

Theory More_Dirichlet_Misc

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

  Generalised Dirichlet products and Legendre's identity, and a weighted sum
  of the Möbius μ function
*)
section ‹Miscellaneous material›
theory More_Dirichlet_Misc
imports 
  Prime_Distribution_Elementary_Library
  Prime_Number_Theorem.Prime_Counting_Functions
begin

subsection ‹Generalised Dirichlet products›

(* TODO: Move to Dirichlet_Series *)

definition dirichlet_prod' :: "(nat  'a :: comm_semiring_1)  (real  'a)  real  'a" where
  "dirichlet_prod' f g x = sum_upto (λm. f m * g (x / real m)) x"

lemma dirichlet_prod'_one_left:
  "dirichlet_prod' (λn. if n = 1 then 1 else 0) f x = (if x  1 then f x else 0)"
proof -
  have  "dirichlet_prod' (λn. if n = 1 then 1 else 0) f x =
           (i | 0 < i  real i  x. (if i = Suc 0 then 1 else 0) * f (x / real i))"
    by (simp add: dirichlet_prod'_def sum_upto_def)
  also have " = (i(if x  1 then {1::nat} else {}). f x)"
    by (intro sum.mono_neutral_cong_right) (auto split: if_splits)
  also have " = (if x  1 then f x else 0)"
    by simp
  finally show ?thesis .
qed

lemma dirichlet_prod'_cong:
  assumes "n. n > 0  real n  x  f n = f' n"
  assumes "y. y  1  y  x  g y = g' y"
  assumes "x = x'"
  shows   "dirichlet_prod' f g x = dirichlet_prod' f' g' x'"
  unfolding dirichlet_prod'_def 
  by (intro sum_upto_cong' assms, (subst assms | simp add: assms field_simps)+)

(* 2.21 *)
lemma dirichlet_prod'_assoc:
  "dirichlet_prod' f (λy. dirichlet_prod' g h y) x = dirichlet_prod' (dirichlet_prod f g) h x"
proof -
  have "dirichlet_prod' f (λy. dirichlet_prod' g h y) x =
          (m | m > 0  real m  x. n | n > 0  real n  x / m. f m * g n * h (x / (m * n)))"
    by (simp add: algebra_simps dirichlet_prod'_def dirichlet_prod_def
                  sum_upto_def sum_distrib_left sum_distrib_right)
  also have " = ((m,n)(SIGMA m:{m. m > 0  real m  x}. {n. n > 0  real n  x / m}).
                     f m * g n * h (x / (m * n)))"
    by (subst sum.Sigma) auto
  also have " = ((mn, m)(SIGMA mn:{mn. mn > 0  real mn  x}. {m. m dvd mn}).
                    f m * g (mn div m) * h (x / mn))"
    by (rule sum.reindex_bij_witness[of _ "λ(mn, m). (m, mn div m)" "λ(m, n). (m * n, m)"])
       (auto simp: case_prod_unfold field_simps dest: dvd_imp_le)
  also have " = dirichlet_prod' (dirichlet_prod f g) h x"
    by (subst sum.Sigma [symmetric])
       (simp_all add: dirichlet_prod'_def dirichlet_prod_def sum_upto_def
                      algebra_simps sum_distrib_left sum_distrib_right)
  finally show ?thesis .
qed

(* 2.22 *)
lemma dirichlet_prod'_inversion1:
  assumes "x1. g x = dirichlet_prod' a f x" "x  1"
          "dirichlet_prod a ainv = (λn. if n = 1 then 1 else 0)"
  shows   "f x = dirichlet_prod' ainv g x"
proof -
  have "dirichlet_prod' ainv g x = dirichlet_prod' ainv (dirichlet_prod' a f) x"
    using assms by (intro dirichlet_prod'_cong) auto
  also have " = dirichlet_prod' (λn. if n = 1 then 1 else 0) f x"
    using assms by (simp add: dirichlet_prod'_assoc dirichlet_prod_commutes)
  also have " = f x"
    using assms by (subst dirichlet_prod'_one_left) auto
  finally show ?thesis ..
qed

lemma dirichlet_prod'_inversion2:
  assumes "x1. f x = dirichlet_prod' ainv g x" "x  1"
          "dirichlet_prod a ainv = (λn. if n = 1 then 1 else 0)"
  shows   "g x = dirichlet_prod' a f x"
proof -
  have "dirichlet_prod' a f x = dirichlet_prod' a (dirichlet_prod' ainv g) x"
    using assms by (intro dirichlet_prod'_cong) auto
  also have " = dirichlet_prod' (λn. if n = 1 then 1 else 0) g x"
    using assms by (simp add: dirichlet_prod'_assoc dirichlet_prod_commutes)
  also have " = g x"
    using assms by (subst dirichlet_prod'_one_left) auto
  finally show ?thesis ..
qed

lemma dirichlet_prod'_inversion:
  assumes "dirichlet_prod a ainv = (λn. if n = 1 then 1 else 0)"
  shows   "(x1. g x = dirichlet_prod' a f x)  (x1. f x = dirichlet_prod' ainv g x)"
  using dirichlet_prod'_inversion1[of g a f _ ainv] dirichlet_prod'_inversion2[of f ainv g _ a]
        assms by blast

lemma dirichlet_prod'_inversion':
  assumes "a 1 * y = 1"
  defines "ainv  dirichlet_inverse a y"
  shows   "(x1. g x = dirichlet_prod' a f x)  (x1. f x = dirichlet_prod' ainv g x)"
  unfolding ainv_def
  by (intro dirichlet_prod'_inversion dirichlet_prod_inverse assms)

(* 3.11 *)
lemma dirichlet_prod'_floor_conv_sum_upto:
  "dirichlet_prod' f (λx. real_of_int (floor x)) x = sum_upto (λn. sum_upto f (x / n)) x"
proof -
  have [simp]: "sum_upto (λ_. 1 :: real) x = real (nat x)" for x
    by (simp add: sum_upto_altdef)
  show ?thesis
    using sum_upto_dirichlet_prod[of "λn. 1::real" f] sum_upto_dirichlet_prod[of f "λn. 1::real"]
    by (simp add: dirichlet_prod'_def dirichlet_prod_commutes)
qed

lemma (in completely_multiplicative_function) dirichlet_prod_self:
  "dirichlet_prod f f n = f n * of_nat (divisor_count n)"
proof (cases "n = 0")
  case False
  have "dirichlet_prod f f n = ((r, d) | r * d = n. f (r * d))"
    by (simp add: dirichlet_prod_altdef2 mult)
  also have " = ((r, d) | r * d = n. f n)"
    by (intro sum.cong) auto
  also have " = f n * of_nat (card {(r, d). r * d = n})"
    by (simp add: mult.commute)
  also have "bij_betw fst {(r, d). r * d = n} {r. r dvd n}"
    by (rule bij_betwI[of _ _ _ "λr. (r, n div r)"]) (use False in auto)
  hence "card {(r, d). r * d = n} = card {r. r dvd n}"
    by (rule bij_betw_same_card)
  also have " = divisor_count n"
    by (simp add: divisor_count_def)
  finally show ?thesis .
qed auto

lemma completely_multiplicative_imp_moebius_mu_inverse:
  fixes f :: "nat  'a :: {comm_ring_1}"
  assumes "completely_multiplicative_function f"
  shows   "dirichlet_prod f (λn. moebius_mu n * f n) n = (if n = 1 then 1 else 0)"
proof -
  interpret completely_multiplicative_function f by fact
  have [simp]: "fds f  0" by (auto simp: fds_eq_iff)
  have "dirichlet_prod f (λn. moebius_mu n * f n) n =
          ((r, d) | r * d = n. moebius_mu r * f (r * d))"
    by (subst dirichlet_prod_commutes)
       (simp add: fds_eq_iff fds_nth_mult fds_nth_fds dirichlet_prod_altdef2 mult_ac mult)
  also have " = ((r, d) | r * d = n. moebius_mu r * f n)"
    by (intro sum.cong) auto
  also have " = dirichlet_prod moebius_mu (λ_. 1) n * f n"
    by (simp add: dirichlet_prod_altdef2 sum_distrib_right case_prod_unfold mult)
  also have "dirichlet_prod moebius_mu (λ_. 1) n = fds_nth (fds moebius_mu * fds_zeta) n"
    by (simp add: fds_nth_mult)
  also have "fds moebius_mu * fds_zeta = 1"
    by (simp add: mult_ac fds_zeta_times_moebius_mu)
  also have "fds_nth 1 n * f n = fds_nth 1 n"
    by (auto simp: fds_eq_iff fds_nth_one)
  finally show ?thesis by (simp add: fds_nth_one)
qed

(* 2.23 *)
lemma dirichlet_prod_inversion_completely_multiplicative:
  fixes a :: "nat  'a :: comm_ring_1"
  assumes "completely_multiplicative_function a"
  shows   "(x1. g x = dirichlet_prod' a f x) 
             (x1. f x = dirichlet_prod' (λn. moebius_mu n * a n) g x)"
  by (intro dirichlet_prod'_inversion ext completely_multiplicative_imp_moebius_mu_inverse assms)

lemma divisor_sigma_conv_dirichlet_prod:
  "divisor_sigma x n = dirichlet_prod (λn. real n powr x) (λ_. 1) n"
proof (cases "n = 0")
  case False
  have "fds (divisor_sigma x) = fds_shift x fds_zeta * fds_zeta"
    using fds_divisor_sigma[of x] by (simp add: mult_ac)
  thus ?thesis using False by (auto simp: fds_eq_iff fds_nth_mult)
qed simp_all


subsection ‹Legendre's identity›

definition legendre_aux :: "real  nat  nat" where
  "legendre_aux x p = (if prime p then (m | m > 0  real (p ^ m)  x. nat x / p ^ m) else 0)"

lemma legendre_aux_not_prime [simp]: "¬prime p  legendre_aux x p = 0"
  by (simp add: legendre_aux_def)

lemma legendre_aux_eq_0:
  assumes "real p > x"
  shows   "legendre_aux x p = 0"
proof (cases "prime p")
  case True
  have [simp]: "¬real p ^ m  x" if "m > 0" for m
  proof -
    have "x < real p ^ 1" using assms by simp
    also have "  real p ^ m"
      using prime_gt_1_nat[OF True] that by (intro power_increasing) auto
    finally show ?thesis by auto
  qed
  from assms have *: "{m. m > 0  real (p ^ m)  x} = {}"
    using prime_gt_1_nat[OF True] by auto
  show ?thesis unfolding legendre_aux_def
    by (subst *) auto
qed (auto simp: legendre_aux_def)

lemma legendre_aux_posD:
  assumes "legendre_aux x p > 0"
  shows   "prime p" "real p  x"
proof -
  show "real p  x" using legendre_aux_eq_0[of x p] assms
    by (cases "real p  x") auto
qed (use assms in auto simp: legendre_aux_def split: if_splits›)

lemma exponents_le_finite:
  assumes "p > (1 :: nat)" "k > 0"
  shows   "finite {i. real (p ^ (k * i + l))  x}"
proof (rule finite_subset)
  show "{i. real (p ^ (k * i + l))  x}  {..nat x}"
  proof safe
    fix i assume i: "real (p ^ (k * i + l))  x"
    have "i < 2 ^ i" by (induction i) auto
    also from assms have "i  k * i + l" by (cases k) auto
    hence "2 ^ i  (2 ^ (k * i + l) :: nat)"
      using assms by (intro power_increasing) auto
    also have "  p ^ (k * i + l)" using assms by (intro power_mono) auto
    also have "real   x" using i by simp
    finally show "i  nat x" by linarith
  qed
qed auto

lemma finite_sum_legendre_aux: 
  assumes "prime p"
  shows   "finite {m. m > 0  real (p ^ m)  x}"
  by (rule finite_subset[OF _ exponents_le_finite[where k = 1 and l = 0 and p = p]])
     (use assms prime_gt_1_nat[of p] in auto)

lemma legendre_aux_set_eq:
  assumes "prime p" "x  1"
  shows   "{m. m > 0  real (p ^ m)  x} = {0<..nat log (real p) x}"
  using prime_gt_1_nat[OF assms(1)] assms
  by (auto simp: le_nat_iff le_log_iff le_floor_iff powr_realpow)

lemma legendre_aux_altdef1:
  "legendre_aux x p = (if prime p  x  1 then
                         (m{0<..nat log (real p) x}. nat x / p ^ m) else 0)"
proof (cases "prime p  x < 1")
  case False
  thus ?thesis using legendre_aux_set_eq[of p x] by (auto simp: legendre_aux_def)
next
  case True
  have [simp]: "¬(real p ^ m  x)" for m
  proof -
    have "x < real 1" using True by simp
    also have "real 1  real (p ^ m)"
      unfolding of_nat_le_iff by (intro one_le_power) (use prime_gt_1_nat[of p] True in auto)
    finally show "¬(real p ^ m  x)" by auto
  qed
  have "{m. m > 0  real (p ^ m)  x} = {}" by simp
  with True show ?thesis by (simp add: legendre_aux_def)
qed

lemma legendre_aux_altdef2:
  assumes "x  1" "prime p" "real p ^ Suc k > x"
  shows   "legendre_aux x p = (m{0<..k}. nat x / p ^ m)"
proof -
  have "legendre_aux x p = (m | m > 0  real (p ^ m)  x. nat x / p ^ m)"
    using assms by (simp add: legendre_aux_def)
  also have " = (m{0<..k}. nat x / p ^ m)"
  proof (intro sum.mono_neutral_left)
    show "{m. 0 < m  real (p ^ m)  x}  {0<..k}"
    proof safe
      fix m assume "m > 0" "real (p ^ m)  x"
      hence "real p ^ m  x" by simp
      also note x < real p ^ Suc k
      finally show "m  {0<..k}" using m > 0
        using prime_gt_1_nat[OF ‹prime p] by (subst (asm) power_strict_increasing_iff) auto
    qed
  qed (use prime_gt_0_nat[of p] assms in auto simp: field_simps)
  finally show ?thesis .
qed

(* 3.14 *)
theorem legendre_identity:
  "sum_upto ln x = prime_sum_upto (λp. legendre_aux x p * ln p) x"
proof -
  define S where "S = (SIGMA p:{p. prime p  real p  x}. {i. i > 0  real (p ^ i)  x})"

  have prime_power_leD: "real p  x" if "real p ^ i  x" "prime p" "i > 0" for p i
  proof -
    have "real p ^ 1  real p ^ i"
      using that prime_gt_1_nat[of p] by (intro power_increasing) auto
    also have "  x" by fact
    finally show "real p  x" by simp
  qed

  have "sum_upto ln x = sum_upto (λn. mangoldt n * real (nat x / real n)) x"
    by (rule sum_upto_ln_conv_sum_upto_mangoldt)
  also have " = ((p, i) | prime p  0 < i  real (p ^ i)  x.
                     ln p * real (nat x / real (p ^ i)))"
    by (subst sum_upto_primepows[where g = "λp i. ln p * real (nat x / real (p ^ i))"])
       (auto simp: mangoldt_non_primepow)
  also have " = ((p,i)S. ln p * real (nat x / p ^ i))"
    using prime_power_leD by (intro sum.cong refl) (auto simp: S_def)
  also have " = (p | prime p  real p  x. i | i > 0  real (p ^ i)  x.
                     ln p * real (nat x / p ^ i))"
  proof (unfold S_def, subst sum.Sigma)
    have "{p. prime p  real p  x}  {..nat x}"
      by (auto simp: le_nat_iff le_floor_iff)
    thus "finite {p. prime p  real p  x}"
      by (rule finite_subset) auto
  next
    show "p{p. prime p  real p  x}. finite {i. 0 < i  real (p ^ i)  x}"
      by (intro ballI finite_sum_legendre_aux) auto
  qed auto
  also have " = (p | prime p  real p  x. ln p *
                    real (i | i > 0  real (p ^ i)  x. (nat x / p ^ i)))"
    by (simp add: sum_distrib_left)
  also have " = (p | prime p  real p  x. ln p * real (legendre_aux x p))"
    by (intro sum.cong refl) (auto simp: legendre_aux_def)
  also have " = prime_sum_upto (λp. ln p * real (legendre_aux x p)) x"
    by (simp add: prime_sum_upto_def)
  finally show ?thesis by (simp add: mult_ac)
qed

lemma legendre_identity':
  "fact (nat x) = (p | prime p  real p  x. p ^ legendre_aux x p)"
proof -
  have fin: "finite {p. prime p  real p  x}"
    by (rule finite_subset[of _ "{..nat x}"]) (auto simp: le_nat_iff le_floor_iff)
  have "real (fact (nat x)) = exp (sum_upto ln x)"
    by (subst sum_upto_ln_conv_ln_fact) auto
  also have "sum_upto ln x = prime_sum_upto (λp. legendre_aux x p * ln p) x"
    by (rule legendre_identity)
  also have "exp  = (p | prime p  real p  x. exp (ln (real p) * legendre_aux x p))"
    unfolding prime_sum_upto_def using fin by (subst exp_sum) (auto simp: mult_ac)
  also have " = (p | prime p  real p  x. real (p ^ legendre_aux x p))"
  proof (intro prod.cong refl)
    fix p assume "p  {p. prime p  real p  x}"
    hence "p > 0" using prime_gt_0_nat[of p] by auto
    from p > 0 have "exp (ln (real p) * legendre_aux x p) = real p powr real (legendre_aux x p)"
      by (simp add: powr_def)
    also from p > 0 have " = real (p ^ legendre_aux x p)"
      by (subst powr_realpow) auto
    finally show "exp (ln (real p) * legendre_aux x p) = " .
  qed
  also have " = real (p | prime p  real p  x. p ^ legendre_aux x p)"
    by simp
  finally show ?thesis unfolding of_nat_eq_iff .
qed


subsection ‹A weighted sum of the Möbius μ› function›

(* TODO: Move to Dirichlet_Series? *)

(* 3.13 *)
context
  fixes M :: "real  real"
  defines "M  (λx. sum_upto (λn. moebius_mu n / n) x)"
begin

lemma abs_sum_upto_moebius_mu_over_n_less:
  assumes x: "x  2"
  shows   "¦M x¦ < 1"
proof -
  have "x * sum_upto (λn. moebius_mu n / n) x - sum_upto (λn. moebius_mu n * frac (x / n)) x =
          sum_upto (λn. moebius_mu n * (x / n - frac (x / n))) x"
    by (subst mult.commute[of x])
       (simp add: sum_upto_def sum_distrib_right sum_subtractf ring_distribs)
  also have "(λn. x / real n - frac (x / real n)) = (λn. of_int (floor (x / real n)))"
    by (simp add: frac_def)
  also have "sum_upto (λn. moebius_mu n * real_of_int x / real n) x =
               real_of_int (sum_upto (λn. moebius_mu n * x / real n) x)"
    by (simp add: sum_upto_def)
  also have " = 1"
    using x by (subst sum_upto_moebius_times_floor_linear) auto
  finally have eq: "x * M x = 1 + sum_upto (λn. moebius_mu n * frac (x / n)) x"
    by (simp add: M_def)

  have "x * ¦M x¦ = ¦x * M x¦"
    using x by (simp add: abs_mult)
  also note eq
  also have "¦1 + sum_upto (λn. moebius_mu n * frac (x / n)) x¦ 
               1 + ¦sum_upto (λn. moebius_mu n * frac (x / n)) x¦"
    by linarith
  also have "¦sum_upto (λn. moebius_mu n * frac (x / n)) x¦ 
               sum_upto (λn. ¦moebius_mu n * frac (x / n)¦) x"
    unfolding sum_upto_def by (rule sum_abs)
  also have "  sum_upto (λn. frac (x / n)) x"
    unfolding sum_upto_def by (intro sum_mono) (auto simp: moebius_mu_def abs_mult)
  also have " = (n{0<..nat x}. frac (x / n))"
    by (simp add: sum_upto_altdef)
  also have "{0<..nat x} = insert 1 {1<..nat x}"
    using x by (auto simp: le_nat_iff le_floor_iff)
  also have "(n. frac (x / n)) = frac x + (n{1<..nat x}. frac (x / n))"
    by (subst sum.insert) auto
  also have "(n{1<..nat x}. frac (x / n)) < (n{1<..nat x}. 1)"
    using x by (intro sum_strict_mono frac_lt_1) auto
  also have " = nat x - 1" by simp
  also have "1 + (frac x + real (nat x - 1)) = x"
    using x by (subst of_nat_diff) (auto simp: le_nat_iff le_floor_iff frac_def)
  finally have "x * ¦M x¦ < x * 1" by simp
  with x show "¦M x¦ < 1"
    by (subst (asm) mult_less_cancel_left_pos) auto
qed 

lemma sum_upto_moebius_mu_over_n_eq:
  assumes "x < 2"
  shows   "M x = (if x  1 then 1 else 0)"
proof (cases "x  1")
  case True
  have "M x = (n{n. n > 0  real n  x}. moebius_mu n / n)"
    by (simp add: M_def sum_upto_def)
  also from assms True have "{n. n > 0  real n  x} = {1}"
    by auto
  thus ?thesis using True by (simp add: M_def sum_upto_def)
next
  case False
  have "M x = (n{n. n > 0  real n  x}. moebius_mu n / n)"
    by (simp add: M_def sum_upto_def)
  also from False have "{n. n > 0  real n  x} = {}"
    by auto
  finally show ?thesis using False by (simp add: M_def)
qed

lemma abs_sum_upto_moebius_mu_over_n_le: "¦M x¦  1"
  using sum_upto_moebius_mu_over_n_eq[of x] abs_sum_upto_moebius_mu_over_n_less[of x]
  by (cases "x < 2") auto

end

end

Theory Primes_Omega

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

  The primes ω function (i.e. the number of distinct prime factors)
*)
section ‹The Prime ω› function›
theory Primes_Omega
  imports Dirichlet_Series.Dirichlet_Series Dirichlet_Series.Divisor_Count
begin

text ‹
  The prime ω› function $\omega(n)$ counts the number of distinct prime factors of n›.
›

definition primes_omega :: "nat  nat" where
  "primes_omega n = card (prime_factors n)"

lemma primes_omega_prime [simp]: "prime p  primes_omega p = 1"
  by (simp add: primes_omega_def prime_factorization_prime)

lemma primes_omega_0 [simp]: "primes_omega 0 = 0"
  by (simp add: primes_omega_def)

lemma primes_omega_1 [simp]: "primes_omega 1 = 0"
  by (simp add: primes_omega_def)

lemma primes_omega_Suc_0 [simp]: "primes_omega (Suc 0) = 0"
  by (simp add: primes_omega_def)

lemma primes_omega_power [simp]: "n > 0  primes_omega (x ^ n) = primes_omega x"
  by (simp add: primes_omega_def prime_factors_power)

lemma primes_omega_primepow [simp]: "primepow n  primes_omega n = 1"
  by (auto simp: primepow_def)

lemma primes_omega_eq_0_iff: "primes_omega n = 0  n = 0  n = 1"
  by (auto simp: primes_omega_def prime_factorization_empty_iff)

lemma primes_omega_pos [simp, intro]: "n > 1  primes_omega n > 0"
  by (cases "primes_omega n > 0") (auto simp: primes_omega_eq_0_iff)

lemma primes_omega_mult_coprime:
  assumes "coprime x y" "x > 0  y > 0"
  shows   "primes_omega (x * y) = primes_omega x + primes_omega y"
proof (cases "x = 0  y = 0")
  case False
  hence "prime_factors (x * y) = prime_factors x  prime_factors y"
    by (subst prime_factorization_mult) auto
  also {
    have "prime_factors x  prime_factors y = set_mset (prime_factorization (gcd x y))"
      using False by (subst prime_factorization_gcd) auto
    also have "gcd x y = 1" using ‹coprime x y by auto
    finally have "card (prime_factors x  prime_factors y) = primes_omega x + primes_omega y"
      unfolding primes_omega_def by (intro card_Un_disjoint) (use False in auto)
  }
  finally show ?thesis by (simp add: primes_omega_def)
qed (use assms in auto)

lemma divisor_count_squarefree:
  assumes "squarefree n" "n > 0"
  shows   "divisor_count n = 2 ^ primes_omega n"
proof -
  have "divisor_count n = (pprime_factors n. Suc (multiplicity p n))"
    using assms by (subst divisor_count.prod_prime_factors') auto
  also have " = (pprime_factors n. 2)"
    using assms assms by (intro prod.cong) (auto simp: squarefree_factorial_semiring')
  finally show ?thesis by (simp add: primes_omega_def)
qed

end

Theory Primorial

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

  The primorial function x#, i.\,e. the product of all primes no greater than x.
*)
section ‹The Primorial function›
theory Primorial
  imports Prime_Distribution_Elementary_Library Primes_Omega
begin

subsection ‹Definition and basic properties›

definition primorial :: "real  nat" where
  "primorial x = {p. prime p  real p  x}"

lemma primorial_mono: "x  y  primorial x  primorial y"
  unfolding primorial_def
  by (intro dvd_imp_le prod_dvd_prod_subset)
     (auto intro!: prod_pos finite_primes_le dest: prime_gt_0_nat)

lemma prime_factorization_primorial:
  "prime_factorization (primorial x) = mset_set {p. prime p  real p  x}"
proof (intro multiset_eqI)
  fix p :: nat
  note fin = finite_primes_le[of x]
  show "count (prime_factorization (primorial x)) p =
          count (mset_set {p. prime p  real p  x}) p"
  proof (cases "prime p")
    case True
    hence "count (prime_factorization (primorial x)) p =
             sum (multiplicity p) {p. prime p  real p  x}"
      unfolding primorial_def count_prime_factorization using fin
      by (subst prime_elem_multiplicity_prod_distrib) auto
    also from True have " = sum (λ_. 1) (if p  x then {p} else {})" using fin
      by (intro sum.mono_neutral_cong_right) (auto simp: prime_multiplicity_other split: if_splits)
    also have " = count (mset_set {p. prime p  real p  x}) p"
      using True fin by auto
    finally show ?thesis .
  qed auto
qed

lemma prime_factors_primorial [simp]:
  "prime_factors (primorial x) = {p. prime p  real p  x}"
  unfolding prime_factorization_primorial using finite_primes_le[of x] by simp

lemma primorial_pos [simp, intro]: "primorial x > 0"
  unfolding primorial_def by (intro prod_pos) (auto dest: prime_gt_0_nat)

lemma primorial_neq_zero [simp]: "primorial x  0"
  by auto

lemma of_nat_primes_omega_primorial [simp]: "real (primes_omega (primorial x)) = primes_pi x"
  by (simp add: primes_omega_def primes_pi_def prime_sum_upto_def)

lemma primes_omega_primorial: "primes_omega (primorial x) = nat primes_pi x"
  by (simp add: primes_omega_def primes_pi_def prime_sum_upto_def)

lemma prime_dvd_primorial_iff: "prime p  p dvd primorial x  p  x"
  using finite_primes_le[of x]
  by (auto simp: primorial_def prime_dvd_prod_iff dest: primes_dvd_imp_eq)

lemma squarefree_primorial [intro]: "squarefree (primorial x)"
  unfolding primorial_def
  by (intro squarefree_prod_coprime) (auto simp: squarefree_prime intro: primes_coprime)

lemma primorial_ge: "primorial x  2 powr primes_pi x"
proof -
  have "2 powr primes_pi x = real (p | prime p  real p  x. 2)"
    by (simp add: primes_pi_def prime_sum_upto_def powr_realpow)
  also have "(p | prime p  real p  x. 2)  (p | prime p  real p  x. p)"
    by (intro prod_mono) (auto dest: prime_gt_1_nat)
  also have " = primorial x" by (simp add: primorial_def)
  finally show ?thesis by simp
qed

lemma primorial_at_top: "filterlim primorial at_top at_top"
proof -
  have "filterlim (λx. real (primorial x)) at_top at_top"
  proof (rule filterlim_at_top_mono)
    show "eventually (λx. primorial x  2 powr primes_pi x) at_top"
      by (intro always_eventually primorial_ge allI)
    have "filterlim (λx. exp (ln 2 * primes_pi x)) at_top at_top"
      by (intro filterlim_compose[OF exp_at_top]
                filterlim_tendsto_pos_mult_at_top[OF tendsto_const] π_at_top) auto
    thus "filterlim (λx. 2 powr primes_pi x) at_top at_top"
      by (simp add: powr_def mult_ac)
  qed
  thus ?thesis unfolding filterlim_sequentially_iff_filterlim_real [symmetric] .
qed

lemma totient_primorial:
  "real (totient (primorial x)) =
     real (primorial x) * (p | prime p  real p  x. 1 - 1 / real p)" for x
proof -
  have "real (totient (primorial x)) =
          primorial x * (pprime_factors (primorial x). 1 - 1 / p)"
    by (rule totient_formula2)
  thus ?thesis by simp
qed

lemma ln_primorial: "ln (primorial x) = primes_theta x"
proof -
  have "finite {p. prime p  real p  x}"
    by (rule finite_subset[of _ "{..nat x}"]) (auto simp: le_nat_iff le_floor_iff)
  thus ?thesis unfolding of_nat_prod primorial_def
    by (subst ln_prod) (auto dest: prime_gt_0_nat simp: θ_def prime_sum_upto_def)
qed

lemma divisor_count_primorial: "divisor_count (primorial x) = 2 powr primes_pi x"
proof -
  have "divisor_count (primorial x) = (p | prime p  real p  x. divisor_count p)"
    unfolding primorial_def
    by (subst divisor_count.prod_coprime) (auto simp: primes_coprime)
  also have " = (p | prime p  real p  x. 2)"
    by (intro prod.cong divisor_count.prime) auto
  also have " = 2 powr primes_pi x"
    by (simp add: primes_pi_def prime_sum_upto_def powr_realpow)
  finally show ?thesis .
qed


subsection ‹An alternative view on primorials›

text ‹
  The following function is an alternative representation of primorials; instead of taking
  the product of all primes up to a given real bound x›, it takes the product of the first
  k› primes. This is sometimes more convenient.
›
definition primorial' :: "nat  nat" where
  "primorial' n = (k<n. nth_prime k)"

lemma primorial'_0 [simp]: "primorial' 0 = 1"
  and primorial'_1 [simp]: "primorial' 1 = 2"
  and primorial'_2 [simp]: "primorial' 2 = 6"
  and primorial'_3 [simp]: "primorial' 3 = 30"
  by (simp_all add: primorial'_def lessThan_nat_numeral)

lemma primorial'_Suc: "primorial' (Suc n) = nth_prime n * primorial' n"
  by (simp add: primorial'_def)

lemma primorial'_pos [intro]: "primorial' n > 0"
  unfolding primorial'_def by (auto intro: prime_gt_0_nat)

lemma primorial'_neq_0 [simp]: "primorial' n  0"
  by auto

lemma strict_mono_primorial': "strict_mono primorial'"
  unfolding strict_mono_Suc_iff
proof
  fix n :: nat
  have "primorial' n * 1 < primorial' n * nth_prime n"
    using prime_gt_1_nat[OF prime_nth_prime[of n]]
    by (intro mult_strict_left_mono) auto
  thus "primorial' n < primorial' (Suc n)"
    by (simp add: primorial'_Suc)
qed

lemma prime_factorization_primorial':
  "prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})"
proof -
  have "prime_factorization (primorial' k) = (i<k. prime_factorization (nth_prime i))"
    unfolding primorial'_def by (subst prime_factorization_prod) (auto intro: prime_gt_0_nat)
  also have " = (i<k. {#nth_prime i#})"
    by (intro sum.cong prime_factorization_prime) auto
  also have " = (pnth_prime ` {..<k}. {#p#})"
    by (subst sum.reindex) (auto intro: inj_onI)
  also have " = mset_set (nth_prime ` {..<k})"
    by simp
  finally show ?thesis .
qed

lemma prime_factors_primorial': "prime_factors (primorial' k) = nth_prime ` {..<k}"
  by (simp add: prime_factorization_primorial')

lemma primes_omega_primorial' [simp]: "primes_omega (primorial' k) = k"
  unfolding primes_omega_def prime_factors_primorial' by (subst card_image) (auto intro: inj_onI)

lemma squarefree_primorial' [intro]: "squarefree (primorial' x)"
  unfolding primorial'_def
  by (intro squarefree_prod_coprime) (auto intro: squarefree_prime intro: primes_coprime)

lemma divisor_count_primorial' [simp]: "divisor_count (primorial' k) = 2 ^ k"
  by (subst divisor_count_squarefree) auto

lemma totient_primorial':
  "totient (primorial' k) = primorial' k * (i<k. 1 - 1 / nth_prime i)"
  unfolding totient_formula2 prime_factors_primorial'
  by (subst prod.reindex) (auto intro: inj_onI)

lemma primorial_conv_primorial': "primorial x = primorial' (nat primes_pi x)"
  unfolding primorial_def primorial'_def
proof (rule prod.reindex_bij_witness[of _ nth_prime "λp. nat primes_pi (real p) - 1"])
  fix p assume p: "p  {p. prime p  real p  x}"
  have [simp]: "primes_pi 2 = 1" by (auto simp: eval_π)
  have "primes_pi p  1"
    using p π_mono[of 2 "real p"] by (auto dest!: prime_gt_1_nat)
  with p show "nth_prime (nat primes_pi p - 1) = p"
    using π_pos[of "real p"]
    by (intro nth_prime_eqI'')
       (auto simp: le_nat_iff le_floor_iff primes_pi_def prime_sum_upto_def of_nat_diff)
  from p have "nat primes_pi (real p)  nat primes_pi x"
    by (intro nat_mono floor_mono π_mono) auto
  hence "nat primes_pi (real p) - 1 < nat primes_pi x"
    using ‹primes_pi p  1 by linarith
  thus  "nat primes_pi (real p) - 1  {..<nat primes_pi x}" by simp
  show "nth_prime (nat primes_pi (real p) - 1) = p"
    using p ‹primes_pi p  1
    by (intro nth_prime_eqI'') (auto simp: le_nat_iff primes_pi_def prime_sum_upto_def)
next
  fix k assume k: "k  {..<nat primes_pi x}"
  thus *: "nat primes_pi (real (nth_prime k)) - 1 = k" by auto
  from k have "¬(x < 2)" by (intro notI) auto
  hence "x  2" by simp
  have "real (nth_prime k)  real (nth_prime (nat primes_pi x - 1))"
    using k by simp
  also have "  x"
    using nth_prime_partition''[of x] x  2 by auto
  finally show "nth_prime k  {p. prime p  real p  x}"
    by auto
qed

lemma primorial'_conv_primorial:
  assumes "n > 0"
  shows   "primorial' n = primorial (nth_prime (n - 1))"
proof -
  have "primorial (nth_prime (n - 1)) = (k<nat (int (n - 1) + 1). nth_prime k)"
    by (simp add: primorial_conv_primorial' primorial'_def)
  also have "nat (int (n - 1) + 1) = n"
    using assms by auto
  finally show ?thesis by (simp add: primorial'_def)
qed


subsection ‹Maximal compositeness of primorials›

text ‹
  Primorials are maximally composite, i.\,e.\ any number with k› distinct prime factors
  is as least as big as the primorial with k› distinct prime factors, and and number less
  than a primorial has strictly less prime factors.
›

lemma nth_prime_le_prime_sequence:
  fixes p :: "nat  nat"
  assumes "strict_mono_on p {..<n}" and "k. k < n  prime (p k)" and "k < n"
  shows   "nth_prime k  p k"
  using assms(3)
proof (induction k)
  case 0
  hence "prime (p 0)" by (intro assms)
  hence "p 0  2" by (auto dest: prime_gt_1_nat)
  thus ?case by simp
next
  case (Suc k)
  have IH: "Suc (nth_prime k)  Suc (p k)" using Suc by simp
  have "nth_prime (Suc k) = smallest_prime_beyond (Suc (nth_prime k))"
    by (simp add: nth_prime_Suc)
  also {
    have "Suc (nth_prime k)  Suc (p k)" using Suc by simp
    also have "  smallest_prime_beyond (Suc (p k))"
      by (rule smallest_prime_beyond_le)
    finally have "smallest_prime_beyond (Suc (nth_prime k))  smallest_prime_beyond (Suc (p k))"
      by (rule smallest_prime_beyond_smallest[OF prime_smallest_prime_beyond])
  }
  also have "p k < p (Suc k)"
    using Suc by (intro strict_mono_onD[OF assms(1)]) auto
  hence "smallest_prime_beyond (Suc (p k))  p (Suc k)"
    using Suc.prems by (intro smallest_prime_beyond_smallest assms) auto
  finally show ?case .
qed

theorem primorial'_primes_omega_le:
  fixes n :: nat
  assumes n: "n > 0"
  shows "primorial' (primes_omega n)  n"
proof (cases "n = 1")
  case True
  thus ?thesis by simp
next
  case False
  with assms have "n > 1" by simp
  define m where "m = primes_omega n"
  define P where "P = {p. prime p  real p  primes_pi n}"
  define ps where "ps = sorted_list_of_set (prime_factors n)"
  have set_ps: "set ps = prime_factors n" by (simp add: ps_def)
  have [simp]: "length ps = m" by (simp add: ps_def m_def primes_omega_def)
  have "sorted ps" "distinct ps" by (simp_all add: ps_def)
  hence mono: "strict_mono_on (λk. ps ! k) {..<m}"
    by (intro strict_mono_onI le_neq_trans) (auto simp: sorted_nth_mono distinct_conv_nth)
  from n > 1 have "m > 0"
    by (auto simp: m_def prime_factorization_empty_iff intro!: Nat.gr0I)

  have "primorial' m = (k<m. nth_prime k)"
    using m > 0 by (simp add: of_nat_diff primorial'_def m_def)
  also have "(k<m. nth_prime k)  (k<m. ps ! k ^ multiplicity (ps ! k) n)"
  proof (intro prod_mono conjI)
    fix i assume i: "i  {..<m}"
    hence p: "ps ! i  prime_factors n"
      using set_ps by (auto simp: set_conv_nth)
    with i set_ps have "nth_prime i  ps ! i"
      by (intro nth_prime_le_prime_sequence[where n = m] mono) (auto simp: set_conv_nth)
    also have "  ps ! i ^ multiplicity (ps ! i) n"
      using p by (intro self_le_power) (auto simp: prime_factors_multiplicity dest: prime_gt_1_nat)
    finally show "nth_prime i  " .
  qed auto
  also have " = (p(λi. ps ! i) ` {..<m}. p ^ multiplicity p n)"
    using ‹distinct ps by (subst prod.reindex) (auto intro!: inj_onI simp: distinct_conv_nth)
  also have "(λi. ps ! i) ` {..<m} = set ps"
    by (auto simp: set_conv_nth)
  also have "set ps = prime_factors n"
    by (simp add: set_ps)
  also have "(pprime_factors n. p ^ multiplicity p n) = n"
    using n > 1 by (intro prime_factorization_nat [symmetric]) auto
  finally show "primorial' m  n" .
qed

lemma primes_omega_less_primes_omega_primorial:
  fixes n :: nat
  assumes n: "n > 0" and "n < primorial x"
  shows "primes_omega n < primes_omega (primorial x)"
proof (cases "n > 1")
  case False
  have [simp]: "primes_pi 2 = 1" by (simp add: eval_π)
  from False assms have [simp]: "n = 1" by auto
  from assms have "¬(x < 2)"
    by (intro notI) (auto simp: primorial_conv_primorial')
  thus ?thesis using assms π_mono[of 2 x] by auto
next
  case True
  define m where "m = primes_omega n"
  have le: "primorial' m  n"
    using primorial'_primes_omega_le[of n] n > 1 by (simp add: m_def primes_omega_def)
  also have " < primorial x" by fact
  also have " = primorial' (nat primes_pi x)"
    by (simp add: primorial_conv_primorial')
  finally have "m < nat primes_pi x"
    using strict_mono_less[OF strict_mono_primorial'] by simp
  hence "m < primes_pi x" by linarith
  also have " = primes_omega (primorial x)" by simp
  finally show ?thesis unfolding m_def of_nat_less_iff .
qed

lemma primes_omega_le_primes_omega_primorial:
  fixes n :: nat
  assumes "n  primorial x"
  shows   "primes_omega n  primes_omega (primorial x)"
proof -
  consider "n = 0" | "n > 0" "n = primorial x" | "n > 0" "n  primorial x" by force
  thus ?thesis
    by cases (use primes_omega_less_primes_omega_primorial[of n x] assms in auto)
qed

end

Theory Lcm_Nat_Upto

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

  The LCM of {1..n}, including the relationship Lcm {1..n} = exp (ψ n).
*)

section ‹The LCM of the first $n$ natural numbers›
theory Lcm_Nat_Upto
  imports Prime_Number_Theorem.Prime_Counting_Functions
begin

text ‹
  In this section, we examine @{term "Lcm {1..(n::nat)}"}. In particular,
  we will show that it is equal to $e^{\psi(n)}$ and thus (by the PNT) $e^{n + o(n)}$.
›
lemma multiplicity_Lcm:
  fixes A :: "'a :: {semiring_Gcd, factorial_semiring_gcd} set"
  assumes "finite A" "A  {}" "prime p" "0  A"
  shows   "multiplicity p (Lcm A) = Max (multiplicity p ` A)"
  using assms
proof (induction A rule: finite_ne_induct)
  case (insert x A)
  have "Lcm (insert x A) = lcm x (Lcm A)" by simp
  also have "multiplicity p  = Max (multiplicity p ` insert x A)"
    using insert by (subst multiplicity_lcm) (auto simp: Lcm_0_iff)
  finally show ?case by simp
qed auto

text ‹
  The multiplicity of any prime p› in @{term "Lcm {1..(n::nat)}"} differs from
  that in @{term "Lcm {1..(n - 1 :: nat)}"} iff n› is a power of p›, in which case
  it is greater by 1.
›
lemma multiplicity_Lcm_atLeast1AtMost_Suc:
  fixes p n :: nat
  assumes p: "prime p" and n: "n > 0"
  shows "multiplicity p (Lcm {1..Suc n}) =
           (if k. Suc n = p ^ k then 1 else 0) + multiplicity p (Lcm {1..n})"
proof -
  define k where "k = Max (multiplicity p ` {1..n})"
  define l where "l = multiplicity p (Suc n)"
  have eq: "{1..Suc n} = insert (Suc n) {1..n}" by auto
  from ‹prime p have "p > 1" by (auto dest: prime_gt_1_nat)

  have "multiplicity p (Lcm {1..Suc n}) = Max (multiplicity p ` {1..Suc n})"
    using assms by (subst multiplicity_Lcm) auto
  also have "multiplicity p ` {1..Suc n} =
               insert (multiplicity p (Suc n)) (multiplicity p ` {1..n})"
    by (simp only: eq image_insert)
  also have "Max  = max l k"
    unfolding l_def k_def using assms by (subst Max.insert) auto
  also have " = (if k. Suc n = p ^ k then 1 else 0) + k"
  proof (cases "k. Suc n = p ^ k")
    case False
    have "p ^ l dvd Suc n"
      unfolding l_def by (intro multiplicity_dvd)
    hence "p ^ l  Suc n"
      unfolding l_def by (intro dvd_imp_le multiplicity_dvd) auto
    moreover have "Suc n  p ^ l" using False by blast
    ultimately have "p ^ l < Suc n" by linarith
    moreover have "p ^ l > 0" using p > 1 by (intro zero_less_power) auto
    ultimately have "l = multiplicity p (p ^ l)" and "p ^ l  {1..n}"
      using ‹prime p by auto
    hence "l  k" unfolding k_def by (intro Max.coboundedI) auto
    with False show ?thesis by (simp add: l_def k_def)
  next
    case True
    then obtain x where x: "Suc n = p ^ x" by blast
    from x and n > 0 have "x > 0" by (intro Nat.gr0I) auto
    from x have [simp]: "l = x" using ‹prime p by (simp add: l_def)
    have "x = k + 1"
    proof (intro antisym)
      have "p ^ (x - 1) < Suc n"
        using x > 0 p > 1 unfolding x by (intro power_strict_increasing) auto
      moreover have "p ^ (x - 1) > 0"
        using p > 1 by (intro zero_less_power) auto
      ultimately have "multiplicity p (p ^ (x - 1)) = x - 1" and "p ^ (x - 1)  {1..n}"
        using ‹prime p by auto
      hence "x - 1  k"
        unfolding k_def by (intro Max.coboundedI) force+
      thus "x  k + 1" by linarith
    next
      have "multiplicity p y < x" if "y  {1..n}" for y
      proof -
        have "p ^ multiplicity p y  y"
          using that by (intro dvd_imp_le multiplicity_dvd) auto
        also have " < Suc n" using that by simp
        also have " = p ^ x" by (fact x)
        finally show "multiplicity p y < x"
          using p > 1 by (subst (asm) power_strict_increasing_iff)
      qed
      hence "k < x"
        using n > 0 unfolding k_def by (subst Max_less_iff) auto
      thus "k + 1  x" by simp
    qed
    thus ?thesis using True by simp
  qed
  also have "k = multiplicity p (Lcm {1..n})"
    unfolding k_def using n > 0 and ‹prime p by (subst multiplicity_Lcm) auto
  finally show ?thesis .
qed

text ‹
  Consequently, term‹Lcm {1..(n::nat)} differs from term‹Lcm {1..(n-1::nat)}
  iff n› is of the form $p^k$ for some prime $p$, in which case it is greater by a factor
  of p›.
›
lemma Lcm_atLeast1AtMost_Suc:
  "Lcm {1..Suc n} = Lcm {1..n} * (if primepow (Suc n) then aprimedivisor (Suc n) else 1)"
proof (cases "n > 0")
  case True
  show ?thesis
  proof (rule multiplicity_eq_nat)
    fix p :: nat assume "prime p"
    define x where "x = (if primepow (Suc n) then aprimedivisor (Suc n) else 1)"
    have "x > 0"
      using n > 0 by (auto simp: x_def intro!: aprimedivisor_pos_nat)
  
    have "multiplicity p (Lcm {1..n} * x) = multiplicity p (Lcm {1..n}) + multiplicity p x"
      using ‹prime p x > 0 by (subst prime_elem_multiplicity_mult_distrib) auto
    also consider "k. Suc n = p ^ k" | "primepow (Suc n)" "¬(k. Suc n = p ^ k)" 
                | "¬primepow (Suc n)" by blast
    hence "multiplicity p x = (if k. Suc n = p ^ k then 1 else 0)"
    proof cases
      assume "k. Suc n = p ^ k"
      thus ?thesis using ‹prime p n > 0
        by (auto simp: x_def aprimedivisor_prime_power intro!: Nat.gr0I)
    next
      assume *: "primepow (Suc n)" "k. Suc n = p ^ k"
      then obtain q k where qk: "prime q" "Suc n = q ^ k" "k > 0" "q  p"
        by (auto simp: primepow_def)
      thus ?thesis using ‹prime p
        by (subst *) (auto simp: x_def aprimedivisor_prime_power prime_multiplicity_other)
    next
      assume *: "¬primepow (Suc n)"
      hence **: "k. Suc n = p ^ k" using ‹prime p n > 0 by auto
      from * show ?thesis unfolding x_def
        by (subst **) auto
    qed
    also have "multiplicity p (Lcm {1..n}) +  = multiplicity p (Lcm {1..Suc n})"
      using ‹prime p n > 0 by (subst multiplicity_Lcm_atLeast1AtMost_Suc) (auto simp: x_def)
    finally show "multiplicity p (Lcm {1..Suc n}) = multiplicity p (Lcm {1..n} * x)" ..
  qed (use n > 0 in auto intro!: Nat.gr0I dest: aprimedivisor_pos_nat›) 
qed auto

text ‹
  It follows by induction that $\text{Lcm}\ \{1..n\} = e^{\psi(n)}$.
›
lemma Lcm_atLeast1AtMost_conv_ψ:
  includes prime_counting_notation
  shows "real (Lcm {1..n}) = exp (ψ (real n))"
proof (induction n)
  case (Suc n)
  have "real (Lcm {1..Suc n}) =
          real (Lcm {1..n}) * (if primepow (Suc n) then aprimedivisor (Suc n) else 1)"
    by (subst Lcm_atLeast1AtMost_Suc) auto
  also {
    assume "primepow (Suc n)"
    hence "Suc n > Suc 0" by (rule primepow_gt_Suc_0)
    hence "aprimedivisor (Suc n) > 0" by (intro aprimedivisor_pos_nat) auto
  }
  hence "(if primepow (Suc n) then aprimedivisor (Suc n) else 1) = exp (mangoldt (Suc n))"
    by (simp add: mangoldt_def)
  also have "Lcm {1..n} *  = exp (ψ (real n + 1))"
    using Suc.IH by (simp add: primes_psi_def sum_upto_plus1 exp_add)
  finally show ?case by (simp add: add_ac)
qed simp_all

lemma Lcm_upto_real_conv_ψ:
  includes prime_counting_notation
  shows "real (Lcm {1..nat x}) = exp (ψ x)"
  by (subst Lcm_atLeast1AtMost_conv_ψ) (simp add: primes_psi_def sum_upto_altdef)

end

Theory 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

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)"
          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_field_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_field_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_field_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 (λa. a powr - s) {1..}  mono_on (λx. - (x powr - s)) {1..}"
    using assms by (intro disjI2) (auto intro!: mono_onI powr_mono2')

  from assms have "s < 1  s > 1" by linarith
  hence "mono_on (λa. a powr (1 - s) / (1 - s) + z) {1..}"
  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 (λa. a powr (1 - s) / (1 - s) + z) {1..} 
        mono_on (λx. - (x powr (1 - s) / (1 - s) + z)) {1..}" 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 (λa. 1) {1..}  mono_on (λx::real. -1 :: real) {1..}"
      using assms by (intro disjI2) (auto intro!: mono_onI powr_mono2')
  
    from assms have "s < 1  s > 1" by linarith
    hence "mono_on (λa. a powr (1 - s) / (1 - s)) {1..}"
    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 (λa. a powr (1 - s) / (1 - s)) {1..} 
          mono_on (λx. - (x powr (1 - s) / (1 - s))) {1..}" 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:
  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 (λa. a powr s) {1..}  mono_on (λx. - (x powr s)) {1..}"
    using assms by (intro disjI1) (auto intro!: mono_onI powr_mono2)
  show "mono_on (λa. a powr (1 + s) / (1 + s)) {1..} 
        mono_on (λx. - (x powr (1 + s) / (1 + s))) {1..}"
    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

Theory Moebius_Mu_Sum

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

  Properties of the summatory Möbius μ function, including its relationship to
  the Prime Number Theorem.
*)
section ‹The summatory Möbius μ› function›
theory Moebius_Mu_Sum
imports
  More_Dirichlet_Misc
  Dirichlet_Series.Partial_Summation
  Prime_Number_Theorem.Prime_Counting_Functions
  Dirichlet_Series.Arithmetic_Summatory_Asymptotics
  Shapiro_Tauberian
  Partial_Zeta_Bounds
  Prime_Number_Theorem.Prime_Number_Theorem_Library
  Prime_Distribution_Elementary_Library
begin

text ‹
  In this section, we shall examine the summatory Möbius μ› function
  $M(x) := \sum_{n\leq x} \mu(n)$. The main result is that $M(x) \in o(x)$ is equivalent
  to the Prime Number Theorem.
›

context
  includes prime_counting_notation
  fixes M H :: "real  real"
  defines "M  sum_upto moebius_mu"
  defines "H  sum_upto (λn. moebius_mu n * ln n)"
begin

lemma sum_upto_moebius_mu_integral: "x > 1  ((λt. M t / t) has_integral M x * ln x - H x) {1..x}"
  and sum_upto_moebius_mu_integrable: "a  1  (λt. M t / t) integrable_on {a..b}"
proof -
  {
    fix a b :: real
    assume ab: "a  1" "a < b"
    have "((λt. M t * (1 / t)) has_integral M b * ln b - M a * ln a -
            (nreal -` {a<..b}. moebius_mu n * ln (real n))) {a..b}"
      unfolding M_def using ab
      by (intro partial_summation_strong [where X = "{}"])
         (auto intro!: derivative_eq_intros continuous_intros
               simp flip: has_field_derivative_iff_has_vector_derivative)
  } note * = this
  {
    fix x :: real assume x: "x > 1"
    have "(nreal -` {1<..x}. moebius_mu n * ln (real n)) = H x"
      unfolding H_def sum_upto_def by (intro sum.mono_neutral_cong_left) (use x in auto)
    thus "((λt. M t / t) has_integral M x * ln x - H x) {1..x}" using *[of 1 x] x by simp
  }
  {
    fix a b :: real assume ab: "a  1"
    show "(λt. M t / t) integrable_on {a..b}"
      using *[of a b] ab
      by (cases a b rule: linorder_cases) (auto intro: integrable_negligible)
  }
qed

lemma sum_moebius_mu_bound:
  assumes "x  0"
  shows   "¦M x¦  x"
proof -
  have "¦M x¦  sum_upto (λn. ¦moebius_mu n¦) x"
    unfolding M_def sum_upto_def by (rule sum_abs)
  also have "  sum_upto (λn. 1) x"
    unfolding sum_upto_def by (intro sum_mono) (auto simp: moebius_mu_def)
  also have "  x" using assms
    by (simp add: sum_upto_altdef)
  finally show ?thesis .
qed

lemma sum_moebius_mu_aux1: "(λx. M x / x - H x / (x * ln x))  O(λx. 1 / ln x)"
proof -
  define R where "R = (λx. integral {1..x} (λt. M t / t))"
  have "eventually (λx. M x / x - H x / (x * ln x) = R x / (x * ln x)) at_top"
    using eventually_gt_at_top[of 1]
  proof eventually_elim
    case (elim x)
    thus ?case
      using sum_upto_moebius_mu_integral[of x] by (simp add: R_def has_integral_iff field_simps)
  qed
  hence "(λx. M x / x - H x / (x * ln x))  Θ(λx. R x / (x * ln x))"
    by (intro bigthetaI_cong)
  also have "(λx. R x / (x * ln x))  O(λx. x / (x * ln x))"
  proof (intro landau_o.big.divide_right)
    have "M  O(λx. x)"
      using sum_moebius_mu_bound
      by (intro bigoI[where c = 1] eventually_mono[OF eventually_ge_at_top[of 0]]) auto
    hence "(λt. M t / t)  O(λt. 1)"
      by (simp add: landau_divide_simps)
    thus "R  O(λx. x)"
      unfolding R_def
      by (intro integral_bigo[where g' = "λ_. 1"])
         (auto simp: filterlim_ident has_integral_iff intro!: sum_upto_moebius_mu_integrable)
  qed (intro eventually_mono[OF eventually_gt_at_top[of 1]], auto)
  also have "(λx::real. x / (x * ln x))  Θ(λx. 1 / ln x)"
    by real_asymp
  finally show ?thesis .
qed

(* 4.13 *)
lemma sum_moebius_mu_aux2: "((λx. M x / x - H x / (x * ln x))  0) at_top"
proof -
  have "(λx. M x / x - H x / (x * ln x))  O(λx. 1 / ln x)"
    by (rule sum_moebius_mu_aux1)
  also have "(λx. 1 / ln x)  o(λ_. 1 :: real)"
    by real_asymp
  finally show ?thesis by (auto dest!: smalloD_tendsto)
qed

lemma sum_moebius_mu_ln_eq: "H = (λx. - dirichlet_prod' moebius_mu ψ x)"
proof
  fix x :: real
  have "fds mangoldt = (fds_deriv (fds moebius_mu) * fds_zeta :: real fds)"
    using fds_mangoldt' by (simp add: mult_ac)
  hence eq: "fds_deriv (fds moebius_mu) = fds moebius_mu * (fds mangoldt :: real fds)"
    by (subst (asm) fds_moebius_inversion [symmetric])
  have "-H x = sum_upto (λn. -ln n * moebius_mu n) x"
    by (simp add: H_def sum_upto_def sum_negf mult_ac)
  also have " = sum_upto (λn. dirichlet_prod moebius_mu mangoldt n) x"
    using eq by (intro sum_upto_cong) (auto simp: fds_eq_iff fds_nth_deriv fds_nth_mult)
  also have " = dirichlet_prod' moebius_mu ψ x"
    by (subst sum_upto_dirichlet_prod) (simp add: primes_psi_def dirichlet_prod'_def)
  finally show "H x = -dirichlet_prod' moebius_mu ψ x"
    by simp
qed

(* 4.14 *)
theorem PNT_implies_sum_moebius_mu_sublinear:
  assumes "ψ ∼[at_top] (λx. x)"
  shows   "M  o(λx. x)"
proof -
  have "((λx. H x / (x * ln x))  0) at_top"
  proof (rule tendstoI)
    fix ε' :: real assume ε': "ε' > 0"
    define ε where "ε = ε' / 2"
    from ε' have ε: "ε > 0" by (simp add: ε_def)
    from assms have "((λx. ψ x / x)  1) at_top"
      by (elim asymp_equivD_strong) (auto intro!: eventually_mono[OF eventually_gt_at_top[of 0]])
    from tendstoD[OF this ε] have "eventually (λx. ¦ψ x / x - 1¦ < ε) at_top"
      by (simp add: dist_norm)
    hence "eventually (λx. ¦ψ x - x¦ < ε * x) at_top"
      using eventually_gt_at_top[of 0] by eventually_elim (auto simp: abs_if field_simps)
    then obtain A' where A': "x. x  A'  ¦ψ x - x¦ < ε * x"
      by (auto simp: eventually_at_top_linorder)
    define A where "A = max 2 A'"
    from A' have A: "A  2" "x. x  A  ¦ψ x - x¦ < ε * x"
      by (auto simp: A_def)
  
    have H_bound: "¦H x¦ / (x * ln x)  (1 + ε + ψ A) / ln x + ε" if "x  A" for x
    proof -
      from x  A have "x  2" using A(1) by linarith
      note x = x  A x  2
  
      define y where "y = nat floor (x / A)"
      have "real y = real_of_int x / A" using A x by (simp add: y_def)
      also have "real_of_int x / A  x / A" by linarith
      also have "  x" using x A(1) by (simp add: field_simps)
      finally have "y  x" .
      have "y  1" using x A(1) by (auto simp: y_def le_nat_iff le_floor_iff)
      note y = y  1 y  x
  
      define S1 where [simp]: "S1 = sum_upto (λm. moebius_mu m * ψ (x / m)) y"
      define S2 where [simp]: "S2 = (m | m > y  real m  x. moebius_mu m * ψ (x / m))"
  
      have fin: "finite {m. y < m  real m  x}"
        by (rule finite_subset[of _ "{..nat x}"]) (auto simp: le_nat_iff le_floor_iff)
      have "H x = -dirichlet_prod' moebius_mu ψ x"
        by (simp add: sum_moebius_mu_ln_eq)
      also have "dirichlet_prod' moebius_mu ψ x =
                   (m | m > 0  real m  x. moebius_mu m * ψ (x / m))"
        unfolding dirichlet_prod'_def sum_upto_def ..
      also have "{m. m > 0  real m  x} = {0<..y}  {m. y < m  real m  x}"
        using x y A(1) by auto
      also have "(m. moebius_mu m * ψ (x / m)) = S1 + S2"
        unfolding dirichlet_prod'_def sum_upto_def S1_def S2_def using fin
        by (subst sum.union_disjoint) (auto intro: sum.cong)
      finally have abs_H_eq: "¦H x¦ = ¦S1 + S2¦" by simp
  
      define S1_1 where [simp]: "S1_1 = sum_upto (λm. moebius_mu m / m) y"
      define S1_2 where [simp]: "S1_2 = sum_upto (λm. moebius_mu m * (ψ (x / m) - x / m)) y"
  
      have "¦S1¦ = ¦x * S1_1 + S1_2¦"
        by (simp add: sum_upto_def sum_distrib_left sum_distrib_right
                      mult_ac sum_subtractf ring_distribs)
      also have "  x * ¦S1_1¦ + ¦S1_2¦"
        by (rule order.trans[OF abs_triangle_ineq]) (use x in simp add: abs_mult›)
      also have "  x * 1 + ε * x * (ln x + 1)"
      proof (intro add_mono mult_left_mono)
        show "¦S1_1¦  1"
          using abs_sum_upto_moebius_mu_over_n_le[of y] by simp
      next
        have "¦S1_2¦  sum_upto (λm. ¦moebius_mu m * (ψ (x / m) - x / m)¦) y"
          unfolding S1_2_def sum_upto_def by (rule sum_abs)
        also have "  sum_upto (λm. 1 * (ε * (x / m))) y"
          unfolding abs_mult sum_upto_def
        proof (intro sum_mono mult_mono less_imp_le[OF A(2)])
          fix m assume m: "m  {i. 0 < i  real i  real y}"
          hence "real m  real y" by simp
          also from x A(1) have " = of_int x / A" by (simp add: y_def)
          also have "  x / A" by linarith
          finally show "A  x / real m" using A(1) m by (simp add: field_simps)
        qed (auto simp: moebius_mu_def field_simps)
        also have " = ε * x * (i{0<..y}. inverse (real i))"
          by (simp add: sum_upto_altdef sum_distrib_left divide_simps)
        also have "(i{0<..y}. inverse (real i)) = harm (nat y)"
          unfolding harm_def by (intro sum.cong) auto
        also have "  ln (nat y) + 1"
          by (rule harm_le) (use y in auto)
        also have "ln (nat y)  ln x"
          using y by simp
        finally show "¦S1_2¦  ε * x * (ln x + 1)" using ε x by simp
      qed (use x in auto)
      finally have S1_bound: "¦S1¦  x + ε * x * ln x + ε * x"
        by (simp add: algebra_simps)
      
      have "¦S2¦  (m | y < m  real m  x. ¦moebius_mu m * ψ (x / m)¦)"
        unfolding S2_def by (rule sum_abs)
      also have "  (m | y < m  real m  x. 1 * ψ A)"
        unfolding abs_mult using y
      proof (intro sum_mono mult_mono)
        fix m assume m: "m  {m. y < m  real m  x}"
        hence "y < m" by simp
        moreover have "y = of_int x / A" using x A(1) by (simp add: y_def)
        ultimately have "x / A < m" by simp
        hence "x / A  real m" by linarith
        hence "ψ (x / real m)  ψ A"
          using m A(1) by (intro ψ_mono) (auto simp: field_simps)
        thus "¦ψ (x / real m)¦  ψ A"
          by (simp add: ψ_nonneg)
      qed (auto simp: moebius_mu_def ψ_nonneg field_simps intro!: ψ_mono)
      also have "  sum_upto (λ_. 1 * ψ A) x"
        unfolding sum_upto_def by (intro sum_mono2) auto
      also have " = real (nat x) * ψ A"
        by (simp add: sum_upto_altdef)
      also have "  x * ψ A"
        using x by (intro mult_right_mono) auto
      finally have S2_bound: "¦S2¦  x * ψ A" .
  
      have "¦H x¦  ¦S1¦ + ¦S2¦" using abs_H_eq by linarith
      also have "  x + ε * x * ln x + ε * x + x * ψ A"
        by (intro add_mono S1_bound S2_bound)
      finally have "¦H x¦  (1 + ε + ψ A) * x + ε * x * ln x"
        by (simp add: algebra_simps)
      thus "¦H x¦ / (x * ln x)  (1 + ε + ψ A) / ln x + ε"
        using x by (simp add: field_simps)
    qed
  
    have "eventually (λx. ¦H x¦ / (x * ln x)  (1 + ε + ψ A) / ln x + ε) at_top"
      using eventually_ge_at_top[of A] by eventually_elim (use H_bound in auto)
    moreover have "eventually (λx. (1 + ε + ψ A) / ln x + ε < ε') at_top"
      unfolding ε_def using ε' by real_asymp
    moreover have "eventually (λx. ¦H x¦ / (x * ln x) = ¦H x / (x * ln x)¦) at_top"
      using eventually_gt_at_top[of 1] by eventually_elim (simp add: abs_mult)
    ultimately have "eventually (λx. ¦H x / (x * ln x)¦ < ε') at_top"
      by eventually_elim simp
    thus "eventually (λx. dist (H x / (x * ln x)) 0 < ε') at_top"
      by (simp add: dist_norm)
  qed
  hence "(λx. H x / (x * ln x))  o(λ_. 1)"
    by (intro smalloI_tendsto) auto
  hence "(λx. H x / (x * ln x) + (M x / x - H x / (x * ln x)))  o(λ_. 1)"
  proof (rule sum_in_smallo)
    have "(λx. M x / x - H x / (x * ln x))  O(λx. 1 / ln x)"
      by (rule sum_moebius_mu_aux1)
    also have "(λx::real. 1 / ln x)  o(λ_. 1)"
      by real_asymp
    finally show "(λx. M x / x - H x / (x * ln x))  o(λ_. 1)" .
  qed
  thus ?thesis by (simp add: landau_divide_simps)
qed

(* 4.15 *)
theorem sum_moebius_mu_sublinear_imp_PNT:
  assumes "M  o(λx. x)"
  shows   "ψ ∼[at_top] (λx. x)"
proof -
  define σ :: "nat  real" where [simp]: "σ = (λn. real (divisor_count n))"
  define C where [simp]: "C = (euler_mascheroni :: real)"
  define f :: "nat  real" where "f = (λn. σ n - ln n - 2 * C)"
  define F where [simp]: "F = sum_upto f"
  write moebius_mu ("μ")

  ― ‹The proof is based on the fact that $\psi(x)-x$ can be approximated fairly well by
      the Dirichlet product $\sum_{n\leq x} \sum_{d\mid n} \mu(d) f(n/d)$:›
  have eq: "ψ x - x = -sum_upto (dirichlet_prod μ f) x - frac x - 2 * C" if x: "x  1" for x
  proof -
    have "x - ψ x - 2 * C =
            sum_upto (λ_. 1) x - sum_upto mangoldt x - sum_upto (λn. if n = 1 then 2 * C else 0) x"
      using x by (simp add: sum_upto_altdef ψ_def le_nat_iff le_floor_iff)
    also have " = sum_upto (λn. 1 - mangoldt n - (if n = 1 then 2 * C else 0)) x"
      by (simp add: sum_upto_def sum_subtractf)
    also have " = sum_upto (dirichlet_prod μ f) x"
      by (intro sum_upto_cong refl moebius_inversion)
         (auto simp: divisor_count_def sum_subtractf mangoldt_sum f_def)
    finally show "ψ x - x = -sum_upto (dirichlet_prod μ f) x - frac x - 2 * C"
      by (simp add: algebra_simps frac_def)
  qed

  ― ‹We now obtain a bound of the form ¦F x¦ ≤ B * sqrt x›.›
  have "F  O(sqrt)"
  proof -
    have "F  Θ(λx. (sum_upto σ x - (x * ln x + (2 * C - 1) * x)) -
                      (sum_upto ln x - x * ln x + x) + 2 * C * frac x)" (is "_  Θ(?rhs)")
      by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of 1]])
         (auto simp: sum_upto_altdef sum_subtractf f_def frac_def algebra_simps sum.distrib)
    also have "?rhs  O(sqrt)"
    proof (rule sum_in_bigo, rule sum_in_bigo)
      show "(λx. sum_upto σ x - (x * ln x + (2 * C - 1) * x))  O(sqrt)"
        unfolding C_def σ_def by (rule summatory_divisor_count_asymptotics)
      show "(λx. sum_upto (λx. ln (real x)) x - x * ln x + x)  O(sqrt)"
        by (rule landau_o.big.trans[OF sum_upto_ln_stirling_weak_bigo]) real_asymp
    qed (use euler_mascheroni_pos in real_asymp)
    finally show ?thesis .
  qed
  hence "(λn. F (real n))  O(sqrt)"
    by (rule landau_o.big.compose) real_asymp
  from natfun_bigoE[OF this, of 1] obtain B :: real
    where B: "B > 0" "n. n  1  ¦F (real n)¦  B * sqrt (real n)"
    by auto
  have B': "¦F x¦  B * sqrt x" if "x  1" for x
  proof -
    have "¦F x¦  B * sqrt (nat x)"
      using B(2)[of "nat x"] that by (simp add: sum_upto_altdef le_nat_iff le_floor_iff)
    also have "  B * sqrt x"
      using B(1) that by (intro mult_left_mono) auto
    finally show ?thesis .
  qed

  ― ‹Next, we obtain a good bound for $\sum_{n\leq x} \frac{1}{\sqrt{n}}$.›
  from zeta_partial_sum_le_pos''[of "1 / 2"] obtain A 
    where A: "A > 0" "x. x  1  ¦sum_upto (λn. 1 / sqrt n) x¦  A * sqrt x"
    by (auto simp: max_def powr_half_sqrt powr_minus field_simps)

  ― ‹Finally, we show that $\sum_{n\leq x} \sum_{d\mid n} \mu(d) f(n/d) \in o(x)$.›
  have "sum_upto (dirichlet_prod μ f)  o(λx. x)"
  proof (rule landau_o.smallI)
    fix ε :: real
    assume ε: "ε > 0"
  
    have *: "eventually (λx. ¦sum_upto (dirichlet_prod μ f) x¦  ε * x) at_top"
      if b: "b  1" "A * B / sqrt b  ε / 3" "B / sqrt b  ε / 3" for b
    proof -
      define K :: real where "K = sum_upto (λn. ¦f n¦ / n) b"
      have "C  (1 / 2)" using euler_mascheroni_gt_19_over_33 by auto
      hence K: "K > 0" unfolding K_def f_def sum_upto_def
        by (intro sum_pos2[where i = 1]) (use b  1 in auto)
      have "eventually (λx. ¦M x / x¦ < ε / 3 / K) at_top"
        using smalloD_tendsto[OF assms] ε K by (auto simp: tendsto_iff dist_norm)
      then obtain c' where c': "x. x  c'  ¦M x / x¦ < ε / 3 / K"
        by (auto simp: eventually_at_top_linorder)
      define c where "c = max 1 c'"
      have c: "¦M x¦ < ε / 3 / K * x" if "x  c" for x
        using c'[of x] that by (simp add: c_def field_simps)
  
      show "eventually (λx. ¦sum_upto (dirichlet_prod μ f) x¦  ε * x) at_top"
        using eventually_ge_at_top[of "b * c"] eventually_ge_at_top[of 1] eventually_ge_at_top[of b]
      proof eventually_elim
        case (elim x)
        define a where "a = x / b"
        from elim b  1 have ab: "a  1" "b  1" "a * b = x"
          by (simp_all add: a_def field_simps)
        from ab have "a * 1  a * b" by (intro mult_mono) auto
        hence "a  x" by (simp add: ab(3))
        from ab have "a * 1  a * b" and "1 * b  a * b" by (intro mult_mono; simp)+
        hence "a  x" "b  x" by (simp_all add: ab(3))
        have "a = x / b" "b = x / a" using ab by (simp_all add: field_simps)
  
        have "sum_upto (dirichlet_prod μ f) x =
                sum_upto (λn. μ n * F (x / n)) a + sum_upto (λn. M (x / n) * f n) b - M a * F b"
          unfolding M_def F_def by (rule hyperbola_method) (use ab in auto)
        also have "¦¦  ε / 3 * x + ε / 3 * x + ε / 3 * x"
        proof (rule order.trans[OF abs_triangle_ineq4] order.trans[OF abs_triangle_ineq] add_mono)+
          have "¦sum_upto (λn. μ n * F (x / real n)) a¦  sum_upto (λn. ¦μ n * F (x / real n)¦) a"
            unfolding sum_upto_def by (rule sum_abs)
          also have "  sum_upto (λn. 1 * (B * sqrt (x / real n))) a"
            unfolding sum_upto_def abs_mult using a  x
            by (intro sum_mono mult_mono B') (auto simp: moebius_mu_def)
          also have " = B * sqrt x * sum_upto (λn. 1 / sqrt n) a"
            by (simp add: sum_upto_def sum_distrib_left real_sqrt_divide)
          also have "  B * sqrt x * ¦sum_upto (λn. 1 / sqrt n) a¦"
            using B(1) x  1 by (intro mult_left_mono) auto
          also have "  B * sqrt x * (A * sqrt a)"
            using a  1 B(1) x  1 by (intro mult_left_mono A) auto
          also have " = A * B / sqrt b * x"
            using ab x  1x  1 by (subst a = x / b) (simp_all add: field_simps real_sqrt_divide)
          also have "  ε / 3 * x" using x  1 by (intro mult_right_mono b) auto
          finally show "¦sum_upto (λn. μ n * F (x / n)) a¦  ε / 3 * x" .
        next
          have "¦sum_upto (λn. M (x / n) * f n) b¦  sum_upto (λn. ¦M (x / n) * f n¦) b"
            unfolding sum_upto_def by (rule sum_abs)
          also have "  sum_upto (λn. ε / 3 / K * (x / n) * ¦f n¦) b"
            unfolding sum_upto_def abs_mult
          proof (intro sum_mono mult_right_mono)
            fix n assume n: "n  {n. n > 0  real n  b}"
            have "c  0" by (simp add: c_def)
            with n have "c * n  c * b" by (intro mult_left_mono) auto
            also have "  x" using b * c  x by (simp add: algebra_simps)
            finally show "¦M (x / real n)¦  ε / 3 / K * (x / real n)"
              by (intro less_imp_le[OF c]) (use n in auto simp: field_simps)
          qed auto
          also have " = ε / 3 * x / K * sum_upto (λn. ¦f n¦ / n) b"
            by (simp add: sum_upto_def sum_distrib_left)
          also have " = ε / 3 * x"
            unfolding K_def [symmetric] using K by simp
          finally show "¦sum_upto (λn. M (x / real n) * f n) b¦  ε / 3 * x" .
        next
          have "¦M a * F b¦  a * (B * sqrt b)"
            unfolding abs_mult using ab by (intro mult_mono sum_moebius_mu_bound B') auto
          also have " = B / sqrt b * x"
            using ab(1,2) by (simp add: real_sqrt_mult b = x / a real_sqrt_divide field_simps)
          also have "  ε / 3 * x" using x  1 by (intro mult_right_mono b) auto
          finally show "¦M a * F b¦  ε / 3 * x" .
        qed
        also have " = ε * x" by simp
        finally show ?case .
      qed
    qed
    
    have "eventually (λb::real. b  1  A * B / sqrt b  ε / 3  B / sqrt b  ε / 3) at_top"
      using ε by (intro eventually_conj; real_asymp)
    then obtain b where "b  1" "A * B / sqrt b  ε / 3" "B / sqrt b  ε / 3"
      by (auto simp: eventually_at_top_linorder)
    from *[OF this] have "eventually (λx. ¦sum_upto (dirichlet_prod μ f) x¦  ε * x) at_top" .
    thus "eventually (λx. norm (sum_upto (dirichlet_prod μ f) x)  ε * norm x) at_top"
      using eventually_ge_at_top[of 0] by eventually_elim simp
  qed

  have "(λx. ψ x - x)  Θ(λx. -(sum_upto (dirichlet_prod μ f) x + (frac x + 2 * C)))"
    by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of 1]], subst eq) auto
  hence "(λx. ψ x - x)  Θ(λx. sum_upto (dirichlet_prod μ f) x + (frac x + 2 * C))"
    by (simp only: landau_theta.uminus)
  also have "(λx. sum_upto (dirichlet_prod μ f) x + (frac x + 2 * C))  o(λx. x)"
    using ‹sum_upto (dirichlet_prod μ f)  o(λx. x) by (rule sum_in_smallo) real_asymp+
  finally show ?thesis by (rule smallo_imp_asymp_equiv)
qed


text ‹
  We now turn to a related fact: For the weighted sum $A(x) := \sum_{n\leq x} \mu(n)/n$, the
  asymptotic relation $A(x)\in o(1)$ is also equivalent to the Prime Number Theorem.
  Like Apostol, we only show one direction, namely that $A(x)\in o(1)$ implies the PNT.
›

context
  fixes A defines "A  sum_upto (λn. moebius_mu n / n)"
begin

lemma sum_upto_moebius_mu_integral': "x > 1  (A has_integral x * A x - M x) {1..x}"
  and sum_upto_moebius_mu_integrable': "a  1  A integrable_on {a..b}"
proof -
  {
    fix a b :: real
    assume ab: "a  1" "a < b"
    have "((λt. A t * 1) has_integral A b * b - A a * a -
            (nreal -` {a<..b}. moebius_mu n / n * n)) {a..b}"
      unfolding M_def A_def using ab
      by (intro partial_summation_strong [where X = "{}"])
         (auto intro!: derivative_eq_intros continuous_intros
               simp flip: has_field_derivative_iff_has_vector_derivative)
  } note * = this
  {
    fix x :: real assume x: "x > 1"
    have [simp]: "A 1 = 1" by (simp add: A_def)
    have "(nreal -` {1<..x}. moebius_mu n / n * n) =
            (ninsert 1 (real -` {1<..x}). moebius_mu n / n * n) - 1"
      using finite_vimage_real_of_nat_greaterThanAtMost[of 1 x] by (subst sum.insert) auto
    also have "insert 1 (real -` {1<..x}) = {n. n > 0  real n  x}"
      using x by auto
    also have "(n | 0 < n  real n  x. moebius_mu n / real n * real n) = M x"
      unfolding M_def sum_upto_def by (intro sum.cong) auto
    finally show "(A has_integral x * A x - M x) {1..x}" using *[of 1 x] x by (simp add: mult_ac)
  }
  {
    fix a b :: real assume ab: "a  1"
    show "A integrable_on {a..b}"
      using *[of a b] ab
      by (cases a b rule: linorder_cases) (auto intro: integrable_negligible)
  }
qed

(* 4.16 *)
theorem sum_moebius_mu_div_n_smallo_imp_PNT:
  assumes smallo: "A  o(λ_. 1)"
  shows   "M  o(λx. x)" and "ψ ∼[at_top] (λx. x)"
proof -
  have "eventually (λx. M x = x * A x - integral {1..x} A) at_top"
    using eventually_gt_at_top[of 1]
    by eventually_elim (use sum_upto_moebius_mu_integral' in simp add: has_integral_iff›)
  hence "M  Θ(λx. x * A x - integral {1..x} A)"
    by (rule bigthetaI_cong)
  also have "(λx. x * A x - integral {1..x} A)  o(λx. x)"
  proof (intro sum_in_smallo)
    from smallo show "(λx. x * A x)  o(λx. x)"
      by (simp add: landau_divide_simps)
    show "(λx. integral {1..x} A)  o(λx. x)"
      by (intro integral_smallo[OF smallo] sum_upto_moebius_mu_integrable')
         (auto intro!: derivative_eq_intros filterlim_ident)
  qed
  finally show "M  o(λx. x)" .
  thus "ψ ∼[at_top] (λx. x)"
    by (rule sum_moebius_mu_sublinear_imp_PNT)
qed

end

end

end

Theory Elementary_Prime_Bounds

(*
  File: