Theory Arithmetic_Summatory_Asymptotics
section ‹Asymptotics of summatory arithmetic functions›
theory Arithmetic_Summatory_Asymptotics
imports
Euler_MacLaurin.Euler_MacLaurin_Landau
Arithmetic_Summatory
Dirichlet_Series_Analysis
Landau_Symbols.Landau_More
begin
subsection ‹Auxiliary bounds›
lemma sum_inverse_squares_tail_bound:
assumes "d > 0"
shows "summable (λn. 1 / (real (Suc n) + d) ^ 2)"
"(∑n. 1 / (real (Suc n) + d) ^ 2) ≤ 1 / d"
proof -
show *: "summable (λn. 1 / (real (Suc n) + d) ^ 2)"
proof (rule summable_comparison_test, intro allI exI impI)
fix n :: nat
from assms show "norm (1 / (real (Suc n) + d) ^ 2) ≤ 1 / real (Suc n) ^ 2"
unfolding norm_divide norm_one norm_power
by (intro divide_left_mono power_mono) simp_all
qed (insert inverse_squares_sums, simp add: sums_iff)
show "(∑n. 1 / (real (Suc n) + d) ^ 2) ≤ 1 / d"
proof (rule sums_le)
fix n have "1 / (real (Suc n) + d) ^ 2 ≤ 1 / ((real n + d) * (real (Suc n) + d))"
unfolding power2_eq_square using assms
by (intro divide_left_mono mult_mono mult_pos_pos add_nonneg_pos) simp_all
also have "… = 1 / (real n + d) - 1 / (real (Suc n) + d)"
using assms by (simp add: divide_simps)
finally show "1 / (real (Suc n) + d)⇧2 ≤ 1 / (real n + d) - 1 / (real (Suc n) + d)" .
next
show "(λn. 1 / (real (Suc n) + d)⇧2) sums (∑n. 1 / (real (Suc n) + d)⇧2)"
using * by (simp add: sums_iff)
next
have "(λn. 1 / (real n + d) - 1 / (real (Suc n) + d)) sums (1 / (real 0 + d) - 0)"
by (intro telescope_sums' real_tendsto_divide_at_top[OF tendsto_const],
subst add.commute, rule filterlim_tendsto_add_at_top[OF tendsto_const
filterlim_real_sequentially])
thus "(λn. 1 / (real n + d) - 1 / (real (Suc n) + d)) sums (1 / d)" by simp
qed
qed
lemma moebius_sum_tail_bound:
assumes "d > 0"
shows "abs (∑n. moebius_mu (Suc n + d) / real (Suc n + d)^2) ≤ 1 / d" (is "abs ?S ≤ _")
proof -
have *: "summable (λn. 1 / (real (Suc n + d))⇧2)"
by (insert sum_inverse_squares_tail_bound(1)[of "real d"] assms, simp_all add: add_ac)
have **: "summable (λn. abs (moebius_mu (Suc n + d) / real (Suc n + d)^2))"
proof (rule summable_comparison_test, intro exI allI impI)
fix n :: nat
show "norm (¦moebius_mu (Suc n + d) / (real (Suc n + d))^2¦) ≤
1 / (real (Suc n + d))^2"
unfolding real_norm_def abs_abs abs_divide power_abs abs_of_nat
by (intro divide_right_mono abs_moebius_mu_le) simp_all
qed (insert *)
from ** have "abs ?S ≤ (∑n. abs (moebius_mu (Suc n + d) / real (Suc n + d)^2))"
by (rule summable_rabs)
also have "… ≤ (∑n. 1 / (real (Suc n) + d) ^ 2)"
proof (intro suminf_le allI)
fix n :: nat
show "abs (moebius_mu (Suc n + d) / (real (Suc n + d))^2) ≤ 1 / (real (Suc n) + real d)^2"
unfolding abs_divide abs_of_nat power_abs of_nat_add [symmetric]
by (intro divide_right_mono abs_moebius_mu_le) simp_all
qed (insert * **, simp_all add: add_ac)
also from assms have "… ≤ 1 / d" by (intro sum_inverse_squares_tail_bound) simp_all
finally show ?thesis .
qed
lemma sum_upto_inverse_bound:
"sum_upto (λi. 1 / real i) x ≥ 0"
"eventually (λx. sum_upto (λi. 1 / real i) x ≤ ln x + 13 / 22) at_top"
proof -
show "sum_upto (λi. 1 / real i) x ≥ 0"
by (simp add: sum_upto_def sum_nonneg)
from order_tendstoD(2)[OF euler_mascheroni_LIMSEQ euler_mascheroni_less_13_over_22]
obtain N where N: "⋀n. n ≥ N ⟹ harm n - ln (real n) < 13 / 22"
unfolding eventually_at_top_linorder by blast
show "eventually (λx. sum_upto (λi. 1 / real i) x ≤ ln x + 13 / 22) at_top"
using eventually_ge_at_top[of "max (real N) 1"]
proof eventually_elim
case (elim x)
have "sum_upto (λi. 1 / real i) x = (∑i∈{0<..nat ⌊x⌋}. 1 / real i)"
by (simp add: sum_upto_altdef)
also have "… = harm (nat ⌊x⌋)"
unfolding harm_def by (intro sum.cong refl) (auto simp: field_simps)
also have "… ≤ ln (real (nat ⌊x⌋)) + 13 / 22"
using N[of "nat ⌊x⌋"] elim by (auto simp: le_nat_iff le_floor_iff)
also have "ln (real (nat ⌊x⌋)) ≤ ln x" using elim by (subst ln_le_cancel_iff) auto
finally show ?case by - simp
qed
qed
lemma sum_upto_inverse_bigo: "sum_upto (λi. 1 / real i) ∈ O(λx. ln x)"
proof -
have "eventually (λx. norm (sum_upto (λi. 1 / real i) x) ≤ 1 * norm (ln x + 13/22)) at_top"
using eventually_ge_at_top[of "1::real"] sum_upto_inverse_bound(2)
by eventually_elim (insert sum_upto_inverse_bound(1), simp_all)
hence "sum_upto (λi. 1 / real i) ∈ O(λx. ln x + 13/22)"
by (rule bigoI)
also have "(λx::real. ln x + 13/22) ∈ O(λx. ln x)" by simp
finally show ?thesis .
qed
lemma
defines "G ≡ (λx::real. (∑n. moebius_mu (n + Suc (nat ⌊x⌋)) / (n + Suc (nat ⌊x⌋))^2) :: real)"
shows moebius_sum_tail_bound': "⋀t. t ≥ 2 ⟹ ¦G t¦ ≤ 1 / (t - 1)"
and moebius_sum_tail_bigo: "G ∈ O(λt. 1 / t)"
proof -
show "¦G t¦ ≤ 1 / (t - 1)" if t: "t ≥ 2" for t
proof -
from t have "¦G t¦ ≤ 1 / real (nat ⌊t⌋)"
unfolding G_def using moebius_sum_tail_bound[of "nat ⌊t⌋"] by simp
also have "t ≤ 1 + real_of_int ⌊t⌋" by linarith
hence "1 / real (nat ⌊t⌋) ≤ 1 / (t - 1)" using t by (simp add: field_simps)
finally show ?thesis .
qed
hence "G ∈ O(λt. 1 / (t - 1))"
by (intro bigoI[of _ 1] eventually_mono[OF eventually_ge_at_top[of "2::real"]]) auto
also have "(λt::real. 1 / (t - 1)) ∈ Θ(λt. 1 / t)" by simp
finally show "G ∈ O(λt. 1 / t)" .
qed
subsection ‹Summatory totient function›
theorem summatory_totient_asymptotics:
"(λx. sum_upto (λn. real (totient n)) x - 3 / pi⇧2 * x⇧2) ∈ O(λx. x * ln x)"
proof -
define H where "H = (λx. of_int (floor x) * (of_int (floor x) + 1) / 2 - x ^ 2 / 2 :: real)"
define H' where "H' = (λx. sum_upto (λn. moebius_mu n * H (x / real n)) x)"
have H: "sum_upto real x = x^2/2 + H x" if "x ≥ 0" for x
using that by (simp add: sum_upto_real H_def)
define G where "G = (λx::real. (∑n. moebius_mu (n + Suc (nat ⌊x⌋)) / (n + Suc (nat ⌊x⌋))^2))"
have H_bound: "¦H t¦ ≤ t / 2" if "t ≥ 0" for t
proof -
have "H t - t / 2 = (-(t - of_int (floor t))) * (floor t + t + 1) / 2"
by (simp add: H_def field_simps power2_eq_square)
also have "… ≤ 0" using that by (intro mult_nonpos_nonneg divide_nonpos_nonneg) simp_all
finally have "H t ≤ t / 2" by simp
have "-H t - t / 2 = (t - of_int (floor t) - 1) * (of_int (floor t) + t) / 2"
by (simp add: H_def field_simps power2_eq_square)
also have "… ≤ 0" using that
by (intro divide_nonpos_nonneg mult_nonpos_nonneg) ((simp; fail) | linarith)+
finally have "-H t ≤ t / 2" by simp
with ‹H t ≤ t / 2› show "¦H t¦ ≤ t / 2" by simp
qed
have H'_bound: "¦H' t¦ ≤ t / 2 * sum_upto (λi. 1 / real i) t" if "t ≥ 0" for t
proof -
have "¦H' t¦ ≤ (∑i | 0 < i ∧ real i ≤ t. ¦moebius_mu i * H (t / real i)¦)"
unfolding H'_def sum_upto_def by (rule sum_abs)
also have "… ≤ (∑i | 0 < i ∧ real i ≤ t. 1 * ((t / real i) / 2))"
unfolding abs_mult using that
by (intro sum_mono mult_mono abs_moebius_mu_le H_bound) simp_all
also have "… = t / 2 * sum_upto (λi. 1 / real i) t"
by (simp add: sum_upto_def sum_distrib_left sum_distrib_right mult_ac)
finally show ?thesis .
qed
hence "H' ∈ O(λt. t * sum_upto (λi. 1 / real i) t)"
using sum_upto_inverse_bound(1)
by (intro bigoI[of _ "1/2"] eventually_mono[OF eventually_ge_at_top[of "0::real"]])
(auto elim!: eventually_mono simp: abs_mult)
also have "(λt. t * sum_upto (λi. 1 / real i) t) ∈ O(λt. t * ln t)"
by (intro landau_o.big.mult sum_upto_inverse_bigo) simp_all
finally have H'_bigo: "H' ∈ O(λx. x * ln x)" .
{
fix x :: real assume x: "x ≥ 0"
have "sum_upto (λn. real (totient n)) x = sum_upto (λn. of_int (int (totient n))) x"
by simp
also have "… = sum_upto (λn. moebius_mu n * sum_upto real (x / real n)) x"
by (subst totient_conv_moebius_mu) (simp add: sum_upto_dirichlet_prod of_int_dirichlet_prod)
also have "… = sum_upto (λn. moebius_mu n * ((x / real n) ^ 2 / 2 + H (x / real n))) x" using x
by (intro sum_upto_cong) (simp_all add: H)
also have "… = x^2 / 2 * sum_upto (λn. moebius_mu n / real n ^ 2) x + H' x"
by (simp add: sum_upto_def H'_def sum.distrib ring_distribs
sum_distrib_left sum_distrib_right power_divide mult_ac)
also have "sum_upto (λn. moebius_mu n / real n ^ 2) x =
(∑n∈{..<Suc (nat ⌊x⌋)}. moebius_mu n / real n ^ 2)"
unfolding sum_upto_altdef by (intro sum.mono_neutral_cong_left refl) auto
also have "… = 6 / pi ^ 2 - G x"
using sums_split_initial_segment[OF moebius_over_square_sums, of "Suc (nat ⌊x⌋)"]
by (auto simp: sums_iff algebra_simps G_def)
finally have "sum_upto (λn. real (totient n)) x = 3 / pi⇧2 * x⇧2 - x⇧2 / 2 * G x + H' x"
by (simp add: algebra_simps)
}
hence "(λx. sum_upto (λn. real (totient n)) x - 3 / pi^2 * x^2) ∈
Θ(λx. (-(x^2) / 2) * G x + H' x)"
by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of "0::real"]])
(auto elim!: eventually_mono)
also have "(λx. (-(x^2) / 2) * G x + H' x) ∈ O(λx. x * ln x)"
proof (intro sum_in_bigo H'_bigo)
have "(λx. (- (x^2) / 2) * G x) ∈ O(λx. x^2 * (1 / x))"
using moebius_sum_tail_bigo [folded G_def] by (intro landau_o.big.mult) simp_all
also have "(λx::real. x^2 * (1 / x)) ∈ O(λx. x * ln x)" by simp
finally show "(λx. (- (x^2) / 2) * G x) ∈ O(λx. x * ln x)" .
qed
finally show ?thesis .
qed
theorem summatory_totient_asymptotics':
"(λx. sum_upto (λn. real (totient n)) x) =o (λx. 3 / pi⇧2 * x⇧2) +o O(λx. x * ln x)"
using summatory_totient_asymptotics
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)
theorem summatory_totient_asymptotics'':
"sum_upto (λn. real (totient n)) ∼[at_top] (λx. 3 / pi⇧2 * x⇧2)"
proof -
have "(λx. sum_upto (λn. real (totient n)) x - 3 / pi⇧2 * x⇧2) ∈ O(λx. x * ln x)"
by (rule summatory_totient_asymptotics)
also have "(λx. x * ln x) ∈ o(λx. 3 / pi ^ 2 * x ^ 2)" by simp
finally show ?thesis by (simp add: asymp_equiv_altdef)
qed
subsection ‹Asymptotic distribution of squarefree numbers›
lemma le_sqrt_iff: "x ≥ 0 ⟹ x ≤ sqrt y ⟷ x^2 ≤ y"
using real_sqrt_le_iff[of "x^2" y] by (simp del: real_sqrt_le_iff)
theorem squarefree_asymptotics: "(λx. card {n. real n ≤ x ∧ squarefree n} - 6 / pi⇧2 * x) ∈ O(sqrt)"
proof -
define f :: "nat ⇒ real" where "f = (λn. if n = 0 then 0 else 1)"
define g :: "nat ⇒ real" where "g = dirichlet_prod (ind squarefree) moebius_mu"
interpret g: multiplicative_function g unfolding g_def
by (intro multiplicative_dirichlet_prod squarefree.multiplicative_function_axioms
moebius_mu.multiplicative_function_axioms)
interpret g: multiplicative_function' g "λp k. if k = 2 then -1 else 0" "λ_. 0"
proof
interpret g': multiplicative_dirichlet_prod' "ind squarefree" moebius_mu
"λp k. if 1 < k then 0 else 1" "λp k. if k = 1 then - 1 else 0" "λ_. 1" "λ_. - 1"
by (intro multiplicative_dirichlet_prod'.intro squarefree.multiplicative_function'_axioms
moebius_mu.multiplicative_function'_axioms)
fix p k :: nat assume "prime p" "k > 0"
hence "g (p ^ k) = (∑i∈{0<..<k}. (if Suc 0 < i then 0 else 1) *
(if k - i = Suc 0 then - 1 else 0))"
by (auto simp: g'.prime_power g_def)
also have "… = (∑i∈{0<..<k}. (if k = 2 then -1 else 0))"
by (intro sum.cong refl) auto
also from ‹k > 0› have "… = (if k = 2 then -1 else 0)" by simp
finally show "g (p ^ k) = …" .
qed simp_all
have mult_g_square: "multiplicative_function (λn. g (n ^ 2))"
by standard (simp_all add: power_mult_distrib g.mult_coprime)
have g_square: "g (m ^ 2) = moebius_mu m" for m
using mult_g_square moebius_mu.multiplicative_function_axioms
proof (rule multiplicative_function_eqI)
fix p k :: nat assume *: "prime p" "k > 0"
have "g ((p ^ k) ^ 2) = g (p ^ (2 * k))" by (simp add: power_mult [symmetric] mult_ac)
also from * have "… = (if k = 1 then -1 else 0)" by (simp add: g.prime_power)
also from * have "… = moebius_mu (p ^ k)" by (simp add: moebius_mu.prime_power)
finally show "g ((p ^ k) ^ 2) = moebius_mu (p ^ k)" .
qed
have g_nonsquare: "g m = 0" if "¬is_square m" for m
proof (cases "m = 0")
case False
from that False obtain p where p: "prime p" "odd (multiplicity p m)"
using is_nth_power_conv_multiplicity_nat[of 2 m] by auto
from p have "multiplicity p m ≠ 2" by auto
moreover from p have "p ∈ prime_factors m"
by (auto simp: prime_factors_multiplicity intro!: Nat.gr0I)
ultimately have "(∏p∈prime_factors m. if multiplicity p m = 2 then - 1 else 0 :: real) = 0"
(is "?P = _") by auto
also have "?P = g m" using False by (subst g.prod_prime_factors') auto
finally show ?thesis .
qed auto
have abs_g_le: "abs (g m) ≤ 1" for m
by (cases "is_square m")
(auto simp: g_square g_nonsquare abs_moebius_mu_le elim!: is_nth_powerE)
have fds_g: "fds g = fds_ind squarefree * fds moebius_mu"
by (rule fds_eqI) (simp add: g_def fds_nth_mult)
have "fds g * fds_zeta = fds_ind squarefree * (fds_zeta * fds moebius_mu)"
by (simp add: fds_g mult_ac)
also have "fds_zeta * fds moebius_mu = (1 :: real fds)"
by (rule fds_zeta_times_moebius_mu)
finally have *: "fds_ind squarefree = fds g * fds_zeta" by simp
have ind_squarefree: "ind squarefree = dirichlet_prod g f"
proof
fix n :: nat
from * show "ind squarefree n = dirichlet_prod g f n"
by (cases "n = 0") (simp_all add: fds_eq_iff fds_nth_mult f_def)
qed
define H :: "real ⇒ real"
where "H = (λx. sum_upto (λm. g (m^2) * (real_of_int ⌊x / real (m⇧2)⌋ - x / real (m^2))) (sqrt x))"
define J where "J = (λx::real. (∑n. moebius_mu (n + Suc (nat ⌊x⌋)) / (n + Suc (nat ⌊x⌋))^2))"
have "eventually (λx. norm (H x) ≤ 1 * norm (sqrt x)) at_top"
using eventually_ge_at_top[of "0::real"]
proof eventually_elim
case (elim x)
have "abs (H x) ≤ sum_upto (λm. abs (g (m^2) * (real_of_int ⌊x / real (m⇧2)⌋ -
x / real (m^2)))) (sqrt x)" (is "_ ≤ ?S") unfolding H_def sum_upto_def
by (rule sum_abs)
also have "x / (real m)⇧2 - real_of_int ⌊x / (real m)⇧2⌋ ≤ 1" for m by linarith
hence "?S ≤ sum_upto (λm. 1 * 1) (sqrt x)" unfolding abs_mult sum_upto_def
by (intro sum_mono mult_mono abs_g_le) simp_all
also have "… = of_int ⌊sqrt x⌋" using elim by (simp add: sum_upto_altdef)
also have "… ≤ sqrt x" by linarith
finally show ?case using elim by simp
qed
hence H_bigo: "H ∈ O(λx. sqrt x)" by (rule bigoI)
let ?A = "λx. card {n. real n ≤ x ∧ squarefree n}"
have "eventually (λx. ?A x - 6 / pi⇧2 * x = (-x) * J (sqrt x) + H x) at_top"
using eventually_ge_at_top[of "0::real"]
proof eventually_elim
fix x :: real assume x: "x ≥ 0"
have "{n. real n ≤ x ∧ squarefree n} = {n. n > 0 ∧ real n ≤ x ∧ squarefree n}"
by (auto intro!: Nat.gr0I)
also have "card … = sum_upto (ind squarefree :: nat ⇒ real) x"
by (rule sum_upto_ind [symmetric])
also have "… = sum_upto (λd. g d * sum_upto f (x / real d)) x" (is "_ = ?S")
unfolding ind_squarefree by (rule sum_upto_dirichlet_prod)
also have "sum f {0<..nat ⌊x / real i⌋} = of_int ⌊x / real i⌋" if "i > 0" for i
using x by (simp add: f_def)
hence "?S = sum_upto (λd. g d * of_int ⌊x / real d⌋) x"
unfolding sum_upto_altdef by (intro sum.cong refl) simp_all
also have "… = sum_upto (λm. g (m ^ 2) * of_int ⌊x / real (m ^ 2)⌋) (sqrt x)"
unfolding sum_upto_def
proof (intro sum.reindex_bij_betw_not_neutral [symmetric])
show "bij_betw power2 ({i. 0 < i ∧ real i ≤ sqrt x} - {})
({i. 0 < i ∧ real i ≤ x} - {i∈{0<..nat ⌊x⌋}. ¬is_square i})"
by (auto simp: bij_betw_def inj_on_def power_eq_iff_eq_base le_sqrt_iff
is_nth_power_def le_nat_iff le_floor_iff)
qed (auto simp: g_nonsquare)
also have "… = x * sum_upto (λm. g (m ^ 2) / real m ^ 2) (sqrt x) + H x"
by (simp add: H_def sum_upto_def sum.distrib ring_distribs sum_subtractf
sum_distrib_left sum_distrib_right mult_ac)
also have "sum_upto (λm. g (m ^ 2) / real m ^ 2) (sqrt x) =
sum_upto (λm. moebius_mu m / real m ^ 2) (sqrt x)"
unfolding sum_upto_altdef by (intro sum.cong refl) (simp_all add: g_square)
also have "sum_upto (λm. moebius_mu m / (real m)⇧2) (sqrt x) =
(∑m<Suc (nat ⌊sqrt x⌋). moebius_mu m / (real m) ^ 2)"
unfolding sum_upto_altdef by (intro sum.mono_neutral_cong_left) auto
also have "… = (6 / pi^2 - J (sqrt x))"
using sums_split_initial_segment[OF moebius_over_square_sums, of "Suc (nat ⌊sqrt x⌋)"]
by (auto simp: sums_iff algebra_simps J_def sum_upto_altdef)
finally show "?A x - 6 / pi⇧2 * x = (-x) * J (sqrt x) + H x"
by (simp add: algebra_simps)
qed
hence "(λx. ?A x - 6 / pi⇧2 * x) ∈ Θ(λx. (-x) * J (sqrt x) + H x)"
by (rule bigthetaI_cong)
also have "(λx. (-x) * J (sqrt x) + H x) ∈ O(λx. sqrt x)"
proof (intro sum_in_bigo H_bigo)
have "(λx. J (sqrt x)) ∈ O(λx. 1 / sqrt x)" unfolding J_def
using moebius_sum_tail_bigo sqrt_at_top by (rule landau_o.big.compose)
hence "(λx. (-x) * J (sqrt x)) ∈ O(λx. x * (1 / sqrt x))"
by (intro landau_o.big.mult) simp_all
also have "(λx::real. x * (1 / sqrt x)) ∈ Θ(λx. sqrt x)"
by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of "0::real"]])
(auto simp: field_simps)
finally show "(λx. (-x) * J (sqrt x)) ∈ O(λx. sqrt x)" .
qed
finally show ?thesis .
qed
theorem squarefree_asymptotics':
"(λx. card {n. real n ≤ x ∧ squarefree n}) =o (λx. 6 / pi⇧2 * x) +o O(λx. sqrt x)"
using squarefree_asymptotics
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)
theorem squarefree_asymptotics'':
"(λx. card {n. real n ≤ x ∧ squarefree n}) ∼[at_top] (λx. 6 / pi⇧2 * x)"
proof -
have "(λx. card {n. real n ≤ x ∧ squarefree n} - 6 / pi⇧2 * x) ∈ O(λx. sqrt x)"
by (rule squarefree_asymptotics)
also have "(sqrt :: real ⇒ real) ∈ Θ(λx. x powr (1/2))"
by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of "0::real"]])
(auto simp: powr_half_sqrt)
also have "(λx::real. x powr (1/2)) ∈ o(λx. 6 / pi ^ 2 * x)" by simp
finally show ?thesis by (simp add: asymp_equiv_altdef)
qed
subsection ‹The hyperbola method›
lemma hyperbola_method_bigo:
fixes f g :: "nat ⇒ 'a :: real_normed_field"
assumes "(λx. sum_upto (λn. f n * sum_upto g (x / real n)) (sqrt x) - R x) ∈ O(b)"
assumes "(λx. sum_upto (λn. sum_upto f (x / real n) * g n) (sqrt x) - S x) ∈ O(b)"
assumes "(λx. sum_upto f (sqrt x) * sum_upto g (sqrt x) - T x) ∈ O(b)"
shows "(λx. sum_upto (dirichlet_prod f g) x - (R x + S x - T x)) ∈ O(b)"
proof -
let ?A = "λx. (sum_upto (λn. f n * sum_upto g (x / real n)) (sqrt x) - R x) +
(sum_upto (λn. sum_upto f (x / real n) * g n) (sqrt x) - S x) +
(-(sum_upto f (sqrt x) * sum_upto g (sqrt x) - T x))"
have "(λx. sum_upto (dirichlet_prod f g) x - (R x + S x - T x)) ∈ Θ(?A)"
by (intro bigthetaI_cong eventually_mono[OF eventually_ge_at_top[of "0::real"]])
(auto simp: hyperbola_method_sqrt)
also from assms have "?A ∈ O(b)"
by (intro sum_in_bigo(1)) (simp_all only: landau_o.big.uminus_in_iff)
finally show ?thesis .
qed
lemma frac_le_1: "frac x ≤ 1"
unfolding frac_def by linarith
lemma ln_minus_ln_floor_bound:
assumes "x ≥ 2"
shows "ln x - ln (floor x) ∈ {0..<1 / (x - 1)}"
proof -
from assms have "ln (floor x) ≥ ln (x - 1)" by (subst ln_le_cancel_iff) simp_all
hence "ln x - ln (floor x) ≤ ln ((x - 1) + 1) - ln (x - 1)" by simp
also from assms have "… < 1 / (x - 1)" by (intro ln_diff_le_inverse) simp_all
finally have "ln x - ln (floor x) < 1 / (x - 1)" by simp
moreover from assms have "ln x ≥ ln (of_int ⌊x⌋)" by (subst ln_le_cancel_iff) simp_all
ultimately show ?thesis by simp
qed
lemma ln_minus_ln_floor_bigo:
"(λx::real. ln x - ln (floor x)) ∈ O(λx. 1 / x)"
proof -
have "eventually (λx. norm (ln x - ln (floor x)) ≤ 1 * norm (1 / (x - 1))) at_top"
using eventually_ge_at_top[of "2::real"]
proof eventually_elim
case (elim x)
with ln_minus_ln_floor_bound[OF this] show ?case by auto
qed
hence "(λx::real. ln x - ln (floor x)) ∈ O(λx. 1 / (x - 1))" by (rule bigoI)
also have "(λx::real. 1 / (x - 1)) ∈ O(λx. 1 / x)" by simp
finally show ?thesis .
qed
lemma divisor_count_asymptotics_aux:
"(λx. sum_upto (λn. sum_upto (λ_. 1) (x / real n)) (sqrt x) -
(x * ln x / 2 + euler_mascheroni * x)) ∈ O(sqrt)"
proof -
define R where "R = (λx. ∑i∈{0<..nat ⌊sqrt x⌋}. frac (x / real i))"
define S where "S = (λx. ln (real (nat ⌊sqrt x⌋)) - ln x / 2)"
have R_bound: "R x ∈ {0..sqrt x}" if x: "x ≥ 0" for x
proof -
have "R x ≤ (∑i∈{0<..nat ⌊sqrt x⌋}. 1)" unfolding R_def by (intro sum_mono frac_le_1)
also from x have "… = of_int ⌊sqrt x⌋" by simp
also have "… ≤ sqrt x" by simp
finally have "R x ≤ sqrt x" .
moreover have "R x ≥ 0" unfolding R_def by (intro sum_nonneg) simp_all
ultimately show ?thesis by simp
qed
have R_bound': "norm (R x) ≤ 1 * norm (sqrt x)" if "x ≥ 0" for x
using R_bound[OF that] that by simp
have R_bigo: "R ∈ O(sqrt)" using eventually_ge_at_top[of "0::real"]
by (intro bigoI[of _ 1], elim eventually_mono) (rule R_bound')
have "eventually (λx. sum_upto (λn. sum_upto (λ_. 1 :: real) (x / real n)) (sqrt x) =
x * harm (nat ⌊sqrt x⌋) - R x) at_top"
using eventually_ge_at_top[of "0 :: real"]
proof eventually_elim
case (elim x)
have "sum_upto (λn. sum_upto (λ_. 1 :: real) (x / real n)) (sqrt x) =
(∑i∈{0<..nat ⌊sqrt x⌋}. of_int ⌊x / real i⌋)" using elim
by (simp add: sum_upto_altdef)
also have "… = x * (∑i∈{0<..nat ⌊sqrt x⌋}. 1 / real i) - R x"
by (simp add: sum_subtractf frac_def R_def sum_distrib_left)
also have "{0<..nat ⌊sqrt x⌋} = {1..nat ⌊sqrt x⌋}" by auto
also have "(∑i∈…. 1 / real i) = harm (nat ⌊sqrt x⌋)" by (simp add: harm_def divide_simps)
finally show ?case .
qed
hence "(λx. sum_upto (λn. sum_upto (λ_. 1 :: real) (x / real n)) (sqrt x) -
(x * ln x / 2 + euler_mascheroni * x)) ∈
Θ(λx. x * (harm (nat ⌊sqrt x⌋) - (ln (nat ⌊sqrt x⌋) + euler_mascheroni)) - R x + x * S x)"
(is "_ ∈ Θ(?A)")
by (intro bigthetaI_cong) (elim eventually_mono, simp_all add: algebra_simps S_def)
also have "?A ∈ O(sqrt)"
proof (intro sum_in_bigo)
have "(λx. - S x) ∈ Θ(λx. ln (sqrt x) - ln (of_int ⌊sqrt x⌋))"
by (intro bigthetaI_cong eventually_mono [OF eventually_ge_at_top[of "1::real"]])
(auto simp: S_def ln_sqrt)
also have "(λx. ln (sqrt x) - ln (of_int ⌊sqrt x⌋)) ∈ O(λx. 1 / sqrt x)"
by (rule landau_o.big.compose[OF ln_minus_ln_floor_bigo sqrt_at_top])
finally have "(λx. x * S x) ∈ O(λx. x * (1 / sqrt x))" by (intro landau_o.big.mult) simp_all
also have "(λx::real. x * (1 / sqrt x)) ∈ Θ(λx. sqrt x)"
by (intro bigthetaI_cong eventually_mono [OF eventually_gt_at_top[of "0::real"]])
(auto simp: field_simps)
finally show "(λx. x * S x) ∈ O(sqrt)" .
next
let ?f = "λx::real. harm (nat ⌊sqrt x⌋) - (ln (real (nat ⌊sqrt x⌋)) + euler_mascheroni)"
have "?f ∈ O(λx. 1 / real (nat ⌊sqrt x⌋))"
proof (rule landau_o.big.compose[of _ _ _ "λx. nat ⌊sqrt x⌋"])
show "filterlim (λx::real. nat ⌊sqrt x⌋) at_top at_top"
by (intro filterlim_compose[OF filterlim_nat_sequentially]
filterlim_compose[OF filterlim_floor_sequentially] sqrt_at_top)
next
show "(λa. harm a - (ln (real a) + euler_mascheroni)) ∈ O(λa. 1 / real a)"
by (rule harm_expansion_bigo_simple2)
qed
also have "(λx. 1 / real (nat ⌊sqrt x⌋)) ∈ O(λx. 1 / (sqrt x - 1))"
proof (rule bigoI[of _ 1], use eventually_ge_at_top[of 2] in eventually_elim)
case (elim x)
have "sqrt x ≤ 1 + real_of_int ⌊sqrt x⌋" by linarith
with elim show ?case by (simp add: field_simps)
qed
also have "(λx::real. 1 / (sqrt x - 1)) ∈ O(λx. 1 / sqrt x)"
by (rule landau_o.big.compose[OF _ sqrt_at_top]) simp_all
finally have "(λx. x * ?f x) ∈ O(λx. x * (1 / sqrt x))"
by (intro landau_o.big.mult landau_o.big_refl)
also have "(λx::real. x * (1 / sqrt x)) ∈ Θ(λx. sqrt x)"
by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of "0::real"]])
(auto elim!: eventually_mono simp: field_simps)
finally show "(λx. x * ?f x) ∈ O(sqrt)" .
qed fact+
finally show ?thesis .
qed
lemma sum_upto_sqrt_bound:
assumes x: "x ≥ (0 :: real)"
shows "norm ((sum_upto (λ_. 1) (sqrt x))⇧2 - x) ≤ 2 * norm (sqrt x)"
proof -
from x have "0 ≤ 2 * sqrt x * (1 - frac (sqrt x)) + frac (sqrt x) ^ 2"
by (intro add_nonneg_nonneg mult_nonneg_nonneg) (simp_all add: frac_le_1)
also from x have "… = (sqrt x - frac (sqrt x)) ^ 2 - x + 2 * sqrt x"
by (simp add: algebra_simps power2_eq_square)
also have "sqrt x - frac (sqrt x) = of_int ⌊sqrt x⌋" by (simp add: frac_def)
finally have "(of_int ⌊sqrt x⌋) ^ 2 - x ≥ -2 * sqrt x" by (simp add: algebra_simps)
moreover from x have "of_int (⌊sqrt x⌋) ^ 2 ≤ sqrt x ^ 2"
by (intro power_mono) simp_all
with x have "of_int (⌊sqrt x⌋) ^ 2 - x ≤ 0" by simp
ultimately have "sum_upto (λ_. 1) (sqrt x) ^ 2 - x ∈ {-2 * sqrt x..0}"
using x by (simp add: sum_upto_altdef)
with x show ?thesis by simp
qed
lemma summatory_divisor_count_asymptotics:
"(λx. sum_upto (λn. real (divisor_count n)) x -
(x * ln x + (2 * euler_mascheroni - 1) * x)) ∈ O(sqrt)"
proof -
let ?f = "λx. x * ln x / 2 + euler_mascheroni * x"
have "(λx. sum_upto (dirichlet_prod (λ_. 1 :: real) (λ_. 1)) x - (?f x + ?f x - x)) ∈ O(sqrt)"
(is "?g ∈ _")
proof (rule hyperbola_method_bigo)
have "eventually (λx::real. norm (sum_upto (λ_. 1) (sqrt x) ^ 2 - x) ≤
2 * norm (sqrt x)) at_top"
using eventually_ge_at_top[of "0::real"] by eventually_elim (rule sum_upto_sqrt_bound)
thus "(λx::real. sum_upto (λ_. 1) (sqrt x) * sum_upto (λ_. 1) (sqrt x) - x) ∈ O(sqrt)"
by (intro bigoI[of _ 2]) (simp_all add: power2_eq_square)
next
show "(λx. sum_upto (λn. 1 * sum_upto (λ_. 1) (x / real n)) (sqrt x) -
(x * ln x / 2 + euler_mascheroni * x)) ∈ O(sqrt)"
using divisor_count_asymptotics_aux by simp
next
show "(λx. sum_upto (λn. sum_upto (λ_. 1) (x / real n) * 1) (sqrt x) -
(x * ln x / 2 + euler_mascheroni * x)) ∈ O(sqrt)"
using divisor_count_asymptotics_aux by simp
qed
also have "divisor_count n = dirichlet_prod (λ_. 1) (λ_. 1) n" for n
using fds_divisor_count
by (cases "n = 0") (simp_all add: fds_eq_iff power2_eq_square fds_nth_mult)
hence "?g = (λx. sum_upto (λn. real (divisor_count n)) x -
(x * ln x + (2 * euler_mascheroni - 1) * x))"
by (intro ext) (simp_all add: algebra_simps dirichlet_prod_def)
finally show ?thesis .
qed
theorem summatory_divisor_count_asymptotics':
"(λx. sum_upto (λn. real (divisor_count n)) x) =o
(λx. x * ln x + (2 * euler_mascheroni - 1) * x) +o O(λx. sqrt x)"
using summatory_divisor_count_asymptotics
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)
theorem summatory_divisor_count_asymptotics'':
"sum_upto (λn. real (divisor_count n)) ∼[at_top] (λx. x * ln x)"
proof -
have "(λx. sum_upto (λn. real (divisor_count n)) x -
(x * ln x + (2 * euler_mascheroni - 1) * x)) ∈ O(sqrt)"
by (rule summatory_divisor_count_asymptotics)
also have "sqrt ∈ Θ(λx. x powr (1/2))"
by (intro bigthetaI_cong eventually_mono [OF eventually_ge_at_top[of "0::real"]])
(auto elim!: eventually_mono simp: powr_half_sqrt)
also have "(λx::real. x powr (1/2)) ∈ o(λx. x * ln x + (2 * euler_mascheroni - 1) * x)" by simp
finally have "sum_upto (λn. real (divisor_count n)) ∼[at_top]
(λx. x * ln x + (2 * euler_mascheroni - 1) * x)"
by (simp add: asymp_equiv_altdef)
also have "… ∼[at_top] (λx. x * ln x)" by (subst asymp_equiv_add_right) simp_all
finally show ?thesis .
qed
lemma summatory_divisor_eq:
"sum_upto (λn. real (divisor_count n)) (real m) = card {(n,d). n ∈ {0<..m} ∧ d dvd n}"
proof -
have "sum_upto (λn. real (divisor_count n)) m = card (SIGMA n:{0<..m}. {d. d dvd n})"
unfolding sum_upto_altdef divisor_count_def by (subst card_SigmaI) simp_all
also have "(SIGMA n:{0<..m}. {d. d dvd n}) = {(n,d). n ∈ {0<..m} ∧ d dvd n}" by auto
finally show ?thesis .
qed
context
fixes M :: "nat ⇒ real"
defines "M ≡ λm. card {(n,d). n ∈ {0<..m} ∧ d dvd n} / card {0<..m}"
begin
lemma mean_divisor_count_asymptotics:
"(λm. M m - (ln m + 2 * euler_mascheroni - 1)) ∈ O(λm. 1 / sqrt m)"
proof -
have "(λm. M m - (ln m + 2 * euler_mascheroni - 1))
∈ Θ(λm. (sum_upto (λn. real (divisor_count n)) (real m) -
(m * ln m + (2 * euler_mascheroni - 1) * m)) / m)" (is "_ ∈ Θ(?f)")
unfolding M_def
by (intro bigthetaI_cong eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
(auto simp: summatory_divisor_eq field_simps)
also have "?f ∈ O(λm. sqrt m / m)"
by (intro landau_o.big.compose[OF _ filterlim_real_sequentially] landau_o.big.divide_right
summatory_divisor_count_asymptotics eventually_at_top_not_equal)
also have "(λm::nat. sqrt m / m) ∈ Θ(λm. 1 / sqrt m)"
by (intro bigthetaI_cong eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
(auto simp: field_simps)
finally show ?thesis .
qed
theorem mean_divisor_count_asymptotics':
"M =o (λx. ln x + 2 * euler_mascheroni - 1) +o O(λx. 1 / sqrt x)"
using mean_divisor_count_asymptotics
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)
theorem mean_divisor_count_asymptotics'': "M ∼[at_top] ln"
proof -
have "(λx. M x - (ln x + 2 * euler_mascheroni - 1)) ∈ O(λx. 1 / sqrt x)"
by (rule mean_divisor_count_asymptotics)
also have "(λx. 1 / sqrt (real x)) ∈ Θ(λx. x powr (-1/2))"
using eventually_gt_at_top[of "0::nat"]
by (intro bigthetaI_cong)
(auto elim!: eventually_mono simp: powr_half_sqrt field_simps powr_minus)
also have "(λx::nat. x powr (-1/2)) ∈ o(λx. ln x + 2 * euler_mascheroni - 1)"
by (intro smallo_real_nat_transfer) simp_all
finally have "M ∼[at_top] (λx. ln x + 2 * euler_mascheroni - 1)"
by (simp add: asymp_equiv_altdef)
also have "… = (λx::nat. ln x + (2 * euler_mascheroni - 1))" by (simp add: algebra_simps)
also have "… ∼[at_top] (λx::nat. ln x)" by (subst asymp_equiv_add_right) auto
finally show ?thesis .
qed
end
subsection ‹The asymptotic ditribution of coprime pairs›
context
fixes A :: "nat ⇒ (nat × nat) set"
defines "A ≡ (λN. {(m,n) ∈ {1..N} × {1..N}. coprime m n})"
begin
lemma coprime_pairs_asymptotics:
"(λN. real (card (A N)) - 6 / pi⇧2 * (real N)⇧2) ∈ O(λN. real N * ln (real N))"
proof -
define C :: "nat ⇒ (nat × nat) set"
where "C = (λN. (⋃m∈{1..N}. (λn. (m,n)) ` totatives m))"
define D :: "nat ⇒ (nat × nat) set"
where "D = (λN. (⋃n∈{1..N}. (λm. (m,n)) ` totatives n))"
have fin: "finite (C N)" "finite (D N)" for N unfolding C_def D_def
by (intro finite_UN_I finite_imageI; simp)+
have *: "card (A N) = 2 * (∑m∈{0<..N}. totient m) - 1" if N: "N > 0" for N
proof -
have "A N = C N ∪ D N"
by (auto simp add: A_def C_def D_def totatives_def image_iff ac_simps)
also have "card … = card (C N) + card (D N) - card (C N ∩ D N)"
using card_Un_Int[OF fin[of N]] by arith
also have "C N ∩ D N = {(1, 1)}" using N by (auto simp: image_iff totatives_def C_def D_def)
also have "D N = (λ(x,y). (y,x)) ` C N" by (simp add: image_UN image_image C_def D_def)
also have "card … = card (C N)" by (rule card_image) (simp add: inj_on_def C_def)
also have "card (C N) = (∑m∈{1..N}. card ((λn. (m,n)) ` totatives m))"
unfolding C_def by (intro card_UN_disjoint) auto
also have "… = (∑m∈{1..N}. totient m)" unfolding totient_def
by (subst card_image) (auto simp: inj_on_def)
also have "… = (∑m∈{0<..N}. totient m)" by (intro sum.cong refl) auto
finally show "card (A N) = 2 * … - 1" by simp
qed
have **: "(∑m∈{0<..N}. totient m) ≥ 1" if "N ≥ 1" for N
proof -
have "1 ≤ N" by fact
also have "N = (∑m∈{0<..N}. 1)" by simp
also have "(∑m∈{0<..N}. 1) ≤ (∑m∈{0<..N}. totient m)"
by (intro sum_mono) (simp_all add: Suc_le_eq)
finally show ?thesis .
qed
have "(λN. real (card (A N)) - 6 / pi⇧2 * (real N)⇧2) ∈
Θ(λN. 2 * (sum_upto (λm. real (totient m)) (real N) - (3 / pi⇧2 * (real N)⇧2)) - 1)"
(is "_ ∈ Θ(?f)") using * **
by (intro bigthetaI_cong eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
(auto simp: of_nat_diff sum_upto_altdef)
also have "?f ∈ O(λN. real N * ln (real N))"
proof (rule landau_o.big.compose[OF _ filterlim_real_sequentially], rule sum_in_bigo)
show " (λx. 2 * (sum_upto (λm. real (totient m)) x - 3 / pi⇧2 * x⇧2)) ∈ O(λx. x * ln x)"
by (subst landau_o.big.cmult_in_iff, simp, rule summatory_totient_asymptotics)
qed simp_all
finally show ?thesis .
qed
theorem coprime_pairs_asymptotics':
"(λN. real (card (A N))) =o (λN. 6 / pi⇧2 * (real N)⇧2) +o O(λN. real N * ln (real N))"
using coprime_pairs_asymptotics
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)
theorem coprime_pairs_asymptotics'':
"(λN. real (card (A N))) ∼[at_top] (λN. 6 / pi⇧2 * (real N)⇧2)"
proof -
have "(λN. real (card (A N)) - 6 / pi⇧2 * (real N) ^ 2) ∈ O(λN. real N * ln (real N))"
by (rule coprime_pairs_asymptotics)
also have "(λN. real N * ln (real N)) ∈ o(λN. 6 / pi ^ 2 * real N ^ 2)"
by (rule landau_o.small.compose[OF _ filterlim_real_sequentially]) simp
finally show ?thesis by (simp add: asymp_equiv_altdef)
qed
theorem coprime_probability_tendsto:
"(λN. card (A N) / card ({1..N} × {1..N})) ⇢ 6 / pi⇧2"
proof -
have "(λN. 6 / pi ^ 2) ∼[at_top] (λN. 6 / pi ^ 2 * real N ^ 2 / real N ^ 2)"
using eventually_gt_at_top[of "0::nat"]
by (intro asymp_equiv_refl_ev) (auto elim!: eventually_mono)
also have "… ∼[at_top] (λN. real (card (A N)) / real N ^ 2)"
by (intro asymp_equiv_intros asymp_equiv_symI[OF coprime_pairs_asymptotics''])
also have "… ∼[at_top] (λN. real (card (A N)) / real (card ({1..N} × {1..N})))"
by (simp add: power2_eq_square)
finally have "… ∼[at_top] (λ_. 6 / pi ^ 2)" by (simp add: asymp_equiv_sym)
thus ?thesis by (rule asymp_equivD_const)
qed
end
subsection ‹The asymptotics of the number of Farey fractions›
definition farey_fractions :: "nat ⇒ rat set" where
"farey_fractions N = {q :: rat ∈ {0<..1}. snd (quotient_of q) ≤ int N} "
lemma Fract_eq_coprime:
assumes "Rat.Fract a b = Rat.Fract c d" "b > 0" "d > 0" "coprime a b" "coprime c d"
shows "a = c" "b = d"
proof -
from assms have "a * d = c * b" by (auto simp: eq_rat)
hence "abs (a * d) = abs (c * b)" by (simp only:)
hence "abs a * abs d = abs c * abs b" by (simp only: abs_mult)
also have "?this ⟷ abs a = abs c ∧ d = b"
using assms by (subst coprime_crossproduct_int) simp_all
finally show "b = d" by simp
with ‹a * d = c * b› and ‹b > 0› show "a = c" by simp
qed
lemma quotient_of_split:
"P (quotient_of q) = (∀a b. b > 0 ⟶ coprime a b ⟶ q = Rat.Fract a b ⟶ P (a, b))"
by (cases q) (auto simp: quotient_of_Fract dest: Fract_eq_coprime)
lemma quotient_of_split_asm:
"P (Rat.quotient_of q) = (¬(∃a b. b > 0 ∧ coprime a b ∧ q = Rat.Fract a b ∧ ¬P (a, b)))"
using quotient_of_split[of P q] by blast
lemma farey_fractions_bij:
"bij_betw (λ(a,b). Rat.Fract (int a) (int b))
{(a,b)|a b. 0 < a ∧ a ≤ b ∧ b ≤ N ∧ coprime a b} (farey_fractions N)"
proof (rule bij_betwI[of _ _ _ "λq. case quotient_of q of (a, b) ⇒ (nat a, nat b)"], goal_cases)
case 1
show ?case
by (auto simp: farey_fractions_def Rat.zero_less_Fract_iff Rat.Fract_le_one_iff
Rat.quotient_of_Fract Rat.normalize_def gcd_int_def Let_def)
next
case 2
show ?case
by (auto simp add: farey_fractions_def Rat.Fract_le_one_iff Rat.zero_less_Fract_iff split: prod.splits quotient_of_split_asm)
(simp add: coprime_int_iff [symmetric])
next
case (3 x)
thus ?case by (auto simp: Rat.quotient_of_Fract Rat.normalize_def Let_def gcd_int_def)
next
case (4 x)
thus ?case unfolding farey_fractions_def
by (split quotient_of_split) (auto simp: Rat.zero_less_Fract_iff)
qed
lemma card_farey_fractions: "card (farey_fractions N) = sum totient {0<..N}"
proof -
have "card (farey_fractions N) = card {(a,b)|a b. 0 < a ∧ a ≤ b ∧ b ≤ N ∧ coprime a b}"
using farey_fractions_bij by (rule bij_betw_same_card [symmetric])
also have "{(a,b)|a b. 0 < a ∧ a ≤ b ∧ b ≤ N ∧ coprime a b} =
(⋃b∈{0<..N}. (λa. (a, b)) ` totatives b)"
by (auto simp: totatives_def image_iff)
also have "card … = (∑b∈{0<..N}. card ((λa. (a, b)) ` totatives b))"
by (intro card_UN_disjoint) auto
also have "… = (∑b∈{0<..N}. totient b)"
unfolding totient_def by (intro sum.cong refl card_image) (auto simp: inj_on_def)
finally show ?thesis .
qed
lemma card_farey_fractions_asymptotics:
"(λN. real (card (farey_fractions N)) - 3 / pi⇧2 * (real N)⇧2) ∈ O(λN. real N * ln (real N))"
proof -
have "(λN. sum_upto (λn. real (totient n)) (real N) - 3 / pi⇧2 * (real N)⇧2)
∈ O(λN. real N * ln (real N))" (is "?f ∈ _")
using summatory_totient_asymptotics filterlim_real_sequentially
by (rule landau_o.big.compose)
also have "?f = (λN. real (card (farey_fractions N)) - 3 / pi⇧2 * (real N)⇧2)"
by (intro ext) (simp add: sum_upto_altdef card_farey_fractions)
finally show ?thesis .
qed
theorem card_farey_fractions_asymptotics':
"(λN. card (farey_fractions N)) =o (λN. 3 / pi⇧2 * N^2) +o O(λN. N * ln N)"
using card_farey_fractions_asymptotics
by (subst set_minus_plus [symmetric]) (simp_all add: fun_diff_def)
theorem card_farey_fractions_asymptotics'':
"(λN. real (card (farey_fractions N))) ∼[at_top] (λN. 3 / pi⇧2 * (real N)⇧2)"
proof -
have "(λN. real (card (farey_fractions N)) - 3 / pi⇧2 * (real N) ^ 2) ∈ O(λN. real N * ln (real N))"
by (rule card_farey_fractions_asymptotics)
also have "(λN. real N * ln (real N)) ∈ o(λN. 3 / pi ^ 2 * real N ^ 2)"
by (rule landau_o.small.compose[OF _ filterlim_real_sequentially]) simp
finally show ?thesis by (simp add: asymp_equiv_altdef)
qed
end