src/HOL/Analysis/Poly_Roots.thy
changeset 63627 6ddb43c6b711
parent 63594 bd218a9320b5
child 63918 6bf55e6e0b75
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,301 @@
     1.4 +(*  Author: John Harrison and Valentina Bruno
     1.5 +    Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
     1.6 +*)
     1.7 +
     1.8 +section \<open>polynomial functions: extremal behaviour and root counts\<close>
     1.9 +
    1.10 +theory Poly_Roots
    1.11 +imports Complex_Main
    1.12 +begin
    1.13 +
    1.14 +subsection\<open>Geometric progressions\<close>
    1.15 +
    1.16 +lemma setsum_gp_basic:
    1.17 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.18 +  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
    1.19 +  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
    1.20 +
    1.21 +lemma setsum_gp0:
    1.22 +  fixes x :: "'a::{comm_ring,division_ring}"
    1.23 +  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
    1.24 +  using setsum_gp_basic[of x n]
    1.25 +  by (simp add: mult.commute divide_simps)
    1.26 +
    1.27 +lemma setsum_power_add:
    1.28 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.29 +  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
    1.30 +  by (simp add: setsum_right_distrib power_add)
    1.31 +
    1.32 +lemma setsum_power_shift:
    1.33 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.34 +  assumes "m \<le> n"
    1.35 +  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
    1.36 +proof -
    1.37 +  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
    1.38 +    by (simp add: setsum_right_distrib power_add [symmetric])
    1.39 +  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
    1.40 +    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
    1.41 +  finally show ?thesis .
    1.42 +qed
    1.43 +
    1.44 +lemma setsum_gp_multiplied:
    1.45 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.46 +  assumes "m \<le> n"
    1.47 +  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
    1.48 +proof -
    1.49 +  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
    1.50 +    by (metis mult.assoc mult.commute assms setsum_power_shift)
    1.51 +  also have "... =x^m * (1 - x^Suc(n-m))"
    1.52 +    by (metis mult.assoc setsum_gp_basic)
    1.53 +  also have "... = x^m - x^Suc n"
    1.54 +    using assms
    1.55 +    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
    1.56 +  finally show ?thesis .
    1.57 +qed
    1.58 +
    1.59 +lemma setsum_gp:
    1.60 +  fixes x :: "'a::{comm_ring,division_ring}"
    1.61 +  shows   "(\<Sum>i=m..n. x^i) =
    1.62 +               (if n < m then 0
    1.63 +                else if x = 1 then of_nat((n + 1) - m)
    1.64 +                else (x^m - x^Suc n) / (1 - x))"
    1.65 +using setsum_gp_multiplied [of m n x]
    1.66 +apply auto
    1.67 +by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
    1.68 +
    1.69 +lemma setsum_gp_offset:
    1.70 +  fixes x :: "'a::{comm_ring,division_ring}"
    1.71 +  shows   "(\<Sum>i=m..m+n. x^i) =
    1.72 +       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
    1.73 +  using setsum_gp [of x m "m+n"]
    1.74 +  by (auto simp: power_add algebra_simps)
    1.75 +
    1.76 +lemma setsum_gp_strict:
    1.77 +  fixes x :: "'a::{comm_ring,division_ring}"
    1.78 +  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
    1.79 +  by (induct n) (auto simp: algebra_simps divide_simps)
    1.80 +
    1.81 +subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
    1.82 +
    1.83 +lemma sub_polyfun:
    1.84 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.85 +  shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
    1.86 +           (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)"
    1.87 +proof -
    1.88 +  have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
    1.89 +        (\<Sum>i\<le>n. a i * (x^i - y^i))"
    1.90 +    by (simp add: algebra_simps setsum_subtractf [symmetric])
    1.91 +  also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
    1.92 +    by (simp add: power_diff_sumr2 ac_simps)
    1.93 +  also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
    1.94 +    by (simp add: setsum_right_distrib ac_simps)
    1.95 +  also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
    1.96 +    by (simp add: nested_setsum_swap')
    1.97 +  finally show ?thesis .
    1.98 +qed
    1.99 +
   1.100 +lemma sub_polyfun_alt:
   1.101 +  fixes x :: "'a::{comm_ring,monoid_mult}"
   1.102 +  shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
   1.103 +           (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
   1.104 +proof -
   1.105 +  { fix j
   1.106 +    have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) =
   1.107 +          (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)"
   1.108 +      by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
   1.109 +  then show ?thesis
   1.110 +    by (simp add: sub_polyfun)
   1.111 +qed
   1.112 +
   1.113 +lemma polyfun_linear_factor:
   1.114 +  fixes a :: "'a::{comm_ring,monoid_mult}"
   1.115 +  shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) =
   1.116 +                  (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)"
   1.117 +proof -
   1.118 +  { fix z
   1.119 +    have "(\<Sum>i\<le>n. c i * z^i) - (\<Sum>i\<le>n. c i * a^i) =
   1.120 +          (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
   1.121 +      by (simp add: sub_polyfun setsum_left_distrib)
   1.122 +    then have "(\<Sum>i\<le>n. c i * z^i) =
   1.123 +          (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)
   1.124 +          + (\<Sum>i\<le>n. c i * a^i)"
   1.125 +      by (simp add: algebra_simps) }
   1.126 +  then show ?thesis
   1.127 +    by (intro exI allI)
   1.128 +qed
   1.129 +
   1.130 +lemma polyfun_linear_factor_root:
   1.131 +  fixes a :: "'a::{comm_ring,monoid_mult}"
   1.132 +  assumes "(\<Sum>i\<le>n. c i * a^i) = 0"
   1.133 +  shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)"
   1.134 +  using polyfun_linear_factor [of c n a] assms
   1.135 +  by simp
   1.136 +
   1.137 +lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
   1.138 +  by (metis norm_triangle_mono order.trans order_refl)
   1.139 +
   1.140 +lemma polyfun_extremal_lemma:
   1.141 +  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   1.142 +  assumes "e > 0"
   1.143 +    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"
   1.144 +proof (induction n)
   1.145 +  case 0
   1.146 +  show ?case
   1.147 +    by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms)
   1.148 +next
   1.149 +  case (Suc n)
   1.150 +  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" ..
   1.151 +  show ?case
   1.152 +  proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify)
   1.153 +    fix z::'a
   1.154 +    assume "max 1 (max M ((e + norm (c (Suc n))) / e)) \<le> norm z"
   1.155 +    then have norm1: "0 < norm z" "M \<le> norm z" "(e + norm (c (Suc n))) / e \<le> norm z"
   1.156 +      by auto
   1.157 +    then have norm2: "(e + norm (c (Suc n))) \<le> e * norm z"  "(norm z * norm z ^ n) > 0"
   1.158 +      apply (metis assms less_divide_eq mult.commute not_le)
   1.159 +      using norm1 apply (metis mult_pos_pos zero_less_power)
   1.160 +      done
   1.161 +    have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) =
   1.162 +          (e + norm (c (Suc n))) * (norm z * norm z ^ n)"
   1.163 +      by (simp add: norm_mult norm_power algebra_simps)
   1.164 +    also have "... \<le> (e * norm z) * (norm z * norm z ^ n)"
   1.165 +      using norm2 by (metis real_mult_le_cancel_iff1)
   1.166 +    also have "... = e * (norm z * (norm z * norm z ^ n))"
   1.167 +      by (simp add: algebra_simps)
   1.168 +    finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n))
   1.169 +                  \<le> e * (norm z * (norm z * norm z ^ n))" .
   1.170 +    then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1
   1.171 +      by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle)
   1.172 +    qed
   1.173 +qed
   1.174 +
   1.175 +lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
   1.176 +proof -
   1.177 +  have "b \<le> norm y - norm x"
   1.178 +    using assms by linarith
   1.179 +  then show ?thesis
   1.180 +    by (metis (no_types) add.commute norm_diff_ineq order_trans)
   1.181 +qed
   1.182 +
   1.183 +lemma polyfun_extremal:
   1.184 +  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   1.185 +  assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0"
   1.186 +    shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity"
   1.187 +using assms
   1.188 +proof (induction n)
   1.189 +  case 0 then show ?case
   1.190 +    by simp
   1.191 +next
   1.192 +  case (Suc n)
   1.193 +  show ?case
   1.194 +  proof (cases "c (Suc n) = 0")
   1.195 +    case True
   1.196 +    with Suc show ?thesis
   1.197 +      by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq)
   1.198 +  next
   1.199 +    case False
   1.200 +    with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n]
   1.201 +    obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow>
   1.202 +               norm (\<Sum>i\<le>n. c i * z^i) \<le> norm (c (Suc n)) / 2 * norm z ^ Suc n"
   1.203 +      by auto
   1.204 +    show ?thesis
   1.205 +    unfolding eventually_at_infinity
   1.206 +    proof (rule exI [where x="max M (max 1 ((\<bar>B\<bar> + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
   1.207 +      fix z::'a
   1.208 +      assume les: "M \<le> norm z"  "1 \<le> norm z"  "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z"
   1.209 +      then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))"
   1.210 +        by (metis False pos_divide_le_eq zero_less_norm_iff)
   1.211 +      then have "\<bar>B\<bar> * 2 + 2 \<le> norm z ^ (Suc n) * norm (c (Suc n))"
   1.212 +        by (metis \<open>1 \<le> norm z\<close> order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc)
   1.213 +      then show "B \<le> norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les
   1.214 +        apply auto
   1.215 +        apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"])
   1.216 +        apply (simp_all add: norm_mult norm_power)
   1.217 +        done
   1.218 +    qed
   1.219 +  qed
   1.220 +qed
   1.221 +
   1.222 +lemma polyfun_rootbound:
   1.223 + fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   1.224 + assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
   1.225 +   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"
   1.226 +using assms
   1.227 +proof (induction n arbitrary: c)
   1.228 + case (Suc n) show ?case
   1.229 + proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}")
   1.230 +   case False
   1.231 +   then obtain a where a: "(\<Sum>i\<le>Suc n. c i * a^i) = 0"
   1.232 +     by auto
   1.233 +   from polyfun_linear_factor_root [OF this]
   1.234 +   obtain b where "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i< Suc n. b i * z^i)"
   1.235 +     by auto
   1.236 +   then have b: "\<And>z. (\<Sum>i\<le>Suc n. c i * z^i) = (z - a) * (\<Sum>i\<le>n. b i * z^i)"
   1.237 +     by (metis lessThan_Suc_atMost)
   1.238 +   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}"
   1.239 +     by auto
   1.240 +   have c0: "c 0 = - (a * b 0)" using  b [of 0]
   1.241 +     by simp
   1.242 +   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"
   1.243 +     by (metis Suc.prems le0 minus_zero mult_zero_right)
   1.244 +   have "\<exists>k\<le>n. b k \<noteq> 0"
   1.245 +     apply (rule ccontr)
   1.246 +     using polyfun_extremal [OF extr_prem, of 1]
   1.247 +     apply (auto simp: eventually_at_infinity b simp del: setsum_atMost_Suc)
   1.248 +     apply (drule_tac x="of_real ba" in spec, simp)
   1.249 +     done
   1.250 +   then show ?thesis using Suc.IH [of b] ins_ab
   1.251 +     by (auto simp: card_insert_if)
   1.252 +   qed simp
   1.253 +qed simp
   1.254 +
   1.255 +corollary
   1.256 +  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   1.257 +  assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
   1.258 +    shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
   1.259 +      and polyfun_rootbound_card:   "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
   1.260 +using polyfun_rootbound [OF assms] by auto
   1.261 +
   1.262 +lemma polyfun_finite_roots:
   1.263 +  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   1.264 +    shows  "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)"
   1.265 +proof (cases " \<exists>k\<le>n. c k \<noteq> 0")
   1.266 +  case True then show ?thesis
   1.267 +    by (blast intro: polyfun_rootbound_finite)
   1.268 +next
   1.269 +  case False then show ?thesis
   1.270 +    by (auto simp: infinite_UNIV_char_0)
   1.271 +qed
   1.272 +
   1.273 +lemma polyfun_eq_0:
   1.274 +  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   1.275 +    shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
   1.276 +proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
   1.277 +  case True
   1.278 +  then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
   1.279 +    by (simp add: infinite_UNIV_char_0)
   1.280 +  with True show ?thesis
   1.281 +    by (metis (poly_guards_query) polyfun_rootbound_finite)
   1.282 +next
   1.283 +  case False
   1.284 +  then show ?thesis
   1.285 +    by auto
   1.286 +qed
   1.287 +
   1.288 +lemma polyfun_eq_const:
   1.289 +  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   1.290 +    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)"
   1.291 +proof -
   1.292 +  {fix z
   1.293 +    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"
   1.294 +      by (induct n) auto
   1.295 +  } then
   1.296 +  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)"
   1.297 +    by auto
   1.298 +  also have "... \<longleftrightarrow>  c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)"
   1.299 +    by (auto simp: polyfun_eq_0)
   1.300 +  finally show ?thesis .
   1.301 +qed
   1.302 +
   1.303 +end
   1.304 +