author hoelzl Wed Apr 02 18:35:02 2014 +0200 (2014-04-02) changeset 56370 7c717ba55a0b parent 56369 2704ca85be98 child 56371 fb9ae0727548
reorder Complex_Analysis_Basics; rename DD to deriv
```     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.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.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.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.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.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.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.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
```