# HG changeset patch
# User Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
# Date 1535977732 -3600
# Node ID 725d5ed565635df79bee54d752a4d7667d1d65e5
# Parent  511d163ab623b0d419e2ed2bd22a5cf94fd5f9da
tagged 1 theory: Great_Picard

diff -r 511d163ab623 -r 725d5ed56563 src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Wed Aug 29 20:01:39 2018 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy	Mon Sep 03 13:28:52 2018 +0100
@@ -1,4 +1,4 @@
-section\<open>The Great Picard Theorem and its Applications\<close>
+section%important \<open>The Great Picard Theorem and its Applications\<close>
 
 text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close>
 
@@ -9,13 +9,13 @@
   
 subsection\<open>Schottky's theorem\<close>
 
-lemma Schottky_lemma0:
+lemma%important Schottky_lemma0:
   assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a \<in> S"
       and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
   obtains g where "g holomorphic_on S"
                   "norm(g a) \<le> 1 + norm(f a) / 3"
                   "\<And>z. z \<in> S \<Longrightarrow> f z = cos(of_real pi * g z)"
-proof -
+proof%unimportant -
   obtain g where holg: "g holomorphic_on S" and g: "norm(g a) \<le> pi + norm(f a)"
              and f_eq_cos: "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
     using contractible_imp_holomorphic_arccos_bounded [OF assms]
@@ -38,7 +38,7 @@
 qed
 
 
-lemma Schottky_lemma1:
+lemma%unimportant Schottky_lemma1:
   fixes n::nat
   assumes "0 < n"
   shows "0 < n + sqrt(real n ^ 2 - 1)"
@@ -54,7 +54,7 @@
 qed
 
 
-lemma Schottky_lemma2:
+lemma%unimportant Schottky_lemma2:
   fixes x::real
   assumes "0 \<le> x"
   obtains n where "0 < n" "\<bar>x - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
@@ -158,12 +158,12 @@
 qed
 
 
-lemma Schottky_lemma3:
+lemma%important Schottky_lemma3:
   fixes z::complex
   assumes "z \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
              \<union> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
   shows "cos(pi * cos(pi * z)) = 1 \<or> cos(pi * cos(pi * z)) = -1"
-proof -
+proof%unimportant -
   have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \<ge> 0" for x::real
     by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
   have 1: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) -
@@ -223,13 +223,13 @@
 qed
 
 
-theorem Schottky:
+theorem%important Schottky:
   assumes holf: "f holomorphic_on cball 0 1"
       and nof0: "norm(f 0) \<le> r"
       and not01: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not>(f z = 0 \<or> f z = 1)"
       and "0 < t" "t < 1" "norm z \<le> t"
     shows "norm(f z) \<le> exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))"
-proof -
+proof%unimportant -
   obtain h where holf: "h holomorphic_on cball 0 1"
              and nh0: "norm (h 0) \<le> 1 + norm(2 * f 0 - 1) / 3"
              and h:   "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 = cos(of_real pi * h z)"
@@ -374,14 +374,14 @@
 qed
 
   
-subsection\<open>The Little Picard Theorem\<close>
+subsection%important\<open>The Little Picard Theorem\<close>
 
-lemma Landau_Picard:
+lemma%important Landau_Picard:
   obtains R
     where "\<And>z. 0 < R z"
           "\<And>f. \<lbrakk>f holomorphic_on cball 0 (R(f 0));
                  \<And>z. norm z \<le> R(f 0) \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1\<rbrakk> \<Longrightarrow> norm(deriv f 0) < 1"
-proof -
+proof%unimportant -
   define R where "R \<equiv> \<lambda>z. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))"
   show ?thesis
   proof
@@ -436,10 +436,10 @@
   qed
 qed
 
-lemma little_Picard_01:
+lemma%important little_Picard_01:
   assumes holf: "f holomorphic_on UNIV" and f01: "\<And>z. f z \<noteq> 0 \<and> f z \<noteq> 1"
   obtains c where "f = (\<lambda>x. c)"
-proof -
+proof%unimportant -
   obtain R
     where Rpos: "\<And>z. 0 < R z"
       and R:    "\<And>h. \<lbrakk>h holomorphic_on cball 0 (R(h 0));
@@ -481,11 +481,11 @@
 qed
 
 
-theorem little_Picard:
+theorem%important little_Picard:
   assumes holf: "f holomorphic_on UNIV"
       and "a \<noteq> b" "range f \<inter> {a,b} = {}"
     obtains c where "f = (\<lambda>x. c)"
-proof -
+proof%unimportant -
   let ?g = "\<lambda>x. 1/(b - a)*(f x - b) + 1"
   obtain c where "?g = (\<lambda>x. c)"
   proof (rule little_Picard_01)
@@ -505,7 +505,7 @@
 
 text\<open>A couple of little applications of Little Picard\<close>
 
-lemma holomorphic_periodic_fixpoint:
+lemma%unimportant holomorphic_periodic_fixpoint:
   assumes holf: "f holomorphic_on UNIV"
       and "p \<noteq> 0" and per: "\<And>z. f(z + p) = f z"
   obtains x where "f x = x"
@@ -527,7 +527,7 @@
 qed
 
 
-lemma holomorphic_involution_point:
+lemma%unimportant holomorphic_involution_point:
   assumes holfU: "f holomorphic_on UNIV" and non: "\<And>a. f \<noteq> (\<lambda>x. a + x)"
   obtains x where "f(f x) = x"
 proof -
@@ -614,9 +614,9 @@
 qed
 
 
-subsection\<open>The Arzelà--Ascoli theorem\<close>
+subsection%important\<open>The Arzelà--Ascoli theorem\<close>
 
-lemma subsequence_diagonalization_lemma:
+lemma%unimportant subsequence_diagonalization_lemma:
   fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
   assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)"
       and P_P:  "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
@@ -660,7 +660,7 @@
   qed
 qed
 
-lemma function_convergent_subsequence:
+lemma%unimportant function_convergent_subsequence:
   fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
    obtains k where "strict_mono (k::nat\<Rightarrow>nat)" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
@@ -698,7 +698,7 @@
 qed
 
 
-theorem Arzela_Ascoli:
+theorem%important Arzela_Ascoli:
   fixes \<F> :: "[nat,'a::euclidean_space] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   assumes "compact S"
       and M: "\<And>n x. x \<in> S \<Longrightarrow> norm(\<F> n x) \<le> M"
@@ -707,7 +707,7 @@
                  \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n y. y \<in> S \<and> norm(x - y) < d \<longrightarrow> norm(\<F> n x - \<F> n y) < e)"
   obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)"
                     "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(k n) x - g x) < e"
-proof -
+proof%unimportant -
   have UEQ: "\<And>e. 0 < e \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e)"
     apply (rule compact_uniformly_equicontinuous [OF \<open>compact S\<close>, of "range \<F>"])
     using equicont by (force simp: dist_commute dist_norm)+
@@ -788,14 +788,14 @@
 
 
 
-subsubsection\<open>Montel's theorem\<close>
+subsubsection%important\<open>Montel's theorem\<close>
 
 text\<open>a sequence of holomorphic functions uniformly bounded
 on compact subsets of an open set S has a subsequence that converges to a
 holomorphic function, and converges \emph{uniformly} on compact subsets of S.\<close>
 
 
-theorem Montel:
+theorem%important Montel:
   fixes \<F> :: "[nat,complex] \<Rightarrow> complex"
   assumes "open S"
       and \<H>: "\<And>h. h \<in> \<H> \<Longrightarrow> h holomorphic_on S"
@@ -805,7 +805,7 @@
     where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)"
           "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
           "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"        
-proof -
+proof%unimportant -
   obtain K where comK: "\<And>n. compact(K n)" and KS: "\<And>n::nat. K n \<subseteq> S"
              and subK: "\<And>X. \<lbrakk>compact X; X \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X \<subseteq> K n"
     using open_Union_compact_subsets [OF \<open>open S\<close>] by metis
@@ -993,9 +993,9 @@
 
 
 
-subsection\<open>Some simple but useful cases of Hurwitz's theorem\<close>
+subsection%important\<open>Some simple but useful cases of Hurwitz's theorem\<close>
 
-proposition Hurwitz_no_zeros:
+proposition%important Hurwitz_no_zeros:
   assumes S: "open S" "connected S"
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
@@ -1004,7 +1004,7 @@
       and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
       and "z0 \<in> S"
       shows "g z0 \<noteq> 0"
-proof
+proof%unimportant
   assume g0: "g z0 = 0"
   obtain h r m
     where "0 < m" "0 < r" and subS: "ball z0 r \<subseteq> S"
@@ -1159,7 +1159,7 @@
   ultimately show False using \<open>0 < m\<close> by auto
 qed
 
-corollary Hurwitz_injective:
+corollary%important Hurwitz_injective:
   assumes S: "open S" "connected S"
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
@@ -1167,7 +1167,7 @@
       and nonconst: "~ g constant_on S"
       and inj: "\<And>n. inj_on (\<F> n) S"
     shows "inj_on g S"
-proof -
+proof%unimportant -
   have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2
   proof -
     obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2"
@@ -1229,15 +1229,15 @@
 
 
 
-subsection\<open>The Great Picard theorem\<close>
+subsection%important\<open>The Great Picard theorem\<close>
 
-lemma GPicard1:
+lemma%important GPicard1:
   assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X"
       and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
       and X01:  "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
       and r:    "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> r"
   obtains B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-proof -
+proof%unimportant -
   obtain e where "e > 0" and e: "cball w e \<subseteq> S"
     using assms open_contains_cball_eq by blast
   show ?thesis
@@ -1277,20 +1277,20 @@
   qed (use \<open>e > 0\<close> in auto)
 qed 
 
-lemma GPicard2:
+lemma%important GPicard2:
   assumes "S \<subseteq> T" "connected T" "S \<noteq> {}" "open S" "\<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S"
     shows "S = T"
-  by (metis assms open_subset connected_clopen closedin_limpt)
+  by%unimportant (metis assms open_subset connected_clopen closedin_limpt)
 
     
-lemma GPicard3:
+lemma%important GPicard3:
   assumes S: "open S" "connected S" "w \<in> S" and "Y \<subseteq> X"
       and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
       and X01:  "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
       and no_hw_le1: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> 1"
       and "compact K" "K \<subseteq> S"
   obtains B where "\<And>h z. \<lbrakk>h \<in> Y; z \<in> K\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-proof -
+proof%unimportant -
   define U where "U \<equiv> {z \<in> S. \<exists>B Z. 0 < B \<and> open Z \<and> z \<in> Z \<and> Z \<subseteq> S \<and>
                                (\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B)}"
   then have "U \<subseteq> S" by blast
@@ -1432,11 +1432,11 @@
 qed
 
 
-lemma GPicard4:
+lemma%important GPicard4:
   assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" 
       and AE: "\<And>e. \<lbrakk>0 < e; e < k\<rbrakk> \<Longrightarrow> \<exists>d. 0 < d \<and> d < e \<and> (\<forall>z \<in> sphere 0 d. norm(f z) \<le> B)"
   obtains \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> norm(f z) \<le> B"
-proof -
+proof%unimportant -
   obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k/2" and \<epsilon>: "\<And>z. norm z = \<epsilon> \<Longrightarrow> norm(f z) \<le> B"
     using AE [of "k/2"] \<open>0 < k\<close> by auto
   show ?thesis
@@ -1471,13 +1471,13 @@
 qed
   
 
-lemma GPicard5:
+lemma%important GPicard5:
   assumes holf: "f holomorphic_on (ball 0 1 - {0})"
       and f01:  "\<And>z. z \<in> ball 0 1 - {0} \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1"
   obtains e B where "0 < e" "e < 1" "0 < B" 
                     "(\<forall>z \<in> ball 0 e - {0}. norm(f z) \<le> B) \<or>
                      (\<forall>z \<in> ball 0 e - {0}. norm(f z) \<ge> B)"
-proof -
+proof%unimportant -
   have [simp]: "1 + of_nat n \<noteq> (0::complex)" for n
     using of_nat_eq_0_iff by fastforce
   have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n
@@ -1614,13 +1614,13 @@
 qed
 
   
-lemma GPicard6:
+lemma%important GPicard6:
   assumes "open M" "z \<in> M" "a \<noteq> 0" and holf: "f holomorphic_on (M - {z})"
       and f0a: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> 0 \<and> f w \<noteq> a"
   obtains r where "0 < r" "ball z r \<subseteq> M" 
                   "bounded(f ` (ball z r - {z})) \<or>
                    bounded((inverse \<circ> f) ` (ball z r - {z}))"
-proof -
+proof%unimportant -
   obtain r where "0 < r" and r: "ball z r \<subseteq> M"
     using assms openE by blast 
   let ?g = "\<lambda>w. f (z + of_real r * w) / a"
@@ -1669,11 +1669,11 @@
 qed
   
 
-theorem great_Picard:
+theorem%important great_Picard:
   assumes "open M" "z \<in> M" "a \<noteq> b" and holf: "f holomorphic_on (M - {z})"
       and fab: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> a \<and> f w \<noteq> b"
   obtains l where "(f \<longlongrightarrow> l) (at z) \<or> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
-proof -
+proof%unimportant -
   obtain r where "0 < r" and zrM: "ball z r \<subseteq> M" 
              and r: "bounded((\<lambda>z. f z - a) ` (ball z r - {z})) \<or>
                      bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))"
@@ -1776,19 +1776,19 @@
 qed
 
 
-corollary great_Picard_alt:
+corollary%important great_Picard_alt:
   assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
     and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   obtains a where "- {a} \<subseteq> f ` (M - {z})"
-  apply (simp add: subset_iff image_iff)
-  by (metis great_Picard [OF M _ holf] non)
+  apply%unimportant (simp add: subset_iff image_iff)
+  by%unimportant (metis great_Picard [OF M _ holf] non)
     
 
-corollary great_Picard_infinite:
+corollary%important great_Picard_infinite:
   assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
     and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   obtains a where "\<And>w. w \<noteq> a \<Longrightarrow> infinite {x. x \<in> M - {z} \<and> f x = w}"
-proof -
+proof%unimportant -
   have False if "a \<noteq> b" and ab: "finite {x. x \<in> M - {z} \<and> f x = a}" "finite {x. x \<in> M - {z} \<and> f x = b}" for a b
   proof -
     have finab: "finite {x. x \<in> M - {z} \<and> f x \<in> {a,b}}"
@@ -1830,11 +1830,11 @@
     by meson
 qed
 
-corollary Casorati_Weierstrass:
+corollary%important Casorati_Weierstrass:
   assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})"
       and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   shows "closure(f ` (M - {z})) = UNIV"
-proof -
+proof%unimportant -
   obtain a where a: "- {a} \<subseteq> f ` (M - {z})"
     using great_Picard_alt [OF assms] .
   have "UNIV = closure(- {a})"