# HG changeset patch
# User hoelzl
# Date 1395085130 -3600
# Node ID f998bdd4076382cd76c318d5d71dc58742f046b7
# Parent  528fae0816eac1a3996e98fc532491fb34e55b92
remove sums_seq, it is not used

diff -r 528fae0816ea -r f998bdd40763 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 17 19:50:59 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 17 20:38:50 2014 +0100
@@ -1983,23 +1983,19 @@
 
 subsection {* Differentiation of a series *}
 
-definition sums_seq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> nat set \<Rightarrow> bool"
-    (infixl "sums'_seq" 12)
-  where "(f sums_seq l) s \<longleftrightarrow> ((\<lambda>n. setsum f (s \<inter> {0..n})) ---> l) sequentially"
-
 lemma has_derivative_series:
   fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes "convex s"
-    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
-    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) (k \<inter> {0..n}) - g' x h) \<le> e * norm h"
+    and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)"
+    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) {0..<n} - g' x h) \<le> e * norm h"
     and "x \<in> s"
-    and "((\<lambda>n. f n x) sums_seq l) k"
-  shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g' x) (at x within s)"
-  unfolding sums_seq_def
+    and "(\<lambda>n. f n x) sums l"
+  shows "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within s)"
+  unfolding sums_def
   apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
   apply (metis assms(2) has_derivative_setsum)
   using assms(4-5)
-  unfolding sums_seq_def
+  unfolding sums_def
   apply auto
   done