--- a/src/HOL/Analysis/Great_Picard.thy Mon Sep 03 15:04:04 2018 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy Mon Sep 03 15:35:38 2018 +0200
@@ -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})"