Facts about complex n-th roots
authoreberlm <eberlm@in.tum.de>
Tue Nov 21 17:18:10 2017 +0100 (19 months ago)
changeset 670824e4bea76e559
parent 67081 6a8c148db36f
child 67083 6b2c0681ef28
Facts about complex n-th roots
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Tue Nov 21 14:11:31 2017 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Nov 21 17:18:10 2017 +0100
     1.3 @@ -957,6 +957,162 @@
     1.4  lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
     1.5    using cis_arg [of y] by (simp add: complex_eq_iff)
     1.6  
     1.7 +subsection \<open>Complex n-th roots\<close>
     1.8 +
     1.9 +lemma bij_betw_roots_unity:
    1.10 +  assumes "n > 0"
    1.11 +  shows   "bij_betw (\<lambda>k. cis (2 * pi * real k / real n)) {..<n} {z. z ^ n = 1}" 
    1.12 +    (is "bij_betw ?f _ _")
    1.13 +  unfolding bij_betw_def
    1.14 +proof (intro conjI)
    1.15 +  show inj: "inj_on ?f {..<n}" unfolding inj_on_def
    1.16 +  proof (safe, goal_cases)
    1.17 +    case (1 k l)
    1.18 +    hence kl: "k < n" "l < n" by simp_all
    1.19 +    from 1 have "1 = ?f k / ?f l" by simp
    1.20 +    also have "\<dots> = cis (2*pi*(real k - real l)/n)"
    1.21 +      using assms by (simp add: field_simps cis_divide)
    1.22 +    finally have "cos (2*pi*(real k - real l) / n) = 1"
    1.23 +      by (simp add: complex_eq_iff)
    1.24 +    then obtain m :: int where "2 * pi * (real k - real l) / real n = real_of_int m * 2 * pi"
    1.25 +      by (subst (asm) cos_one_2pi_int) blast
    1.26 +    hence "real_of_int (int k - int l) = real_of_int (m * int n)"
    1.27 +      unfolding of_int_diff of_int_mult using assms by (simp add: divide_simps)
    1.28 +    also note of_int_eq_iff
    1.29 +    finally have *: "abs m * n = abs (int k - int l)" by (simp add: abs_mult)
    1.30 +    also have "\<dots> < int n" using kl by linarith
    1.31 +    finally have "m = 0" using assms by simp
    1.32 +    with * show "k = l" by simp
    1.33 +  qed
    1.34 +
    1.35 +  have subset: "?f ` {..<n} \<subseteq> {z. z ^ n = 1}"
    1.36 +  proof safe
    1.37 +    fix k :: nat
    1.38 +    have "cis (2 * pi * real k / real n) ^ n = cis (2 * pi) ^ k"
    1.39 +      using assms by (simp add: DeMoivre mult_ac)
    1.40 +    also have "cis (2 * pi) = 1" by (simp add: complex_eq_iff)
    1.41 +    finally show "?f k ^ n = 1" by simp
    1.42 +  qed
    1.43 +
    1.44 +  have "n = card {..<n}" by simp
    1.45 +  also from assms and subset have "\<dots> \<le> card {z::complex. z ^ n = 1}"
    1.46 +    by (intro card_inj_on_le[OF inj]) (auto simp: finite_roots_unity)
    1.47 +  finally have card: "card {z::complex. z ^ n = 1} = n"
    1.48 +    using assms by (intro antisym card_roots_unity) auto
    1.49 +
    1.50 +  have "card (?f ` {..<n}) = card {z::complex. z ^ n = 1}" 
    1.51 +    using card inj by (subst card_image) auto
    1.52 +  with subset and assms show "?f ` {..<n} = {z::complex. z ^ n = 1}"
    1.53 +    by (intro card_subset_eq finite_roots_unity) auto
    1.54 +qed
    1.55 +
    1.56 +lemma card_roots_unity_eq:
    1.57 +  assumes "n > 0"
    1.58 +  shows   "card {z::complex. z ^ n = 1} = n"
    1.59 +  using bij_betw_same_card [OF bij_betw_roots_unity [OF assms]] by simp
    1.60 +
    1.61 +lemma bij_betw_nth_root_unity:
    1.62 +  fixes c :: complex and n :: nat
    1.63 +  assumes c: "c \<noteq> 0" and n: "n > 0"
    1.64 +  defines "c' \<equiv> root n (norm c) * cis (arg c / n)"
    1.65 +  shows "bij_betw (\<lambda>z. c' * z) {z. z ^ n = 1} {z. z ^ n = c}"
    1.66 +proof -
    1.67 +  have "c' ^ n = of_real (root n (norm c) ^ n) * cis (arg c)"
    1.68 +    unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
    1.69 +  also from n have "root n (norm c) ^ n = norm c" by simp
    1.70 +  also from c have "of_real \<dots> * cis (arg c) = c" by (simp add: cis_arg Complex.sgn_eq)
    1.71 +  finally have [simp]: "c' ^ n = c" .
    1.72 +
    1.73 +  show ?thesis unfolding bij_betw_def inj_on_def
    1.74 +  proof safe
    1.75 +    fix z :: complex assume "z ^ n = 1"
    1.76 +    hence "(c' * z) ^ n = c' ^ n" by (simp add: power_mult_distrib)
    1.77 +    also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (arg c)"
    1.78 +      unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
    1.79 +    also from n have "root n (norm c) ^ n = norm c" by simp
    1.80 +    also from c have "\<dots> * cis (arg c) = c" by (simp add: cis_arg Complex.sgn_eq)
    1.81 +    finally show "(c' * z) ^ n = c" .
    1.82 +  next
    1.83 +    fix z assume z: "c = z ^ n"
    1.84 +    define z' where "z' = z / c'"
    1.85 +    from c and n have "c' \<noteq> 0" by (auto simp: c'_def)
    1.86 +    with n c have "z = c' * z'" and "z' ^ n = 1"
    1.87 +      by (auto simp: z'_def power_divide z)
    1.88 +    thus "z \<in> (\<lambda>z. c' * z) ` {z. z ^ n = 1}" by blast
    1.89 +  qed (insert c n, auto simp: c'_def)
    1.90 +qed
    1.91 +
    1.92 +lemma finite_nth_roots [intro]:
    1.93 +  assumes "n > 0"
    1.94 +  shows   "finite {z::complex. z ^ n = c}"
    1.95 +proof (cases "c = 0")
    1.96 +  case True
    1.97 +  with assms have "{z::complex. z ^ n = c} = {0}" by auto
    1.98 +  thus ?thesis by simp
    1.99 +next
   1.100 +  case False
   1.101 +  from assms have "finite {z::complex. z ^ n = 1}" by (intro finite_roots_unity) simp_all
   1.102 +  also have "?this \<longleftrightarrow> ?thesis"
   1.103 +    by (rule bij_betw_finite, rule bij_betw_nth_root_unity) fact+
   1.104 +  finally show ?thesis .
   1.105 +qed
   1.106 +
   1.107 +lemma card_nth_roots:
   1.108 +  assumes "c \<noteq> 0" "n > 0"
   1.109 +  shows   "card {z::complex. z ^ n = c} = n"
   1.110 +proof -
   1.111 +  have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}"
   1.112 +    by (rule sym, rule bij_betw_same_card, rule bij_betw_nth_root_unity) fact+
   1.113 +  also have "\<dots> = n" by (rule card_roots_unity_eq) fact+
   1.114 +  finally show ?thesis .
   1.115 +qed
   1.116 +
   1.117 +lemma sum_roots_unity:
   1.118 +  assumes "n > 1"
   1.119 +  shows   "\<Sum>{z::complex. z ^ n = 1} = 0"
   1.120 +proof -
   1.121 +  define \<omega> where "\<omega> = cis (2 * pi / real n)"
   1.122 +  have [simp]: "\<omega> \<noteq> 1"
   1.123 +  proof
   1.124 +    assume "\<omega> = 1"
   1.125 +    with assms obtain k :: int where "2 * pi / real n = 2 * pi * of_int k"
   1.126 +      by (auto simp: \<omega>_def complex_eq_iff cos_one_2pi_int)
   1.127 +    with assms have "real n * of_int k = 1" by (simp add: field_simps)
   1.128 +    also have "real n * of_int k = of_int (int n * k)" by simp
   1.129 +    also have "1 = (of_int 1 :: real)" by simp
   1.130 +    also note of_int_eq_iff
   1.131 +    finally show False using assms by (auto simp: zmult_eq_1_iff)
   1.132 +  qed
   1.133 +
   1.134 +  have "(\<Sum>z | z ^ n = 1. z :: complex) = (\<Sum>k<n. cis (2 * pi * real k / real n))"
   1.135 +    using assms by (intro sum.reindex_bij_betw [symmetric] bij_betw_roots_unity) auto
   1.136 +  also have "\<dots> = (\<Sum>k<n. \<omega> ^ k)"
   1.137 +    by (intro sum.cong refl) (auto simp: \<omega>_def DeMoivre mult_ac)
   1.138 +  also have "\<dots> = (\<omega> ^ n - 1) / (\<omega> - 1)"
   1.139 +    by (subst geometric_sum) auto
   1.140 +  also have "\<omega> ^ n - 1 = cis (2 * pi) - 1" using assms by (auto simp: \<omega>_def DeMoivre)
   1.141 +  also have "\<dots> = 0" by (simp add: complex_eq_iff)
   1.142 +  finally show ?thesis by simp
   1.143 +qed
   1.144 +
   1.145 +lemma sum_nth_roots:
   1.146 +  assumes "n > 1"
   1.147 +  shows   "\<Sum>{z::complex. z ^ n = c} = 0"
   1.148 +proof (cases "c = 0")
   1.149 +  case True
   1.150 +  with assms have "{z::complex. z ^ n = c} = {0}" by auto
   1.151 +  also have "\<Sum>\<dots> = 0" by simp
   1.152 +  finally show ?thesis .
   1.153 +next
   1.154 +  case False
   1.155 +  define c' where "c' = root n (norm c) * cis (arg c / n)"
   1.156 +  from False and assms have "(\<Sum>{z. z ^ n = c}) = (\<Sum>z | z ^ n = 1. c' * z)"
   1.157 +    by (subst sum.reindex_bij_betw [OF bij_betw_nth_root_unity, symmetric])
   1.158 +       (auto simp: sum_distrib_left finite_roots_unity c'_def)
   1.159 +  also from assms have "\<dots> = 0"
   1.160 +    by (simp add: sum_distrib_left [symmetric] sum_roots_unity)
   1.161 +  finally show ?thesis .
   1.162 +qed
   1.163  
   1.164  subsection \<open>Square root of complex numbers\<close>
   1.165