--- a/src/HOL/Analysis/Conformal_Mappings.thy Sun Sep 17 21:04:02 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Sep 19 16:37:19 2017 +0100
@@ -739,7 +739,7 @@
lemma holomorphic_factor_zero_nonconstant:
assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
and "\<xi> \<in> S" "f \<xi> = 0"
- and nonconst: "\<And>c. \<exists>z \<in> S. f z \<noteq> c"
+ and nonconst: "~ f constant_on S"
obtains g r n
where "0 < n" "0 < r" "ball \<xi> r \<subseteq> S"
"g holomorphic_on ball \<xi> r"
@@ -747,7 +747,7 @@
"\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
proof (cases "\<forall>n>0. (deriv ^^ n) f \<xi> = 0")
case True then show ?thesis
- using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by auto
+ using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by (simp add: constant_on_def)
next
case False
then obtain n0 where "n0 > 0" and n0: "(deriv ^^ n0) f \<xi> \<noteq> 0" by blast
@@ -3074,18 +3074,19 @@
lemma holomorphic_factor_zero_Ex1:
assumes "open s" "connected s" "z \<in> s" and
- holo:"f holomorphic_on s"
- and "f z = 0" and "\<exists>w\<in>s. f w \<noteq> 0"
+ holf: "f holomorphic_on s"
+ and f: "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0"
shows "\<exists>!n. \<exists>g r. 0 < n \<and> 0 < r \<and>
g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0)"
proof (rule ex_ex1I)
- obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and
+ have "\<not> f constant_on s"
+ by (metis \<open>z\<in>s\<close> constant_on_def f)
+ then obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and
g:"g holomorphic_on ball z r"
"\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w"
"\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
- using holomorphic_factor_zero_nonconstant[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
- by (metis assms(3) assms(5) assms(6))
+ by (blast intro: holomorphic_factor_zero_nonconstant[OF holf \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>])
define r' where "r' \<equiv> r/2"
have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'"
--- a/src/HOL/Analysis/Great_Picard.thy Sun Sep 17 21:04:02 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy Tue Sep 19 16:37:19 2017 +0100
@@ -1000,7 +1000,7 @@
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: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
+ and nonconst: "~ 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"
@@ -1164,14 +1164,14 @@
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: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
+ and nonconst: "~ g constant_on S"
and inj: "\<And>n. inj_on (\<F> n) S"
shows "inj_on g S"
proof -
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 nonconst by blast
+ using constant_on_def nonconst by blast
have "(\<lambda>z. g z - g z1) holomorphic_on S"
by (intro holomorphic_intros holg)
then obtain r where "0 < r" "ball z2 r \<subseteq> S" "\<And>z. dist z2 z < r \<and> z \<noteq> z2 \<Longrightarrow> g z \<noteq> g z1"
@@ -1214,7 +1214,8 @@
show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
by simp
qed
- show "\<And>c. \<exists>z\<in>S - {z1}. g z - g z1 \<noteq> c"
+ show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}"
+ unfolding constant_on_def
by (metis Diff_iff \<open>z0 \<in> S\<close> empty_iff insert_iff right_minus_eq z0 z12)
show "\<And>n z. z \<in> S - {z1} \<Longrightarrow> \<F> n z - \<F> n z1 \<noteq> 0"
by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 \<open>z1 \<in> S\<close>)
@@ -1360,8 +1361,9 @@
using \<open>Z \<subseteq> S\<close> e hol\<G> by force
show "\<And>n z. z \<in> ball v e \<Longrightarrow> (\<G> \<circ> j) n z \<noteq> 0"
using \<G>not0 \<open>Z \<subseteq> S\<close> e by fastforce
- show "\<exists>z\<in>ball v e. h z \<noteq> c" for c
- proof -
+ show "\<not> h constant_on ball v e"
+ proof (clarsimp simp: constant_on_def)
+ fix c
have False if "\<And>z. dist v z < e \<Longrightarrow> h z = c"
proof -
have "h v = c"
@@ -1389,7 +1391,7 @@
show False
using \<open>C < cmod (\<F> (j n) y)\<close> le_C not_less by blast
qed
- then show ?thesis by force
+ then show "\<exists>x\<in>ball v e. h x \<noteq> c" by force
qed
show "h holomorphic_on ball v e"
by (simp add: holh)
@@ -1828,7 +1830,6 @@
by meson
qed
-
corollary 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)"