src/HOL/Analysis/Poly_Roots.thy
author paulson <lp15@cam.ac.uk>
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
     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>Basics about polynomial functions: extremal behaviour and root counts.\<close>
    12 
    13 lemma sub_polyfun:
    14   fixes x :: "'a::{comm_ring,monoid_mult}"
    15   shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
    16            (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)"
    17 proof -
    18   have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
    19         (\<Sum>i\<le>n. a i * (x^i - y^i))"
    20     by (simp add: algebra_simps sum_subtractf [symmetric])
    21   also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
    22     by (simp add: power_diff_sumr2 ac_simps)
    23   also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
    24     by (simp add: sum_distrib_left ac_simps)
    25   also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
    26     by (simp add: nested_sum_swap')
    27   finally show ?thesis .
    28 qed
    29 
    30 lemma sub_polyfun_alt:
    31   fixes x :: "'a::{comm_ring,monoid_mult}"
    32   shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
    33            (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
    34 proof -
    35   { fix j
    36     have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) =
    37           (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)"
    38       by (rule sum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
    39   then show ?thesis
    40     by (simp add: sub_polyfun)
    41 qed
    42 
    43 lemma polyfun_linear_factor:
    44   fixes a :: "'a::{comm_ring,monoid_mult}"
    45   shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) =
    46                   (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)"
    47 proof -
    48   { fix z
    49     have "(\<Sum>i\<le>n. c i * z^i) - (\<Sum>i\<le>n. c i * a^i) =
    50           (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
    51       by (simp add: sub_polyfun sum_distrib_right)
    52     then have "(\<Sum>i\<le>n. c i * z^i) =
    53           (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)
    54           + (\<Sum>i\<le>n. c i * a^i)"
    55       by (simp add: algebra_simps) }
    56   then show ?thesis
    57     by (intro exI allI)
    58 qed
    59 
    60 lemma polyfun_linear_factor_root:
    61   fixes a :: "'a::{comm_ring,monoid_mult}"
    62   assumes "(\<Sum>i\<le>n. c i * a^i) = 0"
    63   shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)"
    64   using polyfun_linear_factor [of c n a] assms
    65   by simp
    66 
    67 lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
    68   by (metis norm_triangle_mono order.trans order_refl)
    69 
    70 lemma polyfun_extremal_lemma:
    71   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
    72   assumes "e > 0"
    73     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"
    74 proof (induction n)
    75   case 0
    76   show ?case
    77     by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms)
    78 next
    79   case (Suc n)
    80   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" ..
    81   show ?case
    82   proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify)
    83     fix z::'a
    84     assume "max 1 (max M ((e + norm (c (Suc n))) / e)) \<le> norm z"
    85     then have norm1: "0 < norm z" "M \<le> norm z" "(e + norm (c (Suc n))) / e \<le> norm z"
    86       by auto
    87     then have norm2: "(e + norm (c (Suc n))) \<le> e * norm z"  "(norm z * norm z ^ n) > 0"
    88       apply (metis assms less_divide_eq mult.commute not_le)
    89       using norm1 apply (metis mult_pos_pos zero_less_power)
    90       done
    91     have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) =
    92           (e + norm (c (Suc n))) * (norm z * norm z ^ n)"
    93       by (simp add: norm_mult norm_power algebra_simps)
    94     also have "... \<le> (e * norm z) * (norm z * norm z ^ n)"
    95       using norm2 by (metis real_mult_le_cancel_iff1)
    96     also have "... = e * (norm z * (norm z * norm z ^ n))"
    97       by (simp add: algebra_simps)
    98     finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n))
    99                   \<le> e * (norm z * (norm z * norm z ^ n))" .
   100     then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1
   101       by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle)
   102     qed
   103 qed
   104 
   105 lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
   106 proof -
   107   have "b \<le> norm y - norm x"
   108     using assms by linarith
   109   then show ?thesis
   110     by (metis (no_types) add.commute norm_diff_ineq order_trans)
   111 qed
   112 
   113 lemma polyfun_extremal:
   114   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   115   assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0"
   116     shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity"
   117 using assms
   118 proof (induction n)
   119   case 0 then show ?case
   120     by simp
   121 next
   122   case (Suc n)
   123   show ?case
   124   proof (cases "c (Suc n) = 0")
   125     case True
   126     with Suc show ?thesis
   127       by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq)
   128   next
   129     case False
   130     with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n]
   131     obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow>
   132                norm (\<Sum>i\<le>n. c i * z^i) \<le> norm (c (Suc n)) / 2 * norm z ^ Suc n"
   133       by auto
   134     show ?thesis
   135     unfolding eventually_at_infinity
   136     proof (rule exI [where x="max M (max 1 ((\<bar>B\<bar> + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
   137       fix z::'a
   138       assume les: "M \<le> norm z"  "1 \<le> norm z"  "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z"
   139       then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))"
   140         by (metis False pos_divide_le_eq zero_less_norm_iff)
   141       then have "\<bar>B\<bar> * 2 + 2 \<le> norm z ^ (Suc n) * norm (c (Suc n))"
   142         by (metis \<open>1 \<le> norm z\<close> order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc)
   143       then show "B \<le> norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les
   144         apply auto
   145         apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"])
   146         apply (simp_all add: norm_mult norm_power)
   147         done
   148     qed
   149   qed
   150 qed
   151 
   152 lemma polyfun_rootbound:
   153  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   154  assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
   155    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"
   156 using assms
   157 proof (induction n arbitrary: c)
   158  case (Suc n) show ?case
   159  proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}")
   160    case False
   161    then obtain a where a: "(\<Sum>i\<le>Suc n. c i * a^i) = 0"
   162      by auto
   163    from polyfun_linear_factor_root [OF this]
   164    obtain b where "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i< Suc n. b i * z^i)"
   165      by auto
   166    then have b: "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i\<le>n. b i * z^i)"
   167      by (metis lessThan_Suc_atMost)
   168    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}"
   169      by auto
   170    have c0: "c 0 = - (a * b 0)" using  b [of 0]
   171      by simp
   172    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"
   173      by (metis Suc.prems le0 minus_zero mult_zero_right)
   174    have "\<exists>k\<le>n. b k \<noteq> 0"
   175      apply (rule ccontr)
   176      using polyfun_extremal [OF extr_prem, of 1]
   177      apply (auto simp: eventually_at_infinity b simp del: sum_atMost_Suc)
   178      apply (drule_tac x="of_real ba" in spec, simp)
   179      done
   180    then show ?thesis using Suc.IH [of b] ins_ab
   181      by (auto simp: card_insert_if)
   182    qed simp
   183 qed simp
   184 
   185 corollary
   186   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   187   assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
   188     shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
   189       and polyfun_rootbound_card:   "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
   190 using polyfun_rootbound [OF assms] by auto
   191 
   192 lemma polyfun_finite_roots:
   193   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   194     shows  "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)"
   195 proof (cases " \<exists>k\<le>n. c k \<noteq> 0")
   196   case True then show ?thesis
   197     by (blast intro: polyfun_rootbound_finite)
   198 next
   199   case False then show ?thesis
   200     by (auto simp: infinite_UNIV_char_0)
   201 qed
   202 
   203 lemma polyfun_eq_0:
   204   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   205     shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
   206 proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
   207   case True
   208   then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
   209     by (simp add: infinite_UNIV_char_0)
   210   with True show ?thesis
   211     by (metis (poly_guards_query) polyfun_rootbound_finite)
   212 next
   213   case False
   214   then show ?thesis
   215     by auto
   216 qed
   217 
   218 lemma polyfun_eq_const:
   219   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   220     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)"
   221 proof -
   222   {fix z
   223     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"
   224       by (induct n) auto
   225   } then
   226   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)"
   227     by auto
   228   also have "... \<longleftrightarrow>  c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)"
   229     by (auto simp: polyfun_eq_0)
   230   finally show ?thesis .
   231 qed
   232 
   233 end
   234