Quelle Poly_Roots.thy

Sprache: Isabelle

(*  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   "(∑i≤n. a i * x^i) - (∑i≤n. a i * y^i) =
           (x - y) * (∑j∑k= Suc j..n. a k * y^(k - Suc j) * x^j)"
proof -
  have "(∑i≤n. a i * x^i) - (∑i≤n. a i * y^i) =
        (∑i≤n. a i * (x^i - y^i))"
    by (simp add: algebra_simps sum_subtractf [symmetric])
  also have "... = (∑i≤n. a i * (x - y) * (∑j
    by (simp add: power_diff_sumr2 ac_simps)
  also have "... = (x - y) * (∑i≤n. (∑j
    by (simp add: sum_distrib_left ac_simps)
  also have "... = (x - y) * (∑j∑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   "(∑i≤n. a i * x^i) - (∑i≤n. a i * y^i) =
           (x - y) * (∑j∑k
proof -
  { fix j
    have "(∑k = Suc j..n. a k * y^(k - Suc j) * x^j) =
          (∑k
      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. (∑i≤n. c i * z^i) =
                  (z-a) * (∑i∑i≤n. c i * a^i)"
proof -
  { fix z
    have "(∑i≤n. c i * z^i) - (∑i≤n. c i * a^i) =
          (z - a) * (∑j∑k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
      by (simp add: sub_polyfun sum_distrib_right)
    then have "(∑i≤n. c i * z^i) =
          (z - a) * (∑j∑k = Suc j..n. c k * a^(k - Suc j)) * z^j)
          + (∑i≤n. 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 "(∑i≤n. c i * a^i) = 0"
  shows  "∃b. ∀z. (∑i≤n. c i * z^i) = (z-a) * (∑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(∑i≤n. 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 (∑i≤n. 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 (∑i≤Suc 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)"
  by (smt (verit) add.commute assms norm_diff_ineq)

proposition polyfun_extremal:
  fixes c :: "nat ==> 'a::real_normed_div_algebra"
  assumes "∃k. k ≠ 0 ∧ k ≤ n ∧ c k ≠ 0"
    shows "eventually (λz. norm(∑i≤n. 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 (∑i≤n. 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 ((∑i≤n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les
        apply (intro 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. (∑i≤n. c i * z^i) = 0} ∧ card {z. (∑i≤n. c i * z^i) = 0} ≤ n"
using assms
proof (induction n arbitrary: c)
case (Suc n) show ?case
proof (cases "{z. (∑i≤Suc n. c i * z^i) = 0} = {}")
   case False
   then obtain a where a: "(∑i≤Suc n. c i * a^i) = 0"
     by auto
   from polyfun_linear_factor_root [OF this]
   obtain b where "∧z. (∑i≤Suc n. c i * z^i) = (z - a) * (∑i< Suc n. b i * z^i)"
     by auto
   then have b: "∧z. (∑i≤Suc n. c i * z^i) = (z - a) * (∑i≤n. b i * z^i)"
     by (metis lessThan_Suc_atMost)
   then have ins_ab: "{z. (∑i≤Suc n. c i * z^i) = 0} = insert a {z. (∑i≤n. b i * z^i) = 0}"
     by auto
   have c0: "c 0 = - (a * b 0)" using  b [of 0]
     by simp
   then have extr_prem: "¬ (∃k≤n. b k ≠ 0) ==> ∃k. k ≠ 0 ∧ k ≤ Suc n ∧ c k ≠ 0"
     by (metis Suc.prems le0 minus_zero mult_zero_right)
   have "∃k≤n. b k ≠ 0"
     using polyfun_extremal [OF extr_prem, of 1]
     apply (simp add: eventually_at_infinity b del: sum.atMost_Suc)
     by (metis norm_of_nat real_arch_simple)
   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. (∑i≤n. c i * z^i) = 0}"
      and polyfun_rootbound_card:   "card {z. (∑i≤n. 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. (∑i≤n. c i * z^i) = 0} ⟷ (∃k. k ≤ n ∧ c k ≠ 0)"
proof (cases " ∃k≤n. 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. (∑i≤n. c i * z^i) = 0) ⟷ (∀k. k ≤ n ⟶ c k = 0)"
proof (cases "(∀z. (∑i≤n. c i * z^i) = 0)")
  case True
  then have "¬ finite {z. (∑i≤n. 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. (∑i≤n. c i * z^i) = k) ⟷ c 0 = k ∧ (∀k. k ≠ 0 ∧ k ≤ n ⟶ c k = 0)"
proof -
  have "∧z. (∑i≤n. c i * z^i) = (∑i≤n. (if i = 0 then c 0 - k else c i) * z^i) + k"
    by (induct n) auto
  then have "(∀z. (∑i≤n. c i * z^i) = k) ⟷ (∀z. (∑i≤n. (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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-04-30) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.