# Theory Multiplicative_Function

theory Multiplicative_Function
imports Dirichlet_Misc
```(*
File:      Multiplicative_Function.thy
Author:    Manuel Eberl, TU München
*)
section ‹Multiplicative arithmetic functions›
theory Multiplicative_Function
imports
"HOL-Number_Theory.Number_Theory"
Dirichlet_Misc
begin

subsection ‹Definition›

locale multiplicative_function =
fixes f :: "nat ⇒ 'a :: comm_semiring_1"
assumes zero [simp]: "f 0 = 0"
assumes one [simp]: "f 1 = 1"
assumes mult_coprime_aux: "a > 1 ⟹ b > 1 ⟹ coprime a b ⟹ f (a * b) = f a * f b"
begin

lemma Suc_0 [simp]: "f (Suc 0) = 1"
using one by (simp del: one)

lemma mult_coprime:
assumes "coprime a b"
shows   "f (a * b) = f a * f b"
proof -
{fix n :: nat consider "n = 0" | "n = 1" | "n > 1" by force} note P = this
show ?thesis by (cases a rule: P; cases b rule: P) (simp_all add: mult_coprime_aux assms)
qed

lemma prod_coprime:
assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≠ y ⟹ coprime (g x) (g y)"
shows   "f (prod g A) = (∏x∈A. f (g x))"
using assms
proof (induction rule: infinite_finite_induct)
case (insert x A)
from insert have "f (prod g (insert x A)) = f (g x * prod g A)" by simp
also have "… = f (g x) * f (prod g A)" using insert.prems insert.hyps
by (auto intro: mult_coprime prod_coprime_right)
also have "… = (∏x∈insert x A. f (g x))" using insert by simp
finally show ?case .
qed auto

lemma prod_prime_factors:
assumes "n > 0"
shows   "f n = (∏p∈prime_factors n. f (p ^ multiplicity p n))"
proof -
have "n = (∏p∈prime_factors n. p ^ multiplicity p n)"
using Primes.prime_factorization_nat assms by blast
also have "f … = (∏p∈prime_factors n. f (p ^ multiplicity p n))"
by (rule prod_coprime) (auto simp add: in_prime_factors_imp_prime primes_coprime)
finally show ?thesis .
qed

lemma multiplicative_sum_divisors: "multiplicative_function (λn. ∑d | d dvd n. f d)"
proof
fix a b :: nat assume ab: "a > 1" "b > 1" "coprime a b"
hence "(∑d | d dvd a * b. f d) = (∑r | r dvd a. ∑s | s dvd b. f (r * s))"
by (intro sum_divisors_coprime_mult)
also have "… = (∑r | r dvd a. ∑s | s dvd b. f r * f s)"
using ab(3)
by (auto intro!: sum.cong intro: mult_coprime coprime_imp_coprime dvd_trans)
also have "… = (∑r | r dvd a. f r) * (∑s | s dvd b. f s)"
by (subst sum_distrib_right, subst sum_distrib_left) simp_all
finally show "(∑d | d dvd a * b. f d) = (∑r | r dvd a. f r) * (∑s | s dvd b. f s)" .
qed auto

end

locale multiplicative_function' = multiplicative_function f for f :: "nat ⇒ 'a :: comm_semiring_1" +
fixes f_prime_power :: "nat ⇒ nat ⇒ 'a" and f_prime :: "nat ⇒ 'a"
assumes prime_power: "prime p ⟹ k > 0 ⟹ f (p ^ k) = f_prime_power p k"
assumes prime_aux: "prime p ⟹ f_prime_power p 1 = f_prime p"
begin

lemma prime: "prime p ⟹ f p = f_prime p"
using prime_power[of p 1] prime_aux[of p] by simp

lemma prod_prime_factors':
assumes "n > 0"
shows   "f n = (∏p∈prime_factors n. f_prime_power p (multiplicity p n))"
by (subst prod_prime_factors[OF assms(1)])
(intro prod.cong refl prime_power, auto simp: prime_factors_multiplicity)

lemma efficient_code_aux:
assumes "n > 0" "set ps = (λp. (p, multiplicity p n - 1)) ` prime_factors n" "distinct ps"
shows   "f n = (∏(p,d) ← ps. f_prime_power p (Suc d))"
proof -
from assms have
"(∏(p,d) ← ps. f_prime_power p (Suc d)) =
(∏(p,d)∈(λp. (p, multiplicity p n - 1)) ` prime_factors n. f_prime_power p (Suc d))"
by (subst prod.distinct_set_conv_list [symmetric]) simp_all
also have "… = (∏x∈prime_factors n. f_prime_power x (multiplicity x n))"
by (subst prod.reindex) (auto simp: inj_on_def prime_factors_multiplicity intro!: prod.cong)
also have "… = f n" by (rule prod_prime_factors' [symmetric]) fact+
finally show ?thesis ..
qed

lemma efficient_code:
assumes "set (ps ()) = (λp. (p, multiplicity p n - 1)) ` prime_factors n" "distinct (ps ())"
shows   "f n = (if n = 0 then 0 else (∏(p,d) ← ps (). f_prime_power p (Suc d)))"
using efficient_code_aux[of n "ps ()"] assms by simp

end

locale completely_multiplicative_function =
fixes f :: "nat ⇒ 'a :: comm_semiring_1"
assumes zero_aux: "f 0 = 0"
assumes one_aux:  "f (Suc 0) = 1"
assumes mult_aux: "a > 1 ⟹ b > 1 ⟹ f (a * b) = f a * f b"
begin

lemma mult: "f (a * b) = f a * f b"
proof -
{fix n :: nat consider "n = 0" | "n = 1" | "n > 1" by force} note P = this
show ?thesis by (cases a rule: P; cases b rule: P) (simp_all add: zero_aux one_aux mult_aux)
qed

sublocale multiplicative_function f
by standard (simp_all add: zero_aux one_aux mult)

lemma prod: "f (prod g A) = (∏x∈A. f (g x))"
by (induction A rule: infinite_finite_induct) (simp_all add: mult)

lemma power: "f (n ^ m) = f n ^ m"
by (induction m) (simp_all add: mult)

lemma prod_prime_factors': "n > 0 ⟹ f n = (∏p∈prime_factors n. f p ^ multiplicity p n)"
by (subst prime_factorization_nat) (simp_all add: prod power)

end

locale completely_multiplicative_function' =
completely_multiplicative_function f for f :: "nat ⇒ 'a :: comm_semiring_1" +
fixes f_prime :: "nat ⇒ 'a"
assumes f_prime: "prime p ⟹ f p = f_prime p"
begin

lemma prod_prime_factors'': "n > 0 ⟹ f n = (∏p∈prime_factors n. f_prime p ^ multiplicity p n)"
by (subst prod_prime_factors') (auto simp: f_prime prime_factors_multiplicity intro!: prod.cong)

lemma efficient_code_aux:
assumes "n > 0" "set ps = (λp. (p, multiplicity p n - 1)) ` prime_factors n" "distinct ps"
shows   "f n = (∏(p,d) ← ps. f_prime p ^ Suc d)"
proof -
from assms have
"(∏(p,d) ← ps. f_prime p ^ Suc d) =
(∏(p,d)∈(λp. (p, multiplicity p n - 1)) ` prime_factors n. f_prime p ^ Suc d)"
by (subst prod.distinct_set_conv_list [symmetric]) simp_all
also have "… = (∏x∈prime_factors n. f_prime x ^ multiplicity x n)"
by (subst prod.reindex) (auto simp: inj_on_def prime_factors_multiplicity
simp del: power_Suc intro!: prod.cong)
also have "… = f n" by (rule prod_prime_factors'' [symmetric]) fact+
finally show ?thesis ..
qed

lemma efficient_code:
assumes "set (ps ()) = (λp. (p, multiplicity p n - 1)) ` prime_factors n" "distinct (ps ())"
shows   "f n = (if n = 0 then 0 else (∏(p,d) ← ps (). f_prime p ^ Suc d))"
using efficient_code_aux[of n "ps ()"] assms by simp

end

lemma multiplicative_function_eqI:
assumes "multiplicative_function f" "multiplicative_function g"
assumes "⋀p k. prime p ⟹ k > 0 ⟹ f (p ^ k) = g (p ^ k)"
shows   "f n = g n"
proof -
interpret f: multiplicative_function f by fact
interpret g: multiplicative_function g by fact
show ?thesis
proof (cases "n > 0")
case True
thus ?thesis
using f.prod_prime_factors[OF True] g.prod_prime_factors[OF True]
by (auto intro!: prod.cong assms simp: prime_factors_multiplicity)
qed simp_all
qed

lemma multiplicative_function_of_natI:
"multiplicative_function f ⟹ multiplicative_function (λn. of_nat (f n))"
unfolding multiplicative_function_def by auto

lemma multiplicative_function_of_natD:
"multiplicative_function (λn. of_nat (f n) :: 'a :: {ring_char_0, comm_semiring_1}) ⟹
multiplicative_function f"
unfolding multiplicative_function_def
by (auto simp: of_nat_mult [symmetric] of_nat_eq_1_iff simp del: of_nat_mult)

lemma multiplicative_function_mult:
assumes "multiplicative_function f"  "multiplicative_function g"
shows   "multiplicative_function (λn. f n * g n)"
proof
interpret f: multiplicative_function f by fact
interpret g: multiplicative_function g by fact
show "f 0 * g 0 = 0" "f 1 * g 1 = 1" by simp_all
fix a b :: nat assume "a > 1" "b > 1" "coprime a b"
thus "f (a * b) * g (a * b) = (f a * g a) * (f b * g b)"
by (simp_all add: f.mult_coprime g.mult_coprime mult_ac)
qed

lemma multiplicative_function_inverse:
fixes f :: "nat ⇒ 'a :: field"
assumes "multiplicative_function f"
shows   "multiplicative_function (λn. inverse (f n))"
proof
interpret f: multiplicative_function f by fact
show "inverse (f 0) = 0" "inverse (f 1) = 1" by simp_all
fix a b :: nat assume "a > 1" "b > 1" "coprime a b"
thus "inverse (f (a * b)) = inverse (f a) * inverse (f b)"
qed

lemma multiplicative_function_divide:
fixes f :: "nat ⇒ 'a :: field"
assumes "multiplicative_function f"  "multiplicative_function g"
shows   "multiplicative_function (λn. f n / g n)"
proof -
have "multiplicative_function (λn. f n * inverse (g n))"
by (intro multiplicative_function_mult multiplicative_function_inverse assms)
also have "(λn. f n * inverse (g n)) = (λn. f n / g n)"
finally show ?thesis .
qed

lemma completely_multiplicative_function_mult:
assumes "completely_multiplicative_function f" "completely_multiplicative_function g"
shows   "completely_multiplicative_function (λn. f n * g n)"
proof
interpret f: completely_multiplicative_function f by fact
interpret g: completely_multiplicative_function g by fact
show "f 0 * g 0 = 0" "f (Suc 0) * g (Suc 0) = 1" by simp_all
fix a b :: nat assume "a > 1" "b > 1"
thus "f (a * b) * g (a * b) = (f a * g a) * (f b * g b)"
by (simp_all add: f.mult g.mult mult_ac)
qed

lemma completely_multiplicative_function_inverse:
fixes f :: "nat ⇒ 'a :: field"
assumes "completely_multiplicative_function f"
shows   "completely_multiplicative_function (λn. inverse (f n))"
proof
interpret f: completely_multiplicative_function f by fact
show "inverse (f 0) = 0" "inverse (f (Suc 0)) = 1" by simp_all
fix a b :: nat assume "a > 1" "b > 1"
thus "inverse (f (a * b)) = inverse (f a) * inverse (f b)"
qed

lemma completely_multiplicative_function_divide:
fixes f :: "nat ⇒ 'a :: field"
assumes "completely_multiplicative_function f"  "completely_multiplicative_function g"
shows   "completely_multiplicative_function (λn. f n / g n)"
proof -
have "completely_multiplicative_function (λn. f n * inverse (g n))"
by (intro completely_multiplicative_function_mult
completely_multiplicative_function_inverse assms)
also have "(λn. f n * inverse (g n)) = (λn. f n / g n)"
finally show ?thesis .
qed

lemma (in multiplicative_function) completely_multiplicativeI:
assumes "⋀p k. prime p ⟹ k > 0 ⟹ f (p ^ k) = f p ^ k"
shows   "completely_multiplicative_function f"
proof
fix m n :: nat assume mn: "m > 1" "n > 1"
define P where "P = prime_factors (m * n)"
have "f (m * n) = (∏p∈P. f (p ^ multiplicity p (m * n)))"
using mn by (subst prod_prime_factors) (auto simp: P_def)
also have "… = (∏p∈P. f p ^ multiplicity p (m * n))"
by (intro prod.cong) (auto simp: assms prime_factors_multiplicity P_def)
also have "… = (∏p∈P. f p ^ multiplicity p m * f p ^ multiplicity p n)"
by (intro prod.cong refl, subst prime_elem_multiplicity_mult_distrib)
(use mn in ‹auto simp: P_def prime_factors_multiplicity power_add›)
also have "… = (∏p∈P. f p ^ multiplicity p m) * (∏p∈P. f p ^ multiplicity p n)"
by (rule prod.distrib)
also have "(∏p∈P. f p ^ multiplicity p m) = (∏p∈prime_factors m. f p ^ multiplicity p m)"
unfolding P_def by (intro prod.mono_neutral_right dvd_prime_factors finite_set_mset)
(use mn in ‹auto simp: prime_factors_multiplicity›)
also have "… = (∏p∈prime_factors m. f (p ^ multiplicity p m))"
by (intro prod.cong) (auto simp: assms prime_factors_multiplicity)
also have "… = f m"
using mn by (intro prod_prime_factors [symmetric]) auto
also have "(∏p∈P. f p ^ multiplicity p n) = (∏p∈prime_factors n. f p ^ multiplicity p n)"
unfolding P_def by (intro prod.mono_neutral_right dvd_prime_factors finite_set_mset)
(use mn in ‹auto simp: prime_factors_multiplicity›)
also have "… = (∏p∈prime_factors n. f (p ^ multiplicity p n))"
by (intro prod.cong) (auto simp: assms prime_factors_multiplicity)
also have "… = f n"
using mn by (intro prod_prime_factors [symmetric]) auto
finally show "f (m * n) = f m * f n" .
qed auto

subsection ‹Indicator function›

definition ind :: "(nat ⇒ bool) ⇒ nat ⇒ 'a :: semiring_1" where
"ind P n = (if n > 0 ∧ P n then 1 else 0)"

lemma ind_0 [simp]: "ind P 0 = 0" by (simp add: ind_def)

lemma ind_nonzero: "n > 0 ⟹ ind P n = (if P n then 1 else 0)"

lemma ind_True [simp]: "P n ⟹ n > 0 ⟹ ind P n = 1"

lemma ind_False [simp]: "¬P n ⟹ n > 0 ⟹ ind P n = 0"

lemma ind_eq_1_iff: "ind P n = 1 ⟷ n > 0 ∧ P n"