--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Oct 29 15:40:52 2015 +0100
@@ -6019,12 +6019,6 @@
subsection \<open>Taylor series expansion\<close>
-lemma
- setsum_telescope:
- fixes f::"nat \<Rightarrow> 'a::ab_group_add"
- shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"
- by (induct i) simp_all
-
lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative:
assumes "p>0"
and f0: "Df 0 = f"