--- a/src/HOL/Analysis/Poly_Roots.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Poly_Roots.thy Tue Apr 25 16:39:54 2017 +0100
@@ -8,73 +8,6 @@
imports Complex_Main
begin
-subsection\<open>Geometric progressions\<close>
-
-lemma sum_gp_basic:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
- by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
-
-lemma sum_gp0:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
- using sum_gp_basic[of x n]
- by (simp add: mult.commute divide_simps)
-
-lemma sum_power_add:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
- by (simp add: sum_distrib_left power_add)
-
-lemma sum_power_shift:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- assumes "m \<le> n"
- shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
-proof -
- have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
- by (simp add: sum_distrib_left power_add [symmetric])
- also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
- 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
- finally show ?thesis .
-qed
-
-lemma sum_gp_multiplied:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- assumes "m \<le> n"
- shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
-proof -
- have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
- by (metis mult.assoc mult.commute assms sum_power_shift)
- also have "... =x^m * (1 - x^Suc(n-m))"
- by (metis mult.assoc sum_gp_basic)
- also have "... = x^m - x^Suc n"
- using assms
- by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
- finally show ?thesis .
-qed
-
-lemma sum_gp:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i=m..n. x^i) =
- (if n < m then 0
- else if x = 1 then of_nat((n + 1) - m)
- else (x^m - x^Suc n) / (1 - x))"
-using sum_gp_multiplied [of m n x]
-apply auto
-by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
-
-lemma sum_gp_offset:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i=m..m+n. x^i) =
- (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
- using sum_gp [of x m "m+n"]
- by (auto simp: power_add algebra_simps)
-
-lemma sum_gp_strict:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
- by (induct n) (auto simp: algebra_simps divide_simps)
-
subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
lemma sub_polyfun: