author | eberlm <eberlm@in.tum.de> |

Tue Nov 21 17:18:10 2017 +0100 (19 months ago) | |

changeset 67082 | 4e4bea76e559 |

parent 67081 | 6a8c148db36f |

child 67083 | 6b2c0681ef28 |

Facts about complex n-th roots

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