src/HOL/Analysis/Poly_Roots.thy
changeset 65578 e4997c181cce
parent 64267 b9a1486e79be
child 67968 a5ad4c015d1c
     1.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -8,73 +8,6 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -subsection\<open>Geometric progressions\<close>
     1.8 -
     1.9 -lemma sum_gp_basic:
    1.10 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.11 -  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
    1.12 -  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
    1.13 -
    1.14 -lemma sum_gp0:
    1.15 -  fixes x :: "'a::{comm_ring,division_ring}"
    1.16 -  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
    1.17 -  using sum_gp_basic[of x n]
    1.18 -  by (simp add: mult.commute divide_simps)
    1.19 -
    1.20 -lemma sum_power_add:
    1.21 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.22 -  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
    1.23 -  by (simp add: sum_distrib_left power_add)
    1.24 -
    1.25 -lemma sum_power_shift:
    1.26 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.27 -  assumes "m \<le> n"
    1.28 -  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
    1.29 -proof -
    1.30 -  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
    1.31 -    by (simp add: sum_distrib_left power_add [symmetric])
    1.32 -  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
    1.33 -    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
    1.34 -  finally show ?thesis .
    1.35 -qed
    1.36 -
    1.37 -lemma sum_gp_multiplied:
    1.38 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.39 -  assumes "m \<le> n"
    1.40 -  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
    1.41 -proof -
    1.42 -  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
    1.43 -    by (metis mult.assoc mult.commute assms sum_power_shift)
    1.44 -  also have "... =x^m * (1 - x^Suc(n-m))"
    1.45 -    by (metis mult.assoc sum_gp_basic)
    1.46 -  also have "... = x^m - x^Suc n"
    1.47 -    using assms
    1.48 -    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
    1.49 -  finally show ?thesis .
    1.50 -qed
    1.51 -
    1.52 -lemma sum_gp:
    1.53 -  fixes x :: "'a::{comm_ring,division_ring}"
    1.54 -  shows   "(\<Sum>i=m..n. x^i) =
    1.55 -               (if n < m then 0
    1.56 -                else if x = 1 then of_nat((n + 1) - m)
    1.57 -                else (x^m - x^Suc n) / (1 - x))"
    1.58 -using sum_gp_multiplied [of m n x]
    1.59 -apply auto
    1.60 -by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
    1.61 -
    1.62 -lemma sum_gp_offset:
    1.63 -  fixes x :: "'a::{comm_ring,division_ring}"
    1.64 -  shows   "(\<Sum>i=m..m+n. x^i) =
    1.65 -       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
    1.66 -  using sum_gp [of x m "m+n"]
    1.67 -  by (auto simp: power_add algebra_simps)
    1.68 -
    1.69 -lemma sum_gp_strict:
    1.70 -  fixes x :: "'a::{comm_ring,division_ring}"
    1.71 -  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
    1.72 -  by (induct n) (auto simp: algebra_simps divide_simps)
    1.73 -
    1.74  subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
    1.75  
    1.76  lemma sub_polyfun: