1 (* Author: John Harrison and Valentina Bruno |
|
2 Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson |
|
3 *) |
|
4 |
|
5 section \<open>polynomial functions: extremal behaviour and root counts\<close> |
|
6 |
|
7 theory Poly_Roots |
|
8 imports Complex_Main |
|
9 begin |
|
10 |
|
11 subsection\<open>Geometric progressions\<close> |
|
12 |
|
13 lemma setsum_gp_basic: |
|
14 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
15 shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n" |
|
16 by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) |
|
17 |
|
18 lemma setsum_gp0: |
|
19 fixes x :: "'a::{comm_ring,division_ring}" |
|
20 shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" |
|
21 using setsum_gp_basic[of x n] |
|
22 by (simp add: mult.commute divide_simps) |
|
23 |
|
24 lemma setsum_power_add: |
|
25 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
26 shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)" |
|
27 by (simp add: setsum_right_distrib power_add) |
|
28 |
|
29 lemma setsum_power_shift: |
|
30 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
31 assumes "m \<le> n" |
|
32 shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)" |
|
33 proof - |
|
34 have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))" |
|
35 by (simp add: setsum_right_distrib power_add [symmetric]) |
|
36 also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)" |
|
37 using \<open>m \<le> n\<close> by (intro setsum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto |
|
38 finally show ?thesis . |
|
39 qed |
|
40 |
|
41 lemma setsum_gp_multiplied: |
|
42 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
43 assumes "m \<le> n" |
|
44 shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n" |
|
45 proof - |
|
46 have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)" |
|
47 by (metis mult.assoc mult.commute assms setsum_power_shift) |
|
48 also have "... =x^m * (1 - x^Suc(n-m))" |
|
49 by (metis mult.assoc setsum_gp_basic) |
|
50 also have "... = x^m - x^Suc n" |
|
51 using assms |
|
52 by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) |
|
53 finally show ?thesis . |
|
54 qed |
|
55 |
|
56 lemma setsum_gp: |
|
57 fixes x :: "'a::{comm_ring,division_ring}" |
|
58 shows "(\<Sum>i=m..n. x^i) = |
|
59 (if n < m then 0 |
|
60 else if x = 1 then of_nat((n + 1) - m) |
|
61 else (x^m - x^Suc n) / (1 - x))" |
|
62 using setsum_gp_multiplied [of m n x] |
|
63 apply auto |
|
64 by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) |
|
65 |
|
66 lemma setsum_gp_offset: |
|
67 fixes x :: "'a::{comm_ring,division_ring}" |
|
68 shows "(\<Sum>i=m..m+n. x^i) = |
|
69 (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" |
|
70 using setsum_gp [of x m "m+n"] |
|
71 by (auto simp: power_add algebra_simps) |
|
72 |
|
73 lemma setsum_gp_strict: |
|
74 fixes x :: "'a::{comm_ring,division_ring}" |
|
75 shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))" |
|
76 by (induct n) (auto simp: algebra_simps divide_simps) |
|
77 |
|
78 subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close> |
|
79 |
|
80 lemma sub_polyfun: |
|
81 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
82 shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
|
83 (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)" |
|
84 proof - |
|
85 have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
|
86 (\<Sum>i\<le>n. a i * (x^i - y^i))" |
|
87 by (simp add: algebra_simps setsum_subtractf [symmetric]) |
|
88 also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))" |
|
89 by (simp add: power_diff_sumr2 ac_simps) |
|
90 also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))" |
|
91 by (simp add: setsum_right_distrib ac_simps) |
|
92 also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))" |
|
93 by (simp add: nested_setsum_swap') |
|
94 finally show ?thesis . |
|
95 qed |
|
96 |
|
97 lemma sub_polyfun_alt: |
|
98 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
99 shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
|
100 (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)" |
|
101 proof - |
|
102 { fix j |
|
103 have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) = |
|
104 (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)" |
|
105 by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto } |
|
106 then show ?thesis |
|
107 by (simp add: sub_polyfun) |
|
108 qed |
|
109 |
|
110 lemma polyfun_linear_factor: |
|
111 fixes a :: "'a::{comm_ring,monoid_mult}" |
|
112 shows "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = |
|
113 (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)" |
|
114 proof - |
|
115 { fix z |
|
116 have "(\<Sum>i\<le>n. c i * z^i) - (\<Sum>i\<le>n. c i * a^i) = |
|
117 (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)" |
|
118 by (simp add: sub_polyfun setsum_left_distrib) |
|
119 then have "(\<Sum>i\<le>n. c i * z^i) = |
|
120 (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j) |
|
121 + (\<Sum>i\<le>n. c i * a^i)" |
|
122 by (simp add: algebra_simps) } |
|
123 then show ?thesis |
|
124 by (intro exI allI) |
|
125 qed |
|
126 |
|
127 lemma polyfun_linear_factor_root: |
|
128 fixes a :: "'a::{comm_ring,monoid_mult}" |
|
129 assumes "(\<Sum>i\<le>n. c i * a^i) = 0" |
|
130 shows "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)" |
|
131 using polyfun_linear_factor [of c n a] assms |
|
132 by simp |
|
133 |
|
134 lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b" |
|
135 by (metis norm_triangle_mono order.trans order_refl) |
|
136 |
|
137 lemma polyfun_extremal_lemma: |
|
138 fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
|
139 assumes "e > 0" |
|
140 shows "\<exists>M. \<forall>z. M \<le> norm z \<longrightarrow> norm(\<Sum>i\<le>n. c i * z^i) \<le> e * norm(z) ^ Suc n" |
|
141 proof (induction n) |
|
142 case 0 |
|
143 show ?case |
|
144 by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms) |
|
145 next |
|
146 case (Suc n) |
|
147 then obtain M where M: "\<forall>z. M \<le> norm z \<longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n" .. |
|
148 show ?case |
|
149 proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify) |
|
150 fix z::'a |
|
151 assume "max 1 (max M ((e + norm (c (Suc n))) / e)) \<le> norm z" |
|
152 then have norm1: "0 < norm z" "M \<le> norm z" "(e + norm (c (Suc n))) / e \<le> norm z" |
|
153 by auto |
|
154 then have norm2: "(e + norm (c (Suc n))) \<le> e * norm z" "(norm z * norm z ^ n) > 0" |
|
155 apply (metis assms less_divide_eq mult.commute not_le) |
|
156 using norm1 apply (metis mult_pos_pos zero_less_power) |
|
157 done |
|
158 have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) = |
|
159 (e + norm (c (Suc n))) * (norm z * norm z ^ n)" |
|
160 by (simp add: norm_mult norm_power algebra_simps) |
|
161 also have "... \<le> (e * norm z) * (norm z * norm z ^ n)" |
|
162 using norm2 by (metis real_mult_le_cancel_iff1) |
|
163 also have "... = e * (norm z * (norm z * norm z ^ n))" |
|
164 by (simp add: algebra_simps) |
|
165 finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) |
|
166 \<le> e * (norm z * (norm z * norm z ^ n))" . |
|
167 then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1 |
|
168 by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle) |
|
169 qed |
|
170 qed |
|
171 |
|
172 lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)" |
|
173 proof - |
|
174 have "b \<le> norm y - norm x" |
|
175 using assms by linarith |
|
176 then show ?thesis |
|
177 by (metis (no_types) add.commute norm_diff_ineq order_trans) |
|
178 qed |
|
179 |
|
180 lemma polyfun_extremal: |
|
181 fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
|
182 assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0" |
|
183 shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity" |
|
184 using assms |
|
185 proof (induction n) |
|
186 case 0 then show ?case |
|
187 by simp |
|
188 next |
|
189 case (Suc n) |
|
190 show ?case |
|
191 proof (cases "c (Suc n) = 0") |
|
192 case True |
|
193 with Suc show ?thesis |
|
194 by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq) |
|
195 next |
|
196 case False |
|
197 with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n] |
|
198 obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> |
|
199 norm (\<Sum>i\<le>n. c i * z^i) \<le> norm (c (Suc n)) / 2 * norm z ^ Suc n" |
|
200 by auto |
|
201 show ?thesis |
|
202 unfolding eventually_at_infinity |
|
203 proof (rule exI [where x="max M (max 1 ((\<bar>B\<bar> + 1) / (norm (c (Suc n)) / 2)))"], clarsimp) |
|
204 fix z::'a |
|
205 assume les: "M \<le> norm z" "1 \<le> norm z" "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z" |
|
206 then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))" |
|
207 by (metis False pos_divide_le_eq zero_less_norm_iff) |
|
208 then have "\<bar>B\<bar> * 2 + 2 \<le> norm z ^ (Suc n) * norm (c (Suc n))" |
|
209 by (metis \<open>1 \<le> norm z\<close> order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc) |
|
210 then show "B \<le> norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les |
|
211 apply auto |
|
212 apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"]) |
|
213 apply (simp_all add: norm_mult norm_power) |
|
214 done |
|
215 qed |
|
216 qed |
|
217 qed |
|
218 |
|
219 lemma polyfun_rootbound: |
|
220 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}" |
|
221 assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0" |
|
222 shows "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<and> card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n" |
|
223 using assms |
|
224 proof (induction n arbitrary: c) |
|
225 case (Suc n) show ?case |
|
226 proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}") |
|
227 case False |
|
228 then obtain a where a: "(\<Sum>i\<le>Suc n. c i * a^i) = 0" |
|
229 by auto |
|
230 from polyfun_linear_factor_root [OF this] |
|
231 obtain b where "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i< Suc n. b i * z^i)" |
|
232 by auto |
|
233 then have b: "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i\<le>n. b i * z^i)" |
|
234 by (metis lessThan_Suc_atMost) |
|
235 then have ins_ab: "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = insert a {z. (\<Sum>i\<le>n. b i * z^i) = 0}" |
|
236 by auto |
|
237 have c0: "c 0 = - (a * b 0)" using b [of 0] |
|
238 by simp |
|
239 then have extr_prem: "~ (\<exists>k\<le>n. b k \<noteq> 0) \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> k \<le> Suc n \<and> c k \<noteq> 0" |
|
240 by (metis Suc.prems le0 minus_zero mult_zero_right) |
|
241 have "\<exists>k\<le>n. b k \<noteq> 0" |
|
242 apply (rule ccontr) |
|
243 using polyfun_extremal [OF extr_prem, of 1] |
|
244 apply (auto simp: eventually_at_infinity b simp del: setsum_atMost_Suc) |
|
245 apply (drule_tac x="of_real ba" in spec, simp) |
|
246 done |
|
247 then show ?thesis using Suc.IH [of b] ins_ab |
|
248 by (auto simp: card_insert_if) |
|
249 qed simp |
|
250 qed simp |
|
251 |
|
252 corollary |
|
253 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}" |
|
254 assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0" |
|
255 shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}" |
|
256 and polyfun_rootbound_card: "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n" |
|
257 using polyfun_rootbound [OF assms] by auto |
|
258 |
|
259 lemma polyfun_finite_roots: |
|
260 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}" |
|
261 shows "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)" |
|
262 proof (cases " \<exists>k\<le>n. c k \<noteq> 0") |
|
263 case True then show ?thesis |
|
264 by (blast intro: polyfun_rootbound_finite) |
|
265 next |
|
266 case False then show ?thesis |
|
267 by (auto simp: infinite_UNIV_char_0) |
|
268 qed |
|
269 |
|
270 lemma polyfun_eq_0: |
|
271 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}" |
|
272 shows "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)" |
|
273 proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)") |
|
274 case True |
|
275 then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}" |
|
276 by (simp add: infinite_UNIV_char_0) |
|
277 with True show ?thesis |
|
278 by (metis (poly_guards_query) polyfun_rootbound_finite) |
|
279 next |
|
280 case False |
|
281 then show ?thesis |
|
282 by auto |
|
283 qed |
|
284 |
|
285 lemma polyfun_eq_const: |
|
286 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}" |
|
287 shows "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = k) \<longleftrightarrow> c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)" |
|
288 proof - |
|
289 {fix z |
|
290 have "(\<Sum>i\<le>n. c i * z^i) = (\<Sum>i\<le>n. (if i = 0 then c 0 - k else c i) * z^i) + k" |
|
291 by (induct n) auto |
|
292 } then |
|
293 have "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = k) \<longleftrightarrow> (\<forall>z. (\<Sum>i\<le>n. (if i = 0 then c 0 - k else c i) * z^i) = 0)" |
|
294 by auto |
|
295 also have "... \<longleftrightarrow> c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)" |
|
296 by (auto simp: polyfun_eq_0) |
|
297 finally show ?thesis . |
|
298 qed |
|
299 |
|
300 end |
|
301 |
|