reorder Complex_Analysis_Basics; rename DD to deriv
authorhoelzl
Wed Apr 02 18:35:02 2014 +0200 (2014-04-02)
changeset 563707c717ba55a0b
parent 56369 2704ca85be98
child 56371 fb9ae0727548
reorder Complex_Analysis_Basics; rename DD to deriv
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 18:35:01 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 18:35:02 2014 +0200
     1.3 @@ -8,36 +8,26 @@
     1.4  imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
     1.5  begin
     1.6  
     1.7 -subsection {*Complex number lemmas *}
     1.8 +subsection{*General lemmas*}
     1.9 +
    1.10 +lemma has_derivative_mult_right:
    1.11 +  fixes c:: "'a :: real_normed_algebra"
    1.12 +  shows "((op * c) has_derivative (op * c)) F"
    1.13 +by (rule has_derivative_mult_right [OF has_derivative_id])
    1.14 +
    1.15 +lemma has_derivative_of_real[has_derivative_intros, simp]: 
    1.16 +  "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
    1.17 +  using bounded_linear.has_derivative[OF bounded_linear_of_real] .
    1.18 +
    1.19 +lemma has_vector_derivative_real_complex:
    1.20 +  "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a)"
    1.21 +  using has_derivative_compose[of of_real of_real a UNIV f "op * f'"]
    1.22 +  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
    1.23  
    1.24  lemma fact_cancel:
    1.25    fixes c :: "'a::real_field"
    1.26    shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
    1.27    by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
    1.28 -
    1.29 -lemma
    1.30 -  shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
    1.31 -    and open_halfspace_Re_gt: "open {z. Re(z) > b}"
    1.32 -    and closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
    1.33 -    and closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
    1.34 -    and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
    1.35 -    and open_halfspace_Im_lt: "open {z. Im(z) < b}"
    1.36 -    and open_halfspace_Im_gt: "open {z. Im(z) > b}"
    1.37 -    and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
    1.38 -    and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
    1.39 -    and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
    1.40 -  by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
    1.41 -            isCont_Im isCont_ident isCont_const)+
    1.42 -
    1.43 -lemma closed_complex_Reals: "closed (Reals :: complex set)"
    1.44 -proof -
    1.45 -  have "(Reals :: complex set) = {z. Im z = 0}"
    1.46 -    by (auto simp: complex_is_Real_iff)
    1.47 -  then show ?thesis
    1.48 -    by (metis closed_halfspace_Im_eq)
    1.49 -qed
    1.50 -
    1.51 -
    1.52  lemma linear_times:
    1.53    fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
    1.54    by (auto simp: linearI distrib_left)
    1.55 @@ -87,7 +77,27 @@
    1.56      shows  "b \<le> Im(l)"
    1.57    by (metis assms tendsto_le [OF _ _ tendsto_const]  tendsto_Im)
    1.58  
    1.59 -subsection{*General lemmas*}
    1.60 +lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
    1.61 +  by auto
    1.62 +
    1.63 +lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
    1.64 +  by auto
    1.65 +
    1.66 +lemma has_real_derivative:
    1.67 +  fixes f :: "real \<Rightarrow> real" 
    1.68 +  assumes "(f has_derivative f') F"
    1.69 +  obtains c where "(f has_real_derivative c) F"
    1.70 +proof -
    1.71 +  obtain c where "f' = (\<lambda>x. x * c)"
    1.72 +    by (metis assms has_derivative_bounded_linear real_bounded_linear)
    1.73 +  then show ?thesis
    1.74 +    by (metis assms that has_field_derivative_def mult_commute_abs)
    1.75 +qed
    1.76 +
    1.77 +lemma has_real_derivative_iff:
    1.78 +  fixes f :: "real \<Rightarrow> real" 
    1.79 +  shows "(\<exists>c. (f has_real_derivative c) F) = (\<exists>D. (f has_derivative D) F)"
    1.80 +  by (metis has_field_derivative_def has_real_derivative)
    1.81  
    1.82  lemma continuous_mult_left:
    1.83    fixes c::"'a::real_normed_algebra" 
    1.84 @@ -128,12 +138,6 @@
    1.85  
    1.86  subsection{*DERIV stuff*}
    1.87  
    1.88 -lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
    1.89 -  by auto
    1.90 -
    1.91 -lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
    1.92 -  by auto
    1.93 -
    1.94  lemma DERIV_zero_connected_constant:
    1.95    fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
    1.96    assumes "connected s"
    1.97 @@ -146,36 +150,32 @@
    1.98  by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
    1.99  
   1.100  lemma DERIV_zero_constant:
   1.101 -  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   1.102 +  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
   1.103    shows    "\<lbrakk>convex s;
   1.104               \<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)\<rbrakk> 
   1.105               \<Longrightarrow> \<exists>c. \<forall>x \<in> s. f(x) = c"
   1.106 -  unfolding has_field_derivative_def
   1.107 -  by (auto simp: lambda_zero intro: has_derivative_zero_constant)
   1.108 +  by (auto simp: has_field_derivative_def lambda_zero intro: has_derivative_zero_constant)
   1.109  
   1.110  lemma DERIV_zero_unique:
   1.111 -  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   1.112 +  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
   1.113    assumes "convex s"
   1.114        and d0: "\<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
   1.115        and "a \<in> s"
   1.116        and "x \<in> s"
   1.117      shows "f x = f a"
   1.118 -  by (rule has_derivative_zero_unique [where f=f, OF assms(1,3) refl _ assms(4)])
   1.119 +  by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)])
   1.120       (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
   1.121  
   1.122  lemma DERIV_zero_connected_unique:
   1.123 -  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   1.124 +  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
   1.125    assumes "connected s"
   1.126        and "open s"
   1.127        and d0: "\<And>x. x\<in>s \<Longrightarrow> DERIV f x :> 0"
   1.128        and "a \<in> s"
   1.129        and "x \<in> s"
   1.130      shows "f x = f a" 
   1.131 -    apply (rule has_derivative_zero_unique_strong_connected [of s "{}" f])
   1.132 -    using assms
   1.133 -    apply auto
   1.134 -    apply (metis DERIV_continuous_on)
   1.135 -  by (metis at_within_open has_field_derivative_def lambda_zero)
   1.136 +    by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)])
   1.137 +       (metis has_field_derivative_def lambda_zero d0)
   1.138  
   1.139  lemma DERIV_transform_within:
   1.140    assumes "(f has_field_derivative f') (at a within s)"
   1.141 @@ -200,74 +200,91 @@
   1.142      shows "DERIV g a :> f'"
   1.143    by (blast intro: assms DERIV_transform_within)
   1.144  
   1.145 +subsection{*Further useful properties of complex conjugation*}
   1.146 +
   1.147 +lemma continuous_within_cnj: "continuous (at z within s) cnj"
   1.148 +by (metis bounded_linear_cnj linear_continuous_within)
   1.149 +
   1.150 +lemma continuous_on_cnj: "continuous_on s cnj"
   1.151 +by (metis bounded_linear_cnj linear_continuous_on)
   1.152 +
   1.153 +subsection {*Some limit theorems about real part of real series etc.*}
   1.154 +
   1.155 +(*MOVE? But not to Finite_Cartesian_Product*)
   1.156 +lemma sums_vec_nth :
   1.157 +  assumes "f sums a"
   1.158 +  shows "(\<lambda>x. f x $ i) sums a $ i"
   1.159 +using assms unfolding sums_def
   1.160 +by (auto dest: tendsto_vec_nth [where i=i])
   1.161 +
   1.162 +lemma summable_vec_nth :
   1.163 +  assumes "summable f"
   1.164 +  shows "summable (\<lambda>x. f x $ i)"
   1.165 +using assms unfolding summable_def
   1.166 +by (blast intro: sums_vec_nth)
   1.167 +
   1.168 +subsection {*Complex number lemmas *}
   1.169 +
   1.170 +lemma
   1.171 +  shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
   1.172 +    and open_halfspace_Re_gt: "open {z. Re(z) > b}"
   1.173 +    and closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
   1.174 +    and closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
   1.175 +    and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
   1.176 +    and open_halfspace_Im_lt: "open {z. Im(z) < b}"
   1.177 +    and open_halfspace_Im_gt: "open {z. Im(z) > b}"
   1.178 +    and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
   1.179 +    and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
   1.180 +    and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
   1.181 +  by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
   1.182 +            isCont_Im isCont_ident isCont_const)+
   1.183 +
   1.184 +lemma closed_complex_Reals: "closed (Reals :: complex set)"
   1.185 +proof -
   1.186 +  have "(Reals :: complex set) = {z. Im z = 0}"
   1.187 +    by (auto simp: complex_is_Real_iff)
   1.188 +  then show ?thesis
   1.189 +    by (metis closed_halfspace_Im_eq)
   1.190 +qed
   1.191 +
   1.192 +lemma real_lim:
   1.193 +  fixes l::complex
   1.194 +  assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   1.195 +  shows  "l \<in> \<real>"
   1.196 +proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
   1.197 +  show "eventually (\<lambda>x. f x \<in> \<real>) F"
   1.198 +    using assms(3, 4) by (auto intro: eventually_mono)
   1.199 +qed
   1.200 +
   1.201 +lemma real_lim_sequentially:
   1.202 +  fixes l::complex
   1.203 +  shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
   1.204 +by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
   1.205 +
   1.206 +lemma real_series: 
   1.207 +  fixes l::complex
   1.208 +  shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
   1.209 +unfolding sums_def
   1.210 +by (metis real_lim_sequentially setsum_in_Reals)
   1.211 +
   1.212 +lemma Lim_null_comparison_Re:
   1.213 +   "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F \<Longrightarrow>  (g ---> 0) F \<Longrightarrow> (f ---> 0) F"
   1.214 +  by (metis Lim_null_comparison complex_Re_zero tendsto_Re)
   1.215  
   1.216  subsection{*Holomorphic functions*}
   1.217  
   1.218 -lemma has_derivative_ident[has_derivative_intros, simp]: 
   1.219 -     "FDERIV complex_of_real x :> complex_of_real"
   1.220 -  by (simp add: has_derivative_def tendsto_const bounded_linear_of_real)
   1.221 -
   1.222 -lemma has_real_derivative:
   1.223 -  fixes f :: "real\<Rightarrow>real" 
   1.224 -  assumes "(f has_derivative f') F"
   1.225 -    obtains c where "(f has_derivative (\<lambda>x. x * c)) F"
   1.226 -proof -
   1.227 -  obtain c where "f' = (\<lambda>x. x * c)"
   1.228 -    by (metis assms has_derivative_bounded_linear real_bounded_linear)
   1.229 -  then show ?thesis
   1.230 -    by (metis assms that)
   1.231 -qed
   1.232 -
   1.233 -lemma has_real_derivative_iff:
   1.234 -  fixes f :: "real\<Rightarrow>real" 
   1.235 -  shows "(\<exists>f'. (f has_derivative (\<lambda>x. x * f')) F) = (\<exists>D. (f has_derivative D) F)"
   1.236 -by (auto elim: has_real_derivative)
   1.237 -
   1.238  definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
   1.239             (infixr "(complex'_differentiable)" 50)  
   1.240    where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
   1.241  
   1.242 -definition DD :: "['a \<Rightarrow> 'a::real_normed_field, 'a] \<Rightarrow> 'a" --{*for real, complex?*}
   1.243 -  where "DD f x \<equiv> THE f'. (f has_derivative (\<lambda>x. x * f')) (at x)"
   1.244 -
   1.245 -definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
   1.246 -           (infixl "(holomorphic'_on)" 50)
   1.247 -  where "f holomorphic_on s \<equiv> \<forall>x \<in> s. \<exists>f'. (f has_field_derivative f') (at x within s)"
   1.248 -  
   1.249 -lemma holomorphic_on_empty: "f holomorphic_on {}"
   1.250 -  by (simp add: holomorphic_on_def)
   1.251 -
   1.252 -lemma holomorphic_on_differentiable:
   1.253 -     "f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. f complex_differentiable (at x within s))"
   1.254 -unfolding holomorphic_on_def complex_differentiable_def has_field_derivative_def
   1.255 -by (metis mult_commute_abs)
   1.256 -
   1.257 -lemma holomorphic_on_open:
   1.258 -    "open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
   1.259 -  by (auto simp: holomorphic_on_def has_field_derivative_def at_within_open [of _ s])
   1.260 -
   1.261 -lemma complex_differentiable_imp_continuous_at: 
   1.262 -    "f complex_differentiable (at x) \<Longrightarrow> continuous (at x) f"
   1.263 +lemma complex_differentiable_imp_continuous_at:
   1.264 +    "f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
   1.265    by (metis DERIV_continuous complex_differentiable_def)
   1.266  
   1.267 -lemma holomorphic_on_imp_continuous_on: 
   1.268 -    "f holomorphic_on s \<Longrightarrow> continuous_on s f"
   1.269 -  by (metis DERIV_continuous continuous_on_eq_continuous_within holomorphic_on_def) 
   1.270 -
   1.271 -lemma has_derivative_within_open:
   1.272 -  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> (f has_field_derivative f') (at a within s) \<longleftrightarrow> DERIV f a :> f'"
   1.273 -  by (simp add: has_field_derivative_def) (metis has_derivative_within_open)
   1.274 -
   1.275 -lemma holomorphic_on_subset:
   1.276 -    "f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
   1.277 -  unfolding holomorphic_on_def
   1.278 -  by (metis DERIV_subset subsetD)
   1.279 -
   1.280  lemma complex_differentiable_within_subset:
   1.281      "\<lbrakk>f complex_differentiable (at x within s); t \<subseteq> s\<rbrakk>
   1.282       \<Longrightarrow> f complex_differentiable (at x within t)"
   1.283 -  unfolding complex_differentiable_def
   1.284 -  by (metis DERIV_subset)
   1.285 +  by (metis DERIV_subset complex_differentiable_def)
   1.286  
   1.287  lemma complex_differentiable_at_within:
   1.288      "\<lbrakk>f complex_differentiable (at x)\<rbrakk>
   1.289 @@ -275,36 +292,28 @@
   1.290    unfolding complex_differentiable_def
   1.291    by (metis DERIV_subset top_greatest)
   1.292  
   1.293 -
   1.294 -lemma has_derivative_mult_right:
   1.295 -  fixes c:: "'a :: real_normed_algebra"
   1.296 -  shows "((op * c) has_derivative (op * c)) F"
   1.297 -by (rule has_derivative_mult_right [OF has_derivative_id])
   1.298 -
   1.299 -lemma complex_differentiable_linear:
   1.300 -     "(op * c) complex_differentiable F"
   1.301 +lemma complex_differentiable_linear: "(op * c) complex_differentiable F"
   1.302  proof -
   1.303 -  have "\<And>u::complex. (\<lambda>x. x * u) = op * u"
   1.304 -    by (rule ext) (simp add: mult_ac)
   1.305 -  then show ?thesis
   1.306 -    unfolding complex_differentiable_def has_field_derivative_def
   1.307 +  show ?thesis
   1.308 +    unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
   1.309      by (force intro: has_derivative_mult_right)
   1.310  qed
   1.311  
   1.312 -lemma complex_differentiable_const:
   1.313 -  "(\<lambda>z. c) complex_differentiable F"
   1.314 +lemma complex_differentiable_const: "(\<lambda>z. c) complex_differentiable F"
   1.315    unfolding complex_differentiable_def has_field_derivative_def
   1.316    by (rule exI [where x=0])
   1.317       (metis has_derivative_const lambda_zero) 
   1.318  
   1.319 -lemma complex_differentiable_id:
   1.320 -  "(\<lambda>z. z) complex_differentiable F"
   1.321 +lemma complex_differentiable_ident: "(\<lambda>z. z) complex_differentiable F"
   1.322    unfolding complex_differentiable_def has_field_derivative_def
   1.323    by (rule exI [where x=1])
   1.324       (simp add: lambda_one [symmetric])
   1.325  
   1.326 +lemma complex_differentiable_id: "id complex_differentiable F"
   1.327 +  unfolding id_def by (rule complex_differentiable_ident)
   1.328 +
   1.329  lemma complex_differentiable_minus:
   1.330 -    "f complex_differentiable F \<Longrightarrow> (\<lambda>z. -(f z)) complex_differentiable F"
   1.331 +  "f complex_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) complex_differentiable F"
   1.332    using assms unfolding complex_differentiable_def
   1.333    by (metis field_differentiable_minus)
   1.334  
   1.335 @@ -314,6 +323,11 @@
   1.336    using assms unfolding complex_differentiable_def
   1.337    by (metis field_differentiable_add)
   1.338  
   1.339 +lemma complex_differentiable_setsum:
   1.340 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
   1.341 +  by (induct I rule: infinite_finite_induct)
   1.342 +     (auto intro: complex_differentiable_add complex_differentiable_const)
   1.343 +
   1.344  lemma complex_differentiable_diff:
   1.345    assumes "f complex_differentiable F" "g complex_differentiable F"
   1.346      shows "(\<lambda>z. f z - g z) complex_differentiable F"
   1.347 @@ -363,177 +377,17 @@
   1.348    using assms unfolding complex_differentiable_def
   1.349    by (metis DERIV_image_chain)
   1.350  
   1.351 +lemma complex_differentiable_compose:
   1.352 +  "f complex_differentiable at z \<Longrightarrow> g complex_differentiable at (f z)
   1.353 +          \<Longrightarrow> (g o f) complex_differentiable at z"
   1.354 +by (metis complex_differentiable_at_within complex_differentiable_compose_within)
   1.355 +
   1.356  lemma complex_differentiable_within_open:
   1.357       "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f complex_differentiable at a within s \<longleftrightarrow> 
   1.358                            f complex_differentiable at a"
   1.359    unfolding complex_differentiable_def
   1.360    by (metis at_within_open)
   1.361  
   1.362 -lemma holomorphic_transform:
   1.363 -     "\<lbrakk>f holomorphic_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g holomorphic_on s"
   1.364 -  apply (auto simp: holomorphic_on_def has_field_derivative_def)
   1.365 -  by (metis complex_differentiable_def complex_differentiable_transform_within has_field_derivative_def linordered_field_no_ub)
   1.366 -
   1.367 -lemma holomorphic_eq:
   1.368 -     "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on s"
   1.369 -  by (metis holomorphic_transform)
   1.370 -
   1.371 -subsection{*Holomorphic*}
   1.372 -
   1.373 -lemma holomorphic_on_linear:
   1.374 -     "(op * c) holomorphic_on s"
   1.375 -  unfolding holomorphic_on_def  by (metis DERIV_cmult_Id)
   1.376 -
   1.377 -lemma holomorphic_on_const:
   1.378 -     "(\<lambda>z. c) holomorphic_on s"
   1.379 -  unfolding holomorphic_on_def  
   1.380 -  by (metis DERIV_const)
   1.381 -
   1.382 -lemma holomorphic_on_id:
   1.383 -     "id holomorphic_on s"
   1.384 -  unfolding holomorphic_on_def id_def  
   1.385 -  by (metis DERIV_ident)
   1.386 -
   1.387 -lemma holomorphic_on_compose:
   1.388 -  "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s)
   1.389 -           \<Longrightarrow> (g o f) holomorphic_on s"
   1.390 -  unfolding holomorphic_on_def
   1.391 -  by (metis DERIV_image_chain imageI)
   1.392 -
   1.393 -lemma holomorphic_on_compose_gen:
   1.394 -  "\<lbrakk>f holomorphic_on s; g holomorphic_on t; f ` s \<subseteq> t\<rbrakk> \<Longrightarrow> (g o f) holomorphic_on s"
   1.395 -  unfolding holomorphic_on_def
   1.396 -  by (metis DERIV_image_chain DERIV_subset image_subset_iff)
   1.397 -
   1.398 -lemma holomorphic_on_minus:
   1.399 -  "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
   1.400 -  unfolding holomorphic_on_def
   1.401 -by (metis DERIV_minus)
   1.402 -
   1.403 -lemma holomorphic_on_add:
   1.404 -  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
   1.405 -  unfolding holomorphic_on_def
   1.406 -  by (metis DERIV_add)
   1.407 -
   1.408 -lemma holomorphic_on_diff:
   1.409 -  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
   1.410 -  unfolding holomorphic_on_def
   1.411 -  by (metis DERIV_diff)
   1.412 -
   1.413 -lemma holomorphic_on_mult:
   1.414 -  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
   1.415 -  unfolding holomorphic_on_def
   1.416 -  by auto (metis DERIV_mult)
   1.417 -
   1.418 -lemma holomorphic_on_inverse:
   1.419 -  "\<lbrakk>f holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on s"
   1.420 -  unfolding holomorphic_on_def
   1.421 -  by (metis DERIV_inverse')
   1.422 -
   1.423 -lemma holomorphic_on_divide:
   1.424 -  "\<lbrakk>f holomorphic_on s; g holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on s"
   1.425 -  unfolding holomorphic_on_def
   1.426 -  by (metis (full_types) DERIV_divide)
   1.427 -
   1.428 -lemma holomorphic_on_power:
   1.429 -  "f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
   1.430 -  unfolding holomorphic_on_def
   1.431 -  by (metis DERIV_power)
   1.432 -
   1.433 -lemma holomorphic_on_setsum:
   1.434 -  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
   1.435 -  unfolding holomorphic_on_def
   1.436 -  apply (induct I rule: infinite_finite_induct) 
   1.437 -  apply (force intro: DERIV_const DERIV_add)+
   1.438 -  done
   1.439 -
   1.440 -lemma DERIV_imp_DD: "DERIV f x :> f' \<Longrightarrow> DD f x = f'"
   1.441 -    apply (simp add: DD_def has_field_derivative_def mult_commute_abs)
   1.442 -    apply (rule the_equality, assumption)
   1.443 -    apply (metis DERIV_unique has_field_derivative_def)
   1.444 -    done
   1.445 -
   1.446 -lemma DD_iff_derivative_differentiable:
   1.447 -  fixes f :: "real\<Rightarrow>real" 
   1.448 -  shows   "DERIV f x :> DD f x \<longleftrightarrow> f differentiable at x"
   1.449 -unfolding DD_def differentiable_def 
   1.450 -by (metis (full_types) DD_def DERIV_imp_DD has_field_derivative_def has_real_derivative_iff 
   1.451 -          mult_commute_abs)
   1.452 -
   1.453 -lemma DD_iff_derivative_complex_differentiable:
   1.454 -  fixes f :: "complex\<Rightarrow>complex" 
   1.455 -  shows "DERIV f x :> DD f x \<longleftrightarrow> f complex_differentiable at x"
   1.456 -unfolding DD_def complex_differentiable_def
   1.457 -by (metis DD_def DERIV_imp_DD)
   1.458 -
   1.459 -lemma complex_differentiable_compose:
   1.460 -  "f complex_differentiable at z \<Longrightarrow> g complex_differentiable at (f z)
   1.461 -          \<Longrightarrow> (g o f) complex_differentiable at z"
   1.462 -by (metis complex_differentiable_at_within complex_differentiable_compose_within)
   1.463 -
   1.464 -lemma complex_derivative_chain:
   1.465 -  fixes z::complex
   1.466 -  shows
   1.467 -  "f complex_differentiable at z \<Longrightarrow> g complex_differentiable at (f z)
   1.468 -          \<Longrightarrow> DD (g o f) z = DD g (f z) * DD f z"
   1.469 -by (metis DD_iff_derivative_complex_differentiable DERIV_chain DERIV_imp_DD)
   1.470 -
   1.471 -lemma comp_derivative_chain:
   1.472 -  fixes z::real
   1.473 -  shows "\<lbrakk>f differentiable at z; g differentiable at (f z)\<rbrakk> 
   1.474 -         \<Longrightarrow> DD (g o f) z = DD g (f z) * DD f z"
   1.475 -by (metis DD_iff_derivative_differentiable DERIV_chain DERIV_imp_DD)
   1.476 -
   1.477 -lemma complex_derivative_linear: "DD (\<lambda>w. c * w) = (\<lambda>z. c)"
   1.478 -by (metis DERIV_imp_DD DERIV_cmult_Id)
   1.479 -
   1.480 -lemma complex_derivative_ident: "DD (\<lambda>w. w) = (\<lambda>z. 1)"
   1.481 -by (metis DERIV_imp_DD DERIV_ident)
   1.482 -
   1.483 -lemma complex_derivative_const: "DD (\<lambda>w. c) = (\<lambda>z. 0)"
   1.484 -by (metis DERIV_imp_DD DERIV_const)
   1.485 -
   1.486 -lemma complex_derivative_add:
   1.487 -  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
   1.488 -   \<Longrightarrow> DD (\<lambda>w. f w + g w) z = DD f z + DD g z"
   1.489 -  unfolding complex_differentiable_def
   1.490 -  by (rule DERIV_imp_DD) (metis (poly_guards_query) DERIV_add DERIV_imp_DD)  
   1.491 -
   1.492 -lemma complex_derivative_diff:
   1.493 -  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
   1.494 -   \<Longrightarrow> DD (\<lambda>w. f w - g w) z = DD f z - DD g z"
   1.495 -  unfolding complex_differentiable_def
   1.496 -  by (rule DERIV_imp_DD) (metis (poly_guards_query) DERIV_diff DERIV_imp_DD)
   1.497 -
   1.498 -lemma complex_derivative_mult:
   1.499 -  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
   1.500 -   \<Longrightarrow> DD (\<lambda>w. f w * g w) z = f z * DD g z + DD f z * g z"
   1.501 -  unfolding complex_differentiable_def
   1.502 -  by (rule DERIV_imp_DD) (metis DERIV_imp_DD DERIV_mult')
   1.503 -
   1.504 -lemma complex_derivative_cmult:
   1.505 -  "f complex_differentiable at z \<Longrightarrow> DD (\<lambda>w. c * f w) z = c * DD f z"
   1.506 -  unfolding complex_differentiable_def
   1.507 -  by (metis DERIV_cmult DERIV_imp_DD)
   1.508 -
   1.509 -lemma complex_derivative_cmult_right:
   1.510 -  "f complex_differentiable at z \<Longrightarrow> DD (\<lambda>w. f w * c) z = DD f z * c"
   1.511 -  unfolding complex_differentiable_def
   1.512 -  by (metis DERIV_cmult_right DERIV_imp_DD)
   1.513 -
   1.514 -lemma complex_derivative_transform_within_open:
   1.515 -  "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk> 
   1.516 -   \<Longrightarrow> DD f z = DD g z"
   1.517 -  unfolding holomorphic_on_def
   1.518 -  by (rule DERIV_imp_DD) (metis has_derivative_within_open DERIV_imp_DD DERIV_transform_within_open)
   1.519 -
   1.520 -lemma complex_derivative_compose_linear:
   1.521 -    "f complex_differentiable at (c * z) \<Longrightarrow> DD (\<lambda>w. f (c * w)) z = c * DD f (c * z)"
   1.522 -apply (rule DERIV_imp_DD)
   1.523 -apply (simp add: DD_iff_derivative_complex_differentiable [symmetric])
   1.524 -apply (metis DERIV_chain' DERIV_cmult_Id comm_semiring_1_class.normalizing_semiring_rules(7))  
   1.525 -done
   1.526 -
   1.527  subsection{*Caratheodory characterization.*}
   1.528  
   1.529  lemma complex_differentiable_caratheodory_at:
   1.530 @@ -548,40 +402,193 @@
   1.531    using DERIV_caratheodory_within [of f]
   1.532    by (simp add: complex_differentiable_def has_field_derivative_def)
   1.533  
   1.534 +subsection{*Holomorphic*}
   1.535 +
   1.536 +definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
   1.537 +           (infixl "(holomorphic'_on)" 50)
   1.538 +  where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f complex_differentiable (at x within s)"
   1.539 +  
   1.540 +lemma holomorphic_on_empty: "f holomorphic_on {}"
   1.541 +  by (simp add: holomorphic_on_def)
   1.542 +
   1.543 +lemma holomorphic_on_open:
   1.544 +    "open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
   1.545 +  by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s])
   1.546 +
   1.547 +lemma holomorphic_on_imp_continuous_on: 
   1.548 +    "f holomorphic_on s \<Longrightarrow> continuous_on s f"
   1.549 +  by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def) 
   1.550 +
   1.551 +lemma holomorphic_on_subset:
   1.552 +    "f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
   1.553 +  unfolding holomorphic_on_def
   1.554 +  by (metis complex_differentiable_within_subset subsetD)
   1.555 +
   1.556 +lemma holomorphic_transform: "\<lbrakk>f holomorphic_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g holomorphic_on s"
   1.557 +  by (metis complex_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
   1.558 +
   1.559 +lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
   1.560 +  by (metis holomorphic_transform)
   1.561 +
   1.562 +lemma holomorphic_on_linear: "(op * c) holomorphic_on s"
   1.563 +  unfolding holomorphic_on_def by (metis complex_differentiable_linear)
   1.564 +
   1.565 +lemma holomorphic_on_const: "(\<lambda>z. c) holomorphic_on s"
   1.566 +  unfolding holomorphic_on_def by (metis complex_differentiable_const)
   1.567 +
   1.568 +lemma holomorphic_on_ident: "(\<lambda>x. x) holomorphic_on s"
   1.569 +  unfolding holomorphic_on_def by (metis complex_differentiable_ident)
   1.570 +
   1.571 +lemma holomorphic_on_id: "id holomorphic_on s"
   1.572 +  unfolding id_def by (rule holomorphic_on_ident)
   1.573 +
   1.574 +lemma holomorphic_on_compose:
   1.575 +  "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
   1.576 +  using complex_differentiable_compose_within[of f _ s g]
   1.577 +  by (auto simp: holomorphic_on_def)
   1.578 +
   1.579 +lemma holomorphic_on_compose_gen:
   1.580 +  "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
   1.581 +  by (metis holomorphic_on_compose holomorphic_on_subset)
   1.582 +
   1.583 +lemma holomorphic_on_minus: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
   1.584 +  by (metis complex_differentiable_minus holomorphic_on_def)
   1.585 +
   1.586 +lemma holomorphic_on_add:
   1.587 +  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
   1.588 +  unfolding holomorphic_on_def by (metis complex_differentiable_add)
   1.589 +
   1.590 +lemma holomorphic_on_diff:
   1.591 +  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
   1.592 +  unfolding holomorphic_on_def by (metis complex_differentiable_diff)
   1.593 +
   1.594 +lemma holomorphic_on_mult:
   1.595 +  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
   1.596 +  unfolding holomorphic_on_def by (metis complex_differentiable_mult)
   1.597 +
   1.598 +lemma holomorphic_on_inverse:
   1.599 +  "\<lbrakk>f holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on s"
   1.600 +  unfolding holomorphic_on_def by (metis complex_differentiable_inverse)
   1.601 +
   1.602 +lemma holomorphic_on_divide:
   1.603 +  "\<lbrakk>f holomorphic_on s; g holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on s"
   1.604 +  unfolding holomorphic_on_def by (metis complex_differentiable_divide)
   1.605 +
   1.606 +lemma holomorphic_on_power:
   1.607 +  "f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
   1.608 +  unfolding holomorphic_on_def by (metis complex_differentiable_power)
   1.609 +
   1.610 +lemma holomorphic_on_setsum:
   1.611 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
   1.612 +  unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
   1.613 +
   1.614 +definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.615 +  "deriv f x \<equiv> THE D. DERIV f x :> D"
   1.616 +
   1.617 +lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
   1.618 +  unfolding deriv_def by (metis the_equality DERIV_unique)
   1.619 +
   1.620 +lemma DERIV_deriv_iff_real_differentiable:
   1.621 +  fixes x :: real
   1.622 +  shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
   1.623 +  unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
   1.624 +
   1.625 +lemma real_derivative_chain:
   1.626 +  fixes x :: real
   1.627 +  shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
   1.628 +    \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
   1.629 +  by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
   1.630 +
   1.631 +lemma DERIV_deriv_iff_complex_differentiable:
   1.632 +  "DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
   1.633 +  unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
   1.634 +
   1.635 +lemma complex_derivative_chain:
   1.636 +  "f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
   1.637 +    \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
   1.638 +  by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
   1.639 +
   1.640 +lemma complex_derivative_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
   1.641 +  by (metis DERIV_imp_deriv DERIV_cmult_Id)
   1.642 +
   1.643 +lemma complex_derivative_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
   1.644 +  by (metis DERIV_imp_deriv DERIV_ident)
   1.645 +
   1.646 +lemma complex_derivative_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
   1.647 +  by (metis DERIV_imp_deriv DERIV_const)
   1.648 +
   1.649 +lemma complex_derivative_add:
   1.650 +  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
   1.651 +   \<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
   1.652 +  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   1.653 +  by (auto intro!: DERIV_imp_deriv DERIV_intros)
   1.654 +
   1.655 +lemma complex_derivative_diff:
   1.656 +  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
   1.657 +   \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
   1.658 +  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   1.659 +  by (auto intro!: DERIV_imp_deriv DERIV_intros)
   1.660 +
   1.661 +lemma complex_derivative_mult:
   1.662 +  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
   1.663 +   \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
   1.664 +  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   1.665 +  by (auto intro!: DERIV_imp_deriv DERIV_intros)
   1.666 +
   1.667 +lemma complex_derivative_cmult:
   1.668 +  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
   1.669 +  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   1.670 +  by (auto intro!: DERIV_imp_deriv DERIV_intros)
   1.671 +
   1.672 +lemma complex_derivative_cmult_right:
   1.673 +  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
   1.674 +  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
   1.675 +  by (auto intro!: DERIV_imp_deriv DERIV_intros)
   1.676 +
   1.677 +lemma complex_derivative_transform_within_open:
   1.678 +  "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk> 
   1.679 +   \<Longrightarrow> deriv f z = deriv g z"
   1.680 +  unfolding holomorphic_on_def
   1.681 +  by (rule DERIV_imp_deriv)
   1.682 +     (metis DERIV_deriv_iff_complex_differentiable DERIV_transform_within_open at_within_open)
   1.683 +
   1.684 +lemma complex_derivative_compose_linear:
   1.685 +  "f complex_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
   1.686 +apply (rule DERIV_imp_deriv)
   1.687 +apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric])
   1.688 +apply (metis DERIV_chain' DERIV_cmult_Id comm_semiring_1_class.normalizing_semiring_rules(7))  
   1.689 +done
   1.690 +
   1.691  subsection{*analyticity on a set*}
   1.692  
   1.693  definition analytic_on (infixl "(analytic'_on)" 50)  
   1.694    where
   1.695     "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
   1.696  
   1.697 -lemma analytic_imp_holomorphic:
   1.698 -     "f analytic_on s \<Longrightarrow> f holomorphic_on s"
   1.699 -  unfolding analytic_on_def holomorphic_on_def
   1.700 -  apply (simp add: has_derivative_within_open [OF _ open_ball])
   1.701 -  apply (metis DERIV_subset dist_self mem_ball top_greatest)
   1.702 -  done
   1.703 +lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
   1.704 +  by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
   1.705 +     (metis centre_in_ball complex_differentiable_at_within)
   1.706  
   1.707 -lemma analytic_on_open:
   1.708 -     "open s \<Longrightarrow> f analytic_on s \<longleftrightarrow> f holomorphic_on s"
   1.709 +lemma analytic_on_open: "open s \<Longrightarrow> f analytic_on s \<longleftrightarrow> f holomorphic_on s"
   1.710  apply (auto simp: analytic_imp_holomorphic)
   1.711  apply (auto simp: analytic_on_def holomorphic_on_def)
   1.712  by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
   1.713  
   1.714  lemma analytic_on_imp_differentiable_at:
   1.715    "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f complex_differentiable (at x)"
   1.716 - apply (auto simp: analytic_on_def holomorphic_on_differentiable)
   1.717 + apply (auto simp: analytic_on_def holomorphic_on_def)
   1.718  by (metis Topology_Euclidean_Space.open_ball centre_in_ball complex_differentiable_within_open)
   1.719  
   1.720 -lemma analytic_on_subset:
   1.721 -     "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t"
   1.722 +lemma analytic_on_subset: "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t"
   1.723    by (auto simp: analytic_on_def)
   1.724  
   1.725 -lemma analytic_on_Un:
   1.726 -    "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
   1.727 +lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
   1.728    by (auto simp: analytic_on_def)
   1.729  
   1.730 -lemma analytic_on_Union:
   1.731 -  "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
   1.732 +lemma analytic_on_Union: "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
   1.733 +  by (auto simp: analytic_on_def)
   1.734 +
   1.735 +lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"
   1.736    by (auto simp: analytic_on_def)
   1.737    
   1.738  lemma analytic_on_holomorphic:
   1.739 @@ -608,17 +615,16 @@
   1.740  qed
   1.741  
   1.742  lemma analytic_on_linear: "(op * c) analytic_on s"
   1.743 -  apply (simp add: analytic_on_holomorphic holomorphic_on_linear)
   1.744 -  by (metis open_UNIV top_greatest)
   1.745 +  by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
   1.746  
   1.747  lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
   1.748 -  unfolding analytic_on_def
   1.749 -  by (metis holomorphic_on_const zero_less_one)
   1.750 +  by (metis analytic_on_def holomorphic_on_const zero_less_one)
   1.751 +
   1.752 +lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
   1.753 +  by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
   1.754  
   1.755  lemma analytic_on_id: "id analytic_on s"
   1.756 -  unfolding analytic_on_def
   1.757 -  apply (simp add: holomorphic_on_id)
   1.758 -  by (metis gt_ex)
   1.759 +  unfolding id_def by (rule analytic_on_ident)
   1.760  
   1.761  lemma analytic_on_compose:
   1.762    assumes f: "f analytic_on s"
   1.763 @@ -791,47 +797,38 @@
   1.764  
   1.765  lemma 
   1.766    assumes "f analytic_on {z}" "g analytic_on {z}"
   1.767 -  shows complex_derivative_add_at: "DD (\<lambda>w. f w + g w) z = DD f z + DD g z"
   1.768 -    and complex_derivative_diff_at: "DD (\<lambda>w. f w - g w) z = DD f z - DD g z"
   1.769 -    and complex_derivative_mult_at: "DD (\<lambda>w. f w * g w) z =
   1.770 -           f z * DD g z + DD f z * g z"
   1.771 +  shows complex_derivative_add_at: "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
   1.772 +    and complex_derivative_diff_at: "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
   1.773 +    and complex_derivative_mult_at: "deriv (\<lambda>w. f w * g w) z =
   1.774 +           f z * deriv g z + deriv f z * g z"
   1.775  proof -
   1.776    obtain s where s: "open s" "z \<in> s" "f holomorphic_on s" "g holomorphic_on s"
   1.777      using assms by (metis analytic_at_two)
   1.778 -  show "DD (\<lambda>w. f w + g w) z = DD f z + DD g z"
   1.779 -    apply (rule DERIV_imp_DD [OF DERIV_add])
   1.780 +  show "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
   1.781 +    apply (rule DERIV_imp_deriv [OF DERIV_add])
   1.782      using s
   1.783 -    apply (auto simp: holomorphic_on_open complex_differentiable_def DD_iff_derivative_complex_differentiable)
   1.784 +    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
   1.785      done
   1.786 -  show "DD (\<lambda>w. f w - g w) z = DD f z - DD g z"
   1.787 -    apply (rule DERIV_imp_DD [OF DERIV_diff])
   1.788 +  show "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
   1.789 +    apply (rule DERIV_imp_deriv [OF DERIV_diff])
   1.790      using s
   1.791 -    apply (auto simp: holomorphic_on_open complex_differentiable_def DD_iff_derivative_complex_differentiable)
   1.792 +    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
   1.793      done
   1.794 -  show "DD (\<lambda>w. f w * g w) z = f z * DD g z + DD f z * g z"
   1.795 -    apply (rule DERIV_imp_DD [OF DERIV_mult'])
   1.796 +  show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
   1.797 +    apply (rule DERIV_imp_deriv [OF DERIV_mult'])
   1.798      using s
   1.799 -    apply (auto simp: holomorphic_on_open complex_differentiable_def DD_iff_derivative_complex_differentiable)
   1.800 +    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
   1.801      done
   1.802  qed
   1.803  
   1.804  lemma complex_derivative_cmult_at:
   1.805 -  "f analytic_on {z} \<Longrightarrow>  DD (\<lambda>w. c * f w) z = c * DD f z"
   1.806 +  "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
   1.807  by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
   1.808  
   1.809  lemma complex_derivative_cmult_right_at:
   1.810 -  "f analytic_on {z} \<Longrightarrow>  DD (\<lambda>w. f w * c) z = DD f z * c"
   1.811 +  "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
   1.812  by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
   1.813  
   1.814 -text{*A composition lemma for functions of mixed type*}
   1.815 -lemma has_vector_derivative_real_complex:
   1.816 -  fixes f :: "complex \<Rightarrow> complex"
   1.817 -  assumes "DERIV f (of_real a) :> f'"
   1.818 -  shows "((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a)"
   1.819 -  using diff_chain_at [OF has_derivative_ident, of f "op * f'" a] assms
   1.820 -  unfolding has_field_derivative_def has_vector_derivative_def o_def
   1.821 -  by (auto simp: mult_ac scaleR_conv_of_real)
   1.822 -
   1.823  subsection{*Complex differentiation of sequences and series*}
   1.824  
   1.825  lemma has_complex_derivative_sequence:
   1.826 @@ -975,61 +972,13 @@
   1.827    using assms 
   1.828    by auto
   1.829  
   1.830 -subsection{*Further useful properties of complex conjugation*}
   1.831 -
   1.832 -lemma continuous_within_cnj: "continuous (at z within s) cnj"
   1.833 -by (metis bounded_linear_cnj linear_continuous_within)
   1.834 -
   1.835 -lemma continuous_on_cnj: "continuous_on s cnj"
   1.836 -by (metis bounded_linear_cnj linear_continuous_on)
   1.837 -
   1.838 -subsection {*Some limit theorems about real part of real series etc.*}
   1.839 -
   1.840 -lemma real_lim:
   1.841 -  fixes l::complex
   1.842 -  assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   1.843 -  shows  "l \<in> \<real>"
   1.844 -proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
   1.845 -  show "eventually (\<lambda>x. f x \<in> \<real>) F"
   1.846 -    using assms(3, 4) by (auto intro: eventually_mono)
   1.847 -qed
   1.848 -
   1.849 -lemma real_lim_sequentially:
   1.850 -  fixes l::complex
   1.851 -  shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
   1.852 -by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
   1.853 -
   1.854 -lemma real_series: 
   1.855 -  fixes l::complex
   1.856 -  shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
   1.857 -unfolding sums_def
   1.858 -by (metis real_lim_sequentially setsum_in_Reals)
   1.859 -
   1.860 -
   1.861 -lemma Lim_null_comparison_Re:
   1.862 -   "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F \<Longrightarrow>  (g ---> 0) F \<Longrightarrow> (f ---> 0) F"
   1.863 -  by (metis Lim_null_comparison complex_Re_zero tendsto_Re)
   1.864 -
   1.865 -
   1.866 -(*MOVE? But not to Finite_Cartesian_Product*)
   1.867 -lemma sums_vec_nth :
   1.868 -  assumes "f sums a"
   1.869 -  shows "(\<lambda>x. f x $ i) sums a $ i"
   1.870 -using assms unfolding sums_def
   1.871 -by (auto dest: tendsto_vec_nth [where i=i])
   1.872 -
   1.873 -lemma summable_vec_nth :
   1.874 -  assumes "summable f"
   1.875 -  shows "summable (\<lambda>x. f x $ i)"
   1.876 -using assms unfolding summable_def
   1.877 -by (blast intro: sums_vec_nth)
   1.878 +subsection {* Taylor on Complex Numbers *}
   1.879  
   1.880  lemma setsum_Suc_reindex:
   1.881    fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   1.882      shows  "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
   1.883  by (induct n) auto
   1.884  
   1.885 -text{*A kind of complex Taylor theorem.*}
   1.886  lemma complex_taylor:
   1.887    assumes s: "convex s" 
   1.888        and f: "\<And>i x. x \<in> s \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within s)"
   1.889 @@ -1127,6 +1076,7 @@
   1.890  qed
   1.891  
   1.892  text{* Something more like the traditional MVT for real components.*}
   1.893 +
   1.894  lemma complex_mvt_line:
   1.895    assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
   1.896      shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:01 2014 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:02 2014 +0200
     2.3 @@ -903,8 +903,6 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 -
     2.8 -
     2.9  subsection {* Differentiability of inverse function (most basic form) *}
    2.10  
    2.11  lemma has_derivative_inverse_basic:
     3.1 --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Wed Apr 02 18:35:01 2014 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Wed Apr 02 18:35:02 2014 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  theory Multivariate_Analysis
     3.5 -imports Fashoda Extended_Real_Limits Determinants Ordered_Euclidean_Space
     3.6 +imports Fashoda Extended_Real_Limits Determinants Ordered_Euclidean_Space Complex_Analysis_Basics
     3.7  begin
     3.8  
     3.9  end