# 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 \ 'a::real_normed_vector) \ 'a \ nat set \ bool" - (infixl "sums'_seq" 12) - where "(f sums_seq l) s \ ((\n. setsum f (s \ {0..n})) ---> l) sequentially" - lemma has_derivative_series: fixes f :: "nat \ 'm::euclidean_space \ 'n::euclidean_space" assumes "convex s" - and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" - and "\e>0. \N. \n\N. \x\s. \h. norm (setsum (\i. f' i x h) (k \ {0..n}) - g' x h) \ e * norm h" + and "\n x. x \ s \ ((f n) has_derivative (f' n x)) (at x within s)" + and "\e>0. \N. \n\N. \x\s. \h. norm (setsum (\i. f' i x h) {0.. e * norm h" and "x \ s" - and "((\n. f n x) sums_seq l) k" - shows "\g. \x\s. ((\n. f n x) sums_seq (g x)) k \ (g has_derivative g' x) (at x within s)" - unfolding sums_seq_def + and "(\n. f n x) sums l" + shows "\g. \x\s. (\n. f n x) sums (g x) \ (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