src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 68055 2cab37094fc4
parent 67979 53323937ee25
child 68239 0764ee22a4d1
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 28 21:37:45 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Apr 29 14:46:11 2018 +0100
     1.3 @@ -837,15 +837,13 @@
     1.4      qed
     1.5    } note ** = this
     1.6    show ?thesis
     1.7 -  unfolding has_field_derivative_def
     1.8 +    unfolding has_field_derivative_def
     1.9    proof (rule has_derivative_sequence [OF cvs _ _ x])
    1.10 -    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (( * ) (f' n x))) (at x within s)"
    1.11 -      by (metis has_field_derivative_def df)
    1.12 -  next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.13 +  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.14      by (rule tf)
    1.15 -  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    1.16 +  next show "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    1.17      by (blast intro: **)
    1.18 -  qed
    1.19 +  qed (metis has_field_derivative_def df)
    1.20  qed
    1.21  
    1.22  lemma has_complex_derivative_series:
    1.23 @@ -884,7 +882,7 @@
    1.24        by (metis df has_field_derivative_def mult_commute_abs)
    1.25    next show " ((\<lambda>n. f n x) sums l)"
    1.26      by (rule sf)
    1.27 -  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    1.28 +  next show "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    1.29      by (blast intro: **)
    1.30    qed
    1.31  qed
    1.32 @@ -896,7 +894,7 @@
    1.33    assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    1.34    assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    1.35    assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
    1.36 -  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
    1.37 +  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
    1.38  proof -
    1.39    from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
    1.40      unfolding uniformly_convergent_on_def by blast
    1.41 @@ -905,7 +903,6 @@
    1.42      by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
    1.43    then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
    1.44      "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
    1.45 -  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
    1.46    from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
    1.47      by (simp add: has_field_derivative_def s)
    1.48    have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
    1.49 @@ -915,15 +912,6 @@
    1.50      by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
    1.51  qed
    1.52  
    1.53 -lemma field_differentiable_series':
    1.54 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
    1.55 -  assumes "convex s" "open s"
    1.56 -  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    1.57 -  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    1.58 -  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
    1.59 -  shows   "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x0)"
    1.60 -  using field_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
    1.61 -
    1.62  subsection\<open>Bound theorem\<close>
    1.63  
    1.64  lemma field_differentiable_bound: