Theory HOL-Analysis.Poly_Roots

(*  Author: John Harrison and Valentina Bruno
    Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
*)

section ‹Polynomial Functions: Extremal Behaviour and Root Counts›

theory Poly_Roots
imports Complex_Main
begin

subsection‹Basics about polynomial functions: extremal behaviour and root counts›

lemma sub_polyfun:
  fixes x :: "'a::{comm_ring,monoid_mult}"
  shows   "(in. a i * x^i) - (in. a i * y^i) =
           (x - y) * (j<n. k= Suc j..n. a k * y^(k - Suc j) * x^j)"
proof -
  have "(in. a i * x^i) - (in. a i * y^i) =
        (in. a i * (x^i - y^i))"
    by (simp add: algebra_simps sum_subtractf [symmetric])
  also have "... = (in. a i * (x - y) * (j<i. y^(i - Suc j) * x^j))"
    by (simp add: power_diff_sumr2 ac_simps)
  also have "... = (x - y) * (in. (j<i. a i * y^(i - Suc j) * x^j))"
    by (simp add: sum_distrib_left ac_simps)
  also have "... = (x - y) * (j<n. (i=Suc j..n. a i * y^(i - Suc j) * x^j))"
    by (simp add: sum.nested_swap')
  finally show ?thesis .
qed

lemma sub_polyfun_alt:
  fixes x :: "'a::{comm_ring,monoid_mult}"
  shows   "(in. a i * x^i) - (in. a i * y^i) =
           (x - y) * (j<n. k<n-j. a (j+k+1) * y^k * x^j)"
proof -
  { fix j
    have "(k = Suc j..n. a k * y^(k - Suc j) * x^j) =
          (k <n - j. a (Suc (j + k)) * y^k * x^j)"
      by (rule sum.reindex_bij_witness[where i="λi. i + Suc j" and j="λi. i - Suc j"]) auto }
  then show ?thesis
    by (simp add: sub_polyfun)
qed

lemma polyfun_linear_factor:
  fixes a :: "'a::{comm_ring,monoid_mult}"
  shows  "b. z. (in. c i * z^i) =
                  (z-a) * (i<n. b i * z^i) + (in. c i * a^i)"
proof -
  { fix z
    have "(in. c i * z^i) - (in. c i * a^i) =
          (z - a) * (j<n. (k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
      by (simp add: sub_polyfun sum_distrib_right)
    then have "(in. c i * z^i) =
          (z - a) * (j<n. (k = Suc j..n. c k * a^(k - Suc j)) * z^j)
          + (in. c i * a^i)"
      by (simp add: algebra_simps) }
  then show ?thesis
    by (intro exI allI)
qed

lemma polyfun_linear_factor_root:
  fixes a :: "'a::{comm_ring,monoid_mult}"
  assumes "(in. c i * a^i) = 0"
  shows  "b. z. (in. c i * z^i) = (z-a) * (i<n. b i * z^i)"
  using polyfun_linear_factor [of c n a] assms
  by simp

lemma adhoc_norm_triangle: "a + norm(y)  b ==> norm(x)  a ==> norm(x + y)  b"
  by (metis norm_triangle_mono order.trans order_refl)

proposition polyfun_extremal_lemma:
  fixes c :: "nat  'a::real_normed_div_algebra"
  assumes "e > 0"
    shows "M. z. M  norm z  norm(in. c i * z^i)  e * norm(z) ^ Suc n"
proof (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 obtain M where M: "z. M  norm z  norm (in. c i * z^i)  e * norm z ^ Suc n" ..
  show ?case
  proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify)
    fix z::'a
    assume "max 1 (max M ((e + norm (c (Suc n))) / e))  norm z"
    then have norm1: "0 < norm z" "M  norm z" "(e + norm (c (Suc n))) / e  norm z"
      by auto
    then have norm2: "(e + norm (c (Suc n)))  e * norm z"  "(norm z * norm z ^ n) > 0"
      apply (metis assms less_divide_eq mult.commute not_le)
      using norm1 apply (metis mult_pos_pos zero_less_power)
      done
    have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) =
          (e + norm (c (Suc n))) * (norm z * norm z ^ n)"
      by (simp add: norm_mult norm_power algebra_simps)
    also have "...  (e * norm z) * (norm z * norm z ^ n)"
      using norm2
      using assms mult_mono by fastforce
    also have "... = e * (norm z * (norm z * norm z ^ n))"
      by (simp add: algebra_simps)
    finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n))
                   e * (norm z * (norm z * norm z ^ n))" .
    then show "norm (iSuc n. c i * z^i)  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 "¦b¦ + 1  norm(y) - a" "norm(x)  a" shows "b  norm(x + y)"
proof -
  have "b  norm y - norm x"
    using assms by linarith
  then show ?thesis
    by (metis (no_types) add.commute norm_diff_ineq order_trans)
qed

proposition polyfun_extremal:
  fixes c :: "nat  'a::real_normed_div_algebra"
  assumes "k. k  0  k  n  c k  0"
    shows "eventually (λz. norm(in. c i * z^i)  B) at_infinity"
using assms
proof (induction n)
  case 0 then show ?case
    by simp
next
  case (Suc n)
  show ?case
  proof (cases "c (Suc n) = 0")
    case True
    with Suc show ?thesis
      by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq)
  next
    case False
    with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n]
    obtain M where M: "z. M  norm z 
               norm (in. c i * z^i)  norm (c (Suc n)) / 2 * norm z ^ Suc n"
      by auto
    show ?thesis
    unfolding eventually_at_infinity
    proof (rule exI [where x="max M (max 1 ((¦B¦ + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
      fix z::'a
      assume les: "M  norm z"  "1  norm z"  "(¦B¦ * 2 + 2) / norm (c (Suc n))  norm z"
      then have "¦B¦ * 2 + 2  norm z * norm (c (Suc n))"
        by (metis False pos_divide_le_eq zero_less_norm_iff)
      then have "¦B¦ * 2 + 2  norm z ^ (Suc n) * norm (c (Suc n))"
        by (metis 1  norm z order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc)
      then show "B  norm ((in. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les
        apply auto
        apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"])
        apply (simp_all add: norm_mult norm_power)
        done
    qed
  qed
qed

proposition polyfun_rootbound:
 fixes c :: "nat  'a::{comm_ring,real_normed_div_algebra}"
 assumes "k. k  n  c k  0"
   shows "finite {z. (in. c i * z^i) = 0}  card {z. (in. c i * z^i) = 0}  n"
using assms
proof (induction n arbitrary: c)
 case (Suc n) show ?case
 proof (cases "{z. (iSuc n. c i * z^i) = 0} = {}")
   case False
   then obtain a where a: "(iSuc n. c i * a^i) = 0"
     by auto
   from polyfun_linear_factor_root [OF this]
   obtain b where "z. (iSuc n. c i * z^i) = (z - a) * (i< Suc n. b i * z^i)"
     by auto
   then have b: "z. (iSuc n. c i * z^i) = (z - a) * (in. b i * z^i)"
     by (metis lessThan_Suc_atMost)
   then have ins_ab: "{z. (iSuc n. c i * z^i) = 0} = insert a {z. (in. b i * z^i) = 0}"
     by auto
   have c0: "c 0 = - (a * b 0)" using  b [of 0]
     by simp
   then have extr_prem: "¬ (kn. b k  0)  k. k  0  k  Suc n  c k  0"
     by (metis Suc.prems le0 minus_zero mult_zero_right)
   have "kn. b k  0"
     apply (rule ccontr)
     using polyfun_extremal [OF extr_prem, of 1]
     apply (auto simp: eventually_at_infinity b simp del: sum.atMost_Suc)
     apply (drule_tac x="of_real ba" in spec, simp)
     done
   then show ?thesis using Suc.IH [of b] ins_ab
     by (auto simp: card_insert_if)
   qed simp
qed simp

corollary
  fixes c :: "nat  'a::{comm_ring,real_normed_div_algebra}"
  assumes "k. k  n  c k  0"
    shows polyfun_rootbound_finite: "finite {z. (in. c i * z^i) = 0}"
      and polyfun_rootbound_card:   "card {z. (in. c i * z^i) = 0}  n"
using polyfun_rootbound [OF assms] by auto

proposition polyfun_finite_roots:
  fixes c :: "nat  'a::{comm_ring,real_normed_div_algebra}"
    shows  "finite {z. (in. c i * z^i) = 0}  (k. k  n  c k  0)"
proof (cases " kn. c k  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:
  fixes c :: "nat  'a::{comm_ring,real_normed_div_algebra}"
    shows  "(z. (in. c i * z^i) = 0)  (k. k  n  c k = 0)"
proof (cases "(z. (in. c i * z^i) = 0)")
  case True
  then have "¬ finite {z. (in. c i * z^i) = 0}"
    by (simp add: infinite_UNIV_char_0)
  with True show ?thesis
    by (metis (poly_guards_query) polyfun_rootbound_finite)
next
  case False
  then show ?thesis
    by auto
qed

theorem polyfun_eq_const:
  fixes c :: "nat  'a::{comm_ring,real_normed_div_algebra}"
    shows  "(z. (in. c i * z^i) = k)  c 0 = k  (k. k  0  k  n  c k = 0)"
proof -
  {fix z
    have "(in. c i * z^i) = (in. (if i = 0 then c 0 - k else c i) * z^i) + k"
      by (induct n) auto
  } then
  have "(z. (in. c i * z^i) = k)  (z. (in. (if i = 0 then c 0 - k else c i) * z^i) = 0)"
    by auto
  also have "...   c 0 = k  (k. k  0  k  n  c k = 0)"
    by (auto simp: polyfun_eq_0)
  finally show ?thesis .
qed

end