16 |
16 |
17 lemma csqrt[algebra]: "csqrt z ^ 2 = z" |
17 lemma csqrt[algebra]: "csqrt z ^ 2 = z" |
18 proof- |
18 proof- |
19 obtain x y where xy: "z = Complex x y" by (cases z) |
19 obtain x y where xy: "z = Complex x y" by (cases z) |
20 {assume y0: "y = 0" |
20 {assume y0: "y = 0" |
21 {assume x0: "x \<ge> 0" |
21 {assume x0: "x \<ge> 0" |
22 then have ?thesis using y0 xy real_sqrt_pow2[OF x0] |
22 then have ?thesis using y0 xy real_sqrt_pow2[OF x0] |
23 by (simp add: csqrt_def power2_eq_square)} |
23 by (simp add: csqrt_def power2_eq_square)} |
24 moreover |
24 moreover |
25 {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith |
25 {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith |
26 then have ?thesis using y0 xy real_sqrt_pow2[OF x0] |
26 then have ?thesis using y0 xy real_sqrt_pow2[OF x0] |
27 by (simp add: csqrt_def power2_eq_square) } |
27 by (simp add: csqrt_def power2_eq_square) } |
28 ultimately have ?thesis by blast} |
28 ultimately have ?thesis by blast} |
29 moreover |
29 moreover |
30 {assume y0: "y\<noteq>0" |
30 {assume y0: "y\<noteq>0" |
31 {fix x y |
31 {fix x y |
32 let ?z = "Complex x y" |
32 let ?z = "Complex x y" |
33 from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto |
33 from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto |
34 hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+ |
34 hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+ |
35 hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) } |
35 hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) } |
36 note th = this |
36 note th = this |
37 have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2" |
37 have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2" |
38 by (simp add: power2_eq_square) |
38 by (simp add: power2_eq_square) |
39 from th[of x y] |
39 from th[of x y] |
40 have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all |
40 have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all |
41 then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x" |
41 then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x" |
42 unfolding power2_eq_square by simp |
42 unfolding power2_eq_square by simp |
43 have "sqrt 4 = sqrt (2^2)" by simp |
43 have "sqrt 4 = sqrt (2^2)" by simp |
44 hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs) |
44 hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs) |
45 have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y" |
45 have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y" |
46 using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0 |
46 using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0 |
47 unfolding power2_eq_square |
47 unfolding power2_eq_square |
48 by (simp add: algebra_simps real_sqrt_divide sqrt4) |
48 by (simp add: algebra_simps real_sqrt_divide sqrt4) |
49 from y0 xy have ?thesis apply (simp add: csqrt_def power2_eq_square) |
49 from y0 xy have ?thesis apply (simp add: csqrt_def power2_eq_square) |
50 apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric]) |
50 apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric]) |
51 using th1 th2 ..} |
51 using th1 th2 ..} |
52 ultimately show ?thesis by blast |
52 ultimately show ?thesis by blast |
214 hence "\<exists>z. ?P z n" ..} |
214 hence "\<exists>z. ?P z n" ..} |
215 moreover |
215 moreover |
216 {assume o: "odd n" |
216 {assume o: "odd n" |
217 from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp |
217 from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp |
218 have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) + |
218 have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) + |
219 Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = |
219 Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = |
220 ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra |
220 ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra |
221 also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2" |
221 also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2" |
222 apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"] |
222 apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"] |
223 by (simp add: power2_eq_square) |
223 by (simp add: power2_eq_square) |
224 finally |
224 finally |
225 have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) + |
225 have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) + |
226 Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = |
226 Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = |
227 1" |
227 1" |
228 apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric]) |
228 apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric]) |
229 using right_inverse[OF b'] |
229 using right_inverse[OF b'] |
230 by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps) |
230 by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps) |
231 have th0: "cmod (complex_of_real (cmod b) / b) = 1" |
231 have th0: "cmod (complex_of_real (cmod b) / b) = 1" |
232 apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps ) |
232 apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps ) |
233 by (simp add: real_sqrt_mult[symmetric] th0) |
233 by (simp add: real_sqrt_mult[symmetric] th0) |
234 from o have "\<exists>m. n = Suc (2*m)" by presburger+ |
234 from o have "\<exists>m. n = Suc (2*m)" by presburger+ |
235 then obtain m where m: "n = Suc (2*m)" by blast |
235 then obtain m where m: "n = Suc (2*m)" by blast |
236 from unimodular_reduce_norm[OF th0] o |
236 from unimodular_reduce_norm[OF th0] o |
237 have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1" |
237 have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1" |
238 apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp) |
238 apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp) |
301 apply (simp add: Bseq_def) |
301 apply (simp add: Bseq_def) |
302 apply (rule exI[where x= "r + 1"]) |
302 apply (rule exI[where x= "r + 1"]) |
303 using th rp apply simp |
303 using th rp apply simp |
304 using g(2) . |
304 using g(2) . |
305 |
305 |
306 from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x" |
306 from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x" |
307 by blast |
307 by blast |
308 hence x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r" |
308 hence x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r" |
309 unfolding LIMSEQ_def real_norm_def . |
309 unfolding LIMSEQ_def real_norm_def . |
310 |
310 |
311 from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y" |
311 from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y" |
312 by blast |
312 by blast |
313 hence y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r" |
313 hence y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r" |
314 unfolding LIMSEQ_def real_norm_def . |
314 unfolding LIMSEQ_def real_norm_def . |
315 let ?w = "Complex x y" |
315 let ?w = "Complex x y" |
316 from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto |
316 from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto |
317 {fix e assume ep: "e > (0::real)" |
317 {fix e assume ep: "e > (0::real)" |
318 hence e2: "e/2 > 0" by simp |
318 hence e2: "e/2 > 0" by simp |
319 from x[rule_format, OF e2] y[rule_format, OF e2] |
319 from x[rule_format, OF e2] y[rule_format, OF e2] |
320 obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast |
320 obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast |
321 {fix n assume nN12: "n \<ge> N1 + N2" |
321 {fix n assume nN12: "n \<ge> N1 + N2" |
322 hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+ |
322 hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+ |
323 from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]] |
323 from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]] |
324 have "cmod (s (?h n) - ?w) < e" |
324 have "cmod (s (?h n) - ?w) < e" |
325 using metric_bound_lemma[of "s (f (g n))" ?w] by simp } |
325 using metric_bound_lemma[of "s (f (g n))" ?w] by simp } |
326 hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast } |
326 hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast } |
327 with hs show ?thesis by blast |
327 with hs show ?thesis by blast |
328 qed |
328 qed |
329 |
329 |
330 text{* Polynomial is continuous. *} |
330 text{* Polynomial is continuous. *} |
331 |
331 |
332 lemma poly_cont: |
332 lemma poly_cont: |
333 assumes ep: "e > 0" |
333 assumes ep: "e > 0" |
334 shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e" |
334 shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e" |
335 proof- |
335 proof- |
336 obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)" |
336 obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)" |
337 proof |
337 proof |
338 show "degree (offset_poly p z) = degree p" |
338 show "degree (offset_poly p z) = degree p" |
346 show ?thesis unfolding th[symmetric] |
346 show ?thesis unfolding th[symmetric] |
347 proof(induct q) |
347 proof(induct q) |
348 case 0 thus ?case using ep by auto |
348 case 0 thus ?case using ep by auto |
349 next |
349 next |
350 case (pCons c cs) |
350 case (pCons c cs) |
351 from poly_bound_exists[of 1 "cs"] |
351 from poly_bound_exists[of 1 "cs"] |
352 obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast |
352 obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast |
353 from ep m(1) have em0: "e/m > 0" by (simp add: field_simps) |
353 from ep m(1) have em0: "e/m > 0" by (simp add: field_simps) |
354 have one0: "1 > (0::real)" by arith |
354 have one0: "1 > (0::real)" by arith |
355 from real_lbound_gt_zero[OF one0 em0] |
355 from real_lbound_gt_zero[OF one0 em0] |
356 obtain d where d: "d >0" "d < 1" "d < e / m" by blast |
356 obtain d where d: "d >0" "d < 1" "d < e / m" by blast |
357 from d(1,3) m(1) have dm: "d*m > 0" "d*m < e" |
357 from d(1,3) m(1) have dm: "d*m > 0" "d*m < e" |
358 by (simp_all add: field_simps real_mult_order) |
358 by (simp_all add: field_simps real_mult_order) |
359 show ?case |
359 show ?case |
360 proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult) |
360 proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult) |
361 fix d w |
361 fix d w |
362 assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d" |
362 assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d" |
363 hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all |
363 hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all |
364 from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps) |
364 from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps) |
365 from H have th: "cmod (w-z) \<le> d" by simp |
365 from H have th: "cmod (w-z) \<le> d" by simp |
366 from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme |
366 from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme |
367 show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp |
367 show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp |
368 qed |
368 qed |
369 qed |
369 qed |
370 qed |
370 qed |
371 |
371 |
372 text{* Hence a polynomial attains minimum on a closed disc |
372 text{* Hence a polynomial attains minimum on a closed disc |
373 in the complex plane. *} |
373 in the complex plane. *} |
374 lemma poly_minimum_modulus_disc: |
374 lemma poly_minimum_modulus_disc: |
375 "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)" |
375 "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)" |
376 proof- |
376 proof- |
377 {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le |
377 {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le |
378 apply - |
378 apply - |
379 apply (rule exI[where x=0]) |
379 apply (rule exI[where x=0]) |
380 apply auto |
380 apply auto |
381 apply (subgoal_tac "cmod w < 0") |
381 apply (subgoal_tac "cmod w < 0") |
382 apply simp |
382 apply simp |
383 apply arith |
383 apply arith |
384 done } |
384 done } |
385 moreover |
385 moreover |
386 {assume rp: "r \<ge> 0" |
386 {assume rp: "r \<ge> 0" |
387 from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp |
387 from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp |
388 hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x" by blast |
388 hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x" by blast |
389 {fix x z |
389 {fix x z |
390 assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1" |
390 assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1" |
391 hence "- x < 0 " by arith |
391 hence "- x < 0 " by arith |
392 with H(2) norm_ge_zero[of "poly p z"] have False by simp } |
392 with H(2) norm_ge_zero[of "poly p z"] have False by simp } |
393 then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast |
393 then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast |
394 from real_sup_exists[OF mth1 mth2] obtain s where |
394 from real_sup_exists[OF mth1 mth2] obtain s where |
395 s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow>(y < s)" by blast |
395 s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow>(y < s)" by blast |
396 let ?m = "-s" |
396 let ?m = "-s" |
397 {fix y |
397 {fix y |
398 from s[rule_format, of "-y"] have |
398 from s[rule_format, of "-y"] have |
399 "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" |
399 "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" |
400 unfolding minus_less_iff[of y ] equation_minus_iff by blast } |
400 unfolding minus_less_iff[of y ] equation_minus_iff by blast } |
401 note s1 = this[unfolded minus_minus] |
401 note s1 = this[unfolded minus_minus] |
402 from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m" |
402 from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m" |
403 by auto |
403 by auto |
404 {fix n::nat |
404 {fix n::nat |
405 from s1[rule_format, of "?m + 1/real (Suc n)"] |
405 from s1[rule_format, of "?m + 1/real (Suc n)"] |
406 have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" |
406 have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" |
407 by simp} |
407 by simp} |
408 hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" .. |
408 hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" .. |
409 from choice[OF th] obtain g where |
409 from choice[OF th] obtain g where |
410 g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)" |
410 g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)" |
411 by blast |
411 by blast |
412 from bolzano_weierstrass_complex_disc[OF g(1)] |
412 from bolzano_weierstrass_complex_disc[OF g(1)] |
413 obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e" |
413 obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e" |
414 by blast |
414 by blast |
415 {fix w |
415 {fix w |
416 assume wr: "cmod w \<le> r" |
416 assume wr: "cmod w \<le> r" |
417 let ?e = "\<bar>cmod (poly p z) - ?m\<bar>" |
417 let ?e = "\<bar>cmod (poly p z) - ?m\<bar>" |
418 {assume e: "?e > 0" |
418 {assume e: "?e > 0" |
419 hence e2: "?e/2 > 0" by simp |
419 hence e2: "?e/2 > 0" by simp |
420 from poly_cont[OF e2, of z p] obtain d where |
420 from poly_cont[OF e2, of z p] obtain d where |
421 d: "d>0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2" by blast |
421 d: "d>0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2" by blast |
422 {fix w assume w: "cmod (w - z) < d" |
422 {fix w assume w: "cmod (w - z) < d" |
423 have "cmod(poly p w - poly p z) < ?e / 2" |
423 have "cmod(poly p w - poly p z) < ?e / 2" |
424 using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)} |
424 using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)} |
425 note th1 = this |
425 note th1 = this |
426 |
426 |
427 from fz(2)[rule_format, OF d(1)] obtain N1 where |
427 from fz(2)[rule_format, OF d(1)] obtain N1 where |
428 N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast |
428 N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast |
429 from reals_Archimedean2[of "2/?e"] obtain N2::nat where |
429 from reals_Archimedean2[of "2/?e"] obtain N2::nat where |
430 N2: "2/?e < real N2" by blast |
430 N2: "2/?e < real N2" by blast |
431 have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2" |
431 have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2" |
432 using N1[rule_format, of "N1 + N2"] th1 by simp |
432 using N1[rule_format, of "N1 + N2"] th1 by simp |
433 {fix a b e2 m :: real |
433 {fix a b e2 m :: real |
434 have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a |
434 have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a |
435 ==> False" by arith} |
435 ==> False" by arith} |
436 note th0 = this |
436 note th0 = this |
437 have ath: |
437 have ath: |
438 "\<And>m x e. m <= x \<Longrightarrow> x < m + e ==> abs(x - m::real) < e" by arith |
438 "\<And>m x e. m <= x \<Longrightarrow> x < m + e ==> abs(x - m::real) < e" by arith |
439 from s1m[OF g(1)[rule_format]] |
439 from s1m[OF g(1)[rule_format]] |
440 have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" . |
440 have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" . |
441 from seq_suble[OF fz(1), of "N1+N2"] |
441 from seq_suble[OF fz(1), of "N1+N2"] |
442 have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp |
442 have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp |
443 have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0" |
443 have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0" |
444 using N2 by auto |
444 using N2 by auto |
445 from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp |
445 from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp |
446 from g(2)[rule_format, of "f (N1 + N2)"] |
446 from g(2)[rule_format, of "f (N1 + N2)"] |
447 have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" . |
447 have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" . |
448 from order_less_le_trans[OF th01 th00] |
448 from order_less_le_trans[OF th01 th00] |
449 have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" . |
449 have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" . |
450 from N2 have "2/?e < real (Suc (N1 + N2))" by arith |
450 from N2 have "2/?e < real (Suc (N1 + N2))" by arith |
451 with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"] |
451 with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"] |
452 have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide) |
452 have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide) |
453 with ath[OF th31 th32] |
453 with ath[OF th31 th32] |
454 have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith |
454 have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith |
455 have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c" |
455 have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c" |
456 by arith |
456 by arith |
457 have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar> |
457 have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar> |
458 \<le> cmod (poly p (g (f (N1 + N2))) - poly p z)" |
458 \<le> cmod (poly p (g (f (N1 + N2))) - poly p z)" |
459 by (simp add: norm_triangle_ineq3) |
459 by (simp add: norm_triangle_ineq3) |
460 from ath2[OF th22, of ?m] |
460 from ath2[OF th22, of ?m] |
461 have thc2: "2*(?e/2) \<le> \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)" by simp |
461 have thc2: "2*(?e/2) \<le> \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)" by simp |
462 from th0[OF th2 thc1 thc2] have False .} |
462 from th0[OF th2 thc1 thc2] have False .} |
463 hence "?e = 0" by auto |
463 hence "?e = 0" by auto |
464 then have "cmod (poly p z) = ?m" by simp |
464 then have "cmod (poly p z) = ?m" by simp |
465 with s1m[OF wr] |
465 with s1m[OF wr] |
466 have "cmod (poly p z) \<le> cmod (poly p w)" by simp } |
466 have "cmod (poly p z) \<le> cmod (poly p w)" by simp } |
467 hence ?thesis by blast} |
467 hence ?thesis by blast} |
468 ultimately show ?thesis by blast |
468 ultimately show ?thesis by blast |
469 qed |
469 qed |
502 from h have z1: "cmod z \<ge> 1" by arith |
502 from h have z1: "cmod z \<ge> 1" by arith |
503 from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]] |
503 from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]] |
504 have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a" |
504 have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a" |
505 unfolding norm_mult by (simp add: algebra_simps) |
505 unfolding norm_mult by (simp add: algebra_simps) |
506 from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a] |
506 from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a] |
507 have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)" |
507 have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)" |
508 by (simp add: diff_le_eq algebra_simps) |
508 by (simp add: diff_le_eq algebra_simps) |
509 from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" by arith} |
509 from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" by arith} |
510 hence ?case by blast} |
510 hence ?case by blast} |
511 moreover |
511 moreover |
512 {assume cs0: "\<not> (cs \<noteq> 0)" |
512 {assume cs0: "\<not> (cs \<noteq> 0)" |
513 with pCons.prems have c0: "c \<noteq> 0" by simp |
513 with pCons.prems have c0: "c \<noteq> 0" by simp |
514 from cs0 have cs0': "cs = 0" by simp |
514 from cs0 have cs0': "cs = 0" by simp |
515 {fix z |
515 {fix z |
516 assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z" |
516 assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z" |
517 from c0 have "cmod c > 0" by simp |
517 from c0 have "cmod c > 0" by simp |
518 from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)" |
518 from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)" |
519 by (simp add: field_simps norm_mult) |
519 by (simp add: field_simps norm_mult) |
520 have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith |
520 have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith |
521 from complex_mod_triangle_sub[of "z*c" a ] |
521 from complex_mod_triangle_sub[of "z*c" a ] |
522 have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a" |
522 have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a" |
523 by (simp add: algebra_simps) |
523 by (simp add: algebra_simps) |
524 from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" |
524 from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" |
525 using cs0' by simp} |
525 using cs0' by simp} |
526 then have ?case by blast} |
526 then have ?case by blast} |
527 ultimately show ?case by blast |
527 ultimately show ?case by blast |
528 qed simp |
528 qed simp |
529 |
529 |
530 text {* Hence polynomial's modulus attains its minimum somewhere. *} |
530 text {* Hence polynomial's modulus attains its minimum somewhere. *} |
531 lemma poly_minimum_modulus: |
531 lemma poly_minimum_modulus: |
532 "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)" |
532 "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)" |
533 proof(induct p) |
533 proof(induct p) |
534 case (pCons c cs) |
534 case (pCons c cs) |
535 {assume cs0: "cs \<noteq> 0" |
535 {assume cs0: "cs \<noteq> 0" |
536 from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c] |
536 from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c] |
537 obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)" by blast |
537 obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)" by blast |
538 have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith |
538 have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith |
539 from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"] |
539 from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"] |
540 obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)" by blast |
540 obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)" by blast |
541 {fix z assume z: "r \<le> cmod z" |
541 {fix z assume z: "r \<le> cmod z" |
542 from v[of 0] r[OF z] |
542 from v[of 0] r[OF z] |
543 have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" |
543 have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" |
544 by simp } |
544 by simp } |
545 note v0 = this |
545 note v0 = this |
546 from v0 v ath[of r] have ?case by blast} |
546 from v0 v ath[of r] have ?case by blast} |
547 moreover |
547 moreover |
631 let ?p = "poly p" |
631 let ?p = "poly p" |
632 assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p" |
632 assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p" |
633 let ?ths = "\<exists>z. ?p z = 0" |
633 let ?ths = "\<exists>z. ?p z = 0" |
634 |
634 |
635 from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n) |
635 from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n) |
636 from poly_minimum_modulus obtain c where |
636 from poly_minimum_modulus obtain c where |
637 c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast |
637 c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast |
638 {assume pc: "?p c = 0" hence ?ths by blast} |
638 {assume pc: "?p c = 0" hence ?ths by blast} |
639 moreover |
639 moreover |
640 {assume pc0: "?p c \<noteq> 0" |
640 {assume pc0: "?p c \<noteq> 0" |
641 from poly_offset[of p c] obtain q where |
641 from poly_offset[of p c] obtain q where |
642 q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast |
642 q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast |
643 {assume h: "constant (poly q)" |
643 {assume h: "constant (poly q)" |
644 from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto |
644 from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto |
645 {fix x y |
645 {fix x y |
646 from th have "?p x = poly q (x - c)" by auto |
646 from th have "?p x = poly q (x - c)" by auto |
647 also have "\<dots> = poly q (y - c)" |
647 also have "\<dots> = poly q (y - c)" |
648 using h unfolding constant_def by blast |
648 using h unfolding constant_def by blast |
649 also have "\<dots> = ?p y" using th by auto |
649 also have "\<dots> = ?p y" using th by auto |
650 finally have "?p x = ?p y" .} |
650 finally have "?p x = ?p y" .} |
651 with nc have False unfolding constant_def by blast } |
651 with nc have False unfolding constant_def by blast } |
652 hence qnc: "\<not> constant (poly q)" by blast |
652 hence qnc: "\<not> constant (poly q)" by blast |
653 from q(2) have pqc0: "?p c = poly q 0" by simp |
653 from q(2) have pqc0: "?p c = poly q 0" by simp |
654 from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp |
654 from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp |
655 let ?a0 = "poly q 0" |
655 let ?a0 = "poly q 0" |
656 from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp |
656 from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp |
657 from a00 |
657 from a00 |
658 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0" |
658 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0" |
659 by simp |
659 by simp |
660 let ?r = "smult (inverse ?a0) q" |
660 let ?r = "smult (inverse ?a0) q" |
661 have lgqr: "psize q = psize ?r" |
661 have lgqr: "psize q = psize ?r" |
662 using a00 unfolding psize_def degree_def |
662 using a00 unfolding psize_def degree_def |
663 by (simp add: expand_poly_eq) |
663 by (simp add: expand_poly_eq) |
664 {assume h: "\<And>x y. poly ?r x = poly ?r y" |
664 {assume h: "\<And>x y. poly ?r x = poly ?r y" |
665 {fix x y |
665 {fix x y |
666 from qr[rule_format, of x] |
666 from qr[rule_format, of x] |
667 have "poly q x = poly ?r x * ?a0" by auto |
667 have "poly q x = poly ?r x * ?a0" by auto |
668 also have "\<dots> = poly ?r y * ?a0" using h by simp |
668 also have "\<dots> = poly ?r y * ?a0" using h by simp |
669 also have "\<dots> = poly q y" using qr[rule_format, of y] by simp |
669 also have "\<dots> = poly q y" using qr[rule_format, of y] by simp |
670 finally have "poly q x = poly q y" .} |
670 finally have "poly q x = poly q y" .} |
671 with qnc have False unfolding constant_def by blast} |
671 with qnc have False unfolding constant_def by blast} |
672 hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast |
672 hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast |
673 from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1" by auto |
673 from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1" by auto |
674 {fix w |
674 {fix w |
675 have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1" |
675 have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1" |
676 using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac) |
676 using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac) |
677 also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0" |
677 also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0" |
678 using a00 unfolding norm_divide by (simp add: field_simps) |
678 using a00 unfolding norm_divide by (simp add: field_simps) |
679 finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .} |
679 finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .} |
680 note mrmq_eq = this |
680 note mrmq_eq = this |
681 from poly_decompose[OF rnc] obtain k a s where |
681 from poly_decompose[OF rnc] obtain k a s where |
682 kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r" |
682 kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r" |
683 "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast |
683 "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast |
684 {assume "k + 1 = n" |
684 {assume "k + 1 = n" |
685 with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto |
685 with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto |
686 {fix w |
686 {fix w |
687 have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" |
687 have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" |
688 using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)} |
688 using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)} |
689 note hth = this [symmetric] |
689 note hth = this [symmetric] |
690 from reduce_poly_simple[OF kas(1,2)] |
690 from reduce_poly_simple[OF kas(1,2)] |
691 have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast} |
691 have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast} |
692 moreover |
692 moreover |
693 {assume kn: "k+1 \<noteq> n" |
693 {assume kn: "k+1 \<noteq> n" |
694 from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp |
694 from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp |
695 have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))" |
695 have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))" |
696 unfolding constant_def poly_pCons poly_monom |
696 unfolding constant_def poly_pCons poly_monom |
697 using kas(1) apply simp |
697 using kas(1) apply simp |
698 by (rule exI[where x=0], rule exI[where x=1], simp) |
698 by (rule exI[where x=0], rule exI[where x=1], simp) |
699 from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))" |
699 from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))" |
700 by (simp add: psize_def degree_monom_eq) |
700 by (simp add: psize_def degree_monom_eq) |
701 from H[rule_format, OF k1n th01 th02] |
701 from H[rule_format, OF k1n th01 th02] |
702 obtain w where w: "1 + w^k * a = 0" |
702 obtain w where w: "1 + w^k * a = 0" |
703 unfolding poly_pCons poly_monom |
703 unfolding poly_pCons poly_monom |
704 using kas(2) by (cases k, auto simp add: algebra_simps) |
704 using kas(2) by (cases k, auto simp add: algebra_simps) |
705 from poly_bound_exists[of "cmod w" s] obtain m where |
705 from poly_bound_exists[of "cmod w" s] obtain m where |
706 m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast |
706 m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast |
707 have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left) |
707 have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left) |
708 from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp |
708 from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp |
709 then have wm1: "w^k * a = - 1" by simp |
709 then have wm1: "w^k * a = - 1" by simp |
710 have inv0: "0 < inverse (cmod w ^ (k + 1) * m)" |
710 have inv0: "0 < inverse (cmod w ^ (k + 1) * m)" |
711 using norm_ge_zero[of w] w0 m(1) |
711 using norm_ge_zero[of w] w0 m(1) |
712 by (simp add: inverse_eq_divide zero_less_mult_iff) |
712 by (simp add: inverse_eq_divide zero_less_mult_iff) |
713 with real_down2[OF zero_less_one] obtain t where |
713 with real_down2[OF zero_less_one] obtain t where |
714 t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast |
714 t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast |
715 let ?ct = "complex_of_real t" |
715 let ?ct = "complex_of_real t" |
716 let ?w = "?ct * w" |
716 let ?w = "?ct * w" |
717 have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: algebra_simps power_mult_distrib) |
717 have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: algebra_simps power_mult_distrib) |
718 also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w" |
718 also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w" |
719 unfolding wm1 by (simp) |
719 unfolding wm1 by (simp) |
720 finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)" |
720 finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)" |
721 apply - |
721 apply - |
722 apply (rule cong[OF refl[of cmod]]) |
722 apply (rule cong[OF refl[of cmod]]) |
723 apply assumption |
723 apply assumption |
724 done |
724 done |
725 with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"] |
725 with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"] |
726 have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp |
726 have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp |
727 have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith |
727 have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith |
728 have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto |
728 have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto |
729 then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult) |
729 then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult) |
730 from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1" |
730 from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1" |
731 by (simp add: inverse_eq_divide field_simps) |
731 by (simp add: inverse_eq_divide field_simps) |
732 with zero_less_power[OF t(1), of k] |
732 with zero_less_power[OF t(1), of k] |
733 have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" |
733 have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" |
734 apply - apply (rule mult_strict_left_mono) by simp_all |
734 apply - apply (rule mult_strict_left_mono) by simp_all |
735 have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))" using w0 t(1) |
735 have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))" using w0 t(1) |
736 by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult) |
736 by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult) |
737 then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))" |
737 then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))" |
738 using t(1,2) m(2)[rule_format, OF tw] w0 |
738 using t(1,2) m(2)[rule_format, OF tw] w0 |
739 apply (simp only: ) |
739 apply (simp only: ) |
740 apply auto |
740 apply auto |
741 apply (rule mult_mono, simp_all add: norm_ge_zero)+ |
741 apply (rule mult_mono, simp_all add: norm_ge_zero)+ |
742 apply (simp add: zero_le_mult_iff zero_le_power) |
742 apply (simp add: zero_le_mult_iff zero_le_power) |
743 done |
743 done |
744 with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp |
744 with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp |
745 from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1" |
745 from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1" |
746 by auto |
746 by auto |
747 from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121] |
747 from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121] |
748 have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" . |
748 have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" . |
749 from th11 th12 |
749 from th11 th12 |
750 have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1" by arith |
750 have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1" by arith |
751 then have "cmod (poly ?r ?w) < 1" |
751 then have "cmod (poly ?r ?w) < 1" |
752 unfolding kas(4)[rule_format, of ?w] r01 by simp |
752 unfolding kas(4)[rule_format, of ?w] r01 by simp |
753 then have "\<exists>w. cmod (poly ?r w) < 1" by blast} |
753 then have "\<exists>w. cmod (poly ?r w) < 1" by blast} |
754 ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast |
754 ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast |
755 from cr0_contr cq0 q(2) |
755 from cr0_contr cq0 q(2) |
756 have ?ths unfolding mrmq_eq not_less[symmetric] by auto} |
756 have ?ths unfolding mrmq_eq not_less[symmetric] by auto} |
757 ultimately show ?ths by blast |
757 ultimately show ?ths by blast |
964 apply (erule dvd_imp_degree_le [OF pq]) |
964 apply (erule dvd_imp_degree_le [OF pq]) |
965 done |
965 done |
966 |
966 |
967 (* Arithmetic operations on multivariate polynomials. *) |
967 (* Arithmetic operations on multivariate polynomials. *) |
968 |
968 |
969 lemma mpoly_base_conv: |
969 lemma mpoly_base_conv: |
970 "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all |
970 "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all |
971 |
971 |
972 lemma mpoly_norm_conv: |
972 lemma mpoly_norm_conv: |
973 "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all |
973 "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all |
974 |
974 |
975 lemma mpoly_sub_conv: |
975 lemma mpoly_sub_conv: |
976 "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x" |
976 "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x" |
977 by (simp add: diff_def) |
977 by (simp add: diff_def) |
978 |
978 |
979 lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp |
979 lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp |
980 |
980 |
981 lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto |
981 lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto |
982 |
982 |
983 lemma resolve_eq_raw: "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto |
983 lemma resolve_eq_raw: "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto |
984 lemma resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2)) |
984 lemma resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2)) |
985 \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast |
985 \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast |
986 |
986 |
987 lemma poly_divides_pad_rule: |
987 lemma poly_divides_pad_rule: |
988 fixes p q :: "complex poly" |
988 fixes p q :: "complex poly" |
989 assumes pq: "p dvd q" |
989 assumes pq: "p dvd q" |
990 shows "p dvd (pCons (0::complex) q)" |
990 shows "p dvd (pCons (0::complex) q)" |
991 proof- |
991 proof- |
992 have "pCons 0 q = q * [:0,1:]" by simp |
992 have "pCons 0 q = q * [:0,1:]" by simp |
993 then have "q dvd (pCons 0 q)" .. |
993 then have "q dvd (pCons 0 q)" .. |
994 with pq show ?thesis by (rule dvd_trans) |
994 with pq show ?thesis by (rule dvd_trans) |
995 qed |
995 qed |
996 |
996 |
997 lemma poly_divides_pad_const_rule: |
997 lemma poly_divides_pad_const_rule: |
998 fixes p q :: "complex poly" |
998 fixes p q :: "complex poly" |
999 assumes pq: "p dvd q" |
999 assumes pq: "p dvd q" |
1000 shows "p dvd (smult a q)" |
1000 shows "p dvd (smult a q)" |
1001 proof- |
1001 proof- |
1002 have "smult a q = q * [:a:]" by simp |
1002 have "smult a q = q * [:a:]" by simp |
1003 then have "q dvd smult a q" .. |
1003 then have "q dvd smult a q" .. |
1004 with pq show ?thesis by (rule dvd_trans) |
1004 with pq show ?thesis by (rule dvd_trans) |
1005 qed |
1005 qed |
1006 |
1006 |
1007 |
1007 |
1008 lemma poly_divides_conv0: |
1008 lemma poly_divides_conv0: |
1009 fixes p :: "complex poly" |
1009 fixes p :: "complex poly" |
1010 assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0" |
1010 assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0" |
1011 shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs") |
1011 shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs") |
1012 proof- |
1012 proof- |
1013 {assume r: ?rhs |
1013 {assume r: ?rhs |
1014 hence "q = p * 0" by simp |
1014 hence "q = p * 0" by simp |
1015 hence ?lhs ..} |
1015 hence ?lhs ..} |
1016 moreover |
1016 moreover |
1017 {assume l: ?lhs |
1017 {assume l: ?lhs |
1018 {assume q0: "q = 0" |
1018 {assume q0: "q = 0" |