src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 64394 141e1ed8d5a0
parent 64267 b9a1486e79be
child 65587 16a8991ab398
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 25 11:55:38 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 25 15:46:07 2016 +0100
     1.3 @@ -277,144 +277,7 @@
     1.4  
     1.5  subsection\<open>Holomorphic functions\<close>
     1.6  
     1.7 -definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
     1.8 -           (infixr "(field'_differentiable)" 50)
     1.9 -  where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
    1.10 -
    1.11 -lemma field_differentiable_derivI:
    1.12 -    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
    1.13 -by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
    1.14 -
    1.15 -lemma field_differentiable_imp_continuous_at:
    1.16 -    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
    1.17 -  by (metis DERIV_continuous field_differentiable_def)
    1.18 -
    1.19 -lemma field_differentiable_within_subset:
    1.20 -    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
    1.21 -     \<Longrightarrow> f field_differentiable (at x within t)"
    1.22 -  by (metis DERIV_subset field_differentiable_def)
    1.23 -
    1.24 -lemma field_differentiable_at_within:
    1.25 -    "\<lbrakk>f field_differentiable (at x)\<rbrakk>
    1.26 -     \<Longrightarrow> f field_differentiable (at x within s)"
    1.27 -  unfolding field_differentiable_def
    1.28 -  by (metis DERIV_subset top_greatest)
    1.29 -
    1.30 -lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
    1.31 -proof -
    1.32 -  show ?thesis
    1.33 -    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
    1.34 -    by (force intro: has_derivative_mult_right)
    1.35 -qed
    1.36 -
    1.37 -lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
    1.38 -  unfolding field_differentiable_def has_field_derivative_def
    1.39 -  by (rule exI [where x=0])
    1.40 -     (metis has_derivative_const lambda_zero)
    1.41 -
    1.42 -lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
    1.43 -  unfolding field_differentiable_def has_field_derivative_def
    1.44 -  by (rule exI [where x=1])
    1.45 -     (simp add: lambda_one [symmetric])
    1.46 -
    1.47 -lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
    1.48 -  unfolding id_def by (rule field_differentiable_ident)
    1.49 -
    1.50 -lemma field_differentiable_minus [derivative_intros]:
    1.51 -  "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
    1.52 -  unfolding field_differentiable_def
    1.53 -  by (metis field_differentiable_minus)
    1.54 -
    1.55 -lemma field_differentiable_add [derivative_intros]:
    1.56 -  assumes "f field_differentiable F" "g field_differentiable F"
    1.57 -    shows "(\<lambda>z. f z + g z) field_differentiable F"
    1.58 -  using assms unfolding field_differentiable_def
    1.59 -  by (metis field_differentiable_add)
    1.60 -
    1.61 -lemma field_differentiable_add_const [simp,derivative_intros]:
    1.62 -     "op + c field_differentiable F"
    1.63 -  by (simp add: field_differentiable_add)
    1.64 -
    1.65 -lemma field_differentiable_sum [derivative_intros]:
    1.66 -  "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
    1.67 -  by (induct I rule: infinite_finite_induct)
    1.68 -     (auto intro: field_differentiable_add field_differentiable_const)
    1.69 -
    1.70 -lemma field_differentiable_diff [derivative_intros]:
    1.71 -  assumes "f field_differentiable F" "g field_differentiable F"
    1.72 -    shows "(\<lambda>z. f z - g z) field_differentiable F"
    1.73 -  using assms unfolding field_differentiable_def
    1.74 -  by (metis field_differentiable_diff)
    1.75 -
    1.76 -lemma field_differentiable_inverse [derivative_intros]:
    1.77 -  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
    1.78 -  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
    1.79 -  using assms unfolding field_differentiable_def
    1.80 -  by (metis DERIV_inverse_fun)
    1.81 -
    1.82 -lemma field_differentiable_mult [derivative_intros]:
    1.83 -  assumes "f field_differentiable (at a within s)"
    1.84 -          "g field_differentiable (at a within s)"
    1.85 -    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
    1.86 -  using assms unfolding field_differentiable_def
    1.87 -  by (metis DERIV_mult [of f _ a s g])
    1.88 -
    1.89 -lemma field_differentiable_divide [derivative_intros]:
    1.90 -  assumes "f field_differentiable (at a within s)"
    1.91 -          "g field_differentiable (at a within s)"
    1.92 -          "g a \<noteq> 0"
    1.93 -    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
    1.94 -  using assms unfolding field_differentiable_def
    1.95 -  by (metis DERIV_divide [of f _ a s g])
    1.96 -
    1.97 -lemma field_differentiable_power [derivative_intros]:
    1.98 -  assumes "f field_differentiable (at a within s)"
    1.99 -    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
   1.100 -  using assms unfolding field_differentiable_def
   1.101 -  by (metis DERIV_power)
   1.102 -
   1.103 -lemma field_differentiable_transform_within:
   1.104 -  "0 < d \<Longrightarrow>
   1.105 -        x \<in> s \<Longrightarrow>
   1.106 -        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
   1.107 -        f field_differentiable (at x within s)
   1.108 -        \<Longrightarrow> g field_differentiable (at x within s)"
   1.109 -  unfolding field_differentiable_def has_field_derivative_def
   1.110 -  by (blast intro: has_derivative_transform_within)
   1.111 -
   1.112 -lemma field_differentiable_compose_within:
   1.113 -  assumes "f field_differentiable (at a within s)"
   1.114 -          "g field_differentiable (at (f a) within f`s)"
   1.115 -    shows "(g o f) field_differentiable (at a within s)"
   1.116 -  using assms unfolding field_differentiable_def
   1.117 -  by (metis DERIV_image_chain)
   1.118 -
   1.119 -lemma field_differentiable_compose:
   1.120 -  "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
   1.121 -          \<Longrightarrow> (g o f) field_differentiable at z"
   1.122 -by (metis field_differentiable_at_within field_differentiable_compose_within)
   1.123 -
   1.124 -lemma field_differentiable_within_open:
   1.125 -     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
   1.126 -                          f field_differentiable at a"
   1.127 -  unfolding field_differentiable_def
   1.128 -  by (metis at_within_open)
   1.129 -
   1.130 -subsection\<open>Caratheodory characterization\<close>
   1.131 -
   1.132 -lemma field_differentiable_caratheodory_at:
   1.133 -  "f field_differentiable (at z) \<longleftrightarrow>
   1.134 -         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
   1.135 -  using CARAT_DERIV [of f]
   1.136 -  by (simp add: field_differentiable_def has_field_derivative_def)
   1.137 -
   1.138 -lemma field_differentiable_caratheodory_within:
   1.139 -  "f field_differentiable (at z within s) \<longleftrightarrow>
   1.140 -         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
   1.141 -  using DERIV_caratheodory_within [of f]
   1.142 -  by (simp add: field_differentiable_def has_field_derivative_def)
   1.143 -
   1.144 -subsection\<open>Holomorphic\<close>
   1.145 +subsection\<open>Holomorphic functions\<close>
   1.146  
   1.147  definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
   1.148             (infixl "(holomorphic'_on)" 50)
   1.149 @@ -428,6 +291,11 @@
   1.150  lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
   1.151    by (simp add: holomorphic_on_def)
   1.152  
   1.153 +lemma holomorphic_on_imp_differentiable_on:
   1.154 +    "f holomorphic_on s \<Longrightarrow> f differentiable_on s"
   1.155 +  unfolding holomorphic_on_def differentiable_on_def
   1.156 +  by (simp add: field_differentiable_imp_differentiable)
   1.157 +
   1.158  lemma holomorphic_on_imp_differentiable_at:
   1.159     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
   1.160  using at_within_open holomorphic_on_def by fastforce
   1.161 @@ -594,6 +462,20 @@
   1.162      apply (auto simp: holomorphic_derivI)
   1.163      done
   1.164  
   1.165 +subsection\<open>Caratheodory characterization\<close>
   1.166 +
   1.167 +lemma field_differentiable_caratheodory_at:
   1.168 +  "f field_differentiable (at z) \<longleftrightarrow>
   1.169 +         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
   1.170 +  using CARAT_DERIV [of f]
   1.171 +  by (simp add: field_differentiable_def has_field_derivative_def)
   1.172 +
   1.173 +lemma field_differentiable_caratheodory_within:
   1.174 +  "f field_differentiable (at z within s) \<longleftrightarrow>
   1.175 +         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
   1.176 +  using DERIV_caratheodory_within [of f]
   1.177 +  by (simp add: field_differentiable_def has_field_derivative_def)
   1.178 +
   1.179  subsection\<open>Analyticity on a set\<close>
   1.180  
   1.181  definition analytic_on (infixl "(analytic'_on)" 50)