# 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"

lemma nth_prime_2 [simp]: "nth_prime 2 = 5"

lemma nth_prime_3 [simp]: "nth_prime 3 = 7"

(* 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)"
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"
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)"
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]

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)"
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]
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"
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)"
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⌋)"
finally show ?thesis by simp
qed

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. ∀x≥x0. ¦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. ∀x≥1. 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))"
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)"
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"
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. ∀x≥1. ¦sum_upto f x - g x¦ ≤ c * h x"
proof -
have "∃c>0. ∀x≥1. 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. ∀x≥1. 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"
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))"
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])
algebra_simps sum_distrib_left sum_distrib_right)
finally show ?thesis .
qed

(* 2.22 *)
lemma dirichlet_prod'_inversion1:
assumes "∀x≥1. 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 "∀x≥1. 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   "(∀x≥1. g x = dirichlet_prod' a f x) ⟷ (∀x≥1. 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   "(∀x≥1. g x = dirichlet_prod' a f x) ⟷ (∀x≥1. 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
show ?thesis
using sum_upto_dirichlet_prod[of "λn. 1::real" f] sum_upto_dirichlet_prod[of f "λn. 1::real"]
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))"
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})"
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"
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"
also have "fds moebius_mu * fds_zeta = 1"
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   "(∀x≥1. g x = dirichlet_prod' a f x) ⟷
(∀x≥1. 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"

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⌋)))"
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"
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)"
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)))"
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)"
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"

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))"
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)"
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)"
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"

lemma primes_omega_0 [simp]: "primes_omega 0 = 0"

lemma primes_omega_1 [simp]: "primes_omega 1 = 0"

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

lemma primes_omega_power [simp]: "n > 0 ⟹ primes_omega (x ^ n) = primes_omega x"

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 = (∏p∈prime_factors n. Suc (multiplicity p n))"
using assms by (subst divisor_count.prod_prime_factors') auto
also have "… = (∏p∈prime_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"
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 * (∏p∈prime_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"

lemma primorial'_Suc: "primorial' (Suc n) = nth_prime n * primorial' n"

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)"
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 "… = (∑p∈nth_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}"

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)"
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))"
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"
also have "(∏p∈prime_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⌋)"
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))"
also have "Lcm {1..n} * … = exp (ψ (real n + 1))"
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)"
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"])
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: "∃c≥0. ∀x≥0. x * A x - T x ∈ {0..c*x}"
and asymptotics:       "(λx. A x - ln x) ∈ O(λ_. 1)"
and upper:             "∃c≥0. ∀x≥0. S x ≤ c * x"
and lower:             "∃c>0. ∀x≥1/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" "∀n≥1. ¦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 "∃c≥0. ∀x≥0. 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 "∃c≥0. ∀x≥0. 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)"
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"
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)"
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. ∀x≥1/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

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
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)"
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
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)) = (∑i∈insert 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"
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)"
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. ∀x≥1. ¦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

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. ∀x≥1. ¦sum_upto (λn. n powr -s) x - x powr (1-s) / (1-s)¦ ≤ c"
proof -
have "∃c>0. ∀x≥1. ¦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
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. ∀x≥1. ¦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)"
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 "∀x≥1. ¦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" "∀x≥1. ¦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" "∀x≥1. ¦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
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]]
qed

lemma zeta_partial_sum_le_neg:
assumes "s > 0"
shows   "∃c>0. ∀x≥1. ¦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" "∀x≥1. ¦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 -
(∑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_field_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
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)"
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"
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"
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)"
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"

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"
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"
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"
finally have "¦H x¦ ≤ (1 + ε + ψ A) * x + ε * x * ln x"
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"
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"
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"
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"
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"
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_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 "(∑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)"
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:    `