src/HOL/Analysis/Poly_Roots.thy

 (*  Author: John Harrison and Valentina Bruno
     Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
 *)
 
-section \<open>polynomial functions: extremal behaviour and root counts\<close>
+section%important \<open>polynomial functions: extremal behaviour and root counts\<close>
 
 theory Poly_Roots
 imports Complex_Main
 begin
 
-subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
-
-lemma sub_polyfun:
+subsection%important\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
+
+lemma%important sub_polyfun:
   fixes x :: "'a::{comm_ring,monoid_mult}"
   shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
            (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)"
-proof -
+proof%unimportant -
   have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
         (\<Sum>i\<le>n. a i * (x^i - y^i))"
     by (simp add: algebra_simps sum_subtractf [symmetric])
   also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
     by (simp add: power_diff_sumr2 ac_simps)

   also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
     by (simp add: nested_sum_swap')
   finally show ?thesis .
 qed
 
-lemma sub_polyfun_alt:
+lemma%unimportant sub_polyfun_alt:
   fixes x :: "'a::{comm_ring,monoid_mult}"
   shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
            (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
 proof -
   { fix j

       by (rule sum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
   then show ?thesis
     by (simp add: sub_polyfun)
 qed
 
-lemma polyfun_linear_factor:
+lemma%unimportant polyfun_linear_factor:
   fixes a :: "'a::{comm_ring,monoid_mult}"
   shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) =
                   (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)"
 proof -
   { fix z

       by (simp add: algebra_simps) }
   then show ?thesis
     by (intro exI allI)
 qed
 
-lemma polyfun_linear_factor_root:
+lemma%important polyfun_linear_factor_root:
   fixes a :: "'a::{comm_ring,monoid_mult}"
   assumes "(\<Sum>i\<le>n. c i * a^i) = 0"
   shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)"
-  using polyfun_linear_factor [of c n a] assms
-  by simp
-
-lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
+  using%unimportant polyfun_linear_factor [of c n a] assms
+  by%unimportant simp
+
+lemma%unimportant adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
   by (metis norm_triangle_mono order.trans order_refl)
 
-lemma polyfun_extremal_lemma:
+lemma%important polyfun_extremal_lemma:
   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   assumes "e > 0"
     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"
-proof (induction n)
+proof%unimportant (induction n)
   case 0
   show ?case
     by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms)
 next
   case (Suc n)

     then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1
       by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle)
     qed
 qed
 
-lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
+lemma%unimportant norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
 proof -
   have "b \<le> norm y - norm x"
     using assms by linarith
   then show ?thesis
     by (metis (no_types) add.commute norm_diff_ineq order_trans)
 qed
 
-lemma polyfun_extremal:
+lemma%important polyfun_extremal:
   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0"
     shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity"
 using assms
-proof (induction n)
+proof%unimportant (induction n)
   case 0 then show ?case
     by simp
 next
   case (Suc n)
   show ?case

         done
     qed
   qed
 qed
 
-lemma polyfun_rootbound:
+lemma%important polyfun_rootbound:
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
  assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
    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"
 using assms
-proof (induction n arbitrary: c)
+proof%unimportant (induction n arbitrary: c)
  case (Suc n) show ?case
  proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}")
    case False
    then obtain a where a: "(\<Sum>i\<le>Suc n. c i * a^i) = 0"
      by auto

    then show ?thesis using Suc.IH [of b] ins_ab
      by (auto simp: card_insert_if)
    qed simp
 qed simp
 
-corollary
+corollary%important (*FIX ME needs name *)
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
     shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
       and polyfun_rootbound_card:   "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
 using polyfun_rootbound [OF assms] by auto
 
-lemma polyfun_finite_roots:
+lemma%important polyfun_finite_roots:
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
     shows  "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)"
-proof (cases " \<exists>k\<le>n. c k \<noteq> 0")
+proof%unimportant (cases " \<exists>k\<le>n. c k \<noteq> 0")
   case True then show ?thesis
     by (blast intro: polyfun_rootbound_finite)
 next
   case False then show ?thesis
     by (auto simp: infinite_UNIV_char_0)
 qed
 
-lemma polyfun_eq_0:
+lemma%unimportant polyfun_eq_0:
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
     shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
 proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
   case True
   then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"

   case False
   then show ?thesis
     by auto
 qed
 
-lemma polyfun_eq_const:
+lemma%important polyfun_eq_const:
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
     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)"
-proof -
+proof%unimportant -
   {fix z
     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"
       by (induct n) auto
   } then
   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)"