Theory Number_Theoretic_Functions_Extras
section ‹Some Facts About Number-Theoretic Functions›
theory Number_Theoretic_Functions_Extras
imports
"Dirichlet_Series.Dirichlet_Series_Analysis"
"Dirichlet_Series.Divisor_Count"
Lambert_Series_Library
begin
lemma (in nat_power_field) :
"a ≠ 0 ∨ n ≠ 0 ⟹ nat_power n (-a) = inverse (nat_power n a)"
using nat_power_diff[of n 0 a] by (cases "n = 0") (simp_all add: field_simps)
lemma :
fixes a :: "'a :: {nat_power_field, field_char_0}"
shows "divisor_sigma (-a) n = divisor_sigma a n / nat_power n a"
proof (cases "n = 0")
case n: False
have "divisor_sigma (-a :: 'a) n = (∑d | d dvd n. nat_power d (-a))"
by (simp add: divisor_sigma_def)
also have "… = (∑d | d dvd n. nat_power d a / nat_power n a)"
using n by (intro sum.reindex_bij_witness[of _ "λd. n div d" "λd. n div d"])
(auto elim!: dvdE simp: field_simps nat_power_minus nat_power_mult_distrib)
also have "… = divisor_sigma a n / nat_power n a"
by (simp add: sum_divide_distrib divisor_sigma_def)
finally show ?thesis .
qed auto
lemma :
"norm (moebius_mu n ::'a :: {real_normed_algebra_1, comm_ring_1}) = ind squarefree n"
by (subst of_int_moebius_mu [symmetric], subst norm_of_int) (auto simp: abs_moebius_mu)
lemma : "conv_radius (λn. nat_power n a :: 'a :: {nat_power_normed_field, banach}) = 1"
proof (rule tendsto_imp_conv_radius_eq)
show "(λn. ereal (norm (nat_power n a :: 'a) powr (1 / real n))) ⇢ ereal 1"
proof (rule Lim_transform_eventually)
show "(λn. ereal ((real n powr (a ∙ 1)) powr (1 / real n))) ⇢ ereal 1"
by (rule tendsto_ereal) real_asymp
show "eventually (λn. (real n powr (a ∙ 1)) powr (1 / real n) =
ereal (norm (nat_power n a :: 'a) powr (1 / real n))) at_top"
using eventually_gt_at_top[of 0] by eventually_elim (simp add: norm_nat_power)
qed
qed (simp_all add: one_ereal_def)
lemma :
"¬convergent (liouville_lambda :: nat ⇒ 'a :: {real_normed_algebra, comm_ring_1, semiring_char_0})"
proof -
have "¬(liouville_lambda :: nat ⇒ 'a) ⇢ c" for c
proof (rule oscillation_imp_not_tendsto)
show "eventually (λn. liouville_lambda (2 ^ (2 * n)) ∈ {1 :: 'a}) sequentially"
by auto
show "filterlim (λn. 2 ^ (2 * n) :: nat) at_top sequentially"
by real_asymp
show "eventually (λn. liouville_lambda (2 ^ (2 * n + 1)) ∈ {-1 :: 'a}) sequentially"
by (subst liouville_lambda.power) auto
show "filterlim (λn. 2 ^ (2 * n + 1) :: nat) at_top sequentially"
by real_asymp
qed auto
thus ?thesis
by (auto simp: convergent_def)
qed
lemma :
"conv_radius (liouville_lambda :: nat ⇒ 'a :: {real_normed_field, banach}) = 1"
proof -
have "¬summable (liouville_lambda :: nat ⇒ 'a)"
using not_convergent_liouville_lambda[where ?'a = 'a] summable_LIMSEQ_zero
by (auto simp: convergent_def)
hence "conv_radius (liouville_lambda :: nat ⇒ 'a) ≤ norm (1 :: 'a)"
by (intro conv_radius_leI') auto
moreover have "conv_radius (liouville_lambda :: nat ⇒ 'a) ≥ 1"
proof (rule conv_radius_bigo_polynomial)
show "(liouville_lambda :: nat ⇒ 'a) ∈ O(λn. of_nat n ^ 0)"
by (intro bigoI[of _ 1] eventually_mono[OF eventually_gt_at_top[of 0]])
(auto simp: liouville_lambda_def norm_power)
qed
ultimately show ?thesis
by (intro antisym) (auto simp: one_ereal_def)
qed
lemma : "¬convergent (mangoldt :: nat ⇒ 'a :: {real_normed_algebra_1})"
proof -
have *: "¬primepow (6 * n :: nat)" for n
by (rule not_primepowI[of 2 3]) auto
have "¬(mangoldt :: nat ⇒ 'a) ⇢ c" for c
proof (rule oscillation_imp_not_tendsto)
show "eventually (λn. mangoldt (2 ^ n) ∈ {of_real (ln 2) :: 'a}) sequentially"
by (auto simp: mangoldt_primepow)
show "filterlim (λn. 2 ^ n :: nat) at_top sequentially"
by real_asymp
show "eventually (λn. mangoldt (6 * n) ∈ {0 :: 'a}) sequentially"
using * by (auto simp: mangoldt_def)
show "filterlim (λn. 6 * n :: nat) at_top sequentially"
by real_asymp
qed auto
thus ?thesis
by (auto simp: convergent_def)
qed
lemma :
"conv_radius (mangoldt :: nat ⇒ 'a :: {real_normed_field, banach}) = 1"
proof -
have "¬summable (mangoldt :: nat ⇒ 'a)"
using not_convergent_mangoldt[where ?'a = 'a] summable_LIMSEQ_zero
by (auto simp: convergent_def)
hence "conv_radius (mangoldt :: nat ⇒ 'a) ≤ norm (1 :: 'a)"
by (intro conv_radius_leI') auto
moreover have "conv_radius (mangoldt :: nat ⇒ 'a) ≥ 1"
proof (rule conv_radius_bigo_polynomial)
have "(mangoldt :: nat ⇒ 'a) ∈ O(λn. of_real (ln (real n)))"
by (intro bigoI[of _ 1] eventually_mono[OF eventually_gt_at_top[of 0]])
(auto simp: mangoldt_le)
also have "(λn. of_real (ln (real n))) ∈ O(λn. of_nat n :: 'a)"
by (subst landau_o.big.norm_iff [symmetric], unfold norm_of_real norm_of_nat) real_asymp
finally show "(mangoldt :: nat ⇒ 'a) ∈ O(λn. of_nat n ^ 1)"
by simp
qed
ultimately show ?thesis
by (intro antisym) (auto simp: one_ereal_def)
qed
lemma : "¬convergent (moebius_mu :: nat ⇒ 'a :: real_normed_field)"
proof (rule oscillation_imp_not_convergent)
have "infinite {p. prime (p :: nat)}"
by (rule primes_infinite)
hence "frequently (prime :: nat ⇒ bool) cofinite"
by (simp add: Inf_many_def)
hence "frequently (λn. moebius_mu n = (-1 :: 'a)) cofinite"
by (rule frequently_elim1) (simp add: moebius_mu.prime)
thus "frequently (λn. moebius_mu n ∈ {(-1 :: 'a)}) sequentially"
using cofinite_eq_sequentially by fastforce
next
have "infinite (range (λn. 4 * n :: nat))"
by (subst finite_image_iff) (auto simp: inj_on_def)
moreover {
have "¬squarefree (2 ^ 2 :: nat)"
by (subst squarefree_power_iff) auto
also have "2 ^ 2 = (4 :: nat)"
by simp
finally have "range (λn. 4 * n :: nat) ⊆ {n::nat. ¬squarefree n}"
by (auto dest: squarefree_multD)
}
ultimately have "frequently (λn::nat. ¬squarefree n) cofinite"
unfolding INFM_iff_infinite using finite_subset by blast
thus "∃⇩F n in sequentially. moebius_mu n ∈ {0}"
unfolding cofinite_eq_sequentially by (rule frequently_elim1) auto
qed auto
lemma :
"conv_radius (moebius_mu :: nat ⇒ 'a :: {real_normed_field, banach}) = 1"
proof -
have "¬summable (moebius_mu :: nat ⇒ 'a)"
using not_convergent_moebius_mu[where ?'a = 'a] summable_LIMSEQ_zero
by (auto simp: convergent_def)
hence "conv_radius (moebius_mu :: nat ⇒ 'a) ≤ norm (1 :: 'a)"
by (intro conv_radius_leI') auto
moreover have "conv_radius (moebius_mu :: nat ⇒ 'a) ≥ conv_radius (λ_. 1 :: 'a)"
by (intro conv_radius_mono always_eventually) (auto simp: norm_moebius_mu ind_def)
ultimately show ?thesis
by (intro antisym) (auto simp: one_ereal_def)
qed
lemma :
"¬convergent (λn. of_nat (totient n) :: 'a :: {real_normed_field, banach})"
proof
assume "convergent (λn. of_nat (totient n) :: 'a)"
then obtain L where L: "eventually (λn. totient n = L) at_top"
by (auto simp: convergent_def filterlim_of_nat_iff)
then obtain N where N: "⋀n. n ≥ N ⟹ totient n = L"
unfolding eventually_at_top_linorder by blast
obtain p q where "prime p" "p > N" "prime q" "q > p"
using bigger_prime by blast
with N[of p] N[of q] show False
by (auto simp: totient_prime)
qed
lemma :
"conv_radius (λn. of_nat (totient n) :: 'a :: {real_normed_field, banach}) = 1"
proof -
have "¬summable (λn. of_nat (totient n) :: 'a)"
using not_convergent_totient[where ?'a = 'a] summable_LIMSEQ_zero
by (auto simp: convergent_def)
hence "conv_radius (λn. of_nat (totient n) :: 'a) ≤ norm (1 :: 'a)"
by (intro conv_radius_leI') auto
moreover have "conv_radius (λn. of_nat (totient n) :: 'a) ≥ 1"
proof (rule conv_radius_bigo_polynomial)
show "(λn. of_nat (totient n)) ∈ O(λn. of_nat n ^ 1)"
by (intro bigoI[of _ 1] always_eventually) (auto simp: totient_le)
qed
ultimately show ?thesis
by (intro antisym) (auto simp: one_ereal_def)
qed
end