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_syntax
  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 -
            (∑n∈real -` {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_real_derivative_iff_has_vector_derivative)
  } note * = this
  {
    fix x :: real assume x: "x > 1"
    have "(∑n∈real -` {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 ≥ 1›‹x ≥ 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 -
            (∑n∈real -` {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_real_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 "(∑n∈real -` {1<..x}. moebius_mu n / n * n) =
            (∑n∈insert 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