src/HOL/Analysis/Poly_Roots.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 64267 b9a1486e79be child 67968 a5ad4c015d1c permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
 lp15@56215 ` 1` ```(* Author: John Harrison and Valentina Bruno ``` lp15@56215 ` 2` ``` Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson ``` lp15@56215 ` 3` ```*) ``` lp15@56215 ` 4` wenzelm@61560 ` 5` ```section \polynomial functions: extremal behaviour and root counts\ ``` wenzelm@61560 ` 6` hoelzl@63594 ` 7` ```theory Poly_Roots ``` lp15@56215 ` 8` ```imports Complex_Main ``` lp15@56215 ` 9` ```begin ``` lp15@56215 ` 10` wenzelm@60420 ` 11` ```subsection\Basics about polynomial functions: extremal behaviour and root counts.\ ``` lp15@56215 ` 12` lp15@56215 ` 13` ```lemma sub_polyfun: ``` lp15@56215 ` 14` ``` fixes x :: "'a::{comm_ring,monoid_mult}" ``` lp15@61609 ` 15` ``` shows "(\i\n. a i * x^i) - (\i\n. a i * y^i) = ``` lp15@56215 ` 16` ``` (x - y) * (\jk= Suc j..n. a k * y^(k - Suc j) * x^j)" ``` lp15@56215 ` 17` ```proof - ``` lp15@61609 ` 18` ``` have "(\i\n. a i * x^i) - (\i\n. a i * y^i) = ``` lp15@56215 ` 19` ``` (\i\n. a i * (x^i - y^i))" ``` nipkow@64267 ` 20` ``` by (simp add: algebra_simps sum_subtractf [symmetric]) ``` lp15@56215 ` 21` ``` also have "... = (\i\n. a i * (x - y) * (\ji\n. (\jji=Suc j..n. a i * y^(i - Suc j) * x^j))" ``` nipkow@64267 ` 26` ``` by (simp add: nested_sum_swap') ``` lp15@56215 ` 27` ``` finally show ?thesis . ``` lp15@56215 ` 28` ```qed ``` lp15@56215 ` 29` lp15@56215 ` 30` ```lemma sub_polyfun_alt: ``` lp15@56215 ` 31` ``` fixes x :: "'a::{comm_ring,monoid_mult}" ``` lp15@61609 ` 32` ``` shows "(\i\n. a i * x^i) - (\i\n. a i * y^i) = ``` lp15@56215 ` 33` ``` (x - y) * (\jkk = Suc j..n. a k * y^(k - Suc j) * x^j) = ``` lp15@56215 ` 37` ``` (\k b. \z. (\i\n. c i * z^i) = ``` lp15@56215 ` 46` ``` (z-a) * (\ii\n. c i * a^i)" ``` lp15@56215 ` 47` ```proof - ``` lp15@56215 ` 48` ``` { fix z ``` lp15@61609 ` 49` ``` have "(\i\n. c i * z^i) - (\i\n. c i * a^i) = ``` lp15@56215 ` 50` ``` (z - a) * (\jk = Suc j..n. c k * a^(k - Suc j)) * z^j)" ``` nipkow@64267 ` 51` ``` by (simp add: sub_polyfun sum_distrib_right) ``` lp15@61609 ` 52` ``` then have "(\i\n. c i * z^i) = ``` lp15@56215 ` 53` ``` (z - a) * (\jk = Suc j..n. c k * a^(k - Suc j)) * z^j) ``` lp15@56215 ` 54` ``` + (\i\n. c i * a^i)" ``` lp15@56215 ` 55` ``` by (simp add: algebra_simps) } ``` lp15@56215 ` 56` ``` then show ?thesis ``` lp15@61609 ` 57` ``` by (intro exI allI) ``` lp15@56215 ` 58` ```qed ``` lp15@56215 ` 59` lp15@56215 ` 60` ```lemma polyfun_linear_factor_root: ``` lp15@56215 ` 61` ``` fixes a :: "'a::{comm_ring,monoid_mult}" ``` lp15@56215 ` 62` ``` assumes "(\i\n. c i * a^i) = 0" ``` lp15@56215 ` 63` ``` shows "\b. \z. (\i\n. c i * z^i) = (z-a) * (\i b ==> norm(x) \ a ==> norm(x + y) \ b" ``` lp15@56215 ` 68` ``` by (metis norm_triangle_mono order.trans order_refl) ``` lp15@56215 ` 69` lp15@56215 ` 70` ```lemma polyfun_extremal_lemma: ``` lp15@56215 ` 71` ``` fixes c :: "nat \ 'a::real_normed_div_algebra" ``` lp15@56215 ` 72` ``` assumes "e > 0" ``` lp15@56215 ` 73` ``` shows "\M. \z. M \ norm z \ norm(\i\n. c i * z^i) \ e * norm(z) ^ Suc n" ``` lp15@56215 ` 74` ```proof (induction n) ``` lp15@56215 ` 75` ``` case 0 ``` lp15@61609 ` 76` ``` show ?case ``` haftmann@57512 ` 77` ``` by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms) ``` lp15@56215 ` 78` ```next ``` lp15@56215 ` 79` ``` case (Suc n) ``` lp15@56215 ` 80` ``` then obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" .. ``` lp15@56215 ` 81` ``` show ?case ``` lp15@56215 ` 82` ``` proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify) ``` lp15@56215 ` 83` ``` fix z::'a ``` lp15@56215 ` 84` ``` assume "max 1 (max M ((e + norm (c (Suc n))) / e)) \ norm z" ``` lp15@56215 ` 85` ``` then have norm1: "0 < norm z" "M \ norm z" "(e + norm (c (Suc n))) / e \ norm z" ``` lp15@56215 ` 86` ``` by auto ``` lp15@56215 ` 87` ``` then have norm2: "(e + norm (c (Suc n))) \ e * norm z" "(norm z * norm z ^ n) > 0" ``` lp15@61609 ` 88` ``` apply (metis assms less_divide_eq mult.commute not_le) ``` lp15@56215 ` 89` ``` using norm1 apply (metis mult_pos_pos zero_less_power) ``` lp15@56215 ` 90` ``` done ``` lp15@56215 ` 91` ``` have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) = ``` lp15@56215 ` 92` ``` (e + norm (c (Suc n))) * (norm z * norm z ^ n)" ``` lp15@56215 ` 93` ``` by (simp add: norm_mult norm_power algebra_simps) ``` lp15@56215 ` 94` ``` also have "... \ (e * norm z) * (norm z * norm z ^ n)" ``` lp15@61609 ` 95` ``` using norm2 by (metis real_mult_le_cancel_iff1) ``` lp15@56215 ` 96` ``` also have "... = e * (norm z * (norm z * norm z ^ n))" ``` lp15@56215 ` 97` ``` by (simp add: algebra_simps) ``` lp15@56215 ` 98` ``` finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) ``` lp15@56215 ` 99` ``` \ e * (norm z * (norm z * norm z ^ n))" . ``` lp15@56215 ` 100` ``` then show "norm (\i\Suc n. c i * z^i) \ e * norm z ^ Suc (Suc n)" using M norm1 ``` lp15@56215 ` 101` ``` by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle) ``` lp15@56215 ` 102` ``` qed ``` lp15@56215 ` 103` ```qed ``` lp15@56215 ` 104` lp15@62626 ` 105` ```lemma norm_lemma_xy: assumes "\b\ + 1 \ norm(y) - a" "norm(x) \ a" shows "b \ norm(x + y)" ``` lp15@62626 ` 106` ```proof - ``` lp15@62626 ` 107` ``` have "b \ norm y - norm x" ``` lp15@62626 ` 108` ``` using assms by linarith ``` lp15@62626 ` 109` ``` then show ?thesis ``` lp15@62626 ` 110` ``` by (metis (no_types) add.commute norm_diff_ineq order_trans) ``` lp15@62626 ` 111` ```qed ``` lp15@56215 ` 112` lp15@56215 ` 113` ```lemma polyfun_extremal: ``` lp15@56215 ` 114` ``` fixes c :: "nat \ 'a::real_normed_div_algebra" ``` lp15@56215 ` 115` ``` assumes "\k. k \ 0 \ k \ n \ c k \ 0" ``` lp15@56215 ` 116` ``` shows "eventually (\z. norm(\i\n. c i * z^i) \ B) at_infinity" ``` lp15@56215 ` 117` ```using assms ``` lp15@56215 ` 118` ```proof (induction n) ``` lp15@56215 ` 119` ``` case 0 then show ?case ``` lp15@56215 ` 120` ``` by simp ``` lp15@56215 ` 121` ```next ``` lp15@56215 ` 122` ``` case (Suc n) ``` lp15@56215 ` 123` ``` show ?case ``` lp15@56215 ` 124` ``` proof (cases "c (Suc n) = 0") ``` lp15@56215 ` 125` ``` case True ``` lp15@56215 ` 126` ``` with Suc show ?thesis ``` lp15@56215 ` 127` ``` by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq) ``` lp15@56215 ` 128` ``` next ``` lp15@56215 ` 129` ``` case False ``` lp15@56215 ` 130` ``` with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n] ``` lp15@61609 ` 131` ``` obtain M where M: "\z. M \ norm z \ ``` lp15@56215 ` 132` ``` norm (\i\n. c i * z^i) \ norm (c (Suc n)) / 2 * norm z ^ Suc n" ``` lp15@56215 ` 133` ``` by auto ``` lp15@56215 ` 134` ``` show ?thesis ``` lp15@56215 ` 135` ``` unfolding eventually_at_infinity ``` wenzelm@61945 ` 136` ``` proof (rule exI [where x="max M (max 1 ((\B\ + 1) / (norm (c (Suc n)) / 2)))"], clarsimp) ``` lp15@56215 ` 137` ``` fix z::'a ``` lp15@56215 ` 138` ``` assume les: "M \ norm z" "1 \ norm z" "(\B\ * 2 + 2) / norm (c (Suc n)) \ norm z" ``` lp15@56215 ` 139` ``` then have "\B\ * 2 + 2 \ norm z * norm (c (Suc n))" ``` lp15@56215 ` 140` ``` by (metis False pos_divide_le_eq zero_less_norm_iff) ``` lp15@61609 ` 141` ``` then have "\B\ * 2 + 2 \ norm z ^ (Suc n) * norm (c (Suc n))" ``` wenzelm@60420 ` 142` ``` by (metis \1 \ norm z\ order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc) ``` lp15@56215 ` 143` ``` then show "B \ norm ((\i\n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les ``` lp15@56215 ` 144` ``` apply auto ``` lp15@56215 ` 145` ``` apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"]) ``` lp15@56215 ` 146` ``` apply (simp_all add: norm_mult norm_power) ``` lp15@56215 ` 147` ``` done ``` lp15@56215 ` 148` ``` qed ``` lp15@56215 ` 149` ``` qed ``` lp15@56215 ` 150` ```qed ``` lp15@56215 ` 151` lp15@56215 ` 152` ```lemma polyfun_rootbound: ``` lp15@56215 ` 153` ``` fixes c :: "nat \ 'a::{comm_ring,real_normed_div_algebra}" ``` lp15@56215 ` 154` ``` assumes "\k. k \ n \ c k \ 0" ``` lp15@56215 ` 155` ``` shows "finite {z. (\i\n. c i * z^i) = 0} \ card {z. (\i\n. c i * z^i) = 0} \ n" ``` lp15@56215 ` 156` ```using assms ``` lp15@56215 ` 157` ```proof (induction n arbitrary: c) ``` lp15@56215 ` 158` ``` case (Suc n) show ?case ``` lp15@56215 ` 159` ``` proof (cases "{z. (\i\Suc n. c i * z^i) = 0} = {}") ``` lp15@56215 ` 160` ``` case False ``` lp15@56215 ` 161` ``` then obtain a where a: "(\i\Suc n. c i * a^i) = 0" ``` lp15@56215 ` 162` ``` by auto ``` lp15@56215 ` 163` ``` from polyfun_linear_factor_root [OF this] ``` lp15@56215 ` 164` ``` obtain b where "\z. (\i\Suc n. c i * z^i) = (z - a) * (\i< Suc n. b i * z^i)" ``` lp15@56215 ` 165` ``` by auto ``` lp15@56215 ` 166` ``` then have b: "\z. (\i\Suc n. c i * z^i) = (z - a) * (\i\n. b i * z^i)" ``` lp15@56215 ` 167` ``` by (metis lessThan_Suc_atMost) ``` lp15@56215 ` 168` ``` then have ins_ab: "{z. (\i\Suc n. c i * z^i) = 0} = insert a {z. (\i\n. b i * z^i) = 0}" ``` lp15@56215 ` 169` ``` by auto ``` lp15@56215 ` 170` ``` have c0: "c 0 = - (a * b 0)" using b [of 0] ``` lp15@56215 ` 171` ``` by simp ``` lp15@56215 ` 172` ``` then have extr_prem: "~ (\k\n. b k \ 0) \ \k. k \ 0 \ k \ Suc n \ c k \ 0" ``` lp15@56215 ` 173` ``` by (metis Suc.prems le0 minus_zero mult_zero_right) ``` lp15@61609 ` 174` ``` have "\k\n. b k \ 0" ``` lp15@56215 ` 175` ``` apply (rule ccontr) ``` lp15@56215 ` 176` ``` using polyfun_extremal [OF extr_prem, of 1] ``` nipkow@64267 ` 177` ``` apply (auto simp: eventually_at_infinity b simp del: sum_atMost_Suc) ``` lp15@56215 ` 178` ``` apply (drule_tac x="of_real ba" in spec, simp) ``` lp15@56215 ` 179` ``` done ``` lp15@56215 ` 180` ``` then show ?thesis using Suc.IH [of b] ins_ab ``` lp15@56215 ` 181` ``` by (auto simp: card_insert_if) ``` lp15@56215 ` 182` ``` qed simp ``` lp15@56215 ` 183` ```qed simp ``` lp15@56215 ` 184` lp15@56215 ` 185` ```corollary ``` lp15@56215 ` 186` ``` fixes c :: "nat \ 'a::{comm_ring,real_normed_div_algebra}" ``` lp15@56215 ` 187` ``` assumes "\k. k \ n \ c k \ 0" ``` lp15@56215 ` 188` ``` shows polyfun_rootbound_finite: "finite {z. (\i\n. c i * z^i) = 0}" ``` lp15@56215 ` 189` ``` and polyfun_rootbound_card: "card {z. (\i\n. c i * z^i) = 0} \ n" ``` lp15@56215 ` 190` ```using polyfun_rootbound [OF assms] by auto ``` lp15@56215 ` 191` lp15@56215 ` 192` ```lemma polyfun_finite_roots: ``` lp15@56215 ` 193` ``` fixes c :: "nat \ 'a::{comm_ring,real_normed_div_algebra}" ``` lp15@56215 ` 194` ``` shows "finite {z. (\i\n. c i * z^i) = 0} \ (\k. k \ n \ c k \ 0)" ``` lp15@56215 ` 195` ```proof (cases " \k\n. c k \ 0") ``` lp15@61609 ` 196` ``` case True then show ?thesis ``` lp15@56215 ` 197` ``` by (blast intro: polyfun_rootbound_finite) ``` lp15@56215 ` 198` ```next ``` lp15@61609 ` 199` ``` case False then show ?thesis ``` lp15@56215 ` 200` ``` by (auto simp: infinite_UNIV_char_0) ``` lp15@56215 ` 201` ```qed ``` lp15@56215 ` 202` lp15@56215 ` 203` ```lemma polyfun_eq_0: ``` lp15@56215 ` 204` ``` fixes c :: "nat \ 'a::{comm_ring,real_normed_div_algebra}" ``` lp15@56215 ` 205` ``` shows "(\z. (\i\n. c i * z^i) = 0) \ (\k. k \ n \ c k = 0)" ``` lp15@56215 ` 206` ```proof (cases "(\z. (\i\n. c i * z^i) = 0)") ``` lp15@56215 ` 207` ``` case True ``` lp15@56215 ` 208` ``` then have "~ finite {z. (\i\n. c i * z^i) = 0}" ``` lp15@56215 ` 209` ``` by (simp add: infinite_UNIV_char_0) ``` lp15@56215 ` 210` ``` with True show ?thesis ``` lp15@56215 ` 211` ``` by (metis (poly_guards_query) polyfun_rootbound_finite) ``` lp15@56215 ` 212` ```next ``` lp15@56215 ` 213` ``` case False ``` lp15@56215 ` 214` ``` then show ?thesis ``` lp15@56215 ` 215` ``` by auto ``` lp15@56215 ` 216` ```qed ``` lp15@56215 ` 217` lp15@56215 ` 218` ```lemma polyfun_eq_const: ``` lp15@56215 ` 219` ``` fixes c :: "nat \ 'a::{comm_ring,real_normed_div_algebra}" ``` lp15@56215 ` 220` ``` shows "(\z. (\i\n. c i * z^i) = k) \ c 0 = k \ (\k. k \ 0 \ k \ n \ c k = 0)" ``` lp15@56215 ` 221` ```proof - ``` lp15@56215 ` 222` ``` {fix z ``` lp15@56215 ` 223` ``` have "(\i\n. c i * z^i) = (\i\n. (if i = 0 then c 0 - k else c i) * z^i) + k" ``` lp15@56215 ` 224` ``` by (induct n) auto ``` lp15@56215 ` 225` ``` } then ``` lp15@56215 ` 226` ``` have "(\z. (\i\n. c i * z^i) = k) \ (\z. (\i\n. (if i = 0 then c 0 - k else c i) * z^i) = 0)" ``` lp15@56215 ` 227` ``` by auto ``` lp15@56215 ` 228` ``` also have "... \ c 0 = k \ (\k. k \ 0 \ k \ n \ c k = 0)" ``` lp15@56215 ` 229` ``` by (auto simp: polyfun_eq_0) ``` lp15@56215 ` 230` ``` finally show ?thesis . ``` lp15@56215 ` 231` ```qed ``` lp15@56215 ` 232` lp15@56215 ` 233` ```end ``` lp15@56215 ` 234`