author hoelzl Mon, 17 Mar 2014 20:38:50 +0100 changeset 56183 f998bdd40763 parent 56182 528fae0816ea child 56187 2666cd7d380c
remove sums_seq, it is not used
```--- 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
```