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>
```