src/HOL/Analysis/Poly_Roots.thy
author hoelzl
Mon, 08 Aug 2016 14:13:14 +0200
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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     1
(*  Author: John Harrison and Valentina Bruno
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     2
    Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     3
*)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     4
61560
7c985fd653c5 tuned imports;
wenzelm
parents: 60420
diff changeset
     5
section \<open>polynomial functions: extremal behaviour and root counts\<close>
7c985fd653c5 tuned imports;
wenzelm
parents: 60420
diff changeset
     6
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 62626
diff changeset
     7
theory Poly_Roots
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
imports Complex_Main
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
begin
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59867
diff changeset
    11
subsection\<open>Geometric progressions\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    12
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    13
lemma setsum_gp_basic:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    14
  fixes x :: "'a::{comm_ring,monoid_mult}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    15
  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    16
  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    17
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    18
lemma setsum_gp0:
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59615
diff changeset
    19
  fixes x :: "'a::{comm_ring,division_ring}"
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    20
  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    21
  using setsum_gp_basic[of x n]
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    22
  by (simp add: mult.commute divide_simps)
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    23
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    24
lemma setsum_power_add:
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    25
  fixes x :: "'a::{comm_ring,monoid_mult}"
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    26
  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    27
  by (simp add: setsum_right_distrib power_add)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    28
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    29
lemma setsum_power_shift:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    30
  fixes x :: "'a::{comm_ring,monoid_mult}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    31
  assumes "m \<le> n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    32
  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    33
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    34
  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    35
    by (simp add: setsum_right_distrib power_add [symmetric])
57129
7edb7550663e introduce more powerful reindexing rules for big operators
hoelzl
parents: 56215
diff changeset
    36
  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59867
diff changeset
    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
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    39
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    40
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    41
lemma setsum_gp_multiplied:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    42
  fixes x :: "'a::{comm_ring,monoid_mult}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
  assumes "m \<le> n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    45
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    47
    by (metis mult.assoc mult.commute assms setsum_power_shift)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    48
  also have "... =x^m * (1 - x^Suc(n-m))"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    49
    by (metis mult.assoc setsum_gp_basic)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    50
  also have "... = x^m - x^Suc n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    51
    using assms
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    52
    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    53
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    56
lemma setsum_gp:
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59615
diff changeset
    57
  fixes x :: "'a::{comm_ring,division_ring}"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    58
  shows   "(\<Sum>i=m..n. x^i) =
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    59
               (if n < m then 0
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    60
                else if x = 1 then of_nat((n + 1) - m)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    61
                else (x^m - x^Suc n) / (1 - x))"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    62
using setsum_gp_multiplied [of m n x]
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    63
apply auto
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57129
diff changeset
    64
by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    65
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    66
lemma setsum_gp_offset:
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59615
diff changeset
    67
  fixes x :: "'a::{comm_ring,division_ring}"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    68
  shows   "(\<Sum>i=m..m+n. x^i) =
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    69
       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
  using setsum_gp [of x m "m+n"]
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
  by (auto simp: power_add algebra_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    72
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    73
lemma setsum_gp_strict:
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59615
diff changeset
    74
  fixes x :: "'a::{comm_ring,division_ring}"
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    75
  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 58877
diff changeset
    76
  by (induct n) (auto simp: algebra_simps divide_simps)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    77
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59867
diff changeset
    78
subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    79
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    80
lemma sub_polyfun:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    81
  fixes x :: "'a::{comm_ring,monoid_mult}"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    82
  shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
           (x - y) * (\<Sum>j<n. \<Sum>k= Suc j..n. a k * y^(k - Suc j) * x^j)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    84
proof -
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    85
  have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    86
        (\<Sum>i\<le>n. a i * (x^i - y^i))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    87
    by (simp add: algebra_simps setsum_subtractf [symmetric])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    88
  also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    89
    by (simp add: power_diff_sumr2 ac_simps)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    90
  also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    91
    by (simp add: setsum_right_distrib ac_simps)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
  also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
    by (simp add: nested_setsum_swap')
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    94
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
lemma sub_polyfun_alt:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
  fixes x :: "'a::{comm_ring,monoid_mult}"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
    99
  shows   "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
           (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   102
  { fix j
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   103
    have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) =
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   104
          (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)"
57129
7edb7550663e introduce more powerful reindexing rules for big operators
hoelzl
parents: 56215
diff changeset
   105
      by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   106
  then show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   107
    by (simp add: sub_polyfun)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   110
lemma polyfun_linear_factor:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   111
  fixes a :: "'a::{comm_ring,monoid_mult}"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   112
  shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) =
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   113
                  (z-a) * (\<Sum>i<n. b i * z^i) + (\<Sum>i\<le>n. c i * a^i)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   114
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
  { fix z
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   116
    have "(\<Sum>i\<le>n. c i * z^i) - (\<Sum>i\<le>n. c i * a^i) =
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
          (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
      by (simp add: sub_polyfun setsum_left_distrib)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   119
    then have "(\<Sum>i\<le>n. c i * z^i) =
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
          (z - a) * (\<Sum>j<n. (\<Sum>k = Suc j..n. c k * a^(k - Suc j)) * z^j)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
          + (\<Sum>i\<le>n. c i * a^i)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
      by (simp add: algebra_simps) }
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
  then show ?thesis
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   124
    by (intro exI allI)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   127
lemma polyfun_linear_factor_root:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   128
  fixes a :: "'a::{comm_ring,monoid_mult}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
  assumes "(\<Sum>i\<le>n. c i * a^i) = 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
  shows  "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c i * z^i) = (z-a) * (\<Sum>i<n. b i * z^i)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
  using polyfun_linear_factor [of c n a] assms
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
  by simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   133
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
lemma adhoc_norm_triangle: "a + norm(y) \<le> b ==> norm(x) \<le> a ==> norm(x + y) \<le> b"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
  by (metis norm_triangle_mono order.trans order_refl)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
lemma polyfun_extremal_lemma:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   139
  assumes "e > 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
proof (induction n)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   142
  case 0
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   143
  show ?case
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57129
diff changeset
   144
    by (rule exI [where x="norm (c 0) / e"]) (auto simp: mult.commute pos_divide_le_eq assms)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
  case (Suc n)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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" ..
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
  show ?case
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
  proof (rule exI [where x="max 1 (max M ((e + norm(c(Suc n))) / e))"], clarify)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
    fix z::'a
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
    assume "max 1 (max M ((e + norm (c (Suc n))) / e)) \<le> norm z"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
    then have norm1: "0 < norm z" "M \<le> norm z" "(e + norm (c (Suc n))) / e \<le> norm z"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
      by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
    then have norm2: "(e + norm (c (Suc n))) \<le> e * norm z"  "(norm z * norm z ^ n) > 0"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   155
      apply (metis assms less_divide_eq mult.commute not_le)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   156
      using norm1 apply (metis mult_pos_pos zero_less_power)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
      done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
    have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n)) =
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   159
          (e + norm (c (Suc n))) * (norm z * norm z ^ n)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   160
      by (simp add: norm_mult norm_power algebra_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   161
    also have "... \<le> (e * norm z) * (norm z * norm z ^ n)"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   162
      using norm2 by (metis real_mult_le_cancel_iff1)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
    also have "... = e * (norm z * (norm z * norm z ^ n))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   164
      by (simp add: algebra_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   165
    finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n))
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   166
                  \<le> e * (norm z * (norm z * norm z ^ n))" .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   167
    then show "norm (\<Sum>i\<le>Suc n. c i * z^i) \<le> e * norm z ^ Suc (Suc n)" using M norm1
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
      by (drule_tac x=z in spec) (auto simp: intro!: adhoc_norm_triangle)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
    qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
62626
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   172
lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   173
proof -
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   174
  have "b \<le> norm y - norm x"
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   175
    using assms by linarith
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   176
  then show ?thesis
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   177
    by (metis (no_types) add.commute norm_diff_ineq order_trans)
de25474ce728 Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents: 61945
diff changeset
   178
qed
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   179
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   180
lemma polyfun_extremal:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   181
  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   182
  assumes "\<exists>k. k \<noteq> 0 \<and> k \<le> n \<and> c k \<noteq> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   183
    shows "eventually (\<lambda>z. norm(\<Sum>i\<le>n. c i * z^i) \<ge> B) at_infinity"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   184
using assms
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   185
proof (induction n)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   186
  case 0 then show ?case
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   187
    by simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   188
next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
  case (Suc n)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   190
  show ?case
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   191
  proof (cases "c (Suc n) = 0")
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   192
    case True
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   193
    with Suc show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   194
      by auto (metis diff_is_0_eq diffs0_imp_equal less_Suc_eq_le not_less_eq)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   195
  next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   196
    case False
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   197
    with polyfun_extremal_lemma [of "norm(c (Suc n)) / 2" c n]
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   198
    obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   199
               norm (\<Sum>i\<le>n. c i * z^i) \<le> norm (c (Suc n)) / 2 * norm z ^ Suc n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   200
      by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   201
    show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   202
    unfolding eventually_at_infinity
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61610
diff changeset
   203
    proof (rule exI [where x="max M (max 1 ((\<bar>B\<bar> + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   204
      fix z::'a
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   205
      assume les: "M \<le> norm z"  "1 \<le> norm z"  "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   206
      then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   207
        by (metis False pos_divide_le_eq zero_less_norm_iff)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   208
      then have "\<bar>B\<bar> * 2 + 2 \<le> norm z ^ (Suc n) * norm (c (Suc n))"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59867
diff changeset
   209
        by (metis \<open>1 \<le> norm z\<close> order.trans mult_right_mono norm_ge_zero self_le_power zero_less_Suc)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   210
      then show "B \<le> norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * (z * z ^ n))" using M les
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   211
        apply auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   212
        apply (rule norm_lemma_xy [where a = "norm (c (Suc n)) * norm z ^ (Suc n) / 2"])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   213
        apply (simp_all add: norm_mult norm_power)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   214
        done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   215
    qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   216
  qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   217
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   218
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   219
lemma polyfun_rootbound:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   220
 fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   221
 assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   223
using assms
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   224
proof (induction n arbitrary: c)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   225
 case (Suc n) show ?case
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   226
 proof (cases "{z. (\<Sum>i\<le>Suc n. c i * z^i) = 0} = {}")
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   227
   case False
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   228
   then obtain a where a: "(\<Sum>i\<le>Suc n. c i * a^i) = 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   229
     by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   230
   from polyfun_linear_factor_root [OF this]
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   232
     by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   234
     by (metis lessThan_Suc_atMost)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   236
     by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   237
   have c0: "c 0 = - (a * b 0)" using  b [of 0]
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   238
     by simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   240
     by (metis Suc.prems le0 minus_zero mult_zero_right)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   241
   have "\<exists>k\<le>n. b k \<noteq> 0"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   242
     apply (rule ccontr)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   243
     using polyfun_extremal [OF extr_prem, of 1]
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   244
     apply (auto simp: eventually_at_infinity b simp del: setsum_atMost_Suc)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   245
     apply (drule_tac x="of_real ba" in spec, simp)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   246
     done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   247
   then show ?thesis using Suc.IH [of b] ins_ab
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   248
     by (auto simp: card_insert_if)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   249
   qed simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   250
qed simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   251
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   252
corollary
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   253
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   254
  assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   255
    shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   256
      and polyfun_rootbound_card:   "card {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<le> n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   257
using polyfun_rootbound [OF assms] by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   258
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   259
lemma polyfun_finite_roots:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   260
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   261
    shows  "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0} \<longleftrightarrow> (\<exists>k. k \<le> n \<and> c k \<noteq> 0)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   262
proof (cases " \<exists>k\<le>n. c k \<noteq> 0")
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   263
  case True then show ?thesis
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   264
    by (blast intro: polyfun_rootbound_finite)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   265
next
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60420
diff changeset
   266
  case False then show ?thesis
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   267
    by (auto simp: infinite_UNIV_char_0)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   268
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   269
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   270
lemma polyfun_eq_0:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   271
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   272
    shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   273
proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   274
  case True
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   275
  then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   276
    by (simp add: infinite_UNIV_char_0)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   277
  with True show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   278
    by (metis (poly_guards_query) polyfun_rootbound_finite)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   279
next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   280
  case False
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   281
  then show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   282
    by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   283
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   284
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   285
lemma polyfun_eq_const:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   286
  fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   288
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   289
  {fix z
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   291
      by (induct n) auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   292
  } then
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   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)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   294
    by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   295
  also have "... \<longleftrightarrow>  c 0 = k \<and> (\<forall>k. k \<noteq> 0 \<and> k \<le> n \<longrightarrow> c k = 0)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   296
    by (auto simp: polyfun_eq_0)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   297
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   298
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   299
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   300
end
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   301