Theory Gauss_Sums_Auxiliary

(*
File:     Gauss_Sums_Auxiliary.thy
Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM
*)
section ‹Auxiliary material›
theory Gauss_Sums_Auxiliary
imports
Dirichlet_L.Dirichlet_Characters
Dirichlet_Series.Moebius_Mu
Dirichlet_Series.More_Totient
begin

subsection ‹Various facts›

lemma sum_div_reduce:
fixes d :: nat and f :: "nat ⇒ complex"
assumes "d dvd k" "d > 0"
shows "(∑n | n ∈ {1..k} ∧ d dvd n. f n) = (∑c ∈ {1..k div d}. f (c*d))"
by (rule sum.reindex_bij_witness[of _ "λk. k * d" "λk. k div d"])
(use assms in ‹fastforce simp: div_le_mono›)+

lemma prod_div_sub:
fixes f :: "nat ⇒ complex"
assumes "finite A" "B ⊆ A" "∀b ∈ B. f b ≠ 0"
shows "(∏ i ∈ A - B. f i) = ((∏ i ∈ A. f i) div (∏ i ∈ B. f i))"
using assms
proof (induction "card B" arbitrary: B)
case 0
then show ?case
using infinite_super by fastforce
next
case (Suc n)
then show ?case
proof -
obtain B' x where decomp: "B = B' ∪ {x} ∧ x ∉ B'"
using card_eq_SucD[OF Suc(2)[symmetric]] insert_is_Un by auto
then have B'card: "card B' = n" using Suc(2)
using Suc.prems(2) assms(1) finite_subset by fastforce
have "prod f (A - B) = prod f ((A-B') - {x})"
also have "… = (prod f (A-B')) div f x"
using prod_diff1[of "A-B'" f x] Suc decomp by auto
also have "… = (prod f A div prod f B') div f x"
using Suc(1)[of B'] Suc(3) B'card decomp
Suc.prems(2) Suc.prems(3) by force
also have "… = prod f A div (prod f B' * f x)" by auto
also have "… = prod f A div prod f B"
using decomp Suc.prems(2) assms(1) finite_subset by fastforce
finally show ?thesis by blast
qed
qed

lemma linear_gcd:
fixes a b c d :: nat
assumes "a > 0" "b > 0" "c > 0" "d > 0"
assumes "coprime a c" "coprime b d"
shows "gcd (a*b) (c*d) = (gcd a d) * (gcd b c)"
using assms
proof -
define q1 :: nat where "q1 = a div gcd a d"
define q2 :: nat where "q2 = c div gcd b c"
define q3 :: nat where "q3 = b div gcd b c"
define q4 :: nat where "q4 = d div gcd a d"

have "coprime q1 q2" "coprime q3 q4"
unfolding q1_def q2_def q3_def q4_def
proof -
have "coprime (a div gcd a d) c"
using ‹coprime a c› coprime_mult_left_iff[of "a div gcd a d" "gcd a d" c]
dvd_mult_div_cancel[OF gcd_dvd1, of a b] by simp
then show "coprime (a div gcd a d) (c div gcd b c)"
using coprime_mult_right_iff[of "a div gcd a d" "gcd b c" "c div gcd b c"]
dvd_div_mult_self[OF gcd_dvd2[of b c]] by auto
have "coprime (b div gcd b c) d"
using ‹coprime b d› coprime_mult_left_iff[of "b div gcd b c" "gcd b c" d]
dvd_mult_div_cancel[OF gcd_dvd1, of a b] by simp
then show "coprime (b div gcd b c) (d div gcd a d)"
using coprime_mult_right_iff[of "b div gcd b c" "gcd a d" "d div gcd a d"]
dvd_div_mult_self[OF gcd_dvd2[of b c]] by auto
qed
moreover have "coprime q1 q4" "coprime q3 q2"
unfolding q1_def q2_def q3_def q4_def
using assms div_gcd_coprime by blast+
ultimately have 1: "coprime (q1*q3) (q2*q4)"
by simp
have "gcd (a*b) (c*d) = (gcd a d) * (gcd b c) * gcd (q1*q3) (q2*q4)"
unfolding q1_def q2_def q3_def q4_def
by (subst gcd_mult_distrib_nat[of "gcd a d * gcd b c"],
from this 1 show "gcd (a*b) (c*d) = (gcd a d) * (gcd b c)" by auto
qed

lemma reindex_product_bij:
fixes a b m k :: nat
defines "S ≡ {(d1,d2). d1 dvd gcd a m ∧ d2 dvd gcd k b}"
defines "T ≡ {d. d dvd (gcd a m) * (gcd k b)}"
defines "f ≡ (λ(d1,d2). d1 * d2)"
assumes "coprime a k"
shows "bij_betw f S T"
unfolding bij_betw_def
proof
show inj: "inj_on f S"
unfolding f_def
proof -
{fix d1 d2 d1' d2'
assume "(d1,d2) ∈ S" "(d1',d2') ∈ S"
then have dvd: "d1 dvd gcd a m" "d2 dvd gcd k b"
"d1' dvd gcd a m" "d2' dvd gcd k b"
unfolding S_def by simp+
assume "f (d1,d2) = f (d1',d2')"
then have eq: "d1 * d2 = d1' * d2'"
unfolding f_def by simp
from eq dvd have eq1: "d1 = d1'"
by (simp,meson assms coprime_crossproduct_nat coprime_divisors)
from eq dvd have eq2: "d2 = d2'"
using assms(4) eq1 by auto
from eq1 eq2 have "d1 = d1' ∧ d2 = d2'" by simp}
then show "inj_on (λ(d1, d2). d1 * d2) S"
using S_def f_def by (intro inj_onI,blast)
qed
show surj: "f  S = T"
proof -
{fix d
have "d dvd (gcd a m) * (gcd k b)
⟷ (∃d1 d2. d = d1*d2 ∧ d1 dvd gcd a m ∧ d2 dvd gcd k b)"
using division_decomp mult_dvd_mono by blast}
then show ?thesis
unfolding f_def S_def T_def image_def
by auto
qed
qed

lemma p_div_set:
shows "{p. p ∈prime_factors a ∧ ¬ p dvd N} =
({p. p ∈prime_factors (a*N)} - {p. p ∈prime_factors N})"
(is "?A = ?B")
proof
show "?A ⊆ ?B"
proof (simp)
{ fix p
assume as: "p ∈# prime_factorization a" "¬ p dvd N"
then have 1: "p ∈ prime_factors (a * N)"
proof -
from in_prime_factors_iff[of p a] as
have "a ≠ 0" "p dvd a" "prime p" by simp+
have "N ≠ 0" using ‹¬ p dvd N› by blast
have "a * N ≠ 0" using ‹a ≠ 0› ‹N ≠ 0› by auto
have "p dvd a*N" using ‹p dvd a› by simp
show ?thesis
using ‹a*N ≠ 0› ‹p dvd a*N› ‹prime p› in_prime_factors_iff by blast
qed
from as have 2: "p ∉ prime_factors N" by blast
from 1 2 have "p ∈ prime_factors (a * N) - prime_factors N"
by blast
}
then show "{p. p ∈# prime_factorization a ∧ ¬ p dvd N}
⊆ prime_factors (a * N) - prime_factors N" by blast
qed

show "?B ⊆ ?A"
proof (simp)
{ fix p
assume as: "p ∈ prime_factors (a * N) - prime_factors N"
then have 1: "¬ p dvd N"
proof -
from as have "p ∈ prime_factors (a * N)" "p ∉ prime_factors N"
using DiffD1 DiffD2 by blast+
then show ?thesis by (simp add: in_prime_factors_iff)
qed
have 2: "p ∈# prime_factorization a"
proof -
have "p dvd (a*N)" "prime p" "a*N ≠ 0" using in_prime_factors_iff as by blast+
have "p dvd a" using ‹¬ p dvd N› prime_dvd_multD[OF ‹prime p› ‹p dvd (a*N)›] by blast
have "a ≠ 0" using ‹a*N ≠ 0› by simp
show ?thesis using in_prime_factors_iff ‹a ≠ 0› ‹p dvd a› ‹prime p› by blast
qed
from 1 2 have "p ∈ {p. p ∈# prime_factorization a ∧ ¬ p dvd N}" by blast
}
then show "prime_factors (a * N) - prime_factors N
⊆ {p. p ∈# prime_factorization a ∧ ¬ p dvd N}" by blast
qed
qed

lemma coprime_iff_prime_factors_disjoint:
fixes x y :: "'a :: factorial_semiring"
assumes "x ≠ 0" "y ≠ 0"
shows "coprime x y ⟷ prime_factors x ∩ prime_factors y = {}"
proof
assume "coprime x y"
have False if "p ∈ prime_factors x" "p ∈ prime_factors y" for p
proof -
from that assms have "p dvd x" "p dvd y"
by (auto simp: prime_factors_dvd)
with ‹coprime x y› have "p dvd 1"
using coprime_common_divisor by auto
with that assms show False by (auto simp: prime_factors_dvd)
qed
thus "prime_factors x ∩ prime_factors y = {}" by auto
next
assume disjoint: "prime_factors x ∩ prime_factors y = {}"
show "coprime x y"
proof (rule coprimeI)
fix d assume d: "d dvd x" "d dvd y"
show "is_unit d"
proof (rule ccontr)
assume "¬is_unit d"
moreover from this and d assms have "d ≠ 0" by auto
ultimately obtain p where p: "prime p" "p dvd d"
using prime_divisor_exists by auto
with d and assms have "p ∈ prime_factors x ∩ prime_factors y"
by (auto simp: prime_factors_dvd)
with disjoint show False by auto
qed
qed
qed

lemma coprime_cong_prime_factors:
fixes x y :: "'a :: factorial_semiring_gcd"
assumes "x ≠ 0" "y ≠ 0" "x' ≠ 0" "y' ≠ 0"
assumes "prime_factors x = prime_factors x'"
assumes "prime_factors y = prime_factors y'"
shows   "coprime x y ⟷ coprime x' y'"
using assms by (simp add: coprime_iff_prime_factors_disjoint)

lemma moebius_prod_not_coprime:
assumes "¬ coprime N d"
shows "moebius_mu (N*d) = 0"
proof -
from assms obtain l where l_form: "l dvd N ∧ l dvd d ∧ ¬ is_unit l"
unfolding coprime_def by blast
then have "l * l dvd N * d" using mult_dvd_mono by auto
then have "l⇧2 dvd N*d" by (subst power2_eq_square,blast)
then have "¬ squarefree (N*d)"
unfolding squarefree_def coprime_def using l_form by blast
then show "moebius_mu (N*d) = 0"
using moebius_mu_def by auto
qed

text‹Theorem 2.18›

(* TODO Place in corresponding theory *)
lemma sum_divisors_moebius_mu_times_multiplicative:
fixes f :: "nat ⇒ 'a :: {comm_ring_1}"
assumes "multiplicative_function f" and "n > 0"
shows   "(∑d | d dvd n. moebius_mu d * f d) = (∏p∈prime_factors n. 1 - f p)"
proof -
define g where "g = (λn. ∑d | d dvd n. moebius_mu d * f d)"
define g' where "g' = dirichlet_prod (λn. moebius_mu n * f n) (λn. if n = 0 then 0 else 1)"
interpret f: multiplicative_function f by fact
have "multiplicative_function (λn. if n = 0 then 0 else 1 :: 'a)"
by standard auto
interpret multiplicative_function g' unfolding g'_def
by (intro multiplicative_dirichlet_prod multiplicative_function_mult
moebius_mu.multiplicative_function_axioms assms) fact+

have g'_primepow: "g' (p ^ k) = 1 - f p" if "prime p" "k > 0" for p k
proof -
have "g' (p ^ k) = (∑i≤k. moebius_mu (p ^ i) * f (p ^ i))"
using that by (simp add: g'_def dirichlet_prod_prime_power)
also have "… = (∑i∈{0, 1}. moebius_mu (p ^ i) * f (p ^ i))"
using that by (intro sum.mono_neutral_right) (auto simp: moebius_mu_power')
also have "… = 1 - f p"
using that by (simp add: moebius_mu.prime)
finally show ?thesis .
qed

have "g' n = g n"
by (simp add: g_def g'_def dirichlet_prod_def)
also from assms have "g' n = (∏p∈prime_factors n. g' (p ^ multiplicity p n))"
by (intro prod_prime_factors) auto
also have "… = (∏p∈prime_factors n. 1 - f p)"
by (intro prod.cong) (auto simp: g'_primepow prime_factors_multiplicity)
finally show ?thesis by (simp add: g_def)
qed

lemma multiplicative_ind_coprime [intro]: "multiplicative_function (ind (coprime N))"
by (intro multiplicative_function_ind) auto

lemma sum_divisors_moebius_mu_times_multiplicative_revisited:
fixes f :: "nat ⇒ 'a :: {comm_ring_1}"
assumes "multiplicative_function f" "n > 0" "N > 0"
shows   "(∑d | d dvd n ∧ coprime N d. moebius_mu d * f d) =
(∏p∈{p. p ∈ prime_factors n ∧ ¬ (p dvd N)}. 1 - f p)"
proof -
have "(∑d | d dvd n ∧ coprime N d. moebius_mu d * f d) =
(∑d | d dvd n. moebius_mu d * (ind (coprime N) d * f d))"
using assms by (intro sum.mono_neutral_cong_left) (auto simp: ind_def)
also have "… = (∏p∈prime_factors n. 1 - ind (coprime N) p * f p)"
using assms by (intro sum_divisors_moebius_mu_times_multiplicative)
(auto intro: multiplicative_function_mult)
also from assms have "… = (∏p | p ∈ prime_factors n ∧ ¬(p dvd N). 1 - f p)"
by (intro prod.mono_neutral_cong_right)
(auto simp: ind_def prime_factors_dvd coprime_commute dest: prime_imp_coprime)
finally show ?thesis .
qed

subsection ‹Neutral element of the Dirichlet product›

definition "dirichlet_prod_neutral n = (if n = 1 then 1 else 0)" for n :: nat

lemma dirichlet_prod_neutral_intro:
fixes S :: "nat ⇒ complex" and f :: "nat ⇒ nat ⇒ complex"
defines "S ≡ (λ(n::nat). (∑k | k ∈ {1..n} ∧ coprime k n. (f k n)))"
shows "S(n) = (∑k ∈ {1..n}. f k n * dirichlet_prod_neutral (gcd k n))"
proof -
let ?g = "λk. (f k n)* (dirichlet_prod_neutral (gcd k n))"
have zeros: "∀k ∈ {1..n} - {k. k ∈ {1..n} ∧ coprime k n}. ?g k = 0"
proof
fix k
assume "k ∈ {1..n} - {k ∈ {1..n}. coprime k n}"
then show "(f k n) * dirichlet_prod_neutral (gcd k n) = 0"
by (simp add: dirichlet_prod_neutral_def[of "gcd k n"] split: if_splits,presburger)
qed

have "S n = (∑k | k ∈ {1..n} ∧ coprime k n. (f k n))"
also have "… = sum ?g {k. k ∈ {1..n} ∧ coprime k n}"
by (simp add: dirichlet_prod_neutral_def split: if_splits)
also have "… = sum ?g {1..n}"
by (intro sum.mono_neutral_left, auto simp add: zeros)
finally show ?thesis by blast
qed

lemma dirichlet_prod_neutral_right_neutral:
"dirichlet_prod f dirichlet_prod_neutral n = f n " if "n > 0" for f :: "nat ⇒ complex" and n
proof -
{fix d :: nat
assume "d dvd n"
then have eq: "n = d ⟷ n div d = 1"
using div_self that dvd_mult_div_cancel by force
have "f(d)*dirichlet_prod_neutral(n div d) = (if n = d then f(d) else 0)"
note summand = this

have "dirichlet_prod f dirichlet_prod_neutral n =
(∑d | d dvd n. f(d)*dirichlet_prod_neutral(n div d))"
unfolding dirichlet_prod_def by blast
also have "… = (∑d | d dvd n. (if n = d then f(d) else 0))"
using summand by simp
also have "… = (∑d | d = n. (if n = d then f(d) else 0))"
using that by (intro sum.mono_neutral_right, auto)
also have "… = f(n)"  by simp
finally show ?thesis by simp
qed

lemma dirichlet_prod_neutral_left_neutral:
"dirichlet_prod dirichlet_prod_neutral f n = f n "
if "n > 0" for f :: "nat ⇒ complex" and n
using dirichlet_prod_neutral_right_neutral[OF that, of f]
dirichlet_prod_commutes[of f dirichlet_prod_neutral]
by argo

corollary I_right_neutral_0:
fixes f :: "nat ⇒ complex"
assumes "f 0 = 0"
shows "dirichlet_prod f dirichlet_prod_neutral n = f n"
using assms dirichlet_prod_neutral_right_neutral by (cases n, simp, blast)

subsection ‹Multiplicative functions›

lemma mult_id: "multiplicative_function id"

lemma mult_moebius: "multiplicative_function moebius_mu"
using Moebius_Mu.moebius_mu.multiplicative_function_axioms
by simp

lemma mult_of_nat: "multiplicative_function of_nat"
using multiplicative_function_def of_nat_0 of_nat_1 of_nat_mult by blast

lemma mult_of_nat_c: "completely_multiplicative_function of_nat"

lemma completely_multiplicative_nonzero:
fixes f :: "nat ⇒ complex"
assumes "completely_multiplicative_function f"
"d ≠ 0"
"⋀p. prime p ⟹ f(p) ≠ 0"
shows "f(d) ≠ 0"
using assms(2)
proof (induction d rule: nat_less_induct)
case (1 n)
then show ?case
proof (cases "n = 1")
case True
then show ?thesis
using assms(1)
unfolding completely_multiplicative_function_def by simp
next
case False
then obtain p where 2:"prime p ∧ p dvd n"
using prime_factor_nat by blast
then obtain a where 3: "n = p * a"  "a ≠ 0"
using 1 by auto
then have 4: "f(a) ≠ 0" using 1
using 2 prime_nat_iff by fastforce
have 5: "f(p) ≠ 0" using assms(3) 2 by simp
from 3 4 5 show ?thesis
qed
qed

lemma multipl_div:
fixes m k d1 d2 :: nat and f :: "nat ⇒ complex"
assumes "multiplicative_function f" "d1 dvd m" "d2 dvd k" "coprime m k"
shows "f ((m*k) div (d1*d2)) = f(m div d1) * f(k div d2)"
using assms
unfolding multiplicative_function_def
using assms(1) multiplicative_function.mult_coprime by fastforce

lemma multipl_div_mono:
fixes m k d :: nat and f :: "nat ⇒ complex"
assumes "completely_multiplicative_function f"
"d dvd k" "d > 0"
"⋀p. prime p ⟹ f(p) ≠ 0"
shows "f (k div d) = f(k) div f(d)"
proof -
have "d ≠ 0" using assms(2,3) by auto
then have nz: "f(d) ≠ 0" using assms(1,4) completely_multiplicative_nonzero by simp

from assms(2,3) obtain a where div: "k = a * d " by fastforce
have "f (k div d) = f ((a*d) div d)" using div by simp
also have "… = f(a)" using assms(3) div by simp
also have "… = f(a)*f(d) div f(d)" using nz by auto
also have "… = f(a*d) div f(d)"
by (simp add: div assms(1) completely_multiplicative_function.mult)
also have "… = f (k) div f(d)" using div by simp
finally show ?thesis by simp
qed

lemma comp_to_mult: "completely_multiplicative_function f ⟹
multiplicative_function f"
unfolding completely_multiplicative_function_def
multiplicative_function_def by auto

end

Theory Periodic_Arithmetic

(*
File:     Periodic_Arithmetic.thy
Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM

Periodic arithmetic functions
*)
section ‹Periodic arithmetic functions›
theory Periodic_Arithmetic
imports
Complex_Main
"HOL-Number_Theory.Cong"
begin

definition
"periodic_arithmetic f k = (∀n. f (n+k) = f n)"
for n :: int and k :: nat and f :: "nat ⇒ complex"

lemma const_periodic_arithmetic: "periodic_arithmetic (λx. y) k"
unfolding periodic_arithmetic_def by blast

fixes f g :: "nat ⇒ complex"
assumes "periodic_arithmetic f k"
assumes "periodic_arithmetic g k"
shows "periodic_arithmetic (λn. f n + g n) k"
using assms unfolding periodic_arithmetic_def by simp

lemma mult_periodic_arithmetic:
fixes f g :: "nat ⇒ complex"
assumes "periodic_arithmetic f k"
assumes "periodic_arithmetic g k"
shows "periodic_arithmetic (λn. f n * g n) k"
using assms unfolding periodic_arithmetic_def  by simp

lemma scalar_mult_periodic_arithmetic:
fixes f :: "nat ⇒ complex" and a :: complex
assumes "periodic_arithmetic f k"
shows "periodic_arithmetic (λn. a * f n) k"
using mult_periodic_arithmetic[OF const_periodic_arithmetic[of a k] assms(1)] by simp

lemma fin_sum_periodic_arithmetic_set:
fixes f g :: "nat ⇒ complex"
assumes "∀i∈A. periodic_arithmetic (h i) k"
shows "periodic_arithmetic (λn. ∑i ∈ A. h i n) k"
using assms by (simp add: periodic_arithmetic_def)

lemma mult_period:
assumes "periodic_arithmetic g k"
shows "periodic_arithmetic g (k*q)"
using assms
proof (induction q)
case 0 then show ?case unfolding periodic_arithmetic_def by simp
next
case (Suc m)
then show ?case
unfolding periodic_arithmetic_def
proof -
{ fix n
have "g (n + k * Suc m) = g (n + k +  k * m)"
also have "… = g(n)"
using Suc.IH[OF Suc.prems] assms
unfolding periodic_arithmetic_def by simp
finally have "g (n + k * Suc m) = g(n)" by blast
}
then show "∀n. g (n + k * Suc m) = g n" by auto
qed
qed

lemma unique_periodic_arithmetic_extension:
assumes "k > 0"
assumes "∀j<k. g j = h j"
assumes "periodic_arithmetic g k" and "periodic_arithmetic h k"
shows "g i = h i"
proof (cases "i < k")
case True then show ?thesis using assms by simp
next
case False then show ?thesis
proof -
have "k * (i div k) + (i mod k) = i ∧ (i mod k) < k"
then obtain q r where euclid_div: "k*q + r = i ∧ r < k"
using mult.commute by blast
from assms(3) assms(4)
have  "periodic_arithmetic g (k*q)" "periodic_arithmetic h (k*q)"
using mult_period by simp+
have "g(k*q+r) = g(r)"
using ‹periodic_arithmetic g (k*q)› unfolding periodic_arithmetic_def
using add.commute[of "k*q" r] by presburger
also have "… = h(r)"
using euclid_div assms(2) by simp
also have "… = h(k*q+r)"
using ‹periodic_arithmetic h (k*q)› add.commute[of "k*q" r]
unfolding periodic_arithmetic_def by presburger
also have "… = h(i)" using euclid_div by simp
finally show "g(i) = h(i)" using euclid_div by simp
qed
qed

lemma periodic_arithmetic_sum_periodic_arithmetic:
assumes "periodic_arithmetic f k"
shows "(∑l ∈ {m..n}. f l) = (∑l ∈ {m+k..n+k}. f l)"
using periodic_arithmetic_def assms
by (intro sum.reindex_bij_witness
[of "{m..n}" "λl. l-k" "λl. l+k" "{m+k..n+k}" f f])
auto

lemma mod_periodic_arithmetic:
fixes n m :: nat
assumes "periodic_arithmetic f k"
assumes "n mod k = m mod k"
shows "f n = f m"
proof -
obtain q where 1: "n = q*k+(n mod k)"
using div_mult_mod_eq[of n k,symmetric] by blast
obtain q' where 2: "m = q'*k+(m mod k)"
using div_mult_mod_eq[of m k,symmetric] by blast
from 1 have "f n = f (q*k+(n mod k))" by auto
also have "… = f (n mod k)"
using mult_period[of f k q] assms(1) periodic_arithmetic_def[of f "k*q"]
also have "… = f (m mod k)" using assms(2) by auto
also have "… = f (q'*k+(m mod k))"
using mult_period[of f k q'] assms(1) periodic_arithmetic_def[of f "k*q'"]
also have "… = f m" using 2 by auto
finally show "f n = f m" by simp
qed

lemma cong_periodic_arithmetic:
assumes "periodic_arithmetic f k" "[a = b] (mod k)"
shows   "f a = f b"
using assms mod_periodic_arithmetic[of f k a b] by (auto simp: cong_def)

lemma cong_nat_imp_eq:
fixes m :: nat
assumes "m > 0" "x ∈ {a..<a+m}" "y ∈ {a..<a+m}" "[x = y] (mod m)"
shows   "x = y"
using assms
proof (induction x y rule: linorder_wlog)
case (le x y)
have "[y - x = 0] (mod m)"
using cong_diff_iff_cong_0_nat cong_sym le by blast
thus "x = y"
using le by (auto simp: cong_def)
qed (auto simp: cong_sym)

lemma inj_on_mod_nat:
fixes m :: nat
assumes "m > 0"
shows   "inj_on (λx. x mod m) {a..<a+m}"
proof
fix x y assume xy: "x ∈ {a..<a+m}" "y ∈ {a..<a+m}" and eq: "x mod m = y mod m"
from ‹m > 0› and xy show "x = y"
by (rule cong_nat_imp_eq) (use eq in ‹simp_all add: cong_def›)
qed

lemma bij_betw_mod_nat_atLeastLessThan:
fixes k d :: nat
assumes "k > 0"
defines "g ≡ (λi. nat ((int i - int d) mod int k) + d)"
shows   "bij_betw (λi. i mod k) {d..<d+k} {..<k}"
unfolding bij_betw_def
proof
show inj: "inj_on (λi. i mod k) {d..<d + k}"
by (rule inj_on_mod_nat) fact+
have "(λi. i mod k)  {d..<d + k} ⊆ {..<k}"
by auto
moreover have "card ((λi. i mod k)  {d..<d + k}) = card {..<k}"
using inj by (subst card_image) auto
ultimately show "(λi. i mod k)  {d..<d + k} = {..<k}"
by (intro card_subset_eq) auto
qed

lemma periodic_arithmetic_sum_periodic_arithmetic_shift:
fixes k d :: nat
assumes "periodic_arithmetic f k" "k > 0" "d > 0"
shows "(∑l ∈ {0..k-1}. f l) = (∑l ∈ {d..d+k-1}. f l)"
proof -
have "(∑l ∈ {0..k-1}. f l) = (∑l ∈ {0..<k}. f l)"
using assms(2) by (intro sum.cong) auto
also have "… = (∑l ∈ {d..<d+k}. f (l mod k))"
using assms(2)
by (simp add: sum.reindex_bij_betw[OF bij_betw_mod_nat_atLeastLessThan[of k d]]
lessThan_atLeast0)
also have "… = (∑l ∈ {d..<d+k}. f l)"
using mod_periodic_arithmetic[of f k] assms(1) sum.cong
by (meson mod_mod_trivial)
also have "… = (∑l ∈ {d..d+k-1}. f l)"
using assms(2,3) by (intro sum.cong) auto
finally show ?thesis by auto
qed

lemma self_bij_0_k:
fixes a k :: nat
assumes "coprime a k" "[a*i = 1] (mod k)" "k > 0"
shows "bij_betw (λr. r*a mod k) {0..k-1} {0..k-1}"
unfolding bij_betw_def
proof
show "inj_on (λr. r*a mod k) {0..k-1}"
proof -
{fix r1 r2
assume in_k: "r1 ∈ {0..k-1}" "r2 ∈ {0..k-1}"
assume as: "[r1*a = r2*a] (mod k)"
then have "[r1*a*i = r2*a*i] (mod k)"
using cong_scalar_right by blast
then have "[r1 = r2] (mod k)"
using cong_mult_rcancel_nat as assms(1) by simp
then have "r1 = r2" using in_k
using assms(3) cong_less_modulus_unique_nat by auto}
note eq = this
show ?thesis unfolding inj_on_def
by (safe, simp add: eq cong_def)
qed
define f where "f = (λr. r * a mod k)"
show "f  {0..k - 1} = {0..k - 1} "
unfolding image_def
proof (standard)
show "{y. ∃x∈{0..k - 1}. y = f x} ⊆ {0..k - 1}"
proof -
{fix y
assume "y ∈ {y. ∃x∈{0..k - 1}. y = f x}"
then obtain x where "y = f x" by blast
then have "y ∈ {0..k-1}"
unfolding f_def
using Suc_pred assms(3) lessThan_Suc_atMost by fastforce}
then show ?thesis by blast
qed
show "{0..k - 1} ⊆ {y. ∃x∈{0..k - 1}. y = f x}"
proof -
{ fix x
assume ass: "x ∈ {0..k-1}"
then have "x * i mod k ∈ {0..k-1}"
proof -
have "x * i mod k ∈ {0..<k}" by (simp add: assms(3))
have "{0..<k} = {0..k-1}" using Suc_diff_1 assms(3) by auto
show ?thesis using ‹x * i mod k ∈ {0..<k}› ‹{0..<k} = {0..k-1}› by blast
qed
then have "f (x * i mod k) = x"
proof -
have "f (x * i mod k) = (x * i mod k) * a mod k"
unfolding f_def by blast
also have "… = (x*i*a) mod k"
also have "… = (x*1) mod k"
using assms(2)
unfolding cong_def
by (subst mult.assoc, subst (2) mult.commute,
subst mod_mult_right_eq[symmetric],simp)
also have "… = x" using ass assms(3) by auto
finally show ?thesis .
qed
then have "x ∈ {y. ∃x∈{0..k - 1}. y = f x}"
using ‹x * i mod k ∈ {0..k-1}› by force
}
then show ?thesis by blast
qed
qed
qed

lemma periodic_arithmetic_homothecy:
assumes "periodic_arithmetic f k"
shows   "periodic_arithmetic (λl. f (l*a)) k"
unfolding periodic_arithmetic_def
proof
fix n
have "f ((n + k) * a) = f(n*a+k*a)" by (simp add: algebra_simps)
also have "… = f(n*a)"
using mult_period[OF assms] unfolding periodic_arithmetic_def by simp
finally show "f ((n + k) * a) = f (n * a)" by simp
qed

theorem periodic_arithmetic_remove_homothecy:
assumes "coprime a k" "periodic_arithmetic f k" "k > 0"
shows "(∑l=1..k. f l) = (∑l=1..k. f (l*a))"
proof -
obtain i where inv: "[a*i = 1] (mod k)"
using assms(1) coprime_iff_invertible_nat[of a k] by auto
from this self_bij_0_k assms
have bij: "bij_betw (λr. r * a mod k) {0..k - 1} {0..k - 1}" by blast

have "(∑l = 1..k. f(l)) = (∑l = 0..k-1. f(l))"
using periodic_arithmetic_sum_periodic_arithmetic_shift[of f k 1] assms by simp
also have "… = (∑l = 0..k-1. f(l*a mod k))"
using sum.reindex_bij_betw[OF bij,symmetric] by blast
also have "… = (∑l = 0..k-1. f(l*a))"
by (intro sum.cong refl) (use mod_periodic_arithmetic[OF assms(2)] mod_mod_trivial in blast)
also have "… = (∑l = 1..k. f(l*a))"
using periodic_arithmetic_sum_periodic_arithmetic_shift[of "(λl. f(l*a))" k 1]
periodic_arithmetic_homothecy[OF assms(2)] assms(3) by fastforce
finally show ?thesis by blast
qed

end

Theory Complex_Roots_Of_Unity

(*
File:     Complex_Roots_Of_Unity.thy
Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM

Complex roots of unity (exp(2iπ/n)) and sums over them.
*)
theory Complex_Roots_Of_Unity
imports
"HOL-Analysis.Analysis"
Periodic_Arithmetic
begin

section ‹Complex roots of unity›

definition
"unity_root k n = cis (2 * pi * of_int n / of_nat k)"

lemma
unity_root_k_0 [simp]: "unity_root k 0 = 1" and
unity_root_0_n [simp]: "unity_root 0 n = 1"
unfolding unity_root_def by simp+

lemma unity_root_conv_exp:
"unity_root k n = exp (of_real (2*pi*n/k) * 𝗂)"
unfolding unity_root_def
by (subst cis_conv_exp,subst mult.commute,blast)

lemma unity_root_mod:
"unity_root k (n mod int k) = unity_root k n"
proof (cases "k = 0")
case True then show ?thesis by simp
next
case False
obtain q :: int where q_def: "n = q*k + (n mod k)"
using div_mult_mod_eq[symmetric] by blast
have "n / k = q + (n mod k) / k"
proof (auto simp add: divide_simps False)
have "real_of_int n = real_of_int (q*k + (n mod k))"
using q_def by simp
also have "… = real_of_int q * real k + real_of_int (n mod k)"
finally show "real_of_int n = real_of_int q * real k + real_of_int (n mod k)"
by blast
qed
then have "(2*pi*n/k) = 2*pi*q + (2*pi*(n mod k)/k)"
using False by (auto simp add: field_simps)
then have "(2*pi*n/k)*𝗂 = 2*pi*q*𝗂 + (2*pi*(n mod k)/k)*𝗂" (is "?l = ?r1 + ?r2")
then have "exp ?l = exp ?r2"
then show ?thesis
using unity_root_def unity_root_conv_exp by simp
qed

lemma unity_root_cong:
assumes "[m = n] (mod int k)"
shows   "unity_root k m = unity_root k n"
proof -
from assms have "m mod int k = n mod int k"
by (auto simp: cong_def)
hence "unity_root k (m mod int k) = unity_root k (n mod int k)"
by simp
thus ?thesis by (simp add: unity_root_mod)
qed

lemma unity_root_mod_nat:
"unity_root k (nat (n mod int k)) = unity_root k n"
proof (cases k)
case (Suc l)
then have "n mod int k ≥ 0" by auto
show ?thesis
unfolding int_nat_eq
by (simp add: ‹n mod int k ≥ 0› unity_root_mod)
qed auto

lemma unity_root_eqD:
assumes gr: "k > 0"
assumes eq: "unity_root k i = unity_root k j"
shows "i mod k = j mod k"
proof -
let ?arg1 = "(2*pi*i/k)* 𝗂"
let ?arg2 = "(2*pi*j/k)* 𝗂"
from eq unity_root_conv_exp have "exp ?arg1 = exp ?arg2" by simp
from this exp_eq
obtain n :: int where "?arg1 = ?arg2 +(2*n*pi)*𝗂" by blast
then have e1: "?arg1 - ?arg2 = 2*n*pi*𝗂" by simp
have e2: "?arg1 - ?arg2 = 2*(i-j)*(1/k)*pi*𝗂"
from e1 e2 have "2*n*pi*𝗂 = 2*(i-j)*(1/k)*pi*𝗂" by simp
then have "2*n*k*pi*𝗂 = 2*(i-j)*pi*𝗂"
then have "2*n*k = 2*(i-j)"
by (meson complex_i_not_zero mult_cancel_right of_int_eq_iff of_real_eq_iff pi_neq_zero)
then have "n*k = i-j" by auto
then show ?thesis by Groebner_Basis.algebra
qed

lemma unity_root_eq_1_iff:
fixes k n :: nat
assumes "k > 0"
shows "unity_root k n = 1 ⟷ k dvd n"
proof -
have "unity_root k n = exp ((2*pi*n/k) * 𝗂)"
also have "exp ((2*pi*n/k)* 𝗂) = 1 ⟷ k dvd n"
using complex_root_unity_eq_1[of k n] assms
finally show ?thesis by simp
qed

lemma unity_root_pow: "unity_root k n ^ m = unity_root k (n * m)"
using unity_root_def
by (simp add: Complex.DeMoivre mult.commute algebra_split_simps(6))

lemma unity_root_add: "unity_root k (m + n) = unity_root k m * unity_root k n"

lemma unity_root_uminus: "unity_root k (-m) = cnj (unity_root k m)"
unfolding unity_root_conv_exp exp_cnj by simp

lemma inverse_unity_root: "inverse (unity_root k m) = cnj (unity_root k m)"
unfolding unity_root_conv_exp exp_cnj by (simp add: field_simps exp_minus)

lemma unity_root_diff: "unity_root k (m - n) = unity_root k m * cnj (unity_root k n)"

lemma unity_root_eq_1_iff_int:
fixes k :: nat and n :: int
assumes "k > 0"
shows "unity_root k n = 1 ⟷ k dvd n"
proof (cases "n ≥ 0")
case True
obtain n' where "n = int n'"
using zero_le_imp_eq_int[OF True] by blast
then show ?thesis
using unity_root_eq_1_iff[OF ‹k > 0›, of n'] of_nat_dvd_iff by blast
next
case False
then have "-n ≥ 0" by auto
have "unity_root k n = inverse (unity_root k (-n))"
unfolding inverse_unity_root by (simp add: unity_root_uminus)
then have "(unity_root k n = 1) = (unity_root k (-n) = 1)"
by simp
also have "(unity_root k (-n) = 1) = (k dvd (-n))"
using unity_root_eq_1_iff[of k "nat (-n)",OF ‹k > 0›] False
int_dvd_int_iff[of k "nat (-n)"] nat_0_le[OF ‹-n ≥ 0›] by auto
finally show ?thesis by simp
qed

lemma unity_root_eq_1 [simp]: "int k dvd n ⟹ unity_root k n = 1"
by (cases "k = 0") (auto simp: unity_root_eq_1_iff_int)

lemma unity_periodic_arithmetic:
"periodic_arithmetic (unity_root k) k"
unfolding periodic_arithmetic_def
proof
fix n
have "unity_root k (n + k) = unity_root k ((n+k) mod k)"
using unity_root_mod[of k] zmod_int by presburger
also have "unity_root k ((n+k) mod k) = unity_root k n"
using unity_root_mod zmod_int by auto
finally show "unity_root k (n + k) = unity_root k n" by simp
qed

lemma unity_periodic_arithmetic_mult:
"periodic_arithmetic (λn. unity_root k (m * int n)) k"
unfolding periodic_arithmetic_def
proof
fix n
have "unity_root k (m * int (n + k)) =
unity_root k (m*n + m*k)"
also have "… = unity_root k (m*n)"
using unity_root_mod[of k "m * int n"] unity_root_mod[of k "m * int n + m * int k"]
mod_mult_self3 by presburger
finally show "unity_root k (m * int (n + k)) =
unity_root k (m * int n)" by simp
qed

lemma unity_root_periodic_arithmetic_mult_minus:
shows "periodic_arithmetic (λi. unity_root k (-int i*int m)) k"
unfolding periodic_arithmetic_def
proof
fix n
have "unity_root k (-(n + k) * m) = cnj (unity_root k (n*m+k*m))"
also have "… = cnj (unity_root k (n*m))"
using mult_period[of "unity_root k" k m] unity_periodic_arithmetic[of k]
unfolding periodic_arithmetic_def by presburger
also have "… = unity_root k (-n*m)"
finally show "unity_root k (-(n + k) * m) = unity_root k (-n*m)"
by simp
qed

lemma unity_div:
fixes a :: int and d :: nat
assumes "d dvd k"
shows "unity_root k (a*d) = unity_root (k div d) a"
proof -
have 1: "(2*pi*(a*d)/k) = (2*pi*a)/(k div d)"
using Suc_pred assms by (simp add: divide_simps, fastforce)
have "unity_root k (a*d) = exp ((2*pi*(a*d)/k)* 𝗂)"
using unity_root_conv_exp by simp
also have "… = exp (((2*pi*a)/(k div d))* 𝗂)"
using 1 by simp
also have "… = unity_root (k div d) a"
using unity_root_conv_exp by simp
finally show ?thesis by simp
qed

lemma unity_div_num:
assumes "k > 0" "d > 0" "d dvd k"
shows "unity_root k (x * (k div d)) = unity_root d x"
using assms dvd_div_mult_self unity_div by auto

section ‹Geometric sums of roots of unity›

text‹
Apostol calls these geometric sums', which is a bit too generic. We therefore decided
to refer to them as sums of roots of unity'.
›
definition "unity_root_sum k n = (∑m<k. unity_root k (n * of_nat m))"

lemma unity_root_sum_0_left [simp]: "unity_root_sum 0 n = 0" and
unity_root_sum_0_right [simp]: "k > 0 ⟹ unity_root_sum k 0 = k"
unfolding unity_root_sum_def by simp_all

text ‹Theorem 8.1›
theorem unity_root_sum:
fixes k :: nat and n :: int
assumes gr: "k ≥ 1"
shows "k dvd n ⟹ unity_root_sum k n = k"
and "¬k dvd n ⟹ unity_root_sum k n = 0"
proof -
assume dvd: "k dvd n"
let ?x = "unity_root k n"
have unit: "?x = 1" using dvd gr unity_root_eq_1_iff_int by auto
have exp: "?x^m = unity_root k (n*m)" for m using unity_root_pow by simp
have "unity_root_sum k n = (∑m<k. unity_root k (n*m))"
using unity_root_sum_def by simp
also have "… = (∑m<k. ?x^m)" using exp by auto
also have "… = (∑m<k. 1)" using unit by simp
also have "… = k" using gr by (induction k, auto)
finally show "unity_root_sum k n = k" by simp
next
assume dvd: "¬k dvd n"
let ?x = "unity_root k n"
have "?x ≠ 1" using dvd gr unity_root_eq_1_iff_int by auto
have "(?x^k - 1)/(?x - 1) = (∑m<k. ?x^m)"
using geometric_sum[of ?x k, OF ‹?x ≠ 1›] by auto
then have sum: "unity_root_sum k n = (?x^k - 1)/(?x - 1)"
using unity_root_sum_def unity_root_pow by simp
have "?x^k = 1"
using gr unity_root_eq_1_iff_int unity_root_pow by simp
then show "unity_root_sum k n = 0" using sum by auto
qed

corollary unity_root_sum_periodic_arithmetic:
"periodic_arithmetic (unity_root_sum k) k"
unfolding periodic_arithmetic_def
proof
fix n
show "unity_root_sum k (n + k) = unity_root_sum k n"
by (cases "k = 0"; cases "k dvd n") (auto simp add: unity_root_sum)
qed

lemma unity_root_sum_nonzero_iff:
fixes r :: int
assumes "k ≥ 1" and "r ∈ {-k<..<k}"
shows "unity_root_sum k r ≠ 0 ⟷ r = 0"
proof
assume "unity_root_sum k r ≠ 0"
then have "k dvd r" using unity_root_sum assms by blast
then show "r = 0" using assms(2)
using dvd_imp_le_int by force
next
assume "r = 0"
then have "k dvd r" by auto
then have "unity_root_sum k r = k"
using assms(1) unity_root_sum by blast
then show "unity_root_sum k r ≠ 0" using assms(1) by simp
qed

end

Theory Finite_Fourier_Series

(*
File:     Finite_Fourier_Series.thy
Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM

Existence and uniqueness of finite Fourier series for periodic arithmetic functions
*)
section ‹Finite Fourier series›
theory Finite_Fourier_Series
imports
Polynomial_Interpolation.Lagrange_Interpolation
Complex_Roots_Of_Unity
begin

subsection ‹Auxiliary facts›

lemma lagrange_exists:
assumes d: "distinct (map fst zs_ws)"
defines e: "(p :: complex poly) ≡ lagrange_interpolation_poly zs_ws"
shows "degree p ≤ (length zs_ws)-1"
"(∀x y. (x,y) ∈ set zs_ws ⟶ poly p x = y)"
proof -
from e show "degree p ≤ (length zs_ws - 1)"
using degree_lagrange_interpolation_poly by auto
from e d have
"poly p x = y" if "(x,y) ∈ set zs_ws" for x y
using that lagrange_interpolation_poly by auto
then show "(∀x y. (x,y) ∈ set zs_ws ⟶ poly p x = y)"
by auto
qed

lemma lagrange_unique:
assumes o: "length zs_ws > 0" (* implicit in theorem *)
assumes d: "distinct (map fst zs_ws)"
assumes 1: "degree (p1 :: complex poly) ≤ (length zs_ws)-1 ∧
(∀x y. (x,y) ∈ set zs_ws ⟶ poly p1 x = y)"
assumes 2: "degree (p2 :: complex poly) ≤ (length zs_ws)-1 ∧
(∀x y. (x,y) ∈ set zs_ws ⟶ poly p2 x = y)"
shows "p1 = p2"
proof (cases "p1 - p2 = 0")
case True then show ?thesis by simp
next
case False
have "poly (p1-p2) x = 0" if "x ∈ set (map fst zs_ws)" for x
using 1 2 that by (auto simp add: field_simps)
from this d have 3: "card {x. poly (p1-p2) x = 0} ≥ length zs_ws"
proof (induction zs_ws)
case Nil then show ?case by simp
next
case (Cons z_w zs_ws)
from  False poly_roots_finite
have f: "finite {x. poly (p1 - p2) x = 0}" by blast
from Cons have "set (map fst (z_w # zs_ws)) ⊆ {x. poly (p1 - p2) x = 0}"
by auto
then have i: "card (set (map fst (z_w # zs_ws))) ≤ card {x. poly (p1 - p2) x = 0}"
using card_mono f by blast
have "length (z_w # zs_ws) ≤ card (set (map fst (z_w # zs_ws)))"
using Cons.prems(2) distinct_card by fastforce
from this i show ?case by simp
qed
from 1 2 have 4: "degree (p1 - p2) ≤ (length zs_ws)-1"
using degree_diff_le by blast

have "p1 - p2 = 0"
proof (rule ccontr)
assume "p1 - p2 ≠ 0"
then have "card {x. poly (p1-p2) x = 0} ≤ degree (p1-p2)"
using poly_roots_degree by blast
then have "card {x. poly (p1-p2) x = 0} ≤ (length zs_ws)-1"
using 4 by auto
then show "False" using 3 o by linarith
qed
then show ?thesis by simp
qed

text ‹Theorem 8.2›
corollary lagrange:
assumes "length zs_ws > 0" "distinct (map fst zs_ws)"
shows "(∃! (p :: complex poly).
degree p ≤ length zs_ws - 1 ∧
(∀x y. (x, y) ∈ set zs_ws ⟶ poly p x = y))"
using assms lagrange_exists lagrange_unique by blast

lemma poly_altdef':
assumes gr: "k ≥ degree p"
shows "poly p (z::complex) = (∑i≤k. coeff p i * z ^ i)"
proof -
{fix z
have 1: "poly p z = (∑i≤degree p. coeff p i * z ^ i)"
using poly_altdef[of p z] by simp
have "poly p z = (∑i≤k. coeff p i * z ^ i)"
using gr
proof (induction k)
case 0 then show ?case by (simp add: poly_altdef)
next
case (Suc k)
then show ?case
using "1" le_degree not_less_eq_eq by fastforce
qed}
then show ?thesis using gr by blast
qed

subsection ‹Definition and uniqueness›

definition finite_fourier_poly :: "complex list ⇒ complex poly" where
"finite_fourier_poly ws =
(let k = length ws
in  poly_of_list [1 / k * (∑m<k. ws ! m * unity_root k (-n*m)). n ← [0..<k]])"

lemma degree_poly_of_list_le: "degree (poly_of_list ws) ≤ length ws - 1"
by (intro degree_le) (auto simp: nth_default_def)

lemma degree_finite_fourier_poly: "degree (finite_fourier_poly ws) ≤ length ws - 1"
unfolding finite_fourier_poly_def
proof (subst Let_def)
let ?unrolled_list = "
(map (λn. complex_of_real (1 / real (length ws)) *
(∑m<length ws.
ws ! m *
unity_root (length ws) (- int n * int m)))
[0..<length ws])"
have "degree (poly_of_list ?unrolled_list) ≤ length ?unrolled_list - 1"
by (rule degree_poly_of_list_le)
also have "… = length [0..<length ws] - 1"
using length_map by auto
also have "… = length ws - 1" by auto
finally show "degree (poly_of_list ?unrolled_list) ≤ length ws - 1" by blast
qed

lemma coeff_finite_fourier_poly:
assumes "n < length ws"
defines "k ≡ length ws"
shows "coeff (finite_fourier_poly ws) n =
(1/k) * (∑m < k. ws ! m * unity_root k (-n*m))"
using assms degree_finite_fourier_poly
by (auto simp: Let_def nth_default_def finite_fourier_poly_def)

lemma poly_finite_fourier_poly:
fixes m :: int and ws
defines "k ≡ length ws"
assumes "m ∈ {0..<k}"
assumes "m < length ws"
shows "poly (finite_fourier_poly ws) (unity_root k m) = ws ! (nat m)"
proof -
have "k > 0" using assms by auto

have distr: "
(∑j<length ws. ws ! j * unity_root k (-i*j))*(unity_root k (m*i)) =
(∑j<length ws. ws ! j * unity_root k (-i*j)*(unity_root k (m*i)))"
for i
using sum_distrib_right[of "λj. ws ! j * unity_root k (-i*j)"
"{..<k}" "(unity_root k (m*i))"]
using k_def by blast

{fix j i :: nat
have "unity_root k (-i*j)*(unity_root k (m*i)) = unity_root k (-i*j+m*i)"
by (simp add: unity_root_diff unity_root_uminus field_simps)
also have "… = unity_root k (i*(m-j))"
finally have "unity_root k (-i*j)*(unity_root k (m*i)) = unity_root k (i*(m-j))"
by simp
then have "ws ! j * unity_root k (-i*j)*(unity_root k (m*i)) =
ws ! j * unity_root k (i*(m-j))"
by auto
} note prod = this

have zeros:
"(unity_root_sum k (m-j) ≠ 0 ⟷ m = j)
" if "j ≥ 0 ∧ j < k"  for j
using k_def that assms unity_root_sum_nonzero_iff[of _ "m-j"] by simp
then have sum_eq:
"(∑j≤k-1. ws ! j * unity_root_sum k (m-j)) =
(∑j∈{nat m}.  ws ! j * unity_root_sum k (m-j))"
using assms(2) by (intro sum.mono_neutral_right,auto)

have "poly (finite_fourier_poly ws) (unity_root k m) =
(∑i≤k-1. coeff (finite_fourier_poly ws) i * (unity_root k m) ^ i)"
using degree_finite_fourier_poly[of ws] k_def
poly_altdef'[of "finite_fourier_poly ws" "k-1" "unity_root k m"] by blast
also have "… = (∑i<k. coeff (finite_fourier_poly ws) i * (unity_root k m) ^ i)"
using assms(2) by (intro sum.cong) auto
also have "… = (∑i<k. 1 / k *
(∑j<k. ws ! j * unity_root k (-i*j)) * (unity_root k m) ^ i)"
using coeff_finite_fourier_poly[of _ ws] k_def by auto
also have "… = (∑i<k. 1 / k *
(∑j<k. ws ! j * unity_root k (-i*j))*(unity_root k (m*i)))"
using unity_root_pow by auto
also have "… = (∑i<k. 1 / k *
(∑j<k. ws ! j * unity_root k (-i*j)*(unity_root k (m*i))))"
using distr k_def by simp
also have "… = (∑i<k. 1 / k *
(∑j<k. ws ! j * unity_root k (i*(m-j))))"
using prod by presburger
also have "… = 1 / k * (∑i<k.
(∑j<k. ws ! j * unity_root k (i*(m-j))))"
also have "… = 1 / k * (∑j<k.
(∑i<k. ws ! j * unity_root k (i*(m-j))))"
using sum.swap by fastforce
also have "… = 1 / k * (∑j<k. ws ! j * (∑i<k. unity_root k (i*(m-j))))"
also have "… = 1 / k * (∑j<k. ws ! j * unity_root_sum k (m-j))"
unfolding unity_root_sum_def by (simp add: algebra_simps)
also have "(∑j<k. ws ! j * unity_root_sum k (m-j)) = (∑j≤k-1. ws ! j * unity_root_sum k (m-j))"
using ‹k > 0› by (intro sum.cong) auto
also have "… = (∑j∈{nat m}.  ws ! j * unity_root_sum k (m-j))"
using sum_eq .
also have "… = ws ! (nat m) * k"
using assms(2) by (auto simp: algebra_simps)
finally have "poly (finite_fourier_poly ws) (unity_root k m) = ws ! (nat m)"
using assms(2) by auto
then show ?thesis by simp
qed

text ‹Theorem 8.3›
theorem finite_fourier_poly_unique:
assumes "length ws > 0"
defines "k ≡ length ws"
assumes "(degree p ≤ k - 1)"
assumes "(∀m ≤ k-1. (ws ! m) = poly p (unity_root k m))"
shows "p = finite_fourier_poly ws"
proof -
let ?z = "map (λm. unity_root k m) [0..<k]"
have k: "k > 0" using assms by auto
from k have d1: "distinct ?z"
unfolding distinct_conv_nth using unity_root_eqD[OF k] by force
let ?zs_ws = "zip ?z ws"
from d1 k_def have d2: "distinct (map fst ?zs_ws)" by simp
have l2: "length ?zs_ws > 0" using assms(1) k_def by auto
have l3: "length ?zs_ws = k" by (simp add: k_def)

from degree_finite_fourier_poly have degree: "degree (finite_fourier_poly ws) ≤ k - 1"
using k_def by simp

have interp: "poly (finite_fourier_poly ws) x = y"
if "(x, y) ∈ set ?zs_ws" for x y
proof -
from that obtain n where "
x = map (unity_root k ∘ int) [0..<k] ! n ∧
y = ws ! n ∧
n < length ws"
using in_set_zip[of "(x,y)" "(map (unity_root k) (map int [0..<k]))" ws]
by auto
then have "
x = unity_root k (int n) ∧
y = ws ! n ∧
n < length ws"
using nth_map[of n "[0..<k]" "unity_root k ∘ int" ] k_def by simp
thus "poly (finite_fourier_poly ws) x = y"
qed

have interp_p: "poly p x = y" if "(x,y) ∈ set ?zs_ws" for x y
proof -
from that obtain n where "
x = map (unity_root k ∘ int) [0..<k] ! n ∧
y = ws ! n ∧
n < length ws"
using in_set_zip[of "(x,y)" "(map (unity_root k) (map int [0..<k]))" ws]
by auto
then have rw: "x = unity_root k (int n)" "y = ws ! n" "n < length ws"
using nth_map[of n "[0..<k]" "unity_root k ∘ int" ] k_def by simp+
show "poly p x = y"
unfolding rw(1,2) using assms(4) rw(3) k_def by simp
qed

from lagrange_unique[of _ p "finite_fourier_poly ws"] d2 l2
have l: "
degree p ≤ k - 1 ∧
(∀x y. (x, y) ∈ set ?zs_ws ⟶ poly p x = y) ⟹
degree (finite_fourier_poly ws) ≤ k - 1 ∧
(∀x y. (x, y) ∈ set ?zs_ws ⟶ poly (finite_fourier_poly ws) x = y) ⟹
p = (finite_fourier_poly ws)"
using l3 by fastforce
from assms degree interp interp_p l3
show "p = (finite_fourier_poly ws)" using l by blast
qed

text ‹
The following alternative formulation returns a coefficient
›
definition finite_fourier_poly' :: "(nat ⇒ complex) ⇒ nat ⇒ complex poly" where
"finite_fourier_poly' ws k =
(poly_of_list [1 / k * (∑m<k. (ws m) * unity_root k (-n*m)). n ← [0..<k]])"

lemma finite_fourier_poly'_conv_finite_fourier_poly:
"finite_fourier_poly' ws k = finite_fourier_poly [ws n. n ← [0..<k]]"
unfolding finite_fourier_poly_def finite_fourier_poly'_def by simp

lemma coeff_finite_fourier_poly':
assumes "n < k"
shows "coeff (finite_fourier_poly' ws k) n =
(1/k) * (∑m < k. (ws m) * unity_root k (-n*m))"
proof -
let ?ws = "[ws n. n ← [0..<k]]"
have "coeff (finite_fourier_poly' ws k) n =
coeff (finite_fourier_poly ?ws) n"
also have "coeff (finite_fourier_poly ?ws) n =
1 / k * (∑m<k. (?ws ! m) * unity_root k (- n*m))"
using assms by (auto simp: coeff_finite_fourier_poly)
also have "… = (1/k) * (∑m < k. (ws m) * unity_root k (-n*m))"
using assms by simp
finally show ?thesis by simp
qed

lemma degree_finite_fourier_poly': "degree (finite_fourier_poly' ws k) ≤ k - 1"
using degree_finite_fourier_poly[of "[ws n. n ← [0..<k]]"]
by (auto simp: finite_fourier_poly'_conv_finite_fourier_poly)

lemma poly_finite_fourier_poly':
fixes m :: int and k
assumes "m ∈ {0..<k}"
shows "poly (finite_fourier_poly' ws k) (unity_root k m) = ws (nat m)"
using assms poly_finite_fourier_poly[of m "[ws n. n ← [0..<k]]"]
by (auto simp: finite_fourier_poly'_conv_finite_fourier_poly poly_finite_fourier_poly)

lemma finite_fourier_poly'_unique:
assumes "k > 0"
assumes "degree p ≤ k - 1"
assumes "∀m≤k-1. ws m = poly p (unity_root k m)"
shows "p = finite_fourier_poly' ws k"
proof -
let ?ws = "[ws n. n ← [0..<k]]"
from finite_fourier_poly_unique have "p = finite_fourier_poly ?ws" using assms by simp
also have "… = finite_fourier_poly' ws k"
using finite_fourier_poly'_conv_finite_fourier_poly ..
finally show "p = finite_fourier_poly' ws k" by blast
qed

lemma fourier_unity_root:
fixes k :: nat
assumes "k > 0"
shows "poly (finite_fourier_poly' f k) (unity_root k m) =
(∑n<k.1/k*(∑m<k.(f m)*unity_root k (-n*m))*unity_root k (m*n))"
proof -
have "poly (finite_fourier_poly' f k) (unity_root k m) =
(∑n≤k-1. coeff (finite_fourier_poly' f k) n *(unity_root k m)^n)"
using poly_altdef'[of "finite_fourier_poly' f k" "k-1" "unity_root k m"]
degree_finite_fourier_poly'[of f k] by simp
also have "… = (∑n≤k-1. coeff (finite_fourier_poly' f k) n *(unity_root k (m*n)))"
using unity_root_pow by simp
also have "… = (∑n<k. coeff (finite_fourier_poly' f k) n *(unity_root k (m*n)))"
using assms by (intro sum.cong) auto
also have "… = (∑n<k.(1/k)*(∑m<k.(f m)*unity_root k (-n*m))*(unity_root k (m*n)))"
using coeff_finite_fourier_poly'[of _ k f] by simp
finally show
"poly (finite_fourier_poly' f k) (unity_root k m) =
(∑n<k.1/k*(∑m<k.(f m)*unity_root k (-n*m))*unity_root k (m*n))"
by blast
qed

subsection ‹Expansion of an arithmetical function›

text ‹Theorem 8.4›
theorem fourier_expansion_periodic_arithmetic:
assumes "k > 0"
assumes "periodic_arithmetic f k"
defines "g ≡ (λn. (1 / k) * (∑m<k. f m * unity_root k (-n * m)))"
shows "periodic_arithmetic g k"
and "f m = (∑n<k. g n * unity_root k (m * n))"
proof -
{fix l
from unity_periodic_arithmetic mult_period
have period: "periodic_arithmetic (λx. unity_root k x) (k*l)" by simp}
note period = this
{fix n l
have "unity_root k (-(n+k)*l) = cnj (unity_root k ((n+k)*l))"
also have "unity_root k ((n+k)*l) = unity_root k (n*l)"
by (intro unity_root_cong) (auto simp: cong_def algebra_simps)
also have "cnj … = unity_root k (-n*l)"
using unity_root_uminus by simp
finally have "unity_root k (-(n+k)*l) = unity_root k (-n*l)" by simp}
note u_period = this

show 1: "periodic_arithmetic g k"
unfolding periodic_arithmetic_def
proof
fix n

have "g(n+k) = (1 / k) * (∑m<k. f(m) * unity_root k (-(n+k)*m))"
using assms(3) by fastforce
also have "… = (1 / k) * (∑m<k. f(m) * unity_root k (-n*m))"
proof -
have "(∑m<k. f(m) * unity_root k (-(n+k)*m)) =
(∑m<k. f(m) * unity_root k (-n*m))"
by (intro sum.cong) (use u_period in auto)
then show ?thesis by argo
qed
also have "… = g(n)"
using assms(3) by fastforce
finally show "g(n+k) = g(n)" by simp
qed

show "f(m) = (∑n<k. g(n)* unity_root k (m * int n))"
proof -
{
fix m
assume range: "m ∈ {0..<k}"
have "f(m) = (∑n<k. g(n)* unity_root k (m * int n))"
proof -
have "f m = poly (finite_fourier_poly' f k) (unity_root k m)"
using range by (simp add: poly_finite_fourier_poly')
also have "… = (∑n<k. (1 / k) * (∑m<k. f(m) * unity_root k (-n*m))* unity_root k (m*n))"
using fourier_unity_root assms(1) by blast
also have "… = (∑n<k. g(n)* unity_root k (m*n))"
using assms by simp
finally show ?thesis by auto
qed}
note concentrated = this

have "periodic_arithmetic (λm. (∑n<k. g(n)* unity_root k (m * int n))) k"
proof -
have "periodic_arithmetic (λn. g(n)* unity_root k (i * int n)) k"  for i :: int
using 1 unity_periodic_arithmetic mult_periodic_arithmetic
unity_periodic_arithmetic_mult by auto
then have p_s: "∀i<k. periodic_arithmetic (λn. g(n)* unity_root k (i * int n)) k"
by simp
have "periodic_arithmetic (λi. ∑n<k. g(n)* unity_root k (i * int n)) k"
unfolding periodic_arithmetic_def
proof
fix n
show "(∑na<k. g na * unity_root k (int (n + k) * int na)) =
(∑na<k. g na * unity_root k (int n * int na))"
(insert period, unfold periodic_arithmetic_def, blast)
qed
then show ?thesis by simp
qed

from this assms(1-2) concentrated
unique_periodic_arithmetic_extension[of k f "(λi. ∑n<k. g(n)* unity_root k (i * int n))"  m]
show "f m = (∑n<k. g n * unity_root k (int m * int n))" by simp
qed
qed

theorem fourier_expansion_periodic_arithmetic_unique:
fixes f g :: "nat ⇒ complex"
assumes "k > 0"
assumes "periodic_arithmetic f k" and "periodic_arithmetic g k"
assumes "⋀m. m < k ⟹ f m = (∑n<k. g n * unity_root k (int (m * n)))"
shows   "g n = (1 / k) * (∑m<k. f m * unity_root k (-n * m))"
proof -
let ?p = "poly_of_list [g(n). n ← [0..<k]]"
have d: "degree ?p ≤ k-1"
proof -
have "degree ?p ≤ length [g(n). n ← [0..<k]] - 1"
using degree_poly_of_list_le by blast
also have "… = length [0..<k] - 1"
using length_map by auto
finally show ?thesis by simp
qed
have c: "coeff ?p i = (if i < k then g(i) else 0)" for i
{fix z
have "poly ?p z = (∑n≤k-1. coeff ?p n* z^n)"
using poly_altdef'[of ?p "k-1"] d by blast
also have "… = (∑n<k. coeff ?p n* z^n)"
using ‹k > 0› by (intro sum.cong) auto
also have "… = (∑n<k. (if n < k then g(n) else 0)* z^n)"
using c by simp
also have "… = (∑n<k. g(n)* z^n)"
by (simp split: if_splits)
finally have "poly ?p z = (∑n<k. g n * z ^ n)" .}
note eval = this
{fix i
have "poly ?p (unity_root k i) = (∑n<k. g(n)* (unity_root k i)^n)"
using eval by blast
then have "poly ?p (unity_root k i) = (∑n<k. g(n)* (unity_root k (i*n)))"
using unity_root_pow by auto}
note interpolation = this

{
fix m
assume b: "m ≤ k-1"
from d assms(1)
have "f m = (∑n<k. g(n) * unity_root k (m*n))"
using assms(4) b by auto
also have "… = poly ?p (unity_root k m)"
using interpolation by simp
finally have "f m = poly ?p (unity_root k m)" by auto
}

from this finite_fourier_poly'_unique[of k _ f]
have p_is_fourier: "?p = finite_fourier_poly' f k"
using assms(1) d by blast

{
fix n
assume b: "n ≤ k-1"
have f_1: "coeff ?p n = (1 / k) * (∑m<k. f(m) * unity_root k (-n*m))"
using p_is_fourier using assms(1) b by (auto simp: coeff_finite_fourier_poly')
then have "g(n) = (1 / k) * (∑m<k. f(m) * unity_root k (-n*m))"
using c b assms(1)
proof -
have 1: "coeff ?p n = (1 / k) * (∑m<k. f(m) * unity_root k (-n*m))"
using f_1 by blast
have 2: "coeff ?p n =  g n"
using c assms(1) b by simp
show ?thesis using 1 2 by argo
qed
}

(* now show right hand side is periodic and use unique_periodic_extension *)
have "periodic_arithmetic (λn. (1 / k) * (∑m<k. f(m) * unity_root k (-n*m))) k"
proof -
have "periodic_arithmetic (λi. unity_root k (-int i*int m)) k" for m
using unity_root_periodic_arithmetic_mult_minus by simp
then have "periodic_arithmetic (λi. f(m) * unity_root k (-i*m)) k" for m
then show "periodic_arithmetic (λi. (1 / k) * (∑m<k. f m * unity_root k (-i*m))) k"
by (intro scalar_mult_periodic_arithmetic fin_sum_periodic_arithmetic_set) auto
qed
note periodich = this
let ?h = "(λi. (1 / k) *(∑m<k. f m * unity_root k (-i*m)))"
from unique_periodic_arithmetic_extension[of k g ?h n]
assms(3) assms(1) periodich
have "g n = (1/k) * (∑m<k. f m * unity_root k (-n*m))"
by (simp add: ‹⋀na. na ≤ k - 1 ⟹ g na = complex_of_real (1 / real k) * (∑m<k. f m * unity_root k (- int na * int m))›)
then show ?thesis by simp
qed

end

Theory Ramanujan_Sums

(*
File:     Ramanujan_Sums.thy
Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM

Ramanujan sums and generalised Ramanujan sums
*)
section ‹Ramanujan sums›
theory Ramanujan_Sums
imports
Dirichlet_Series.Moebius_Mu
Gauss_Sums_Auxiliary
Finite_Fourier_Series
begin

subsection ‹Basic sums›

definition ramanujan_sum :: "nat ⇒ nat ⇒ complex"
where "ramanujan_sum k n = (∑m | m ∈ {1..k} ∧ coprime m k. unity_root k (m*n))"

notation ramanujan_sum ("c")

lemma ramanujan_sum_0_n [simp]: "c 0 n = 0"
unfolding ramanujan_sum_def by simp

lemma sum_coprime_conv_dirichlet_prod_moebius_mu:
fixes F S :: "nat ⇒ complex" and f :: "nat ⇒ nat ⇒ complex"
defines "F ≡ (λn. (∑k ∈ {1..n}. f k n))"
defines "S ≡ (λn. (∑k | k ∈ {1..n} ∧ coprime k n . f k n))"
assumes "⋀a b d. d dvd a ⟹ d dvd b ⟹ f (a div d) (b div d) = f a b"
shows "S n = dirichlet_prod moebius_mu F n"
proof (cases "n = 0")
case True
then show ?thesis
using assms(2) unfolding dirichlet_prod_def by fastforce
next
case False
have "S(n) = (∑k | k ∈ {1..n} ∧ coprime k n . (f k n))"
using assms by blast
also have "… = (∑k ∈ {1..n}. (f k n)* dirichlet_prod_neutral (gcd k n))"
using dirichlet_prod_neutral_intro by blast
also have "… = (∑k ∈ {1..n}. (f k n)* (∑d | d dvd (gcd k n). moebius_mu d))"
proof -
{
fix k
have "dirichlet_prod_neutral (gcd k n) = (if gcd k n = 1 then 1 else 0)"
using dirichlet_prod_neutral_def[of "gcd k n"] by blast
also have "… = (∑d | d dvd gcd k n. moebius_mu d)"
using sum_moebius_mu_divisors'[of "gcd k n"] by auto
finally have "dirichlet_prod_neutral (gcd k n) = (∑d | d dvd gcd k n. moebius_mu d)"
by auto
} note summand = this
then show ?thesis by (simp add: summand)
qed
also have "… = (∑k = 1..n. (∑d | d dvd gcd k n. (f k n) *  moebius_mu d))"
also have "… = (∑k = 1..n. (∑d | d dvd gcd n k. (f k n) *  moebius_mu d))"
using gcd.commute[of _ n] by simp
also have "… = (∑d | d dvd n. ∑k | k ∈ {1..n} ∧ d dvd k. (f k n) * moebius_mu d)"
using sum.swap_restrict[of "{1..n}" "{d. d dvd n}"
"λk d. (f k n)*moebius_mu d" "λk d. d dvd k"] False by auto
also have "… = (∑d | d dvd n. moebius_mu d * (∑k | k ∈ {1..n} ∧ d dvd k. (f k n)))"
also have "… = (∑d | d dvd n. moebius_mu d * (∑q ∈ {1..n div d}. (f q (n div d))))"
proof -
have st: "
(∑k | k ∈ {1..n} ∧ d dvd k. (f k n)) =
(∑q ∈ {1..n div d}. (f q (n div d)))"
if "d dvd n" "d > 0" for d :: nat
by (rule sum.reindex_bij_witness[of _ "λk. k * d" "λk. k div d"])
(use assms(3) that in ‹fastforce simp: div_le_mono›)+
show ?thesis
by (intro sum.cong) (use st False in fastforce)+
qed
also have "… = (∑d | d dvd n. moebius_mu d * F(n div d))"
proof -
have "F (n div d) = (∑q ∈ {1..n div d}. (f q (n div d)))"
if "d dvd n" for d
by (simp add: F_def real_of_nat_div that)
then show ?thesis by auto
qed
also have "… = dirichlet_prod moebius_mu F n"
finally show ?thesis by simp
qed

lemma dirichlet_prod_neutral_sum:
"dirichlet_prod_neutral n = (∑k = 1..n. unity_root n k)" for n :: nat
proof (cases "n = 0")
case True then show ?thesis unfolding dirichlet_prod_neutral_def by simp
next
case False
have 1: "unity_root n 0 = 1" by simp
have 2: "unity_root n n = 1"
proof -
have "1 = unity_root n (int 0)"
using 1 by auto
also have "unity_root n (int 0) = unity_root n (int (0 + n))"
using unity_periodic_arithmetic[of n] periodic_arithmetic_def by algebra
also have "… = unity_root n (int n)" by simp
finally show ?thesis by auto
qed
have "(∑k = 1..n. unity_root n k) = (∑k = 0..n. unity_root n k) - 1"
by (simp add: sum.atLeast_Suc_atMost sum.atLeast0_atMost_Suc_shift 1)
also have "… = ((∑k = 0..n-1. unity_root n k)+1) - 1"
using sum.atLeast0_atMost_Suc[of "(λk. unity_root n k)" "n-1"] False
also have "… = (∑k = 0..n-1. unity_root n k)"
by simp
also have "… = unity_root_sum n 1"
unfolding unity_root_sum_def using ‹n ≠ 0› by (intro sum.cong) auto
also have "… = dirichlet_prod_neutral n"
using unity_root_sum[of n 1] False
by (cases "n = 1",auto simp add: False dirichlet_prod_neutral_def)
finally have 3: "dirichlet_prod_neutral n = (∑k = 1..n. unity_root n k)" by auto
then show ?thesis by blast
qed

lemma moebius_coprime_sum:
"moebius_mu n = (∑k | k ∈ {1..n} ∧ coprime k n . unity_root n (int k))"
proof -
let ?f = "(λk n. unity_root n k)"
from div_dvd_div have "
d dvd a ⟹ d dvd b ⟹
unity_root (a div d) (b div d) =
unity_root a b" for a b d :: nat
using unity_root_def real_of_nat_div by fastforce
then have "(∑k | k ∈ {1..n} ∧ coprime k n. ?f k n) =
dirichlet_prod moebius_mu (λn. ∑k = 1..n. ?f k n) n"
using sum_coprime_conv_dirichlet_prod_moebius_mu[of ?f n] by blast
also have "… = dirichlet_prod moebius_mu dirichlet_prod_neutral n"
also have "… = moebius_mu n"
by (cases "n = 0") (simp_all add: dirichlet_prod_neutral_right_neutral)
finally have "moebius_mu n = (∑k | k ∈ {1..n} ∧ coprime k n. ?f k n)"
by argo
then show ?thesis by blast
qed

corollary ramanujan_sum_1_right [simp]: "c k (Suc 0) = moebius_mu k"
unfolding ramanujan_sum_def using moebius_coprime_sum[of k] by simp

lemma ramanujan_sum_dvd_eq_totient:
assumes "k dvd n"
shows "c k n = totient k"
unfolding ramanujan_sum_def
proof -
have "unity_root k (m*n) = 1" for m
using assms by (cases "k = 0") (auto simp: unity_root_eq_1_iff_int)
then have "(∑m | m ∈ {1..k} ∧ coprime m k. unity_root k (m * n)) =
(∑m | m ∈ {1..k} ∧ coprime m k. 1)" by simp
also have "… = card {m. m ∈ {1..k} ∧ coprime m k}" by simp
also have "… = totient k"
unfolding totient_def totatives_def
proof -
have "{1..k} = {0<..k}" by auto
then show " of_nat (card {m ∈ {1..k}. coprime m k}) =
of_nat (card {ka ∈ {0<..k}. coprime ka k})" by auto
qed
finally show "(∑m | m ∈ {1..k} ∧ coprime m k. unity_root k (m * n)) = totient k"
by auto
qed

subsection ‹Generalised sums›

definition gen_ramanujan_sum :: "(nat ⇒ complex) ⇒ (nat ⇒ complex) ⇒ nat ⇒ nat ⇒ complex" where
"gen_ramanujan_sum f g = (λk n. ∑d | d dvd gcd n k. f d * g (k div d))"

notation gen_ramanujan_sum ("s")

lemma gen_ramanujan_sum_k_1: "s f g k 1 = f 1 * g k"
unfolding gen_ramanujan_sum_def by auto

lemma gen_ramanujan_sum_1_n: "s f g 1 n = f 1 * g 1"
unfolding gen_ramanujan_sum_def by simp

lemma gen_ramanujan_sum_periodic: "periodic_arithmetic (s f g k) k"
unfolding gen_ramanujan_sum_def periodic_arithmetic_def by simp

text ‹Theorem 8.5›
theorem gen_ramanujan_sum_fourier_expansion:
fixes f g :: "nat ⇒ complex" and a :: "nat ⇒ nat ⇒ complex"
assumes "k > 0"
defines "a ≡ (λk m. (1/k) * (∑d| d dvd (gcd m k). g d * f (k div d) * d))"
shows "s f g k n = (∑m≤k-1. a k m * unity_root k (m*n))"
proof -
let ?g = "(λx. 1 / of_nat k * (∑m<k. s f g k m * unity_root k (-x*m)))"
{fix m :: nat
let ?h = "λn d. f d * g (k div d) * unity_root k (- m * int n)"
have "(∑l<k. s f g k l * unity_root k (-m*l)) =
(∑l ∈ {0..k-1}. s f g k l * unity_root k (-m*l))"
using ‹k > 0› by (intro sum.cong) auto
also have "… = (∑l ∈ {1..k}. s f g k l * unity_root k (-m*l))"
proof -
have "periodic_arithmetic (λl. unity_root k (-m*l)) k"
using unity_periodic_arithmetic_mult by blast
then have "periodic_arithmetic (λl. s f g k l * unity_root k (-m*l)) k"
using gen_ramanujan_sum_periodic mult_periodic_arithmetic by blast
from this periodic_arithmetic_sum_periodic_arithmetic_shift[of _ k 1  ]
have "sum (λl. s f g k l * unity_root k (-m*l)) {0..k - 1} =
sum (λl. s f g k l * unity_root k (-m*l)) {1..k}"
using assms(1) zero_less_one by simp
then show ?thesis by argo
qed
also have "… = (∑n∈{1..k}. (∑d | d dvd (gcd n k). f(d) * g(k div d)) * unity_root k (-m*n))"
also have "… = (∑n∈{1..k}. (∑d | d dvd (gcd n k). f(d) * g(k div d) * unity_root k (-m*n)))"
also have "… = (∑d | d dvd k. ∑n | n ∈ {1..k} ∧ d dvd n. ?h n d)"
proof -
have "(∑n = 1..k. ∑d | d dvd gcd n k. ?h n d) =
(∑n = 1..k. ∑d | d dvd k ∧ d dvd n . ?h n d)"
using gcd.commute[of _ k] by simp
also have "… = (∑d | d dvd k. ∑n | n ∈ {1..k} ∧ d dvd n. ?h n d)"
using sum.swap_restrict[of "{1..k}" "{d. d dvd k}"
_ "λn d. d dvd n"] assms by fastforce
finally have "
(∑n = 1..k. ∑d | d dvd gcd n k. ?h n d) =
(∑d | d dvd k. ∑n | n ∈ {1..k} ∧ d dvd n. ?h n d)" by blast
then show ?thesis by simp
qed
also have "… = (∑d | d dvd k. f(d)*g(k div d)*
(∑n | n ∈ {1..k} ∧ d dvd n. unity_root k (- m * int n)))"
also have "… = (∑d | d dvd k. f(d)*g(k div d)*
(∑e ∈ {1..k div d}. unity_root k (- m * (e*d))))"
using assms(1) sum_div_reduce div_greater_zero_iff dvd_div_gt0 by auto
also have "… = (∑d | d dvd k. f(d)*g(k div d)*
(∑e ∈ {1..k div d}. unity_root (k div d) (- m * e)))"
proof -
{
fix d e
assume "d dvd k"
hence "2 * pi * real_of_int (- int m * int (e * d)) / real k =
2 * pi * real_of_int (- int m * int e) / real (k div d)" by auto
hence "unity_root k (- m * (e * d)) = unity_root (k div d) (- m * e)"
unfolding unity_root_def by simp
}
then show ?thesis by simp
qed
also have "… = dirichlet_prod (λd. f(d)*g(k div d))
(λd. (∑e ∈ {1..d}. unity_root d (- m * e))) k"
unfolding dirichlet_prod_def by blast
also have "… = dirichlet_prod (λd. (∑e ∈ {1..d}. unity_root d (- m * e)))
(λd. f(d)*g(k div d)) k"
using dirichlet_prod_commutes[of
"(λd. f(d)*g(k div d))"
"(λd. (∑e ∈ {1..d}. unity_root d (- m * e)))"] by argo
also have "… = (∑d | d dvd k.
(∑e ∈ {1..(d::nat)}. unity_root d (- m * e))*(f(k div d)*g(k div (k div d))))"
unfolding dirichlet_prod_def by blast
also have "… = (∑d | d dvd k. (∑e ∈ {1..(d::nat)}.
unity_root d (- m * e))*(f(k div d)*g(d)))"
proof -
{
fix d :: nat
assume "d dvd k"
then have "k div (k div d) = d"
}
then show ?thesis by simp
qed
also have "… = (∑(d::nat) | d dvd k ∧ d dvd m. d*(f(k div d)*g(d)))"
proof -
{
fix d
assume "d dvd k"
with assms have "d > 0" by (intro Nat.gr0I) auto
have "periodic_arithmetic (λx. unity_root d (- m * int x)) d"
using unity_periodic_arithmetic_mult by blast
then have "(∑e ∈ {1..d}. unity_root d (- m * e)) =
(∑e ∈ {0..d-1}. unity_root d (- m * e))"
using periodic_arithmetic_sum_periodic_arithmetic_shift[of "λe. unity_root d (- m * e)"  d 1] assms ‹d dvd k›
by fastforce
also have "… = unity_root_sum d (-m)"
unfolding unity_root_sum_def using ‹d > 0› by (intro sum.cong) auto
finally have
"(∑e ∈ {1..d}. unity_root d (- m * e)) = unity_root_sum d (-m)"
by argo
}
then have "
(∑d | d dvd k. (∑e = 1..d. unity_root d (- m * int e)) * (f (k div d) * g d)) =
(∑d | d dvd k. unity_root_sum d (-m) * (f (k div d) * g d))" by simp
also have "… = (∑d | d dvd k ∧ d dvd m. unity_root_sum d (-m) * (f (k div d) * g d))"
proof (intro sum.mono_neutral_right,simp add: ‹k > 0›,blast,standard)
fix i
assume as: "i ∈ {d. d dvd k} - {d. d dvd k ∧ d dvd m}"
then have "i ≥ 1" using ‹k > 0› by auto
have "k ≥ 1" using ‹k > 0› by auto
have "¬ i dvd (-m)" using as by auto
thus "unity_root_sum i (- int m) * (f (k div i) * g i) = 0"
using ‹i ≥ 1› by (subst unity_root_sum(2)) auto
qed
also have "… = (∑d | d dvd k ∧ d dvd m. d * (f (k div d) * g d))"
proof -
{fix d :: nat
assume 1: "d dvd m"
assume 2: "d dvd k"
then have "unity_root_sum d (-m) = d"
using unity_root_sum[of d "(-m)"] assms(1) 1 2
by auto}
then show ?thesis by auto
qed
finally show ?thesis by argo
qed
also have "… = (∑d | d dvd gcd m k. of_nat d * (f (k div d) * g d))"
also have "… = (∑d | d dvd gcd m k. g d * f (k div d) * d)"
also have "1 / k * … = a k m" using a_def by auto
finally have "?g m = a k m" by simp}
note a_eq_g = this
{
fix m
from fourier_expansion_periodic_arithmetic(2)[of k "s f g k" ] gen_ramanujan_sum_periodic assms(1)
have "s f g k m = (∑n<k. ?g n * unity_root k (int m * n))"
by blast
also have "… = (∑n<k. a k n * unity_root k (int m * n))"
using a_eq_g by simp
also have "… = (∑n≤k-1. a k n * unity_root k (int m * n))"
using ‹k > 0› by (intro sum.cong) auto
finally have "s f g k m =
(∑n≤k - 1. a k n * unity_root k (int n * int m))"
}
then show ?thesis by blast
qed

text ‹Theorem 8.6›
theorem ramanujan_sum_dirichlet_form:
fixes k n :: nat
assumes "k > 0"
shows "c k n = (∑d | d dvd gcd n k. d * moebius_mu (k div d))"
proof -
define a :: "nat ⇒ nat ⇒ complex"
where "a  =  (λk m.
1 / of_nat k * (∑d | d dvd gcd m k. moebius_mu d * of_nat (k div d) * of_nat d))"

{fix m
have "a k m = (if gcd m k = 1 then 1 else 0)"
proof -
have "a k m = 1 / of_nat k * (∑d | d dvd gcd m k. moebius_mu d * of_nat (k div d) * of_nat d)"
unfolding a_def by blast
also have 2: "… = 1 / of_nat k * (∑d | d dvd gcd m k. moebius_mu d * of_nat k)"
proof -
{fix d :: nat
assume dvd: "d dvd gcd m k"
have "moebius_mu d * of_nat (k div d) * of_nat d = moebius_mu d * of_nat k"
proof -
have "(k div d) * d = k" using dvd by auto
then show "moebius_mu d * of_nat (k div d) * of_nat d = moebius_mu d * of_nat k"
qed} note eq = this
show ?thesis using sum.cong by (simp add: eq)
qed

also have 3: "… = (∑d | d dvd gcd m k. moebius_mu d)"
also have 4: "… =  (if gcd m k = 1 then 1 else 0)"
using sum_moebius_mu_divisors' by blast
finally show "a k m  = (if gcd m k = 1 then 1 else 0)"
using coprime_def by blast
qed} note a_expr = this

let ?f = "(λm. (if gcd m k = 1 then 1 else 0) *
unity_root k (int m * n))"
from gen_ramanujan_sum_fourier_expansion[of k id moebius_mu n] assms
have "s (λx. of_nat (id x)) moebius_mu k n =
(∑m≤k - 1.
1 / of_nat k *
(∑d | d dvd gcd m k.
moebius_mu d * of_nat (k div d) * of_nat d) *
unity_root k (int m * n))" by simp
also have "… = (∑m≤k - 1.
a k m *
unity_root k (int m * n))" using a_def by blast
also have "… = (∑m≤k - 1.
(if gcd m k = 1 then 1 else 0) *
unity_root k (int m * n))" using a_expr by auto
also have "… = (∑m ∈ {1..k}.
(if gcd m k = 1 then 1 else 0) *
unity_root k (int m * n))"
proof -
have "periodic_arithmetic (λm. (if gcd m k = 1 then 1 else 0) *
unity_root k (int m * n)) k"
proof -
have "periodic_arithmetic (λm. if gcd m k = 1 then 1 else 0) k"
moreover have "periodic_arithmetic (λm. unity_root k (int m * n)) k"
using unity_periodic_arithmetic_mult[of k n]
by (subst mult.commute,simp)
ultimately show "periodic_arithmetic ?f k"
using mult_periodic_arithmetic by simp
qed
then have "sum ?f {0..k - 1} = sum ?f {1..k}"
using periodic_arithmetic_sum_periodic_arithmetic_shift[of ?f k 1] by force
then show ?thesis by (simp add: atMost_atLeast0)
qed
also have "… = (∑m | m ∈ {1..k} ∧ gcd m k = 1.
(if gcd m k = 1 then 1 else 0) *
unity_root k (int m * int n))"
by (intro sum.mono_neutral_right,auto)
also have "… = (∑m | m ∈ {1..k} ∧ gcd m k = 1.
unity_root k (int m * int n))" by simp
also have "… = (∑m | m ∈ {1..k} ∧ coprime m k.
unity_root k (int m * int n))"
using coprime_iff_gcd_eq_1 by presburger
also have "… = c k n" unfolding ramanujan_sum_def by simp
finally show ?thesis unfolding gen_ramanujan_sum_def by auto
qed

corollary ramanujan_sum_conv_gen_ramanujan_sum:
"k > 0 ⟹ c k n = s id moebius_mu k n"
using ramanujan_sum_dirichlet_form unfolding gen_ramanujan_sum_def by simp

text ‹Theorem 8.7›
theorem gen_ramanujan_sum_distrib:
fixes f g :: "nat ⇒ complex"
assumes "a > 0" "b > 0" "m > 0" "k > 0" (* remove cond. on m,n *)
assumes "coprime a k" "coprime b m" "coprime k m"
assumes "multiplicative_function f" and
"multiplicative_function g"
shows "s f g (m*k) (a*b) = s f g m a * s f g k b"
proof -
from assms(1-6) have eq: "gcd (m*k) (a*b) = gcd a m * gcd k b"
by (simp add: linear_gcd  gcd.commute mult.commute)
have "s f g (m*k) (a*b) =
(∑d | d dvd gcd (m*k) (a*b). f(d) * g((m*k) div d))"
unfolding gen_ramanujan_sum_def by (rule sum.cong, simp add: gcd.commute,blast)
also have "… =
(∑d | d dvd gcd a m * gcd k b. f(d) * g((m*k) div d))"
using eq by simp
also have "… =
(∑(d1,d2) | d1 dvd gcd a m ∧  d2 dvd gcd k b.
f(d1*d2) * g((m*k) div (d1*d2)))"
proof -
have b: "bij_betw (λ(d1, d2). d1 * d2)
{(d1, d2). d1 dvd gcd a m ∧ d2 dvd gcd k b}
{d. d dvd gcd a m * gcd k b}"
using assms(5) reindex_product_bij by blast
have "(∑(d1, d2) | d1 dvd gcd a m ∧ d2 dvd gcd k b.
f (d1 * d2) * g (m * k div (d1 * d2))) =
(∑x∈{(d1, d2). d1 dvd gcd a m ∧ d2 dvd gcd k b}.
f (case x of (d1, d2) ⇒ d1 * d2)*
g (m * k div (case x of (d1, d2) ⇒ d1 * d2)))"
by (rule sum.cong,auto)
also have "… = (∑d | d dvd gcd a m * gcd k b. f d * g (m * k div d))"
using b by (rule sum.reindex_bij_betw[of "λ(d1,d2). d1*d2" ])
finally show ?thesis by argo
qed
also have "… = (∑d1 | d1 dvd gcd a m. ∑d2 | d2 dvd gcd k b.
f (d1*d2) * g ((m*k) div (d1*d2)))"
by (simp add: sum.cartesian_product) (rule sum.cong,auto)
also have "… = (∑d1 | d1 dvd gcd a m. ∑d2 | d2 dvd gcd k b.
f d1 * f d2 * g ((m*k) div (d1*d2)))"
using assms(5) assms(8) multiplicative_function.mult_coprime
by (intro sum.cong refl) fastforce+
also have "… = (∑d1 | d1 dvd gcd a m. ∑d2 | d2 dvd gcd k b.
f d1 * f d2* g (m div d1) * g (k div d2))"
proof (intro sum.cong refl, clarify, goal_cases)
case (1 d1 d2)
hence "g (m * k div (d1 * d2)) = g (m div d1) * g (k div d2)"
using assms(7,9) multipl_div
by (meson coprime_commute dvd_gcdD1 dvd_gcdD2)
thus ?case by simp
qed
also have "… = (∑i∈{d1. d1 dvd gcd a m}. ∑j∈{d2. d2 dvd gcd k b}.
f i * g (m div i) * (f j * g (k div j)))"
by (rule sum.cong,blast,rule sum.cong,blast,simp)
also have "… = (∑d1 | d1 dvd gcd a m. f d1 * g (m div d1)) *
(∑d2 | d2 dvd gcd k b. f d2 * g (k div d2))"
also have "… = s f g m a * s f g k b"
unfolding gen_ramanujan_sum_def by (simp add: gcd.commute)
finally show ?thesis by blast
qed

corollary gen_ramanujan_sum_distrib_right:
fixes f g :: "nat ⇒ complex"
assumes "a > 0" and "b > 0" and "m > 0" (* TODO: remove cond. on m,n *)
assumes "coprime b m"
assumes "multiplicative_function f" and
"multiplicative_function g"
shows "s f g m (a * b) = s f g m a"
proof -
have "s f g m (a*b) = s f g m a * s f g 1 b"
using assms gen_ramanujan_sum_distrib[of a b m 1 f g] by simp
also have "… = s f g m a * f 1 * g 1"
using gen_ramanujan_sum_1_n by auto
also have "… = s f g m a"
using  assms(5-6)
finally show "s f g m (a*b) = s f g m a" by blast
qed

corollary gen_ramanujan_sum_distrib_left:
fixes f g :: "nat ⇒ complex"
assumes "a > 0" and "k > 0" and "m > 0" (* TODO: remove cond. on m,n *)
assumes "coprime a k" and "coprime k m"
assumes "multiplicative_function f" and
"multiplicative_function g"
shows "s f g (m*k) a = s f g m a * g k"
proof -
have "s f g (m*k) a = s f g m a * s f g k 1"
using assms gen_ramanujan_sum_distrib[of a 1 m k f g] by simp
also have "… = s f g m a * f(1) * g(k)"
using gen_ramanujan_sum_k_1 by auto
also have "… = s f g m a *  g k"
using assms(6)
finally show ?thesis by blast
qed

corollary ramanujan_sum_distrib:
assumes "a > 0" and "k > 0" and "m > 0" and "b > 0" (* TODO: remove cond. on m,n *)
assumes "coprime a k" "coprime b m" "coprime m k"
shows "c (m*k) (a*b) = c m a * c k b"
proof -
have "c (m*k) (a*b) = s id moebius_mu (m*k) (a*b)"
using ramanujan_sum_conv_gen_ramanujan_sum assms(2,3) by simp

also have "… = (s id moebius_mu m a) * (s id moebius_mu k b)"
using gen_ramanujan_sum_distrib[of a b m k id moebius_mu]
assms mult_id mult_moebius mult_of_nat
coprime_commute[of m k] by auto
also have "… = c m a * c k b" using ramanujan_sum_conv_gen_ramanujan_sum assms by simp
finally show ?thesis by simp
qed

corollary ramanujan_sum_distrib_right:
assumes "a > 0" and "k > 0" and "m > 0" and "b > 0" (* remove cond. on m,n *)
assumes "coprime b m"
shows "c m (a*b) = c m a"
using assms ramanujan_sum_conv_gen_ramanujan_sum mult_id mult_moebius
mult_of_nat gen_ramanujan_sum_distrib_right by auto

corollary ramanujan_sum_distrib_left:
assumes "a > 0" "k > 0" "m > 0"  (* remove cond. on m,n *)
assumes "coprime a k" "coprime m k"
shows "c (m*k) a = c m a * moebius_mu k"
using assms
by (simp add: ramanujan_sum_conv_gen_ramanujan_sum, subst gen_ramanujan_sum_distrib_left)
(auto simp: coprime_commute mult_of_nat mult_moebius)

lemma dirichlet_prod_completely_multiplicative_left:
fixes f h :: "nat ⇒ complex" and k :: nat
defines "g ≡ (λk. moebius_mu k * h k)"
defines "F ≡ dirichlet_prod f g"
assumes "k > 0"
assumes "completely_multiplicative_function f"
"multiplicative_function h"
assumes "⋀p. prime p ⟹ f(p) ≠ 0 ∧ f(p) ≠ h(p)"
shows "F k = f k * (∏p∈prime_factors k. 1 - h p / f p)"
proof -
have 1: "multiplicative_function (λp. h(p) div f(p))"
using multiplicative_function_divide
comp_to_mult assms(4,5) by blast
have "F k = dirichlet_prod g f k"
unfolding F_def using dirichlet_prod_commutes[of f g] by auto
also have "… = (∑d | d dvd k. moebius_mu d * h d * f(k div d))"
unfolding g_def dirichlet_prod_def by blast
also have "… = (∑d | d dvd k. moebius_mu d * h d * (f(k) div f(d)))"
using multipl_div_mono[of f _ k] assms(4,6)
by (intro sum.cong,auto,force)
also have "… = f k * (∑d | d dvd k. moebius_mu d * (h d div f(d)))"
also have "… = f k * (∏p∈prime_factors k. 1 - (h p div f p))"
using sum_divisors_moebius_mu_times_multiplicative[of "λp. h p div f p" k] 1
assms(3) by simp
finally show F_eq: "F k = f k * (∏p∈prime_factors k. 1 - (h p div f p))"
by blast
qed

text ‹Theorem 8.8›
theorem gen_ramanujan_sum_dirichlet_expr:
fixes f h :: "nat ⇒ complex" and n k :: nat
defines "g ≡ (λk. moebius_mu k * h k)"
defines "F ≡ dirichlet_prod f g"
defines "N ≡ k div gcd n k"
assumes "completely_multiplicative_function f"
"multiplicative_function h"
assumes "⋀p. prime p ⟹ f(p) ≠ 0 ∧ f(p) ≠ h(p)"
assumes "k > 0" "n > 0"
shows "s f g k n = (F(k)*g(N)) div (F(N))"
proof -
define a where "a ≡ gcd n k"
have 2: "k = a*N" unfolding a_def N_def by auto
have 3: "a > 0" using a_def assms(7,8) by simp
have Ngr0: "N > 0" using assms(7,8) 2 N_def by fastforce
have f_k_not_z: "f k ≠ 0"
using completely_multiplicative_nonzero assms(4,6,7) by blast
have f_N_not_z: "f N ≠ 0"
using completely_multiplicative_nonzero assms(4,6) Ngr0 by blast
have bij: "bij_betw (λd. a div d) {d. d dvd a} {d. d dvd a}"
unfolding bij_betw_def
proof
show inj: "inj_on (λd. a div d) {d. d dvd a}"
using inj_on_def "3" dvd_div_eq_2 by blast
show surj: "(λd. a div d)  {d. d dvd a} = {d. d dvd a}"
unfolding image_def
proof
show " {y. ∃x∈{d. d dvd a}. y = a div x} ⊆ {d. d dvd a}"
by auto
show "{d. d dvd a} ⊆ {y. ∃x∈{d. d dvd a}. y = a div x}"
proof
fix d
assume a: "d ∈ {d. d dvd a}"
from a have 1: "(a div d) ∈ {d. d dvd a}" by auto
from a have 2: "d = a div (a div d)" using 3 by auto
from 1 2 show "d ∈ {y. ∃x∈{d. d dvd a}. y = a div x} " by blast
qed
qed
qed

have "s f g k n = (∑d | d dvd a. f(d)*moebius_mu(k div d)*h(k div d))"
unfolding gen_ramanujan_sum_def g_def a_def by (simp add: mult.assoc)
also have "… = (∑d | d dvd a. f(d) * moebius_mu(a*N div d)*h(a*N div d))"
using 2 by blast
also have "… = (∑d | d dvd a. f(a div d) * moebius_mu(N*d)*h(N*d))"
(is "?a = ?b")
proof -
define f_aux where "f_aux ≡ (λd. f d * moebius_mu (a * N div d) * h (a * N div d))"
have 1: "?a = (∑d | d dvd a. f_aux d)" using f_aux_def by blast
{fix d :: nat
assume "d dvd a"
then have "N * a div (a div d) = N * d"
using 3 by force}
then have 2: "?b = (∑d | d dvd a. f_aux (a div d))"
unfolding f_aux_def by (simp add: algebra_simps)
show "?a = ?b"
using bij 1 2
by (simp add: sum.reindex_bij_betw[of "((div) a)" "{d. d dvd a}" "{d. d dvd a}"])
qed
also have "… = moebius_mu N * h N * f a * (∑d | d dvd a ∧ coprime N d. moebius_mu d * (h d div f d))"
(is "?a = ?b")
proof -
have "?a = (∑d | d dvd a ∧ coprime N d. f(a div d) * moebius_mu (N*d) * h (N*d))"
by (rule sum.mono_neutral_right)(auto simp add: moebius_prod_not_coprime 3)
also have "… = (∑d | d dvd a ∧ coprime N d. moebius_mu N * h N * f(a div d) * moebius_mu d * h d)"
proof (rule sum.cong,simp)
fix d
assume a: "d ∈ {d. d dvd a ∧ coprime N d}"
then have 1: "moebius_mu (N*d) = moebius_mu N * moebius_mu d"
using mult_moebius unfolding multiplicative_function_def
from a have 2: "h (N*d) = h N * h d"
using assms(5) unfolding multiplicative_function_def
show "f (a div d) * moebius_mu (N * d) * h (N * d) =
moebius_mu N * h N * f (a div d) * moebius_mu d * h d"
by (simp add: divide_simps 1 2)
qed
also have "… = (∑d | d dvd a ∧ coprime N d. moebius_mu N * h N * (f a div f d) * moebius_mu d * h d)"
by (intro sum.cong refl) (use multipl_div_mono[of f _ a] assms(4,6-8) 3 in force)
also have "… = moebius_mu N * h N * f a * (∑d | d dvd a ∧ coprime N d. moebius_mu d * (h d div f d))"
finally show ?thesis by blast
qed
also have "… =
moebius_mu N * h N * f a * (∏p∈{p. p ∈ prime_factors a ∧ ¬ (p dvd N)}. 1 - (h p div f p))"
proof -
have "multiplicative_function (λd. h d div f d)"
using multiplicative_function_divide
comp_to_mult
assms(4,5) by blast
then have "(∑d | d dvd a ∧ coprime N d. moebius_mu d * (h d div f d)) =
(∏p∈{p. p ∈ prime_factors a ∧ ¬ (p dvd N)}. 1 - (h p div f p))"
using sum_divisors_moebius_mu_times_multiplicative_revisited[
of "(λd. h d div f d)" a N]
assms(8) Ngr0 3 by blast
then show ?thesis by argo
qed
also have "… = f(a) * moebius_mu(N) * h(N) *
((∏p∈{p. p ∈ prime_factors (a*N)}. 1 - (h p div f p)) div
(∏p∈{p. p ∈ prime_factors N}. 1 - (h p div f p)))"
proof -
have "{p. p ∈prime_factors a ∧ ¬ p dvd N} =
({p. p ∈prime_factors (a*N)} - {p. p ∈prime_factors N})"
using p_div_set[of a N] by blast
then have eq2: "(∏p∈{p. p ∈prime_factors a ∧ ¬ p dvd N}. 1 - h p / f p) =
prod (λp. 1 - h p / f p) ({p. p ∈prime_factors (a*N)} - {p. p ∈prime_factors N})"
by auto
also have eq: "… = prod (λp. 1 - h p / f p) {p. p ∈prime_factors (a*N)} div
prod (λp. 1 - h p / f p) {p. p ∈prime_factors N}"
proof (intro prod_div_sub,simp,simp,simp add: "3" Ngr0 dvd_prime_factors,simp,standard)
fix b
assume "b ∈# prime_factorization N"
then have p_b: "prime b" using in_prime_factors_iff by blast
then show "f b = 0 ∨ h b ≠ f b" using assms(6)[OF p_b] by auto
qed
also have "… = (∏p∈{p. p ∈ prime_factors (a*N)}. 1 - (h p div f p)) div
(∏p∈{p. p ∈ prime_factors N}. 1 - (h p div f p))" by blast
finally have "(∏p∈{p. p ∈prime_factors a ∧ ¬ p dvd N}. 1 - h p / f p) =
(∏p∈{p. p ∈ prime_factors (a*N)}. 1 - (h p div f p)) div
(∏p∈{p. p ∈ prime_factors N}. 1 - (h p div f p))"
using eq eq2 by auto
then show ?thesis by simp
qed
also have "… = f(a) * moebius_mu(N) * h(N) * (F(k) div f(k)) * (f(N) div F(N))"
(is "?a = ?b")
proof -
have "F(N) = (f N) *(∏p∈ prime_factors N. 1 - (h p div f p))"
unfolding F_def g_def
by (intro dirichlet_prod_completely_multiplicative_left) (auto simp add: Ngr0 assms(4-6))
then have eq_1: "(∏p∈ prime_factors N. 1 - (h p div f p)) =
F N div f N" using 2 f_N_not_z by simp
have "F(k) = (f k) * (∏p∈ prime_factors k. 1 - (h p div f p))"
unfolding F_def g_def
by (intro dirichlet_prod_completely_multiplicative_left) (auto simp add: assms(4-7))
then have eq_2: "(∏p∈ prime_factors k. 1 - (h p div f p)) =
F k div f k" using 2 f_k_not_z by simp

have "?a = f a * moebius_mu N * h N *
((∏p∈ prime_factors k. 1 - (h p div f p)) div
(∏p∈ prime_factors N. 1 - (h p div f p)))"
using 2 by (simp add: algebra_simps)
also have  "… = f a * moebius_mu N * h N * ((F k div f k) div (F N div f N))"
finally show ?thesis by simp
qed
also have "… = moebius_mu N * h N * ((F k * f a * f N) div (F N * f k))"
also have "… = moebius_mu N * h N * ((F k * f(a*N)) div (F N * f k))"
proof -
have "f a * f N = f (a*N)"
proof (cases "a = 1 ∨ N = 1")
case True
then show ?thesis
using assms(4) completely_multiplicative_function_def[of f]
by auto
next
case False
then show ?thesis
using 2 assms(4) completely_multiplicative_function_def[of f]
Ngr0 3 by auto
qed
then show ?thesis by simp
qed
also have "… = moebius_mu N * h N * ((F k * f(k)) div (F N * f k))"
using 2 by blast
also have "… = g(N) * (F k div F N)"
using f_k_not_z g_def by simp
also have "… = (F(k)*g(N)) div (F(N))" by auto
finally show ?thesis by simp
qed

(*TODO remove this and substitute
the theorem totient_conv_moebius_mu in More_totient by
this version: int → of_nat*)
lemma totient_conv_moebius_mu_of_nat:
"of_nat (totient n) = dirichlet_prod moebius_mu of_nat 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

corollary ramanujan_sum_k_n_dirichlet_expr:
fixes k n :: nat
assumes "k > 0" "n > 0"
shows "c k n = of_nat (totient k) *
moebius_mu (k div gcd n k) div
of_nat (totient (k div gcd n k))"
proof -
define f :: "nat ⇒ complex"
where "f ≡ of_nat"
define F :: "nat ⇒ complex"
where "F ≡ (λd. dirichlet_prod f moebius_mu d)"
define g :: "nat ⇒ complex "
where "g ≡ (λl. moebius_mu l)"
define N where "N ≡ k div gcd n k"
define h :: "nat ⇒ complex"
where "h ≡ (λx. (if x = 0 then 0 else 1))"

have F_is_totient_k: "F k = totient k"
by (simp add: F_def f_def dirichlet_prod_commutes totient_conv_moebius_mu_of_nat[of k])
have F_is_totient_N: "F N = totient N"
by (simp add: F_def f_def dirichlet_prod_commutes totient_conv_moebius_mu_of_nat[of N])

have "c k n = s id moebius_mu k n"
using ramanujan_sum_conv_gen_ramanujan_sum assms by blast
also have "… =  s f g k n"
unfolding f_def g_def by auto
also have "g = (λk. moebius_mu k * h k)"
by (simp add: fun_eq_iff h_def g_def)
also have "multiplicative_function h"
unfolding h_def by standard auto
hence "s f (λk. moebius_mu k * h k) k n =
dirichlet_prod of_nat (λk. moebius_mu k * h k) k *
(moebius_mu (k div gcd n k) * h (k div gcd n k)) /
dirichlet_prod of_nat (λk. moebius_mu k * h k) (k div gcd n k)"
unfolding f_def using assms mult_of_nat_c
by (intro gen_ramanujan_sum_dirichlet_expr) (auto simp: h_def)
also have "… = of_nat (totient k) * moebius_mu (k div gcd n k) / of_nat (totient (k div gcd n k))"
using F_is_totient_k F_is_totient_N by (auto simp: h_def F_def N_def f_def)
finally show ?thesis .
qed

no_notation ramanujan_sum ("c")
no_notation gen_ramanujan_sum ("s")

end

Theory Gauss_Sums

(*
File:     Gauss_Sums.thy
Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM

Gauss sums and more on Dirichlet characters: induced moduli, separability, primitive characters
*)
theory Gauss_Sums
imports
"HOL-Algebra.Coset"
"HOL-Real_Asymp.Real_Asymp"
Ramanujan_Sums
begin

section ‹Gauss sums›

bundle vec_lambda_notation
begin
notation vec_lambda (binder "χ" 10)
end

bundle no_vec_lambda_notation
begin
no_notation vec_lambda (binder "χ" 10)
end

unbundle no_vec_lambda_notation

subsection ‹Definition and basic properties›
context dcharacter
begin

(* TODO remove when integrating periodic and periodic_function *)
lemma dir_periodic_arithmetic: "periodic_arithmetic χ n"
unfolding periodic_arithmetic_def by (simp add: periodic)

definition "gauss_sum k = (∑m = 1..n . χ(m) * unity_root n (m*k))"

lemma gauss_sum_periodic:
"periodic_arithmetic (λn. gauss_sum n) n"
proof -
have "periodic_arithmetic χ n" using dir_periodic_arithmetic by simp
let ?h = "λm k. χ(m) * unity_root n (m*k)"
{fix m :: nat
have "periodic_arithmetic (λk. unity_root n (m*k)) n"
using unity_periodic_arithmetic_mult[of n m] by simp
have "periodic_arithmetic (?h m) n"
using scalar_mult_periodic_arithmetic[OF ‹periodic_arithmetic (λk. unity_root n (m*k)) n›]
by blast}
then have per_all: "∀m ∈ {1..n}. periodic_arithmetic (?h m) n" by blast
have "periodic_arithmetic (λk. (∑m = 1..n . χ(m) * unity_root n (m*k))) n"
using fin_sum_periodic_arithmetic_set[OF per_all] by blast
then show ?thesis
unfolding gauss_sum_def by blast
qed

lemma ramanujan_sum_conv_gauss_sum:
assumes "χ = principal_dchar n"
shows "ramanujan_sum n k = gauss_sum k"
proof -
{fix m
from assms
have 1: "coprime m n ⟹ χ(m) = 1" and
2: "¬ coprime m n ⟹ χ(m) = 0"
unfolding principal_dchar_def by auto}
note eq = this

have "gauss_sum k = (∑m = 1..n . χ(m) * unity_root n (m*k))"
unfolding gauss_sum_def by simp
also have "… = (∑m | m ∈ {1..n} ∧ coprime m n . χ(m) * unity_root n (m*k))"
also have "… = (∑m | m ∈ {1..n} ∧ coprime m n . unity_root n (m*k))"
also have "… = ramanujan_sum n k" unfolding ramanujan_sum_def by blast
finally show ?thesis ..
qed

lemma cnj_mult_self:
assumes "coprime k n"
shows "cnj (χ k) * χ k = 1"
proof -
have "cnj (χ k) * χ k = norm (χ k)^2"
by (simp add: mult.commute complex_mult_cnj cmod_def)
also have "… = 1"
using norm[of k] assms by simp
finally show ?thesis .
qed

text ‹Theorem 8.9›
theorem gauss_sum_reduction:
assumes "coprime k n"
shows "gauss_sum k = cnj (χ k) * gauss_sum 1"
proof -
from n have n_pos: "n > 0" by simp
have "gauss_sum k = (∑r = 1..n . χ(r) * unity_root n (r*k))"
unfolding gauss_sum_def by simp
also have "… = (∑r = 1..n . cnj (χ(k)) * χ k * χ r * unity_root n (r*k))"
using assms by (intro sum.cong) (auto simp: cnj_mult_self)
also have "… = (∑r = 1..n . cnj (χ(k)) * χ (k*r) * unity_root n (r*k))"
by (intro sum.cong) auto
also have "… = cnj (χ(k)) * (∑r = 1..n . χ (k*r) * unity_root n (r*k))"
also have "…= cnj (χ(k)) * (∑r = 1..n . χ r * unity_root n r)"
proof -
have 1: "periodic_arithmetic (λr. χ r * unity_root n r) n"
using dir_periodic_arithmetic unity_periodic_arithmetic mult_periodic_arithmetic by blast
have "(∑r = 1..n . χ (k*r) * unity_root n (r*k)) =
(∑r = 1..n . χ (r)* unity_root n r)"
using periodic_arithmetic_remove_homothecy[OF assms(1) 1 n_pos]
then show ?thesis by argo
qed
also have "… = cnj (χ(k)) * gauss_sum 1"
using gauss_sum_def by simp
finally show ?thesis .
qed

text ‹
The following variant takes an integer argument instead.
›
definition "gauss_sum_int k = (∑m=1..n. χ m * unity_root n (int m*k))"

sublocale gauss_sum_int: periodic_fun_simple gauss_sum_int "int n"
proof
fix k
show "gauss_sum_int (k + int n) = gauss_sum_int k"
qed

lemma gauss_sum_int_cong:
assumes "[a = b] (mod int n)"
shows   "gauss_sum_int a = gauss_sum_int b"
proof -
from assms obtain k where k: "b = a + int n * k"
by (subst (asm) cong_iff_lin) auto
thus ?thesis
using gauss_sum_int.plus_of_int[of a k] by (auto simp: algebra_simps)
qed

lemma gauss_sum_conv_gauss_sum_int:
"gauss_sum k = gauss_sum_int (int k)"
unfolding gauss_sum_def gauss_sum_int_def by auto

lemma gauss_sum_int_conv_gauss_sum:
"gauss_sum_int k = gauss_sum (nat (k mod n))"
proof -
have "gauss_sum (nat (k mod n)) = gauss_sum_int (int (nat (k mod n)))"
also have "… = gauss_sum_int k"
using n
by (intro gauss_sum_int_cong) (auto simp: cong_def)
finally show ?thesis ..
qed

lemma gauss_int_periodic: "periodic_arithmetic gauss_sum_int n"
unfolding periodic_arithmetic_def gauss_sum_int_conv_gauss_sum by simp

proposition dcharacter_fourier_expansion:
"χ m = (∑k=1..n. 1 / n * gauss_sum_int (-k) * unity_root n (m*k))"
proof -
define g where "g = (λx. 1 / of_nat n *
(∑m<n. χ m * unity_root n (- int x * int m)))"
have per: "periodic_arithmetic χ n" using dir_periodic_arithmetic by simp
have "χ m = (∑k<n. g k * unity_root n (m * int k))"
using fourier_expansion_periodic_arithmetic(2)[OF _ per, of m] n by (auto simp: g_def)
also have "… = (∑k = 1..n. g k * unity_root n (m * int k))"
proof -
have g_per: "periodic_arithmetic g n"
using fourier_expansion_periodic_arithmetic(1)[OF _ per] n by (simp add: g_def)
have fact_per: "periodic_arithmetic (λk. g k * unity_root n (int m * int k)) n"
using mult_periodic_arithmetic[OF g_per] unity_periodic_arithmetic_mult by auto
show ?thesis
proof -
have "(∑k<n. g k * unity_root n (int m * int k)) =
(∑l = 0..n - Suc 0. g l * unity_root n (int m * int l))"
using n by (intro sum.cong) auto
also have "… = (∑l = Suc 0..n. g l * unity_root n (int m * int l))"
using periodic_arithmetic_sum_periodic_arithmetic_shift[OF fact_per, of 1] n by auto
finally show ?thesis by simp
qed
qed
also have "… = (∑k = 1..n. (1 / of_nat n) * gauss_sum_int (-k) * unity_root n (m*k))"
proof -
{fix k :: nat
have shift: "(∑m<n. χ m * unity_root n (- int k * int m)) =
(∑m = 1..n. χ m * unity_root n (- int k * int m))"
proof -
have per_unit: "periodic_arithmetic (λm. unity_root n (- int k * int m)) n"
using unity_periodic_arithmetic_mult by blast
then have prod_per: "periodic_arithmetic (λm. χ m * unity_root n (- int k * int m)) n"
using per mult_periodic_arithmetic by blast
show ?thesis
proof -
have "(∑m<n. χ m * unity_root n (- int k * int m)) =
(∑l = 0..n - Suc 0. χ l * unity_root n (- int k * int l))"
using n by (intro sum.cong) auto
also have "… = (∑m = 1..n. χ m * unity_root n (- int k * int m))"
using periodic_arithmetic_sum_periodic_arithmetic_shift[OF prod_per, of 1] n by auto
finally show ?thesis by simp
qed
qed
have "g k = 1 / of_nat n *
(∑m<n. χ m * unity_root n (- int k * int m))"
using g_def by auto
also have "… = 1 / of_nat n *
(∑m = 1..n. χ m * unity_root n (- int k * int m))"
using shift by simp
also have "… = 1 / of_nat n * gauss_sum_int (-k)"
unfolding gauss_sum_int_def
finally have "g k = 1 / of_nat n * gauss_sum_int (-k)" by simp}
note g_expr = this
show ?thesis
by (rule sum.cong, simp, simp add: g_expr)
qed
finally show ?thesis by auto
qed

subsection ‹Separability›

definition "separable k ⟷ gauss_sum k = cnj (χ k) * gauss_sum 1"

corollary gauss_coprime_separable:
assumes "coprime k n"
shows   "separable k"
using gauss_sum_reduction[OF assms] unfolding separable_def by simp

text ‹Theorem 8.10›
theorem global_separability_condition:
"(∀n>0. separable n) ⟷ (∀k>0. ¬coprime k n ⟶ gauss_sum k = 0)"
proof -
{fix k
assume "¬ coprime k n"
then have "χ(k) = 0" by (simp add: eq_zero)
then have "cnj (χ k) = 0" by blast
then have "separable k ⟷ gauss_sum k = 0"
unfolding separable_def by auto}
note not_case = this

show ?thesis
using gauss_coprime_separable not_case separable_def by blast
qed

lemma of_real_moebius_mu [simp]: "of_real (moebius_mu k) = moebius_mu k"

corollary principal_not_totally_separable:
assumes "χ = principal_dchar n"
shows "¬(∀k > 0. separable k)"
proof -
have n_pos: "n > 0" using n by simp
have tot_0: "totient n ≠ 0" by (simp add: n_pos)
have "moebius_mu (n div gcd n n) ≠ 0" by (simp add: ‹n > 0›)
then have moeb_0: "∃k. moebius_mu (n div gcd k n) ≠ 0" by blast

have lem: "gauss_sum k = totient n * moebius_mu (n div gcd k n) / totient (n div gcd k n)"
if "k > 0" for k
proof -
have "gauss_sum k = ramanujan_sum n k"
using ramanujan_sum_conv_gauss_sum[OF assms(1)] ..
also have "… = totient n * moebius_mu (n div gcd k n) / (totient (n div gcd k n))"
by (simp add: ramanujan_sum_k_n_dirichlet_expr[OF n_pos that])
finally show ?thesis .
qed
have 2: "¬ coprime n n" using n by auto
have 3: "gauss_sum n ≠ 0"
using lem[OF n_pos] tot_0 moebius_mu_1 by simp
from n_pos 2 3 have
"∃k>0. ¬coprime k n ∧ gauss_sum k ≠ 0" by blast
then obtain k where "k > 0 ∧ ¬ coprime k n ∧ gauss_sum k ≠ 0" by blast
note right_not_zero = this

have "cnj (χ k) * gauss_sum 1 = 0" if "¬coprime k n" for k
using that assms by (simp add: principal_dchar_def)
then show ?thesis
unfolding separable_def using right_not_zero by auto
qed

text ‹Theorem 8.11›
theorem gauss_sum_1_mod_square_eq_k:
assumes "(∀k. k > 0 ⟶ separable k)"
shows "norm (gauss_sum 1) ^ 2 = real n"
proof -
have "(norm (gauss_sum 1))^2 = gauss_sum 1 * cnj (gauss_sum 1)"
using complex_norm_square by blast
also have "… = gauss_sum 1 * (∑m = 1..n. cnj (χ(m)) * unity_root n (-m))"
proof -
have "cnj (gauss_sum 1) = (∑m = 1..n. cnj (χ(m)) * unity_root n (-m))"
unfolding gauss_sum_def by (simp add: unity_root_uminus)
then show ?thesis by argo
qed
also have "… = (∑m = 1..n. gauss_sum 1 * cnj (χ(m)) * unity_root n (-m))"
also have "… = (∑m = 1..n. gauss_sum m * unity_root n (-m))"
proof (rule sum.cong,simp)
fix x
assume as: "x ∈ {1..n}"
show "gauss_sum 1 * cnj (χ x) * unity_root n (-x) =
gauss_sum x * unity_root n (-x)"
using assms(1) unfolding separable_def
by (rule allE[of _ x]) (use as in auto)
qed
also have "… = (∑m = 1..n. (∑r = 1..n. χ r * unity_root n (r*m) * unity_root n (-m)))"
unfolding gauss_sum_def
by (rule sum.cong,simp,rule sum_distrib_right)
also have "… = (∑m = 1..n. (∑r = 1..n. χ r * unity_root n (m*(r-1)) ))"
by (intro sum.cong refl) (auto simp: unity_root_diff of_nat_diff unity_root_uminus field_simps)
also have "… = (∑r=1..n. (∑m=1..n.  χ(r) *unity_root n (m*(r-1))))"
by (rule sum.swap)
also have "… = (∑r=1..n. χ(r) *(∑m=1..n. unity_root n (m*(r-1))))"
by (rule sum.cong, simp, simp add: sum_distrib_left)
also have "… = (∑r=1..n. χ(r) * unity_root_sum n (r-1))"
proof (intro sum.cong refl)
fix x
assume "x ∈ {1..n}"
then have 1: "periodic_arithmetic (λm. unity_root n (int (m * (x - 1)))) n"
using unity_periodic_arithmetic_mult[of n "x-1"]
have "(∑m = 1..n. unity_root n (int (m * (x - 1)))) =
(∑m = 0..n-1. unity_root n (int (m * (x - 1))))"
using periodic_arithmetic_sum_periodic_arithmetic_shift[OF 1 _, of 1] n by simp
also have "… = unity_root_sum n (x-1)"
using n unfolding unity_root_sum_def by (intro sum.cong) (auto simp: mult_ac)
finally have "(∑m = 1..n. unity_root n (int (m * (x - 1)))) =
unity_root_sum n (int (x - 1))" .
then show "χ x * (∑m = 1..n. unity_root n (int (m * (x - 1)))) =
χ x * unity_root_sum n (int (x - 1))" by argo
qed
also have "… = (∑r ∈ {1}. χ r * unity_root_sum n (int (r - 1)))"
using n unity_root_sum_nonzero_iff int_ops(6)
by (intro sum.mono_neutral_right) auto
also have "… = χ 1 * n" using n by simp
also have "… = n" by simp
finally show ?thesis
using of_real_eq_iff by fastforce
qed

text ‹Theorem 8.12›
theorem gauss_sum_nonzero_noncoprime_necessary_condition:
assumes "gauss_sum k ≠ 0" "¬coprime k n" "k > 0"
defines "d ≡ n div gcd k n"
assumes "coprime a n" "[a = 1] (mod d)"
shows   "d dvd n" "d < n" "χ a = 1"
proof -
show "d dvd n"
unfolding d_def using n by (subst div_dvd_iff_mult) auto
from assms(2) have "gcd k n ≠ 1" by blast
then have "gcd k n > 1" using assms(3,4) by (simp add: nat_neq_iff)
with n show "d < n" by (simp add: d_def)

have "periodic_arithmetic (λr. χ (r)* unity_root n (k*r)) n"
using mult_periodic_arithmetic[OF dir_periodic_arithmetic unity_periodic_arithmetic_mult] by auto
then have 1: "periodic_arithmetic (λr. χ (r)* unity_root n (r*k)) n"

have "gauss_sum k = (∑m = 1..n . χ(m) * unity_root n (m*k))"
unfolding gauss_sum_def by blast
also have "… = (∑m = 1..n . χ(m*a) * unity_root n (m*a*k))"
using periodic_arithmetic_remove_homothecy[OF assms(5) 1] n by auto
also have "… = (∑m = 1..n . χ(m*a) * unity_root n (m*k))"
proof (intro sum.cong refl)
fix m
from assms(6) obtain b where "a = 1 + b*d"
using ‹d < n› assms(5) cong_to_1'_nat by auto
then have "m*a*k = m*k+m*b*(n div gcd k n)*k"
also have "… = m*k+m*b*n*(k div gcd k n)"
also obtain p where "… = m*k+m*b*n*p" by blast
finally have "m*a*k = m*k+m*b*p*n" by simp
then have 1: "m*a*k mod n= m*k mod n"
using mod_mult_self1 by simp
then have "unity_root n (m * a * k) = unity_root n (m * k)"
proof -
have "unity_root n (m * a * k) = unity_root n ((m * a * k) mod n)"
using unity_root_mod[of n] zmod_int by simp
also have "… = unity_root n (m * k)"
using unity_root_mod[of n] zmod_int 1 by presburger
finally show ?thesis by blast
qed
then show "χ (m * a) * unity_root n (int (m * a * k)) =
χ (m * a) * unity_root n (int (m * k))" by auto
qed
also have "… = (∑m = 1..n . χ(a) * (χ(m) * unity_root n (m*k)))"
by (rule sum.cong,simp,subst mult,simp)
also have "… =  χ(a) * (∑m = 1..n . χ(m) * unity_root n (m*k))"
also have "… = χ(a) * gauss_sum k"
unfolding gauss_sum_def by blast
finally have "gauss_sum k = χ(a) * gauss_sum k" by blast
then show "χ a = 1"
using assms(1) by simp
qed

subsection ‹Induced moduli and primitive characters›

definition "induced_modulus d ⟷ d dvd n ∧ (∀a. coprime a n ∧ [a = 1] (mod d) ⟶ χ a = 1)"

lemma induced_modulus_dvd: "induced_modulus d ⟹ d dvd n"
unfolding induced_modulus_def by blast

lemma induced_modulusI [intro?]:
"d dvd n ⟹ (⋀a. coprime a n ⟹ [a = 1] (mod d) ⟹ χ a = 1) ⟹ induced_modulus d"
unfolding induced_modulus_def by auto

lemma induced_modulusD: "induced_modulus d ⟹ coprime a n ⟹ [a = 1] (mod d) ⟹ χ a = 1"
unfolding induced_modulus_def by blast

lemma zero_not_ind_mod: "¬induced_modulus 0"
unfolding induced_modulus_def using n by simp

lemma div_gcd_dvd1: "(a :: 'a :: semiring_gcd) div gcd a b dvd a"
by (metis dvd_def dvd_div_mult_self gcd_dvd1)

lemma div_gcd_dvd2: "(b :: 'a :: semiring_gcd) div gcd a b dvd b"
by (metis div_gcd_dvd1 gcd.commute)

lemma g_non_zero_ind_mod:
assumes "gauss_sum k ≠ 0" "¬coprime k n" "k > 0"
shows  "induced_modulus (n div gcd k n)"
proof
show "n div gcd k n dvd n"
by (metis dvd_div_mult_self dvd_triv_left gcd.commute gcd_dvd1)
fix a :: nat
assume "coprime a n" "[a = 1] (mod n div gcd k n)"
thus "χ a = 1"
using assms n gauss_sum_nonzero_noncoprime_necessary_condition(3) by auto
qed

lemma induced_modulus_modulus: "induced_modulus n"
unfolding induced_modulus_def
proof (rule conjI,simp,safe)
fix a
assume "[a = 1] (mod n)"
then have "a mod n = 1 mod n"
using cong_def[of a 1 n] by blast
also have "… = 1"
using eq_zero_iff zero_eq_0 by fastforce
finally have 1: "a mod n = 1" by simp

have "χ a = χ (a mod n)" by simp
also have "… = χ 1" using cong_def 1 by auto
also have "… = 1" by simp
finally show "χ a = 1" by blast
qed

text ‹Theorem 8.13›
theorem one_induced_iff_principal:
"induced_modulus 1 ⟷ χ = principal_dchar n"
proof
assume "induced_modulus 1"
then have "(∀a. coprime a n ⟶ χ a = 1)"
unfolding induced_modulus_def by simp
then show "χ = principal_dchar n"
unfolding principal_dchar_def using eq_zero by auto
next
assume as: "χ = principal_dchar n"
{fix a
assume "coprime a n"
then have "χ a = 1"
using principal_dchar_def as by simp}
then show "induced_modulus 1"
unfolding induced_modulus_def by auto
qed

end

locale primitive_dchar = dcharacter +
assumes no_induced_modulus: "¬(∃d<n. induced_modulus d)"

locale nonprimitive_dchar = dcharacter +
assumes induced_modulus: "∃d<n. induced_modulus d"

lemma (in nonprimitive_dchar) nonprimitive: "¬primitive_dchar n χ"
proof
assume "primitive_dchar n χ"
then interpret A: primitive_dchar n "residue_mult_group n" χ
by auto
from A.no_induced_modulus induced_modulus show False by contradiction
qed

lemma (in dcharacter) primitive_dchar_iff:
"primitive_dchar n χ ⟷ ¬(∃d<n. induced_modulus d)"
unfolding primitive_dchar_def primitive_dchar_axioms_def
using dcharacter_axioms by metis

lemma (in residues_nat) principal_not_primitive:
"¬primitive_dchar n (principal_dchar n)"
unfolding principal.primitive_dchar_iff
using principal.one_induced_iff_principal n by auto

lemma (in dcharacter) not_primitive_imp_nonprimitive:
assumes "¬primitive_dchar n χ"
shows   "nonprimitive_dchar n χ"
using assms dcharacter_axioms
unfolding nonprimitive_dchar_def primitive_dchar_def
primitive_dchar_axioms_def nonprimitive_dchar_axioms_def by auto

text ‹Theorem 8.14›
theorem (in dcharacter) prime_nonprincipal_is_primitive:
assumes "prime n"
assumes "χ ≠ principal_dchar n"
shows   "primitive_dchar n χ"
proof -
{fix m
assume "induced_modulus m"
then have "m = n"
using assms prime_nat_iff induced_modulus_def
one_induced_iff_principal by blast}
then show ?thesis using primitive_dchar_iff by blast
qed

text ‹Theorem 8.15›
corollary (in primitive_dchar) primitive_encoding:
"∀k>0. ¬coprime k n ⟶ gauss_sum k = 0"
"∀k>0. separable k"
"norm (gauss_sum 1) ^ 2 = n"
proof safe
show 1: "gauss_sum k = 0" if "k > 0" and "¬coprime k n" for k
proof (rule ccontr)
assume "gauss_sum k ≠ 0"
hence "induced_modulus (n div gcd k n)"
using that by (intro g_non_zero_ind_mod) auto
moreover have "n div gcd k n < n"
using n that
by (meson coprime_iff_gcd_eq_1 div_eq_dividend_iff le_less_trans
linorder_neqE_nat nat_dvd_not_less principal.div_gcd_dvd2 zero_le_one)
ultimately show False using no_induced_modulus by blast
qed

have "(∀n>0. separable n)"
unfolding global_separability_condition by (auto intro!: 1)
thus "separable n" if "n > 0" for n
using that by blast
thus "norm (gauss_sum 1) ^ 2 = n"
using gauss_sum_1_mod_square_eq_k by blast
qed

text ‹Theorem 8.16›
lemma (in dcharacter) induced_modulus_altdef1:
"induced_modulus d ⟷
d dvd n ∧ (∀a b. coprime a n ∧ coprime b n ∧ [a = b] (mod d) ⟶ χ a = χ b)"
proof
assume 1: "induced_modulus d"
with n have d: "d dvd n" "d > 0"
by (auto simp: induced_modulus_def intro: Nat.gr0I)
show " d dvd n ∧ (∀a b. coprime a n ∧ coprime b n ∧ [a = b] (mod d) ⟶ χ(a) = χ(b))"
proof safe
fix a b
assume 2: "coprime a n" "coprime b n" "[a = b] (mod d)"
show "χ(a) = χ(b)"
proof -
from 2(1) obtain a' where eq: "[a*a' = 1] (mod n)"
using cong_solve by blast
from this d have "[a*a' = 1] (mod d)"
using cong_dvd_modulus_nat by blast
from this 1 have "χ(a*a') = 1"
unfolding induced_modulus_def
by (meson "2"(2) eq cong_imp_coprime cong_sym coprime_divisors gcd_nat.refl one_dvd)
then have 3: "χ(a)*χ(a') = 1"
by simp

from 2(3) have "[a*a' = b*a'] (mod d)"
moreover have 4: "[b*a' = 1] (mod d)"
using ‹[a * a' = 1] (mod d)› calculation cong_sym cong_trans by blast
have "χ(b*a') = 1"
proof -
have "coprime (b*a') n"
using "2"(2) cong_imp_coprime[OF cong_sym[OF eq]] by simp
then show ?thesis using 4 induced_modulus_def 1 by blast
qed
then have 4: "χ(b)*χ(a') = 1"
by simp
from 3 4 show "χ(a) = χ(b)"
using mult_cancel_left
by (cases "χ(a') = 0") (fastforce simp add: field_simps)+
qed
qed fact+
next
assume *: "d dvd n ∧ (∀a b. coprime a n ∧ coprime b n ∧ [a = b] (mod d) ⟶ χ a = χ b)"
then have "∀a . coprime a n ∧ coprime 1 n ∧ [a = 1] (mod d) ⟶ χ a = χ 1"
by blast
then have "∀a . coprime a n ∧ [a = 1] (mod d) ⟶ χ a = 1"
using coprime_1_left by simp
then show "induced_modulus d"
unfolding induced_modulus_def using * by blast
qed

text ‹Exercise 8.4›

lemma induced_modulus_altdef2_lemma:
fixes n a d q :: nat
defines "q ≡ (∏ p | prime p ∧ p dvd n ∧ ¬ (p dvd a). p)"
defines "m ≡ a + q * d"
assumes "n > 0" "coprime a d"
shows "[m = a] (mod d)" and "coprime m n"
have fin: "finite {p. prime p ∧ p dvd n ∧ ¬ (p dvd a)}" by (simp add: assms)
{ fix p
assume 4: "prime p" "p dvd m" "p dvd n"
have "p = 1"
proof (cases "p dvd a")
case True
from this assms 4(2) have "p dvd q*d"
then have a1: "p dvd q ∨ p dvd d"
using 4(1) prime_dvd_mult_iff by blast

have a2: "¬ (p dvd q)"
proof (rule ccontr,simp)
assume "p dvd q"
then have "p dvd (∏ p | prime p ∧ p dvd n ∧ ¬ (p dvd a). p)"
unfolding assms by simp
then have "∃x∈{p. prime p ∧ p dvd n ∧ ¬ p dvd a}. p dvd x"
using prime_dvd_prod_iff[OF fin 4(1)] by simp
then obtain x where c: "p dvd x ∧ prime x ∧ ¬ x dvd a" by blast
then have "p = x" using 4(1) by (simp add: primes_dvd_imp_eq)
then show "False" using True c by auto
qed
have a3: "¬ (p dvd d)"
using True assms "4"(1) coprime_def not_prime_unit by auto

from a1 a2 a3 show ?thesis by simp
next
case False
then have "p dvd q"
proof -
have in_s: "p ∈ {p. prime p ∧ p dvd n ∧ ¬ p dvd a}"
using False 4(3) 4(1) by simp
show "p dvd q"
unfolding assms using dvd_prodI[OF fin in_s ] by fast
qed
then have "p dvd q*d" by simp
then have "p dvd a" using 4(2) assms
then show ?thesis using False by auto
qed
}
note lem = this
show "coprime m n"
proof (subst coprime_iff_gcd_eq_1)
{fix a
assume "a dvd m" "a dvd n" "a ≠ 1"
{fix p
assume "prime p" "p dvd a"
then have "p dvd m" "p dvd n"
using ‹a dvd m› ‹a dvd n› by auto
from lem have "p = a"
using not_prime_1 ‹prime p› ‹p dvd m› ‹p dvd n› by blast}
then have "prime a"
using prime_prime_factor[of a] ‹a ≠ 1› by blast
then have "a = 1" using lem ‹a dvd m› ‹a dvd n› by blast
then have "False" using ‹a = 1› ‹a ≠ 1› by blast
}
then show "gcd m n = 1" by blast
qed
qed

text ‹Theorem 8.17›
text‹The case ‹d = 1› is exactly the case described in @{thm dcharacter.one_induced_iff_principal}.›
theorem (in dcharacter) induced_modulus_altdef2:
assumes "d dvd n" "d ≠ 1"
defines "χ⇩1 ≡ principal_dchar n"
shows "induced_modulus d ⟷ (∃Φ. dcharacter d Φ ∧ (∀k. χ k = Φ k * χ⇩1 k))"
proof
from n have n_pos: "n > 0" by simp
assume as_im: "induced_modulus d"
define f where
"f ≡ (λk. k +
(if k = 1 then
0
else (prod id {p. prime p ∧ p dvd n ∧ ¬ (p dvd k)})*d)
)"
have [simp]: "f (Suc 0) = 1" unfolding f_def by simp
{
fix k
assume as: "coprime k d"
hence "[f k = k] (mod d)" "coprime (f k) n"
using induced_modulus_altdef2_lemma[OF n_pos as] by (simp_all add: f_def)
}
note m_prop = this

define Φ where
"Φ ≡ (λn. (if ¬ coprime n d then 0 else χ(f n)))"

have Φ_1: "Φ 1 = 1"
unfolding Φ_def by simp

from assms(1,2) n have "d > 0" by (intro Nat.gr0I) auto
from induced_modulus_altdef1 assms(1) ‹d > 0› as_im
have b: "(∀a b. coprime a n ∧ coprime b n ∧
[a = b] (mod d) ⟶ χ a = χ b)" by blast

have Φ_periodic:  " ∀a. Φ (a + d) = Φ a"
proof
fix a
have "gcd (a+d) d = gcd a d" by auto
then have cop: "coprime (a+d) d = coprime a d"
using coprime_iff_gcd_eq_1 by presburger
show "Φ (a + d) = Φ a"
proof (cases "coprime a d")
case True
from True cop have cop_ad: "coprime (a+d) d" by blast
have p1: "[f (a+d) = f a] (mod d)"
m_prop(1)[of "a",OF True] by (simp add: cong_def)
have p2: "coprime (f (a+d)) n" "coprime (f a) n"
m_prop(2)[of "a", OF True] by blast+
from b p1 p2 have eq: "χ (f (a + d)) = χ (f a)" by blast
show ?thesis
unfolding Φ_def
by (subst cop,simp,safe, simp add: eq)
next
case False
then show ?thesis unfolding Φ_def by (subst cop,simp)
qed
qed

have Φ_mult: "∀a b. a ∈ totatives d ⟶
b ∈ totatives d ⟶ Φ (a * b) = Φ a * Φ b"
proof (safe)
fix a b
assume "a ∈ totatives d" "b ∈ totatives d"
consider (ab) "coprime a d ∧ coprime b d" |
(a)  "coprime a d ∧ ¬ coprime b d" |
(b)  "coprime b d ∧ ¬ coprime a d" |
(n)  "¬ coprime a d ∧ ¬ coprime b d" by blast
then show "Φ (a * b) = Φ a * Φ b"
proof cases
case ab
then have c_ab:
"coprime (a*b) d" "coprime a d" "coprime b d" by simp+
then have p1: "[f (a * b) = a * b] (mod d)" "coprime (f (a * b)) n"
using m_prop[of "a*b", OF c_ab(1)] by simp+
moreover have p2: "[f a = a] (mod d)" "coprime (f a) n"
"[f b = b] (mod d)" "coprime (f b) n"
using m_prop[of "a",OF c_ab(2)]
m_prop[of "b",OF c_ab(3) ] by simp+
have p1s: "[f (a * b) = (f a) * (f b)] (mod d)"
proof -
have "[f (a * b) = a * b] (mod d)"
using p1(1) by blast
moreover have "[a * b = f(a) * f(b)] (mod d)"
using p2(1) p2(3) by (simp add: cong_mult cong_sym)
ultimately show ?thesis using cong_trans by blast
qed
have p2s: "coprime (f a*f b) n"
using p2(2) p2(4) by simp
have "χ (f (a * b)) = χ (f a * f b)"
using p1s p2s p1(2) b by blast
then show ?thesis
unfolding Φ_def by (simp add: c_ab)
qed
have d_gr_1: "d > 1" using assms(1,2)
using ‹0 < d› by linarith
show "∃Φ. dcharacter d Φ ∧ (∀n. χ n = Φ n * χ⇩1 n)"
proof (standard,rule conjI)
show "dcharacter d Φ"
unfolding dcharacter_def residues_nat_def dcharacter_axioms_def
using d_gr_1 Φ_def f_def Φ_mult Φ_1 Φ_periodic by simp
show "∀n. χ n = Φ n * χ⇩1 n"
proof
fix k
show "χ k = Φ k * χ⇩1 k"
proof (cases "coprime k n")
case True
then have "coprime k d" using assms(1) by auto
then have "Φ(k) = χ(f k)" using Φ_def by simp
moreover have "[f k = k] (mod d)"
using m_prop[OF ‹coprime k d›] by simp
moreover have "χ⇩1 k = 1"
using assms(3) principal_dchar_def ‹coprime k n› by auto
ultimately show "χ(k) = Φ(k) * χ⇩1(k)"
proof -
assume "Φ k = χ (f k)" "[f k = k] (mod d)" "χ⇩1 k = 1"
then have "χ k = χ (f k)"
using ‹local.induced_modulus d› induced_modulus_altdef1 assms(1) ‹d > 0›
True ‹coprime k d› m_prop(2) by auto
also have "… = Φ k" by (simp add: ‹Φ k = χ (f k)›)
also have "… = Φ k * χ⇩1 k" by (simp add: ‹χ⇩1 k = 1›)
finally show ?thesis by simp
qed
next
case False
hence "χ k = 0"
using eq_zero_iff by blast
moreover have "χ⇩1 k = 0"
using False assms(3) principal_dchar_def by simp
ultimately show ?thesis by simp
qed
qed
qed
next
assume "(∃Φ. dcharacter d Φ ∧ (∀k. χ k = Φ k * χ⇩1 k))"
then obtain Φ where 1: "dcharacter d Φ" "(∀k. χ k = Φ k * χ⇩1 k)" by blast
show "induced_modulus d"
unfolding induced_modulus_def
proof (rule conjI,fact,safe)
fix k
assume 2: "coprime k n" "[k = 1] (mod d)"
then have "χ⇩1 k = 1" "Φ k = 1"
have "Φ k = Φ (k mod d)" by (simp add: dcharacter.mod[OF 1(1), of k])
also have "… = Φ (1 mod d)" using cong_def[of k 1 d] 2(2) by simp
also have "… = Φ 1" using assms(2) "1"(1) dcharacter.mod by blast
also have "… = 1" using dcharacter.Suc_0[OF 1(1)] by simp
finally show "Φ k = 1" by simp
qed
then show "χ k = 1" using 1(2) by simp
qed
qed

subsection ‹The conductor of a character›

context dcharacter
begin

definition "conductor = Min {d. induced_modulus d}"

lemma conductor_fin: "finite {d. induced_modulus d}"
proof -
let ?A = "{d. induced_modulus d}"
have "?A ⊆ {d. d dvd n}"
unfolding induced_modulus_def by blast
moreover have "finite {d. d dvd n}" using n by simp
ultimately show "finite ?A" using finite_subset by auto
qed

lemma conductor_induced: "induced_modulus conductor"
proof -
have "{d. induced_modulus d} ≠ {}" using induced_modulus_modulus by blast
then show "induced_modulus conductor"
using Min_in[OF conductor_fin ] conductor_def by auto
qed

lemma conductor_le_iff: "conductor ≤ a ⟷ (∃d≤a. induced_modulus d)"
unfolding conductor_def using conductor_fin induced_modulus_modulus by (subst Min_le_iff) auto

lemma conductor_ge_iff: "conductor ≥ a ⟷ (∀d. induced_modulus d ⟶ d ≥ a)"
unfolding conductor_def using conductor_fin induced_modulus_modulus by (subst Min_ge_iff) auto

lemma conductor_leI: "induced_modulus d ⟹ conductor ≤ d"
by (subst conductor_le_iff) auto

lemma conductor_geI: "(⋀d. induced_modulus d ⟹ d ≥ a) ⟹ conductor ≥ a"
by (subst conductor_ge_iff) auto

lemma conductor_dvd: "conductor dvd n"
using conductor_induced unfolding induced_modulus_def by blast

lemma conductor_le_modulus: "conductor ≤ n"
using conductor_dvd by (rule dvd_imp_le) (use n in auto)

lemma conductor_gr_0: "conductor > 0"
unfolding conductor_def using zero_not_ind_mod
using conductor_def conductor_induced neq0_conv by fastforce

lemma conductor_eq_1_iff_principal: "conductor = 1 ⟷ χ = principal_dchar n"
proof
assume "conductor = 1"
then have "induced_modulus 1"
using conductor_induced by auto
then show "χ = principal_dchar n"
using one_induced_iff_principal by blast
next
assume "χ = principal_dchar n"
then have im_1: "induced_modulus 1" using one_induced_iff_principal by auto
show "conductor = 1"
proof -
have "conductor ≤ 1"
using conductor_fin Min_le[OF conductor_fin,simplified,OF im_1]
then show ?thesis using conductor_gr_0 by auto
qed
qed

lemma conductor_principal [simp]: "χ = principal_dchar n ⟹ conductor = 1"
by (subst conductor_eq_1_iff_principal)

lemma nonprimitive_imp_conductor_less:
assumes "¬primitive_dchar n χ"
shows "conductor < n"
proof -
obtain d where d: "induced_modulus d" "d < n"
using primitive_dchar_iff assms by blast
from d(1) have "conductor ≤ d"
by (rule conductor_leI)
also have "… < n" by fact
finally show ?thesis .
qed

lemma (in nonprimitive_dchar) conductor_less_modulus: "conductor < n"
using nonprimitive_imp_conductor_less nonprimitive by metis

text ‹Theorem 8.18›
theorem primitive_principal_form:
defines "χ⇩1 ≡ principal_dchar n"
assumes "χ ≠ principal_dchar n"
shows "∃Φ. primitive_dchar conductor Φ ∧ (∀n. χ(n) = Φ(n) * χ⇩1(n))"
proof -
(*
TODO: perhaps residues_nat should be relaxed to allow n = 1.
Then we could remove the unnecessary precondition here.
It makes no real difference though.
*)
from n have n_pos: "n > 0" by simp
define d where "d = conductor"
have induced: "induced_modulus d"
unfolding d_def using conductor_induced by blast
then have d_not_1: "d ≠ 1"
using one_induced_iff_principal assms by auto
hence d_gt_1: "d > 1" using conductor_gr_0 by (auto simp: d_def)

from induced obtain Φ where Φ_def: "dcharacter d Φ ∧ (∀n. χ n = Φ n * χ⇩1 n)"
using d_not_1
by (subst (asm) induced_modulus_altdef2) (auto simp: d_def conductor_dvd χ⇩1_def)
have phi_dchars: "Φ ∈ dcharacters d" using Φ_def dcharacters_def by auto

interpret Φ: dcharacter d "residue_mult_group d" Φ
using Φ_def by auto

have Φ_prim: "primitive_dchar d Φ"
proof (rule ccontr)
assume "¬ primitive_dchar d Φ"
then obtain q where
1: "q dvd d ∧ q < d ∧ Φ.induced_modulus q"
unfolding Φ.induced_modulus_def Φ.primitive_dchar_iff by blast
then have 2: "induced_modulus q"
proof -
{fix k
assume mod_1: "[k = 1] (mod q)"
assume cop: "coprime k n"
have "χ(k) = Φ(k)*χ⇩1(k)" using Φ_def by auto
also have "… = Φ(k)"
using cop by (simp add: assms principal_dchar_def)
also have "… = 1"
using 1 mod_1 Φ.induced_modulus_def
‹induced_modulus d› cop induced_modulus_def by auto
finally have "χ(k) = 1" by blast}

then show ?thesis
using induced_modulus_def "1" ‹induced_modulus d› by auto
qed

from 1 have "q < d" by simp
moreover have "d ≤ q" unfolding d_def
by (intro conductor_leI) fact
ultimately show False by linarith
qed

from Φ_def Φ_prim d_def phi_dchars show ?thesis by blast
qed

definition primitive_extension :: "nat ⇒ complex" where
"primitive_extension =
(SOME Φ. primitive_dchar conductor Φ ∧ (∀k. χ k = Φ k * principal_dchar n k))"

lemma
assumes nonprincipal: "χ ≠ principal_dchar n"
shows primitive_primitive_extension: "primitive_dchar conductor primitive_extension"
and principal_decomposition:       "χ k = primitive_extension k * principal_dchar n k"
proof -
note * = someI_ex[OF primitive_principal_form[OF nonprincipal], folded primitive_extension_def]
from * show "primitive_dchar conductor primitive_extension" by blast
from * show "χ k = primitive_extension k * principal_dchar n k" by blast
qed

end

subsection ‹The connection between primitivity and separability›

lemma residue_mult_group_coset:
fixes m n m1 m2 :: nat and f :: "nat ⇒ nat" and G H
defines "G ≡ residue_mult_group n"
defines "H ≡ residue_mult_group m"
defines "f ≡ (λk. k mod m)"
assumes "b ∈ (rcosets⇘G⇙ kernel G H f)"
assumes "m1 ∈ b" "m2 ∈ b"
assumes "n > 1" "m dvd n"
shows "m1 mod m = m2 mod m"
proof -
have h_1: "𝟭⇘H⇙ = 1"
using assms(2) unfolding residue_mult_group_def totatives_def by simp

from assms(4)
obtain a :: nat where cos_expr: "b = (kernel G H f) #>⇘G⇙ a ∧ a ∈ carrier G"
using RCOSETS_def[of G "kernel G H f"] by blast
then have cop: "coprime a n"
using assms(1) unfolding residue_mult_group_def totatives_def by auto

obtain a'