Theory PNT_Consequences

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

  Some alternative forms and consequences of the Prime Number Theorem,
  including the asymptotics of the divisor function and Euler's totient function.
*)
section ‹Consequences of the Prime Number Theorem›
theory PNT_Consequences
imports
  Elementary_Prime_Bounds
  Prime_Number_Theorem.Mertens_Theorems
  Prime_Number_Theorem.Prime_Counting_Functions
  Moebius_Mu_Sum
  Lcm_Nat_Upto
  Primorial
  Primes_Omega
begin

text ‹
  In this section, we will define a locale that assumes the Prime Number Theorem in order to
  explore some of its elementary consequences.
›

(*<*)
unbundle prime_counting_notation
(*>*)

subsection ‹Statement and alternative forms of the PNT›

(*<*)
(* TODO: copied from afp-devel; delete in AFP 2019 *)
lemma PNT1_imp_PNT1':
  assumes "π ∼[at_top] (λx. x / ln x)"
  shows   "(λx. ln (π x)) ∼[at_top] ln"
proof -
  (* TODO: Tedious Landau sum reasoning *)
  from assms have "((λx. π x / (x / ln x))  1) at_top"
    by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto
  hence "((λx. ln (π x / (x / ln x)))  ln 1) at_top"
    by (rule tendsto_ln) auto
  also have "?this  ((λx. ln (π x) - ln x + ln (ln x))  0) at_top"
    by (intro filterlim_cong eventually_mono[OF eventually_gt_at_top[of 2]])
       (auto simp: ln_div field_simps ln_mult π_pos)
  finally have "(λx. ln (π x) - ln x + ln (ln x))  o(λ_. 1)"
    by (intro smalloI_tendsto) auto
  also have "(λ_::real. 1 :: real)  o(λx. ln x)"
    by real_asymp
  finally have "(λx. ln (π x) - ln x + ln (ln x) - ln (ln x))  o(λx. ln x)"
    by (rule sum_in_smallo) real_asymp+
  thus *: "(λx. ln (π x)) ∼[at_top] ln"
    by (simp add: asymp_equiv_altdef)
qed

lemma PNT1_imp_PNT2:
  assumes "π ∼[at_top] (λx. x / ln x)"
  shows   "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
proof -
  have "(λx. π x * ln (π x)) ∼[at_top] (λx. x / ln x * ln x)"
    by (intro asymp_equiv_intros assms PNT1_imp_PNT1')
  also have " ∼[at_top] (λx. x)"
    by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 1]])
       (auto simp: field_simps)
  finally show "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
    by simp
qed

lemma PNT2_imp_PNT3:
  assumes "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
  shows   "nth_prime ∼[at_top] (λn. n * ln n)"
proof -
  have "(λn. nth_prime n) ∼[at_top] (λn. π (nth_prime n) * ln (π (nth_prime n)))"
    using assms
    by (rule asymp_equiv_symI [OF asymp_equiv_compose'])
       (auto intro!: filterlim_compose[OF filterlim_real_sequentially nth_prime_at_top])
  also have " = (λn. real (Suc n) * ln (real (Suc n)))"
    by (simp add: add_ac)
  also have " ∼[at_top] (λn. real n * ln (real n))"
    by real_asymp
  finally show "nth_prime ∼[at_top] (λn. n * ln n)" .
qed

lemma PNT3_imp_PNT2:
  assumes "nth_prime ∼[at_top] (λn. n * ln n)"
  shows   "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
proof (rule asymp_equiv_symI, rule asymp_equiv_sandwich_real)
  show "eventually (λx. x  {real (nth_prime (nat π x - 1))..real (nth_prime (nat π x))})
          at_top"
    using eventually_ge_at_top[of 2]
  proof eventually_elim
    case (elim x)
    with nth_prime_partition''[of x] show ?case by auto
  qed
next
  have "(λx. real (nth_prime (nat π x - 1))) ∼[at_top]
           (λx. real (nat π x - 1) * ln (real (nat π x - 1)))"
    by (rule asymp_equiv_compose'[OF _ π_at_top], rule asymp_equiv_compose'[OF assms]) real_asymp
  also have " ∼[at_top] (λx. π x * ln (π x))"
    by (rule asymp_equiv_compose'[OF _ π_at_top]) real_asymp
  finally show "(λx. real (nth_prime (nat π x - 1))) ∼[at_top] (λx. π x * ln (π x))" .
next
  have "(λx. real (nth_prime (nat π x))) ∼[at_top]
           (λx. real (nat π x) * ln (real (nat π x)))"
    by (rule asymp_equiv_compose'[OF _ π_at_top], rule asymp_equiv_compose'[OF assms]) real_asymp
  also have " ∼[at_top] (λx. π x * ln (π x))"
    by (rule asymp_equiv_compose'[OF _ π_at_top]) real_asymp
  finally show "(λx. real (nth_prime (nat π x))) ∼[at_top] (λx. π x * ln (π x))" .
qed

lemma PNT2_imp_PNT1:
  assumes "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
  shows   "(λx. ln (π x)) ∼[at_top] (λx. ln x)"
    and   "π ∼[at_top] (λx. x / ln x)"
proof -
   have ev: "eventually (λx. π x > 0) at_top"
            "eventually (λx. ln (π x) > 0) at_top"
            "eventually (λx. ln (ln (π x)) > 0) at_top"
    by (rule eventually_compose_filterlim[OF _ π_at_top], real_asymp)+

  from assms have "((λx. π x * ln (π x) / x)  1) at_top"
    by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto
  hence "((λx. ln (π x * ln (π x) / x))  ln 1) at_top"
    by (rule tendsto_ln) auto
  moreover have "eventually (λx. ln (π x * ln (π x) / x) =
                   ln (π x) * (1 + ln (ln (π x)) / ln (π x) - ln x / ln (π x))) at_top"
      (is "eventually (λx. _ = _ * ?f x) _")
    using eventually_gt_at_top[of 0] ev
    by eventually_elim (simp add: field_simps ln_mult ln_div)
  ultimately have "((λx. ln (π x) * ?f x)  ln 1) at_top"
    by (rule Lim_transform_eventually)

  moreover have "((λx. 1 / ln (π x))  0) at_top"
    by (rule filterlim_compose[OF _ π_at_top]) real_asymp
  ultimately have "((λx. ln (π x) * ?f x * (1 / ln (π x)))  ln 1 * 0) at_top"
    by (rule tendsto_mult)
  moreover have "eventually (λx. ln (π x) * ?f x * (1 / ln (π x)) = ?f x) at_top"
    using ev by eventually_elim auto
  ultimately have "(?f  ln 1 * 0) at_top"
    by (rule Lim_transform_eventually)
  hence "((λx. 1 + ln (ln (π x)) / ln (π x) - ?f x)  1 + 0 - ln 1 * 0) at_top"
    by (intro tendsto_intros filterlim_compose[OF _ π_at_top]) (real_asymp | simp)+
  hence "((λx. ln x / ln (π x))  1) at_top"
    by simp
  thus *: "(λx. ln (π x)) ∼[at_top] (λx. ln x)"
    by (rule asymp_equiv_symI[OF asymp_equivI'])

  have "eventually (λx. π x = π x * ln (π x) / ln (π x)) at_top"
    using ev by eventually_elim auto
  hence "π ∼[at_top] (λx. π x * ln (π x) / ln (π x))"
    by (rule asymp_equiv_refl_ev)
  also from assms and * have "(λx. π x * ln (π x) / ln (π x)) ∼[at_top] (λx. x / ln x)"
    by (rule asymp_equiv_intros)
  finally show "π ∼[at_top] (λx. x / ln x)" .
qed

lemma PNT4_imp_PNT5:
  assumes "θ ∼[at_top] (λx. x)"
  shows   "ψ ∼[at_top] (λx. x)"
proof -
  define r where "r = (λx. ψ x - θ x)"
  have "r  O(λx. ln x * sqrt x)"
    unfolding r_def by (fact ψ_minus_θ_bigo)
  also have "(λx::real. ln x * sqrt x)  o(λx. x)"
    by real_asymp
  finally have r: "r  o(λx. x)" .

  have "(λx. θ x + r x) ∼[at_top] (λx. x)"
    using assms r by (subst asymp_equiv_add_right) auto
  thus ?thesis by (simp add: r_def)
qed

lemma PNT4_imp_PNT1:
  assumes "θ ∼[at_top] (λx. x)"
  shows   "π ∼[at_top] (λx. x / ln x)"
proof -
  have "(λx. (π x - θ x / ln x) + ((θ x - x) / ln x))  o(λx. x / ln x)"
  proof (rule sum_in_smallo)
    have "(λx. π x - θ x / ln x)  O(λx. x / ln x ^ 2)"
      by (rule π_θ_bigo)
    also have "(λx. x / ln x ^ 2)  o(λx. x / ln x :: real)"
      by real_asymp
    finally show "(λx. π x - θ x / ln x)  o(λx. x / ln x)" .
  next
    have "eventually (λx::real. ln x > 0) at_top" by real_asymp
    hence "eventually (λx::real. ln x  0) at_top" by eventually_elim auto
    thus "(λx. (θ x - x) / ln x)  o(λx. x / ln x)"
      by (intro landau_o.small.divide_right asymp_equiv_imp_diff_smallo assms)
  qed
  thus ?thesis by (simp add: diff_divide_distrib asymp_equiv_altdef)
qed

lemma PNT1_imp_PNT4:
  assumes "π ∼[at_top] (λx. x / ln x)"
  shows   "θ ∼[at_top] (λx. x)"
proof -
  have "θ ∼[at_top] (λx. π x * ln x)"
  proof (rule smallo_imp_asymp_equiv)
    have "(λx. θ x - π x * ln x)  Θ(λx. - ((π x - θ x / ln x) * ln x))"
      by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 1]])
         (auto simp: field_simps)
    also have "(λx. - ((π x - θ x / ln x) * ln x))  O(λx. x / (ln x)2 * ln x)"
      unfolding landau_o.big.uminus_in_iff by (intro landau_o.big.mult_right π_θ_bigo)
    also have "(λx::real. x / (ln x)2 * ln x)  o(λx. x / ln x * ln x)"
      by real_asymp
    also have "(λx. x / ln x * ln x)  Θ(λx. π x * ln x)"
      by (intro asymp_equiv_imp_bigtheta asymp_equiv_intros asymp_equiv_symI[OF assms])
    finally show "(λx. θ x - π x * ln x)  o(λx. π x * ln x)" .
  qed
  also have " ∼[at_top] (λx. x / ln x * ln x)"
    by (intro asymp_equiv_intros assms)
  also have " ∼[at_top] (λx. x)"
    by real_asymp
  finally show ?thesis .
qed

lemma PNT5_imp_PNT4:
  assumes "ψ ∼[at_top] (λx. x)"
  shows   "θ ∼[at_top] (λx. x)"
proof -
  define r where "r = (λx. θ x - ψ x)"
  have "(λx. ψ x - θ x)  O(λx. ln x * sqrt x)"
    by (fact ψ_minus_θ_bigo)
  also have "(λx. ψ x - θ x) = (λx. -r x)"
    by (simp add: r_def)
  finally have "r  O(λx. ln x * sqrt x)"
    by simp
  also have "(λx::real. ln x * sqrt x)  o(λx. x)"
    by real_asymp
  finally have r: "r  o(λx. x)" .

  have "(λx. ψ x + r x) ∼[at_top] (λx. x)"
    using assms r by (subst asymp_equiv_add_right) auto
  thus ?thesis by (simp add: r_def)
qed
(* END TODO *)
(*>*)

locale prime_number_theorem =
  assumes prime_number_theorem [asymp_equiv_intros]: "π ∼[at_top] (λx. x / ln x)"
begin

corollary θ_asymptotics [asymp_equiv_intros]: "θ ∼[at_top] (λx. x)"
  using prime_number_theorem by (rule PNT1_imp_PNT4)

corollary ψ_asymptotics [asymp_equiv_intros]: "ψ ∼[at_top] (λx. x)"
  using θ_asymptotics PNT4_imp_PNT5 by simp
  
corollary ln_π_asymptotics [asymp_equiv_intros]: "(λx. ln (π x)) ∼[at_top] ln"
  using prime_number_theorem PNT1_imp_PNT1' by simp

corollary π_ln_π_asymptotics: "(λx. π x * ln (π x)) ∼[at_top] (λx. x)"
  using prime_number_theorem PNT1_imp_PNT2 by simp

corollary nth_prime_asymptotics [asymp_equiv_intros]:
  "(λn. real (nth_prime n)) ∼[at_top] (λn. real n * ln (real n))"
  using π_ln_π_asymptotics PNT2_imp_PNT3 by simp

corollary moebius_mu_smallo: "sum_upto moebius_mu  o(λx. x)"
  using PNT_implies_sum_moebius_mu_sublinear ψ_asymptotics by simp

lemma ln_θ_asymptotics:
  includes prime_counting_notation
  shows "(λx. ln (θ x) - ln x)  o(λ_. 1)"
proof -
  have [simp]: "θ 2 = ln 2"
    by (simp add: eval_θ)
  have θ_pos: "θ x > 0" if "x  2" for x
  proof -
    have "0 < ln (2 :: real)" by simp
    also have "  θ x"
      using θ_mono[OF that] by simp
    finally show ?thesis .
  qed

  have nz: "eventually (λx. θ x  0  x  0) at_top"
    using eventually_gt_at_top[of 0] by eventually_elim auto
  have "filterlim (λx. θ x / x) (nhds 1) at_top"
    using asymp_equivD_strong[OF θ_asymptotics nz] .
  hence "filterlim (λx. ln (θ x / x)) (nhds (ln 1)) at_top"
    by (rule tendsto_ln) auto
  also have "?this  filterlim (λx. ln (θ x) - ln x) (nhds 0) at_top"
    by (intro filterlim_cong eventually_mono[OF eventually_ge_at_top[of 2]])
       (auto simp: ln_div θ_pos)
  finally show "(λx. ln (θ x) - ln x)  o(λx. 1)"
    by (intro smalloI_tendsto) auto
qed

lemma ln_θ_asymp_equiv [asymp_equiv_intros]:
  includes prime_counting_notation
  shows "(λx. ln (θ x)) ∼[at_top] ln"
proof (rule smallo_imp_asymp_equiv)
  have "(λx. ln (θ x) - ln x)  o(λ_. 1)" by (rule ln_θ_asymptotics)
  also have "(λ_. 1)  O(λx::real. ln x)" by real_asymp
  finally show "(λx. ln (θ x) - ln x)  o(ln)" .
qed

lemma ln_nth_prime_asymptotics:
  "(λn. ln (nth_prime n) - (ln n + ln (ln n)))  o(λ_. 1)"
proof -
  have "filterlim (λn. ln (nth_prime n / (n * ln n))) (nhds (ln 1)) at_top"
    by (intro tendsto_ln asymp_equivD_strong[OF nth_prime_asymptotics])
       (auto intro!: eventually_mono[OF eventually_gt_at_top[of 1]])
  also have "?this  filterlim (λn. ln (nth_prime n) - (ln n + ln (ln n))) (nhds 0) at_top"
    using prime_gt_0_nat[OF prime_nth_prime]
    by (intro filterlim_cong refl eventually_mono[OF eventually_gt_at_top[of 1]])
       (auto simp: field_simps ln_mult ln_div)
  finally show ?thesis by (intro smalloI_tendsto) auto
qed

lemma ln_nth_prime_asymp_equiv [asymp_equiv_intros]:
  "(λn. ln (nth_prime n)) ∼[at_top] ln"
proof -
  have "(λn. ln (nth_prime n) - (ln n + ln (ln n)))  o(ln)"
    using ln_nth_prime_asymptotics by (rule landau_o.small.trans) real_asymp
  hence "(λn. ln (nth_prime n) - (ln n + ln (ln n)) + ln (ln n))  o(ln)"
    by (rule sum_in_smallo) real_asymp
  thus ?thesis by (intro smallo_imp_asymp_equiv) auto
qed


text ‹
  The following versions use a little less notation.
›
corollary prime_number_theorem': "((λx. π x / (x / ln x))  1) at_top"
  using prime_number_theorem
  by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto

corollary prime_number_theorem'':
  "(λx. card {p. prime p  real p  x}) ∼[at_top] (λx. x / ln x)"
proof -
  have "π = (λx. card {p. prime p  real p  x})"
    by (intro ext) (simp add: π_def prime_sum_upto_def)
  with prime_number_theorem show ?thesis by simp
qed

corollary prime_number_theorem''':
  "(λn. card {p. prime p  p  n}) ∼[at_top] (λn. real n / ln (real n))"
proof -
  have "(λn. card {p. prime p  real p  real n}) ∼[at_top] (λn. real n / ln (real n))"
    using prime_number_theorem''
    by (rule asymp_equiv_compose') (simp add: filterlim_real_sequentially)
  thus ?thesis by simp
qed

end


subsection ‹Existence of primes in intervals›

text ‹
  For fixed ε›, The interval $(x; \varepsilon x]$ contains a prime number for any sufficiently
  large x›. This proof was taken from A.\,J. Hildebrand's lecture notes~cite"hildebrand_ant".
›
lemma (in prime_number_theorem) prime_in_interval_exists:
  fixes c :: real
  assumes "c > 1"
  shows   "eventually (λx. p. prime p  real p  {x<..c*x}) at_top"
proof -
  from c > 1 have "(λx. π (c * x) / π x) ∼[at_top] (λx. ((c * x) / ln (c * x)) / (x / ln x))"
    by (intro asymp_equiv_intros asymp_equiv_compose'[OF prime_number_theorem]) real_asymp+
  also have " ∼[at_top] (λx. c)"
    using c > 1 by real_asymp
  finally have "(λx. π (c * x) / π x) ∼[at_top] (λa. c)" by simp
  hence "((λx. π (c * x) / π x)  c) at_top"
    by (rule asymp_equivD_const)
  from this and c > 1 have "eventually (λx. π (c * x) / π x > 1) at_top"
    by (rule order_tendstoD)
  moreover have "eventually (λx. π x > 0) at_top"
    using π_at_top by (auto simp: filterlim_at_top_dense)
  ultimately show ?thesis using eventually_gt_at_top[of 1]
  proof eventually_elim
    case (elim x)
    define P where "P = {p. prime p  real p  {x<..c*x}}"
    from elim and c > 1 have "1 * x < c * x" by (intro mult_strict_right_mono) auto
    hence "x < c * x" by simp
    have "P = {p. prime p  real p  c * x} - {p. prime p  real p  x}"
      by (auto simp: P_def)
    also have "card  = card {p. prime p  real p  c * x} - card {p. prime p  real p  x}"
      using x < c * x by (subst card_Diff_subset) (auto intro: finite_primes_le)
    also have "real  = π (c * x) - π x"
      using π_mono[of x "c * x"] x < c * x
      by (subst of_nat_diff) (auto simp: primes_pi_def prime_sum_upto_def)
    finally have "real (card P) = π (c * x) - π x" by simp
    moreover have "π (c * x) - π x > 0"
      using elim by (auto simp: field_simps)
    ultimately have "real (card P) > 0" by linarith
    hence "card P > 0" by simp
    hence "P  {}" by (intro notI) simp
    thus ?case by (auto simp: P_def)
  qed
qed

text ‹
  The set of rationals whose numerator and denominator are primes is
  dense in $\mathbb{R}_{{}>0}$.
›
lemma (in prime_number_theorem) prime_fractions_dense:
  fixes α ε :: real
  assumes "α > 0" and "ε > 0"
  obtains p q :: nat where "prime p" and "prime q" and "dist (real p / real q) α < ε"
proof -
  define ε' where "ε' = ε / 2"
  from assms have "ε' > 0" by (simp add: ε'_def)
  have "eventually (λx. p. prime p  real p  {x<..(1 + ε' / α) * x}) at_top"
    using assms ε' > 0 by (intro prime_in_interval_exists) (auto simp: field_simps)
  then obtain x0 where x0: "x. x  x0  p. prime p  real p  {x<..(1 + ε' / α) * x}"
    by (auto simp: eventually_at_top_linorder)

  have "q. prime q  q > nat x0 / α" by (rule bigger_prime)
  then obtain q where "prime q" "q > nat x0 / α" by blast
  hence "real q  x0 / α" by linarith
  with α > 0 have "α * real q  x0" by (simp add: field_simps)
  hence "p. prime p  real p  {α * real q<..(1 + ε' / α) * (α * real q)}"
    by (intro x0)
  then obtain p where p: "prime p" "real p > α * real q" "real p  (1 + ε' / α) * (α * real q)"
    using assms by auto

  from p prime q have "real p / real q  (1 + ε' / α) * α"
    using assms by (auto simp: field_simps dest: prime_gt_0_nat)
  also have " = α + ε'"
    using assms by (simp add: field_simps)
  finally have "real p / real q  α + ε'" .
  moreover from p prime q have "real p / real q > α" "real p / real q  (1 + ε' / α) * α"
    using assms by (auto simp: field_simps dest: prime_gt_0_nat)
  ultimately have "dist (real p / real q) α  ε'"
    by (simp add: dist_norm)
  also have " < ε"
    using ε > 0 by (simp add: ε'_def)
  finally show ?thesis using prime p prime q that[of p q] by blast
qed


subsection ‹The logarithm of the primorial›

text ‹
  The PNT directly implies the asymptotics of the logarithm of the primorial function:
›

context prime_number_theorem
begin

lemma ln_primorial_asymp_equiv [asymp_equiv_intros]:
  "(λx. ln (primorial x)) ∼[at_top] (λx. x)"
  by (auto simp: ln_primorial θ_asymptotics)

lemma ln_ln_primorial_asymp_equiv [asymp_equiv_intros]:
  "(λx. ln (ln (primorial x))) ∼[at_top] (λx. ln x)"
  by (auto simp: ln_primorial ln_θ_asymp_equiv)

lemma ln_primorial'_asymp_equiv [asymp_equiv_intros]:
        "(λk. ln (primorial' k)) ∼[at_top] (λk. k * ln k)"
  and ln_ln_primorial'_asymp_equiv [asymp_equiv_intros]:
        "(λk. ln (ln (primorial' k))) ∼[at_top] (λk. ln k)"
  and ln_over_ln_ln_primorial'_asymp_equiv:
        "(λk. ln (primorial' k) / ln (ln (primorial' k))) ∼[at_top] (λk. k)"
proof -
  have lim1: "filterlim (λk. real (nth_prime (k - 1))) at_top at_top"
    by (rule filterlim_compose[OF filterlim_real_sequentially]
             filterlim_compose[OF nth_prime_at_top])+ real_asymp
  have lim2: "filterlim (λk::nat. k - 1) at_top at_top"
    by real_asymp

  have "(λk. ln (primorial' k)) ∼[at_top] (λn. ln (primorial (nth_prime (n - 1))))"
    by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 0]])
       (auto simp: primorial'_conv_primorial)
  also have " ∼[at_top] (λn. nth_prime (n - 1))"
    by (intro asymp_equiv_compose'[OF _ lim1] asymp_equiv_intros)
  also have " ∼[at_top] (λn. real (n - 1) * ln (real (n - 1)))"
    by (intro asymp_equiv_compose'[OF _ lim2] asymp_equiv_intros)
  also have " ∼[at_top] (λn. n * ln n)" by real_asymp
  finally show 1: "(λk. ln (primorial' k)) ∼[at_top] (λk. k * ln k)" .

  have "(λk. ln (ln (primorial' k))) ∼[at_top] (λn. ln (ln (primorial (nth_prime (n - 1)))))"
    by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 0]])
       (auto simp: primorial'_conv_primorial)
  also have " ∼[at_top] (λn. ln (nth_prime (n - 1)))"
    by (intro asymp_equiv_compose'[OF _ lim1] asymp_equiv_intros)
  also have " ∼[at_top] (λn. ln (real (n - 1)))"
    by (intro asymp_equiv_compose'[OF _ lim2] asymp_equiv_intros)
  also have " ∼[at_top] (λn. ln n)" by real_asymp
  finally show 2: "(λk. ln (ln (primorial' k))) ∼[at_top] (λk. ln k)" .
    
  have "(λk. ln (primorial' k) / ln (ln (primorial' k))) ∼[at_top] (λk. (k * ln k) / ln k)"
    by (intro asymp_equiv_intros 1 2)
  also have " ∼[at_top] (λk. k)" by real_asymp
  finally show "(λk. ln (primorial' k) / ln (ln (primorial' k))) ∼[at_top] (λk. k)" .
qed

end


subsection ‹Consequences of the asymptotics of ψ› and θ›

text ‹
  Next, we will show some consequences of $\psi(x)\sim x$ and $\vartheta(x)\sim x$. To this
  end, we first show generically that any function $g = e^{x + o(x)}$ is $o(c^n)$ if $c > e$ and
  $\omega(c^n)$ if $c < e$.
›
locale exp_asymp_equiv_linear =
  fixes f g :: "real  real"
  assumes f_asymp_equiv: "f ∼[at_top] (λx. x)"
  assumes g: "eventually (λx. g x = exp (f x)) F"
begin

lemma
  fixes ε :: real assumes "ε > 0"
  shows smallo:     "g  o(λx. exp ((1 + ε) * x))"
    and smallomega: "g  ω(λx. exp ((1 - ε) * x))"
proof -
  have "(λx. exp (f x) / exp ((1 + ε) * x))  Θ(λx. exp (((f x - x) / x - ε) * x))"
    by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 1]])
       (simp_all add: divide_simps ring_distribs flip: exp_add exp_diff)
  also have "((λx. exp (((f x - x) / x - ε) * x))  0) at_top"
  proof (intro filterlim_compose[OF exp_at_bot] filterlim_tendsto_neg_mult_at_bot)
    have smallo: "(λx. f x - x)  o(λx. x)"
      using f_asymp_equiv by (rule asymp_equiv_imp_diff_smallo)
    show "((λx. (f x - x) / x - ε)  0 - ε) at_top"
      by (intro tendsto_diff smalloD_tendsto[OF smallo] tendsto_const)
  qed (use ε > 0 in auto simp: filterlim_ident)
  hence "(λx. exp (((f x - x) / x - ε) * x))  o(λ_. 1)"
    by (intro smalloI_tendsto) auto
  finally have "(λx. exp (f x))  o(λx. exp ((1 + ε) * x))"
    by (simp add: landau_divide_simps)
  also have "?this  g  o(λx. exp ((1 + ε) * x))"
    using g by (intro landau_o.small.in_cong) (simp add: eq_commute)
  finally show "g  o(λx. exp ((1 + ε) * x))" .
next
  have "(λx. exp (f x) / exp ((1 - ε) * x))  Θ(λx. exp (((f x - x) / x + ε) * x))"
    by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 1]])
       (simp add: ring_distribs flip: exp_add exp_diff)
  also have "filterlim (λx. exp (((f x - x) / x + ε) * x)) at_top at_top"
  proof (intro filterlim_compose[OF exp_at_top] filterlim_tendsto_pos_mult_at_top)
    have smallo: "(λx. f x - x)  o(λx. x)"
      using f_asymp_equiv by (rule asymp_equiv_imp_diff_smallo)
    show "((λx. (f x - x) / x + ε)  0 + ε) at_top"
      by (intro tendsto_add smalloD_tendsto[OF smallo] tendsto_const)
  qed (use ε > 0 in auto simp: filterlim_ident)
  hence "(λx. exp (((f x - x) / x + ε) * x))  ω(λ_. 1)"
    by (simp add: filterlim_at_top_iff_smallomega)
  finally have "(λx. exp (f x))  ω(λx. exp ((1 - ε) * x))"
    by (simp add: landau_divide_simps)
  also have "?this  g  ω(λx. exp ((1 - ε) * x))"
    using g by (intro landau_omega.small.in_cong) (simp add: eq_commute)
  finally show "g  ω(λx. exp ((1 - ε) * x))" .
qed

lemma smallo':
  fixes c :: real assumes "c > exp 1"
  shows "g  o(λx. c powr x)"
proof -
  have "c > 0" by (rule le_less_trans[OF _ assms]) auto
  from c > 0 assms have "exp 1 < exp (ln c)"
    by (subst exp_ln) auto
  hence "ln c > 1" by (subst (asm) exp_less_cancel_iff)
  hence "g  o(λx. exp ((1 + (ln c - 1)) * x))"
    using assms by (intro smallo) auto
  also have "(λx. exp ((1 + (ln c - 1)) * x)) = (λx. c powr x)"
    using c > 0 by (simp add: powr_def mult_ac)
  finally show ?thesis .
qed

lemma smallomega':
  fixes c :: real assumes "c  {0<..<exp 1}"
  shows "g  ω(λx. c powr x)"
proof -
  from assms have "exp 1 > exp (ln c)"
    by (subst exp_ln) auto
  hence "ln c < 1" by (subst (asm) exp_less_cancel_iff)
  hence "g  ω(λx. exp ((1 - (1 - ln c)) * x))"
    using assms by (intro smallomega) auto
  also have "(λx. exp ((1 - (1 - ln c)) * x)) = (λx. c powr x)"
    using assms by (simp add: powr_def mult_ac)
  finally show ?thesis .
qed

end


text ‹
  The primorial fulfils $x\# = e^{\vartheta(x)}$ and is therefore one example of this.
›

context prime_number_theorem
begin

sublocale primorial: exp_asymp_equiv_linear θ "λx. real (primorial x)"
  using θ_asymptotics by unfold_locales (simp_all add: ln_primorial [symmetric])

end


text ‹
  The LCM of the first n› natural numbers is equal to $e^{\psi(n)}$ and is
  therefore another example.
›

context prime_number_theorem
begin

sublocale Lcm_upto: exp_asymp_equiv_linear ψ "λx. real (Lcm {1..nat x})"
  using ψ_asymptotics by unfold_locales (simp_all flip: Lcm_upto_real_conv_ψ)

end


subsection ‹Bounds on the prime ω› function›

text ‹
  Next, we will examine the asymptotic behaviour of the prime ω› function $\omega(n)$,
  i.\,e.\ the number of distinct prime factors of n›. These proofs are again taken from
  A.\,J. Hildebrand's lecture notes~cite"hildebrand_ant".
›

lemma ln_gt_1:
  assumes "x > (3 :: real)"
  shows   "ln x > 1"
proof -
  have "x > exp 1"
    using exp_le assms by linarith
  hence "ln x > ln (exp 1)" using assms by (subst ln_less_cancel_iff) auto
  thus ?thesis by simp
qed

lemma (in prime_number_theorem) primes_omega_primorial'_asymp_equiv:
  "(λk. primes_omega (primorial' k)) ∼[at_top]
     (λk. ln (primorial' k) / ln (ln (primorial' k)))"
  using ln_over_ln_ln_primorial'_asymp_equiv by (simp add: asymp_equiv_sym)

text ‹
  The number of distinct prime factors of n› has maximal order $\ln n / \ln\ln n$:
›
theorem (in prime_number_theorem)
  limsup_primes_omega: "limsup (λn. primes_omega n / (ln n / ln (ln n))) = 1"
proof (intro antisym)
  have "(λk. primes_omega (primorial' k) / (ln (primorial' k) / ln (ln (primorial' k))))  1"
    using primes_omega_primorial'_asymp_equiv
    by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]]) auto
  hence "limsup ((λn. primes_omega n / (ln n / ln (ln n)))  primorial') = ereal 1"
    by (intro lim_imp_Limsup tendsto_ereal) simp_all
  hence "1 = limsup ((λn. ereal (primes_omega n / (ln n / ln (ln n))))  primorial')"
    by (simp add: o_def)
  also have "  limsup (λn. primes_omega n / (ln n / ln (ln n)))"
    using strict_mono_primorial' by (rule limsup_subseq_mono)
  finally show "limsup (λn. primes_omega n / (ln n / ln (ln n)))  1" .
next
  show "limsup (λn. primes_omega n / (ln n / ln (ln n)))  1"
    unfolding Limsup_le_iff
  proof safe
    fix C' :: ereal assume C': "C' > 1"
    from ereal_dense2[OF this] obtain C where C: "C > 1" "ereal C < C'" by auto

    have "(λk. primes_omega (primorial' k) / (ln (primorial' k) / ln (ln (primorial' k))))  1"
      (is "filterlim ?f _ _") using primes_omega_primorial'_asymp_equiv
      by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]]) auto
    from order_tendstoD(2)[OF this C(1)]
    have "eventually (λk. ?f k < C) at_top" .
    then obtain k0 where k0: "k. k  k0  ?f k < C" by (auto simp: eventually_at_top_linorder) 
    
    have "eventually (λn::nat. max 3 k0 / (ln n / ln (ln n)) < C) at_top"
      using C > 1 by real_asymp
    hence "eventually (λn. primes_omega n / (ln n / ln (ln n))  C) at_top"
      using eventually_gt_at_top[of "primorial' (max k0 3)"]
    proof eventually_elim
      case (elim n)
      define k where "k = primes_omega n"
      define m where "m = primorial' k"
      have "primorial' 3  primorial' (max k0 3)"
        by (subst strict_mono_less_eq[OF strict_mono_primorial']) auto
      also have " < n" by fact
      finally have "n > 30" by simp

      show ?case
      proof (cases "k  max 3 k0")
        case True
        hence "m  30"
          using strict_mono_less_eq[OF strict_mono_primorial', of 3 k] by (simp add: m_def k_def)
        have "exp 1 ^ 3  (3 ^ 3 :: real)"
          using exp_le by (intro power_mono) auto
        also have " < m" using m  30 by simp
        finally have "ln (exp 1 ^ 3) < ln m"
          using m  30 by (subst ln_less_cancel_iff) auto
        hence "ln m > 3" by (subst (asm) ln_realpow) auto

        have "primorial' (primes_omega n)  n"
          using n > 30 by (intro primorial'_primes_omega_le) auto
        hence "m  n" unfolding m_def k_def using elim
          by (auto simp: max_def)
        hence "primes_omega n / (ln n / ln (ln n))  k / (ln m / ln (ln m))"
          unfolding k_def using elim m  30 ln_gt_1[of n] ln m > 3
          by (intro frac_le[of "primes_omega n"] divide_ln_mono mult_pos_pos divide_pos_pos) auto
        also have " = ?f k"
          by (simp add: k_def m_def)
        also have " < C"
          by (intro k0) (use True in auto simp: k_def)
        finally show ?thesis by simp
      next
        case False
        hence "primes_omega n / (ln n / ln (ln n))  max 3 k0 / (ln n / ln (ln n))"
          using elim ln_gt_1[of n] n > 30
          by (intro divide_right_mono divide_nonneg_pos) (auto simp: k_def)
        also have " < C"
          using elim by simp
        finally show ?thesis by simp
      qed
    qed
    thus "eventually (λn. ereal (primes_omega n / (ln n / ln (ln n))) < C') at_top"
      by eventually_elim (rule le_less_trans[OF _ C(2)], auto)
  qed
qed


subsection ‹Bounds on the divisor function›

text ‹
  In this section, we shall examine the growth of the divisor function $\sigma_0(n)$.
  In particular, we will show that $\sigma_0(n) < 2^{c\ln n / \ln\ln n}$ for all sufficiently
  large n› if $c > 1$ and $\sigma_0(n) > 2^{c\ln n / \ln\ln n}$ for infinitely many n›
  if $c < 1$.

  An equivalent statement is that $\ln(\sigma_0(n))$ has maximal order
  $\ln 2 \cdot \ln n / \ln\ln n$.

  Following Apostol's somewhat didactic approach, we first show a generic bounding lemma for
  $\sigma_0$ that depends on some function f› that we will specify later.
›
lemma divisor_count_bound_gen:
  fixes f :: "nat  real"
  assumes "eventually (λn. f n  2) at_top"
  defines "c  (8 / ln 2 :: real)"
  defines "g  (λn. (ln n + c * f n * ln (ln n)) / (ln (f n)))"
  shows "eventually (λn. divisor_count n < 2 powr g n) at_top"
proof -
  include prime_counting_notation
  have "eventually (λn::nat. 1 + log 2 n  ln n ^ 2) at_top"  by real_asymp
  thus "eventually (λn. divisor_count n < 2 powr g n) at_top"
    using eventually_gt_at_top[of 2] assms(1)
  proof eventually_elim
    fix n :: nat
    assume n: "n > 2" and "f n  2" and "1 + log 2 n  ln n ^ 2"

    define Pr where [simp]: "Pr = prime_factors n"
    define Pr1 where [simp]: "Pr1 = {pPr. p < f n}"
    define Pr2 where [simp]: "Pr2 = {pPr. p  f n}"
  
    have "exp 1 < real n"
      using e_less_272 n > 2 by linarith
    hence "ln (exp 1) < ln (real n)"
      using n > 2 by (subst ln_less_cancel_iff) auto
    hence "ln (ln n) > ln (ln (exp 1))"
      by (subst ln_less_cancel_iff) auto
    hence "ln (ln n) > 0" by simp
  
    define S2 where "S2 = (pPr2. multiplicity p n)"
    have "f n ^ S2 = (pPr2. f n ^ multiplicity p n)"
      by (simp add: S2_def power_sum)
    also have "  (pPr2. real p ^ multiplicity p n)"
      using f n  2 by (intro prod_mono conjI power_mono) auto
    also from n > 2 have "  (pPr. real p ^ multiplicity p n)"
      by (intro prod_mono2 one_le_power) (auto simp: in_prime_factors_iff dest: prime_gt_0_nat)
    also have " = n"
      using n > 2 by (subst prime_factorization_nat[of n])  auto
    finally have "f n ^ S2  n" .
    hence "ln (f n ^ S2)  ln n"
      using n f n  2 by (subst ln_le_cancel_iff) auto
    hence "S2  ln n / ln (f n)"
      using f n  2 by (simp add: field_simps ln_realpow)
  
    have le_twopow: "Suc a  2 ^ a" for a :: nat by (induction a) auto
    have "(pPr2. Suc (multiplicity p n))  (pPr2. 2 ^ multiplicity p n)"
      by (intro prod_mono conjI le_twopow) auto
    also have " = 2 ^ S2"
      by (simp add: S2_def power_sum)
    also have " = 2 powr real S2"
      by (subst powr_realpow) auto
    also have "  2 powr (ln n / ln (f n))"
      by (intro powr_mono S2  ln n / ln (f n)) auto
    finally have bound2: "real (pPr2. Suc (multiplicity p n))  2 powr (ln n / ln (f n))"
      by simp
  
    have multiplicity_le: "multiplicity p n  log 2 n" if p: "p  Pr" for p
    proof -
      from p have "2 ^ multiplicity p n  p ^ multiplicity p n"
        by (intro power_mono) (auto simp: in_prime_factors_iff dest: prime_gt_1_nat)
      also have " = (p{p}. p ^ multiplicity p n)" by simp
      also from p have "(p{p}. p ^ multiplicity p n)  (pPr. p ^ multiplicity p n)"
        by (intro dvd_imp_le prod_dvd_prod_subset)
           (auto simp: in_prime_factors_iff dest: prime_gt_0_nat)
      also have " = n"
        using n by (subst prime_factorization_nat[of n]) auto
      finally have "2 ^ multiplicity p n  n" .
      hence "log 2 (2 ^ multiplicity p n)  log 2 n"
        using n by (subst log_le_cancel_iff) auto
      thus "multiplicity p n  log 2 n"
        by (subst (asm) log_nat_power) auto    
    qed
  
    have "(pPr1. Suc (multiplicity p n)) = exp (pPr1. ln (multiplicity p n + 1))"
      by (simp add: exp_sum)
    also have "(pPr1. ln (multiplicity p n + 1))  (pPr1. 2 * ln (ln n))"
    proof (intro sum_mono)
      fix p assume p: "p  Pr1"
      have "ln (multiplicity p n + 1)  ln (1 + log 2 n)"
        using p multiplicity_le[of p] by (subst ln_le_cancel_iff) auto
      also have "  ln (ln n ^ 2)"
        using n > 2 1 + log 2 n  ln n ^ 2
        by (subst ln_le_cancel_iff) (auto intro: add_pos_nonneg)
      also have " = 2 * ln (ln n)"
        using n > 2 by (simp add: ln_realpow)
      finally show "ln (multiplicity p n + 1)  2 * ln (ln n)" .
    qed
    also have " = 2 * ln (ln n) * card Pr1"
      by simp
    also have "finite {p. prime p  real p  f n}"
      by (rule finite_subset[of _ "{..nat f n}"]) (auto simp: le_nat_iff le_floor_iff)
    hence "card Pr1  card {p. prime p  real p  f n}"
      by (intro card_mono) auto
    also have "real  = π (f n)"
      by (simp add: primes_pi_def prime_sum_upto_def)
    also have " < 4 * (f n / ln (f n))"
      using f n  2 by (intro π_upper_bound'') auto
    also have "exp (2 * ln (ln (real n)) * (4 * (f n / ln (f n)))) =
                 2 powr (c * f n * ln (ln n) / ln (f n))"
      by (simp add: powr_def c_def)
    finally have bound1: "(pPr1. Suc (multiplicity p n)) <
                             2 powr (c * f n * ln (ln (real n)) / ln (f n))"
      using ln (ln n) > 0 by (simp add: mult_strict_left_mono)
  
    
    have "divisor_count n = (pPr. Suc (multiplicity p n))"
      using n by (subst divisor_count.prod_prime_factors') auto
    also have "Pr = Pr1  Pr2" by auto
    also have "real (p. Suc (multiplicity p n)) =
                 real ((pPr1. Suc (multiplicity p n)) * (pPr2. Suc (multiplicity p n)))"
      by (subst prod.union_disjoint) auto
    also have " < 2 powr (c * f n * ln (ln (real n)) / ln (f n)) * 2 powr (ln n / ln (f n))"
      unfolding of_nat_mult
      by (intro mult_less_le_imp_less bound1 bound2) (auto intro!: prod_nonneg prod_pos)
    also have " = 2 powr g n"
      by (simp add: g_def add_divide_distrib powr_add)
    finally show "real (divisor_count n) < 2 powr g n" .
  qed
qed

text ‹
  Now, Apostol explains that one can choose $f(n) := \ln n / (\ln\ln n) ^ 2$ to obtain
  the desired bound.
›
proposition divisor_count_upper_bound:
  fixes ε :: real
  assumes "ε > 0"
  shows   "eventually (λn. divisor_count n < 2 powr ((1 + ε) * ln n / ln (ln n))) at_top"
proof -
  define c :: real where "c = 8 / ln 2"
  define f :: "nat  real" where "f = (λn. ln n / (ln (ln n)) ^ 2)"
  define g where "g = (λn. (ln n + c * f n * ln (ln n)) / (ln (f n)))"

  have "eventually (λn. divisor_count n < 2 powr g n) at_top"
    unfolding g_def c_def f_def by (rule divisor_count_bound_gen) real_asymp+
  moreover have "eventually (λn. 2 powr g n < 2 powr ((1 + ε) * ln n / ln (ln n))) at_top"
    using ε > 0 unfolding g_def c_def f_def by real_asymp
  ultimately show "eventually (λn. divisor_count n < 2 powr ((1 + ε) * ln n / ln (ln n))) at_top"
    by eventually_elim (rule less_trans)
qed

text ‹
  Next, we will examine the `worst case'. Since any prime factor of n› with multiplicity
  k› contributes a factor of $k + 1$, it is intuitively clear that $\sigma_0(n)$ is
  largest w.\,r.\,t.\ n› if it is a product of small distinct primes.

  We show that indeed, if $n := x\#$ (where $x\#$ denotes the primorial), we have
  $\sigma_0(n) = 2^{\pi(x)}$, which, by the Prime Number Theorem, indeed
  exceeds $c \ln n / \ln\ln n$.
›
theorem (in prime_number_theorem) divisor_count_primorial_gt:
  assumes "ε > 0"
  defines "h  primorial"
  shows "eventually (λx. divisor_count (h x) > 2 powr ((1 - ε) * ln (h x) / ln (ln (h x)))) at_top"
proof -
  have "(λx. (1 - ε) * ln (h x) / ln (ln (h x))) ∼[at_top] (λx. (1 - ε) * θ x / ln (θ x))"
    by (simp add: h_def ln_primorial)
  also have " ∼[at_top] (λx. (1 - ε) * x / ln x)"
    by (intro asymp_equiv_intros θ_asymptotics ln_θ_asymp_equiv)
  finally have *: "(λx. (1 - ε) * ln (h x) / ln (ln (h x))) ∼[at_top] (λx. (1 - ε) * x / ln x)"
    by simp
  have "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - (1 - ε) * x / ln x)  o(λx. (1 - ε) * x / ln x)"
    using asymp_equiv_imp_diff_smallo[OF *] by simp
  also have "?this  (λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - x / ln x + ε * x / ln x)
                 o(λx. (1 - ε) * x / ln x)"
    by (intro landau_o.small.in_cong eventually_mono[OF eventually_gt_at_top[of 1]])
       (auto simp: field_simps)
  also have "(λx. (1 - ε) * x / ln x)  O(λx. x / ln x)"
    by real_asymp
  finally have "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - x / ln x + ε * x / ln x)
                    o(λx. x / ln x)" .
  hence "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - x / ln x + ε * x / ln x - (π x - x / ln x))
            o(λx. x / ln x)"
    by (intro sum_in_smallo[OF _ asymp_equiv_imp_diff_smallo] prime_number_theorem)
  hence "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - π x + ε * (x / ln x))  o(λx. ε * (x / ln x))"
    using ε > 0 by (subst landau_o.small.cmult) (simp_all add: algebra_simps)
  hence "(λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - π x) ∼[at_top] (λx. -ε * (x / ln x))"
    by (intro smallo_imp_asymp_equiv) auto
  hence "eventually (λx. (1 - ε) * ln (h x) / (ln (ln (h x))) - π x < 0 
                         -ε * (x / ln x) < 0) at_top"
    by (rule asymp_equiv_eventually_neg_iff)
  moreover have "eventually (λx. -ε * (x / ln x) < 0) at_top"
    using ε > 0 by real_asymp
  ultimately have "eventually (λx. (1 - ε) * ln (h x) / ln (ln (h x)) < π x) at_top"
    by eventually_elim simp
  thus "eventually (λx. divisor_count (h x) > 2 powr ((1 - ε) * ln (h x) / ln (ln (h x)))) at_top"
  proof eventually_elim
    case (elim x)
    hence "2 powr ((1 - ε) * ln (h x) / ln (ln (h x))) < 2 powr π x"
      by (intro powr_less_mono) auto
    thus ?case by (simp add: divisor_count_primorial h_def)
  qed
qed

text ‹
  Since $h(x)\longrightarrow\infty$, this gives us our infinitely many values of n›
  that exceed the bound.
›
corollary (in prime_number_theorem) divisor_count_lower_bound:
  assumes "ε > 0"
  shows   "frequently (λn. divisor_count n > 2 powr ((1 - ε) * ln n / ln (ln n))) at_top"
proof -
  define h where "h = primorial"
  have "eventually (λn. divisor_count n > 2 powr ((1 - ε) * ln n / ln (ln n)))
          (filtermap h at_top)"
    using divisor_count_primorial_gt[OF assms] by (simp add: eventually_filtermap h_def)
  hence "frequently (λn. divisor_count n > 2 powr ((1 - ε) * ln n / ln (ln n)))
           (filtermap h at_top)"
    by (intro eventually_frequently) (auto simp: filtermap_bot_iff)
  moreover from this and primorial_at_top
    have "filtermap h at_top  at_top" by (simp add: filterlim_def h_def)
  ultimately show ?thesis
    by (rule frequently_mono_filter)
qed

text ‹
  A different formulation that is not quite as tedious to prove is this one:
›
lemma (in prime_number_theorem) ln_divisor_count_primorial'_asymp_equiv:
  "(λk. ln (divisor_count (primorial' k))) ∼[at_top]
     (λk. ln 2 * ln (primorial' k) / ln (ln (primorial' k)))"
proof -
  have "(λk. ln 2 * (ln (primorial' k) / ln (ln (primorial' k)))) ∼[at_top] (λk. ln 2 * k)"
    by (intro asymp_equiv_intros ln_over_ln_ln_primorial'_asymp_equiv)
  also have " ∼[at_top] (λk. ln (divisor_count (primorial' k)))"
    by (simp add: ln_realpow mult_ac)
  finally show ?thesis by (simp add: asymp_equiv_sym mult_ac)
qed

text ‹
  It follows that the maximal order of the divisor function is $\ln 2 \cdot \ln n /\ln \ln n$.
›
theorem (in prime_number_theorem) limsup_divisor_count:
  "limsup (λn. ln (divisor_count n) * ln (ln n) / ln n) = ln 2"
proof (intro antisym)
  let ?h = "primorial'"
  have "2 ^ k = (1 :: real)  k = 0" for k :: nat
    using power_eq_1_iff[of "2::real" k] by auto
  hence "(λk. ln (divisor_count (?h k)) / (ln 2 * ln (?h k) / ln (ln (?h k))))  1"
    using ln_divisor_count_primorial'_asymp_equiv
    by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]])
       (auto simp: power_eq_1_iff)
  hence "(λk. ln (divisor_count (?h k)) / (ln 2 * ln (?h k) / ln (ln (?h k))) * ln 2)  1 * ln 2"
    by (rule tendsto_mult) auto
  hence "(λk. ln (divisor_count (?h k)) / (ln (?h k) / ln (ln (?h k))))  ln 2"
    by simp
  hence "limsup ((λn. ln (divisor_count n) * ln (ln n) / ln n)  primorial') = ereal (ln 2)"
    by (intro lim_imp_Limsup tendsto_ereal) simp_all
  hence "ln 2 = limsup ((λn. ereal (ln (divisor_count n) * ln (ln n) / ln n))  primorial')"
    by (simp add: o_def)
  also have "  limsup (λn. ln (divisor_count n) * ln (ln n) / ln n)"
    using strict_mono_primorial' by (rule limsup_subseq_mono)
  finally show "limsup (λn. ln (divisor_count n) * ln (ln n) / ln n)  ln 2" .
next
  show "limsup (λn. ln (divisor_count n) * ln (ln n) / ln n)  ln 2"
    unfolding Limsup_le_iff
  proof safe
    fix C' assume "C' > ereal (ln 2)"
    from ereal_dense2[OF this] obtain C where C: "C > ln 2" "ereal C < C'" by auto
    define ε where "ε = (C / ln 2) - 1"
    from C have "ε > 0" by (simp add: ε_def)

    have "eventually (λn::nat. ln (ln n) > 0) at_top" by real_asymp
    hence "eventually (λn. ln (divisor_count n) * ln (ln n) / ln n < C) at_top"
      using divisor_count_upper_bound[OF ε > 0] eventually_gt_at_top[of 1]
    proof eventually_elim
      case (elim n)
      hence "ln (divisor_count n) < ln (2 powr ((1 + ε) * ln n / ln (ln n)))"
        by (subst ln_less_cancel_iff) auto
      also have " = (1 + ε) * ln 2 * ln n / ln (ln n)"
        by (simp add: ln_powr)
      finally have "ln (divisor_count n) * ln (ln n) / ln n < (1 + ε) * ln 2"
        using elim by (simp add: field_simps)
      also have " = C" by (simp add: ε_def)
      finally show ?case .
    qed
    thus "eventually (λn. ereal (ln (divisor_count n) * ln (ln n) / ln n) < C') at_top"
      by eventually_elim (rule less_trans[OF _ C(2)], auto)
  qed
qed
    

subsection ‹Mertens' Third Theorem›

text ‹
  In this section, we will show that
  \[\prod_{p\leq x} \left(1 - \frac{1}{p}\right) =
      \frac{C}{\ln x} + O\left(\frac{1}{\ln^2 x}\right)\]
  with explicit bounds for the factor in the `Big-O'. Here, C› is the following constant:
›
definition third_mertens_const :: real where
  "third_mertens_const =
     exp (-(p::nat. if prime p then -ln (1 - 1 / real p) - 1 / real p else 0) - meissel_mertens)"

text ‹
  This constant is actually equal to $e^{-\gamma}$ where $\gamma$ is the Euler--Mascheroni
   constant, but showing this is quite a bit of work, which we shall not do here.
›

lemma third_mertens_const_pos: "third_mertens_const > 0"
  by (simp add: third_mertens_const_def)

theorem
  defines "C  third_mertens_const" 
  shows   mertens_third_theorem_strong:
            "eventually (λx. ¦(p | prime p  real p  x. 1 - 1 / p) - C / ln x¦ 
                                10 * C / ln x ^ 2) at_top"
  and     mertens_third_theorem:
            "(λx. (p | prime p  real p  x. 1 - 1 / p) - C / ln x)  O(λx. 1 / ln x ^ 2)"
proof -
  define Pr where "Pr = (λx. {p. prime p  real p  x})"
  define a :: "nat  real"
    where "a = (λp. if prime p then -ln (1 - 1 / real p) - 1 / real p else 0)"
  define B where "B = suminf a"
  have C_eq: "C = exp (-B - meissel_mertens)"
    by (simp add: B_def a_def third_mertens_const_def C_def)
  have fin: "finite (Pr x)" for x
    by (rule finite_subset[of _ "{..nat x}"]) (auto simp: Pr_def le_nat_iff le_floor_iff)

  define S where "S = (λx. (pPr x. ln (1 - 1 / p)))"
  define R where "R = (λx. S x + ln (ln x) + (B + meissel_mertens))"

  have exp_S: "exp (S x) = (pPr x. (1 - 1 / p))" for x
  proof -
    have "exp (S x) = (pPr x. exp (ln (1 - 1 / p)))"
      by (simp add: S_def exp_sum fin)
    also have " = (pPr x. (1 - 1 / p))"
      by (intro prod.cong) (auto simp: Pr_def dest: prime_gt_1_nat)
    finally show ?thesis .
  qed

  have a_nonneg: "a n  0" for n
  proof (cases "prime n")
    case True
    hence "ln (1 - 1 / n)  -(1 / n)"
      by (intro ln_one_minus_pos_upper_bound) (auto dest: prime_gt_1_nat)
    thus ?thesis by (auto simp: a_def)
  qed (auto simp: a_def)

  have "summable a"
  proof (rule summable_comparison_test_bigo)
    have "a  O(λn. -ln (1 - 1 / n) - 1 / n)"
      by (intro bigoI[of _ 1]) (auto simp: a_def)
    also have "(λn::nat. -ln (1 - 1 / n) - 1 / n)  O(λn. 1 / n ^ 2)"
      by real_asymp
    finally show "a  O(λn. 1 / real n ^ 2)" .
  next
    show "summable (λn. norm (1 / real n ^ 2))"
      using inverse_power_summable[of 2] by (simp add: field_simps)
  qed

  have "eventually (λn. a n  1 / n - 1 / Suc n) at_top"
  proof -
    have "eventually (λn::nat. -ln (1 - 1 / n) - 1 / n  1 / n - 1 / Suc n) at_top"
      by real_asymp
    thus ?thesis using eventually_gt_at_top[of 1]
      by eventually_elim (auto simp: a_def of_nat_diff field_simps)
  qed
  hence "eventually (λm. nm. a n  1 / n - 1 / Suc n) at_top"
    by (rule eventually_all_ge_at_top)
  hence "eventually (λx. nnat x. a n  1 / n - 1 / Suc n) at_top"
    by (rule eventually_compose_filterlim)
       (intro filterlim_compose[OF filterlim_nat_sequentially] filterlim_floor_sequentially)
  hence "eventually (λx. B - sum_upto a x  1 / x) at_top"
    using eventually_ge_at_top[of "1::real"]
  proof eventually_elim
    case (elim x)
    have a_le: "a n  1 / real n - 1 / real (Suc n)" if "real n  x" for n
    proof -
      from that and x  1 have "n  nat x" by linarith
      with elim and that show ?thesis by auto
    qed
    define m where "m = Suc (nat x)"
    have telescope: "(λn. 1 / (n + m) - 1 / (Suc n + m)) sums (1 / real (0 + m) - 0)"
      by (intro telescope_sums') real_asymp

    have "B - (n<m. a n) = (n. a (n + m))"
      unfolding B_def sum_upto_altdef m_def using summable a
      by (subst suminf_split_initial_segment[of _ "Suc (nat x)"]) auto
    also have "(n<m. a n) = sum_upto a x"
      unfolding m_def sum_upto_altdef by (intro sum.mono_neutral_right) (auto simp: a_def)
    also have "(n. a (n + m))  (n. 1 / (n + m) - 1 / (Suc n + m))"
    proof (intro suminf_le allI)
      show "summable (λn. a (n + m))"
        by (rule summable_ignore_initial_segment) fact+
    next
      show "summable (λn. 1 / (n + m) - 1 / (Suc n + m))"
        using telescope by (rule sums_summable)
    next
      fix n :: nat
      have "x  n + m" unfolding m_def using x  1 by linarith
      thus "a (n + m)  1 / (n + m) - 1 / (Suc n + m)"
        using a_le[of "n + m"] x  1 by simp
    qed
    also have " = 1 / m"
      using telescope by (simp add: sums_iff)
    also have "x  m" "m > 0"
      unfolding m_def using x  1 by linarith+
    hence "1 / m  1 / x"
      using x  1 by (intro divide_left_mono) (auto simp: m_def)
    finally show ?case .
  qed

  moreover have "eventually (λx::real. 1 / x  1 / ln x) at_top" by real_asymp
  ultimately have "eventually (λx. B - sum_upto a x  1 / ln x) at_top"
    by eventually_elim (rule order.trans)

  hence "eventually (λx. ¦R x¦  5 / ln x) at_top"
    using eventually_ge_at_top[of 2]
  proof eventually_elim
    case (elim x)
    have "¦(B - sum_upto a x) - (prime_sum_upto (λp. 1 / p) x - ln (ln x) - meissel_mertens)¦ 
             1 / ln x + 4 / ln x"
    proof (intro order.trans[OF abs_triangle_ineq4 add_mono])
      show "¦prime_sum_upto (λp. 1 / real p) x - ln (ln x) - meissel_mertens¦  4 / ln x"
        by (intro mertens_second_theorem x  2)
      have "sum_upto a x  B"
        unfolding B_def sum_upto_def by (intro sum_le_suminf summable a a_nonneg ballI) auto
      thus "¦B - sum_upto a x¦  1 / ln x"
        using elim by linarith
    qed
    also have "sum_upto a x = prime_sum_upto (λp. -ln (1 - 1 / p) - 1 / p) x"
      unfolding sum_upto_def prime_sum_upto_altdef1 a_def by (intro sum.cong allI) auto
    also have " = -S x - prime_sum_upto (λp. 1 / p) x"
      by (simp add: a_def S_def Pr_def prime_sum_upto_def sum_subtractf sum_negf)
    finally show "¦R x¦  5 / ln x"
      by (simp add: R_def)
  qed

  moreover have "eventually (λx::real. ¦5 / ln x¦ < 1 / 2) at_top" by real_asymp
  ultimately have "eventually (λx. exp (R x) - 1  {-5 / ln x..10 / ln x}) at_top"
    using eventually_gt_at_top[of 1]
  proof eventually_elim
    case (elim x)
    have "exp (R x)  exp (5 / ln x)"
      using elim by simp
    also have "  1 + 10 / ln x"
      using real_exp_bound_lemma[of "5 / ln x"] elim by (simp add: abs_if split: if_splits)
    finally have le: "exp (R x)  1 + 10 / ln x" .

    have "1 + (-5 / ln x)  exp (-5 / ln x)"
      by (rule exp_ge_add_one_self)
    also have "exp (-5 / ln x)  exp (R x)"
      using elim by simp
    finally have "exp (R x)  1 - 5 / ln x" by simp
    with le show ?case by simp
  qed

  thus "eventually (λx. ¦(pPr x. 1 - 1 / real p) - C / ln x¦  10 * C / ln x ^ 2) at_top"
    using eventually_gt_at_top[of "exp 1"] eventually_gt_at_top[of 1]
  proof eventually_elim
    case (elim x)
    have "¦exp (R x) - 1¦  10 / ln x"
      using elim by (simp add: abs_if)
    from elim have "¦exp (S x) - C / ln x¦ = C / ln x * ¦exp (R x) - 1¦"
      by (simp add: R_def exp_add C_eq exp_diff exp_minus field_simps)
    also have "  C / ln x * (10 / ln x)"
      using elim by (intro mult_left_mono) (auto simp: C_eq)
    finally show ?case by (simp add: exp_S power2_eq_square mult_ac)
  qed

  thus "(λx. (pPr x. 1 - 1 / real p) - C / ln x)  O(λx. 1 / ln x ^ 2)"
    by (intro bigoI[of _ "10  * C"]) auto
qed

lemma mertens_third_theorem_asymp_equiv:
  "(λx. (p | prime p  real p  x. 1 - 1 / real p)) ∼[at_top]
     (λx. third_mertens_const / ln x)"
  by (rule smallo_imp_asymp_equiv[OF landau_o.big_small_trans[OF mertens_third_theorem]])
     (use third_mertens_const_pos in real_asymp)

text ‹
  We now show an equivalent version where $\prod_{p\leq x} (1 - 1 / p)$ is replaced
  by $\prod_{i=1}^k (1 - 1 / p_i)$:
›
lemma mertens_third_convert:
  assumes "n > 0"
  shows "(k<n. 1 - 1 / real (nth_prime k)) =
           (p | prime p  p  nth_prime (n - 1). 1 - 1 / p)"
proof -
  have "primorial' n = primorial (nth_prime (n - 1))"
    using assms by (simp add: primorial'_conv_primorial)
  also have "real (totient ) =
               primorial' n * (p | prime p  p  nth_prime (n - 1). 1 - 1 / p)"
    using assms by (subst totient_primorial) (auto simp: primorial'_conv_primorial)
  finally show ?thesis
    by (simp add: totient_primorial')
qed

lemma (in prime_number_theorem) mertens_third_theorem_asymp_equiv':
  "(λn. (k<n. 1 - 1 / nth_prime k)) ∼[at_top] (λx. third_mertens_const / ln x)"
proof -
  have lim: "filterlim (λn. real (nth_prime (n - 1))) at_top at_top"
    by (intro filterlim_compose[OF filterlim_real_sequentially]
              filterlim_compose[OF nth_prime_at_top]) real_asymp
  have "(λn. (k<n. 1 - 1 / nth_prime k)) ∼[at_top]
          (λn. (p | prime p  real p  real (nth_prime (n - 1)). 1 - 1 / p))"
    by (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top[of 0]])
       (subst mertens_third_convert, auto)
  also have " ∼[at_top] (λn. third_mertens_const / ln (real (nth_prime (n - 1))))"
    by (intro asymp_equiv_compose'[OF mertens_third_theorem_asymp_equiv lim])
  also have " ∼[at_top] (λn. third_mertens_const / ln (real (n - 1)))"
    by (intro asymp_equiv_intros asymp_equiv_compose'[OF ln_nth_prime_asymp_equiv]) real_asymp
  also have " ∼[at_top] (λn. third_mertens_const / ln (real n))"
    using third_mertens_const_pos by real_asymp
  finally show ?thesis .
qed


subsection ‹Bounds on Euler's totient function›

text ‹
  Similarly to the divisor function, we will show that $\varphi(n)$ has minimal order
  $C n / \ln\ln n$.

  The first part is to show the lower bound:
›
theorem totient_lower_bound:
  fixes ε :: real
  assumes "ε > 0"
  defines "C  third_mertens_const"
  shows "eventually (λn. totient n > (1 - ε) * C * n / ln (ln n)) at_top"
proof -
  include prime_counting_notation
  define f :: "nat  nat" where "f = (λn. card {pprime_factors n. p > ln n})"

  define lb1 where "lb1 = (λn::nat. (p | prime p  real p  ln n. 1 - 1 / p))"
  define lb2 where "lb2 = (λn::nat. (1 - 1 / ln n) powr (ln n / ln (ln n)))"
  define lb1' where "lb1' = (λn::nat. C / ln (ln n) - 10 * C / ln (ln n) ^ 2)"

  have "eventually (λn::nat. 1 + log 2 n  ln n ^ 2) at_top"  by real_asymp
  hence "eventually (λn. totient n / n  lb1 n * lb2 n) at_top"
    using eventually_gt_at_top[of 2]
  proof eventually_elim
    fix n :: nat
    assume n: "n > 2" and "1 + log 2 n  ln n ^ 2"

    define Pr where [simp]: "Pr = prime_factors n"
    define Pr1 where [simp]: "Pr1 = {pPr. p  ln n}"
    define Pr2 where [simp]: "Pr2 = {pPr. p > ln n}"
  
    have "exp 1 < real n"
      using e_less_272 n > 2 by linarith
    hence "ln (exp 1) < ln (real n)"
      using n > 2 by (subst ln_less_cancel_iff) auto
    hence "1 < ln n" by simp
    hence "ln (ln n) > ln (ln (exp 1))"
      by (subst ln_less_cancel_iff) auto
    hence "ln (ln n) > 0" by simp
  
    have "ln n ^ f n  (pPr2. ln n)"
      by (simp add: f_def)
    also have "  real (pPr2. p)" unfolding of_nat_prod
      by (intro prod_mono) (auto dest: prime_gt_1_nat simp: in_prime_factors_iff)
    also {
      have "(pPr2. p) dvd (pPr2. p ^ multiplicity p n)"
        by (intro prod_dvd_prod dvd_power) (auto simp: prime_factors_multiplicity)
      also have " dvd (pPr. p ^ multiplicity p n)"
        by (intro prod_dvd_prod_subset2) auto
      also have " = n"
        using n > 2 by (subst (2) prime_factorization_nat[of n]) auto
      finally have "(pPr2. p)  n"
        using n > 2 by (intro dvd_imp_le) auto
    }
    finally have "ln (ln n ^ f n)  ln n"
      using n > 2 by (subst ln_le_cancel_iff) auto
    also have "ln (ln n ^ f n) = f n * ln (ln n)"
      using n > 2 by (subst ln_realpow) auto
    finally have f_le: "f n  ln n / ln (ln n)"
      using ln (ln n) > 0 by (simp add: field_simps)

    have "(1 - 1 / ln n) powr (ln n / ln (ln n))  (1 - 1 / ln n) powr (real (f n))"
      using n > 2 and ln n > 1 by (intro powr_mono' f_le) auto
    also have " = (pPr2. 1 - 1 / ln n)"
      using n > 2 and ln n > 1 by (subst powr_realpow) (auto simp: f_def)
    also have "  (pPr2. 1 - 1 / p)"
      using n > 2 and ln n > 1
      by (intro prod_mono conjI diff_mono divide_left_mono) (auto dest: prime_gt_1_nat)
    finally have bound2: "(pPr2. 1 - 1 / p)  lb2 n" unfolding lb2_def .

    have "(p | prime p  real p  ln n. inverse (1 - 1 / p))  (pPr1. inverse (1 - 1 / p))"
      using n > 2 by (intro prod_mono2) (auto intro: finite_primes_le  dest: prime_gt_1_nat                                                simp: in_prime_factors_iff field_simps)
    hence "inverse (p | prime p  real p  ln n. 1 - 1 / p)  inverse (pPr1. 1 - 1 / p)"
      by (subst (1 2) prod_inversef [symmetric]) auto
    hence bound1: "(pPr1. 1 - 1 / p)  lb1 n" unfolding lb1_def
      by (rule inverse_le_imp_le)
         (auto intro!: prod_pos simp: in_prime_factors_iff dest: prime_gt_1_nat)

    have "lb1 n * lb2 n  (pPr1. 1 - 1 / p) * (pPr2. 1 - 1 / p)"
      by (intro mult_mono bound1 bound2 prod_nonneg ballI)
         (auto simp: in_prime_factors_iff lb1_def lb2_def dest: prime_gt_1_nat)
    also have " = (pPr1  Pr2. 1 - 1 / p)"
      by (subst prod.union_disjoint) auto
    also have "Pr1  Pr2 = Pr" by auto
    also have "(pPr. 1 - 1 / p) = totient n / n"
      using n by (subst totient_formula2) auto
    finally show "real (totient n) / real n  lb1 n * lb2 n"
      by (simp add: lb1_def lb2_def)
  qed

  moreover have "eventually (λn. ¦lb1 n - C / ln (ln n)¦  10 * C / ln (ln n) ^ 2) at_top"
    unfolding lb1_def C_def using mertens_third_theorem_strong
    by (rule eventually_compose_filterlim) real_asymp

  moreover have "eventually (λn. (1 - ε) * C / ln (ln n) < lb1' n * lb2 n) at_top"
    unfolding lb1'_def lb2_def C_def using third_mertens_const_pos ε > 0 by real_asymp

  ultimately show "eventually (λn. totient n > (1 - ε) * C * n / ln (ln n)) at_top"
    using eventually_gt_at_top[of 0]
  proof eventually_elim
    case (elim n)
    have "(1 - ε) * C / ln (ln n) < lb1' n * lb2 n" by fact
    also have "lb1' n  lb1 n"
      unfolding lb1'_def using elim by linarith
    hence "lb1' n * lb2 n  lb1 n * lb2 n"
      by (intro mult_right_mono) (auto simp: lb2_def)
    also have "  totient n / n" by fact
    finally show "totient n > (1 - ε) * C * n / (ln (ln n))"
      using n > 0 by (simp add: field_simps)
  qed
qed

text ‹
  Next, we examine the `worst case' of $\varphi(n)$ where n› is the primorial of $x$.
  In this case, we have $\varphi(n) < c n / \ln\ln n$ for any $c > C$ for all sufficiently
  large $n$.
›
theorem (in prime_number_theorem) totient_primorial_less:
  fixes ε :: real
  defines "C  third_mertens_const" and "h  primorial"
  assumes "ε > 0"
  shows   "eventually (λx. totient (h x) < (1 + ε) * C * h x / ln (ln (h x))) at_top"
proof -
  have "C > 0" by (simp add: C_def third_mertens_const_pos)

  have "(λx. (1 + ε) * C / ln (ln (h x))) ∼[at_top] (λx. (1 + ε) * C / ln (θ x))"
    by (simp add: ln_primorial h_def)
  also have " ∼[at_top] (λx. (1 + ε) * C / ln x)"
    by (intro asymp_equiv_intros ln_θ_asymp_equiv)
  finally have "(λx. (1 + ε) * C / ln (ln (h x)) - (1 + ε) * C / ln x)  o(λx. (1 + ε) * C / ln x)"
    by (rule asymp_equiv_imp_diff_smallo)
  also have "(λx. (1 + ε) * C / ln x)  O(λx. 1 / ln x)"
    by real_asymp
  also have "(λx. (1 + ε) * C / ln (ln (h x)) - (1 + ε) * C / ln x) =
               (λx. (1 + ε) * C / ln (ln (h x)) - C / ln x - ε * C / ln x)"
    by (simp add: algebra_simps fun_eq_iff add_divide_distrib)
  finally have "(λx. (1 + ε) * C / ln (ln (h x)) - C / ln x - ε * C / ln x)  o(λx. 1 / ln x)" .
  hence "(λx. (1 + ε) * C / ln (ln (h x)) - C / ln x - ε * C / ln x - 
           ((p{p. prime p  real p  x}. 1 - 1 / real p) - C / ln x))  o(λx. 1 / ln x)"
    unfolding C_def
    by (rule sum_in_smallo[OF _ landau_o.big_small_trans[OF mertens_third_theorem]]) real_asymp+
  hence "(λx. ((1 + ε) * C / ln (ln (h x)) - (p{p. prime p  real p  x}. 1 - 1 / real p)) -
                 (ε * C / ln x))  o(λx. 1 / ln x)"
    by (simp add: algebra_simps)
  also have "(λx. 1 / ln x)  O(λx. ε * C / ln x)"
    using ε > 0 by (simp add: landau_divide_simps C_def third_mertens_const_def)
  finally have "(λx. (1 + ε) * C / ln (ln (h x)) - (p | prime p  real p  x. 1 - 1 / p))
                  ∼[at_top] (λx. ε * C / ln x)"
    by (rule smallo_imp_asymp_equiv)

  hence "eventually (λx. (1 + ε) * C / ln (ln (h x)) - (p | prime p  real p  x. 1 - 1 / p) > 0
                           ε * C / ln x > 0) at_top"
    by (rule asymp_equiv_eventually_pos_iff)
  moreover have "eventually (λx. ε * C / ln x > 0) at_top"
    using ε > 0 C > 0 by real_asymp
  ultimately have "eventually (λx. (1 + ε) * C / ln (ln (h x)) >
                      (p | prime p  real p  x. 1 - 1 / p)) at_top"
    by eventually_elim auto
  thus ?thesis
  proof eventually_elim
    case (elim x)
    have "h x > 0" by (auto simp: h_def primorial_def intro!: prod_pos dest: prime_gt_0_nat)
    have "h x * ((1 + ε) * C / ln (ln (h x))) > totient (h x)"
      using elim primorial_pos[of x] unfolding h_def totient_primorial
      by (intro mult_strict_left_mono) auto
    thus ?case by (simp add: mult_ac)
  qed
qed

text ‹
  It follows that infinitely many values of n› exceed $c n / \ln (\ln n)$ when c› is chosen
  larger than C›.
›
corollary (in prime_number_theorem) totient_upper_bound:
  assumes "ε > 0"
  defines "C  third_mertens_const"
  shows   "frequently (λn. totient n < (1 + ε) * C * n / ln (ln n)) at_top"
proof -
  define h where "h = primorial"
  have "eventually (λn. totient n < (1 + ε) * C * n / ln (ln n)) (filtermap h at_top)"
    using totient_primorial_less[OF assms(1)] by (simp add: eventually_filtermap C_def h_def)
  hence "frequently (λn. totient n < (1 + ε) * C * n / ln (ln n)) (filtermap h at_top)"
    by (intro eventually_frequently) (auto simp: filtermap_bot_iff)
  moreover from this and primorial_at_top
    have "filtermap h at_top  at_top" by (simp add: filterlim_def h_def)
  ultimately show ?thesis
    by (rule frequently_mono_filter)
qed

text ‹
  Again, the following alternative formulation is somewhat nicer to prove:
›
lemma (in prime_number_theorem) totient_primorial'_asymp_equiv:
  "(λk. totient (primorial' k)) ∼[at_top] (λk. third_mertens_const * primorial' k / ln k)"
proof -
  let ?C = third_mertens_const
  have "(λk. totient (primorial' k)) ∼[at_top] (λk. primorial' k * (i<k. 1 - 1 / nth_prime i))"
    by (subst totient_primorial') auto
  also have " ∼[at_top] (λk. primorial' k * (?C / ln k))"
    by (intro asymp_equiv_intros mertens_third_theorem_asymp_equiv')
  finally show ?thesis by (simp add: algebra_simps)
qed

lemma (in prime_number_theorem) totient_primorial'_asymp_equiv':
  "(λk. totient (primorial' k)) ∼[at_top]
      (λk. third_mertens_const * primorial' k / ln (ln (primorial' k)))"
proof -
  let ?C = third_mertens_const
  have "(λk. totient (primorial' k)) ∼[at_top] (λk. third_mertens_const * primorial' k / ln k)"
    by (rule totient_primorial'_asymp_equiv)
  also have " ∼[at_top] (λk. third_mertens_const * primorial' k / ln (ln (primorial' k)))"
    by (intro asymp_equiv_intros asymp_equiv_symI[OF ln_ln_primorial'_asymp_equiv])
  finally show ?thesis .
qed

text ‹
  All in all, $\varphi(n)$ has minimal order $cn / \ln\ln n$:
›
theorem (in prime_number_theorem)
  liminf_totient: "liminf (λn. totient n * ln (ln n) / n) = third_mertens_const"
    (is "_ = ereal ?c")
proof (intro antisym)
  have "(λk. totient (primorial' k) / (?c * primorial' k / ln (ln (primorial' k))))  1"
    using totient_primorial'_asymp_equiv'
    by (intro asymp_equivD_strong eventually_mono[OF eventually_gt_at_top[of 1]]) auto
  hence "(λk. totient (primorial' k) / (?c * primorial' k / ln (ln (primorial' k))) * ?c)
              1 * ?c" by (intro tendsto_mult) auto
  hence "(λk. totient (primorial' k) / (primorial' k / ln (ln (primorial' k))))  ?c"
    using third_mertens_const_pos by simp
  hence "liminf ((λn. totient n * ln (ln n) / n)  primorial') = ereal ?c"
    by (intro lim_imp_Liminf tendsto_ereal) simp_all
  hence "?c = liminf ((λn. ereal (totient n * ln (ln n) / n))  primorial')"
    by (simp add: o_def)
  also have "  liminf (λn. totient n * ln (ln n) / n)"
    using strict_mono_primorial' by (rule liminf_subseq_mono)
  finally show "liminf (λn. totient n * ln (ln n) / n)  ?c" .
next
  show "liminf (λn. totient n * ln (ln n) / n)  ?c"
    unfolding le_Liminf_iff
  proof safe
    fix C' assume "C' < ereal ?c"
    from ereal_dense2[OF this] obtain C where C: "C < ?c" "ereal C > C'" by auto
    define ε where "ε = 1 - C / ?c"
    from C have "ε > 0" using third_mertens_const_pos by (simp add: ε_def)

    have "eventually (λn::nat. ln (ln n) > 0) at_top" by real_asymp
    hence "eventually (λn. totient n * ln (ln n) / n > C) at_top"
      using totient_lower_bound[OF ε > 0] eventually_gt_at_top[of 1]
    proof eventually_elim
      case (elim n)
      hence "totient n * ln (ln n) / n > (1 - ε) * ?c"
        by (simp add: field_simps)
      also have "(1 - ε) * ?c = C"
        using third_mertens_const_pos by (simp add: field_simps ε_def)
      finally show ?case .
    qed
    thus "eventually (λn. ereal (totient n * ln (ln n) / n) > C') at_top"
      by eventually_elim (rule less_trans[OF C(2)], auto)
  qed
qed

(*<*)
unbundle no_prime_counting_notation
(*>*)

end