src/HOL/Analysis/Great_Picard.thy

 
 begin
   
 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]
     by blast
   show ?thesis

       by (simp add: f_eq_cos)
   qed
 qed
 
 
-lemma Schottky_lemma1:
+lemma%unimportant Schottky_lemma1:
   fixes n::nat
   assumes "0 < n"
   shows "0 < n + sqrt(real n ^ 2 - 1)"
 proof -
   have "(n-1)^2 \<le> n^2 - 1"

   then show ?thesis
     using assms by linarith
 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"
 proof -
   obtain n0::nat where "0 < n0" "ln(n0 + sqrt(real n0 ^ 2 - 1)) / pi \<le> x"

       by (rule_tac n="Suc n" in that) (auto simp: b_def \<open>0 < n\<close>)
   qed
 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) -
                  (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) +
             inverse

   then show ?thesis
     using power2_eq_1_iff by auto
 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)"
   proof (rule Schottky_lemma0 [of "\<lambda>z. 2 * f z - 1" "cball 0 1" 0])
     show "(\<lambda>z. 2 * f z - 1) holomorphic_on cball 0 1"

 qed
 
   
 subsection%important\<open>The Little Picard Theorem\<close>
 
-proposition 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
     show Rpos: "\<And>z. 0 < R z"
       by (auto simp: R_def)

         using cmod_g'_le Rpos [of "f 0"]  by (simp add: g_eq norm_mult)
     qed
   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));
                       \<And>z. norm z \<le> R(h 0) \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1\<rbrakk> \<Longrightarrow> norm(deriv h 0) < 1"
     using Landau_Picard by metis

       using norm_let1 w by (simp add: DERIV_imp_deriv)
   qed
 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)
     show "?g holomorphic_on UNIV"
       by (intro holomorphic_intros holf)

 qed
 
 
 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"
 proof -
   have False if non: "\<And>x. f x \<noteq> x"

   then show ?thesis
     using that by blast
 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 -
   { assume non_ff [simp]: "\<And>x. f(f x) \<noteq> x"
     then have non_fp [simp]: "f z \<noteq> z" for z

 qed
 
 
 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.
                    \<lbrakk>P i (r \<circ> k1); \<And>j. N \<le> j \<Longrightarrow> \<exists>j'. j \<le> j' \<and> k2 j = k1 j'\<rbrakk> \<Longrightarrow> P i (r \<circ> k2)"
    obtains k where "strict_mono (k :: nat \<Rightarrow> nat)" "\<And>i. P i (r \<circ> k)"

     then show "P i (r \<circ> (\<lambda>n. rr n n))" for i
       by (meson P_rr P_P)
   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"
 proof (cases "S = {}")
   case True

   with \<sigma> that show ?thesis
     by force
 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"
       and equicont:
           "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>
                  \<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)+
   have "continuous_on S g"
        if "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(r n) x - g x) < e"

 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"
       and bounded: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K. norm(h z) \<le> B"
       and rng_f: "range \<F> \<subseteq> \<H>"
   obtains g r
     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
   then have "\<And>i. \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K i. norm(h z) \<le> B"
     by (simp add: bounded)

 
 
 
 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"
       and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
       and nonconst: "\<not> g constant_on S"
       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"
       and holh: "h holomorphic_on ball z0 r"
       and geq:  "\<And>w. w \<in> ball z0 r \<Longrightarrow> g w = (w - z0)^m * h w"

       done
   qed
   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"
       and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
       and nonconst: "\<not> 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"
       using constant_on_def nonconst by blast
     have "(\<lambda>z. g z - g z1) holomorphic_on S"

 
 
 
 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
   proof
     show "0 < exp(pi * exp(pi * (2 + 2 * r + 12)))"

       show ?thesis by simp
     qed
   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
   have "U = S"
   proof (rule GPicard2 [OF \<open>U \<subseteq> S\<close> \<open>connected S\<close>])

   qed
   with that show ?thesis by metis
 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
   proof
     show "\<epsilon> < k"

     qed
   qed (use \<open>0 < \<epsilon>\<close> in auto)
 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
     by (metis norm_of_nat of_nat_Suc)
   have *: "(\<lambda>x::complex. x / of_nat (Suc n)) ` (ball 0 1 - {0}) \<subseteq> ball 0 1 - {0}" for n

       using \<epsilon> by auto 
   qed
 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"
   obtain e B where "0 < e" "e < 1" "0 < B" 
     and B: "(\<forall>z \<in> ball 0 e - {0}. norm(?g z) \<le> B) \<or> (\<forall>z \<in> ball 0 e - {0}. norm(?g z) \<ge> B)"

     qed
   qed
 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}))"
   proof (rule GPicard6 [OF \<open>open M\<close> \<open>z \<in> M\<close>])
     show "b - a \<noteq> 0"

     qed 
   qed
 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%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}}"
       using finite_UnI [OF ab]  unfolding mem_Collect_eq insert_iff empty_iff
       by (simp add: conj_disj_distribL)

   qed
   with that show thesis
     by meson
 qed
 
-theorem 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})"
     by (simp add: closure_interior)
   also have "... \<subseteq> closure(f ` (M - {z}))"