src/HOL/Analysis/Poly_Roots.thy
 author hoelzl Mon Aug 08 14:13:14 2016 +0200 (2016-08-08) changeset 63627 6ddb43c6b711 parent 63594 src/HOL/Multivariate_Analysis/Poly_Roots.thy@bd218a9320b5 child 63918 6bf55e6e0b75 permissions -rw-r--r--
rename HOL-Multivariate_Analysis to HOL-Analysis.
```     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
```