Theory Dirichlet_Characters
section ‹Dirichlet Characters›
theory Dirichlet_Characters
imports
Multiplicative_Characters
"HOL-Number_Theory.Residues"
"Dirichlet_Series.Multiplicative_Function"
begin
text ‹
Dirichlet characters are essentially just the characters of the multiplicative group of
integer residues $\mathbb{ZZ}/n\mathbb{ZZ}$ for some fixed $n$. For convenience, these residues
are usually represented by natural numbers from $0$ to $n - 1$, and we extend the characters to
all natural numbers periodically, so that $\chi(k\mod n) = \chi(k)$ holds.
Numbers that are not coprime to $n$ are not in the group and therefore are assigned $0$ by
all characters.
›
subsection ‹The multiplicative group of residues›
definition residue_mult_group :: "nat ⇒ nat monoid" where
"residue_mult_group n = ⦇ carrier = totatives n, monoid.mult = (λx y. (x * y) mod n), one = 1 ⦈"
definition principal_dchar :: "nat ⇒ nat ⇒ complex" where
"principal_dchar n = (λk. if coprime k n then 1 else 0)"
lemma principal_dchar_coprime [simp]: "coprime k n ⟹ principal_dchar n k = 1"
and principal_dchar_not_coprime [simp]: "¬coprime k n ⟹ principal_dchar n k = 0"
by (simp_all add: principal_dchar_def)
lemma principal_dchar_1 [simp]: "principal_dchar n 1 = 1"
by simp
lemma principal_dchar_minus1 [simp]:
assumes "n > 0"
shows "principal_dchar n (n - Suc 0) = 1"
proof (cases "n = 1")
case False
with assms have "n > 1" by linarith
thus ?thesis using coprime_diff_one_left_nat[of n]
by (intro principal_dchar_coprime) auto
qed auto
lemma mod_in_totatives: "n > 1 ⟹ a mod n ∈ totatives n ⟷ coprime a n"
by (auto simp: totatives_def mod_greater_zero_iff_not_dvd dest: coprime_common_divisor_nat)
bundle dcharacter_syntax
begin
notation principal_dchar ("χ⇩0ı")
end
locale residues_nat =
fixes n :: nat (structure) and G
assumes n: "n > 1"
defines "G ≡ residue_mult_group n"
begin
lemma order [simp]: "order G = totient n"
by (simp add: order_def G_def totient_def residue_mult_group_def)
lemma totatives_mod [simp]: "x ∈ totatives n ⟹ x mod n = x"
using n by (intro mod_less) (auto simp: totatives_def intro!: order.not_eq_order_implies_strict)
lemma principal_dchar_minus1 [simp]: "principal_dchar n (n - Suc 0) = 1"
using principal_dchar_minus1[of n] n by simp
sublocale finite_comm_group G
proof
fix x y assume xy: "x ∈ carrier G" "y ∈ carrier G"
hence "coprime (x * y) n"
by (auto simp: G_def residue_mult_group_def totatives_def)
with xy and n show "x ⊗⇘G⇙ y ∈ carrier G"
using coprime_common_divisor_nat[of "x * y" n]
by (auto simp: G_def residue_mult_group_def totatives_def
mod_greater_zero_iff_not_dvd le_Suc_eq simp del: coprime_mult_left_iff)
next
fix x y z assume xyz: "x ∈ carrier G" "y ∈ carrier G" "z ∈ carrier G"
thus "x ⊗⇘G⇙ y ⊗⇘G⇙ z = x ⊗⇘G⇙ (y ⊗⇘G⇙ z)"
by (auto simp: G_def residue_mult_group_def mult_ac mod_mult_right_eq)
next
fix x assume "x ∈ carrier G"
with n have "x < n" by (auto simp: G_def residue_mult_group_def totatives_def
intro!: order.not_eq_order_implies_strict)
thus " 𝟭⇘G⇙ ⊗⇘G⇙ x = x" and "x ⊗⇘G⇙ 𝟭⇘G⇙ = x"
by (simp_all add: G_def residue_mult_group_def)
next
have "x ∈ Units G" if "x ∈ carrier G" for x unfolding Units_def
proof safe
from that have "x > 0" "coprime x n"
by (auto simp: G_def residue_mult_group_def totatives_def)
from ‹coprime x n› and n obtain y where y: "y < n" "[x * y = 1] (mod n)"
by (subst (asm) coprime_iff_invertible'_nat) auto
hence "x * y mod n = 1"
using n by (simp add: cong_def mult_ac)
moreover from y have "coprime y n"
by (subst coprime_iff_invertible_nat) (auto simp: mult.commute)
ultimately show "∃a∈carrier G. a ⊗⇘G⇙ x = 𝟭⇘G⇙ ∧ x ⊗⇘G⇙ a = 𝟭⇘G⇙" using y
by (intro bexI[of _ y])
(auto simp: G_def residue_mult_group_def totatives_def mult.commute intro!: Nat.gr0I)
qed fact+
thus "carrier G ⊆ Units G" ..
qed (insert n, auto simp: G_def residue_mult_group_def mult_ac)
subsection ‹Definition of Dirichlet characters›
text ‹
The following two functions make the connection between Dirichlet characters and the
multiplicative characters of the residue group.
›
definition c2dc :: "(nat ⇒ complex) ⇒ (nat ⇒ complex)" where
"c2dc χ = (λx. χ (x mod n))"
definition dc2c :: "(nat ⇒ complex) ⇒ (nat ⇒ complex)" where
"dc2c χ = (λx. if x < n then χ x else 0)"
lemma dc2c_c2dc [simp]:
assumes "character G χ"
shows "dc2c (c2dc χ) = χ"
proof -
interpret character G χ by fact
show ?thesis
using n by (auto simp: fun_eq_iff dc2c_def c2dc_def char_eq_0_iff G_def
residue_mult_group_def totatives_def)
qed
end
locale dcharacter = residues_nat +
fixes χ :: "nat ⇒ complex"
assumes mult_aux: "a ∈ totatives n ⟹ b ∈ totatives n ⟹ χ (a * b) = χ a * χ b"
assumes eq_zero: "¬coprime a n ⟹ χ a = 0"
assumes periodic: "χ (a + n) = χ a"
assumes one_not_zero: "χ 1 ≠ 0"
begin
lemma zero_eq_0 [simp]: "χ 0 = 0"
using n by (intro eq_zero) auto
lemma Suc_0 [simp]: "χ (Suc 0) = 1"
using n mult_aux[of 1 1] one_not_zero by (simp add: totatives_def)
lemma periodic_mult: "χ (a + m * n) = χ a"
proof (induction m)
case (Suc m)
have "a + Suc m * n = a + m * n+ n" by simp
also have "χ … = χ (a + m * n)" by (rule periodic)
also have "… = χ a" by (rule Suc.IH)
finally show ?case .
qed simp_all
lemma minus_one_periodic [simp]:
assumes "k > 0"
shows "χ (k * n - 1) = χ (n - 1)"
proof -
have "k * n - 1 = n - 1 + (k - 1) * n"
using assms n by (simp add: algebra_simps)
also have "χ … = χ (n - 1)"
by (rule periodic_mult)
finally show ?thesis .
qed
lemma cong:
assumes "[a = b] (mod n)"
shows "χ a = χ b"
proof -
from assms obtain k1 k2 where *: "b + k1 * n = a + k2 * n"
by (subst (asm) cong_iff_lin_nat) auto
have "χ a = χ (a + k2 * n)" by (rule periodic_mult [symmetric])
also note * [symmetric]
also have "χ (b + k1 * n) = χ b" by (rule periodic_mult)
finally show ?thesis .
qed
lemma mod [simp]: "χ (a mod n) = χ a"
by (rule cong) (simp_all add: cong_def)
lemma mult [simp]: "χ (a * b) = χ a * χ b"
proof (cases "coprime a n ∧ coprime b n")
case True
hence "a mod n ∈ totatives n" "b mod n ∈ totatives n"
using n by (auto simp: totatives_def mod_greater_zero_iff_not_dvd coprime_absorb_right)
hence "χ ((a mod n) * (b mod n)) = χ (a mod n) * χ (b mod n)"
by (rule mult_aux)
also have "χ ((a mod n) * (b mod n)) = χ (a * b)"
by (rule cong) (auto simp: cong_def mod_mult_eq)
finally show ?thesis by simp
next
case False
hence "¬coprime (a * b) n" by simp
with False show ?thesis by (auto simp: eq_zero)
qed
sublocale mult: completely_multiplicative_function χ
by standard auto
lemma eq_zero_iff: "χ x = 0 ⟷ ¬coprime x n"
proof safe
assume "χ x = 0" and "coprime x n"
from cong_solve_coprime_nat [OF this(2)]
obtain y where "[x * y = Suc 0] (mod n)" by blast
hence "χ (x * y) = χ (Suc 0)" by (rule cong)
with ‹χ x = 0› show False by simp
qed (auto simp: eq_zero)
lemma minus_one': "χ (n - 1) ∈ {-1, 1}"
proof -
define n' where "n' = n - 2"
have n: "n = Suc (Suc n')" using n by (simp add: n'_def)
have "(n - 1) ^ 2 = 1 + (n - 2) * n"
by (simp add: power2_eq_square algebra_simps n)
also have "χ … = 1"
by (subst periodic_mult) auto
also have "χ ((n - 1) ^ 2) = χ (n - 1) ^ 2"
by (rule mult.power)
finally show ?thesis
by (subst (asm) power2_eq_1_iff) auto
qed
lemma c2dc_dc2c [simp]: "c2dc (dc2c χ) = χ"
using n by (auto simp: c2dc_def dc2c_def fun_eq_iff intro!: cong simp: cong_def)
lemma character_dc2c: "character G (dc2c χ)"
by standard (insert n, auto simp: G_def residue_mult_group_def dc2c_def totatives_def
intro!: eq_zero)
sublocale dc2c: character G "dc2c χ"
by (fact character_dc2c)
lemma dcharacter_inv_character [intro]: "dcharacter n (inv_character χ)"
by standard (auto simp: inv_character_def eq_zero periodic)
lemma norm: "norm (χ k) = (if coprime k n then 1 else 0)"
proof -
have "χ k = χ (k mod n)" by (intro cong) (auto simp: cong_def)
also from n have "… = dc2c χ (k mod n)" by (simp add: dc2c_def)
also from n have "norm … = (if coprime k n then 1 else 0)"
by (subst dc2c.norm_char) (auto simp: G_def residue_mult_group_def mod_in_totatives)
finally show ?thesis .
qed
lemma norm_le_1: "norm (χ k) ≤ 1"
by (subst norm) auto
end
definition dcharacters :: "nat ⇒ (nat ⇒ complex) set" where
"dcharacters n = {χ. dcharacter n χ}"
context residues_nat
begin
lemma character_dc2c: "dcharacter n χ ⟹ character G (dc2c χ)"
using dcharacter.character_dc2c[of n χ] by (simp add: G_def)
lemma dcharacter_c2dc:
assumes "character G χ"
shows "dcharacter n (c2dc χ)"
proof -
interpret character G χ by fact
show ?thesis
proof
fix x assume "¬coprime x n"
thus "c2dc χ x = 0"
by (auto simp: c2dc_def char_eq_0_iff G_def residue_mult_group_def totatives_def)
qed (insert char_mult char_one n,
auto simp: c2dc_def G_def residue_mult_group_def simp del: char_mult char_one)
qed
lemma principal_dchar_altdef: "principal_dchar n = c2dc (principal_char G)"
using n by (auto simp: c2dc_def principal_dchar_def principal_char_def G_def
residue_mult_group_def fun_eq_iff mod_in_totatives)
sublocale principal: dcharacter n G "principal_dchar n"
by (simp add: principal_dchar_altdef dcharacter_c2dc | rule G_def)+
lemma c2dc_principal [simp]: "c2dc (principal_char G) = principal_dchar n"
by (simp add: principal_dchar_altdef)
lemma dc2c_principal [simp]: "dc2c (principal_dchar n) = principal_char G"
proof -
have "dc2c (c2dc (principal_char G)) = dc2c (principal_dchar n)"
by (subst c2dc_principal) (rule refl)
thus ?thesis by (subst (asm) dc2c_c2dc) simp_all
qed
lemma bij_betw_dcharacters_characters:
"bij_betw dc2c (dcharacters n) (characters G)"
by (intro bij_betwI[where ?g = c2dc])
(auto simp: characters_def dcharacters_def dcharacter_c2dc
character_dc2c dcharacter.c2dc_dc2c)
lemma bij_betw_characters_dcharacters:
"bij_betw c2dc (characters G) (dcharacters n)"
by (intro bij_betwI[where ?g = dc2c])
(auto simp: characters_def dcharacters_def dcharacter_c2dc
character_dc2c dcharacter.c2dc_dc2c)
lemma finite_dcharacters [intro]: "finite (dcharacters n)"
using bij_betw_finite [OF bij_betw_dcharacters_characters] by auto
lemma card_dcharacters [simp]: "card (dcharacters n) = totient n"
using bij_betw_same_card [OF bij_betw_dcharacters_characters] card_characters by simp
end
lemma inv_character_eq_principal_dchar_iff [simp]:
"inv_character χ = principal_dchar n ⟷ χ = principal_dchar n"
by (auto simp add: fun_eq_iff inv_character_def principal_dchar_def)
subsection ‹Sums of Dirichlet characters›
lemma (in dcharacter) sum_dcharacter_totatives:
"(∑x∈totatives n. χ x) = (if χ = principal_dchar n then of_nat (totient n) else 0)"
proof -
from n have "(∑x∈totatives n. χ x) = (∑x∈carrier G. dc2c χ x)"
by (intro sum.cong) (auto simp: totatives_def dc2c_def G_def residue_mult_group_def)
also have "… = (if dc2c χ = principal_char G then of_nat (order G) else 0)"
by (rule dc2c.sum_character)
also have "dc2c χ = principal_char G ⟷ χ = principal_dchar n"
by (metis c2dc_dc2c dc2c_principal principal_dchar_altdef)
finally show ?thesis by simp
qed
lemma (in dcharacter) sum_dcharacter_block:
"(∑x<n. χ x) = (if χ = principal_dchar n then of_nat (totient n) else 0)"
proof -
from n have "(∑x<n. χ x) = (∑x∈totatives n. χ x)"
by (intro sum.mono_neutral_right)
(auto simp: totatives_def eq_zero_iff intro!: Nat.gr0I order.not_eq_order_implies_strict)
also have "… = (if χ = principal_dchar n then of_nat (totient n) else 0)"
by (rule sum_dcharacter_totatives)
finally show ?thesis .
qed
lemma (in dcharacter) sum_dcharacter_block':
"sum χ {Suc 0..n} = (if χ = principal_dchar n then of_nat (totient n) else 0)"
proof -
let ?f = "λk. if k = n then 0 else k" and ?g = "λk. if k = 0 then n else k"
have "sum χ {1..n} = sum χ {..<n}"
using n by (intro sum.reindex_bij_witness[where j = ?f and i = ?g]) (auto simp: eq_zero_iff)
thus ?thesis by (simp add: sum_dcharacter_block)
qed
lemma (in dcharacter) sum_lessThan_dcharacter:
assumes "χ ≠ principal_dchar n"
shows "(∑x<m. χ x) = (∑x<m mod n. χ x)"
proof (induction m rule: less_induct)
case (less m)
show ?case
proof (cases "m < n")
case True
thus ?thesis by simp
next
case False
hence "{..<m} = {..<n} ∪ {n..<m}" by auto
also have "(∑x∈…. χ x) = (∑x<n. χ x) + (∑x∈{n..<m}. χ x)"
by (intro sum.union_disjoint) auto
also from assms have "(∑x<n. χ x) = 0"
by (subst sum_dcharacter_block) simp_all
also from False have "(∑x∈{n..<m}. χ x) = (∑x∈{..<m - n}. χ (x + n))"
by (intro sum.reindex_bij_witness[of _ "λx. x + n" "λx. x - n"]) (auto simp: periodic)
also have "… = (∑x∈{..<m - n}. χ x)" by (simp add: periodic)
also have "… = (∑x<(m - n) mod n. χ x)"
using False and n by (intro less.IH) auto
also from False and n have "(m - n) mod n = m mod n"
by (simp add: le_mod_geq)
finally show ?thesis by simp
qed
qed
lemma (in dcharacter) sum_dcharacter_lessThan_le:
assumes "χ ≠ principal_dchar n"
shows "norm (∑x<m. χ x) ≤ totient n"
proof -
have "(∑x<m. χ x) = (∑x<m mod n. χ x)" by (rule sum_lessThan_dcharacter) fact
also have "… = (∑x | x < m mod n ∧ coprime x n. χ x)"
by (intro sum.mono_neutral_right) (auto simp: eq_zero_iff)
also have "norm … ≤ (∑x | x < m mod n ∧ coprime x n. 1)"
by (rule sum_norm_le) (auto simp: norm)
also have "… = card {x. x < m mod n ∧ coprime x n}" by simp
also have "… ≤ card (totatives n)" unfolding of_nat_le_iff
proof (intro card_mono subsetI)
fix x assume x: "x ∈ {x. x < m mod n ∧ coprime x n}"
hence "x < m mod n" by simp
also have "… < n" using n by simp
finally show "x ∈ totatives n" using x
by (auto simp: totatives_def intro!: Nat.gr0I)
qed auto
also have "… = totient n" by (simp add: totient_def)
finally show ?thesis .
qed
lemma (in dcharacter) sum_dcharacter_atMost_le:
assumes "χ ≠ principal_dchar n"
shows "norm (∑x≤m. χ x) ≤ totient n"
using sum_dcharacter_lessThan_le[OF assms, of "Suc m"] by (subst (asm) lessThan_Suc_atMost)
lemma (in residues_nat) sum_dcharacters:
"(∑χ∈dcharacters n. χ x) = (if [x = 1] (mod n) then of_nat (totient n) else 0)"
proof (cases "coprime x n")
case True
with n have x: "x mod n ∈ totatives n" by (auto simp: mod_in_totatives)
have "(∑χ∈dcharacters n. χ x) = (∑χ∈characters G. c2dc χ x)"
by (rule sum.reindex_bij_betw [OF bij_betw_characters_dcharacters, symmetric])
also from x have "… = (∑χ∈characters G. χ (x mod n))"
by (simp add: c2dc_def)
also from x have "… = (if x mod n = 1 then order G else 0)"
by (subst sum_characters) (unfold G_def residue_mult_group_def, auto)
also from n have "x mod n = 1 ⟷ [x = 1] (mod n)"
by (simp add: cong_def)
finally show ?thesis by simp
next
case False
have "x mod n ≠ 1"
proof
assume *: "x mod n = 1"
have "gcd (x mod n) n = 1" by (subst *) simp
also have "gcd (x mod n) n = gcd x n"
by (subst gcd.commute) (simp only: gcd_red_nat [symmetric])
finally show False using ‹¬coprime x n› unfolding coprime_iff_gcd_eq_1 by contradiction
qed
from False have "(∑χ∈dcharacters n. χ x) = 0"
by (intro sum.neutral) (auto simp: dcharacters_def dcharacter.eq_zero)
with ‹x mod n ≠ 1› and n show ?thesis by (simp add: cong_def)
qed
lemma (in dcharacter) even_dcharacter_linear_sum_eq_0 [simp]:
assumes "χ ≠ principal_dchar n" and "χ (n - 1) = 1"
shows "(∑k=Suc 0..<n. of_nat k * χ k) = 0"
proof -
have "(∑k=1..<n. of_nat k * χ k) = (∑k=1..<n. (of_nat n - of_nat k) * χ (n - k))"
by (intro sum.reindex_bij_witness[where i = "λk. n - k" and j = "λk. n - k"])
(auto simp: of_nat_diff)
also have "… = n * (∑k=1..<n. χ (n - k)) - (∑k=1..<n. k * χ (n - k))"
by (simp add: algebra_simps sum_subtractf sum_distrib_left)
also have "(∑k=1..<n. χ (n - k)) = (∑k=1..<n. χ k)"
by (intro sum.reindex_bij_witness[where i = "λk. n - k" and j = "λk. n - k"]) auto
also have "… = (∑k<n. χ k)"
by (intro sum.mono_neutral_left) (auto simp: Suc_le_eq)
also have "… = 0" using assms by (simp add: sum_dcharacter_block)
also have "(∑k=1..<n. of_nat k * χ (n - k)) = (∑k=1..<n. k * χ k)"
proof (intro sum.cong refl)
fix k assume k: "k ∈ {1..<n}"
have "of_nat k * χ k = of_nat k * χ ((n - 1) * k)"
using assms by (subst mult) simp_all
also have "(n - 1) * k = n - k + (k - 1) * n"
using k by (simp add: algebra_simps)
also have "χ … = χ (n - k)"
by (rule periodic_mult)
finally show "of_nat k * χ (n - k) = of_nat k * χ k" ..
qed
finally show ?thesis by simp
qed
end