# HG changeset patch
# User Wenda Li <wl302@cam.ac.uk>
# Date 1531613644 -3600
# Node ID f36858fdf7686cf9f49f4bbec0255eff45b753ff
# Parent  958511f53de8de6954b4c72a4c19975e251e3ea0
Tagged Conformal_Mappings in HOL-Analysis

diff -r 958511f53de8 -r f36858fdf768 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jul 13 22:10:05 2018 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sun Jul 15 01:14:04 2018 +0100
@@ -9,6 +9,7 @@
 
 begin
 
+(* FIXME mv to Cauchy_Integral_Theorem.thy *)
 subsection\<open>Cauchy's inequality and more versions of Liouville\<close>
 
 lemma Cauchy_higher_deriv_bound:
@@ -54,7 +55,7 @@
     by (auto simp: norm_divide norm_mult norm_power field_simps der_dif le_B0)
 qed
 
-proposition Cauchy_inequality:
+lemma Cauchy_inequality:
     assumes holf: "f holomorphic_on (ball \<xi> r)"
         and contf: "continuous_on (cball \<xi> r) f"
         and "0 < r"
@@ -79,7 +80,7 @@
     by (simp add: norm_divide norm_mult field_simps)
 qed
 
-proposition Liouville_polynomial:
+lemma Liouville_polynomial:
     assumes holf: "f holomorphic_on UNIV"
         and nof: "\<And>z. A \<le> norm z \<Longrightarrow> norm(f z) \<le> B * norm z ^ n"
       shows "f \<xi> = (\<Sum>k\<le>n. (deriv^^k) f 0 / fact k * \<xi> ^ k)"
@@ -165,11 +166,9 @@
     using Liouville_polynomial [OF holf, of 0 B 0, simplified] that by blast
 qed
 
-
-
 text\<open>A holomorphic function f has only isolated zeros unless f is 0.\<close>
 
-proposition powser_0_nonzero:
+lemma powser_0_nonzero:
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
   assumes r: "0 < r"
       and sm: "\<And>x. norm (x - \<xi>) < r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
@@ -222,10 +221,13 @@
     using \<open>0 < r\<close> \<open>0 < s\<close> by (auto simp: dist_commute dist_norm)
 qed
 
+subsection \<open>Analytic continuation\<close>
+
 proposition isolated_zeros:
   assumes holf: "f holomorphic_on S"
       and "open S" "connected S" "\<xi> \<in> S" "f \<xi> = 0" "\<beta> \<in> S" "f \<beta> \<noteq> 0"
-  obtains r where "0 < r" "ball \<xi> r \<subseteq> S" "\<And>z. z \<in> ball \<xi> r - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
+    obtains r where "0 < r" and "ball \<xi> r \<subseteq> S" and 
+        "\<And>z. z \<in> ball \<xi> r - {\<xi>} \<Longrightarrow> f z \<noteq> 0"
 proof -
   obtain r where "0 < r" and r: "ball \<xi> r \<subseteq> S"
     using \<open>open S\<close> \<open>\<xi> \<in> S\<close> open_contains_ball_eq by blast
@@ -246,11 +248,10 @@
     using r s by auto
 qed
 
-
 proposition analytic_continuation:
   assumes holf: "f holomorphic_on S"
-      and S: "open S" "connected S"
-      and "U \<subseteq> S" "\<xi> \<in> S"
+      and "open S" and "connected S"
+      and "U \<subseteq> S" and "\<xi> \<in> S"
       and "\<xi> islimpt U"
       and fU0 [simp]: "\<And>z. z \<in> U \<Longrightarrow> f z = 0"
       and "w \<in> S"
@@ -279,8 +280,10 @@
 qed
 
 corollary analytic_continuation_open:
-  assumes "open s" "open s'" "s \<noteq> {}" "connected s'" "s \<subseteq> s'"
-  assumes "f holomorphic_on s'" "g holomorphic_on s'" "\<And>z. z \<in> s \<Longrightarrow> f z = g z"
+  assumes "open s" and "open s'" and "s \<noteq> {}" and "connected s'" 
+      and "s \<subseteq> s'"
+  assumes "f holomorphic_on s'" and "g holomorphic_on s'" 
+      and "\<And>z. z \<in> s \<Longrightarrow> f z = g z"
   assumes "z \<in> s'"
   shows   "f z = g z"
 proof -
@@ -293,7 +296,6 @@
   thus ?thesis by simp
 qed
 
-
 subsection\<open>Open mapping theorem\<close>
 
 lemma holomorphic_contract_to_zero:
@@ -353,11 +355,10 @@
   with that show ?thesis by blast
 qed
 
-
 theorem open_mapping_thm:
   assumes holf: "f holomorphic_on S"
-      and S: "open S" "connected S"
-      and "open U" "U \<subseteq> S"
+      and S: "open S" and "connected S"
+      and "open U" and "U \<subseteq> S"
       and fne: "~ f constant_on S"
     shows "open (f ` U)"
 proof -
@@ -449,8 +450,8 @@
         using w \<open>open X\<close> interior_eq by auto
       have hol: "(\<lambda>z. f z - x) holomorphic_on S"
         by (simp add: holf holomorphic_on_diff)
-      with fne [unfolded constant_on_def] analytic_continuation [OF hol S \<open>X \<subseteq> S\<close> _ wis]
-           not \<open>X \<subseteq> S\<close> w
+      with fne [unfolded constant_on_def] 
+           analytic_continuation[OF hol S \<open>connected S\<close> \<open>X \<subseteq> S\<close> _ wis] not \<open>X \<subseteq> S\<close> w
       show False by auto
     qed
     ultimately show ?thesis
@@ -462,9 +463,8 @@
     by force
 qed
 
-
 text\<open>No need for @{term S} to be connected. But the nonconstant condition is stronger.\<close>
-corollary open_mapping_thm2:
+corollary%unimportant open_mapping_thm2:
   assumes holf: "f holomorphic_on S"
       and S: "open S"
       and "open U" "U \<subseteq> S"
@@ -494,7 +494,7 @@
     by force
 qed
 
-corollary open_mapping_thm3:
+corollary%unimportant open_mapping_thm3:
   assumes holf: "f holomorphic_on S"
       and "open S" and injf: "inj_on f S"
     shows  "open (f ` S)"
@@ -503,17 +503,15 @@
 apply (simp_all add:)
 using injective_not_constant subset_inj_on by blast
 
-
-
-subsection\<open>Maximum Modulus Principle\<close>
+subsection\<open>Maximum modulus principle\<close>
 
 text\<open>If @{term f} is holomorphic, then its norm (modulus) cannot exhibit a true local maximum that is
    properly within the domain of @{term f}.\<close>
 
 proposition maximum_modulus_principle:
   assumes holf: "f holomorphic_on S"
-      and S: "open S" "connected S"
-      and "open U" "U \<subseteq> S" "\<xi> \<in> U"
+      and S: "open S" and "connected S"
+      and "open U" and "U \<subseteq> S" and "\<xi> \<in> U"
       and no: "\<And>z. z \<in> U \<Longrightarrow> norm(f z) \<le> norm(f \<xi>)"
     shows "f constant_on S"
 proof (rule ccontr)
@@ -535,7 +533,6 @@
     by blast
 qed
 
-
 proposition maximum_modulus_frontier:
   assumes holf: "f holomorphic_on (interior S)"
       and contf: "continuous_on (closure S) f"
@@ -588,7 +585,7 @@
     using z \<open>\<xi> \<in> S\<close> closure_subset by fastforce
 qed
 
-corollary maximum_real_frontier:
+corollary%unimportant maximum_real_frontier:
   assumes holf: "f holomorphic_on (interior S)"
       and contf: "continuous_on (closure S) f"
       and bos: "bounded S"
@@ -599,8 +596,7 @@
       Transcendental.continuous_on_exp holomorphic_on_compose holomorphic_on_exp assms
 by auto
 
-
-subsection\<open>Factoring out a zero according to its order\<close>
+subsection%unimportant \<open>Factoring out a zero according to its order\<close>
 
 lemma holomorphic_factor_order_of_zero:
   assumes holf: "f holomorphic_on S"
@@ -900,8 +896,7 @@
     by meson+
 qed
 
-
-proposition pole_at_infinity:
+lemma pole_at_infinity:
   assumes holf: "f holomorphic_on UNIV" and lim: "((inverse o f) \<longlongrightarrow> l) at_infinity"
   obtains a n where "\<And>z. f z = (\<Sum>i\<le>n. a i * z^i)"
 proof (cases "l = 0")
@@ -1016,10 +1011,9 @@
     qed
 qed
 
+subsection%unimportant \<open>Entire proper functions are precisely the non-trivial polynomials\<close>
 
-subsection\<open>Entire proper functions are precisely the non-trivial polynomials\<close>
-
-proposition proper_map_polyfun:
+lemma proper_map_polyfun:
     fixes c :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,heine_borel}"
   assumes "closed S" and "compact K" and c: "c i \<noteq> 0" "1 \<le> i" "i \<le> n"
     shows "compact (S \<inter> {z. (\<Sum>i\<le>n. c i * z^i) \<in> K})"
@@ -1048,14 +1042,13 @@
     by (auto simp add: vimage_def)
 qed
 
-corollary proper_map_polyfun_univ:
+lemma proper_map_polyfun_univ:
     fixes c :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,heine_borel}"
   assumes "compact K" "c i \<noteq> 0" "1 \<le> i" "i \<le> n"
     shows "compact ({z. (\<Sum>i\<le>n. c i * z^i) \<in> K})"
-using proper_map_polyfun [of UNIV K c i n] assms by simp
+  using proper_map_polyfun [of UNIV K c i n] assms by simp
 
-
-proposition proper_map_polyfun_eq:
+lemma proper_map_polyfun_eq:
   assumes "f holomorphic_on UNIV"
     shows "(\<forall>k. compact k \<longrightarrow> compact {z. f z \<in> k}) \<longleftrightarrow>
            (\<exists>c n. 0 < n \<and> (c n \<noteq> 0) \<and> f = (\<lambda>z. \<Sum>i\<le>n. c i * z^i))"
@@ -1113,10 +1106,9 @@
   then show ?lhs by blast
 qed
 
+subsection \<open>Relating invertibility and nonvanishing of derivative\<close>
 
-subsection\<open>Relating invertibility and nonvanishing of derivative\<close>
-
-proposition has_complex_derivative_locally_injective:
+lemma has_complex_derivative_locally_injective:
   assumes holf: "f holomorphic_on S"
       and S: "\<xi> \<in> S" "open S"
       and dnz: "deriv f \<xi> \<noteq> 0"
@@ -1155,8 +1147,7 @@
     done
 qed
 
-
-proposition has_complex_derivative_locally_invertible:
+lemma has_complex_derivative_locally_invertible:
   assumes holf: "f holomorphic_on S"
       and S: "\<xi> \<in> S" "open S"
       and dnz: "deriv f \<xi> \<noteq> 0"
@@ -1177,8 +1168,7 @@
     using \<open>0 < r\<close> \<open>ball \<xi> r \<subseteq> S\<close> \<open>inj_on f (ball \<xi> r)\<close> that  by blast
 qed
 
-
-proposition holomorphic_injective_imp_regular:
+lemma holomorphic_injective_imp_regular:
   assumes holf: "f holomorphic_on S"
       and "open S" and injf: "inj_on f S"
       and "\<xi> \<in> S"
@@ -1268,7 +1258,6 @@
   qed
 qed
 
-
 text\<open>Hence a nice clean inverse function theorem\<close>
 
 proposition holomorphic_has_inverse:
@@ -1311,7 +1300,6 @@
   qed
 qed
 
-
 subsection\<open>The Schwarz Lemma\<close>
 
 lemma Schwarz1:
@@ -1321,7 +1309,7 @@
       and boS: "bounded S"
       and "S \<noteq> {}"
   obtains w where "w \<in> frontier S"
-                  "\<And>z. z \<in> closure S \<Longrightarrow> norm (f z) \<le> norm (f w)"
+       "\<And>z. z \<in> closure S \<Longrightarrow> norm (f z) \<le> norm (f w)"
 proof -
   have connf: "continuous_on (closure S) (norm o f)"
     using contf continuous_on_compose continuous_on_norm_id by blast
@@ -1376,14 +1364,15 @@
     using that by blast
 qed
 
-
 proposition Schwarz_Lemma:
   assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
       and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
       and \<xi>: "norm \<xi> < 1"
     shows "norm (f \<xi>) \<le> norm \<xi>" and "norm(deriv f 0) \<le> 1"
-      and "((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
-           \<Longrightarrow> \<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1" (is "?P \<Longrightarrow> ?Q")
+      and "((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) 
+            \<or> norm(deriv f 0) = 1)
+           \<Longrightarrow> \<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1" 
+      (is "?P \<Longrightarrow> ?Q")
 proof -
   obtain h where holh: "h holomorphic_on (ball 0 1)"
              and fz_eq: "\<And>z. norm z < 1 \<Longrightarrow> f z = z * (h z)" and df0: "deriv f 0 = h 0"
@@ -1457,9 +1446,11 @@
 corollary Schwarz_Lemma':
   assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
       and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
-    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and>
-           (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
-           \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
+    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) 
+            \<and> norm(deriv f 0) \<le> 1) 
+            \<and> (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) 
+              \<or> norm(deriv f 0) = 1)
+              \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
   using Schwarz_Lemma [OF assms]
   by (metis (no_types) norm_eq_zero zero_less_one)
 
@@ -1667,7 +1658,7 @@
     using \<open>d \<noteq> 0\<close> False by (simp_all add: holf1 holf2 contf)
 qed
 
-proposition holomorphic_on_paste_across_line:
+lemma holomorphic_on_paste_across_line:
   assumes S: "open S" and "d \<noteq> 0"
       and holf1: "f holomorphic_on (S \<inter> {z. d \<bullet> z < k})"
       and holf2: "f holomorphic_on (S \<inter> {z. k < d \<bullet> z})"
@@ -1954,7 +1945,7 @@
 
 proposition Bloch_unit:
   assumes holf: "f holomorphic_on ball a 1" and [simp]: "deriv f a = 1"
-  obtains b r where "1/12 < r" "ball b r \<subseteq> f ` (ball a 1)"
+  obtains b r where "1/12 < r" and "ball b r \<subseteq> f ` (ball a 1)"
 proof -
   define r :: real where "r = 249/256"
   have "0 < r" "r < 1" by (auto simp: r_def)
@@ -2042,7 +2033,6 @@
     by (rule that)
 qed
 
-
 theorem Bloch:
   assumes holf: "f holomorphic_on ball a r" and "0 < r"
       and r': "r' \<le> r * norm (deriv f a) / 12"
@@ -2158,12 +2148,12 @@
   qed
 qed
 
-subsection \<open>Foundations of Cauchy's residue theorem\<close>
+subsection \<open>Cauchy's residue theorem\<close>
 
 text\<open>Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem.
     Interactive Theorem Proving\<close>
 
-definition residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
+definition%important residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
   "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
     \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
 
@@ -2356,7 +2346,6 @@
     by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z \<epsilon>" "circlepath z r"])
 qed
 
-
 lemma residue_holo:
   assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s"
   shows "residue f z = 0"
@@ -2375,11 +2364,9 @@
   thus ?thesis unfolding c_def  by auto
 qed
 
-
 lemma residue_const:"residue (\<lambda>_. c) z = 0"
   by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)
 
-
 lemma residue_add:
   assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
       and g_holo:"g holomorphic_on s - {z}"
@@ -2402,7 +2389,6 @@
     by (auto simp add:c_def)
 qed
 
-
 lemma residue_lmul:
   assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
   shows "residue (\<lambda>z. c * (f z)) z= c * residue f z"
@@ -2524,8 +2510,6 @@
   shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
   using residue_holomorphic_over_power[OF assms] by simp
 
-subsubsection \<open>Cauchy's residue theorem\<close>
-
 lemma get_integrable_path:
   assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
   obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b"
@@ -2929,7 +2913,7 @@
     by auto
 qed
 
-lemma Residue_theorem:
+theorem Residue_theorem:
   fixes s pts::"complex set" and f::"complex \<Rightarrow> complex"
     and g::"real \<Rightarrow> complex"
   assumes "open s" "connected s" "finite pts" and
@@ -2973,7 +2957,8 @@
 
 subsection \<open>Non-essential singular points\<close>
 
-definition is_pole :: "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" where
+definition%important is_pole :: 
+  "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" where
   "is_pole f a =  (LIM x (at a). f x :> at_infinity)"
 
 lemma is_pole_cong:
@@ -3699,13 +3684,17 @@
 
 subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
 
-definition zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
+
+definition%important zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
   "zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
-                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n) \<and> h w \<noteq>0)))"
+                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n)
+                   \<and> h w \<noteq>0)))"
 
-definition zor_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where
-  "zor_poly f z = (SOME h. \<exists>r . r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
-                   \<and> (\<forall>w\<in>cball z r-{z}. f w =  h w * (w-z) powr (zorder f z) \<and> h w \<noteq>0))"
+definition%important zor_poly
+    ::"[complex \<Rightarrow> complex, complex] \<Rightarrow> complex \<Rightarrow> complex" where
+  "zor_poly f z = (SOME h. \<exists>r. r > 0 \<and> h holomorphic_on cball z r \<and> h z \<noteq> 0
+                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w - z) powr (zorder f z)
+                   \<and> h w \<noteq>0))"
 
 lemma zorder_exist:
   fixes f::"complex \<Rightarrow> complex" and z::complex
@@ -3803,7 +3792,6 @@
     by (auto simp add:dist_commute)
 qed
 
-
 lemma 
   fixes f g::"complex \<Rightarrow> complex" and z::complex
   assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"  
@@ -4881,8 +4869,8 @@
 
 theorem Rouche_theorem:
   fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
-  defines "fg\<equiv>(\<lambda>p. f p+ g p)"
-  defines "zeros_fg\<equiv>{p. fg p =0}" and "zeros_f\<equiv>{p. f p=0}"
+  defines "fg\<equiv>(\<lambda>p. f p + g p)"
+  defines "zeros_fg\<equiv>{p. fg p = 0}" and "zeros_f\<equiv>{p. f p = 0}"
   assumes
     "open s" and "connected s" and
     "finite zeros_fg" and