Theory Gauss_Sums
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
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))"
by (rule sum.mono_neutral_right,simp,blast,simp add: eq)
also have "… = (∑m | m ∈ {1..n} ∧ coprime m n . unity_root n (m*k))"
by (simp add: eq)
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))"
by (simp add: sum_distrib_left algebra_simps)
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]
by (simp add: algebra_simps n)
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"
by (simp add: gauss_sum_int_def ring_distribs unity_root_add)
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)))"
by (simp add: gauss_sum_conv_gauss_sum_int)
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
by (simp add: algebra_simps)
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"
by (simp add: moebius_mu_def)
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))"
by (subst sum_distrib_left)(simp add: algebra_simps)
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"]
by (simp add: mult.commute)
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"
by (simp add: algebra_simps)
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"
by (simp add: algebra_simps d_def)
also have "… = m*k+m*b*n*(k div gcd k n)"
by (simp add: div_mult_swap dvd_div_mult)
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))"
by (simp add: sum_distrib_left[symmetric])
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)"
by (simp add: cong_scalar_right)
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"
proof (simp add: assms(2) cong_add_lcancel_0_nat cong_mult_self_right)
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"
by (simp add: dvd_add_right_iff)
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
by (simp add: dvd_add_left_iff)
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)"
using m_prop(1)[of "a+d", OF cop_ad]
m_prop(1)[of "a",OF True] by (simp add: cong_def)
have p2: "coprime (f (a+d)) n" "coprime (f a) n"
using m_prop(2)[of "a+d", OF cop_ad]
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 (simp_all add: Φ_def)
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"
proof (simp add: assms(3) principal_dchar_def)
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]
by (simp add: conductor_def[symmetric])
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 -
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' where "[a * a' = 1] (mod n)"
using cong_solve_coprime_nat[OF cop] by auto
then have a_inv: "(a*a') mod n = 1"
using cong_def[of "a*a'" 1 n] assms(7) by simp
have "m1 ∈ (⋃h∈kernel G H f. {h ⊗⇘G⇙ a})"
"m2 ∈ (⋃h∈kernel G H f. {h ⊗⇘G⇙ a})"
using r_coset_def[of G "kernel G H f" a] cos_expr assms(5,6) by blast+
then have "m1 ∈ (⋃h∈kernel G H f. {(h * a) mod n})"
"m2 ∈ (⋃h∈kernel G H f. {(h * a) mod n})"
using assms(1) unfolding residue_mult_group_def[of n] by auto
then obtain m1' m2' where
m_expr: "m1 = (m1'* a) mod n ∧ m1' ∈ kernel G H f"
"m2 = (m2'* a) mod n ∧ m2' ∈ kernel G H f"
by blast
have eq_1: "m1 mod m = a mod m"
proof -
have "m1 mod m = ((m1'* a) mod n) mod m" using m_expr by blast
also have "… = (m1' * a) mod m"
using euclidean_semiring_cancel_class.mod_mod_cancel assms(8) by blast
also have "… = (m1' mod m) * (a mod m) mod m"
by (simp add: mod_mult_eq)
also have "… = (a mod m) mod m"
using m_expr(1) h_1 unfolding kernel_def assms(3) by simp
also have "… = a mod m" by auto
finally show ?thesis by simp
qed
have eq_2: "m2 mod m = a mod m"
proof -
have "m2 mod m = ((m2'* a) mod n) mod m" using m_expr by blast
also have "… = (m2' * a) mod m"
using euclidean_semiring_cancel_class.mod_mod_cancel assms(8) by blast
also have "… = (m2' mod m) * (a mod m) mod m"
by (simp add: mod_mult_eq)
also have "… = (a mod m) mod m"
using m_expr(2) h_1 unfolding kernel_def assms(3) by simp
also have "… = a mod m" by auto
finally show ?thesis by simp
qed
from eq_1 eq_2 show ?thesis by argo
qed
lemma residue_mult_group_kernel_partition:
fixes m n :: 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 "m > 1" "n > 0" "m dvd n"
shows "partition (carrier G) (rcosets⇘G⇙ kernel G H f)"
and "card (rcosets⇘G⇙ kernel G H f) = totient m"
and "card (kernel G H f) = totient n div totient m"
and "b ∈(rcosets⇘G⇙ kernel G H f) ⟹ b ≠ {}"
and "b ∈(rcosets⇘G⇙ kernel G H f) ⟹ card (kernel G H f) = card b"
and "bij_betw (λb. (the_elem (f ` b))) (rcosets⇘G⇙ kernel G H f) (carrier H)"
proof -
have "1 < m" by fact
also have "m ≤ n" using ‹n > 0› ‹m dvd n› by (intro dvd_imp_le) auto
finally have "n > 1" .
note mn = ‹m > 1› ‹n > 1› ‹m dvd n› ‹m ≤ n›
interpret n: residues_nat n G
using mn by unfold_locales (auto simp: assms)
interpret m: residues_nat m H
using mn by unfold_locales (auto simp: assms)
from mn have subset: "f ` carrier G ⊆ carrier H"
by (auto simp: assms(1-3) residue_mult_group_def totatives_def
dest: coprime_common_divisor_nat intro!: Nat.gr0I)
moreover have super_set: "carrier H ⊆ f ` carrier G"
proof safe
fix k assume "k ∈ carrier H"
hence k: "k > 0" "k ≤ m" "coprime k m"
by (auto simp: assms(2) residue_mult_group_def totatives_def)
from mn ‹k ∈ carrier H› have "k < m"
by (simp add: totatives_less assms(2) residue_mult_group_def)
define P where "P = {p ∈ prime_factors n. ¬(p dvd m)}"
define a where "a = ∏P"
have [simp]: "a ≠ 0" by (auto simp: P_def a_def intro!: Nat.gr0I)
have [simp]: "prime_factors a = P"
proof -
have "prime_factors a = set_mset (sum prime_factorization P)"
unfolding a_def using mn
by (subst prime_factorization_prod)
(auto simp: P_def prime_factors_dvd prime_gt_0_nat)
also have "sum prime_factorization P = (∑p∈P. {#p#})"
using mn by (intro sum.cong) (auto simp: P_def prime_factorization_prime prime_factors_dvd)
finally show ?thesis by (simp add: P_def)
qed
from mn have "coprime m a"
by (subst coprime_iff_prime_factors_disjoint) (auto simp: P_def)
hence "∃x. [x = k] (mod m) ∧ [x = 1] (mod a)"
by (intro binary_chinese_remainder_nat)
then obtain x where x: "[x = k] (mod m)" "[x = 1] (mod a)"
by auto
from x(1) mn k have [simp]: "x ≠ 0"
using coprime_common_divisor[of k m] by (auto intro!: Nat.gr0I simp: cong_def)
from x(2) have "coprime x a"
using cong_imp_coprime cong_sym by force
hence "coprime x (a * m)"
using k cong_imp_coprime[OF cong_sym[OF x(1)]] by auto
also have "?this ⟷ coprime x n" using mn
by (intro coprime_cong_prime_factors)
(auto simp: prime_factors_product P_def in_prime_factors_iff)
finally have "x mod n ∈ totatives n"
using mn by (auto simp: totatives_def intro!: Nat.gr0I)
moreover have "f (x mod n) = k"
using x(1) k mn ‹k < m› by (auto simp: assms(3) cong_def mod_mod_cancel)
ultimately show "k ∈ f ` carrier G"
by (auto simp: assms(1) residue_mult_group_def)
qed
ultimately have image_eq: "f ` carrier G = carrier H" by blast
have [simp]: "f (k ⊗⇘G⇙ l) = f k ⊗⇘H⇙ f l" if "k ∈ carrier G" "l ∈ carrier G" for k l
using that mn by (auto simp: assms(1-3) residue_mult_group_def totatives_def
mod_mod_cancel mod_mult_eq)
interpret f: group_hom G H f
using subset by unfold_locales (auto simp: hom_def)
show "bij_betw (λb. (the_elem (f ` b))) (rcosets⇘G⇙ kernel G H f) (carrier H)"
unfolding bij_betw_def
proof
show "inj_on (λb. (the_elem (f ` b))) (rcosets⇘G⇙ kernel G H f)"
using f.FactGroup_inj_on unfolding FactGroup_def by auto
have eq: "f ` carrier G = carrier H"
using subset super_set by blast
show "(λb. the_elem (f ` b)) ` (rcosets⇘G⇙ kernel G H f) = carrier H"
using f.FactGroup_onto[OF eq] unfolding FactGroup_def by simp
qed
show "partition (carrier G) (rcosets⇘G⇙ kernel G H f)"
proof
show "⋀a. a ∈ carrier G ⟹
∃!b. b ∈ rcosets⇘G⇙ kernel G H f ∧ a ∈ b"
proof -
fix a
assume a_in: "a ∈ carrier G"
show "∃!b. b ∈ rcosets⇘G⇙ kernel G H f ∧ a ∈ b"
proof -
have "∃b. b ∈ rcosets⇘G⇙ kernel G H f ∧ a ∈ b"
using a_in n.rcosets_part_G[OF f.subgroup_kernel]
by blast
then show ?thesis
using group.rcos_disjoint[OF n.is_group f.subgroup_kernel]
by (auto simp: disjoint_def)
qed
qed
next
show "⋀b. b ∈ rcosets⇘G⇙ kernel G H f ⟹ b ⊆ carrier G"
using n.rcosets_part_G f.subgroup_kernel by auto
qed
have lagr: "card (carrier G) = card (rcosets⇘G⇙ kernel G H f) * card (kernel G H f)"
using group.lagrange_finite[OF n.is_group n.fin f.subgroup_kernel] Coset.order_def[of G] by argo
have k_size: "card (kernel G H f) > 0"
using f.subgroup_kernel finite_subset n.subgroupE(1) n.subgroupE(2) by fastforce
have G_size: "card (carrier G) = totient n"
using n.order Coset.order_def[of G] by simp
have H_size: " totient m = card (carrier H)"
using n.order Coset.order_def[of H] by simp
also have "… = card (carrier (G Mod kernel G H f))"
using f.FactGroup_iso[OF image_eq] card_image f.FactGroup_inj_on f.FactGroup_onto image_eq by fastforce
also have "… = card (carrier G) div card (kernel G H f)"
proof -
have "card (carrier (G Mod kernel G H f)) =
card (rcosets⇘G⇙ kernel G H f)"
unfolding FactGroup_def by simp
also have "… = card (carrier G) div card (kernel G H f)"
by (simp add: lagr k_size)
finally show ?thesis by blast
qed
also have "… = totient n div card (kernel G H f)"
using G_size by argo
finally have eq: "totient m = totient n div card (kernel G H f)" by simp
show "card (kernel G H f) = totient n div totient m"
proof -
have "totient m ≠ 0"
using totient_0_iff[of m] assms(4) by blast
have "card (kernel G H f) dvd totient n"
using lagr ‹card (carrier G) = totient n› by auto
have "totient m * card (kernel G H f) = totient n"
unfolding eq using ‹card (kernel G H f) dvd totient n› by auto
have "totient n div totient m = totient m * card (kernel G H f) div totient m"
using ‹totient m * card (kernel G H f) = totient n› by auto
also have "… = card (kernel G H f)"
using nonzero_mult_div_cancel_left[OF ‹totient m ≠ 0›] by blast
finally show ?thesis by auto
qed
show "card (rcosets⇘G⇙ kernel G H f) = totient m"
proof -
have H_size: " totient m = card (carrier H)"
using n.order Coset.order_def[of H] by simp
also have "… = card (carrier (G Mod kernel G H f))"
using f.FactGroup_iso[OF image_eq] card_image f.FactGroup_inj_on f.FactGroup_onto image_eq by fastforce
also have "card (carrier (G Mod kernel G H f)) =
card (rcosets⇘G⇙ kernel G H f)"
unfolding FactGroup_def by simp
finally show "card (rcosets⇘G⇙ kernel G H f) = totient m"
by argo
qed
assume "b ∈ rcosets⇘G⇙ kernel G H f"
then show "b ≠ {}"
proof -
have "card b = card (kernel G H f)"
using ‹b ∈ rcosets⇘G⇙ kernel G H f› f.subgroup_kernel n.card_rcosets_equal n.subgroupE(1) by auto
then have "card b > 0"
by (simp add: k_size)
then show ?thesis by auto
qed
assume b_cos: "b ∈ rcosets⇘G⇙ kernel G H f"
show "card (kernel G H f) = card b"
using group.card_rcosets_equal[OF n.is_group b_cos]
f.subgroup_kernel subgroup.subset by blast
qed
lemma primitive_iff_separable_lemma:
assumes prod: "(∀n. χ n = Φ n * χ⇩1 n) ∧ primitive_dchar d Φ"
assumes ‹d > 1› ‹0 < k› ‹d dvd k› ‹k > 1›
shows "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
(totient k div totient d) * (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
proof -
from assms interpret Φ: primitive_dchar d "residue_mult_group d" Φ
by auto
define G where "G = residue_mult_group k"
define H where "H = residue_mult_group d"
define f where "f = (λt. t mod d)"
from residue_mult_group_kernel_partition(2)[OF ‹d > 1› ‹0 < k› ‹d dvd k›]
have fin_cosets: "finite (rcosets⇘G⇙ kernel G H f)"
using ‹1 < d› card.infinite by (fastforce simp: G_def H_def f_def)
have fin_G: "finite (carrier G)"
unfolding G_def residue_mult_group_def by simp
have eq: "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
(∑m | m ∈ carrier G . Φ(m) * unity_root d m)"
unfolding residue_mult_group_def totatives_def G_def
by (rule sum.cong,auto)
also have "… = sum (λm. Φ(m) * unity_root d m) (carrier G)" by simp
also have eq': "… = sum (sum (λm. Φ m * unity_root d (int m))) (rcosets⇘G⇙ kernel G H f)"
by (rule disjoint_sum [symmetric])
(use fin_G fin_cosets residue_mult_group_kernel_partition(1)[OF ‹d > 1› ‹k > 0› ‹d dvd k›] in
‹auto simp: G_def H_def f_def›)
also have "… =
(∑b ∈ (rcosets⇘G⇙ kernel G H f) . (∑m ∈ b. Φ m * unity_root d (int m)))" by simp
finally have 1: "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
(∑b ∈ (rcosets⇘G⇙ kernel G H f) . (∑m ∈ b. Φ m * unity_root d (int m)))"
using eq eq' by auto
have eq''': "… =
(∑b ∈ (rcosets⇘G⇙ kernel G H f) . (totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
proof (rule sum.cong,simp)
fix b
assume b_in: "b ∈ (rcosets⇘G⇙ kernel G H f)"
note b_not_empty = residue_mult_group_kernel_partition(4)
[OF ‹d > 1› ‹0 < k› ‹d dvd k› b_in[unfolded G_def H_def f_def]]
{
fix m1 m2
assume m_in: "m1 ∈ b" "m2 ∈ b"
have m_mod: "m1 mod d = m2 mod d"
using residue_mult_group_coset[OF b_in[unfolded G_def H_def f_def] m_in ‹k > 1› ‹d dvd k›]
by blast
} note m_mod = this
{
fix m1 m2
assume m_in: "m1 ∈ b" "m2 ∈ b"
have "Φ m1 * unity_root d (int m1) = Φ m2 * unity_root d (int m2)"
proof -
have Φ_periodic: "periodic_arithmetic Φ d" using Φ.dir_periodic_arithmetic by blast
have 1: "Φ m1 = Φ m2"
using mod_periodic_arithmetic[OF ‹periodic_arithmetic Φ d› m_mod[OF m_in]] by simp
have 2: "unity_root d m1 = unity_root d m2"
using m_mod[OF m_in] by (intro unity_root_cong) (auto simp: cong_def simp flip: zmod_int)
from 1 2 show ?thesis by simp
qed
} note all_eq_in_coset = this
from all_eq_in_coset b_not_empty
obtain l where l_prop: "l ∈ b ∧ (∀y ∈ b. Φ y * unity_root d (int y) =
Φ l * unity_root d (int l))" by blast
have "(∑m ∈ b. Φ m * unity_root d (int m)) =
((totient k div totient d) * (Φ l * unity_root d (int l)))"
proof -
have "(∑m ∈ b. Φ m * unity_root d (int m)) =
(∑m ∈ b. Φ l * unity_root d (int l))"
by (rule sum.cong,simp) (use all_eq_in_coset l_prop in blast)
also have "… = card b * Φ l * unity_root d (int l)"
by simp
also have "… = (totient k div totient d) * Φ l * unity_root d (int l)"
using residue_mult_group_kernel_partition(3)[OF ‹d > 1› ‹0 < k› ‹d dvd k›]
residue_mult_group_kernel_partition(5)
[OF ‹d > 1› ‹0 < k› ‹d dvd k› b_in [unfolded G_def H_def f_def]]
by argo
finally have 2:
"(∑m ∈ b. Φ m * unity_root d (int m)) =
(totient k div totient d) * Φ l * unity_root d (int l)"
by blast
from b_not_empty 2 show ?thesis by auto
qed
also have "… = ((totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
proof -
have foral: "(⋀y. y ∈ b ⟹ f y = f l)"
using m_mod l_prop unfolding f_def by blast
have eq: "the_elem (f ` b) = f l"
using the_elem_image_unique[of _ f l, OF b_not_empty foral] by simp
have per: "periodic_arithmetic Φ d" using prod Φ.dir_periodic_arithmetic by blast
show ?thesis
unfolding eq using mod_periodic_arithmetic[OF per, of "l mod d" l]
by (auto simp: f_def unity_root_mod zmod_int)
qed
finally show "(∑m ∈ b. Φ m * unity_root d (int m)) =
((totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
by blast
qed
have "… =
(∑b ∈ (rcosets⇘G⇙ kernel G H f) . (totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
by blast
also have eq'': "
… = (∑h ∈ carrier H . (totient k div totient d) * (Φ (h) * unity_root d (int (h))))"
unfolding H_def G_def f_def
by (rule sum.reindex_bij_betw[OF residue_mult_group_kernel_partition(6)[OF ‹d > 1› ‹0 < k› ‹d dvd k›]])
finally have 2: "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
(totient k div totient d)*(∑h ∈ carrier H . (Φ (h) * unity_root d (int (h))))"
using 1 by (simp add: eq'' eq''' sum_distrib_left)
also have "… = (totient k div totient d)*(∑m | m ∈ {1..d} ∧ coprime m d . (Φ (m) * unity_root d (int (m))))"
unfolding H_def residue_mult_group_def by (simp add: totatives_def Suc_le_eq)
finally show ?thesis by simp
qed
text ‹Theorem 8.19›
theorem (in dcharacter) primitive_iff_separable:
"primitive_dchar n χ ⟷ (∀k>0. separable k)"
proof (cases "χ = principal_dchar n")
case True
thus ?thesis
using principal_not_primitive principal_not_totally_separable by auto
next
case False
note nonprincipal = this
show ?thesis
proof
assume "primitive_dchar n χ"
then interpret A: primitive_dchar n "residue_mult_group n" χ by auto
show "(∀k. k > 0 ⟶ separable k)"
using n A.primitive_encoding(2) by blast
next
assume tot_separable: "∀k>0. separable k"
{
assume as: "¬ primitive_dchar n χ"
have "∃r. r ≠ 0 ∧ ¬ coprime r n ∧ gauss_sum r ≠ 0"
proof -
from n have "n > 0" by simp
define d where "d = conductor"
have "d > 0" unfolding d_def using conductor_gr_0 .
then have "d > 1" using nonprincipal d_def conductor_eq_1_iff_principal by auto
have "d < n" unfolding d_def using nonprimitive_imp_conductor_less[OF as] .
have "d dvd n" unfolding d_def using conductor_dvd by blast
define r where "r = n div d"
have 0: "r ≠ 0" unfolding r_def
using ‹0 < n› ‹d dvd n› dvd_div_gt0 by auto
have "gcd r n > 1"
unfolding r_def
proof -
have "n div d > 1" using ‹1 < n› ‹d < n› ‹d dvd n› by auto
have "n div d dvd n" using ‹d dvd n› by force
have "gcd (n div d) n = n div d" using gcd_nat.absorb1[OF ‹n div d dvd n›] by blast
then show "1 < gcd (n div d) n" using ‹n div d > 1› by argo
qed
then have 1: "¬ coprime r n" by auto
define χ⇩1 where "χ⇩1 = principal_dchar n"
from primitive_principal_form[OF nonprincipal]
obtain Φ where
prod: "(∀k. χ(k) = Φ(k)*χ⇩1(k)) ∧ primitive_dchar d Φ"
using d_def unfolding χ⇩1_def by blast
then have prod1: "(∀k. χ(k) = Φ(k)*χ⇩1(k))" "primitive_dchar d Φ" by blast+
then interpret Φ: primitive_dchar d "residue_mult_group d" Φ
by auto
have "gauss_sum r = (∑m = 1..n . χ(m) * unity_root n (m*r))"
unfolding gauss_sum_def by blast
also have "… = (∑m = 1..n . Φ(m)*χ⇩1(m) * unity_root n (m*r))"
by (rule sum.cong,auto simp add: prod)
also have "… = (∑m | m ∈ {1..n} ∧ coprime m n. Φ(m)*χ⇩1(m) * unity_root n (m*r))"
by (intro sum.mono_neutral_right) (auto simp: χ⇩1_def principal_dchar_def)
also have "… = (∑m | m ∈ {1..n} ∧ coprime m n. Φ(m)*χ⇩1(m) * unity_root d m)"
proof (rule sum.cong,simp)
fix x
assume "x ∈ {m ∈ {1..n}. coprime m n}"
have "unity_root n (int (x * r)) = unity_root d (int x)"
using unity_div_num[OF ‹n > 0› ‹d > 0› ‹d dvd n›]
by (simp add: algebra_simps r_def)
then show "Φ x * χ⇩1 x * unity_root n (int (x * r)) =
Φ x * χ⇩1 x * unity_root d (int x)" by auto
qed
also have "… = (∑m | m ∈ {1..n} ∧ coprime m n. Φ(m) * unity_root d m)"
by (rule sum.cong,auto simp add: χ⇩1_def principal_dchar_def)
also have "… = (totient n div totient d) * (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
using primitive_iff_separable_lemma[OF prod ‹d > 1› ‹n > 0› ‹d dvd n› ‹n > 1›] by blast
also have "… = (totient n div totient d) * Φ.gauss_sum 1"
proof -
have "Φ.gauss_sum 1 = (∑m = 1..d . Φ m * unity_root d (int (m )))"
by (simp add: Φ.gauss_sum_def)
also have "… = (∑m | m ∈ {1..d} . Φ m * unity_root d (int m))"
by (rule sum.cong,auto)
also have "… = (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
by (rule sum.mono_neutral_right) (use Φ.eq_zero in auto)
finally have "Φ.gauss_sum 1 = (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
by blast
then show ?thesis by metis
qed
finally have g_expr: "gauss_sum r = (totient n div totient d) * Φ.gauss_sum 1"
by blast
have t_non_0: "totient n div totient d ≠ 0"
by (simp add: ‹0 < n› ‹d dvd n› dvd_div_gt0 totient_dvd)
have "(norm (Φ.gauss_sum 1))⇧2 = d"
using Φ.primitive_encoding(3) by simp
then have "Φ.gauss_sum 1 ≠ 0"
using ‹0 < d› by auto
then have 2: "gauss_sum r ≠ 0"
using g_expr t_non_0 by auto
from 0 1 2 show "∃r. r ≠ 0 ∧ ¬ coprime r n ∧ gauss_sum r ≠ 0"
by blast
qed
}
note contr = this
show "primitive_dchar n χ"
proof (rule ccontr)
assume "¬ primitive_dchar n χ"
then obtain r where 1: "r ≠ 0 ∧ ¬ coprime r n ∧ gauss_sum r ≠ 0"
using contr by blast
from global_separability_condition tot_separable
have 2: "(∀k>0. ¬ coprime k n ⟶ gauss_sum k = 0)"
by blast
from 1 2 show "False" by blast
qed
qed
qed
text‹Theorem 8.20›
theorem (in primitive_dchar) fourier_primitive:
includes no_vec_lambda_notation
fixes τ :: complex
defines "τ ≡ gauss_sum 1 / sqrt n"
shows "χ m = τ / sqrt n * (∑k=1..n. cnj (χ k) * unity_root n (-m*k))"
and "norm τ = 1"
proof -
have chi_not_principal: "χ ≠ principal_dchar n"
using principal_not_totally_separable primitive_encoding(2) by blast
then have case_0: "(∑k=1..n. χ k) = 0"
proof -
have "sum χ {0..n-1} = sum χ {1..n}"
using periodic_arithmetic_sum_periodic_arithmetic_shift[OF dir_periodic_arithmetic, of 1] n
by auto
also have "{0..n-1} = {..<n}"
using n by auto
finally show "(∑n = 1..n . χ n) = 0"
using sum_dcharacter_block chi_not_principal by simp
qed
have "χ m =
(∑k = 1..n. 1 / of_nat n * gauss_sum_int (- int k) *
unity_root n (int (m * k)))"
using dcharacter_fourier_expansion[of m] by auto
also have "… = (∑k = 1..n. 1 / of_nat n * gauss_sum (nat ((- k) mod n)) *
unity_root n (int (m * k)))"
by (auto simp: gauss_sum_int_conv_gauss_sum)
also have "… = (∑k = 1..n. 1 / of_nat n * cnj (χ (nat ((- k) mod n))) * gauss_sum 1 * unity_root n (int (m * k)))"
proof (rule sum.cong,simp)
fix k
assume "k ∈ {1..n}"
have "gauss_sum (nat (- int k mod int n)) =
cnj (χ (nat (- int k mod int n))) * gauss_sum 1"
proof (cases "nat ((- k) mod n) > 0")
case True
then show ?thesis
using mp[OF spec[OF primitive_encoding(2)] True]
unfolding separable_def by auto
next
case False
then have nat_0: "nat ((- k) mod n) = 0" by blast
show ?thesis
proof -
have "gauss_sum (nat (- int k mod int n)) = gauss_sum 0"
using nat_0 by argo
also have "… = (∑m = 1..n. χ m)"
unfolding gauss_sum_def by (rule sum.cong) auto
also have "… = 0" using case_0 by blast
finally have 1: "gauss_sum (nat (- int k mod int n)) = 0"
by blast
have 2: "cnj (χ (nat (- int k mod int n))) = 0"
using nat_0 zero_eq_0 by simp
show ?thesis using 1 2 by simp
qed
qed
then show "1 / of_nat n * gauss_sum (nat (- int k mod int n)) * unity_root n (int (m * k)) =
1 / of_nat n * cnj (χ (nat (- int k mod int n))) * gauss_sum 1 * unity_root n (int (m * k))"
by auto
qed
also have "… = (∑k = 1..n. 1 / of_nat n * cnj (χ (nat (- int k mod int n))) *
gauss_sum 1 * unity_root n (int (m * (nat (int k mod int n)))))"
proof (rule sum.cong,simp)
fix x
assume "x ∈ {1..n}"
have "unity_root n (m * x) = unity_root n (m * x mod n)"
using unity_root_mod_nat[of n "m*x"] by (simp add: nat_mod_as_int)
also have "… = unity_root n (m * (x mod n))"
by (rule unity_root_cong)
(auto simp: cong_def mod_mult_right_eq simp flip: zmod_int of_nat_mult)
finally have "unity_root n (m * x) = unity_root n (m * (x mod n))" by blast
then show "1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
gauss_sum 1 * unity_root n (int (m * x)) =
1 / of_nat n * cnj (χ (nat (- int x mod int n))) * gauss_sum 1 *
unity_root n (int (m * nat (int x mod int n)))"
by (simp add: nat_mod_as_int)
qed
also have "… = (∑k = 0..n-1. 1 / of_nat n * cnj (χ k) * gauss_sum 1 * unity_root n (- int (m * k)))"
proof -
have b: "bij_betw (λk. nat((-k) mod n)) {1..n} {0..n-1}"
unfolding bij_betw_def
proof
show "inj_on (λk. nat (- int k mod int n)) {1..n}"
unfolding inj_on_def
proof (safe)
fix x y
assume a1: "x ∈ {1..n}" "y ∈ {1..n}"
assume a2: "nat (- x mod n) = nat (- y mod n)"
then have "(- x) mod n = - y mod n"
using n eq_nat_nat_iff by auto
then have "[-int x = - int y] (mod n)"
using cong_def by blast
then have "[x = y] (mod n)"
by (simp add: cong_int_iff cong_minus_minus_iff)
then have cong: "x mod n = y mod n" using cong_def by blast
then show "x = y"
proof (cases "x = n")
case True then show ?thesis using cong a1(2) by auto
next
case False
then have "x mod n = x" using a1(1) by auto
then have "y ≠ n" using a1(1) local.cong by fastforce
then have "y mod n = y" using a1(2) by auto
then show ?thesis using ‹x mod n = x› cong by linarith
qed
qed
show "(λk. nat (- int k mod int n)) ` {1..n} = {0..n - 1}"
unfolding image_def
proof
let ?A = "{y. ∃x∈{1..n}. y = nat (- int x mod int n)}"
let ?B = "{0..n - 1}"
show "?A ⊆ ?B"
proof
fix y
assume "y ∈ {y. ∃x∈{1..n}. y = nat (- int x mod int n)}"
then obtain x where "x∈{1..n} ∧ y = nat (- int x mod int n)" by blast
then show "y ∈ {0..n - 1}" by (simp add: nat_le_iff of_nat_diff)
qed
show "?A ⊇ ?B"
proof
fix x
assume 1: "x ∈ {0..n-1}"
then have "n - x ∈ {1..n}"
using n by auto
have "x = nat (- int (n-x) mod int n)"
proof -
have "nat (- int (n-x) mod int n) = nat (int x) mod int n"
apply(simp add: int_ops(6),rule conjI)
using ‹n - x ∈ {1..n}› by force+
also have "… = x"
using 1 n by auto
finally show ?thesis by presburger
qed
then show "x ∈ {y. ∃x∈{1..n}. y = nat (- int x mod int n)}"
using ‹n - x ∈ {1..n}› by blast
qed
qed
qed
show ?thesis
proof -
have 1: "(∑k = 1..n. 1 / of_nat n * cnj (χ (nat (- int k mod int n))) *
gauss_sum 1 * unity_root n (int (m * nat (int k mod int n)))) =
(∑x = 1..n. 1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
gauss_sum 1 * unity_root n (- int (m * nat (- int x mod int n))))"
proof (rule sum.cong,simp)
fix x
have "(int m * (int x mod int n)) mod n = (m*x) mod n"
by (simp add: mod_mult_right_eq zmod_int)
also have "… = (- ((- int (m*x) mod n))) mod n"
by (simp add: mod_minus_eq of_nat_mod)
have "(int m * (int x mod int n)) mod n = (- (int m * (- int x mod int n))) mod n"
apply(subst mod_mult_right_eq,subst add.inverse_inverse[symmetric],subst (5) add.inverse_inverse[symmetric])
by (subst minus_mult_minus,subst mod_mult_right_eq[symmetric],auto)
then have "unity_root n (int m * (int x mod int n)) =
unity_root n (- (int m * (- int x mod int n)))"
using unity_root_mod[of n "int m * (int x mod int n)"]
unity_root_mod[of n " - (int m * (- int x mod int n))"] by argo
then show "1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
gauss_sum 1 *
unity_root n (int (m * nat (int x mod int n))) =
1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
gauss_sum 1 *
unity_root n (- int (m * nat (- int x mod int n)))"
by clarsimp
qed
also have 2: "(∑x = 1..n. 1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
gauss_sum 1 * unity_root n (- int (m * nat (- int x mod int n)))) =
(∑md = 0..n - 1. 1 / of_nat n * cnj (χ md) * gauss_sum 1 *
unity_root n (- int (m * md)))"
using sum.reindex_bij_betw[OF b, of "λmd. 1 / of_nat n * cnj (χ md) * gauss_sum 1 * unity_root n (- int (m * md))"]
by blast
also have 3: "… = (∑k = 0..n - 1.
1 / of_nat n * cnj (χ k) * gauss_sum 1 *
unity_root n (- int (m * k)))" by blast
finally have "(∑k = 1..n. 1 / of_nat n * cnj (χ (nat (- int k mod int n))) *
gauss_sum 1 * unity_root n (int (m * nat (int k mod int n)))) =
(∑k = 0..n - 1.
1 / of_nat n * cnj (χ k) * gauss_sum 1 *
unity_root n (- int (m * k)))" using 1 2 3 by argo
then show ?thesis by blast
qed
qed
also have "… = (∑k = 1..n.
1 / of_nat n * cnj (χ k) * gauss_sum 1 *
unity_root n (- int (m * k)))"
proof -
let ?f = "(λk. 1 / of_nat n * cnj (χ k) * gauss_sum 1 * unity_root n (- int (m * k)))"
have "?f 0 = 0"
using zero_eq_0 by auto
have "?f n = 0"
using zero_eq_0 mod_periodic_arithmetic[OF dir_periodic_arithmetic, of n 0]
by simp
have "(∑n = 0..n - 1. ?f n) = (∑n = 1..n - 1. ?f n)"
using sum_shift_lb_Suc0_0[of ?f, OF ‹?f 0 = 0›]
by auto
also have "… = (∑n = 1..n. ?f n)"
proof (rule sum.mono_neutral_left,simp,simp,safe)
fix i
assume "i ∈ {1..n}" "i ∉ {1..n - 1}"
then have "i = n" using n by auto
then show "1 / of_nat n * cnj (χ i) * gauss_sum 1 * unity_root n (- int (m * i)) = 0"
using ‹?f n = 0› by blast
qed
finally show ?thesis by blast
qed
also have "… = (∑k = 1..n. (τ / sqrt n) * cnj (χ k) * unity_root n (- int (m * k)))"
proof (rule sum.cong,simp)
fix x
assume "x ∈ {1..n}"
have "τ / sqrt (real n) = 1 / of_nat n * gauss_sum 1"
proof -
have "τ / sqrt (real n) = gauss_sum 1 / sqrt n / sqrt n"
using assms by auto
also have "… = gauss_sum 1 / (sqrt n * sqrt n)"
by (subst divide_divide_eq_left,subst of_real_mult,blast)
also have "… = gauss_sum 1 / n"
using real_sqrt_mult_self by simp
finally show ?thesis by simp
qed
then show
"1 / of_nat n * cnj (χ x) * gauss_sum 1 * unity_root n (- int (m * x)) =
(τ / sqrt n) * cnj (χ x) * unity_root n (- int (m * x))" by simp
qed
also have "… = τ / sqrt (real n) *
(∑k = 1..n. cnj (χ k) * unity_root n (- int (m * k)))"
proof -
have "(∑k = 1..n. τ / sqrt (real n) * cnj (χ k) * unity_root n (- int (m * k))) =
(∑k = 1..n. τ / sqrt (real n) * (cnj (χ k) * unity_root n (- int (m * k))))"
by (rule sum.cong,simp, simp add: algebra_simps)
also have "… = τ / sqrt (real n) * (∑k = 1..n. cnj (χ k) * unity_root n (- int (m * k)))"
by (rule sum_distrib_left[symmetric])
finally show ?thesis by blast
qed
finally show "χ m = (τ / sqrt (real n)) *
(∑k=1..n. cnj (χ k) * unity_root n (- int m * int k))" by simp
have 1: "norm (gauss_sum 1) = sqrt n"
using gauss_sum_1_mod_square_eq_k[OF primitive_encoding(2)]
by (simp add: cmod_def)
from assms have 2: "norm τ = norm (gauss_sum 1) / ¦sqrt n¦"
by (simp add: norm_divide)
show "norm τ = 1" using 1 2 n by simp
qed
unbundle vec_lambda_notation
end