# Theory More_Totient

theory More_Totient
imports Moebius_Mu

section
theory More_Totient
imports
Moebius_Mu

begin

lemma fds_totient_times_zeta:

proof
fix n :: nat assume n:
have
by (simp add: fds_nth_mult)
also from n have
by (simp add: fds_nth_fds dirichlet_prod_def totient_divisor_sum of_nat_sum [symmetric]
del: of_nat_sum)
finally show  .
qed

lemma fds_totient_times_zeta':
using fds_totient_times_zeta[where 'a = nat] by simp

lemma fds_totient:
proof -
have
by (simp add: fds_totient_times_zeta)
also have
by (simp only: mult.assoc fds_zeta_times_moebius_mu mult_1_right)
finally show ?thesis .
qed

lemma totient_conv_moebius_mu:

proof (cases )
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  by standard simp_all
hence
by (intro multiplicative_dirichlet_prod moebius_mu.multiplicative_function_axioms)
also have
by (simp add: fun_eq_iff totient_conv_moebius_mu)
finally show  by (rule multiplicative_function_of_natD)
qed

lemma even_prime_nat:
using prime_odd_nat[of p] prime_gt_1_nat[of p] by (cases ) auto

lemma twopow_dvd_totient:
fixes n :: nat
assumes
defines
shows
proof -
define P where
define P' where
define r where
from  have
unfolding r_def by (rule totient.prod_prime_factors)
also have
by (auto simp: P_def P'_def)
also have
by (subst prod.union_disjoint) (auto simp: P_def P'_def)
finally have eq:  .

have  if  for p
proof -
have  using that by (auto simp: P_def)
moreover have  using prime_gt_1_nat[of p] that by (auto simp: P_def)
ultimately have  by linarith
also have  by simp
also have
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
by (intro prod_dvd_prod totient_even)
hence
by simp
also have
by simp
also have
by (rule eq [symmetric])
finally show ?thesis unfolding k_def P_def .
qed

lemma totient_conv_moebius_mu':
assumes
shows
proof -
have  by simp
also have
using totient_conv_moebius_mu by (simp add: dirichlet_prod_def assms)
also have  by simp
also have
by (rule sum.cong) (simp_all add: field_char_0_class.of_nat_div)
also have
by (simp add: sum_distrib_left)
finally show ?thesis .
qed

lemma totient_prime_power_Suc:
assumes
shows
proof -
have
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
by (subst card_image) (auto simp: inj_on_def)
finally show ?thesis .
qed

interpretation totient: multiplicative_function' totient
proof
fix p k :: nat assume
thus
by (cases k) (simp_all add: totient_prime_power_Suc del: power_Suc)
qed simp_all

end