# Theory Dirichlet_Product

theory Dirichlet_Product
imports Multiplicative_Function
```(*
File:      Dirichlet_Product.thy
Author:    Manuel Eberl, TU München
*)
section ‹Dirichlet convolution›
theory Dirichlet_Product
imports
Complex_Main
Multiplicative_Function
begin

lemma sum_coprime_dvd_cong:
"(∑r | r dvd a. ∑s | s dvd b. f r s) = (∑r | r dvd a. ∑s | s dvd b. g r s)"
if "coprime a b" "⋀r s. coprime r s ⟹ r dvd a ⟹ s dvd b ⟹ f r s = g r s"
using refl proof (rule sum.cong, rule sum.cong)
fix r s
assume "r ∈ {r. r dvd a}" and "s ∈ {s. s dvd b}"
then have "r dvd a" and "s dvd b"
by simp_all
moreover from ‹coprime a b› have "coprime r s"
using ‹r dvd a› ‹s dvd b›
by (auto intro: coprime_imp_coprime dvd_trans)
ultimately show "f r s = g r s"
using that by simp
qed

definition dirichlet_prod :: "(nat ⇒ 'a :: semiring_0) ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'a" where
"dirichlet_prod f g = (λn. ∑d | d dvd n. f d * g (n div d))"

lemma sum_divisors_code:
assumes "n > (0::nat)"
shows   "(∑d | d dvd n. f d) =
fold_atLeastAtMost_nat (λd acc. if d dvd n then f d + acc else acc) 1 n 0"
proof -
have "(λd acc. if d dvd n then f d + acc else acc) = (λd acc. (if d dvd n then f d else 0) + acc)"
by (simp add: fun_eq_iff)
hence "fold_atLeastAtMost_nat (λd acc. if d dvd n then f d + acc else acc) 1 n 0 =
fold_atLeastAtMost_nat (λd acc. (if d dvd n then f d else 0) + acc) 1 n 0"
by (simp only: )
also have "… = (∑d = 1..n. if d dvd n then f d else 0)"
by (rule sum_atLeastAtMost_code [symmetric])
also from assms have "… = (∑d | d dvd n. f d)"
by (intro sum.mono_neutral_cong_right) (auto elim: dvdE dest: dvd_imp_le)
finally show ?thesis ..
qed

lemma dirichlet_prod_code [code]:
"dirichlet_prod f g n = (if n = 0 then 0 else
fold_atLeastAtMost_nat (λd acc. if d dvd n then f d * g (n div d) + acc else acc) 1 n 0)"
unfolding dirichlet_prod_def by (simp add: sum_divisors_code)

lemma dirichlet_prod_0 [simp]: "dirichlet_prod f g 0 = 0"
by (simp add: dirichlet_prod_def)

lemma dirichlet_prod_Suc_0 [simp]: "dirichlet_prod f g (Suc 0) = f (Suc 0) * g (Suc 0)"
by (simp add: dirichlet_prod_def)

lemma dirichlet_prod_cong [cong]:
assumes "(⋀n. n > 0 ⟹ f n = f' n)" "(⋀n. n > 0 ⟹ g n = g' n)"
shows   "dirichlet_prod f g = dirichlet_prod f' g'"
proof
fix n :: nat
show "dirichlet_prod f g n = dirichlet_prod f' g' n"
proof (cases "n = 0")
case False
with assms show ?thesis unfolding dirichlet_prod_def
by (intro ext sum.cong refl) (auto elim!: dvdE)
qed simp_all
qed

lemma dirichlet_prod_altdef1:
"dirichlet_prod f g = (λn. ∑d | d dvd n. f (n div d) * g d)"
proof
fix n :: nat
show "dirichlet_prod f g n = (∑d | d dvd n. f (n div d) * g d)"
proof (cases "n = 0")
case False
hence "dirichlet_prod f g n = (∑d | d dvd n. f (n div (n div d)) * g (n div d))"
unfolding dirichlet_prod_def by (intro sum.cong refl) (auto elim!: dvdE)
also from False have "… = (∑d | d dvd n. f (n div d) * g d)"
by (intro sum.reindex_bij_witness[of _ "(div) n" "(div) n"]) (auto elim!: dvdE)
finally show ?thesis .
qed simp
qed

lemma dirichlet_prod_altdef2:
"dirichlet_prod f g = (λn. ∑(r,d) | r * d = n. f r * g d)"
proof
fix n
show "dirichlet_prod f g n = (∑(r,d) | r * d = n. f r * g d)"
proof (cases "n = 0")
case True
have "(λn::nat. (0, n)) ` UNIV ⊆ {(r,d). r * d = 0}" by auto
moreover have "¬finite ((λn::nat. (0, n)) ` UNIV)"
by (subst finite_image_iff) (auto simp: inj_on_def)
ultimately have "infinite {(r,d). r * d = (0::nat)}"
by (blast dest: finite_subset)
with True show ?thesis by simp
next
case False
have "(∑d | d dvd n. f d * g (n div d)) = (∑r | r dvd n. (∑d | d = n div r. f r * g d))"
by (intro sum.cong refl) auto
also from False have "… = (∑(r,d)∈(SIGMA x:{r. r dvd n}. {d. d = n div x}). f r * g d)"
by (intro sum.Sigma) auto
also from False have "(SIGMA x:{r. r dvd n}. {d. d = n div x}) = {(r,d). r * d = n}"
by auto
finally show ?thesis by (simp add: dirichlet_prod_def)
qed
qed

lemma dirichlet_prod_commutes:
"dirichlet_prod (f :: nat ⇒ 'a :: comm_semiring_0) g = dirichlet_prod g f"
proof
fix n :: nat
show "dirichlet_prod f g n = dirichlet_prod g f n"
proof (cases "n = 0")
case False
have "(∑(r,d) | r * d = n. f r * g d) = (∑(d,r) | r * d = n. f r * g d)"
by (rule sum.reindex_bij_witness [of _ "λ(x,y). (y,x)" "λ(x,y). (y,x)"]) auto
thus ?thesis by (simp add: dirichlet_prod_altdef2 mult.commute)
qed (simp add: dirichlet_prod_def)
qed

lemma finite_divisors_nat': "n > (0 :: nat) ⟹ finite {(a,b). a * b = n}"
by (rule finite_subset[of _ "{0<..n} × {0<..n}"]) auto

lemma dirichlet_prod_assoc_aux1:
assumes "n > 0"
shows "dirichlet_prod f (dirichlet_prod g h) n =
(∑(a, b, c)∈{(a, b, c). a * b * c = n}. f a * g b * h c)"
proof -
have "dirichlet_prod f (dirichlet_prod g h) n =
(∑x∈{(a,b). a * b = n}. (∑(c,d) | c * d = snd x. f (fst x) * g c * h d))"
by (auto intro!: sum.cong simp: dirichlet_prod_altdef2 sum_distrib_left mult.assoc)
also from assms have "… = (∑x∈(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = snd x}).
case x of (x, c, d) ⇒ f (fst x) * g c * h d)"
by (intro sum.Sigma finite_divisors_nat' ballI) auto
also have "… = (∑(a,b,c) | a * b * c = n. f a * g b * h c)"
by (rule sum.reindex_bij_witness
[of _ "λ(a,b,c). ((a, b*c), (b,c))" "λ((a,b),(c,d)). (a, c, d)"])
(auto simp: mult_ac)
finally show ?thesis .
qed

lemma dirichlet_prod_assoc_aux2:
assumes "n > 0"
shows "dirichlet_prod (dirichlet_prod f g) h n =
(∑(a, b, c)∈{(a, b, c). a * b * c = n}. f a * g b * h c)"
proof -
have "dirichlet_prod (dirichlet_prod f g) h n =
(∑x∈{(a,b). a * b = n}. (∑(c,d) | c * d = fst x. f c * g d * h (snd x)))"
by (auto intro!: sum.cong simp: dirichlet_prod_altdef2 sum_distrib_right mult.assoc)
also from assms have "… = (∑x∈(SIGMA x:{(a, b). a * b = n}. {(c, d). c * d = fst x}).
case x of (x, c, d) ⇒ f c * g d * h (snd x))"
by (intro sum.Sigma finite_divisors_nat' ballI) auto
also have "… = (∑(a,b,c) | a * b * c = n. f a * g b * h c)"
by (rule sum.reindex_bij_witness
[of _ "λ(a,b,c). ((a*b, c), (a,b))" "λ((a,b),(c,d)). (c, d, b)"])
(auto simp: mult_ac)
finally show ?thesis .
qed

lemma dirichlet_prod_assoc:
"dirichlet_prod (dirichlet_prod f g) h = dirichlet_prod f (dirichlet_prod g h)"
proof
fix n :: nat
show "dirichlet_prod (dirichlet_prod f g) h n = dirichlet_prod f (dirichlet_prod g h) n"
by (cases "n = 0") (simp_all add: dirichlet_prod_assoc_aux1 dirichlet_prod_assoc_aux2)
qed

lemma dirichlet_prod_const_right [simp]:
assumes "n > 0"
shows   "dirichlet_prod f (λn. if n = Suc 0 then c else 0) n = f n * c"
proof -
have "dirichlet_prod f (λn. if n = Suc 0 then c else 0) n =
(∑d | d dvd n. (if d = n then f n * c else 0))"
unfolding dirichlet_prod_def using assms
by (intro sum.cong refl) (auto elim!: dvdE split: if_splits)
also have "… = f n * c" using assms by (subst sum.delta) auto
finally show ?thesis .
qed

lemma dirichlet_prod_const_left [simp]:
assumes "n > 0"
shows   "dirichlet_prod (λn. if n = Suc 0 then c else 0) g n = c * g n"
proof -
have "dirichlet_prod (λn. if n = Suc 0 then c else 0) g n =
(∑d | d dvd n. (if d = 1 then c * g n else 0))"
unfolding dirichlet_prod_def using assms
by (intro sum.cong refl) (auto elim!: dvdE split: if_splits)
also have "… = c * g n" using assms by (subst sum.delta) auto
finally show ?thesis .
qed

fun dirichlet_inverse :: "(nat ⇒ 'a :: comm_ring_1) ⇒ 'a ⇒ nat ⇒ 'a" where
"dirichlet_inverse f i n =
(if n = 0 then 0 else if n = 1 then i
else -i * (∑d | d dvd n ∧ d < n. f (n div d) * dirichlet_inverse f i d))"

lemma dirichlet_inverse_induct [case_names 0 1 gt1]:
"P 0 ⟹ P (Suc 0) ⟹ (⋀n. n > 1 ⟹ (⋀k. k < n ⟹ P k) ⟹ P n) ⟹ P n"
by induction_schema (force, rule wf_measure [of id], simp)

lemma dirichlet_inverse_0 [simp]: "dirichlet_inverse f i 0 = 0"
by simp

lemma dirichlet_inverse_Suc_0 [simp]: "dirichlet_inverse f i (Suc 0) = i"
by simp

declare dirichlet_inverse.simps [simp del]

lemma dirichlet_inverse_gt_1:
"n > 1 ⟹ dirichlet_inverse f i n =
-i * (∑d | d dvd n ∧ d < n. f (n div d) * dirichlet_inverse f i d)"
by (simp add: dirichlet_inverse.simps)

lemma dirichlet_inverse_cong [cong]:
assumes "⋀n. n > 0 ⟹ f n = f' n" "i = i'" "n = n'"
shows   "dirichlet_inverse f i n = dirichlet_inverse f' i' n'"
proof -
have "dirichlet_inverse f i n = dirichlet_inverse f' i n"
using assms(1)
proof (induction n rule: dirichlet_inverse_induct)
case (gt1 n)
have *: "dirichlet_inverse f i k = dirichlet_inverse f' i k" if "k dvd n ∧ k < n" for k
using that by (intro gt1) auto
have *: "(∑d | d dvd n ∧ d < n. f (n div d) * dirichlet_inverse f i d) =
(∑d | d dvd n ∧ d < n. f' (n div d) * dirichlet_inverse f' i d)"
by (intro sum.cong refl) (subst gt1.prems, auto elim: dvdE simp: *)
consider "n = 0" | "n = 1" | "n > 1" by force
thus ?case
by cases (insert *, simp_all add: dirichlet_inverse_gt_1 * cong: sum.cong)
qed auto
with assms(2,3) show ?thesis by simp
qed

lemma dirichlet_inverse_gt_1':
assumes "n > 1"
shows   "dirichlet_inverse f i n =
-i * dirichlet_prod (λn. if n = 1 then 0 else f n) (dirichlet_inverse f i) n"
proof -
have "dirichlet_prod (λn. if n = 1 then 0 else f n) (dirichlet_inverse f i) n =
(∑d | d dvd n. (if n div d = Suc 0 then 0 else f (n div d)) * dirichlet_inverse f i d)"
by (simp add: dirichlet_prod_altdef1)
also from assms have "… = (∑d | d dvd n ∧ d ≠ n. f (n div d) * dirichlet_inverse f i d)"
by (intro sum.mono_neutral_cong_right) (auto elim: dvdE)
also from assms have "{d. d dvd n ∧ d ≠ n} = {d. d dvd n ∧ d < n}" by (auto dest: dvd_imp_le)
also from assms have "-i * (∑d∈…. f (n div d) * dirichlet_inverse f i d) =
dirichlet_inverse f i n"
by (simp add: dirichlet_inverse_gt_1)
finally show ?thesis ..
qed

lemma of_int_dirichlet_prod:
"of_int (dirichlet_prod f g n) = dirichlet_prod (λn. of_int (f n)) (λn. of_int (g n)) n"
by (simp add: dirichlet_prod_def)

lemma of_int_dirichlet_inverse:
"of_int (dirichlet_inverse f i n) = dirichlet_inverse (λn. of_int (f n)) (of_int i) n"
proof (induction n rule: dirichlet_inverse_induct)
case (gt1 n)
from gt1 have "(of_int (dirichlet_inverse f i n) :: 'a) =
- (of_int i * (∑d | d dvd n ∧ d < n. of_int (f (n div d) * dirichlet_inverse f i d)))"
(is "_ = - (_ * ?A)")
by (simp add: dirichlet_inverse_gt_1 of_int_dirichlet_prod)
also have "?A = (∑d | d dvd n ∧ d < n. of_int (f (n div d)) *
dirichlet_inverse (λn. of_int (f n)) (of_int i) d)"
by (intro sum.cong refl) (auto simp: gt1)
also have "-(of_int i * …) = dirichlet_inverse (λn. of_int (f n)) (of_int i) n"
using gt1.hyps by (simp add: dirichlet_inverse_gt_1)
finally show ?case .
qed simp_all

lemma dirichlet_inverse_code [code]:
"dirichlet_inverse f i n = (if n = 0 then 0 else if n = 1 then i else
-i * fold_atLeastAtMost_nat (λd acc. if d dvd n then f (n div d) *
dirichlet_inverse f i d + acc else acc) 1 (n - 1) 0)"
proof -
consider "n = 0" | "n = 1" | "n > 1" by force
thus ?thesis
proof cases
assume n: "n > 1"
have *: "(λd acc. if d dvd n then f (n div d) * dirichlet_inverse f i d + acc else acc) =
(λd acc. (if d dvd n then f (n div d) * dirichlet_inverse f i d else 0) + acc)"
by (simp add: fun_eq_iff)
have "fold_atLeastAtMost_nat (λd acc. if d dvd n then f (n div d) *
dirichlet_inverse f i d + acc else acc) 1 (n - 1) 0 =
(∑d = 1..n - 1. if d dvd n then f (n div d) * dirichlet_inverse f i d else 0)"
by (subst *, subst sum_atLeastAtMost_code [symmetric]) simp
also from n have "… = (∑d | d dvd n ∧ d < n. f (n div d) * dirichlet_inverse f i d)"
by (intro sum.mono_neutral_cong_right; cases n)
(auto dest: dvd_imp_le elim: dvdE simp: Suc_le_eq intro!: Nat.gr0I)
also from n have "-i * … = dirichlet_inverse f i n"
by (simp add: dirichlet_inverse_gt_1)
finally show ?thesis using n by simp
qed auto
qed

lemma dirichlet_prod_inverse:
assumes "f 1 * i = 1"
shows   "dirichlet_prod f (dirichlet_inverse f i) = (λn. if n = 1 then 1 else 0)"
proof
fix n :: nat
consider "n = 0" | "n = 1" | "n > 1" by force
thus "dirichlet_prod f (dirichlet_inverse f i) n = (if n = 1 then 1 else 0)"
proof cases
assume n: "n > 1"
have fin: "finite {d. d dvd n ∧ d ≠ n}"
by (rule finite_subset[of _ "{d. d dvd n}"]) (insert n, auto)
have "dirichlet_prod f (dirichlet_inverse f i) n =
(∑d | d dvd n. f (n div d) * dirichlet_inverse f i d)"
by (simp add: dirichlet_prod_altdef1)
also have "{d. d dvd n} = insert n {d. d dvd n ∧ d ≠ n}" by auto
also have "(∑d∈…. f (n div d) * dirichlet_inverse f i d) =
f 1 * dirichlet_inverse f i n +
(∑d | d dvd n ∧ d ≠ n. f (n div d) * dirichlet_inverse f i d)"
using fin n by (subst sum.insert) auto
also from n have "dirichlet_inverse f i n =
- i * (∑d | d dvd n ∧ d < n. f (n div d) * dirichlet_inverse f i d)"
by (subst dirichlet_inverse_gt_1) auto
also from n have "{d. d dvd n ∧ d < n} = {d. d dvd n ∧ d ≠ n}" by (auto dest: dvd_imp_le)
also have "f 1 * (- i *
(∑d | d dvd n ∧ d ≠ n. f (n div d) * dirichlet_inverse f i d)) =
-(f 1 * i) *
(∑d | d dvd n ∧ d ≠ n. f (n div d) * dirichlet_inverse f i d)"
by (simp add: mult.assoc)
also have "f 1 * i = 1" by fact
finally show ?thesis using n by simp
qed (insert assms, simp_all add: dirichlet_prod_def)
qed

lemma dirichlet_prod_inverse':
assumes "f 1 * i = 1"
shows   "dirichlet_prod (dirichlet_inverse f i) f = (λn. if n = 1 then 1 else 0)"
using dirichlet_prod_inverse[of f] assms by (simp add: dirichlet_prod_commutes)

lemma dirichlet_inverse_noninvertible:
assumes "f (Suc 0) = (0 :: 'a :: {comm_ring_1})" "i = 0"
shows   "dirichlet_inverse f i n = 0"
using assms
by (induction f i n rule: dirichlet_inverse.induct) (auto simp: dirichlet_inverse.simps)

lemma multiplicative_dirichlet_prod:
assumes "multiplicative_function f"
assumes "multiplicative_function g"
shows   "multiplicative_function (dirichlet_prod f g)"
proof -
interpret f: multiplicative_function f by fact
interpret g: multiplicative_function g by fact
show ?thesis
proof
fix a b :: nat assume "a > 1" "b > 1" and coprime: "coprime a b"
hence "dirichlet_prod f g (a * b) =
(∑r | r dvd a. ∑s | s dvd b. f (r * s) * g (a * b div (r * s)))"
by (simp add: dirichlet_prod_def sum_divisors_coprime_mult)
also have "… = (∑r | r dvd a. ∑s | s dvd b. f r * f s * g (a div r) * g (b div s))"
using ‹coprime a b› proof (rule sum_coprime_dvd_cong)
fix r s
assume "coprime r s" and "r dvd a" and "s dvd b"
with ‹a > 1› ‹b > 1› have "r > 0" "s > 0"
by (auto intro: ccontr)
from ‹coprime r s› have "f (r * s) = f r * f s"
by (rule f.mult_coprime)
moreover from ‹coprime a b› have ‹coprime (a div r) (b div s)›
using ‹r > 0› ‹s > 0› ‹r dvd a› ‹s dvd b› dvd_div_iff_mult [of r a] dvd_div_iff_mult [of s b]
by (auto dest: coprime_imp_coprime dvd_mult_left)
then have "g (a div r * (b div s)) = g (a div r) * g (b div s)"
by (rule g.mult_coprime)
ultimately show "f (r * s) * g (a * b div (r * s)) = f r * f s * g (a div r) * g (b div s)"
using ‹r dvd a› ‹s dvd b› by (simp add: div_mult_div_if_dvd ac_simps)
qed
also have "… = dirichlet_prod f g a * dirichlet_prod f g b"
unfolding dirichlet_prod_def by (simp add: sum_product mult_ac)
finally show "dirichlet_prod f g (a * b) = …" .
qed simp_all
qed

lemma multiplicative_dirichlet_prodD1:
fixes f g :: "nat ⇒ 'a :: comm_semiring_1_cancel"
assumes "multiplicative_function (dirichlet_prod f g)"
assumes "multiplicative_function f"
assumes [simp]: "g 0 = 0"
shows   "multiplicative_function g"
proof -
interpret f: multiplicative_function f by fact
interpret fg: multiplicative_function "dirichlet_prod f g" by fact
show ?thesis
proof
have "dirichlet_prod f g (Suc 0) = 1" by (rule fg.Suc_0)
also have "dirichlet_prod f g (Suc 0) = g 1" by (subst dirichlet_prod_Suc_0) simp
finally show "g 1 = 1" by simp
next
fix a b :: nat assume ab: "a > 1" "b > 1" "coprime a b"
hence "a > 0" "b > 0" "coprime a b" by simp_all
thus "g (a * b) = g a * g b"
proof (induction "a * b" arbitrary: a b rule: less_induct)
case (less a b)
have "dirichlet_prod f g (a * b) + g a * g b =
(∑r | r dvd a * b. f r * g (a * b div r)) + g a * g b"
by (simp add: dirichlet_prod_def)
also have "{r. r dvd a * b} = insert 1 {r. r dvd a * b ∧ r ≠ 1}" by auto
also have "(∑r∈…. f r * g (a * b div r)) + g a * g b =
g (a * b) + ((∑r | r dvd a * b ∧ r ≠ 1. f r * g (a * b div r)) + g a * g b)"
using less.prems
by (subst sum.insert) (auto intro!: finite_subset[OF _ finite_divisors_nat'] simp: add_ac)
also have "(∑r | r dvd a * b ∧ r ≠ 1. f r * g (a * b div r)) =
(∑r | r dvd a * b. if r = 1 then 0 else f r * g (a * b div r))"
using less.prems by (intro sum.mono_neutral_cong_left) (auto intro: finite_divisors_nat')
also have "… = (∑r | r dvd a. ∑d | d dvd b.
if r * d = 1 then 0 else f (r * d) * g (a * b div (r * d)))"
using ‹coprime a b› by (rule sum_divisors_coprime_mult)
also have "… = (∑r | r dvd a. ∑d | d dvd b.
if r * d = 1 then 0 else f (r * d) * g ((a div r) * (b div d)))"
by (intro sum.cong refl) (auto elim!: dvdE)
also have "… = (∑r | r dvd a. ∑d | d dvd b.
if r * d = 1 then 0 else f r * f d * g (a div r) * g (b div d))"
using ‹coprime a b› proof (rule sum_coprime_dvd_cong)
fix r s
assume "coprime r s" and "r dvd a" and "s dvd b"
with ‹a > 0› ‹b > 0› have "r > 0" "s > 0"
by (auto intro: ccontr)
from ‹coprime r s› have f: "f (r * s) = f r * f s"
by (rule f.mult_coprime)
show "(if r * s = 1 then 0 else f (r * s) * g (a div r * (b div s))) =
(if r * s = 1 then 0 else f r * f s * g (a div r) * g (b div s))"
proof (cases "r * s = 1")
case True
then show ?thesis
by simp
next
case False
with ‹r dvd a› ‹s dvd b› less.prems
have "(a div r) * (b div s) ≠ a * b"
by (intro notI) (auto elim!: dvdE)
moreover from ‹r dvd a› ‹s dvd b› less.prems
have "(a div r) * (b div s) ≤ a * b"
by (intro dvd_imp_le mult_dvd_mono Nat.gr0I) (auto elim!: dvdE)
ultimately have "(a div r) * (b div s) < a * b"
by arith
with ‹r dvd a› ‹s dvd b› less.prems
have g: "g ((a div r) * (b div s)) = g (a div r) * g (b div s)"
by (auto intro: less coprime_divisors [OF _ _ ‹coprime a b›] elim!: dvdE)
from False show ?thesis
by (auto simp: less f g ac_simps)
qed
qed
also have "… = (∑(r,d)∈{r. r dvd a}×{d. d dvd b}.
if r * d = 1 then 0 else f r * f d * g (a div r) * g (b div d))"
by (simp add: sum.cartesian_product)
also have "… = (∑(r1,r2) ∈ {r1. r1 dvd a} × {r2. r2 dvd b} - {(1,1)}.
(f r1 * f r2) * g (a div r1) * g (b div r2))" (is "_ = sum ?f ?A")
using less.prems by (intro sum.mono_neutral_cong_right) (auto split: if_splits)
also have "… + g a * g b = ?f (1, 1) + sum ?f ?A" by (simp add: add_ac)
also have "… = sum ?f ({r1. r1 dvd a} × {r2. r2 dvd b})" using less.prems
by (intro sum.remove [symmetric]) auto
also have "… = dirichlet_prod f g a * dirichlet_prod f g b"
by (simp add: sum.cartesian_product sum_product dirichlet_prod_def mult_ac)
also have "g (a * b) + dirichlet_prod f g a * dirichlet_prod f g b =
dirichlet_prod f g (a * b) + g (a * b)"
using less.prems by (simp add: fg.mult_coprime add_ac)
finally show ?case by simp
qed
qed simp_all
qed

lemma multiplicative_dirichlet_prodD2:
fixes f g :: "nat ⇒ 'a :: comm_semiring_1_cancel"
assumes "multiplicative_function (dirichlet_prod f g)"
assumes "multiplicative_function g"
assumes [simp]: "f 0 = 0"
shows   "multiplicative_function f"
proof -
from assms(1) have "multiplicative_function (dirichlet_prod g f)"
by (simp add: dirichlet_prod_commutes)
from multiplicative_dirichlet_prodD1[OF this assms(2)] show ?thesis by simp
qed

lemma multiplicative_dirichlet_inverse:
assumes "multiplicative_function f"
shows   "multiplicative_function (dirichlet_inverse f 1)"
proof (rule multiplicative_dirichlet_prodD1[OF _ assms])
interpret multiplicative_function f by fact
have "multiplicative_function (λn. if n = 1 then 1 else 0)"
by standard simp_all
thus "multiplicative_function (dirichlet_prod f (dirichlet_inverse f 1))"
by (subst dirichlet_prod_inverse) simp_all
qed simp_all

lemma dirichlet_prod_prime_power:
assumes "prime p"
shows   "dirichlet_prod f g (p ^ k) = (∑i≤k. f (p ^ i) * g (p ^ (k - i)))"
proof -
have "dirichlet_prod f g (p ^ k) = (∑i≤k. f (p ^ i) * g (p ^ k div p ^ i))"
unfolding dirichlet_prod_def using assms
by (intro sum.reindex_bij_betw [symmetric] bij_betw_prime_power_divisors)
also from assms have "… = (∑i≤k. f (p ^ i) * g (p ^ (k - i)))"
by (intro sum.cong refl) (auto simp: power_diff')
finally show ?thesis .
qed

lemma dirichlet_prod_prime:
assumes "prime p"
shows   "dirichlet_prod f g p  = f 1 * g p + f p * g 1"
using dirichlet_prod_prime_power[of p f g 1] assms by simp

locale multiplicative_dirichlet_prod =
f: multiplicative_function f + g: multiplicative_function g
for f g :: "nat ⇒ 'a :: comm_semiring_1"
begin

sublocale multiplicative_function "dirichlet_prod f g"
by (intro multiplicative_dirichlet_prod
f.multiplicative_function_axioms g.multiplicative_function_axioms)

end

locale multiplicative_dirichlet_prod' =
f: multiplicative_function' f f_prime_power f_prime +
g: multiplicative_function' g g_prime_power g_prime
for f g :: "nat ⇒ 'a :: comm_semiring_1" and f_prime_power g_prime_power f_prime g_prime
begin

sublocale multiplicative_dirichlet_prod f g ..

sublocale multiplicative_function' "dirichlet_prod f g"
"λp k. f_prime_power p k + g_prime_power p k +
(∑i∈{0<..<k}. f_prime_power p i * g_prime_power p (k - i))"
"λp. f_prime p + g_prime p"
proof (standard, goal_cases)
case (1 p k)
hence "dirichlet_prod f g (p ^ k) = (∑i≤k. f (p ^ i) * g (p ^ (k - i)))"
by (intro dirichlet_prod_prime_power)
also from 1 have "{..k} = insert 0 (insert k {0<..<k})" by auto
also have "(∑i∈…. f (p ^ i) * g (p ^ (k - i))) =
f_prime_power p k + g_prime_power p k +
(∑i∈{0<..<k}. f (p ^ i) * g (p ^ (k - i)))" using 1
by (auto simp: f.prime_power g.prime_power add_ac)
also have "(∑i∈{0<..<k}. f (p ^ i) * g (p ^ (k - i))) =
(∑i∈{0<..<k}. f_prime_power p i * g_prime_power p (k - i))"
using 1 by (intro sum.cong) (auto simp: f.prime_power g.prime_power)
finally show ?case .
next
case (2 p)
have "{0<..<Suc 0} = {}" by auto
with 2 show ?case
by (auto simp: f.prime_power [symmetric] g.prime_power [symmetric] f.prime g.prime add_ac)
qed

end

end
```