1981 qed |
1981 qed |
1982 |
1982 |
1983 |
1983 |
1984 subsection {* Differentiation of a series *} |
1984 subsection {* Differentiation of a series *} |
1985 |
1985 |
1986 definition sums_seq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> nat set \<Rightarrow> bool" |
|
1987 (infixl "sums'_seq" 12) |
|
1988 where "(f sums_seq l) s \<longleftrightarrow> ((\<lambda>n. setsum f (s \<inter> {0..n})) ---> l) sequentially" |
|
1989 |
|
1990 lemma has_derivative_series: |
1986 lemma has_derivative_series: |
1991 fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
1987 fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
1992 assumes "convex s" |
1988 assumes "convex s" |
1993 and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)" |
1989 and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)" |
1994 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" |
1990 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" |
1995 and "x \<in> s" |
1991 and "x \<in> s" |
1996 and "((\<lambda>n. f n x) sums_seq l) k" |
1992 and "(\<lambda>n. f n x) sums l" |
1997 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)" |
1993 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)" |
1998 unfolding sums_seq_def |
1994 unfolding sums_def |
1999 apply (rule has_derivative_sequence[OF assms(1) _ assms(3)]) |
1995 apply (rule has_derivative_sequence[OF assms(1) _ assms(3)]) |
2000 apply (metis assms(2) has_derivative_setsum) |
1996 apply (metis assms(2) has_derivative_setsum) |
2001 using assms(4-5) |
1997 using assms(4-5) |
2002 unfolding sums_seq_def |
1998 unfolding sums_def |
2003 apply auto |
1999 apply auto |
2004 done |
2000 done |
2005 |
2001 |
2006 |
2002 |
2007 text {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *} |
2003 text {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *} |