--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Sun Jan 19 18:18:07 2025 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Jan 22 22:22:27 2025 +0000
@@ -4,9 +4,9 @@
subsection \<open>Non-essential singular points\<close>
-definition\<^marker>\<open>tag important\<close> 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)"
+definition\<^marker>\<open>tag important\<close>
+ 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:
assumes "eventually (\<lambda>x. f x = g x) (at a)" "a=b"
@@ -24,10 +24,10 @@
by (metis add_diff_cancel_right' filterlim_shift_iff is_pole_def)
lemma is_pole_tendsto:
- fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
+ fixes f:: "('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
unfolding is_pole_def
- by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+ by (auto simp add: filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
lemma is_pole_shift_0:
fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)"
@@ -46,9 +46,9 @@
lemma is_pole_inverse_holomorphic:
assumes "open s"
- and f_holo:"f holomorphic_on (s-{z})"
- and pole:"is_pole f z"
- and non_z:"\<forall>x\<in>s-{z}. f x\<noteq>0"
+ and f_holo: "f holomorphic_on (s-{z})"
+ and pole: "is_pole f z"
+ and non_z: "\<forall>x\<in>s-{z}. f x\<noteq>0"
shows "(\<lambda>x. if x=z then 0 else inverse (f x)) holomorphic_on s"
proof -
define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
@@ -56,14 +56,14 @@
by (simp add: g_def cong: LIM_cong)
moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto
hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
- by (auto elim!:continuous_on_inverse simp add:non_z)
+ by (auto elim!:continuous_on_inverse simp add: non_z)
hence "continuous_on (s-{z}) g" unfolding g_def
using continuous_on_eq by fastforce
ultimately have "continuous_on s g" using open_delete[OF \<open>open s\<close>] \<open>open s\<close>
- by (auto simp add:continuous_on_eq_continuous_at)
+ by (auto simp add: continuous_on_eq_continuous_at)
moreover have "(inverse o f) holomorphic_on (s-{z})"
unfolding comp_def using f_holo
- by (auto elim!:holomorphic_on_inverse simp add:non_z)
+ by (auto elim!:holomorphic_on_inverse simp add: non_z)
hence "g holomorphic_on (s-{z})"
using g_def holomorphic_transform by force
ultimately show ?thesis unfolding g_def using \<open>open s\<close>
@@ -125,15 +125,15 @@
lemma is_pole_basic:
assumes "f holomorphic_on A" "open A" "z \<in> A" "f z \<noteq> 0" "n > 0"
- shows "is_pole (\<lambda>w. f w / (w - z) ^ n) z"
+ shows "is_pole (\<lambda>w. f w / (w-z) ^ n) z"
proof (rule is_pole_divide)
have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact
with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at)
- have "filterlim (\<lambda>w. (w - z) ^ n) (nhds 0) (at z)"
+ have "filterlim (\<lambda>w. (w-z) ^ n) (nhds 0) (at z)"
using assms by (auto intro!: tendsto_eq_intros)
- thus "filterlim (\<lambda>w. (w - z) ^ n) (at 0) (at z)"
+ thus "filterlim (\<lambda>w. (w-z) ^ n) (at 0) (at z)"
by (intro filterlim_atI tendsto_eq_intros)
- (insert assms, auto simp: eventually_at_filter)
+ (use assms in \<open>auto simp: eventually_at_filter\<close>)
qed fact+
lemma is_pole_basic':
@@ -161,7 +161,7 @@
then have "filterlim (\<lambda>x. f x + c) at_infinity (at z)"
unfolding is_pole_def .
moreover have "((\<lambda>_. -c) \<longlongrightarrow> -c) (at z)" by auto
- ultimately have " LIM x (at z). f x :> at_infinity"
+ ultimately have "LIM x (at z). f x :> at_infinity"
using tendsto_add_filterlim_at_infinity'[of "(\<lambda>x. f x + c)"
"at z" "(\<lambda>_. - c)" "-c"]
by auto
@@ -237,11 +237,11 @@
unfolding islimpt_sequential by blast
then have "(f \<circ> g) \<longlonglongrightarrow> c"
by (simp add: tendsto_eventually)
- moreover have *: "filterlim g (at z) sequentially"
+ moreover have "filterlim g (at z) sequentially"
using g by (auto simp: filterlim_at)
- have "filterlim (f \<circ> g) at_infinity sequentially"
- unfolding o_def by (rule filterlim_compose [OF _ *])
- (use \<open>is_pole f z\<close> in \<open>simp add: is_pole_def\<close>)
+ then have "filterlim (f \<circ> g) at_infinity sequentially"
+ unfolding o_def
+ using \<open>is_pole f z\<close> filterlim_compose is_pole_def by blast
ultimately show False
using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
qed
@@ -250,10 +250,10 @@
\<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close>
can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close>
(i.e. the singularity is either removable or a pole).\<close>
-definition not_essential::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
+definition not_essential:: "[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
"not_essential f z = (\<exists>x. f\<midarrow>z\<rightarrow>x \<or> is_pole f z)"
-definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
+definition isolated_singularity_at:: "[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
"isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})"
lemma not_essential_cong:
@@ -322,7 +322,7 @@
have "f \<midarrow>x\<rightarrow> c"
by fact
also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y)"
- by (intro filterlim_cong) (auto simp: eventually_at_filter)
+ by (simp add: LIM_equal)
finally show ?thesis
by (meson Lim_at_imp_Lim_at_within)
qed
@@ -332,7 +332,7 @@
using assms(1) holomorphic_transform by fastforce
}
ultimately show ?thesis
- by (rule no_isolated_singularity) (use assms in auto)
+ using assms by (simp add: no_isolated_singularity)
qed
lemma removable_singularity':
@@ -354,18 +354,18 @@
named_theorems singularity_intros "introduction rules for singularities"
lemma holomorphic_factor_unique:
- fixes f::"complex \<Rightarrow> complex" and z::complex and r::real and m n::int
+ fixes f:: "complex \<Rightarrow> complex" and z::complex and r::real and m n::int
assumes "r>0" "g z\<noteq>0" "h z\<noteq>0"
- and asm:"\<forall>w\<in>ball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0 \<and> f w = h w * (w - z) powi m \<and> h w\<noteq>0"
- and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r"
+ and asm: "\<forall>w\<in>ball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0 \<and> f w = h w * (w-z) powi m \<and> h w\<noteq>0"
+ and g_holo: "g holomorphic_on ball z r" and h_holo: "h holomorphic_on ball z r"
shows "n=m"
proof -
- have [simp]:"at z within ball z r \<noteq> bot" using \<open>r>0\<close>
- by (auto simp add:at_within_ball_bot_iff)
+ have [simp]: "at z within ball z r \<noteq> bot" using \<open>r>0\<close>
+ by (auto simp add: at_within_ball_bot_iff)
have False when "n>m"
proof -
have "(h \<longlongrightarrow> 0) (at z within ball z r)"
- proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powi (n - m) * g w"])
+ proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w-z) powi (n - m) * g w"])
have "\<forall>w\<in>ball z r-{z}. h w = (w-z)powi(n-m) * g w"
using \<open>n>m\<close> asm \<open>r>0\<close> by (simp add: field_simps power_int_diff) force
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
@@ -386,16 +386,16 @@
qed
moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)"
using holomorphic_on_imp_continuous_on[OF h_holo]
- by (auto simp add:continuous_on_def \<open>r>0\<close>)
+ by (auto simp add: continuous_on_def \<open>r>0\<close>)
ultimately have "h z=0" by (auto intro!: tendsto_unique)
thus False using \<open>h z\<noteq>0\<close> by auto
qed
moreover have False when "m>n"
proof -
have "(g \<longlongrightarrow> 0) (at z within ball z r)"
- proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powi (m - n) * h w"])
+ proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w-z) powi (m - n) * h w"])
have "\<forall>w\<in>ball z r -{z}. g w = (w-z) powi (m-n) * h w" using \<open>m>n\<close> asm
- by (simp add:field_simps power_int_diff) force
+ by (simp add: field_simps power_int_diff) force
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) powi (m - n) * h x' = g x'" for x' by auto
next
@@ -414,7 +414,7 @@
qed
moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)"
using holomorphic_on_imp_continuous_on[OF g_holo]
- by (auto simp add:continuous_on_def \<open>r>0\<close>)
+ by (auto simp add: continuous_on_def \<open>r>0\<close>)
ultimately have "g z=0" by (auto intro!: tendsto_unique)
thus False using \<open>g z\<noteq>0\<close> by auto
qed
@@ -422,19 +422,19 @@
qed
lemma holomorphic_factor_puncture:
- assumes f_iso:"isolated_singularity_at f z"
+ assumes f_iso: "isolated_singularity_at f z"
and "not_essential f z" \<comment> \<open>\<^term>\<open>f\<close> has either a removable singularity or a pole at \<^term>\<open>z\<close>\<close>
- and non_zero:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" \<comment> \<open>\<^term>\<open>f\<close> will not be constantly zero in a neighbour of \<^term>\<open>z\<close>\<close>
+ and non_zero: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0" \<comment> \<open>\<^term>\<open>f\<close> will not be constantly zero in a neighbour of \<^term>\<open>z\<close>\<close>
shows "\<exists>!n::int. \<exists>g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0
\<and> (\<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0)"
proof -
define P where "P = (\<lambda>f n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0))"
- have imp_unique:"\<exists>!n::int. \<exists>g r. P f n g r" when "\<exists>n g r. P f n g r"
+ have imp_unique: "\<exists>!n::int. \<exists>g r. P f n g r" when "\<exists>n g r. P f n g r"
proof (rule ex_ex1I[OF that])
fix n1 n2 :: int
- assume g1_asm:"\<exists>g1 r1. P f n1 g1 r1" and g2_asm:"\<exists>g2 r2. P f n2 g2 r2"
- define fac where "fac \<equiv> \<lambda>n g r. \<forall>w\<in>cball z r-{z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0"
+ assume g1_asm: "\<exists>g1 r1. P f n1 g1 r1" and g2_asm: "\<exists>g2 r2. P f n2 g2 r2"
+ define fac where "fac \<equiv> \<lambda>n g r. \<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0"
obtain g1 r1 where "0 < r1" and g1_holo: "g1 holomorphic_on cball z r1" and "g1 z\<noteq>0"
and "fac n1 g1 r1" using g1_asm unfolding P_def fac_def by auto
obtain g2 r2 where "0 < r2" and g2_holo: "g2 holomorphic_on cball z r2" and "g2 z\<noteq>0"
@@ -442,16 +442,16 @@
define r where "r \<equiv> min r1 r2"
have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
moreover have "\<forall>w\<in>ball z r-{z}. f w = g1 w * (w-z) powi n1 \<and> g1 w\<noteq>0
- \<and> f w = g2 w * (w - z) powi n2 \<and> g2 w\<noteq>0"
+ \<and> f w = g2 w * (w-z) powi n2 \<and> g2 w\<noteq>0"
using \<open>fac n1 g1 r1\<close> \<open>fac n2 g2 r2\<close> unfolding fac_def r_def
by fastforce
ultimately show "n1=n2"
using g1_holo g2_holo \<open>g1 z\<noteq>0\<close> \<open>g2 z\<noteq>0\<close>
apply (elim holomorphic_factor_unique)
- by (auto simp add:r_def)
+ by (auto simp add: r_def)
qed
- have P_exist:"\<exists> n g r. P h n g r" when
+ have P_exist: "\<exists> n g r. P h n g r" when
"\<exists>z'. (h \<longlongrightarrow> z') (at z)" "isolated_singularity_at h z" "\<exists>\<^sub>Fw in (at z). h w\<noteq>0"
for h
proof -
@@ -474,16 +474,16 @@
by (metis \<open>0 < r\<close> centre_in_ball dist_commute mem_ball that)
moreover note \<open>h' holomorphic_on ball z r\<close>
ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 \<subseteq> ball z r" and
- g:"g holomorphic_on ball z r1"
- "\<And>w. w \<in> ball z r1 \<Longrightarrow> h' w = (w - z) ^ n * g w"
+ g: "g holomorphic_on ball z r1"
+ "\<And>w. w \<in> ball z r1 \<Longrightarrow> h' w = (w-z) ^ n * g w"
"\<And>w. w \<in> ball z r1 \<Longrightarrow> g w \<noteq> 0"
using holomorphic_factor_zero_nonconstant[of _ "ball z r" z thesis,simplified,
OF \<open>h' holomorphic_on ball z r\<close> \<open>r>0\<close> \<open>h' z=0\<close> \<open>\<not> h' constant_on ball z r\<close>]
- by (auto simp add:dist_commute)
+ by (auto simp add: dist_commute)
define rr where "rr=r1/2"
have "P h' n g rr"
unfolding P_def rr_def
- using \<open>n>0\<close> \<open>r1>0\<close> g by (auto simp add:powr_nat)
+ using \<open>n>0\<close> \<open>r1>0\<close> g by (auto simp add: powr_nat)
then have "P h n g rr"
unfolding h'_def P_def by auto
then show ?thesis unfolding P_def by blast
@@ -495,7 +495,7 @@
proof -
have "isCont h' z" "h' z\<noteq>0"
by (auto simp add: Lim_cong_within \<open>h \<midarrow>z\<rightarrow> z'\<close> \<open>z'\<noteq>0\<close> continuous_at h'_def)
- then obtain r2 where r2:"r2>0" "\<forall>x\<in>ball z r2. h' x\<noteq>0"
+ then obtain r2 where r2: "r2>0" "\<forall>x\<in>ball z r2. h' x\<noteq>0"
using continuous_at_avoid[of z h' 0 ] unfolding ball_def by auto
define r1 where "r1=min r2 r / 2"
have "0 < r1" "cball z r1 \<subseteq> ball z r"
@@ -516,14 +516,14 @@
using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
moreover have ?thesis when "is_pole f z"
proof (rule imp_unique[unfolded P_def])
- obtain e where [simp]:"e>0" and e_holo:"f holomorphic_on ball z e - {z}" and e_nz: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0"
+ obtain e where [simp]: "e>0" and e_holo: "f holomorphic_on ball z e - {z}" and e_nz: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0"
proof -
have "\<forall>\<^sub>F z in at z. f z \<noteq> 0"
using \<open>is_pole f z\<close> filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def
by auto
- then obtain e1 where e1:"e1>0" "\<forall>x\<in>ball z e1-{z}. f x\<noteq>0"
- using that eventually_at[of "\<lambda>x. f x\<noteq>0" z UNIV,simplified] by (auto simp add:dist_commute)
- obtain e2 where e2:"e2>0" "f holomorphic_on ball z e2 - {z}"
+ then obtain e1 where e1: "e1>0" "\<forall>x\<in>ball z e1-{z}. f x\<noteq>0"
+ using that eventually_at[of "\<lambda>x. f x\<noteq>0" z UNIV,simplified] by (auto simp add: dist_commute)
+ obtain e2 where e2: "e2>0" "f holomorphic_on ball z e2 - {z}"
using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by auto
show ?thesis
using e1 e2 by (force intro: that[of "min e1 e2"])
@@ -545,22 +545,23 @@
qed
then obtain n g r
where "0 < r" and
- g_holo:"g holomorphic_on cball z r" and "g z\<noteq>0" and
- g_fac:"(\<forall>w\<in>cball z r-{z}. h w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ g_holo: "g holomorphic_on cball z r" and "g z\<noteq>0" and
+ g_fac: "(\<forall>w\<in>cball z r-{z}. h w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
unfolding P_def by auto
have "P f (-n) (inverse o g) r"
proof -
- have "f w = inverse (g w) * (w - z) powi (- n)" when "w\<in>cball z r - {z}" for w
+ have "f w = inverse (g w) * (w-z) powi (- n)" when "w\<in>cball z r - {z}" for w
by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib power_int_minus that)
then show ?thesis
unfolding P_def comp_def
- using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro:holomorphic_intros)
+ using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro: holomorphic_intros)
qed
then show "\<exists>x g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z \<noteq> 0
- \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi x \<and> g w \<noteq> 0)"
+ \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi x \<and> g w \<noteq> 0)"
unfolding P_def by blast
qed
- ultimately show ?thesis using \<open>not_essential f z\<close> unfolding not_essential_def by presburger
+ ultimately show ?thesis
+ using \<open>not_essential f z\<close> unfolding not_essential_def by presburger
qed
lemma not_essential_transform:
@@ -631,9 +632,9 @@
proof -
obtain r1 where "r1>0" "f analytic_on ball z r1 - {z}"
using assms(1) unfolding isolated_singularity_at_def by auto
- then have r1:"f holomorphic_on ball z r1 - {z}"
+ then have r1: "f holomorphic_on ball z r1 - {z}"
using analytic_on_open[of "ball z r1-{z}" f] by blast
- obtain r2 where "r2>0" and r2:"\<forall>w. w \<noteq> z \<and> dist w z < r2 \<longrightarrow> f w \<noteq> 0"
+ obtain r2 where "r2>0" and r2: "\<forall>w. w \<noteq> z \<and> dist w z < r2 \<longrightarrow> f w \<noteq> 0"
using assms(2) unfolding eventually_at by auto
define r3 where "r3=min r1 r2"
have "(\<lambda>w. (f w) powi n) holomorphic_on ball z r3 - {z}"
@@ -644,20 +645,21 @@
qed
lemma non_zero_neighbour:
- assumes f_iso:"isolated_singularity_at f z"
- and f_ness:"not_essential f z"
- and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+ assumes f_iso: "isolated_singularity_at f z"
+ and f_ness: "not_essential f z"
+ and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
shows "\<forall>\<^sub>F w in (at z). f w\<noteq>0"
proof -
- obtain fn fp fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
- and fr: "fp holomorphic_on cball z fr"
- "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
- using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto
+ obtain fn fp fr
+ where [simp]: "fp z \<noteq> 0" and "fr > 0"
+ and fr: "fp holomorphic_on cball z fr"
+ "\<And>w. w \<in> cball z fr - {z} \<Longrightarrow> f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
+ using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
have "f w \<noteq> 0" when " w \<noteq> z" "dist w z < fr" for w
proof -
- have "f w = fp w * (w - z) powi fn" "fp w \<noteq> 0"
- using fr(2)[rule_format, of w] using that by (auto simp add:dist_commute)
- moreover have "(w - z) powi fn \<noteq>0"
+ have "f w = fp w * (w-z) powi fn" "fp w \<noteq> 0"
+ using fr that by (auto simp add: dist_commute)
+ moreover have "(w-z) powi fn \<noteq>0"
unfolding powr_eq_0_iff using \<open>w\<noteq>z\<close> by auto
ultimately show ?thesis by auto
qed
@@ -682,18 +684,18 @@
by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
next
case False
- obtain r1 where r1:"r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 0"
- using continuous_at_avoid[of z f, OF _ False] assms(2,4) continuous_on_eq_continuous_at
+ obtain r1 where r1: "r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 0"
+ using continuous_at_avoid[of z f, OF _ False] assms continuous_on_eq_continuous_at
holo holomorphic_on_imp_continuous_on by blast
- obtain r2 where r2:"r2>0" "ball z r2 \<subseteq> S"
+ obtain r2 where r2: "r2>0" "ball z r2 \<subseteq> S"
using assms openE by blast
show ?thesis unfolding eventually_at
- by (metis (no_types) dist_commute dual_order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
+ by (metis (no_types) dist_commute order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
qed
lemma not_essential_times[singularity_intros]:
- assumes f_ness:"not_essential f z" and g_ness:"not_essential g z"
- assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
+ assumes f_ness: "not_essential f z" and g_ness: "not_essential g z"
+ assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
shows "not_essential (\<lambda>w. f w * g w) z"
proof -
define fg where "fg = (\<lambda>w. f w * g w)"
@@ -704,41 +706,40 @@
from tendsto_cong[OF this] have "fg \<midarrow>z\<rightarrow>0" by auto
then show ?thesis unfolding not_essential_def fg_def by auto
qed
- moreover have ?thesis when f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" and g_nconst:"\<exists>\<^sub>Fw in (at z). g w\<noteq>0"
+ moreover have ?thesis when f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0" and g_nconst: "\<exists>\<^sub>Fw in (at z). g w\<noteq>0"
proof -
- obtain fn fp fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
+ obtain fn fp fr where [simp]: "fp z \<noteq> 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
- "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
- using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto
- obtain gn gp gr where [simp]:"gp z \<noteq> 0" and "gr > 0"
+ "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
+ using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
+ obtain gn gp gr where [simp]: "gp z \<noteq> 0" and "gr > 0"
and gr: "gp holomorphic_on cball z gr"
- "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powi gn \<and> gp w \<noteq> 0"
- using holomorphic_factor_puncture[OF g_iso g_ness g_nconst,THEN ex1_implies_ex] by auto
+ "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w-z) powi gn \<and> gp w \<noteq> 0"
+ using holomorphic_factor_puncture[OF g_iso g_ness g_nconst] by auto
define r1 where "r1=(min fr gr)"
have "r1>0" unfolding r1_def using \<open>fr>0\<close> \<open>gr>0\<close> by auto
- have fg_times:"fg w = (fp w * gp w) * (w - z) powi (fn+gn)" and fgp_nz:"fp w*gp w\<noteq>0"
+ have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w\<noteq>0"
when "w\<in>ball z r1 - {z}" for w
proof -
- have "f w = fp w * (w - z) powi fn" "fp w\<noteq>0"
- using fr(2)[rule_format,of w] that unfolding r1_def by auto
- moreover have "g w = gp w * (w - z) powi gn" "gp w \<noteq> 0"
- using gr(2)[rule_format, of w] that unfolding r1_def by auto
- ultimately show "fg w = (fp w * gp w) * (w - z) powi (fn+gn)" "fp w*gp w\<noteq>0"
- using that unfolding fg_def by (auto simp add:power_int_add)
+ have "f w = fp w * (w-z) powi fn" "fp w\<noteq>0"
+ using fr that unfolding r1_def by auto
+ moreover have "g w = gp w * (w-z) powi gn" "gp w \<noteq> 0"
+ using gr that unfolding r1_def by auto
+ ultimately show "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" "fp w*gp w\<noteq>0"
+ using that by (auto simp add: fg_def power_int_add)
qed
- have [intro]: "fp \<midarrow>z\<rightarrow>fp z" "gp \<midarrow>z\<rightarrow>gp z"
+ obtain [intro]: "fp \<midarrow>z\<rightarrow>fp z" "gp \<midarrow>z\<rightarrow>gp z"
using fr(1) \<open>fr>0\<close> gr(1) \<open>gr>0\<close>
- by (meson open_ball ball_subset_cball centre_in_ball
- continuous_on_eq_continuous_at continuous_within holomorphic_on_imp_continuous_on
- holomorphic_on_subset)+
+ by (metis centre_in_ball continuous_at continuous_on_interior
+ holomorphic_on_imp_continuous_on interior_cball)
have ?thesis when "fn+gn>0"
proof -
- have "(\<lambda>w. (fp w * gp w) * (w - z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0"
+ have "(\<lambda>w. (fp w * gp w) * (w-z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0"
using that by (auto intro!:tendsto_eq_intros)
then have "fg \<midarrow>z\<rightarrow> 0"
- apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
+ using Lim_transform_within[OF _ \<open>r1>0\<close>]
by (smt (verit, best) Diff_iff dist_commute fg_times mem_ball power_int_def singletonD that zero_less_dist_iff)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
@@ -749,7 +750,7 @@
then have "fg \<midarrow>z\<rightarrow> fp z*gp z"
apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
apply (subst fg_times)
- by (auto simp add:dist_commute that)
+ by (auto simp add: dist_commute that)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
moreover have ?thesis when "fn+gn<0"
@@ -773,28 +774,26 @@
qed
lemma not_essential_inverse[singularity_intros]:
- assumes f_ness:"not_essential f z"
- assumes f_iso:"isolated_singularity_at f z"
+ assumes f_ness: "not_essential f z"
+ assumes f_iso: "isolated_singularity_at f z"
shows "not_essential (\<lambda>w. inverse (f w)) z"
proof -
define vf where "vf = (\<lambda>w. inverse (f w))"
have ?thesis when "\<not>(\<exists>\<^sub>Fw in (at z). f w\<noteq>0)"
proof -
have "\<forall>\<^sub>Fw in (at z). f w=0"
- using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
+ using not_eventually that by fastforce
then have "vf \<midarrow>z\<rightarrow>0"
unfolding vf_def by (simp add: tendsto_eventually)
- then show ?thesis unfolding not_essential_def vf_def by auto
+ then show ?thesis
+ unfolding not_essential_def vf_def by auto
qed
moreover have ?thesis when "is_pole f z"
+ by (metis (mono_tags, lifting) filterlim_at filterlim_inverse_at_iff is_pole_def
+ not_essential_def that)
+ moreover have ?thesis when "\<exists>x. f\<midarrow>z\<rightarrow>x " and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
proof -
- have "vf \<midarrow>z\<rightarrow>0"
- using that filterlim_at filterlim_inverse_at_iff unfolding is_pole_def vf_def by blast
- then show ?thesis unfolding not_essential_def vf_def by auto
- qed
- moreover have ?thesis when "\<exists>x. f\<midarrow>z\<rightarrow>x " and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
- proof -
- from that obtain fz where fz:"f\<midarrow>z\<rightarrow>fz" by auto
+ from that obtain fz where fz: "f\<midarrow>z\<rightarrow>fz" by auto
have ?thesis when "fz=0"
proof -
@@ -814,8 +813,8 @@
qed
lemma isolated_singularity_at_inverse[singularity_intros]:
- assumes f_iso:"isolated_singularity_at f z"
- and f_ness:"not_essential f z"
+ assumes f_iso: "isolated_singularity_at f z"
+ and f_ness: "not_essential f z"
shows "isolated_singularity_at (\<lambda>w. inverse (f w)) z"
proof -
define vf where "vf = (\<lambda>w. inverse (f w))"
@@ -825,21 +824,22 @@
using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
then have "\<forall>\<^sub>Fw in (at z). vf w=0"
unfolding vf_def by auto
- then obtain d1 where "d1>0" and d1:"\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> vf x = 0"
+ then obtain d1 where "d1>0" and d1: "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> vf x = 0"
unfolding eventually_at by auto
then have "vf holomorphic_on ball z d1-{z}"
- apply (rule_tac holomorphic_transform[of "\<lambda>_. 0"])
- by (auto simp add:dist_commute)
+ using holomorphic_transform[of "\<lambda>_. 0"]
+ by (metis Diff_iff dist_commute holomorphic_on_const insert_iff mem_ball)
then have "vf analytic_on ball z d1 - {z}"
by (simp add: analytic_on_open open_delete)
- then show ?thesis using \<open>d1>0\<close> unfolding isolated_singularity_at_def vf_def by auto
+ then show ?thesis
+ using \<open>d1>0\<close> unfolding isolated_singularity_at_def vf_def by auto
qed
- moreover have ?thesis when f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+ moreover have ?thesis when f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
proof -
have "\<forall>\<^sub>F w in at z. f w \<noteq> 0" using non_zero_neighbour[OF f_iso f_ness f_nconst] .
- then obtain d1 where d1:"d1>0" "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> f x \<noteq> 0"
+ then obtain d1 where d1: "d1>0" "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> f x \<noteq> 0"
unfolding eventually_at by auto
- obtain d2 where "d2>0" and d2:"f analytic_on ball z d2 - {z}"
+ obtain d2 where "d2>0" and d2: "f analytic_on ball z d2 - {z}"
using f_iso unfolding isolated_singularity_at_def by auto
define d3 where "d3=min d1 d2"
have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
@@ -849,31 +849,33 @@
then have "vf analytic_on ball z d3 - {z}"
unfolding vf_def
by (intro analytic_on_inverse; simp add: d1(2) d3_def dist_commute)
- ultimately show ?thesis unfolding isolated_singularity_at_def vf_def by auto
+ ultimately show ?thesis
+ unfolding isolated_singularity_at_def vf_def by auto
qed
ultimately show ?thesis by auto
qed
lemma not_essential_divide[singularity_intros]:
- assumes f_ness:"not_essential f z" and g_ness:"not_essential g z"
- assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
+ assumes f_ness: "not_essential f z" and g_ness: "not_essential g z"
+ assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
shows "not_essential (\<lambda>w. f w / g w) z"
proof -
have "not_essential (\<lambda>w. f w * inverse (g w)) z"
- by (simp add: f_iso f_ness g_iso g_ness isolated_singularity_at_inverse not_essential_inverse not_essential_times)
- then show ?thesis by (simp add:field_simps)
+ by (simp add: f_iso f_ness g_iso g_ness isolated_singularity_at_inverse
+ not_essential_inverse not_essential_times)
+ then show ?thesis by (simp add: field_simps)
qed
lemma
- assumes f_iso:"isolated_singularity_at f z"
- and g_iso:"isolated_singularity_at g z"
+ assumes f_iso: "isolated_singularity_at f z"
+ and g_iso: "isolated_singularity_at g z"
shows isolated_singularity_at_times[singularity_intros]:
"isolated_singularity_at (\<lambda>w. f w * g w) z"
and isolated_singularity_at_add[singularity_intros]:
"isolated_singularity_at (\<lambda>w. f w + g w) z"
proof -
obtain d1 d2 where "d1>0" "d2>0"
- and d1:"f analytic_on ball z d1 - {z}" and d2:"g analytic_on ball z d2 - {z}"
+ and d1: "f analytic_on ball z d1 - {z}" and d2: "g analytic_on ball z d2 - {z}"
using f_iso g_iso unfolding isolated_singularity_at_def by auto
define d3 where "d3=min d1 d2"
have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
@@ -893,7 +895,7 @@
qed
lemma isolated_singularity_at_uminus[singularity_intros]:
- assumes f_iso:"isolated_singularity_at f z"
+ assumes f_iso: "isolated_singularity_at f z"
shows "isolated_singularity_at (\<lambda>w. - f w) z"
using assms unfolding isolated_singularity_at_def using analytic_on_neg by blast
@@ -1044,7 +1046,7 @@
lemma not_essential_uminus [singularity_intros]:
assumes f_ness: "not_essential f z"
- assumes f_iso:"isolated_singularity_at f z"
+ assumes f_iso: "isolated_singularity_at f z"
shows "not_essential (\<lambda>w. -f w) z"
proof -
have "not_essential (\<lambda>w. -1 * f w) z"
@@ -1065,17 +1067,17 @@
\<and> h w \<noteq>0)))"
definition\<^marker>\<open>tag important\<close> zor_poly
- ::"[complex \<Rightarrow> complex, complex] \<Rightarrow> complex \<Rightarrow> complex" where
+ :: "[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) powi (zorder f z)
+ \<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w-z) powi (zorder f z)
\<and> h w \<noteq>0))"
lemma zorder_exist:
- fixes f::"complex \<Rightarrow> complex" and z::complex
+ fixes f:: "complex \<Rightarrow> complex" and z::complex
defines "n \<equiv> zorder f z" and "g \<equiv> zor_poly f z"
- assumes f_iso:"isolated_singularity_at f z"
- and f_ness:"not_essential f z"
- and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+ assumes f_iso: "isolated_singularity_at f z"
+ and f_ness: "not_essential f z"
+ and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
shows "g z\<noteq>0 \<and> (\<exists>r. r>0 \<and> g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq>0))"
proof -
@@ -1084,13 +1086,13 @@
have "\<exists>!k. \<exists>g r. P k g r"
using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto
then have "\<exists>g r. P n g r"
- unfolding n_def P_def zorder_def
- by (drule_tac theI',argo)
+ unfolding n_def P_def zorder_def by (rule theI')
then have "\<exists>r. P n g r"
- unfolding P_def zor_poly_def g_def n_def
- by (drule_tac someI_ex,argo)
- then obtain r1 where "P n g r1" by auto
- then show ?thesis unfolding P_def by auto
+ unfolding P_def zor_poly_def g_def n_def by (rule someI_ex)
+ then obtain r1 where "P n g r1"
+ by auto
+ then show ?thesis
+ unfolding P_def by auto
qed
lemma zorder_shift:
@@ -1109,7 +1111,7 @@
apply (rule_tac x="h o (\<lambda>u. u-z)" in exI)
apply (rule_tac x="r" in exI)
apply (intro conjI holomorphic_on_compose holomorphic_intros)
- apply (simp_all add: flip: cball_translation_subtract)
+ apply (simp_all flip: cball_translation_subtract)
by (metis diff_add_cancel eq_iff_diff_eq_0 norm_minus_commute)
done
@@ -1117,10 +1119,10 @@
by (rule zorder_shift)
lemma
- fixes f::"complex \<Rightarrow> complex" and z::complex
- assumes f_iso:"isolated_singularity_at f z"
- and f_ness:"not_essential f z"
- and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+ fixes f:: "complex \<Rightarrow> complex" and z::complex
+ assumes f_iso: "isolated_singularity_at f z"
+ and f_ness: "not_essential f z"
+ and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
shows zorder_inverse: "zorder (\<lambda>w. inverse (f w)) z = - zorder f z"
and zor_poly_inverse: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. inverse (f w)) z w
= inverse (zor_poly f z w)"
@@ -1131,33 +1133,32 @@
define fp vfp where
"fp = zor_poly f z" and "vfp = zor_poly vf z"
- obtain fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
+ obtain fr where [simp]: "fp z \<noteq> 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
- "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
+ "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
using zorder_exist[OF f_iso f_ness f_nconst,folded fn_def fp_def]
by auto
- have fr_inverse: "vf w = (inverse (fp w)) * (w - z) powi (-fn)"
+ have fr_inverse: "vf w = (inverse (fp w)) * (w-z) powi (-fn)"
and fr_nz: "inverse (fp w) \<noteq> 0"
when "w\<in>ball z fr - {z}" for w
proof -
- have "f w = fp w * (w - z) powi fn" "fp w \<noteq> 0"
+ have "f w = fp w * (w-z) powi fn" "fp w \<noteq> 0"
using fr(2) that by auto
- then show "vf w = (inverse (fp w)) * (w - z) powi (-fn)" "inverse (fp w)\<noteq>0"
+ then show "vf w = (inverse (fp w)) * (w-z) powi (-fn)" "inverse (fp w)\<noteq>0"
by (simp_all add: power_int_minus vf_def)
qed
- obtain vfr where [simp]:"vfp z \<noteq> 0" and "vfr>0" and vfr:"vfp holomorphic_on cball z vfr"
- "(\<forall>w\<in>cball z vfr - {z}. vf w = vfp w * (w - z) powi vfn \<and> vfp w \<noteq> 0)"
+ obtain vfr where [simp]: "vfp z \<noteq> 0" and "vfr>0" and vfr: "vfp holomorphic_on cball z vfr"
+ "(\<forall>w\<in>cball z vfr - {z}. vf w = vfp w * (w-z) powi vfn \<and> vfp w \<noteq> 0)"
proof -
have "isolated_singularity_at vf z"
using isolated_singularity_at_inverse[OF f_iso f_ness] unfolding vf_def .
moreover have "not_essential vf z"
using not_essential_inverse[OF f_ness f_iso] unfolding vf_def .
moreover have "\<exists>\<^sub>F w in at z. vf w \<noteq> 0"
- using f_nconst unfolding vf_def by (auto elim:frequently_elim1)
+ using f_nconst unfolding vf_def by (auto elim: frequently_elim1)
ultimately show ?thesis using zorder_exist[of vf z, folded vfn_def vfp_def] that by auto
qed
-
define r1 where "r1 = min fr vfr"
have "r1>0" using \<open>fr>0\<close> \<open>vfr>0\<close> unfolding r1_def by simp
show "vfn = - fn"
@@ -1165,8 +1166,8 @@
have \<section>: "\<And>w. \<lbrakk>fp w = 0; dist z w < fr\<rbrakk> \<Longrightarrow> False"
using fr_nz by force
then show "\<forall>w\<in>ball z r1 - {z}.
- vf w = vfp w * (w - z) powi vfn \<and>
- vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w - z) powi (- fn) \<and>
+ vf w = vfp w * (w-z) powi vfn \<and>
+ vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w-z) powi (- fn) \<and>
inverse (fp w) \<noteq> 0"
using fr_inverse r1_def vfr(2)
by (smt (verit) Diff_iff inverse_nonzero_iff_nonzero mem_ball mem_cball)
@@ -1177,13 +1178,14 @@
qed (use \<open>r1>0\<close> in auto)
have "vfp w = inverse (fp w)" when "w\<in>ball z r1-{z}" for w
proof -
- have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}" "w\<noteq>z" using that unfolding r1_def by auto
- from fr_inverse[OF this(1)] fr_nz[OF this(1)] vfr(2)[rule_format,OF this(2)] \<open>vfn = - fn\<close> \<open>w\<noteq>z\<close>
- show ?thesis by auto
+ have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}" "w\<noteq>z"
+ using that unfolding r1_def by auto
+ then show ?thesis
+ by (metis \<open>vfn = - fn\<close> power_int_not_zero right_minus_eq fr_inverse vfr(2)
+ vector_space_over_itself.scale_right_imp_eq)
qed
then show "\<forall>\<^sub>Fw in (at z). vfp w = inverse (fp w)"
- unfolding eventually_at using \<open>r1>0\<close>
- by (metis DiffI dist_commute mem_ball singletonD)
+ unfolding eventually_at by (metis DiffI dist_commute mem_ball singletonD \<open>r1>0\<close>)
qed
lemma zor_poly_shift:
@@ -1193,9 +1195,9 @@
shows "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly (\<lambda>u. f (z + u)) 0 (w-z)"
proof -
obtain r1 where "r1>0" "zor_poly f z z \<noteq> 0" and
- holo1:"zor_poly f z holomorphic_on cball z r1" and
- rball1:"\<forall>w\<in>cball z r1 - {z}.
- f w = zor_poly f z w * (w - z) powi (zorder f z) \<and>
+ holo1: "zor_poly f z holomorphic_on cball z r1" and
+ rball1: "\<forall>w\<in>cball z r1 - {z}.
+ f w = zor_poly f z w * (w-z) powi (zorder f z) \<and>
zor_poly f z w \<noteq> 0"
using zorder_exist[OF iso1 ness1 nzero1] by blast
@@ -1203,54 +1205,50 @@
have "isolated_singularity_at ff 0"
unfolding ff_def
using iso1 isolated_singularity_at_shift_iff[of f 0 z]
- by (simp add:algebra_simps)
+ by (simp add: algebra_simps)
moreover have "not_essential ff 0"
unfolding ff_def
using ness1 not_essential_shift_iff[of f 0 z]
- by (simp add:algebra_simps)
+ by (simp add: algebra_simps)
moreover have "\<exists>\<^sub>F w in at 0. ff w \<noteq> 0"
unfolding ff_def using nzero1
by (smt (verit, ccfv_SIG) add.commute eventually_at_to_0
eventually_mono not_frequently)
- ultimately obtain r2 where "r2>0" "zor_poly ff 0 0 \<noteq> 0" and
- holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
- rball2:"\<forall>w\<in>cball 0 r2 - {0}.
- ff w = zor_poly ff 0 w * w powi (zorder ff 0) \<and>
- zor_poly ff 0 w \<noteq> 0"
+ ultimately
+ obtain r2 where "r2>0" "zor_poly ff 0 0 \<noteq> 0"
+ and holo2: "zor_poly ff 0 holomorphic_on cball 0 r2"
+ and rball2: "\<forall>w\<in>cball 0 r2 - {0}.
+ ff w = zor_poly ff 0 w * w powi (zorder ff 0) \<and> zor_poly ff 0 w \<noteq> 0"
using zorder_exist[of ff 0] by auto
define r where "r=min r1 r2"
have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
- have "zor_poly f z w = zor_poly ff 0 (w - z)"
+ have "zor_poly f z w = zor_poly ff 0 (w-z)"
if "w\<in>ball z r - {z}" for w
proof -
define n where "n \<equiv> zorder f z"
- have "f w = zor_poly f z w * (w - z) powi n"
+ have "f w = zor_poly f z w * (w-z) powi n"
using n_def r_def rball1 that by auto
- moreover have "f w = zor_poly ff 0 (w - z) * (w - z) powi n"
+ moreover have "f w = zor_poly ff 0 (w-z) * (w-z) powi n"
proof -
have "w-z\<in>cball 0 r2 - {0}"
- using r_def that by (auto simp:dist_complex_def)
- from rball2[rule_format, OF this]
- have "ff (w - z) = zor_poly ff 0 (w - z) * (w - z)
- powi (zorder ff 0)"
- by simp
+ using r_def that by (auto simp: dist_complex_def)
+ then have "ff (w-z) = zor_poly ff 0 (w-z) * (w-z) powi (zorder ff 0)"
+ using rball2 by blast
moreover have "of_int (zorder ff 0) = n"
unfolding n_def ff_def by (simp add:zorder_shift' add.commute)
ultimately show ?thesis unfolding ff_def by auto
qed
- ultimately have "zor_poly f z w * (w - z) powi n
- = zor_poly ff 0 (w - z) * (w - z) powi n"
+ ultimately have "zor_poly f z w * (w-z) powi n = zor_poly ff 0 (w-z) * (w-z) powi n"
by auto
- moreover have "(w - z) powi n \<noteq>0"
+ moreover have "(w-z) powi n \<noteq>0"
using that by auto
ultimately show ?thesis
using mult_cancel_right by blast
qed
- then have "\<forall>\<^sub>F w in at z. zor_poly f z w
- = zor_poly ff 0 (w - z)"
+ then have "\<forall>\<^sub>F w in at z. zor_poly f z w = zor_poly ff 0 (w-z)"
unfolding eventually_at
by (metis DiffI \<open>0 < r\<close> dist_commute mem_ball singletonD)
moreover have "isCont (zor_poly f z) z"
@@ -1258,20 +1256,21 @@
by (simp add: \<open>0 < r1\<close> continuous_on_interior)
moreover
have "isCont (zor_poly ff 0) 0"
- using \<open>0 < r2\<close> centre_in_ball continuous_on_interior holo2 holomorphic_on_imp_continuous_on interior_cball by blast
- then have "isCont (\<lambda>w. zor_poly ff 0 (w - z)) z"
+ using \<open>0 < r2\<close> continuous_on_interior holo2 holomorphic_on_imp_continuous_on
+ by fastforce
+ then have "isCont (\<lambda>w. zor_poly ff 0 (w-z)) z"
unfolding isCont_iff by simp
- ultimately show "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly ff 0 (w - z)"
+ ultimately show "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly ff 0 (w-z)"
by (elim at_within_isCont_imp_nhds;auto)
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"
- and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+ 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"
+ and f_ness: "not_essential f z" and g_ness: "not_essential g z"
and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
- shows zorder_times:"zorder (\<lambda>w. f w * g w) z = zorder f z + zorder g z" and
- zor_poly_times:"\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w * g w) z w
+ shows zorder_times: "zorder (\<lambda>w. f w * g w) z = zorder f z + zorder g z" and
+ zor_poly_times: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w * g w) z w
= zor_poly f z w *zor_poly g z w"
proof -
define fg where "fg = (\<lambda>w. f w * g w)"
@@ -1279,32 +1278,32 @@
"fn = zorder f z" and "gn = zorder g z" and "fgn = zorder fg z"
define fp gp fgp where
"fp = zor_poly f z" and "gp = zor_poly g z" and "fgp = zor_poly fg z"
- have f_nconst:"\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst:"\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
+ have f_nconst: "\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst: "\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
using fg_nconst by (auto elim!:frequently_elim1)
- obtain fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
+ obtain fr where [simp]: "fp z \<noteq> 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
- "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
+ "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
using zorder_exist[OF f_iso f_ness f_nconst,folded fp_def fn_def] by auto
- obtain gr where [simp]:"gp z \<noteq> 0" and "gr > 0"
+ obtain gr where [simp]: "gp z \<noteq> 0" and "gr > 0"
and gr: "gp holomorphic_on cball z gr"
- "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powi gn \<and> gp w \<noteq> 0"
+ "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w-z) powi gn \<and> gp w \<noteq> 0"
using zorder_exist[OF g_iso g_ness g_nconst,folded gn_def gp_def] by auto
define r1 where "r1=min fr gr"
have "r1>0" unfolding r1_def using \<open>fr>0\<close> \<open>gr>0\<close> by auto
- have fg_times:"fg w = (fp w * gp w) * (w - z) powi (fn+gn)" and fgp_nz:"fp w*gp w\<noteq>0"
+ have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w\<noteq>0"
when "w\<in>ball z r1 - {z}" for w
proof -
- have "f w = fp w * (w - z) powi fn" "fp w \<noteq> 0"
- using fr(2)[rule_format,of w] that unfolding r1_def by auto
- moreover have "g w = gp w * (w - z) powi gn" "gp w \<noteq> 0"
+ have "f w = fp w * (w-z) powi fn" "fp w \<noteq> 0"
+ using fr(2) r1_def that by auto
+ moreover have "g w = gp w * (w-z) powi gn" "gp w \<noteq> 0"
using gr(2) that unfolding r1_def by auto
- ultimately show "fg w = (fp w * gp w) * (w - z) powi (fn+gn)" "fp w*gp w\<noteq>0"
- using that unfolding fg_def by (auto simp add:power_int_add)
+ ultimately show "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" "fp w*gp w\<noteq>0"
+ using that unfolding fg_def by (auto simp add: power_int_add)
qed
- obtain fgr where [simp]:"fgp z \<noteq> 0" and "fgr > 0"
+ obtain fgr where [simp]: "fgp z \<noteq> 0" and "fgr > 0"
and fgr: "fgp holomorphic_on cball z fgr"
- "\<forall>w\<in>cball z fgr - {z}. fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0"
+ "\<forall>w\<in>cball z fgr - {z}. fg w = fgp w * (w-z) powi fgn \<and> fgp w \<noteq> 0"
proof -
have "isolated_singularity_at fg z"
unfolding fg_def using isolated_singularity_at_times[OF f_iso g_iso] .
@@ -1318,42 +1317,40 @@
define r2 where "r2 = min fgr r1"
have "r2>0" using \<open>r1>0\<close> \<open>fgr>0\<close> unfolding r2_def by simp
show "fgn = fn + gn "
- apply (rule holomorphic_factor_unique[of r2 fgp z "\<lambda>w. fp w * gp w" fg])
- subgoal using \<open>r2>0\<close> by simp
- subgoal by simp
- subgoal by simp
- subgoal
- proof (rule ballI)
- fix w assume "w \<in> ball z r2 - {z}"
- then have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" unfolding r2_def by auto
- then show "fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0
- \<and> fg w = fp w * gp w * (w - z) powi (fn + gn) \<and> fp w * gp w \<noteq> 0"
- using fg_times fgp_nz fgr(2) by blast
- qed
- subgoal using fgr(1) unfolding r2_def r1_def by (auto intro!:holomorphic_intros)
- subgoal using fr(1) gr(1) unfolding r2_def r1_def by (auto intro!:holomorphic_intros)
- done
+ proof (rule holomorphic_factor_unique)
+ show "\<forall>w \<in> ball z r2 - {z}. fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0 \<and> fg w = fp w * gp w * (w - z) powi (fn + gn) \<and> fp w * gp w \<noteq> 0"
+ using fg_times fgp_nz fgr(2) r2_def by fastforce
+ next
+ show "fgp holomorphic_on ball z r2"
+ using fgr(1) r2_def by auto
+ next
+ show "(\<lambda>w. fp w * gp w) holomorphic_on ball z r2"
+ by (metis ball_subset_cball fr(1) gr(1) holomorphic_on_mult holomorphic_on_subset
+ min.cobounded1 min.cobounded2 r1_def r2_def subset_ball)
+ qed (auto simp add: \<open>0 < r2\<close>)
- have "fgp w = fp w *gp w" when "w\<in>ball z r2-{z}" for w
+ have "fgp w = fp w *gp w" when w: "w \<in> ball z r2-{z}" for w
proof -
- have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" "w\<noteq>z" using that unfolding r2_def by auto
- from fg_times[OF this(1)] fgp_nz[OF this(1)] fgr(2)[rule_format,OF this(2)] \<open>fgn = fn + gn\<close> \<open>w\<noteq>z\<close>
- show ?thesis by auto
+ have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" "w\<noteq>z"
+ using w unfolding r2_def by auto
+ then show ?thesis
+ by (metis \<open>fgn = fn + gn\<close> eq_iff_diff_eq_0 fg_times fgr(2) power_int_eq_0_iff
+ mult_right_cancel)
qed
then show "\<forall>\<^sub>Fw in (at z). fgp w = fp w * gp w"
- using \<open>r2>0\<close> unfolding eventually_at by (auto simp add:dist_commute)
+ using \<open>r2>0\<close> unfolding eventually_at 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"
- and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+ 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"
+ and f_ness: "not_essential f z" and g_ness: "not_essential g z"
and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
- shows zorder_divide:"zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" and
- zor_poly_divide:"\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w / g w) z w
- = zor_poly f z w / zor_poly g z w"
+ shows zorder_divide: "zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" and
+ zor_poly_divide: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w / g w) z w
+ = zor_poly f z w / zor_poly g z w"
proof -
- have f_nconst:"\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst:"\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
+ have f_nconst: "\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst: "\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
using fg_nconst by (auto elim!:frequently_elim1)
define vg where "vg=(\<lambda>w. inverse (g w))"
have 1: "isolated_singularity_at vg z"
@@ -1362,59 +1359,53 @@
by (simp add: g_iso g_ness not_essential_inverse vg_def)
moreover have 3: "\<exists>\<^sub>F w in at z. f w * vg w \<noteq> 0"
using fg_nconst vg_def by auto
- ultimately have "zorder (\<lambda>w. f w * vg w) z = zorder f z + zorder vg z"
+ ultimately have "zorder (\<lambda>w. f w * vg w) z = zorder f z + zorder vg z"
using zorder_times[OF f_iso _ f_ness] by blast
then show "zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z"
using zorder_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def
- by (auto simp add:field_simps)
-
+ by (auto simp add: field_simps)
have "\<forall>\<^sub>F w in at z. zor_poly (\<lambda>w. f w * vg w) z w = zor_poly f z w * zor_poly vg z w"
using zor_poly_times[OF f_iso _ f_ness,of vg] 1 2 3 by blast
then show "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w / g w) z w = zor_poly f z w / zor_poly g z w"
using zor_poly_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def
- by eventually_elim (auto simp add:field_simps)
+ by eventually_elim (auto simp add: field_simps)
qed
lemma zorder_exist_zero:
- fixes f::"complex \<Rightarrow> complex" and z::complex
- defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z"
- assumes holo: "f holomorphic_on s" and
- "open s" "connected s" "z\<in>s"
- and non_const: "\<exists>w\<in>s. f w \<noteq> 0"
- shows "(if f z=0 then n > 0 else n=0) \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> s \<and> g holomorphic_on cball z r
+ fixes f:: "complex \<Rightarrow> complex" and z::complex
+ defines "n \<equiv> zorder f z" and "g \<equiv> zor_poly f z"
+ assumes holo: "f holomorphic_on S" and "open S" "connected S" "z\<in>S"
+ and non_const: "\<exists>w\<in>S. f w \<noteq> 0"
+ shows "(if f z=0 then n > 0 else n=0) \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> S \<and> g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r. f w = g w * (w-z) ^ nat n \<and> g w \<noteq>0))"
proof -
- obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> s" "g holomorphic_on cball z r"
- "(\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> S" "g holomorphic_on cball z r"
+ "(\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
proof -
have "g z \<noteq> 0 \<and> (\<exists>r>0. g holomorphic_on cball z r
- \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0))"
+ \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0))"
proof (rule zorder_exist[of f z,folded g_def n_def])
- show "isolated_singularity_at f z" unfolding isolated_singularity_at_def
- using holo assms(4,6)
- by (meson Diff_subset open_ball analytic_on_holomorphic holomorphic_on_subset openE)
+ show "isolated_singularity_at f z"
+ using \<open>open S\<close> \<open>z\<in>S\<close> holo holomorphic_on_imp_analytic_at isolated_singularity_at_analytic
+ by force
show "not_essential f z" unfolding not_essential_def
- using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on
+ using \<open>open S\<close> \<open>z\<in>S\<close> at_within_open continuous_on holo holomorphic_on_imp_continuous_on
by fastforce
- have "\<forall>\<^sub>F w in at z. f w \<noteq> 0 \<and> w\<in>s"
- proof -
- obtain w where "w\<in>s" "f w\<noteq>0" using non_const by auto
- then show ?thesis
- by (rule non_zero_neighbour_alt[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close>])
- qed
+ have "\<forall>\<^sub>F w in at z. f w \<noteq> 0 \<and> w\<in>S"
+ using assms(4,5,6) holo non_const non_zero_neighbour_alt by blast
then show "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
by (auto elim: eventually_frequentlyE)
qed
- then obtain r1 where "g z \<noteq> 0" "r1>0" and r1:"g holomorphic_on cball z r1"
- "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ then obtain r1 where "g z \<noteq> 0" "r1>0" and r1: "g holomorphic_on cball z r1"
+ "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
by auto
- obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> s"
+ obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> S"
using assms(4,6) open_contains_cball_eq by blast
define r3 where "r3 \<equiv> min r1 r2"
- have "r3>0" "cball z r3 \<subseteq> s" using \<open>r1>0\<close> r2 unfolding r3_def by auto
+ have "r3>0" "cball z r3 \<subseteq> S" using \<open>r1>0\<close> r2 unfolding r3_def by auto
moreover have "g holomorphic_on cball z r3"
using r1(1) unfolding r3_def by auto
- moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
using r1(2) unfolding r3_def by auto
ultimately show ?thesis using that[of r3] \<open>g z\<noteq>0\<close> by auto
qed
@@ -1425,24 +1416,24 @@
using r
by (meson Elementary_Metric_Spaces.open_ball analytic_at analytic_at_imp_isCont
ball_subset_cball centre_in_ball holomorphic_on_subset isContD)
- have if_0:"if f z=0 then n > 0 else n=0"
+ have if_0: "if f z=0 then n > 0 else n=0"
proof -
- have "(\<lambda>w. g w * (w - z) powi n) \<midarrow>z\<rightarrow> f z"
+ have "(\<lambda>w. g w * (w-z) powi n) \<midarrow>z\<rightarrow> f z"
using fz_lim Lim_transform_within_open[where s="ball z r"] r by fastforce
- then have "(\<lambda>w. (g w * (w - z) powi n) / g w) \<midarrow>z\<rightarrow> f z/g z"
+ then have "(\<lambda>w. (g w * (w-z) powi n) / g w) \<midarrow>z\<rightarrow> f z/g z"
using gz_lim \<open>g z \<noteq> 0\<close> tendsto_divide by blast
- then have powi_tendsto:"(\<lambda>w. (w - z) powi n) \<midarrow>z\<rightarrow> f z/g z"
+ then have powi_tendsto: "(\<lambda>w. (w-z) powi n) \<midarrow>z\<rightarrow> f z/g z"
using Lim_transform_within_open[where s="ball z r"] r by fastforce
have ?thesis when "n\<ge>0" "f z=0"
proof -
- have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
+ have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
using Lim_transform_within[OF powi_tendsto, where d=r]
by (meson power_int_def r(1) that(1))
- then have *:"(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>f z=0\<close> by simp
+ then have *: "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>f z=0\<close> by simp
moreover have False when "n=0"
proof -
- have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 1"
+ have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 1"
using \<open>n=0\<close> by auto
then show False using * using LIM_unique zero_neq_one by blast
qed
@@ -1452,28 +1443,30 @@
proof -
have False when "n>0"
proof -
- have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
+ have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
using Lim_transform_within[OF powi_tendsto, where d=r]
by (meson \<open>0 \<le> n\<close> power_int_def r(1))
- moreover have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0"
+ moreover have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 0"
using \<open>n>0\<close> by (auto intro!:tendsto_eq_intros)
- ultimately show False using \<open>f z\<noteq>0\<close> \<open>g z\<noteq>0\<close> using LIM_unique divide_eq_0_iff by blast
+ ultimately show False
+ using \<open>f z\<noteq>0\<close> \<open>g z\<noteq>0\<close> LIM_unique divide_eq_0_iff by blast
qed
then show ?thesis using that by force
qed
moreover have False when "n<0"
proof -
- have "(\<lambda>w. inverse ((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z"
+ have "(\<lambda>w. inverse ((w-z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z"
by (smt (verit) LIM_cong power_int_def power_inverse powi_tendsto that)
moreover
- have "(\<lambda>w.((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> 0"
+ have "(\<lambda>w.((w-z) ^ nat (- n))) \<midarrow>z\<rightarrow> 0"
using that by (auto intro!:tendsto_eq_intros)
ultimately
have "(\<lambda>x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \<midarrow>z\<rightarrow> 0"
using tendsto_mult by fastforce
then have "(\<lambda>x. 1::complex) \<midarrow>z\<rightarrow> 0"
using Lim_transform_within_open by fastforce
- then show False using LIM_const_eq by fastforce
+ then show False
+ using LIM_const_eq by fastforce
qed
ultimately show ?thesis by fastforce
qed
@@ -1499,7 +1492,7 @@
then show ?thesis using \<open>g z\<noteq>0\<close> True by auto
next
case False
- then have "f w = g w * (w - z) powi n \<and> g w \<noteq> 0"
+ then have "f w = g w * (w-z) powi n" "g w \<noteq> 0"
using r(4) that by auto
then show ?thesis
by (smt (verit, best) False if_0 int_nat_eq power_int_of_nat)
@@ -1508,17 +1501,17 @@
qed
lemma zorder_exist_pole:
- fixes f::"complex \<Rightarrow> complex" and z::complex
+ fixes f:: "complex \<Rightarrow> complex" and z::complex
defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z"
assumes holo: "f holomorphic_on S-{z}" and "open S" "z\<in>S" and "is_pole f z"
shows "n < 0 \<and> g z\<noteq>0 \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> S \<and> g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w / (w-z) ^ nat (- n) \<and> g w \<noteq>0))"
proof -
obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> S" "g holomorphic_on cball z r"
- "(\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ "(\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
proof -
have "g z \<noteq> 0 \<and> (\<exists>r>0. g holomorphic_on cball z r
- \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0))"
+ \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0))"
proof (rule zorder_exist[of f z,folded g_def n_def])
show "isolated_singularity_at f z" unfolding isolated_singularity_at_def
using holo assms(4,5)
@@ -1529,8 +1522,8 @@
from non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] show "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
by (auto elim: eventually_frequentlyE)
qed
- then obtain r1 where "g z \<noteq> 0" "r1>0" and r1:"g holomorphic_on cball z r1"
- "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ then obtain r1 where "g z \<noteq> 0" "r1>0" and r1: "g holomorphic_on cball z r1"
+ "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
by auto
obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> S"
using assms(4,5) open_contains_cball_eq by metis
@@ -1538,22 +1531,24 @@
have "r3>0" "cball z r3 \<subseteq> S" using \<open>r1>0\<close> r2 unfolding r3_def by auto
moreover have "g holomorphic_on cball z r3"
using r1(1) unfolding r3_def by auto
- moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+ moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
using r1(2) unfolding r3_def by auto
- ultimately show ?thesis using that[of r3] \<open>g z\<noteq>0\<close> by auto
+ ultimately show ?thesis
+ using that[of r3] \<open>g z\<noteq>0\<close> by auto
qed
have "n<0"
proof (rule ccontr)
assume " \<not> n < 0"
define c where "c=(if n=0 then g z else 0)"
- have [simp]:"g \<midarrow>z\<rightarrow> g z"
- by (metis open_ball at_within_open ball_subset_cball centre_in_ball
- continuous_on holomorphic_on_imp_continuous_on holomorphic_on_subset r(1) r(3) )
- have "\<forall>\<^sub>F x in at z. f x = g x * (x - z) ^ nat n"
- unfolding eventually_at_topological
- apply (rule_tac exI[where x="ball z r"])
- by (simp add: \<open>\<not> n < 0\<close> linorder_not_le power_int_def r(1) r(4))
+ have [simp]: "g \<midarrow>z\<rightarrow> g z"
+ using r
+ by (metis centre_in_ball continuous_on_interior holomorphic_on_imp_continuous_on
+ interior_cball isContD)
+ have "\<forall>x \<in> ball z r. x \<noteq> z \<longrightarrow> f x = g x * (x - z) ^ nat n"
+ by (simp add: \<open>\<not> n < 0\<close> linorder_not_le power_int_def r)
+ then have "\<forall>\<^sub>F x in at z. f x = g x * (x - z) ^ nat n"
+ using centre_in_ball eventually_at_topological r(1) by blast
moreover have "(\<lambda>x. g x * (x - z) ^ nat n) \<midarrow>z\<rightarrow> c"
proof (cases "n=0")
case True
@@ -1572,12 +1567,13 @@
moreover have "\<forall>w\<in>cball z r - {z}. f w = g w / (w-z) ^ nat (- n) \<and> g w \<noteq>0"
using r(4) \<open>n<0\<close>
by (smt (verit) inverse_eq_divide mult.right_neutral power_int_def power_inverse times_divide_eq_right)
- ultimately show ?thesis using r(1-3) \<open>g z\<noteq>0\<close> by auto
+ ultimately show ?thesis
+ using r \<open>g z\<noteq>0\<close> by auto
qed
lemma zorder_eqI:
assumes "open S" "z \<in> S" "g holomorphic_on S" "g z \<noteq> 0"
- assumes fg_eq:"\<And>w. \<lbrakk>w \<in> S;w\<noteq>z\<rbrakk> \<Longrightarrow> f w = g w * (w - z) powi n"
+ assumes fg_eq: "\<And>w. \<lbrakk>w \<in> S;w\<noteq>z\<rbrakk> \<Longrightarrow> f w = g w * (w-z) powi n"
shows "zorder f z = n"
proof -
have "continuous_on S g" by (rule holomorphic_on_imp_continuous_on) fact
@@ -1588,7 +1584,7 @@
ultimately obtain r where r: "r > 0" "cball z r \<subseteq> S \<inter> (g -` (-{0}))"
unfolding open_contains_cball by blast
- let ?gg= "(\<lambda>w. g w * (w - z) powi n)"
+ let ?gg= "(\<lambda>w. g w * (w-z) powi n)"
define P where "P = (\<lambda>n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0))"
have "P n g r"
@@ -1611,13 +1607,13 @@
isCont_def not_essential_def)
show " \<forall>\<^sub>F w in at z. w - z \<noteq> 0" by (simp add: eventually_at_filter)
then show "LIM w at z. w - z :> at 0"
- unfolding filterlim_at by (auto intro:tendsto_eq_intros)
+ unfolding filterlim_at by (auto intro: tendsto_eq_intros)
show "isolated_singularity_at g z"
by (meson Diff_subset open_ball analytic_on_holomorphic
assms holomorphic_on_subset isolated_singularity_at_def openE)
qed
moreover
- have "\<forall>\<^sub>F w in at z. g w * (w - z) powi n = f w"
+ have "\<forall>\<^sub>F w in at z. g w * (w-z) powi n = f w"
unfolding eventually_at_topological using assms fg_eq by force
ultimately show "not_essential f z"
using not_essential_transform by blast
@@ -1626,12 +1622,12 @@
fix d::real assume "0 < d"
define z' where "z' \<equiv> z+min d r / 2"
have "z' \<noteq> z" " dist z' z < d "
- unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add:dist_norm)
+ unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add: dist_norm)
moreover have "f z' \<noteq> 0"
proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>])
have "z' \<in> cball z r"
- unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm)
- then show " z' \<in> S" using r(2) by blast
+ unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add: dist_norm)
+ then show "z' \<in> S" using r(2) by blast
show "g z' * (z' - z) powi n \<noteq> 0"
using P_def \<open>P n g r\<close> \<open>z' \<in> cball z r\<close> \<open>z' \<noteq> z\<close> by auto
qed
@@ -1645,47 +1641,47 @@
lemma simple_zeroI:
assumes "open S" "z \<in> S" "g holomorphic_on S" "g z \<noteq> 0"
- assumes "\<And>w. w \<in> S \<Longrightarrow> f w = g w * (w - z)"
+ assumes "\<And>w. w \<in> S \<Longrightarrow> f w = g w * (w-z)"
shows "zorder f z = 1"
using assms zorder_eqI by force
lemma higher_deriv_power:
- shows "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) w =
- pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)"
+ shows "(deriv ^^ j) (\<lambda>w. (w-z) ^ n) w =
+ pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j)"
proof (induction j arbitrary: w)
case 0
thus ?case by auto
next
case (Suc j w)
- have "(deriv ^^ Suc j) (\<lambda>w. (w - z) ^ n) w = deriv ((deriv ^^ j) (\<lambda>w. (w - z) ^ n)) w"
+ have "(deriv ^^ Suc j) (\<lambda>w. (w-z) ^ n) w = deriv ((deriv ^^ j) (\<lambda>w. (w-z) ^ n)) w"
by simp
- also have "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) =
- (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j))"
+ also have "(deriv ^^ j) (\<lambda>w. (w-z) ^ n) =
+ (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j))"
using Suc by (intro Suc.IH ext)
also {
have "(\<dots> has_field_derivative of_nat (n - j) *
- pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - Suc j)) (at w)"
+ pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - Suc j)) (at w)"
using Suc.prems by (auto intro!: derivative_eq_intros)
also have "of_nat (n - j) * pochhammer (of_nat (Suc n - j)) j =
pochhammer (of_nat (Suc n - Suc j)) (Suc j)"
by (cases "Suc j \<le> n", subst pochhammer_rec)
- (insert Suc.prems, simp_all add: algebra_simps Suc_diff_le pochhammer_0_left)
- finally have "deriv (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)) w =
- \<dots> * (w - z) ^ (n - Suc j)"
+ (use Suc.prems in \<open>simp_all add: algebra_simps Suc_diff_le pochhammer_0_left\<close>)
+ finally have "deriv (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j)) w =
+ \<dots> * (w-z) ^ (n - Suc j)"
by (rule DERIV_imp_deriv)
}
finally show ?case .
qed
lemma zorder_zero_eqI:
- assumes f_holo:"f holomorphic_on S" and "open S" "z \<in> S"
+ assumes f_holo: "f holomorphic_on S" and "open S" "z \<in> S"
assumes zero: "\<And>i. i < nat n \<Longrightarrow> (deriv ^^ i) f z = 0"
assumes nz: "(deriv ^^ nat n) f z \<noteq> 0" and "n\<ge>0"
shows "zorder f z = n"
proof -
- obtain r where [simp]:"r>0" and "ball z r \<subseteq> S"
+ obtain r where [simp]: "r>0" and "ball z r \<subseteq> S"
using \<open>open S\<close> \<open>z\<in>S\<close> openE by blast
- have nz':"\<exists>w\<in>ball z r. f w \<noteq> 0"
+ have nz': "\<exists>w\<in>ball z r. f w \<noteq> 0"
proof (rule ccontr)
assume "\<not> (\<exists>w\<in>ball z r. f w \<noteq> 0)"
then have "eventually (\<lambda>u. f u = 0) (nhds z)"
@@ -1701,7 +1697,7 @@
obtain e where e_if: "if f z = 0 then 0 < zn else zn = 0" and
[simp]: "e>0" and "cball z e \<subseteq> ball z r" and
g_holo: "g holomorphic_on cball z e" and
- e_fac: "(\<forall>w\<in>cball z e. f w = g w * (w - z) ^ nat zn \<and> g w \<noteq> 0)"
+ e_fac: "(\<forall>w\<in>cball z e. f w = g w * (w-z) ^ nat zn \<and> g w \<noteq> 0)"
proof -
have "f holomorphic_on ball z r"
using f_holo \<open>ball z r \<subseteq> S\<close> by auto
@@ -1712,23 +1708,23 @@
by (metis centre_in_cball less_le_not_le order_refl)
define A where "A \<equiv> (\<lambda>i. of_nat (i choose (nat zn)) * fact (nat zn) * (deriv ^^ (i - nat zn)) g z)"
- have deriv_A:"(deriv ^^ i) f z = (if zn \<le> int i then A i else 0)" for i
+ have deriv_A: "(deriv ^^ i) f z = (if zn \<le> int i then A i else 0)" for i
proof -
have "eventually (\<lambda>w. w \<in> ball z e) (nhds z)"
using \<open>cball z e \<subseteq> ball z r\<close> \<open>e>0\<close> by (intro eventually_nhds_in_open) auto
- hence "eventually (\<lambda>w. f w = (w - z) ^ (nat zn) * g w) (nhds z)"
+ hence "eventually (\<lambda>w. f w = (w-z) ^ (nat zn) * g w) (nhds z)"
using e_fac eventually_mono by fastforce
- hence "(deriv ^^ i) f z = (deriv ^^ i) (\<lambda>w. (w - z) ^ nat zn * g w) z"
+ hence "(deriv ^^ i) f z = (deriv ^^ i) (\<lambda>w. (w-z) ^ nat zn * g w) z"
by (intro higher_deriv_cong_ev) auto
also have "\<dots> = (\<Sum>j=0..i. of_nat (i choose j) *
- (deriv ^^ j) (\<lambda>w. (w - z) ^ nat zn) z * (deriv ^^ (i - j)) g z)"
+ (deriv ^^ j) (\<lambda>w. (w-z) ^ nat zn) z * (deriv ^^ (i - j)) g z)"
using g_holo \<open>e>0\<close>
by (intro higher_deriv_mult[of _ "ball z e"]) (auto intro!: holomorphic_intros)
also have "\<dots> = (\<Sum>j=0..i. if j = nat zn then
of_nat (i choose nat zn) * fact (nat zn) * (deriv ^^ (i - nat zn)) g z else 0)"
proof (intro sum.cong refl, goal_cases)
case (1 j)
- have "(deriv ^^ j) (\<lambda>w. (w - z) ^ nat zn) z =
+ have "(deriv ^^ j) (\<lambda>w. (w-z) ^ nat zn) z =
pochhammer (of_nat (Suc (nat zn) - j)) j * 0 ^ (nat zn - j)"
by (subst higher_deriv_power) auto
also have "\<dots> = (if j = nat zn then fact j else 0)"
@@ -1745,18 +1741,15 @@
qed
have False when "n<zn"
- proof -
- have "(deriv ^^ nat n) f z = 0"
- using deriv_A[of "nat n"] that \<open>n\<ge>0\<close> by auto
- with nz show False by auto
- qed
+ using deriv_A[of "nat n"] that \<open>n\<ge>0\<close> by (simp add: nz)
moreover have "n\<le>zn"
proof -
- have "g z \<noteq> 0" using e_fac[rule_format,of z] \<open>e>0\<close> by simp
+ have "g z \<noteq> 0"
+ by (simp add: \<open>g z \<noteq> 0\<close>)
then have "(deriv ^^ nat zn) f z \<noteq> 0"
- using deriv_A[of "nat zn"] by(auto simp add:A_def)
+ using deriv_A[of "nat zn"] by(auto simp add: A_def)
then have "nat zn \<ge> nat n" using zero[of "nat zn"] by linarith
- moreover have "zn\<ge>0" using e_if by (auto split:if_splits)
+ moreover have "zn\<ge>0" using e_if by (auto split: if_splits)
ultimately show ?thesis using nat_le_eq_zle by blast
qed
ultimately show ?thesis unfolding zn_def by fastforce
@@ -1764,7 +1757,7 @@
lemma
assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'"
- shows zorder_cong:"zorder f z = zorder g z'" and zor_poly_cong:"zor_poly f z = zor_poly g z'"
+ shows zorder_cong: "zorder f z = zorder g z'" and zor_poly_cong: "zor_poly f z = zor_poly g z'"
proof -
define P where "P = (\<lambda>ff n h r. 0 < r \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
\<and> (\<forall>w\<in>cball z r - {z}. ff w = h w * (w-z) powi n \<and> h w\<noteq>0))"
@@ -1772,19 +1765,19 @@
proof -
have *: "\<exists>r. P g n h r" if "\<exists>r. P f n h r" and "eventually (\<lambda>x. f x = g x) (at z)" for f g
proof -
- from that(1) obtain r1 where r1_P:"P f n h r1" by auto
- from that(2) obtain r2 where "r2>0" and r2_dist:"\<forall>x. x \<noteq> z \<and> dist x z \<le> r2 \<longrightarrow> f x = g x"
+ from that(1) obtain r1 where r1_P: "P f n h r1" by auto
+ from that(2) obtain r2 where "r2>0" and r2_dist: "\<forall>x. x \<noteq> z \<and> dist x z \<le> r2 \<longrightarrow> f x = g x"
unfolding eventually_at_le by auto
define r where "r=min r1 r2"
have "r>0" "h z\<noteq>0" using r1_P \<open>r2>0\<close> unfolding r_def P_def by auto
moreover have "h holomorphic_on cball z r"
using r1_P unfolding P_def r_def by auto
- moreover have "g w = h w * (w - z) powi n \<and> h w \<noteq> 0" when "w\<in>cball z r - {z}" for w
+ moreover have "g w = h w * (w-z) powi n \<and> h w \<noteq> 0" when "w\<in>cball z r - {z}" for w
proof -
- have "f w = h w * (w - z) powi n \<and> h w \<noteq> 0"
+ have "f w = h w * (w-z) powi n \<and> h w \<noteq> 0"
using r1_P that unfolding P_def r_def by auto
- moreover have "f w=g w" using r2_dist[rule_format,of w] that unfolding r_def
- by (simp add: dist_commute)
+ moreover have "f w=g w"
+ using r2_dist that by (simp add: dist_commute r_def)
ultimately show ?thesis by simp
qed
ultimately show ?thesis unfolding P_def by auto
@@ -1792,7 +1785,7 @@
from assms have eq': "eventually (\<lambda>z. g z = f z) (at z)"
by (simp add: eq_commute)
show ?thesis
- by (rule iffI[OF *[OF _ assms(1)] *[OF _ eq']])
+ using "*" assms(1) eq' by blast
qed
then show "zorder f z = zorder g z'" "zor_poly f z = zor_poly g z'"
using \<open>z=z'\<close> unfolding P_def zorder_def zor_poly_def by auto
@@ -1810,8 +1803,9 @@
proof -
define P where
"P = (\<lambda>f n h r. 0 < r \<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) powi n \<and> h w \<noteq> 0))"
- have *: "P (\<lambda>x. c * f x) n (\<lambda>x. c * h x) r" if "P f n h r" "c \<noteq> 0" for f n h r c
+ h z \<noteq> 0 \<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w-z) powi n \<and> h w \<noteq> 0))"
+ have *: "P (\<lambda>x. c * f x) n (\<lambda>x. c * h x) r"
+ if "P f n h r" "c \<noteq> 0" for f n h r c
using that unfolding P_def by (auto intro!: holomorphic_intros)
have "(\<exists>h r. P (\<lambda>x. c * f x) n h r) \<longleftrightarrow> (\<exists>h r. P f n h r)" for n
using *[of f n _ _ c] *[of "\<lambda>x. c * f x" n _ _ "inverse c"] \<open>c \<noteq> 0\<close>
@@ -1827,17 +1821,17 @@
lemma zorder_nonzero_div_power:
assumes sz: "open S" "z \<in> S" "f holomorphic_on S" "f z \<noteq> 0" and "n > 0"
- shows "zorder (\<lambda>w. f w / (w - z) ^ n) z = - n"
+ shows "zorder (\<lambda>w. f w / (w-z) ^ n) z = - n"
by (intro zorder_eqI [OF sz]) (simp add: inverse_eq_divide power_int_minus)
lemma zor_poly_eq:
assumes "isolated_singularity_at f z" "not_essential f z" "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
- shows "eventually (\<lambda>w. zor_poly f z w = f w * (w - z) powi - zorder f z) (at z)"
+ shows "eventually (\<lambda>w. zor_poly f z w = f w * (w-z) powi - zorder f z) (at z)"
proof -
- obtain r where r:"r>0"
- "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w - z) powi (zorder f z))"
+ obtain r where r: "r>0"
+ "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w-z) powi (zorder f z))"
using zorder_exist[OF assms] by blast
- then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w - z) powi - zorder f z"
+ then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w-z) powi - zorder f z"
by (auto simp: field_simps power_int_minus)
have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
using r eventually_at_ball'[of r z UNIV] by auto
@@ -1846,12 +1840,12 @@
lemma zor_poly_zero_eq:
assumes "f holomorphic_on S" "open S" "connected S" "z \<in> S" "\<exists>w\<in>S. f w \<noteq> 0"
- shows "eventually (\<lambda>w. zor_poly f z w = f w / (w - z) ^ nat (zorder f z)) (at z)"
+ shows "eventually (\<lambda>w. zor_poly f z w = f w / (w-z) ^ nat (zorder f z)) (at z)"
proof -
- obtain r where r:"r>0"
- "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w - z) ^ nat (zorder f z))"
+ obtain r where r: "r>0"
+ "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w-z) ^ nat (zorder f z))"
using zorder_exist_zero[OF assms] by auto
- then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w / (w - z) ^ nat (zorder f z)"
+ then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w / (w-z) ^ nat (zorder f z)"
by (auto simp: field_simps powr_minus)
have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
using r eventually_at_ball'[of r z UNIV] by auto
@@ -1859,15 +1853,15 @@
qed
lemma zor_poly_pole_eq:
- assumes f_iso:"isolated_singularity_at f z" "is_pole f z"
- shows "eventually (\<lambda>w. zor_poly f z w = f w * (w - z) ^ nat (- zorder f z)) (at z)"
+ assumes f_iso: "isolated_singularity_at f z" "is_pole f z"
+ shows "eventually (\<lambda>w. zor_poly f z w = f w * (w-z) ^ nat (- zorder f z)) (at z)"
proof -
- obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}"
+ obtain e where [simp]: "e>0" and f_holo: "f holomorphic_on ball z e - {z}"
using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast
- obtain r where r:"r>0"
- "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w / (w - z) ^ nat (- zorder f z))"
+ obtain r where r: "r>0"
+ "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w / (w-z) ^ nat (- zorder f z))"
using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>] by auto
- then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w - z) ^ nat (- zorder f z)"
+ then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w-z) ^ nat (- zorder f z)"
by (auto simp: field_simps)
have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
using r eventually_at_ball'[of r z UNIV] by auto
@@ -1892,7 +1886,7 @@
by eventually_elim (insert r, auto simp: field_simps power_int_minus)
moreover have "continuous_on (ball z0 r) (zor_poly f z0)"
using r by (intro holomorphic_on_imp_continuous_on) auto
- with r(1,2) have "isCont (zor_poly f z0) z0"
+ with r have "isCont (zor_poly f z0) z0"
by (auto simp: continuous_on_eq_continuous_at)
hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
unfolding isCont_def .
@@ -1935,7 +1929,7 @@
lemma zor_poly_pole_eqI:
fixes f :: "complex \<Rightarrow> complex" and z0 :: complex
defines "n \<equiv> zorder f z0"
- assumes f_iso:"isolated_singularity_at f z0" and "is_pole f z0"
+ assumes f_iso: "isolated_singularity_at f z0" and "is_pole f z0"
assumes lim: "((\<lambda>x. f (g x) * (g x - z0) ^ nat (-n)) \<longlongrightarrow> c) F"
assumes g: "filterlim g (at z0) F" and "F \<noteq> bot"
shows "zor_poly f z0 z0 = c"
@@ -1943,9 +1937,12 @@
obtain r where r: "r > 0" "zor_poly f z0 holomorphic_on cball z0 r"
proof -
have "\<exists>\<^sub>F w in at z0. f w \<noteq> 0"
- using non_zero_neighbour_pole[OF \<open>is_pole f z0\<close>] by (auto elim:eventually_frequentlyE)
- moreover have "not_essential f z0" unfolding not_essential_def using \<open>is_pole f z0\<close> by simp
- ultimately show ?thesis using that zorder_exist[OF f_iso,folded n_def] by auto
+ using non_zero_neighbour_pole[OF \<open>is_pole f z0\<close>]
+ by (auto elim: eventually_frequentlyE)
+ moreover have "not_essential f z0"
+ unfolding not_essential_def using \<open>is_pole f z0\<close> by simp
+ ultimately show ?thesis
+ using that zorder_exist[OF f_iso,folded n_def] by auto
qed
from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)"
using eventually_at_ball'[of r z0 UNIV] by auto
@@ -1979,15 +1976,15 @@
ultimately have "isolated_singularity_at f x"
by (auto simp: isolated_singularity_at_def analytic_on_open
intro!: exI[of _ r] holomorphic_on_subset[OF holo])
- hence ev: "\<forall>\<^sub>F w in at x. zor_poly f x w = f w * (w - x) ^ nat (- zorder f x)"
+ hence ev: "\<forall>\<^sub>F w in at x. zor_poly f x w = f w * (w-x) ^ nat (- zorder f x)"
using \<open>is_pole f x\<close> zor_poly_pole_eq by blast
define P where "P = zor_poly f x"
define n where "n = nat (-zorder f x)"
obtain r where r: "r > 0" "cball x r \<subseteq> A" "P holomorphic_on cball x r" "zorder f x < 0" "P x \<noteq> 0"
- "\<forall>w\<in>cball x r - {x}. f w = P w / (w - x) ^ n \<and> P w \<noteq> 0"
- unfolding P_def n_def using zorder_exist_pole[OF holo assms(2,3,1)] by blast
+ "\<forall>w\<in>cball x r - {x}. f w = P w / (w-x) ^ n \<and> P w \<noteq> 0"
+ using P_def assms holo n_def zorder_exist_pole by blast
have n: "n > 0"
using r(4) by (auto simp: n_def)
@@ -1995,7 +1992,7 @@
if "w \<in> ball x r" for w
using that by (intro holomorphic_derivI[OF holomorphic_on_subset[OF r(3), of "ball x r"]]) auto
- define D where "D = (\<lambda>w. (deriv P w * (w - x) - of_nat n * P w) / (w - x) ^ (n + 1))"
+ define D where "D = (\<lambda>w. (deriv P w * (w-x) - of_nat n * P w) / (w-x) ^ (n + 1))"
define n' where "n' = n - 1"
have n': "n = Suc n'"
using n by (simp add: n'_def)
@@ -2010,12 +2007,10 @@
have ev': "eventually (\<lambda>w. w \<in> ball x r - {x}) (nhds w)"
using w by (intro eventually_nhds_in_open) auto
- have "((\<lambda>w. P w / (w - x) ^ n) has_field_derivative D w) (at w)"
- apply (rule derivative_eq_intros refl | use w in force)+
- using w
- apply (simp add: divide_simps D_def)
- apply (simp add: n' algebra_simps)
- done
+ have \<section>: "(deriv P w * (w-x) ^ n - P w * (n * (w-x) ^ (n-1))) / ((w-x) ^ n * (w-x) ^ n) = D w"
+ using w n' by (simp add: divide_simps D_def) (simp add: algebra_simps)
+ have "((\<lambda>w. P w / (w-x) ^ n) has_field_derivative D w) (at w)"
+ by (rule derivative_eq_intros refl | use w \<section> in force)+
also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
using r by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
finally have "(f has_field_derivative D w) (at w)" .
@@ -2036,7 +2031,7 @@
proof (rule zorder_eqI)
show "open (ball x r)" "x \<in> ball x r"
using \<open>r > 0\<close> by auto
- show "f' w = (deriv P w * (w - x) - of_nat n * P w) * (w - x) powi (- int (Suc n))"
+ show "f' w = (deriv P w * (w-x) - of_nat n * P w) * (w-x) powi (- int (Suc n))"
if "w \<in> ball x r" "w \<noteq> x" for w
using that D_eq[of w] n by (auto simp: D_def power_int_diff power_int_minus powr_nat' divide_simps)
qed (use r n in \<open>auto intro!: holomorphic_intros\<close>)
@@ -2081,7 +2076,8 @@
qed
have "g holomorphic_on A"
- unfolding g_def using assms assms(1) holo by (intro removable_singularity) auto
+ unfolding g_def using assms assms(1) holo
+ by (intro removable_singularity) auto
hence "deriv g holomorphic_on A"
by (intro holomorphic_deriv assms)
hence "continuous_on A (deriv g)"
@@ -2124,15 +2120,12 @@
thus ?thesis
proof cases
case 1
- hence "is_pole f' x"
- using is_pole_deriv' assms by blast
- thus ?thesis by (auto simp: not_essential_def)
+ thus ?thesis
+ using assms is_pole_deriv' by blast
next
case (2 c)
- from 2 have "\<exists>c. f' \<midarrow>x\<rightarrow> c"
- by (rule removable_singularity_deriv'[OF _ assms(2-4)])
thus ?thesis
- by (auto simp: not_essential_def)
+ by (meson assms removable_singularity_deriv' tendsto_imp_not_essential)
qed
qed
@@ -2178,7 +2171,7 @@
next
case 2
have "filterlim (\<lambda>x. f (g x)) at_infinity sequentially"
- by (rule filterlim_compose[OF _ g(1)]) (use 2 in \<open>auto simp: is_pole_def\<close>)
+ using "2" filterlim_compose g(1) is_pole_def by blast
with fg have False
by (meson not_tendsto_and_filterlim_at_infinity sequentially_bot)
thus ?thesis ..
@@ -2241,13 +2234,14 @@
hence **: "f \<midarrow>x\<rightarrow> c"
by (simp add: tendsto_eventually)
show False
- using not_tendsto_and_filterlim_at_infinity[OF _ ** assms(1)[unfolded is_pole_def]] by simp
+ using ** \<open>is_pole f x\<close> at_neq_bot is_pole_def
+ not_tendsto_and_filterlim_at_infinity by blast
qed
lemma neg_zorder_imp_is_pole:
- assumes iso:"isolated_singularity_at f z" and f_ness:"not_essential f z"
- and "zorder f z < 0" and fre_nz:"\<exists>\<^sub>F w in at z. f w \<noteq> 0 "
+ assumes iso: "isolated_singularity_at f z" and f_ness: "not_essential f z"
+ and "zorder f z < 0" and fre_nz: "\<exists>\<^sub>F w in at z. f w \<noteq> 0 "
shows "is_pole f z"
proof -
define P where "P = zor_poly f z"
@@ -2255,24 +2249,23 @@
have "n<0" unfolding n_def by (simp add: assms(3))
define nn where "nn = nat (-n)"
- obtain r where "P z \<noteq> 0" "r>0" and r_holo:"P holomorphic_on cball z r" and
- w_Pn:"(\<forall>w\<in>cball z r - {z}. f w = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+ obtain r where r: "P z \<noteq> 0" "r>0" and r_holo: "P holomorphic_on cball z r" and
+ w_Pn: "(\<forall>w\<in>cball z r - {z}. f w = P w * (w-z) powi n \<and> P w \<noteq> 0)"
using zorder_exist[OF iso f_ness fre_nz,folded P_def n_def] by auto
- have "is_pole (\<lambda>w. P w * (w - z) powi n) z"
+ have "is_pole (\<lambda>w. P w * (w-z) powi n) z"
unfolding is_pole_def
proof (rule tendsto_mult_filterlim_at_infinity)
show "P \<midarrow>z\<rightarrow> P z"
- by (meson open_ball \<open>0 < r\<close> ball_subset_cball centre_in_ball
- continuous_on_eq_continuous_at continuous_on_subset
- holomorphic_on_imp_continuous_on isContD r_holo)
+ by (metis \<open>r>0\<close> r_holo centre_in_ball continuous_on_interior
+ holomorphic_on_imp_continuous_on interior_cball isContD)
show "P z\<noteq>0" by (simp add: \<open>P z \<noteq> 0\<close>)
have "LIM x at z. inverse ((x - z) ^ nat (-n)) :> at_infinity"
apply (subst filterlim_inverse_at_iff[symmetric])
using \<open>n<0\<close>
by (auto intro!:tendsto_eq_intros filterlim_atI
- simp add:eventually_at_filter)
+ simp add: eventually_at_filter)
then show "LIM x at z. (x - z) powi n :> at_infinity"
proof (elim filterlim_mono_eventually)
have "inverse ((x - z) ^ nat (-n)) = (x - z) powi n"
@@ -2283,18 +2276,18 @@
by (simp add: eventually_at_filter)
qed auto
qed
- moreover have "\<forall>\<^sub>F w in at z. f w = P w * (w - z) powi n"
+ moreover have "\<forall>\<^sub>F w in at z. f w = P w * (w-z) powi n"
unfolding eventually_at_le
using w_Pn \<open>r>0\<close> by (force simp add: dist_commute)
ultimately show ?thesis using is_pole_cong by fast
qed
lemma is_pole_divide_zorder:
- 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"
- and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+ 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"
+ and f_ness: "not_essential f z" and g_ness: "not_essential g z"
and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
- and z_less:"zorder f z < zorder g z"
+ and z_less: "zorder f z < zorder g z"
shows "is_pole (\<lambda>z. f z / g z) z"
proof -
define fn gn fg where "fn=zorder f z" and "gn=zorder g z"
@@ -2302,15 +2295,15 @@
have "isolated_singularity_at fg z"
unfolding fg_def using f_iso g_iso g_ness
- by (auto intro:singularity_intros)
+ by (auto intro: singularity_intros)
moreover have "not_essential fg z"
unfolding fg_def using f_iso g_iso g_ness f_ness
- by (auto intro:singularity_intros)
+ by (auto intro: singularity_intros)
moreover have "zorder fg z < 0"
proof -
have "zorder fg z = fn - gn"
- using zorder_divide[OF f_iso g_iso f_ness g_ness
- fg_nconst,folded fn_def gn_def fg_def] .
+ using zorder_divide[OF f_iso g_iso f_ness g_ness fg_nconst]
+ by (simp add: fg_def fn_def gn_def)
then show ?thesis
using z_less by (simp add: fn_def gn_def)
qed
@@ -2321,7 +2314,7 @@
qed
lemma isolated_pole_imp_nzero_times:
- assumes f_iso:"isolated_singularity_at f z"
+ assumes f_iso: "isolated_singularity_at f z"
and "is_pole f z"
shows "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
proof (rule ccontr)
@@ -2350,30 +2343,30 @@
by (meson analytic_deriv assms isolated_singularity_at_def)
lemma zorder_deriv_minus_1:
- fixes f g::"complex \<Rightarrow> complex" and z::complex
- assumes f_iso:"isolated_singularity_at f z"
- and f_ness:"not_essential f z"
- and f_nconst:"\<exists>\<^sub>F w in at z. f w \<noteq> 0"
- and f_ord:"zorder f z \<noteq>0"
+ fixes f g:: "complex \<Rightarrow> complex" and z::complex
+ assumes f_iso: "isolated_singularity_at f z"
+ and f_ness: "not_essential f z"
+ and f_nconst: "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ and f_ord: "zorder f z \<noteq>0"
shows "zorder (deriv f) z = zorder f z - 1"
proof -
define P where "P = zor_poly f z"
define n where "n = zorder f z"
have "n\<noteq>0" unfolding n_def using f_ord by auto
- obtain r where "P z \<noteq> 0" "r>0" and P_holo:"P holomorphic_on cball z r"
+ obtain r where "P z \<noteq> 0" "r>0" and P_holo: "P holomorphic_on cball z r"
and "(\<forall>w\<in>cball z r - {z}. f w
- = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+ = P w * (w-z) powi n \<and> P w \<noteq> 0)"
using zorder_exist[OF f_iso f_ness f_nconst,folded P_def n_def] by auto
from this(4)
- have f_eq:"(\<forall>w\<in>cball z r - {z}. f w
- = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+ have f_eq: "(\<forall>w\<in>cball z r - {z}. f w
+ = P w * (w-z) powi n \<and> P w \<noteq> 0)"
using complex_powr_of_int f_ord n_def by presburger
- define D where "D = (\<lambda>w. (deriv P w * (w - z) + of_int n * P w)
- * (w - z) powi (n - 1))"
+ define D where "D = (\<lambda>w. (deriv P w * (w-z) + of_int n * P w)
+ * (w-z) powi (n - 1))"
- have deriv_f_eq:"deriv f w = D w" if "w \<in> ball z r - {z}" for w
+ have deriv_f_eq: "deriv f w = D w" if "w \<in> ball z r - {z}" for w
proof -
have ev': "eventually (\<lambda>w. w \<in> ball z r - {z}) (nhds w)"
using that by (intro eventually_nhds_in_open) auto
@@ -2384,11 +2377,10 @@
moreover have "(P has_field_derivative deriv P w) (at w)"
by (meson DiffD1 Elementary_Metric_Spaces.open_ball P_holo
ball_subset_cball holomorphic_derivI holomorphic_on_subset that)
- ultimately have "((\<lambda>w. P w * (w - z) powi n) has_field_derivative D w) (at w)"
+ ultimately have "((\<lambda>w. P w * (w-z) powi n) has_field_derivative D w) (at w)"
unfolding D_def using that
apply (auto intro!: derivative_eq_intros)
- apply (fold wz_def)
- by (auto simp:algebra_simps simp flip:power_int_add_1')
+ by (auto simp: algebra_simps simp flip:power_int_add_1' wz_def)
also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
using f_eq
by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
@@ -2402,14 +2394,13 @@
proof (rule zorder_eqI)
show "open (ball z r)" "z \<in> ball z r"
using \<open>r > 0\<close> by auto
- define g where "g=(\<lambda>w. (deriv P w * (w - z) + of_int n * P w))"
+ define g where "g=(\<lambda>w. (deriv P w * (w-z) + of_int n * P w))"
show "g holomorphic_on ball z r"
unfolding g_def using P_holo
by (auto intro!:holomorphic_intros)
show "g z \<noteq> 0"
unfolding g_def using \<open>P z \<noteq> 0\<close> \<open>n\<noteq>0\<close> by auto
- show "deriv f w =
- (deriv P w * (w - z) + of_int n * P w) * (w - z) powi (n - 1)"
+ show "deriv f w = (deriv P w * (w-z) + of_int n * P w) * (w-z) powi (n - 1)"
if "w \<in> ball z r" "w \<noteq> z" for w
using D_def deriv_f_eq that by blast
qed
@@ -2417,20 +2408,19 @@
lemma deriv_divide_is_pole: \<comment>\<open>Generalises @{thm zorder_deriv}\<close>
- fixes f g::"complex \<Rightarrow> complex" and z::complex
- assumes f_iso:"isolated_singularity_at f z"
- and f_ness:"not_essential f z"
+ fixes f g:: "complex \<Rightarrow> complex" and z::complex
+ assumes f_iso: "isolated_singularity_at f z"
+ and f_ness: "not_essential f z"
and fg_nconst: "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
- and f_ord:"zorder f z \<noteq>0"
+ and f_ord: "zorder f z \<noteq>0"
shows "is_pole (\<lambda>z. deriv f z / f z) z"
proof (rule neg_zorder_imp_is_pole)
define ff where "ff=(\<lambda>w. deriv f w / f w)"
show "isolated_singularity_at ff z"
using f_iso f_ness unfolding ff_def
- by (auto intro:singularity_intros)
+ by (auto intro: singularity_intros)
show "not_essential ff z"
- unfolding ff_def using f_ness f_iso
- by (auto intro:singularity_intros)
+ unfolding ff_def using f_ness f_iso by (auto intro: singularity_intros)
have "zorder ff z = zorder (deriv f) z - zorder f z"
unfolding ff_def using f_iso f_ness fg_nconst
@@ -2444,8 +2434,8 @@
qed
lemma is_pole_deriv_divide_is_pole:
- fixes f g::"complex \<Rightarrow> complex" and z::complex
- assumes f_iso:"isolated_singularity_at f z"
+ fixes f g:: "complex \<Rightarrow> complex" and z::complex
+ assumes f_iso: "isolated_singularity_at f z"
and "is_pole f z"
shows "is_pole (\<lambda>z. deriv f z / f z) z"
proof (rule deriv_divide_is_pole[OF f_iso])
--- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy Sun Jan 19 18:18:07 2025 +0000
+++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy Wed Jan 22 22:22:27 2025 +0000
@@ -63,8 +63,10 @@
qed
show ?thesis
unfolding Moebius_function_def
- apply (intro holomorphic_intros)
- by (metis "*" mult.commute complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 right_minus_eq)
+ proof (intro holomorphic_intros)
+ show "\<And>z. z \<in> ball 0 1 \<Longrightarrow> 1 - cnj w * z \<noteq> 0"
+ by (metis * complex_cnj_cnj complex_cnj_mult complex_mod_cnj mem_ball_0 mult.commute mult_1 right_minus_eq)
+ qed
qed
lemma Moebius_function_compose:
@@ -80,7 +82,7 @@
have "w2 * cnj w2 = 1"
using that meq by (auto simp: algebra_simps)
then show "z = 0"
- by (metis (no_types) \<open>cmod w2 < 1\<close> complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one)
+ using \<open>cmod w2 < 1\<close> complex_mod_sqrt_Re_mult_cnj by force
qed
moreover have "z - w2 - w1 * (1 - cnj w2 * z) = z * (1 - cnj w2 * z - cnj w1 * (z - w2))"
using meq by (fastforce simp: algebra_simps)
@@ -151,10 +153,9 @@
by force
have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
if "z \<in> ball 0 1" for z::complex
- proof (rule DERIV_chain' [where g=f])
- show "(f has_field_derivative deriv f (of_real r * z)) (at (of_real r * z))"
- by (metis holomorphic_derivI [OF holF \<open>open S\<close>] \<open>f \<in> F\<close> image_subset_iff r01 that)
- qed simp
+ using DERIV_chain' [where g=f] \<open>open S\<close>
+ by (meson DERIV_cmult_Id \<open>f \<in> F\<close> holF holomorphic_derivI image_subset_iff
+ r01 that)
have df0: "((\<lambda>w. f (r * w)) has_field_derivative deriv f 0 * r) (at 0)"
using * [of 0] by simp
have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
@@ -316,12 +317,7 @@
qed
qed
have norm\<psi>1: "norm(\<psi> (h (f z))) < 1" if "z \<in> S" for z
- proof -
- have "norm (\<psi> (h (f z)) ^ 2) < 1"
- by (metis (no_types) that DIM_complex \<psi>2 h01 image_subset_iff mem_ball_0 nf1)
- then show ?thesis
- by (metis le_less_trans mult_less_cancel_left2 norm_ge_zero norm_power not_le power2_eq_square)
- qed
+ by (metis \<psi>2 h01 image_subset_iff mem_ball_0 nf1 norm_power power_less1_D that)
then have \<psi>01: "\<psi> (h (f 0)) \<in> ball 0 1"
by (simp add: \<open>0 \<in> S\<close>)
obtain p q where p0: "p (\<psi> (h (f 0))) = 0"
@@ -535,7 +531,7 @@
using gxy by (auto simp: path_image_join)
qed (use gxy holf in auto)
then have fintxy: "f contour_integrable_on linepath x y"
- by (metis (no_types, lifting) contour_integrable_joinD1 contour_integrable_joinD2 gxy(2) has_contour_integral_integrable pathfinish_linepath pathstart_reversepath valid_path_imp_reverse valid_path_join valid_path_linepath vp(2))
+ using gxy(2) has_contour_integral_integrable vp by fastforce
have fintgx: "f contour_integrable_on (?g x)" "f contour_integrable_on (?g y)"
using openS contour_integrable_holomorphic_simple gxy holf vp by blast+
show ?thesis
@@ -671,8 +667,8 @@
unfolding norm_divide
using \<open>r > 0\<close> g_not_r [OF \<open>z \<in> S\<close>] g_not_r [OF \<open>a \<in> S\<close>]
by (simp_all add: field_split_simps dist_commute dist_norm)
- then show "?f ` S \<subseteq> ball 0 1"
- by auto
+ then show "?f ` S \<subseteq> ball 0 1"
+ by auto
show "inj_on ?f S"
using \<open>r > 0\<close> eqg apply (clarsimp simp: inj_on_def)
by (metis diff_add_cancel)
@@ -697,7 +693,7 @@
proof (intro exI conjI)
show "g \<circ> k holomorphic_on h ` S"
by (smt (verit) holg holk holomorphic_on_compose holomorphic_on_subset imageE image_subset_iff kh)
- show "\<forall>z\<in>h ` S. f z = ((g \<circ> k) z)\<^sup>2"
+ show "\<forall>z \<in> h ` S. f z = ((g \<circ> k) z)\<^sup>2"
using eqg kh by auto
qed
qed
@@ -714,22 +710,13 @@
qed
lemma homeomorphic_to_disc:
- assumes S: "S \<noteq> {}"
- and prev: "S = UNIV \<or>
+ assumes "S = UNIV \<or>
(\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
- (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
- (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
+ (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
+ (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
shows "S homeomorphic ball (0::complex) 1"
- using prev
-proof
- assume "S = UNIV" then show ?thesis
- using homeomorphic_ball01_UNIV homeomorphic_sym by blast
-next
- assume ?P
- then show ?thesis
- unfolding homeomorphic_minimal
- using holomorphic_on_imp_continuous_on by blast
-qed
+ by (smt (verit, ccfv_SIG) holomorphic_on_imp_continuous_on homeomorphic_ball01_UNIV
+ homeomorphic_minimal assms)
lemma homeomorphic_to_disc_imp_simply_connected:
assumes "S = {} \<or> S homeomorphic ball (0::complex) 1"
@@ -900,15 +887,11 @@
using n \<open>cmod x < 1\<close> by (auto simp: field_split_simps algebra_simps D_def)
moreover have " f ` D n \<inter> closure (f ` A n) = {}"
proof -
- have op_fDn: "open(f ` (D n))"
- proof (rule invariance_of_domain)
- show "continuous_on (D n) f"
- by (rule continuous_on_subset [OF contf D01])
- show "open (D n)"
- by (simp add: D_def)
- show "inj_on f (D n)"
- unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
- qed
+ have"inj_on f (D n)"
+ unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
+ then have op_fDn: "open(f ` (D n))"
+ by (metis invariance_of_domain D_def Elementary_Metric_Spaces.open_ball
+ continuous_on_subset [OF contf D01])
have injf: "inj_on f (ball 0 1)"
by (metis mem_ball_0 inj_on_def gf)
have "D n \<union> A n \<subseteq> ball 0 1"
@@ -992,9 +975,9 @@
by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K)
qed (use \<open>compact L\<close> \<open>C \<subseteq> L\<close> in auto)
qed
- obtain U V where "open U" and "compact (closure U)" and "open V" "K \<subseteq> U"
- and V: "\<Inter>(range X) - K \<subseteq> V" and "U \<inter> V = {}"
- using separation_normal_compact [OF \<open>compact K\<close> clo] by blast
+ obtain U V where "open U" "open V" and "compact (closure U)"
+ and V: "\<Inter>(range X) - K \<subseteq> V" and U: "K \<subseteq> U" "U \<inter> V = {}"
+ by (metis Diff_disjoint separation_normal_compact [OF \<open>compact K\<close> clo])
then have "U \<inter> (\<Inter> (range X) - K) = {}"
by blast
have "(closure U - U) \<inter> (\<Inter>n. X n \<inter> closure U) \<noteq> {}"
@@ -1049,12 +1032,8 @@
moreover have "(\<Inter>n. X n \<inter> closure U) = (\<Inter>n. X n) \<inter> closure U"
by blast
moreover have "x \<in> U" if "\<And>n. x \<in> X n" "x \<in> closure U" for x
- proof -
- have "x \<notin> V"
- using \<open>U \<inter> V = {}\<close> \<open>open V\<close> closure_iff_nhds_not_empty that(2) by blast
- then show ?thesis
- by (metis (no_types) Diff_iff INT_I V \<open>K \<subseteq> U\<close> subsetD that(1))
- qed
+ by (metis Diff_iff INT_I U V \<open>open V\<close> closure_iff_nhds_not_empty
+ order.refl subsetD that)
ultimately show False
by (auto simp: open_Int_closure_eq_empty [OF \<open>open V\<close>, of U])
qed
@@ -1101,7 +1080,7 @@
moreover have "closed C"
using C_ccsw clo_ccs by blast
ultimately show False
- by (metis C False \<open>S \<noteq> UNIV\<close> C_ccsw bot_eq_sup_iff connected_component_eq_UNIV frontier_Int_closed
+ by (metis C \<open>S \<noteq> {}\<close> \<open>S \<noteq> UNIV\<close> C_ccsw bot_eq_sup_iff connected_component_eq_UNIV frontier_Int_closed
frontier_closed frontier_complement frontier_eq_empty frontier_of_components_subset in_components_maximal inf.orderE)
qed
then show "connected_component_set (- S) w \<inter> frontier S \<noteq> {}"
@@ -1114,14 +1093,18 @@
by (auto simp: closed_Compl closed_connected_component frontier_def openS)
show "frontier (connected_component_set (- S) z) \<subseteq> frontier (- S)"
using frontier_of_connected_component_subset by fastforce
- have "\<not> bounded (-S)"
+ have "connected (closure S - S)"
+ by (metis confr frontier_def interior_open openS)
+ moreover have "\<not> bounded (-S)"
by (simp add: True cobounded_imp_unbounded)
+ moreover have "bounded (connected_component_set (- S) w)"
+ using C_ccsw \<open>bounded C\<close> by auto
+ ultimately have "z \<notin> S"
+ using \<open>w \<notin> S\<close> openS
+ by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset
+ connected_component_eq_self connected_diff_open_from_closed subset_UNIV)
then have "connected_component_set (- S) z \<noteq> {}"
- unfolding connected_component_eq_empty
- using confr openS \<open>bounded C\<close> \<open>w \<notin> S\<close>
- apply (simp add: frontier_def interior_open C_ccsw)
- by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset connected_component_eq_self
- connected_diff_open_from_closed subset_UNIV)
+ by (metis ComplI connected_component_eq_empty)
then show "frontier (connected_component_set (- S) z) \<noteq> {}"
by (metis False \<open>S \<noteq> UNIV\<close> connected_component_eq_UNIV frontier_complement frontier_eq_empty)
qed
@@ -1285,8 +1268,8 @@
obtain \<delta> where "0 < \<delta>" "\<And>w. \<lbrakk>w \<in> S; dist w z < \<delta>\<rbrakk> \<Longrightarrow> dist (g w) (g z) < cmod (g z)"
using contg [unfolded continuous_on_iff] by (metis \<open>g z \<noteq> 0\<close> \<open>z \<in> S\<close> zero_less_norm_iff)
then have \<delta>: "\<And>w. \<lbrakk>w \<in> S; w \<in> ball z \<delta>\<rbrakk> \<Longrightarrow> g w + g z \<noteq> 0"
- apply (clarsimp simp: dist_norm)
- by (metis add_diff_cancel_left' dist_0_norm dist_complex_def less_le_not_le norm_increases_online norm_minus_commute)
+ by (metis add.commute add_cancel_right_left dist_commute dist_complex_def mem_ball
+ norm_increases_online norm_not_less_zero norm_zero order_less_asym)
have *: "(\<lambda>x. (f x - f z) / (x - z) / (g x + g z)) \<midarrow>z\<rightarrow> deriv f z / (g z + g z)"
proof (intro tendsto_intros)
show "(\<lambda>x. (f x - f z) / (x - z)) \<midarrow>z\<rightarrow> deriv f z"
@@ -1303,10 +1286,9 @@
using \<open>z \<in> S\<close> \<open>0 < \<delta>\<close> by simp
show "\<And>x. \<lbrakk>x \<in> ball z \<delta> \<inter> S; x \<noteq> z\<rbrakk>
\<Longrightarrow> (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)"
- using \<delta>
- apply (simp add: geq \<open>z \<in> S\<close> divide_simps)
- apply (auto simp: algebra_simps power2_eq_square)
- done
+ using \<delta> \<open>z \<in> S\<close>
+ apply (simp add: geq field_split_simps power2_eq_square)
+ by (metis distrib_left mult_cancel_right)
qed
then show "\<exists>f'. (g has_field_derivative f') (at z)" ..
qed
@@ -1401,7 +1383,7 @@
assume g: "g holomorphic_on ball 0 1" "\<forall>z\<in>ball 0 1. g z \<in> S \<and> f (g z) = z"
and "\<forall>z\<in>S. cmod (f z) < 1 \<and> g (f z) = z"
then have "S = g ` (ball 0 1)"
- by (force simp:)
+ by force
then have "open S"
by (metis open_ball g inj_on_def open_mapping_thm3)
}
@@ -1480,9 +1462,10 @@
proof -
have "closed_segment t u \<subseteq> {0..1}"
using closed_segment_eq_real_ivl t that by auto
+ then have "\<And>r. \<lbrakk>r \<in> closed_segment t u\<rbrakk> \<Longrightarrow> dist (p t) (p r) < cmod (p t - \<zeta>)"
+ by (smt (verit, best) d dist_commute dist_in_closed_segment subsetD \<open>dist u t < d\<close>)
then have piB: "path_image(subpath t u p) \<subseteq> ?B"
- apply (clarsimp simp add: path_image_subpath_gen)
- by (metis subsetD le_less_trans \<open>dist u t < d\<close> d dist_commute dist_in_closed_segment)
+ by (auto simp: path_image_subpath_gen)
have *: "path (g \<circ> subpath t u p)"
proof (rule path_continuous_image)
show "path (subpath t u p)"
@@ -1561,9 +1544,7 @@
qed
show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
by (rule continuous_intros)+
- show "(\<lambda>w. \<zeta> + exp w) \<in> UNIV \<rightarrow> -{\<zeta>}"
- by auto
- qed
+ qed auto
then have "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"