Theory Dirichlet_Series.More_Totient
section ‹Euler's $\phi$ function›
theory More_Totient
imports
Moebius_Mu
"HOL-Number_Theory.Number_Theory"
begin
lemma fds_totient_times_zeta:
"fds (λn. of_nat (totient n) :: 'a :: comm_semiring_1) * fds_zeta = fds of_nat"
proof
fix n :: nat assume n: "n > 0"
have "fds_nth (fds (λn. of_nat (totient n)) * fds_zeta) n =
dirichlet_prod (λn. of_nat (totient n)) (λ_. 1) n"
by (simp add: fds_nth_mult)
also from n have "… = fds_nth (fds of_nat) n"
by (simp add: fds_nth_fds dirichlet_prod_def totient_divisor_sum of_nat_sum [symmetric]
del: of_nat_sum)
finally show "fds_nth (fds (λn. of_nat (totient n)) * fds_zeta) n = fds_nth (fds of_nat) n" .
qed
lemma fds_totient_times_zeta': "fds totient * fds_zeta = fds id"
using fds_totient_times_zeta[where 'a = nat] by simp
lemma fds_totient: "fds (λn. of_nat (totient n)) = fds of_nat * fds moebius_mu"
proof -
have "fds (λn. of_nat (totient n)) * fds_zeta * fds moebius_mu = fds of_nat * fds moebius_mu"
by (simp add: fds_totient_times_zeta)
also have "fds (λn. of_nat (totient n)) * fds_zeta * fds moebius_mu =
fds (λn. of_nat (totient n))"
by (simp only: mult.assoc fds_zeta_times_moebius_mu mult_1_right)
finally show ?thesis .
qed
lemma totient_conv_moebius_mu:
"int (totient n) = dirichlet_prod moebius_mu int n"
proof (cases "n = 0")
case False
show ?thesis
by (rule moebius_inversion)
(insert False, simp_all add: of_nat_sum [symmetric] totient_divisor_sum del: of_nat_sum)
qed simp_all
interpretation totient: multiplicative_function totient
proof -
have "multiplicative_function int" by standard simp_all
hence "multiplicative_function (dirichlet_prod moebius_mu int)"
by (intro multiplicative_dirichlet_prod moebius_mu.multiplicative_function_axioms)
also have "dirichlet_prod moebius_mu int = (λn. int (totient n))"
by (simp add: fun_eq_iff totient_conv_moebius_mu)
finally show "multiplicative_function totient" by (rule multiplicative_function_of_natD)
qed
lemma even_prime_nat: "prime p ⟹ even p ⟹ p = (2::nat)"
using prime_odd_nat[of p] prime_gt_1_nat[of p] by (cases "p = 2") auto
lemma twopow_dvd_totient:
fixes n :: nat
assumes "n > 0"
defines "k ≡ card {p∈prime_factors n. odd p}"
shows "2 ^ k dvd totient n"
proof -
define P where "P = {p∈prime_factors n. odd p}"
define P' where "P' = {p∈prime_factors n. even p}"
define r where "r = (λp. multiplicity p n)"
from ‹n > 0› have "totient n = (∏p∈prime_factors n. totient (p ^ r p))"
unfolding r_def by (rule totient.prod_prime_factors)
also have "prime_factors n = P ∪ P'"
by (auto simp: P_def P'_def)
also have "(∏p∈…. totient (p ^ r p)) =
(∏p∈P. totient (p ^ r p)) * (∏p∈P'. totient (p ^ r p))"
by (subst prod.union_disjoint) (auto simp: P_def P'_def)
finally have eq: "totient n = …" .
have "p ^ r p > 2" if "p ∈ P" for p
proof -
have "p ≠ 2" using that by (auto simp: P_def)
moreover have "p > 1" using prime_gt_1_nat[of p] that by (auto simp: P_def)
ultimately have "2 < p" by linarith
also have "p = p ^ 1" by simp
also have "p ^ 1 ≤ p ^ r p"
using that prime_gt_1_nat[of p]
by (intro power_increasing) (auto simp: P_def prime_factors_multiplicity r_def)
finally show ?thesis .
qed
hence "(∏p∈P. 2) dvd (∏p∈P. totient (p ^ r p))"
by (intro prod_dvd_prod totient_even)
hence "2 ^ card P dvd (∏p∈P. totient (p ^ r p))"
by simp
also have "… dvd (∏p∈P. totient (p ^ r p)) * (∏p∈P'. totient (p ^ r p))"
by simp
also have "… = totient n"
by (rule eq [symmetric])
finally show ?thesis unfolding k_def P_def .
qed
lemma totient_conv_moebius_mu':
assumes "n > (0::nat)"
shows "real (totient n) = real n * (∑d | d dvd n. moebius_mu d / real d)"
proof -
have "real (totient n) = of_int (int (totient n))" by simp
also have "int (totient n) = (∑d | d dvd n. moebius_mu d * int (n div d))"
using totient_conv_moebius_mu by (simp add: dirichlet_prod_def assms)
also have "real_of_int (∑d | d dvd n. moebius_mu d * int (n div d)) =
(∑d | d dvd n. moebius_mu d * real (n div d))" by simp
also have "… = (∑d | d dvd n. real n * moebius_mu d / real d)"
by (rule sum.cong) (simp_all add: field_char_0_class.of_nat_div)
also have "… = real n * (∑d | d dvd n. moebius_mu d / real d)"
by (simp add: sum_distrib_left)
finally show ?thesis .
qed
lemma totient_prime_power_Suc:
assumes "prime p"
shows "totient (p ^ Suc n) = p ^ Suc n - p ^ n"
proof -
have "totient (p ^ Suc n) = p ^ Suc n - card ((*) p ` {0<..p ^ n})"
unfolding totient_def totatives_prime_power_Suc[OF assms]
by (subst card_Diff_subset) (insert assms, auto simp: prime_gt_0_nat)
also from assms have "card ((*) p ` {0<..p^n}) = p ^ n"
by (subst card_image) (auto simp: inj_on_def)
finally show ?thesis .
qed
interpretation totient: multiplicative_function' totient "λp k. p ^ k - p ^ (k - 1)" "λp. p - 1"
proof
fix p k :: nat assume "prime p" "k > 0"
thus "totient (p ^ k) = p ^ k - p ^ (k - 1)"
by (cases k) (simp_all add: totient_prime_power_Suc del: power_Suc)
qed simp_all
end