Tagged Conformal_Mappings in HOL-Analysis
authorWenda Li <wl302@cam.ac.uk>
Sun Jul 15 01:14:04 2018 +0100 (18 months ago)
changeset 68629f36858fdf768
parent 68628 958511f53de8
child 68630 c55f6f0b3854
child 68633 ae4373f3d8d3
child 68639 357fca99a65a
Tagged Conformal_Mappings in HOL-Analysis
src/HOL/Analysis/Conformal_Mappings.thy
     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jul 13 22:10:05 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sun Jul 15 01:14:04 2018 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  
     1.5  begin
     1.6  
     1.7 +(* FIXME mv to Cauchy_Integral_Theorem.thy *)
     1.8  subsection\<open>Cauchy's inequality and more versions of Liouville\<close>
     1.9  
    1.10  lemma Cauchy_higher_deriv_bound:
    1.11 @@ -54,7 +55,7 @@
    1.12      by (auto simp: norm_divide norm_mult norm_power field_simps der_dif le_B0)
    1.13  qed
    1.14  
    1.15 -proposition Cauchy_inequality:
    1.16 +lemma Cauchy_inequality:
    1.17      assumes holf: "f holomorphic_on (ball \<xi> r)"
    1.18          and contf: "continuous_on (cball \<xi> r) f"
    1.19          and "0 < r"
    1.20 @@ -79,7 +80,7 @@
    1.21      by (simp add: norm_divide norm_mult field_simps)
    1.22  qed
    1.23  
    1.24 -proposition Liouville_polynomial:
    1.25 +lemma Liouville_polynomial:
    1.26      assumes holf: "f holomorphic_on UNIV"
    1.27          and nof: "\<And>z. A \<le> norm z \<Longrightarrow> norm(f z) \<le> B * norm z ^ n"
    1.28        shows "f \<xi> = (\<Sum>k\<le>n. (deriv^^k) f 0 / fact k * \<xi> ^ k)"
    1.29 @@ -165,11 +166,9 @@
    1.30      using Liouville_polynomial [OF holf, of 0 B 0, simplified] that by blast
    1.31  qed
    1.32  
    1.33 -
    1.34 -
    1.35  text\<open>A holomorphic function f has only isolated zeros unless f is 0.\<close>
    1.36  
    1.37 -proposition powser_0_nonzero:
    1.38 +lemma powser_0_nonzero:
    1.39    fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
    1.40    assumes r: "0 < r"
    1.41        and sm: "\<And>x. norm (x - \<xi>) < r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
    1.42 @@ -222,10 +221,13 @@
    1.43      using \<open>0 < r\<close> \<open>0 < s\<close> by (auto simp: dist_commute dist_norm)
    1.44  qed
    1.45  
    1.46 +subsection \<open>Analytic continuation\<close>
    1.47 +
    1.48  proposition isolated_zeros:
    1.49    assumes holf: "f holomorphic_on S"
    1.50        and "open S" "connected S" "\<xi> \<in> S" "f \<xi> = 0" "\<beta> \<in> S" "f \<beta> \<noteq> 0"
    1.51 -  obtains r where "0 < r" "ball \<xi> r \<subseteq> S" "\<And>z. z \<in> ball \<xi> r - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
    1.52 +    obtains r where "0 < r" and "ball \<xi> r \<subseteq> S" and 
    1.53 +        "\<And>z. z \<in> ball \<xi> r - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
    1.54  proof -
    1.55    obtain r where "0 < r" and r: "ball \<xi> r \<subseteq> S"
    1.56      using \<open>open S\<close> \<open>\<xi> \<in> S\<close> open_contains_ball_eq by blast
    1.57 @@ -246,11 +248,10 @@
    1.58      using r s by auto
    1.59  qed
    1.60  
    1.61 -
    1.62  proposition analytic_continuation:
    1.63    assumes holf: "f holomorphic_on S"
    1.64 -      and S: "open S" "connected S"
    1.65 -      and "U \<subseteq> S" "\<xi> \<in> S"
    1.66 +      and "open S" and "connected S"
    1.67 +      and "U \<subseteq> S" and "\<xi> \<in> S"
    1.68        and "\<xi> islimpt U"
    1.69        and fU0 [simp]: "\<And>z. z \<in> U \<Longrightarrow> f z = 0"
    1.70        and "w \<in> S"
    1.71 @@ -279,8 +280,10 @@
    1.72  qed
    1.73  
    1.74  corollary analytic_continuation_open:
    1.75 -  assumes "open s" "open s'" "s \<noteq> {}" "connected s'" "s \<subseteq> s'"
    1.76 -  assumes "f holomorphic_on s'" "g holomorphic_on s'" "\<And>z. z \<in> s \<Longrightarrow> f z = g z"
    1.77 +  assumes "open s" and "open s'" and "s \<noteq> {}" and "connected s'" 
    1.78 +      and "s \<subseteq> s'"
    1.79 +  assumes "f holomorphic_on s'" and "g holomorphic_on s'" 
    1.80 +      and "\<And>z. z \<in> s \<Longrightarrow> f z = g z"
    1.81    assumes "z \<in> s'"
    1.82    shows   "f z = g z"
    1.83  proof -
    1.84 @@ -293,7 +296,6 @@
    1.85    thus ?thesis by simp
    1.86  qed
    1.87  
    1.88 -
    1.89  subsection\<open>Open mapping theorem\<close>
    1.90  
    1.91  lemma holomorphic_contract_to_zero:
    1.92 @@ -353,11 +355,10 @@
    1.93    with that show ?thesis by blast
    1.94  qed
    1.95  
    1.96 -
    1.97  theorem open_mapping_thm:
    1.98    assumes holf: "f holomorphic_on S"
    1.99 -      and S: "open S" "connected S"
   1.100 -      and "open U" "U \<subseteq> S"
   1.101 +      and S: "open S" and "connected S"
   1.102 +      and "open U" and "U \<subseteq> S"
   1.103        and fne: "~ f constant_on S"
   1.104      shows "open (f ` U)"
   1.105  proof -
   1.106 @@ -449,8 +450,8 @@
   1.107          using w \<open>open X\<close> interior_eq by auto
   1.108        have hol: "(\<lambda>z. f z - x) holomorphic_on S"
   1.109          by (simp add: holf holomorphic_on_diff)
   1.110 -      with fne [unfolded constant_on_def] analytic_continuation [OF hol S \<open>X \<subseteq> S\<close> _ wis]
   1.111 -           not \<open>X \<subseteq> S\<close> w
   1.112 +      with fne [unfolded constant_on_def] 
   1.113 +           analytic_continuation[OF hol S \<open>connected S\<close> \<open>X \<subseteq> S\<close> _ wis] not \<open>X \<subseteq> S\<close> w
   1.114        show False by auto
   1.115      qed
   1.116      ultimately show ?thesis
   1.117 @@ -462,9 +463,8 @@
   1.118      by force
   1.119  qed
   1.120  
   1.121 -
   1.122  text\<open>No need for @{term S} to be connected. But the nonconstant condition is stronger.\<close>
   1.123 -corollary open_mapping_thm2:
   1.124 +corollary%unimportant open_mapping_thm2:
   1.125    assumes holf: "f holomorphic_on S"
   1.126        and S: "open S"
   1.127        and "open U" "U \<subseteq> S"
   1.128 @@ -494,7 +494,7 @@
   1.129      by force
   1.130  qed
   1.131  
   1.132 -corollary open_mapping_thm3:
   1.133 +corollary%unimportant open_mapping_thm3:
   1.134    assumes holf: "f holomorphic_on S"
   1.135        and "open S" and injf: "inj_on f S"
   1.136      shows  "open (f ` S)"
   1.137 @@ -503,17 +503,15 @@
   1.138  apply (simp_all add:)
   1.139  using injective_not_constant subset_inj_on by blast
   1.140  
   1.141 -
   1.142 -
   1.143 -subsection\<open>Maximum Modulus Principle\<close>
   1.144 +subsection\<open>Maximum modulus principle\<close>
   1.145  
   1.146  text\<open>If @{term f} is holomorphic, then its norm (modulus) cannot exhibit a true local maximum that is
   1.147     properly within the domain of @{term f}.\<close>
   1.148  
   1.149  proposition maximum_modulus_principle:
   1.150    assumes holf: "f holomorphic_on S"
   1.151 -      and S: "open S" "connected S"
   1.152 -      and "open U" "U \<subseteq> S" "\<xi> \<in> U"
   1.153 +      and S: "open S" and "connected S"
   1.154 +      and "open U" and "U \<subseteq> S" and "\<xi> \<in> U"
   1.155        and no: "\<And>z. z \<in> U \<Longrightarrow> norm(f z) \<le> norm(f \<xi>)"
   1.156      shows "f constant_on S"
   1.157  proof (rule ccontr)
   1.158 @@ -535,7 +533,6 @@
   1.159      by blast
   1.160  qed
   1.161  
   1.162 -
   1.163  proposition maximum_modulus_frontier:
   1.164    assumes holf: "f holomorphic_on (interior S)"
   1.165        and contf: "continuous_on (closure S) f"
   1.166 @@ -588,7 +585,7 @@
   1.167      using z \<open>\<xi> \<in> S\<close> closure_subset by fastforce
   1.168  qed
   1.169  
   1.170 -corollary maximum_real_frontier:
   1.171 +corollary%unimportant maximum_real_frontier:
   1.172    assumes holf: "f holomorphic_on (interior S)"
   1.173        and contf: "continuous_on (closure S) f"
   1.174        and bos: "bounded S"
   1.175 @@ -599,8 +596,7 @@
   1.176        Transcendental.continuous_on_exp holomorphic_on_compose holomorphic_on_exp assms
   1.177  by auto
   1.178  
   1.179 -
   1.180 -subsection\<open>Factoring out a zero according to its order\<close>
   1.181 +subsection%unimportant \<open>Factoring out a zero according to its order\<close>
   1.182  
   1.183  lemma holomorphic_factor_order_of_zero:
   1.184    assumes holf: "f holomorphic_on S"
   1.185 @@ -900,8 +896,7 @@
   1.186      by meson+
   1.187  qed
   1.188  
   1.189 -
   1.190 -proposition pole_at_infinity:
   1.191 +lemma pole_at_infinity:
   1.192    assumes holf: "f holomorphic_on UNIV" and lim: "((inverse o f) \<longlongrightarrow> l) at_infinity"
   1.193    obtains a n where "\<And>z. f z = (\<Sum>i\<le>n. a i * z^i)"
   1.194  proof (cases "l = 0")
   1.195 @@ -1016,10 +1011,9 @@
   1.196      qed
   1.197  qed
   1.198  
   1.199 +subsection%unimportant \<open>Entire proper functions are precisely the non-trivial polynomials\<close>
   1.200  
   1.201 -subsection\<open>Entire proper functions are precisely the non-trivial polynomials\<close>
   1.202 -
   1.203 -proposition proper_map_polyfun:
   1.204 +lemma proper_map_polyfun:
   1.205      fixes c :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,heine_borel}"
   1.206    assumes "closed S" and "compact K" and c: "c i \<noteq> 0" "1 \<le> i" "i \<le> n"
   1.207      shows "compact (S \<inter> {z. (\<Sum>i\<le>n. c i * z^i) \<in> K})"
   1.208 @@ -1048,14 +1042,13 @@
   1.209      by (auto simp add: vimage_def)
   1.210  qed
   1.211  
   1.212 -corollary proper_map_polyfun_univ:
   1.213 +lemma proper_map_polyfun_univ:
   1.214      fixes c :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,heine_borel}"
   1.215    assumes "compact K" "c i \<noteq> 0" "1 \<le> i" "i \<le> n"
   1.216      shows "compact ({z. (\<Sum>i\<le>n. c i * z^i) \<in> K})"
   1.217 -using proper_map_polyfun [of UNIV K c i n] assms by simp
   1.218 +  using proper_map_polyfun [of UNIV K c i n] assms by simp
   1.219  
   1.220 -
   1.221 -proposition proper_map_polyfun_eq:
   1.222 +lemma proper_map_polyfun_eq:
   1.223    assumes "f holomorphic_on UNIV"
   1.224      shows "(\<forall>k. compact k \<longrightarrow> compact {z. f z \<in> k}) \<longleftrightarrow>
   1.225             (\<exists>c n. 0 < n \<and> (c n \<noteq> 0) \<and> f = (\<lambda>z. \<Sum>i\<le>n. c i * z^i))"
   1.226 @@ -1113,10 +1106,9 @@
   1.227    then show ?lhs by blast
   1.228  qed
   1.229  
   1.230 +subsection \<open>Relating invertibility and nonvanishing of derivative\<close>
   1.231  
   1.232 -subsection\<open>Relating invertibility and nonvanishing of derivative\<close>
   1.233 -
   1.234 -proposition has_complex_derivative_locally_injective:
   1.235 +lemma has_complex_derivative_locally_injective:
   1.236    assumes holf: "f holomorphic_on S"
   1.237        and S: "\<xi> \<in> S" "open S"
   1.238        and dnz: "deriv f \<xi> \<noteq> 0"
   1.239 @@ -1155,8 +1147,7 @@
   1.240      done
   1.241  qed
   1.242  
   1.243 -
   1.244 -proposition has_complex_derivative_locally_invertible:
   1.245 +lemma has_complex_derivative_locally_invertible:
   1.246    assumes holf: "f holomorphic_on S"
   1.247        and S: "\<xi> \<in> S" "open S"
   1.248        and dnz: "deriv f \<xi> \<noteq> 0"
   1.249 @@ -1177,8 +1168,7 @@
   1.250      using \<open>0 < r\<close> \<open>ball \<xi> r \<subseteq> S\<close> \<open>inj_on f (ball \<xi> r)\<close> that  by blast
   1.251  qed
   1.252  
   1.253 -
   1.254 -proposition holomorphic_injective_imp_regular:
   1.255 +lemma holomorphic_injective_imp_regular:
   1.256    assumes holf: "f holomorphic_on S"
   1.257        and "open S" and injf: "inj_on f S"
   1.258        and "\<xi> \<in> S"
   1.259 @@ -1268,7 +1258,6 @@
   1.260    qed
   1.261  qed
   1.262  
   1.263 -
   1.264  text\<open>Hence a nice clean inverse function theorem\<close>
   1.265  
   1.266  proposition holomorphic_has_inverse:
   1.267 @@ -1311,7 +1300,6 @@
   1.268    qed
   1.269  qed
   1.270  
   1.271 -
   1.272  subsection\<open>The Schwarz Lemma\<close>
   1.273  
   1.274  lemma Schwarz1:
   1.275 @@ -1321,7 +1309,7 @@
   1.276        and boS: "bounded S"
   1.277        and "S \<noteq> {}"
   1.278    obtains w where "w \<in> frontier S"
   1.279 -                  "\<And>z. z \<in> closure S \<Longrightarrow> norm (f z) \<le> norm (f w)"
   1.280 +       "\<And>z. z \<in> closure S \<Longrightarrow> norm (f z) \<le> norm (f w)"
   1.281  proof -
   1.282    have connf: "continuous_on (closure S) (norm o f)"
   1.283      using contf continuous_on_compose continuous_on_norm_id by blast
   1.284 @@ -1376,14 +1364,15 @@
   1.285      using that by blast
   1.286  qed
   1.287  
   1.288 -
   1.289  proposition Schwarz_Lemma:
   1.290    assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
   1.291        and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
   1.292        and \<xi>: "norm \<xi> < 1"
   1.293      shows "norm (f \<xi>) \<le> norm \<xi>" and "norm(deriv f 0) \<le> 1"
   1.294 -      and "((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
   1.295 -           \<Longrightarrow> \<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1" (is "?P \<Longrightarrow> ?Q")
   1.296 +      and "((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) 
   1.297 +            \<or> norm(deriv f 0) = 1)
   1.298 +           \<Longrightarrow> \<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1" 
   1.299 +      (is "?P \<Longrightarrow> ?Q")
   1.300  proof -
   1.301    obtain h where holh: "h holomorphic_on (ball 0 1)"
   1.302               and fz_eq: "\<And>z. norm z < 1 \<Longrightarrow> f z = z * (h z)" and df0: "deriv f 0 = h 0"
   1.303 @@ -1457,9 +1446,11 @@
   1.304  corollary Schwarz_Lemma':
   1.305    assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
   1.306        and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
   1.307 -    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and>
   1.308 -           (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
   1.309 -           \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
   1.310 +    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) 
   1.311 +            \<and> norm(deriv f 0) \<le> 1) 
   1.312 +            \<and> (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) 
   1.313 +              \<or> norm(deriv f 0) = 1)
   1.314 +              \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
   1.315    using Schwarz_Lemma [OF assms]
   1.316    by (metis (no_types) norm_eq_zero zero_less_one)
   1.317  
   1.318 @@ -1667,7 +1658,7 @@
   1.319      using \<open>d \<noteq> 0\<close> False by (simp_all add: holf1 holf2 contf)
   1.320  qed
   1.321  
   1.322 -proposition holomorphic_on_paste_across_line:
   1.323 +lemma holomorphic_on_paste_across_line:
   1.324    assumes S: "open S" and "d \<noteq> 0"
   1.325        and holf1: "f holomorphic_on (S \<inter> {z. d \<bullet> z < k})"
   1.326        and holf2: "f holomorphic_on (S \<inter> {z. k < d \<bullet> z})"
   1.327 @@ -1954,7 +1945,7 @@
   1.328  
   1.329  proposition Bloch_unit:
   1.330    assumes holf: "f holomorphic_on ball a 1" and [simp]: "deriv f a = 1"
   1.331 -  obtains b r where "1/12 < r" "ball b r \<subseteq> f ` (ball a 1)"
   1.332 +  obtains b r where "1/12 < r" and "ball b r \<subseteq> f ` (ball a 1)"
   1.333  proof -
   1.334    define r :: real where "r = 249/256"
   1.335    have "0 < r" "r < 1" by (auto simp: r_def)
   1.336 @@ -2042,7 +2033,6 @@
   1.337      by (rule that)
   1.338  qed
   1.339  
   1.340 -
   1.341  theorem Bloch:
   1.342    assumes holf: "f holomorphic_on ball a r" and "0 < r"
   1.343        and r': "r' \<le> r * norm (deriv f a) / 12"
   1.344 @@ -2158,12 +2148,12 @@
   1.345    qed
   1.346  qed
   1.347  
   1.348 -subsection \<open>Foundations of Cauchy's residue theorem\<close>
   1.349 +subsection \<open>Cauchy's residue theorem\<close>
   1.350  
   1.351  text\<open>Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem.
   1.352      Interactive Theorem Proving\<close>
   1.353  
   1.354 -definition residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
   1.355 +definition%important residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
   1.356    "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
   1.357      \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
   1.358  
   1.359 @@ -2356,7 +2346,6 @@
   1.360      by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z \<epsilon>" "circlepath z r"])
   1.361  qed
   1.362  
   1.363 -
   1.364  lemma residue_holo:
   1.365    assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s"
   1.366    shows "residue f z = 0"
   1.367 @@ -2375,11 +2364,9 @@
   1.368    thus ?thesis unfolding c_def  by auto
   1.369  qed
   1.370  
   1.371 -
   1.372  lemma residue_const:"residue (\<lambda>_. c) z = 0"
   1.373    by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)
   1.374  
   1.375 -
   1.376  lemma residue_add:
   1.377    assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
   1.378        and g_holo:"g holomorphic_on s - {z}"
   1.379 @@ -2402,7 +2389,6 @@
   1.380      by (auto simp add:c_def)
   1.381  qed
   1.382  
   1.383 -
   1.384  lemma residue_lmul:
   1.385    assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
   1.386    shows "residue (\<lambda>z. c * (f z)) z= c * residue f z"
   1.387 @@ -2524,8 +2510,6 @@
   1.388    shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
   1.389    using residue_holomorphic_over_power[OF assms] by simp
   1.390  
   1.391 -subsubsection \<open>Cauchy's residue theorem\<close>
   1.392 -
   1.393  lemma get_integrable_path:
   1.394    assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
   1.395    obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b"
   1.396 @@ -2929,7 +2913,7 @@
   1.397      by auto
   1.398  qed
   1.399  
   1.400 -lemma Residue_theorem:
   1.401 +theorem Residue_theorem:
   1.402    fixes s pts::"complex set" and f::"complex \<Rightarrow> complex"
   1.403      and g::"real \<Rightarrow> complex"
   1.404    assumes "open s" "connected s" "finite pts" and
   1.405 @@ -2973,7 +2957,8 @@
   1.406  
   1.407  subsection \<open>Non-essential singular points\<close>
   1.408  
   1.409 -definition is_pole :: "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" where
   1.410 +definition%important is_pole :: 
   1.411 +  "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" where
   1.412    "is_pole f a =  (LIM x (at a). f x :> at_infinity)"
   1.413  
   1.414  lemma is_pole_cong:
   1.415 @@ -3699,13 +3684,17 @@
   1.416  
   1.417  subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
   1.418  
   1.419 -definition zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
   1.420 +
   1.421 +definition%important zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
   1.422    "zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
   1.423 -                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n) \<and> h w \<noteq>0)))"
   1.424 +                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n)
   1.425 +                   \<and> h w \<noteq>0)))"
   1.426  
   1.427 -definition zor_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where
   1.428 -  "zor_poly f z = (SOME h. \<exists>r . r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
   1.429 -                   \<and> (\<forall>w\<in>cball z r-{z}. f w =  h w * (w-z) powr (zorder f z) \<and> h w \<noteq>0))"
   1.430 +definition%important zor_poly
   1.431 +    ::"[complex \<Rightarrow> complex, complex] \<Rightarrow> complex \<Rightarrow> complex" where
   1.432 +  "zor_poly f z = (SOME h. \<exists>r. r > 0 \<and> h holomorphic_on cball z r \<and> h z \<noteq> 0
   1.433 +                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w - z) powr (zorder f z)
   1.434 +                   \<and> h w \<noteq>0))"
   1.435  
   1.436  lemma zorder_exist:
   1.437    fixes f::"complex \<Rightarrow> complex" and z::complex
   1.438 @@ -3803,7 +3792,6 @@
   1.439      by (auto simp add:dist_commute)
   1.440  qed
   1.441  
   1.442 -
   1.443  lemma 
   1.444    fixes f g::"complex \<Rightarrow> complex" and z::complex
   1.445    assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"  
   1.446 @@ -4881,8 +4869,8 @@
   1.447  
   1.448  theorem Rouche_theorem:
   1.449    fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
   1.450 -  defines "fg\<equiv>(\<lambda>p. f p+ g p)"
   1.451 -  defines "zeros_fg\<equiv>{p. fg p =0}" and "zeros_f\<equiv>{p. f p=0}"
   1.452 +  defines "fg\<equiv>(\<lambda>p. f p + g p)"
   1.453 +  defines "zeros_fg\<equiv>{p. fg p = 0}" and "zeros_f\<equiv>{p. f p = 0}"
   1.454    assumes
   1.455      "open s" and "connected s" and
   1.456      "finite zeros_fg" and