src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 68239 0764ee22a4d1
parent 68055 2cab37094fc4
child 68255 009f783d1bac
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 19 20:42:34 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun May 20 18:37:34 2018 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  lemma has_derivative_mult_right:
     1.5    fixes c:: "'a :: real_normed_algebra"
     1.6    shows "((( * ) c) has_derivative (( * ) c)) F"
     1.7 -by (rule has_derivative_mult_right [OF has_derivative_id])
     1.8 +by (rule has_derivative_mult_right [OF has_derivative_ident])
     1.9  
    1.10  lemma has_derivative_of_real[derivative_intros, simp]:
    1.11    "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
    1.12 @@ -382,7 +382,7 @@
    1.13  lemma holomorphic_on_Un [holomorphic_intros]:
    1.14    assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
    1.15    shows   "f holomorphic_on (A \<union> B)"
    1.16 -  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A] 
    1.17 +  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
    1.18                               at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
    1.19  
    1.20  lemma holomorphic_on_If_Un [holomorphic_intros]:
    1.21 @@ -839,10 +839,10 @@
    1.22    show ?thesis
    1.23      unfolding has_field_derivative_def
    1.24    proof (rule has_derivative_sequence [OF cvs _ _ x])
    1.25 -  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.26 -    by (rule tf)
    1.27 -  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.28 -    by (blast intro: **)
    1.29 +    show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.30 +      by (rule tf)
    1.31 +  next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    1.32 +      unfolding eventually_sequentially by (blast intro: **)
    1.33    qed (metis has_field_derivative_def df)
    1.34  qed
    1.35  
    1.36 @@ -882,8 +882,8 @@
    1.37        by (metis df has_field_derivative_def mult_commute_abs)
    1.38    next show " ((\<lambda>n. f n x) sums l)"
    1.39      by (rule sf)
    1.40 -  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.41 -    by (blast intro: **)
    1.42 +  next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    1.43 +      unfolding eventually_sequentially by (blast intro: **)
    1.44    qed
    1.45  qed
    1.46  
    1.47 @@ -922,10 +922,8 @@
    1.48        and "x \<in> s"  "y \<in> s"
    1.49      shows "norm(f x - f y) \<le> B * norm(x - y)"
    1.50    apply (rule differentiable_bound [OF cvs])
    1.51 -  apply (rule ballI, erule df [unfolded has_field_derivative_def])
    1.52 -  apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn)
    1.53 -  apply fact
    1.54 -  apply fact
    1.55 +  apply (erule df [unfolded has_field_derivative_def])
    1.56 +  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
    1.57    done
    1.58  
    1.59  subsection\<open>Inverse function theorem for complex derivatives\<close>