Theory HOL-Number_Theory.Prime_Powers

(*
  File:      HOL/Number_Theory/Prime_Powers.thy
  Author:    Manuel Eberl <manuel@pruvisto.org>

  Prime powers and the Mangoldt function
*)
section ‹Prime powers›
theory Prime_Powers
  imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet"
begin

definition aprimedivisor :: "'a :: normalization_semidom ⇒ 'a" where
  "aprimedivisor q = (SOME p. prime p ∧ p dvd q)"

definition primepow :: "'a :: normalization_semidom ⇒ bool" where
  "primepow n ⟷ (∃p k. prime p ∧ k > 0 ∧ n = p ^ k)"

definition primepow_factors :: "'a :: normalization_semidom ⇒ 'a set" where
  "primepow_factors n = {x. primepow x ∧ x dvd n}"
  
lemma primepow_gt_Suc_0: "primepow n ⟹ n > Suc 0"
  using one_less_power[of "p::nat" for p] by (auto simp: primepow_def prime_nat_iff)

lemma
  assumes "prime p" "p dvd n"
  shows prime_aprimedivisor: "prime (aprimedivisor n)" 
    and aprimedivisor_dvd:   "aprimedivisor n dvd n"
proof -
  from assms have "∃p. prime p ∧ p dvd n" by auto
  from someI_ex[OF this] show "prime (aprimedivisor n)" "aprimedivisor n dvd n"
      unfolding aprimedivisor_def by (simp_all add: conj_commute)
qed    

lemma
  assumes "n ≠ 0" "¬is_unit (n :: 'a :: factorial_semiring)"
  shows prime_aprimedivisor': "prime (aprimedivisor n)" 
    and aprimedivisor_dvd':   "aprimedivisor n dvd n"
proof -
  from someI_ex[OF prime_divisor_exists[OF assms]] 
    show "prime (aprimedivisor n)" "aprimedivisor n dvd n"
      unfolding aprimedivisor_def by (simp_all add: conj_commute)
qed

lemma aprimedivisor_of_prime [simp]: 
  assumes "prime p"
  shows   "aprimedivisor p = p"
proof -
  from assms have "∃q. prime q ∧ q dvd p" by auto
  from someI_ex[OF this, folded aprimedivisor_def] assms show ?thesis
    by (auto intro: primes_dvd_imp_eq)
qed

lemma aprimedivisor_pos_nat: "(n::nat) > 1 ⟹ aprimedivisor n > 0"
  using aprimedivisor_dvd'[of n] by (auto elim: dvdE intro!: Nat.gr0I)

lemma aprimedivisor_primepow_power:
  assumes "primepow n" "k > 0"
  shows   "aprimedivisor (n ^ k) = aprimedivisor n"
proof -
  from assms obtain p l where l: "prime p" "l > 0" "n = p ^ l"
    by (auto simp: primepow_def)
  from l assms have *: "prime (aprimedivisor (n ^ k))" "aprimedivisor (n ^ k) dvd n ^ k"
    by (intro prime_aprimedivisor[of p] aprimedivisor_dvd[of p] dvd_power; 
        simp add: power_mult [symmetric])+
  from * l have "aprimedivisor (n ^ k) dvd p ^ (l * k)" by (simp add: power_mult)
  with assms * l have "aprimedivisor (n ^ k) dvd p" 
    by (subst (asm) prime_dvd_power_iff) simp_all
  with l assms have "aprimedivisor (n ^ k) = p"
    by (intro primes_dvd_imp_eq prime_aprimedivisor l) (auto simp: power_mult [symmetric])
  moreover from l have "aprimedivisor n dvd p ^ l" 
    by (auto intro: aprimedivisor_dvd simp: prime_gt_0_nat)
  with assms l have "aprimedivisor n dvd p"
    by (subst (asm) prime_dvd_power_iff) (auto intro!: prime_aprimedivisor simp: prime_gt_0_nat)
  with l assms have "aprimedivisor n = p"
    by (intro primes_dvd_imp_eq prime_aprimedivisor l) auto
  ultimately show ?thesis by simp
qed

lemma aprimedivisor_prime_power:
  assumes "prime p" "k > 0"
  shows   "aprimedivisor (p ^ k) = p"
proof -
  from assms have *: "prime (aprimedivisor (p ^ k))" "aprimedivisor (p ^ k) dvd p ^ k"
    by (intro prime_aprimedivisor[of p] aprimedivisor_dvd[of p]; simp add: prime_nat_iff)+
  from assms * have "aprimedivisor (p ^ k) dvd p" 
    by (subst (asm) prime_dvd_power_iff) simp_all
  with assms * show "aprimedivisor (p ^ k) = p" by (intro primes_dvd_imp_eq)
qed

lemma prime_factorization_primepow:
  assumes "primepow n"
  shows   "prime_factorization n = 
             replicate_mset (multiplicity (aprimedivisor n) n) (aprimedivisor n)"
  using assms
  by (auto simp: primepow_def aprimedivisor_prime_power prime_factorization_prime_power)

lemma primepow_decompose:
  fixes n :: "'a :: factorial_semiring_multiplicative"
  assumes "primepow n"
  shows   "aprimedivisor n ^ multiplicity (aprimedivisor n) n = n"
proof -
  from assms have "n ≠ 0" by (intro notI) (auto simp: primepow_def)
  hence "n = unit_factor n * prod_mset (prime_factorization n)"
    by (subst prod_mset_prime_factorization) simp_all
  also from assms have "unit_factor n = 1" by (auto simp: primepow_def unit_factor_power)
  also have "prime_factorization n = 
               replicate_mset (multiplicity (aprimedivisor n) n) (aprimedivisor n)"
    by (intro prime_factorization_primepow assms)
  also have "prod_mset … = aprimedivisor n ^ multiplicity (aprimedivisor n) n" by simp
  finally show ?thesis by simp
qed

lemma prime_power_not_one:
  assumes "prime p" "k > 0"
  shows   "p ^ k ≠ 1"
proof
  assume "p ^ k = 1"
  hence "is_unit (p ^ k)" by simp
  thus False using assms by (simp add: is_unit_power_iff)
qed

lemma zero_not_primepow [simp]: "¬primepow 0"
  by (auto simp: primepow_def)

lemma one_not_primepow [simp]: "¬primepow 1"
  by (auto simp: primepow_def prime_power_not_one)

lemma primepow_not_unit [simp]: "primepow p ⟹ ¬is_unit p"
  by (auto simp: primepow_def is_unit_power_iff)

lemma not_primepow_Suc_0_nat [simp]: "¬primepow (Suc 0)"
  using primepow_gt_Suc_0[of "Suc 0"] by auto

lemma primepow_gt_0_nat: "primepow n ⟹ n > (0::nat)"
  using primepow_gt_Suc_0[of n] by simp

lemma unit_factor_primepow:
  fixes p :: "'a :: factorial_semiring_multiplicative"
  shows "primepow p ⟹ unit_factor p = 1"
  by (auto simp: primepow_def unit_factor_power)

lemma aprimedivisor_primepow:
  assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring_multiplicative)"
  shows   "aprimedivisor (p * n) = p" "aprimedivisor n = p"
proof -
  from assms have [simp]: "n ≠ 0" by auto
  define q where "q = aprimedivisor n"
  with assms have q: "prime q" by (auto simp: q_def intro!: prime_aprimedivisor)
  from ‹primepow n› have n: "n = q ^ multiplicity q n" 
    by (simp add: primepow_decompose q_def)
  have nz: "multiplicity q n ≠ 0"
  proof
    assume "multiplicity q n = 0"
    with n have n': "n = unit_factor n" by simp
    have "is_unit n" by (subst n', rule unit_factor_is_unit) (insert assms, auto)
    with assms show False by auto
  qed
  with ‹prime p› ‹p dvd n› q have "p dvd q" 
    by (subst (asm) n) (auto intro: prime_dvd_power)
  with ‹prime p› q have "p = q" by (intro primes_dvd_imp_eq)
  thus "aprimedivisor n = p" by (simp add: q_def)

  define r where "r = aprimedivisor (p * n)"
  with assms have r: "r dvd (p * n)" "prime r" unfolding r_def
    by (intro aprimedivisor_dvd[of p] prime_aprimedivisor[of p]; simp)+
  hence "r dvd q ^ Suc (multiplicity q n)"
    by (subst (asm) n) (auto simp: ‹p = q› dest: dvd_unit_imp_unit)
  with r have "r dvd q" 
    by (auto intro: prime_dvd_power_nat simp: prime_dvd_mult_iff dest: prime_dvd_power)
  with r q have "r = q" by (intro primes_dvd_imp_eq)
  thus "aprimedivisor (p * n) = p" by (simp add: r_def ‹p = q›)
qed

lemma power_eq_prime_powerD:
  fixes p :: "'a :: factorial_semiring"
  assumes "prime p" "n > 0" "x ^ n = p ^ k"
  shows   "∃i. normalize x = normalize (p ^ i)"
proof -
  have "normalize x = normalize (p ^ multiplicity p x)"
  proof (rule multiplicity_eq_imp_eq)
    fix q :: 'a assume "prime q"
    from assms have "multiplicity q (x ^ n) = multiplicity q (p ^ k)" by simp
    with ‹prime q› and assms have "n * multiplicity q x = k * multiplicity q p"
      by (subst (asm) (1 2) prime_elem_multiplicity_power_distrib) (auto simp: power_0_left)
    with assms and ‹prime q› show "multiplicity q x = multiplicity q (p ^ multiplicity p x)"
      by (cases "p = q") (auto simp: multiplicity_distinct_prime_power prime_multiplicity_other)
  qed (insert assms, auto simp: power_0_left)
  thus ?thesis by auto
qed
  

lemma primepow_power_iff:
  fixes p :: "'a :: factorial_semiring_multiplicative"
  assumes "unit_factor p = 1"
  shows   "primepow (p ^ n) ⟷ primepow p ∧ n > 0"
proof safe
  assume "primepow (p ^ n)"
  hence n: "n ≠ 0" by (auto intro!: Nat.gr0I)
  thus "n > 0" by simp
  from assms have [simp]: "normalize p = p"
    using normalize_mult_unit_factor[of p] by (simp only: mult.right_neutral)
  from ‹primepow (p ^ n)› obtain q k where *: "k > 0" "prime q" "p ^ n = q ^ k"
    by (auto simp: primepow_def)
  with power_eq_prime_powerD[of q n p k] n 
    obtain i where eq: "normalize p = normalize (q ^ i)" by auto
  with primepow_not_unit[OF ‹primepow (p ^ n)›] have "i ≠ 0" 
    by (intro notI) (simp add: normalize_1_iff is_unit_power_iff del: primepow_not_unit)
  with ‹normalize p = normalize (q ^ i)› ‹prime q› show "primepow p"
    by (auto simp: normalize_power primepow_def intro!: exI[of _ q] exI[of _ i])
next
  assume "primepow p" "n > 0"
  then obtain q k where *: "k > 0" "prime q" "p = q ^ k" by (auto simp: primepow_def)
  with ‹n > 0› show "primepow (p ^ n)"
    by (auto simp: primepow_def power_mult intro!: exI[of _ q] exI[of _ "k * n"])
qed

lemma primepow_power_iff_nat:
  "p > 0 ⟹ primepow (p ^ n) ⟷ primepow (p :: nat) ∧ n > 0"
  by (rule primepow_power_iff) (simp_all add: unit_factor_nat_def)

lemma primepow_prime [simp]: "prime n ⟹ primepow n"
  by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"])

lemma primepow_prime_power [simp]: 
    "prime (p :: 'a :: factorial_semiring_multiplicative) ⟹ primepow (p ^ n) ⟷ n > 0"
  by (subst primepow_power_iff) auto

lemma aprimedivisor_vimage:
  assumes "prime (p :: 'a :: factorial_semiring_multiplicative)"
  shows   "aprimedivisor -` {p} ∩ primepow_factors n = {p ^ k |k. k > 0 ∧ p ^ k dvd n}"
proof safe
  fix q assume q: "q ∈ primepow_factors n"
  hence q': "q ≠ 0" "q ≠ 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one)
  let ?n = "multiplicity (aprimedivisor q) q"
  from q q' have "q = aprimedivisor q ^ ?n ∧ ?n > 0 ∧ aprimedivisor q ^ ?n dvd n"
    by (auto simp: primepow_decompose primepow_factors_def prime_multiplicity_gt_zero_iff
          prime_aprimedivisor' prime_imp_prime_elem aprimedivisor_dvd')
  thus "∃k. q = aprimedivisor q ^ k ∧ k > 0 ∧ aprimedivisor q ^ k dvd n" ..
next
  fix k :: nat assume k: "p ^ k dvd n" "k > 0"
  with assms show "p ^ k ∈ aprimedivisor -` {p}"
    by (auto simp: aprimedivisor_prime_power)
  with assms k show "p ^ k ∈ primepow_factors n"
    by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI)
qed

lemma aprimedivisor_nat:
  assumes "n ≠ (Suc 0::nat)"
  shows   "prime (aprimedivisor n)" "aprimedivisor n dvd n"
proof -
  from assms have "∃p. prime p ∧ p dvd n" by (intro prime_factor_nat) auto
  from someI_ex[OF this, folded aprimedivisor_def] 
    show "prime (aprimedivisor n)" "aprimedivisor n dvd n" by blast+
qed
  
lemma aprimedivisor_gt_Suc_0:
  assumes "n ≠ Suc 0"
  shows   "aprimedivisor n > Suc 0"
proof -
  from assms have "prime (aprimedivisor n)" by (rule aprimedivisor_nat)
  thus "aprimedivisor n > Suc 0" by (simp add: prime_nat_iff)
qed

lemma aprimedivisor_le_nat:
  assumes "n > Suc 0"
  shows   "aprimedivisor n ≤ n"
proof -
  from assms have "aprimedivisor n dvd n" by (intro aprimedivisor_nat) simp_all
  with assms show "aprimedivisor n ≤ n"
    by (intro dvd_imp_le) simp_all
qed

lemma bij_betw_primepows: 
  "bij_betw (λ(p,k). p ^ Suc k :: 'a :: factorial_semiring_multiplicative) 
     (Collect prime × UNIV) (Collect primepow)"
proof (rule bij_betwI [where ?g = "(λn. (aprimedivisor n, multiplicity (aprimedivisor n) n - 1))"], 
       goal_cases)
  case 1
  show "(λ(p, k). p ^ Suc k :: 'a) ∈ Collect prime × UNIV → Collect primepow"
    by (auto intro!: primepow_prime_power simp del: power_Suc )
next
  case 2
  show ?case
    by (auto simp: primepow_def prime_aprimedivisor)
next
  case (3 n)
  thus ?case
    by (auto simp: aprimedivisor_prime_power simp del: power_Suc)
next
  case (4 n)
  hence *: "0 < multiplicity (aprimedivisor n) n"
    by (subst prime_multiplicity_gt_zero_iff)
       (auto intro!: prime_imp_prime_elem aprimedivisor_dvd simp: primepow_def prime_aprimedivisor)
  have "aprimedivisor n * aprimedivisor n ^ (multiplicity (aprimedivisor n) n - Suc 0) =
          aprimedivisor n ^ Suc (multiplicity (aprimedivisor n) n - Suc 0)" by simp
  also from * have "Suc (multiplicity (aprimedivisor n) n - Suc 0) =
                      multiplicity (aprimedivisor n) n"
    by (subst Suc_diff_Suc) (auto simp: prime_multiplicity_gt_zero_iff)
  also have "aprimedivisor n ^ … = n"
    using 4 by (subst primepow_decompose) auto
  finally show ?case by auto
qed

(* TODO Generalise *)
lemma primepow_multD:
  assumes "primepow (a * b :: nat)"
  shows   "a = 1 ∨ primepow a" "b = 1 ∨ primepow b"
proof -
  from assms obtain p k where k: "k > 0" "a * b = p ^ k" "prime p"
    unfolding primepow_def by auto
  then obtain i j where "a = p ^ i" "b = p ^ j"
    using prime_power_mult_nat[of p a b] by blast
  with ‹prime p› show "a = 1 ∨ primepow a" "b = 1 ∨ primepow b" by auto
qed

lemma primepow_mult_aprimedivisorI:
  assumes "primepow (n :: 'a :: factorial_semiring_multiplicative)"
  shows   "primepow (aprimedivisor n * n)"
  by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric],
      subst primepow_prime_power) 
     (insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0)
 
lemma primepow_factors_altdef:
  fixes x :: "'a :: factorial_semiring_multiplicative"
  assumes "x ≠ 0"
  shows "primepow_factors x = {p ^ k |p k. p ∈ prime_factors x ∧ k ∈ {0<.. multiplicity p x}}"
proof (intro equalityI subsetI)
  fix q assume "q ∈ primepow_factors x"
  then obtain p k where pk: "prime p" "k > 0" "q = p ^ k" "q dvd x" 
    unfolding primepow_factors_def primepow_def by blast
  moreover have "k ≤ multiplicity p x" using pk assms by (intro multiplicity_geI) auto
  ultimately show "q ∈ {p ^ k |p k. p ∈ prime_factors x ∧ k ∈ {0<.. multiplicity p x}}"
    by (auto simp: prime_factors_multiplicity intro!: exI[of _ p] exI[of _ k])
qed (auto simp: primepow_factors_def prime_factors_multiplicity multiplicity_dvd')

lemma finite_primepow_factors:
  assumes "x ≠ (0 :: 'a :: factorial_semiring_multiplicative)"
  shows   "finite (primepow_factors x)"
proof -
  have "finite (SIGMA p:prime_factors x. {0<..multiplicity p x})"
    by (intro finite_SigmaI) simp_all
  hence "finite ((λ(p,k). p ^ k) ` …)" (is "finite ?A") by (rule finite_imageI)
  also have "?A = primepow_factors x"
    using assms by (subst primepow_factors_altdef) fast+
  finally show ?thesis .
qed

lemma aprimedivisor_primepow_factors_conv_prime_factorization:
  assumes [simp]: "n ≠ (0 :: 'a :: factorial_semiring_multiplicative)"
  shows   "image_mset aprimedivisor (mset_set (primepow_factors n)) = prime_factorization n" 
          (is "?lhs = ?rhs")
proof (intro multiset_eqI)
  fix p :: 'a
  show "count ?lhs p = count ?rhs p"
  proof (cases "prime p")
    case False
    have "p ∉# image_mset aprimedivisor (mset_set (primepow_factors n))"
    proof
      assume "p ∈# image_mset aprimedivisor (mset_set (primepow_factors n))"
      then obtain q where "p = aprimedivisor q" "q ∈ primepow_factors n"
        by (auto simp: finite_primepow_factors)
      with False prime_aprimedivisor'[of q] have "q = 0 ∨ is_unit q" by auto
      with ‹q ∈ primepow_factors n› show False by (auto simp: primepow_factors_def primepow_def)
    qed
    hence "count ?lhs p = 0" by (simp only: Multiset.not_in_iff)
    with False show ?thesis by (simp add: count_prime_factorization)
  next
    case True
    hence p: "p ≠ 0" "¬is_unit p" by auto
    have "count ?lhs p = card (aprimedivisor -` {p} ∩ primepow_factors n)"
      by (simp add: count_image_mset finite_primepow_factors)
    also have "aprimedivisor -` {p} ∩ primepow_factors n = {p^k |k. k > 0 ∧ p ^ k dvd n}"
      using True by (rule aprimedivisor_vimage)
    also from True have "… = (λk. p ^ k) ` {0<..multiplicity p n}"
      by (subst power_dvd_iff_le_multiplicity) auto
    also from p True have "card … = multiplicity p n"
      by (subst card_image) (auto intro!: inj_onI dest: prime_power_inj)
    also from True have "… = count (prime_factorization n) p" 
      by (simp add: count_prime_factorization)
    finally show ?thesis .
  qed
qed

lemma prime_elem_aprimedivisor_nat: "d > Suc 0 ⟹ prime_elem (aprimedivisor d)"
  using prime_aprimedivisor'[of d] by simp

lemma aprimedivisor_gt_0_nat [simp]: "d > Suc 0 ⟹ aprimedivisor d > 0"
  using prime_aprimedivisor'[of d] by (simp add: prime_gt_0_nat)

lemma aprimedivisor_gt_Suc_0_nat [simp]: "d > Suc 0 ⟹ aprimedivisor d > Suc 0"
  using prime_aprimedivisor'[of d] by (simp add: prime_gt_Suc_0_nat)

lemma aprimedivisor_not_Suc_0_nat [simp]: "d > Suc 0 ⟹ aprimedivisor d ≠ Suc 0"
  using aprimedivisor_gt_Suc_0[of d] by (intro notI) auto

lemma multiplicity_aprimedivisor_gt_0_nat [simp]:
  "d > Suc 0 ⟹ multiplicity (aprimedivisor d) d > 0"
  by (subst multiplicity_gt_zero_iff) (auto intro: aprimedivisor_dvd')

lemma primepowI:
  "prime p ⟹ k > 0 ⟹ p ^ k = n ⟹ primepow n ∧ aprimedivisor n = p"
  unfolding primepow_def by (auto simp: aprimedivisor_prime_power)

lemma not_primepowI:
  assumes "prime p" "prime q" "p ≠ q" "p dvd n" "q dvd n"
  shows   "¬primepow n"
  using assms by (auto simp: primepow_def dest!: prime_dvd_power[rotated] dest: primes_dvd_imp_eq)

lemma sum_prime_factorization_conv_sum_primepow_factors:
  fixes n :: "'a :: factorial_semiring_multiplicative"
  assumes "n ≠ 0"
  shows "(∑q∈primepow_factors n. f (aprimedivisor q)) = (∑p∈#prime_factorization n. f p)"
proof -
  from assms have "prime_factorization n = image_mset aprimedivisor (mset_set (primepow_factors n))"
    by (rule aprimedivisor_primepow_factors_conv_prime_factorization [symmetric])
  also have "(∑p∈#…. f p) = (∑q∈primepow_factors n. f (aprimedivisor q))"
    by (simp add: image_mset.compositionality sum_unfold_sum_mset o_def)
  finally show ?thesis ..
qed    

lemma multiplicity_aprimedivisor_Suc_0_iff:
  assumes "primepow (n :: 'a :: factorial_semiring_multiplicative)"
  shows   "multiplicity (aprimedivisor n) n = Suc 0 ⟷ prime n"
  by (subst (3) primepow_decompose [OF assms, symmetric])
     (insert assms, auto simp add: prime_power_iff intro!: prime_aprimedivisor')


definition mangoldt :: "nat ⇒ 'a :: real_algebra_1" where
  "mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"

lemma mangoldt_0 [simp]: "mangoldt 0 = 0"
  by (simp add: mangoldt_def)

lemma mangoldt_Suc_0 [simp]: "mangoldt (Suc 0) = 0"
  by (simp add: mangoldt_def)

lemma of_real_mangoldt [simp]: "of_real (mangoldt n) = mangoldt n"
  by (simp add: mangoldt_def)

lemma mangoldt_sum:
  assumes "n ≠ 0"
  shows   "(∑d | d dvd n. mangoldt d :: 'a :: real_algebra_1) = of_real (ln (real n))"
proof -
  have "(∑d | d dvd n. mangoldt d :: 'a) = of_real (∑d | d dvd n. mangoldt d)" by simp
  also have "(∑d | d dvd n. mangoldt d) = (∑d ∈ primepow_factors n. ln (real (aprimedivisor d)))"
    using assms by (intro sum.mono_neutral_cong_right) (auto simp: primepow_factors_def mangoldt_def)
  also have "… = ln (real (∏d ∈ primepow_factors n. aprimedivisor d))"
    using assms finite_primepow_factors[of n]
    by (subst ln_prod [symmetric])
       (auto simp: primepow_factors_def intro!: aprimedivisor_pos_nat 
             intro: Nat.gr0I primepow_gt_Suc_0)
  also have "primepow_factors n = 
               (λ(p,k). p ^ k) ` (SIGMA p:prime_factors n. {0<..multiplicity p n})" 
    (is "_ = _ ` ?A") by (subst primepow_factors_altdef[OF assms]) fast+
  also have "prod aprimedivisor … = (∏(p,k)∈?A. aprimedivisor (p ^ k))"
    by (subst prod.reindex)
       (auto simp: inj_on_def prime_power_inj'' prime_factors_multiplicity 
                   prod.Sigma [symmetric] case_prod_unfold)
  also have "… = (∏(p,k)∈?A. p)" 
    by (intro prod.cong refl) (auto simp: aprimedivisor_prime_power prime_factors_multiplicity)
  also have "… = (∏x∈prime_factors n. ∏k∈{0<..multiplicity x n}. x)"
    by (rule prod.Sigma [symmetric]) auto
  also have "… = (∏x∈prime_factors n. x ^ multiplicity x n)" 
    by (intro prod.cong refl) (simp add: prod_constant)
  also have "… = n" using assms by (intro prime_factorization_nat [symmetric]) simp
  finally show ?thesis .
qed

lemma mangoldt_primepow:
   "prime p ⟹ mangoldt (p ^ k) = (if k > 0 then of_real (ln (real p)) else 0)"
  by (simp add: mangoldt_def aprimedivisor_prime_power)

lemma mangoldt_primepow' [simp]: "prime p ⟹ k > 0 ⟹ mangoldt (p ^ k) = of_real (ln (real p))"
  by (subst mangoldt_primepow) auto

lemma mangoldt_prime [simp]: "prime p ⟹ mangoldt p = of_real (ln (real p))"    
  using mangoldt_primepow[of p 1] by simp

lemma mangoldt_nonneg: "0 ≤ (mangoldt d :: real)"
  using aprimedivisor_gt_Suc_0_nat[of d]
  by (auto simp: mangoldt_def of_nat_le_iff[of 1 x for x, unfolded of_nat_1] Suc_le_eq
           intro!: ln_ge_zero dest: primepow_gt_Suc_0)

lemma norm_mangoldt [simp]:
  "norm (mangoldt n :: 'a :: real_normed_algebra_1) = mangoldt n"
proof (cases "primepow n")
  case True
  hence "prime (aprimedivisor n)"
    by (intro prime_aprimedivisor') 
       (auto simp: primepow_def prime_gt_0_nat)
  hence "aprimedivisor n > 1" by (simp add: prime_gt_Suc_0_nat)
  with True show ?thesis by (auto simp: mangoldt_def abs_if)
qed (auto simp: mangoldt_def)

lemma Re_mangoldt [simp]: "Re (mangoldt n) = mangoldt n"
  and Im_mangoldt [simp]: "Im (mangoldt n) = 0"
  by (simp_all add: mangoldt_def)

lemma abs_mangoldt [simp]: "abs (mangoldt n :: real) = mangoldt n"
  using norm_mangoldt[of n, where ?'a = real, unfolded real_norm_def] .

lemma mangoldt_le: 
  assumes "n > 0"
  shows   "mangoldt n ≤ ln n"
proof (cases "primepow n")
  case True
  from True have "prime (aprimedivisor n)"
    by (intro prime_aprimedivisor') 
       (auto simp: primepow_def prime_gt_0_nat)
  hence gt_1: "aprimedivisor n > 1" by (simp add: prime_gt_Suc_0_nat)
  from True have "mangoldt n = ln (aprimedivisor n)"
    by (simp add: mangoldt_def)
  also have "… ≤ ln n" using True gt_1 
    by (subst ln_le_cancel_iff) (auto intro!: Nat.gr0I dvd_imp_le aprimedivisor_dvd')
  finally show ?thesis .
qed (insert assms, auto simp: mangoldt_def)

end