theory Complex_Singularities
imports Conformal_Mappings
begin
subsection \<open>Non-essential singular points\<close>
definition\<^marker>\<open>tag important\<close> is_pole ::
"('a::topological_space \ 'b::real_normed_vector) \ 'a \ bool" where
"is_pole f a = (LIM x (at a). f x :> at_infinity)"
lemma is_pole_cong:
assumes "eventually (\x. f x = g x) (at a)" "a=b"
shows "is_pole f a \ is_pole g b"
unfolding is_pole_def using assms by (intro filterlim_cong,auto)
lemma is_pole_transform:
assumes "is_pole f a" "eventually (\x. f x = g x) (at a)" "a=b"
shows "is_pole g b"
using is_pole_cong assms by auto
lemma is_pole_tendsto:
fixes f::"('a::topological_space \ 'b::real_normed_div_algebra)"
shows "is_pole f x \ ((inverse o f) \ 0) (at x)"
unfolding is_pole_def
by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
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:"\x\s-{z}. f x\0"
shows "(\x. if x=z then 0 else inverse (f x)) holomorphic_on s"
proof -
define g where "g \ \x. if x=z then 0 else inverse (f x)"
have "isCont g z" unfolding isCont_def using is_pole_tendsto[OF pole]
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)
hence "continuous_on (s-{z}) g" unfolding g_def
apply (subst continuous_on_cong[where t="s-{z}" and g="inverse o f"])
by auto
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)
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)
hence "g holomorphic_on (s-{z})"
apply (subst holomorphic_cong[where t="s-{z}" and g="inverse o f"])
by (auto simp add:g_def)
ultimately show ?thesis unfolding g_def using \<open>open s\<close>
by (auto elim!: no_isolated_singularity)
qed
lemma not_is_pole_holomorphic:
assumes "open A" "x \ A" "f holomorphic_on A"
shows "\is_pole f x"
proof -
have "continuous_on A f" by (intro holomorphic_on_imp_continuous_on) fact
with assms have "isCont f x" by (simp add: continuous_on_eq_continuous_at)
hence "f \x\ f x" by (simp add: isCont_def)
thus "\is_pole f x" unfolding is_pole_def
using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto
qed
lemma is_pole_inverse_power: "n > 0 \ is_pole (\z::complex. 1 / (z - a) ^ n) a"
unfolding is_pole_def inverse_eq_divide [symmetric]
by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
(auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)
lemma is_pole_inverse: "is_pole (\z::complex. 1 / (z - a)) a"
using is_pole_inverse_power[of 1 a] by simp
lemma is_pole_divide:
fixes f :: "'a :: t2_space \ 'b :: real_normed_field"
assumes "isCont f z" "filterlim g (at 0) (at z)" "f z \ 0"
shows "is_pole (\z. f z / g z) z"
proof -
have "filterlim (\z. f z * inverse (g z)) at_infinity (at z)"
by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"]
filterlim_compose[OF filterlim_inverse_at_infinity])+
(insert assms, auto simp: isCont_def)
thus ?thesis by (simp add: field_split_simps is_pole_def)
qed
lemma is_pole_basic:
assumes "f holomorphic_on A" "open A" "z \ A" "f z \ 0" "n > 0"
shows "is_pole (\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 (\w. (w - z) ^ n) (nhds 0) (at z)"
using assms by (auto intro!: tendsto_eq_intros)
thus "filterlim (\w. (w - z) ^ n) (at 0) (at z)"
by (intro filterlim_atI tendsto_eq_intros)
(insert assms, auto simp: eventually_at_filter)
qed fact+
lemma is_pole_basic':
assumes "f holomorphic_on A" "open A" "0 \ A" "f 0 \ 0" "n > 0"
shows "is_pole (\w. f w / w ^ n) 0"
using is_pole_basic[of f A 0] assms by simp
text \<open>The proposition
\<^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 \ complex, complex] \ bool" where
"not_essential f z = (\x. f\z\x \ is_pole f z)"
definition isolated_singularity_at::"[complex \ complex, complex] \ bool" where
"isolated_singularity_at f z = (\r>0. f analytic_on ball z r-{z})"
named_theorems singularity_intros "introduction rules for singularities"
lemma holomorphic_factor_unique:
fixes f::"complex \ complex" and z::complex and r::real and m n::int
assumes "r>0" "g z\0" "h z\0"
and asm:"\w\ball z r-{z}. f w = g w * (w-z) powr n \ g w\0 \ f w = h w * (w - z) powr m \ h w\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 \ bot" using \r>0\
by (auto simp add:at_within_ball_bot_iff)
have False when "n>m"
proof -
have "(h \ 0) (at z within ball z r)"
proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (n - m) * g w"])
have "\w\ball z r-{z}. h w = (w-z)powr(n-m) * g w"
using \<open>n>m\<close> asm \<open>r>0\<close>
apply (auto simp add:field_simps powr_diff)
by force
then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\
\<Longrightarrow> (x' - z) powr (n - m) * g x' = h x'" for x' by auto
next
define F where "F \ at z within ball z r"
define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
apply (subst Lim_ident_at)
using \<open>n>m\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \ 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(g \ g z) F"
using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \<open>r>0\<close>
unfolding F_def by auto
ultimately show " ((\w. f' w * g w) \ 0) F" using tendsto_mult by fastforce
qed
moreover have "(h \ 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>)
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 \ 0) (at z within ball z r)"
proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (m - n) * h w"])
have "\w\ball z r -{z}. g w = (w-z) powr (m-n) * h w" using \m>n\ asm
apply (auto simp add:field_simps powr_diff)
by force
then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\
\<Longrightarrow> (x' - z) powr (m - n) * h x' = g x'" for x' by auto
next
define F where "F \ at z within ball z r"
define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
apply (subst Lim_ident_at)
using \<open>m>n\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \ 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(h \ h z) F"
using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close>
unfolding F_def by auto
ultimately show " ((\w. f' w * h w) \ 0) F" using tendsto_mult by fastforce
qed
moreover have "(g \ 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>)
ultimately have "g z=0" by (auto intro!: tendsto_unique)
thus False using \<open>g z\<noteq>0\<close> by auto
qed
ultimately show "n=m" by fastforce
qed
lemma holomorphic_factor_puncture:
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:"\\<^sub>Fw in (at z). f w\0" \ \\<^term>\f\ will not be constantly zero in a neighbour of \<^term>\z\\
shows "\!n::int. \g r. 0 < r \ g holomorphic_on cball z r \ g z\0
\<and> (\<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powr n \<and> g w\<noteq>0)"
proof -
define P where "P = (\f n g r. 0 < r \ g holomorphic_on cball z r \ g z\0
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr (of_int n) \<and> g w\<noteq>0))"
have imp_unique:"\!n::int. \g r. P f n g r" when "\n g r. P f n g r"
proof (rule ex_ex1I[OF that])
fix n1 n2 :: int
assume g1_asm:"\g1 r1. P f n1 g1 r1" and g2_asm:"\g2 r2. P f n2 g2 r2"
define fac where "fac \ \n g r. \w\cball z r-{z}. f w = g w * (w - z) powr (of_int n) \ g w \ 0"
obtain g1 r1 where "0 < r1" and g1_holo: "g1 holomorphic_on cball z r1" and "g1 z\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\0"
and "fac n2 g2 r2" using g2_asm unfolding P_def fac_def 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
moreover have "\w\ball z r-{z}. f w = g1 w * (w-z) powr n1 \ g1 w\0
\<and> f w = g2 w * (w - z) powr 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)
qed
have P_exist:"\ n g r. P h n g r" when
"\z'. (h \ z') (at z)" "isolated_singularity_at h z" "\\<^sub>Fw in (at z). h w\0"
for h
proof -
from that(2) obtain r where "r>0" "h analytic_on ball z r - {z}"
unfolding isolated_singularity_at_def by auto
obtain z' where "(h \ z') (at z)" using \\z'. (h \ z') (at z)\ by auto
define h' where "h'=(\<lambda>x. if x=z then z' else h x)"
have "h' holomorphic_on ball z r"
apply (rule no_isolated_singularity'[of "{z}"])
subgoal by (metis LIM_equal Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> empty_iff h'_def insert_iff)
subgoal using \<open>h analytic_on ball z r - {z}\<close> analytic_imp_holomorphic h'_def holomorphic_transform
by fastforce
by auto
have ?thesis when "z'=0"
proof -
have "h' z=0" using that unfolding h'_def by auto
moreover have "\ h' constant_on ball z r"
using \<open>\<exists>\<^sub>Fw in (at z). h w\<noteq>0\<close> unfolding constant_on_def frequently_def eventually_at h'_def
apply simp
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 \ ball z r" and
g:"g holomorphic_on ball z r1"
"\w. w \ ball z r1 \ h' w = (w - z) ^ n * g w"
"\w. w \ ball z r1 \ g w \ 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)
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)
then have "P h n g rr"
unfolding h'_def P_def by auto
then show ?thesis unfolding P_def by blast
qed
moreover have ?thesis when "z'\0"
proof -
have "h' z\0" using that unfolding h'_def by auto
obtain r1 where "r1>0" "cball z r1 \ ball z r" "\x\cball z r1. h' x\0"
proof -
have "isCont h' z" "h' z\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" "\x\ball z r2. h' x\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 \ ball z r"
using \<open>r2>0\<close> \<open>r>0\<close> unfolding r1_def by auto
moreover have "\x\cball z r1. h' x \ 0"
using r2 unfolding r1_def by simp
ultimately show ?thesis using that by auto
qed
then have "P h' 0 h' r1" using \<open>h' holomorphic_on ball z r\<close> unfolding P_def by auto
then have "P h 0 h' r1" unfolding P_def h'_def by auto
then show ?thesis unfolding P_def by blast
qed
ultimately show ?thesis by auto
qed
have ?thesis when "\x. (f \ x) (at z)"
apply (rule_tac imp_unique[unfolded P_def])
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: "\x\ball z e-{z}. f x\0"
proof -
have "\\<^sub>F z in at z. f z \ 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" "\x\ball z e1-{z}. f x\0"
using that eventually_at[of "\x. f x\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
define e where "e=min e1 e2"
show ?thesis
apply (rule that[of e])
using e1 e2 unfolding e_def by auto
qed
define h where "h \ \x. inverse (f x)"
have "\n g r. P h n g r"
proof -
have "h \z\ 0"
using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce
moreover have "\\<^sub>Fw in (at z). h w\0"
using non_zero
apply (elim frequently_rev_mp)
unfolding h_def eventually_at by (auto intro:exI[where x=1])
moreover have "isolated_singularity_at h z"
unfolding isolated_singularity_at_def h_def
apply (rule exI[where x=e])
using e_holo e_nz \<open>e>0\<close> by (metis open_ball analytic_on_open
holomorphic_on_inverse open_delete)
ultimately show ?thesis
using P_exist[of h] by auto
qed
then obtain n g r
where "0 < r" and
g_holo:"g holomorphic_on cball z r" and "g z\0" and
g_fac:"(\w\cball z r-{z}. h w = g w * (w - z) powr of_int n \ g w \ 0)"
unfolding P_def by auto
have "P f (-n) (inverse o g) r"
proof -
have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\cball z r - {z}" for w
using g_fac[rule_format,of w] that unfolding h_def
apply (auto simp add:powr_minus )
by (metis inverse_inverse_eq inverse_mult_distrib)
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)
qed
then show "\x g r. 0 < r \ g holomorphic_on cball z r \ g z \ 0
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int 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
qed
lemma not_essential_transform:
assumes "not_essential g z"
assumes "\\<^sub>F w in (at z). g w = f w"
shows "not_essential f z"
using assms unfolding not_essential_def
by (simp add: filterlim_cong is_pole_cong)
lemma isolated_singularity_at_transform:
assumes "isolated_singularity_at g z"
assumes "\\<^sub>F w in (at z). g w = f w"
shows "isolated_singularity_at f z"
proof -
obtain r1 where "r1>0" and r1:"g analytic_on ball z r1 - {z}"
using assms(1) unfolding isolated_singularity_at_def by auto
obtain r2 where "r2>0" and r2:" \x. x \ z \ dist x z < r2 \ g x = f x"
using assms(2) unfolding eventually_at by auto
define r3 where "r3=min r1 r2"
have "r3>0" unfolding r3_def using \<open>r1>0\<close> \<open>r2>0\<close> by auto
moreover have "f analytic_on ball z r3 - {z}"
proof -
have "g holomorphic_on ball z r3 - {z}"
using r1 unfolding r3_def by (subst (asm) analytic_on_open,auto)
then have "f holomorphic_on ball z r3 - {z}"
using r2 unfolding r3_def
by (auto simp add:dist_commute elim!:holomorphic_transform)
then show ?thesis by (subst analytic_on_open,auto)
qed
ultimately show ?thesis unfolding isolated_singularity_at_def by auto
qed
lemma not_essential_powr[singularity_intros]:
assumes "LIM w (at z). f w :> (at x)"
shows "not_essential (\w. (f w) powr (of_int n)) z"
proof -
define fp where "fp=(\w. (f w) powr (of_int n))"
have ?thesis when "n>0"
proof -
have "(\w. (f w) ^ (nat n)) \z\ x ^ nat n"
using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
then have "fp \z\ x ^ nat n" unfolding fp_def
apply (elim Lim_transform_within[where d=1],simp)
by (metis less_le powr_0 powr_of_int that zero_less_nat_eq zero_power)
then show ?thesis unfolding not_essential_def fp_def by auto
qed
moreover have ?thesis when "n=0"
proof -
have "fp \z\ 1 "
apply (subst tendsto_cong[where g="\_.1"])
using that filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def by auto
then show ?thesis unfolding fp_def not_essential_def by auto
qed
moreover have ?thesis when "n<0"
proof (cases "x=0")
case True
have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
apply (subst filterlim_inverse_at_iff[symmetric],simp)
apply (rule filterlim_atI)
subgoal using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
subgoal using filterlim_at_within_not_equal[OF assms,of 0]
by (eventually_elim,insert that,auto)
done
then have "LIM w (at z). fp w :> at_infinity"
proof (elim filterlim_mono_eventually)
show "\\<^sub>F x in at z. inverse (f x ^ nat (- n)) = fp x"
using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def
apply eventually_elim
using powr_of_int that by auto
qed auto
then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto
next
case False
let ?xx= "inverse (x ^ (nat (-n)))"
have "(\w. inverse ((f w) ^ (nat (-n)))) \z\?xx"
using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
then have "fp \z\?xx"
apply (elim Lim_transform_within[where d=1],simp)
unfolding fp_def by (metis inverse_zero nat_mono_iff nat_zero_as_int neg_0_less_iff_less
not_le power_eq_0_iff powr_0 powr_of_int that)
then show ?thesis unfolding fp_def not_essential_def by auto
qed
ultimately show ?thesis by linarith
qed
lemma isolated_singularity_at_powr[singularity_intros]:
assumes "isolated_singularity_at f z" "\\<^sub>F w in (at z). f w\0"
shows "isolated_singularity_at (\w. (f w) powr (of_int n)) z"
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}"
using analytic_on_open[of "ball z r1-{z}" f] by blast
obtain r2 where "r2>0" and r2:"\w. w \ z \ dist w z < r2 \ f w \ 0"
using assms(2) unfolding eventually_at by auto
define r3 where "r3=min r1 r2"
have "(\w. (f w) powr of_int n) holomorphic_on ball z r3 - {z}"
apply (rule holomorphic_on_powr_of_int)
subgoal unfolding r3_def using r1 by auto
subgoal unfolding r3_def using r2 by (auto simp add:dist_commute)
done
moreover have "r3>0" unfolding r3_def using \<open>0 < r1\<close> \<open>0 < r2\<close> by linarith
ultimately show ?thesis unfolding isolated_singularity_at_def
apply (subst (asm) analytic_on_open[symmetric])
by auto
qed
lemma non_zero_neighbour:
assumes f_iso:"isolated_singularity_at f z"
and f_ness:"not_essential f z"
and f_nconst:"\\<^sub>Fw in (at z). f w\0"
shows "\\<^sub>F w in (at z). f w\0"
proof -
obtain fn fp fr where [simp]:"fp z \ 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
"\w\cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \ fp w \ 0"
using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto
have "f w \ 0" when " w \ z" "dist w z < fr" for w
proof -
have "f w = fp w * (w - z) powr of_int fn" "fp w \ 0"
using fr(2)[rule_format, of w] using that by (auto simp add:dist_commute)
moreover have "(w - z) powr of_int fn \0"
unfolding powr_eq_0_iff using \<open>w\<noteq>z\<close> by auto
ultimately show ?thesis by auto
qed
then show ?thesis using \<open>fr>0\<close> unfolding eventually_at by auto
qed
lemma non_zero_neighbour_pole:
assumes "is_pole f z"
shows "\\<^sub>F w in (at z). f w\0"
using assms filterlim_at_infinity_imp_eventually_ne[of f "at z" 0]
unfolding is_pole_def by auto
lemma non_zero_neighbour_alt:
assumes holo: "f holomorphic_on S"
and "open S" "connected S" "z \ S" "\ \ S" "f \ \ 0"
shows "\\<^sub>F w in (at z). f w\0 \ w\S"
proof (cases "f z = 0")
case True
from isolated_zeros[OF holo \<open>open S\<close> \<open>connected S\<close> \<open>z \<in> S\<close> True \<open>\<beta> \<in> S\<close> \<open>f \<beta> \<noteq> 0\<close>]
obtain r where "0 < r" "ball z r \ S" "\w \ ball z r - {z}.f w \ 0" by metis
then show ?thesis unfolding eventually_at
apply (rule_tac x=r in exI)
by (auto simp add:dist_commute)
next
case False
obtain r1 where r1:"r1>0" "\y. dist z y < r1 \ f y \ 0"
using continuous_at_avoid[of z f, OF _ False] assms(2,4) continuous_on_eq_continuous_at
holo holomorphic_on_imp_continuous_on by blast
obtain r2 where r2:"r2>0" "ball z r2 \ S"
using assms(2) assms(4) openE by blast
show ?thesis unfolding eventually_at
apply (rule_tac x="min r1 r2" in exI)
using r1 r2 by (auto simp add:dist_commute)
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"
shows "not_essential (\w. f w * g w) z"
proof -
define fg where "fg = (\w. f w * g w)"
have ?thesis when "\ ((\\<^sub>Fw in (at z). f w\0) \ (\\<^sub>Fw in (at z). g w\0))"
proof -
have "\\<^sub>Fw in (at z). fg w=0"
using that[unfolded frequently_def, simplified] unfolding fg_def
by (auto elim: eventually_rev_mp)
from tendsto_cong[OF this] have "fg \z\0" by auto
then show ?thesis unfolding not_essential_def fg_def by auto
qed
moreover have ?thesis when f_nconst:"\\<^sub>Fw in (at z). f w\0" and g_nconst:"\\<^sub>Fw in (at z). g w\0"
proof -
obtain fn fp fr where [simp]:"fp z \ 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
"\w\cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \ fp w \ 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 \ 0" and "gr > 0"
and gr: "gp holomorphic_on cball z gr"
"\w\cball z gr - {z}. g w = gp w * (w - z) powr of_int gn \ gp w \ 0"
using holomorphic_factor_puncture[OF g_iso g_ness g_nconst,THEN ex1_implies_ex] 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) powr (of_int (fn+gn))" and fgp_nz:"fp w*gp w\0"
when "w\ball z r1 - {z}" for w
proof -
have "f w = fp w * (w - z) powr of_int fn" "fp w\0"
using fr(2)[rule_format,of w] that unfolding r1_def by auto
moreover have "g w = gp w * (w - z) powr of_int gn" "gp w \ 0"
using gr(2)[rule_format, of w] that unfolding r1_def by auto
ultimately show "fg w = (fp w * gp w) * (w - z) powr (of_int (fn+gn))" "fp w*gp w\0"
unfolding fg_def by (auto simp add:powr_add)
qed
have [intro]: "fp \z\fp z" "gp \z\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)+
have ?thesis when "fn+gn>0"
proof -
have "(\w. (fp w * gp w) * (w - z) ^ (nat (fn+gn))) \z\0"
using that by (auto intro!:tendsto_eq_intros)
then have "fg \z\ 0"
apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
by (metis (no_types, hide_lams) Diff_iff cball_trivial dist_commute dist_self
eq_iff_diff_eq_0 fg_times less_le linorder_not_le mem_ball mem_cball powr_of_int
that)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
moreover have ?thesis when "fn+gn=0"
proof -
have "(\w. fp w * gp w) \z\fp z*gp z"
using that by (auto intro!:tendsto_eq_intros)
then have "fg \z\ 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)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
moreover have ?thesis when "fn+gn<0"
proof -
have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity"
apply (rule filterlim_divide_at_infinity)
apply (insert that, auto intro!:tendsto_eq_intros filterlim_atI)
using eventually_at_topological by blast
then have "is_pole fg z" unfolding is_pole_def
apply (elim filterlim_transform_within[OF _ _ \<open>r1>0\<close>],simp)
apply (subst fg_times,simp add:dist_commute)
apply (subst powr_of_int)
using that by (auto simp add:field_split_simps)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
ultimately show ?thesis unfolding not_essential_def fg_def by fastforce
qed
ultimately show ?thesis by auto
qed
lemma not_essential_inverse[singularity_intros]:
assumes f_ness:"not_essential f z"
assumes f_iso:"isolated_singularity_at f z"
shows "not_essential (\w. inverse (f w)) z"
proof -
define vf where "vf = (\w. inverse (f w))"
have ?thesis when "\(\\<^sub>Fw in (at z). f w\0)"
proof -
have "\\<^sub>Fw in (at z). f w=0"
using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
then have "\\<^sub>Fw in (at z). vf w=0"
unfolding vf_def by auto
from tendsto_cong[OF this] have "vf \z\0" unfolding vf_def by auto
then show ?thesis unfolding not_essential_def vf_def by auto
qed
moreover have ?thesis when "is_pole f z"
proof -
have "vf \z\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 "\x. f\z\x " and f_nconst:"\\<^sub>Fw in (at z). f w\0"
proof -
from that obtain fz where fz:"f\z\fz" by auto
have ?thesis when "fz=0"
proof -
have "(\w. inverse (vf w)) \z\0"
using fz that unfolding vf_def by auto
moreover have "\\<^sub>F w in at z. inverse (vf w) \ 0"
using non_zero_neighbour[OF f_iso f_ness f_nconst]
unfolding vf_def by auto
ultimately have "is_pole vf z"
using filterlim_inverse_at_iff[of vf "at z"] unfolding filterlim_at is_pole_def by auto
then show ?thesis unfolding not_essential_def vf_def by auto
qed
moreover have ?thesis when "fz\0"
proof -
have "vf \z\inverse fz"
using fz that unfolding vf_def by (auto intro:tendsto_eq_intros)
then show ?thesis unfolding not_essential_def vf_def by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis using f_ness unfolding not_essential_def by auto
qed
lemma isolated_singularity_at_inverse[singularity_intros]:
assumes f_iso:"isolated_singularity_at f z"
and f_ness:"not_essential f z"
shows "isolated_singularity_at (\w. inverse (f w)) z"
proof -
define vf where "vf = (\w. inverse (f w))"
have ?thesis when "\(\\<^sub>Fw in (at z). f w\0)"
proof -
have "\\<^sub>Fw in (at z). f w=0"
using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
then have "\\<^sub>Fw in (at z). vf w=0"
unfolding vf_def by auto
then obtain d1 where "d1>0" and d1:"\x. x \ z \ dist x z < d1 \ vf x = 0"
unfolding eventually_at by auto
then have "vf holomorphic_on ball z d1-{z}"
apply (rule_tac holomorphic_transform[of "\_. 0"])
by (auto simp add:dist_commute)
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
qed
moreover have ?thesis when f_nconst:"\\<^sub>Fw in (at z). f w\0"
proof -
have "\\<^sub>F w in at z. f w \ 0" using non_zero_neighbour[OF f_iso f_ness f_nconst] .
then obtain d1 where d1:"d1>0" "\x. x \ z \ dist x z < d1 \ f x \ 0"
unfolding eventually_at by auto
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
moreover have "vf analytic_on ball z d3 - {z}"
unfolding vf_def
apply (rule analytic_on_inverse)
subgoal using d2 unfolding d3_def by (elim analytic_on_subset) auto
subgoal for w using d1 unfolding d3_def by (auto simp add:dist_commute)
done
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"
shows "not_essential (\w. f w / g w) z"
proof -
have "not_essential (\w. f w * inverse (g w)) z"
apply (rule not_essential_times[where g="\w. inverse (g w)"])
using assms by (auto intro: isolated_singularity_at_inverse not_essential_inverse)
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"
shows isolated_singularity_at_times[singularity_intros]:
"isolated_singularity_at (\w. f w * g w) z" and
isolated_singularity_at_add[singularity_intros]:
"isolated_singularity_at (\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}"
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
have "(\w. f w * g w) analytic_on ball z d3 - {z}"
apply (rule analytic_on_mult)
using d1 d2 unfolding d3_def by (auto elim:analytic_on_subset)
then show "isolated_singularity_at (\w. f w * g w) z"
using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto
have "(\w. f w + g w) analytic_on ball z d3 - {z}"
apply (rule analytic_on_add)
using d1 d2 unfolding d3_def by (auto elim:analytic_on_subset)
then show "isolated_singularity_at (\w. f w + g w) z"
using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto
qed
lemma isolated_singularity_at_uminus[singularity_intros]:
assumes f_iso:"isolated_singularity_at f z"
shows "isolated_singularity_at (\w. - f w) z"
using assms unfolding isolated_singularity_at_def using analytic_on_neg by blast
lemma isolated_singularity_at_id[singularity_intros]:
"isolated_singularity_at (\w. w) z"
unfolding isolated_singularity_at_def by (simp add: gt_ex)
lemma isolated_singularity_at_minus[singularity_intros]:
assumes f_iso:"isolated_singularity_at f z"
and g_iso:"isolated_singularity_at g z"
shows "isolated_singularity_at (\w. f w - g w) z"
using isolated_singularity_at_uminus[THEN isolated_singularity_at_add[OF f_iso,of "\w. - g w"]
,OF g_iso] by simp
lemma isolated_singularity_at_divide[singularity_intros]:
assumes f_iso:"isolated_singularity_at f z"
and g_iso:"isolated_singularity_at g z"
and g_ness:"not_essential g z"
shows "isolated_singularity_at (\w. f w / g w) z"
using isolated_singularity_at_inverse[THEN isolated_singularity_at_times[OF f_iso,
of "\w. inverse (g w)"],OF g_iso g_ness] by (simp add:field_simps)
lemma isolated_singularity_at_const[singularity_intros]:
"isolated_singularity_at (\w. c) z"
unfolding isolated_singularity_at_def by (simp add: gt_ex)
lemma isolated_singularity_at_holomorphic:
assumes "f holomorphic_on s-{z}" "open s" "z\s"
shows "isolated_singularity_at f z"
using assms unfolding isolated_singularity_at_def
by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)
subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
"zorder f z = (THE n. (\h r. r>0 \ h holomorphic_on cball z r \ h z\0
\<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w-z) powr (of_int n)
\<and> h w \<noteq>0)))"
definition\<^marker>\<open>tag important\<close> zor_poly
::"[complex \ complex, complex] \ complex \ complex" where
"zor_poly f z = (SOME h. \r. r > 0 \ h holomorphic_on cball z r \ h z \ 0
\<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w - z) powr (zorder f z)
\<and> h w \<noteq>0))"
lemma zorder_exist:
fixes f::"complex \ complex" and z::complex
defines "n\zorder f z" and "g\zor_poly f z"
assumes f_iso:"isolated_singularity_at f z"
and f_ness:"not_essential f z"
and f_nconst:"\\<^sub>Fw in (at z). f w\0"
shows "g z\0 \ (\r. r>0 \ g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr n \<and> g w \<noteq>0))"
proof -
define P where "P = (\n g r. 0 < r \ g holomorphic_on cball z r \ g z\0
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr (of_int n) \<and> g w\<noteq>0))"
have "\!n. \g r. P n g r"
using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto
then have "\g r. P n g r"
unfolding n_def P_def zorder_def
by (drule_tac theI',argo)
then have "\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
qed
lemma
fixes f::"complex \ complex" and z::complex
assumes f_iso:"isolated_singularity_at f z"
and f_ness:"not_essential f z"
and f_nconst:"\\<^sub>Fw in (at z). f w\0"
shows zorder_inverse: "zorder (\w. inverse (f w)) z = - zorder f z"
and zor_poly_inverse: "\\<^sub>Fw in (at z). zor_poly (\w. inverse (f w)) z w
= inverse (zor_poly f z w)"
proof -
define vf where "vf = (\w. inverse (f w))"
define fn vfn where
"fn = zorder f z" and "vfn = zorder vf z"
define fp vfp where
"fp = zor_poly f z" and "vfp = zor_poly vf z"
obtain fr where [simp]:"fp z \ 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
"\w\cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \ fp w \ 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) powr (of_int (-fn))"
and fr_nz: "inverse (fp w)\0"
when "w\ball z fr - {z}" for w
proof -
have "f w = fp w * (w - z) powr of_int fn" "fp w\0"
using fr(2)[rule_format,of w] that by auto
then show "vf w = (inverse (fp w)) * (w - z) powr (of_int (-fn))" "inverse (fp w)\0"
unfolding vf_def by (auto simp add:powr_minus)
qed
obtain vfr where [simp]:"vfp z \ 0" and "vfr>0" and vfr:"vfp holomorphic_on cball z vfr"
"(\w\cball z vfr - {z}. vf w = vfp w * (w - z) powr of_int vfn \ vfp w \ 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 "\\<^sub>F w in at z. vf w \ 0"
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"
apply (rule holomorphic_factor_unique[of r1 vfp z "\w. inverse (fp w)" vf])
subgoal using \<open>r1>0\<close> by simp
subgoal by simp
subgoal by simp
subgoal
proof (rule ballI)
fix w assume "w \ ball z r1 - {z}"
then have "w \ ball z fr - {z}" "w \ cball z vfr - {z}" unfolding r1_def by auto
from fr_inverse[OF this(1)] fr_nz[OF this(1)] vfr(2)[rule_format,OF this(2)]
show "vf w = vfp w * (w - z) powr of_int vfn \ vfp w \ 0
\<and> vf w = inverse (fp w) * (w - z) powr of_int (- fn) \<and> inverse (fp w) \<noteq> 0" by auto
qed
subgoal using vfr(1) unfolding r1_def by (auto intro!:holomorphic_intros)
subgoal using fr unfolding r1_def by (auto intro!:holomorphic_intros)
done
have "vfp w = inverse (fp w)" when "w\ball z r1-{z}" for w
proof -
have "w \ ball z fr - {z}" "w \ cball z vfr - {z}" "w\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
qed
then show "\\<^sub>Fw in (at z). vfp w = inverse (fp w)"
unfolding eventually_at using \<open>r1>0\<close>
apply (rule_tac x=r1 in exI)
by (auto simp add:dist_commute)
qed
lemma
fixes f g::"complex \ 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: "\\<^sub>Fw in (at z). f w * g w\ 0"
shows zorder_times:"zorder (\w. f w * g w) z = zorder f z + zorder g z" and
zor_poly_times:"\\<^sub>Fw in (at z). zor_poly (\w. f w * g w) z w
= zor_poly f z w *zor_poly g z w"
proof -
define fg where "fg = (\w. f w * g w)"
define fn gn fgn where
"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:"\\<^sub>Fw in (at z). f w \ 0" and g_nconst:"\\<^sub>Fw in (at z).g w\ 0"
using fg_nconst by (auto elim!:frequently_elim1)
obtain fr where [simp]:"fp z \ 0" and "fr > 0"
and fr: "fp holomorphic_on cball z fr"
"\w\cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \ fp w \ 0"
using zorder_exist[OF f_iso f_ness f_nconst,folded fp_def fn_def] by auto
obtain gr where [simp]:"gp z \ 0" and "gr > 0"
and gr: "gp holomorphic_on cball z gr"
"\w\cball z gr - {z}. g w = gp w * (w - z) powr of_int gn \ gp w \ 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) powr (of_int (fn+gn))" and fgp_nz:"fp w*gp w\0"
when "w\ball z r1 - {z}" for w
proof -
have "f w = fp w * (w - z) powr of_int fn" "fp w\0"
using fr(2)[rule_format,of w] that unfolding r1_def by auto
moreover have "g w = gp w * (w - z) powr of_int gn" "gp w \ 0"
using gr(2)[rule_format, of w] that unfolding r1_def by auto
ultimately show "fg w = (fp w * gp w) * (w - z) powr (of_int (fn+gn))" "fp w*gp w\0"
unfolding fg_def by (auto simp add:powr_add)
qed
obtain fgr where [simp]:"fgp z \ 0" and "fgr > 0"
and fgr: "fgp holomorphic_on cball z fgr"
"\w\cball z fgr - {z}. fg w = fgp w * (w - z) powr of_int fgn \ fgp w \ 0"
proof -
have "fgp z \ 0 \ (\r>0. fgp holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r - {z}. fg w = fgp w * (w - z) powr of_int fgn \<and> fgp w \<noteq> 0))"
apply (rule zorder_exist[of fg z, folded fgn_def fgp_def])
subgoal unfolding fg_def using isolated_singularity_at_times[OF f_iso g_iso] .
subgoal unfolding fg_def using not_essential_times[OF f_ness g_ness f_iso g_iso] .
subgoal unfolding fg_def using fg_nconst .
done
then show ?thesis using that by blast
qed
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 "\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 \ ball z r2 - {z}"
then have "w \ ball z r1 - {z}" "w \ cball z fgr - {z}" unfolding r2_def by auto
from fg_times[OF this(1)] fgp_nz[OF this(1)] fgr(2)[rule_format,OF this(2)]
show "fg w = fgp w * (w - z) powr of_int fgn \ fgp w \ 0
\<and> fg w = fp w * gp w * (w - z) powr of_int (fn + gn) \<and> fp w * gp w \<noteq> 0" by auto
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
have "fgp w = fp w *gp w" when "w\ball z r2-{z}" for w
proof -
have "w \ ball z r1 - {z}" "w \ cball z fgr - {z}" "w\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
qed
then show "\\<^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)
qed
lemma
fixes f g::"complex \ 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: "\\<^sub>Fw in (at z). f w * g w\ 0"
shows zorder_divide:"zorder (\w. f w / g w) z = zorder f z - zorder g z" and
zor_poly_divide:"\\<^sub>Fw in (at z). zor_poly (\w. f w / g w) z w
= zor_poly f z w / zor_poly g z w"
proof -
have f_nconst:"\\<^sub>Fw in (at z). f w \ 0" and g_nconst:"\\<^sub>Fw in (at z).g w\ 0"
using fg_nconst by (auto elim!:frequently_elim1)
define vg where "vg=(\w. inverse (g w))"
have "zorder (\w. f w * vg w) z = zorder f z + zorder vg z"
apply (rule zorder_times[OF f_iso _ f_ness,of vg])
subgoal unfolding vg_def using isolated_singularity_at_inverse[OF g_iso g_ness] .
subgoal unfolding vg_def using not_essential_inverse[OF g_ness g_iso] .
subgoal unfolding vg_def using fg_nconst by (auto elim!:frequently_elim1)
done
then show "zorder (\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)
have "\\<^sub>F w in at z. zor_poly (\w. f w * vg w) z w = zor_poly f z w * zor_poly vg z w"
apply (rule zor_poly_times[OF f_iso _ f_ness,of vg])
subgoal unfolding vg_def using isolated_singularity_at_inverse[OF g_iso g_ness] .
subgoal unfolding vg_def using not_essential_inverse[OF g_ness g_iso] .
subgoal unfolding vg_def using fg_nconst by (auto elim!:frequently_elim1)
done
then show "\\<^sub>Fw in (at z). zor_poly (\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
apply eventually_elim
by (auto simp add:field_simps)
qed
lemma zorder_exist_zero:
fixes f::"complex \ complex" and z::complex
defines "n\zorder f z" and "g\zor_poly f z"
assumes holo: "f holomorphic_on s" and
"open s" "connected s" "z\s"
and non_const: "\w\s. f w \ 0"
shows "(if f z=0 then n > 0 else n=0) \ (\r. r>0 \ cball z r \ s \ 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 \ 0" and r: "r>0" "cball z r \ s" "g holomorphic_on cball z r"
"(\w\cball z r - {z}. f w = g w * (w - z) powr of_int n \ g w \ 0)"
proof -
have "g z \ 0 \ (\r>0. g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int 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 "not_essential f z" unfolding not_essential_def
using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on
by fastforce
have "\\<^sub>F w in at z. f w \ 0 \ w\s"
proof -
obtain w where "w\s" "f w\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
then show "\\<^sub>F w in at z. f w \ 0"
apply (elim eventually_frequentlyE)
by auto
qed
then obtain r1 where "g z \ 0" "r1>0" and r1:"g holomorphic_on cball z r1"
"(\w\cball z r1 - {z}. f w = g w * (w - z) powr of_int n \ g w \ 0)"
by auto
obtain r2 where r2: "r2>0" "cball z r2 \ s"
using assms(4,6) open_contains_cball_eq by blast
define r3 where "r3=min r1 r2"
have "r3>0" "cball z r3 \ s" using \r1>0\ r2 unfolding r3_def by auto
moreover have "g holomorphic_on cball z r3"
using r1(1) unfolding r3_def by auto
moreover have "(\w\cball z r3 - {z}. f w = g w * (w - z) powr of_int n \ g w \ 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
have if_0:"if f z=0 then n > 0 else n=0"
proof -
have "f\ z \ f z"
by (metis assms(4,6,7) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
then have "(\w. g w * (w - z) powr of_int n) \z\ f z"
apply (elim Lim_transform_within_open[where s="ball z r"])
using r by auto
moreover have "g \z\g z"
by (metis (mono_tags, lifting) open_ball at_within_open_subset
ball_subset_cball centre_in_ball continuous_on holomorphic_on_imp_continuous_on r(1,3) subsetCE)
ultimately have "(\w. (g w * (w - z) powr of_int n) / g w) \z\ f z/g z"
apply (rule_tac tendsto_divide)
using \<open>g z\<noteq>0\<close> by auto
then have powr_tendsto:"(\w. (w - z) powr of_int n) \z\ f z/g z"
apply (elim Lim_transform_within_open[where s="ball z r"])
using r by auto
have ?thesis when "n\0" "f z=0"
proof -
have "(\w. (w - z) ^ nat n) \z\ f z/g z"
using powr_tendsto
apply (elim Lim_transform_within[where d=r])
by (auto simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
then have *:"(\w. (w - z) ^ nat n) \z\ 0" using \f z=0\ by simp
moreover have False when "n=0"
proof -
have "(\w. (w - z) ^ nat n) \z\ 1"
using \<open>n=0\<close> by auto
then show False using * using LIM_unique zero_neq_one by blast
qed
ultimately show ?thesis using that by fastforce
qed
moreover have ?thesis when "n\0" "f z\0"
proof -
have False when "n>0"
proof -
have "(\w. (w - z) ^ nat n) \z\ f z/g z"
using powr_tendsto
apply (elim Lim_transform_within[where d=r])
by (auto simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
moreover have "(\w. (w - z) ^ nat n) \z\ 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
qed
then show ?thesis using that by force
qed
moreover have False when "n<0"
proof -
have "(\w. inverse ((w - z) ^ nat (- n))) \z\ f z/g z"
"(\w.((w - z) ^ nat (- n))) \z\ 0"
subgoal using powr_tendsto powr_of_int that
by (elim Lim_transform_within_open[where s=UNIV],auto)
subgoal using that by (auto intro!:tendsto_eq_intros)
done
from tendsto_mult[OF this,simplified]
have "(\x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \z\ 0" .
then have "(\x. 1::complex) \z\ 0"
by (elim Lim_transform_within_open[where s=UNIV],auto)
then show False using LIM_const_eq by fastforce
qed
ultimately show ?thesis by fastforce
qed
moreover have "f w = g w * (w-z) ^ nat n \ g w \0" when "w\cball z r" for w
proof (cases "w=z")
case True
then have "f \z\f w"
using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on by fastforce
then have "(\w. g w * (w-z) ^ nat n) \z\f w"
proof (elim Lim_transform_within[OF _ \<open>r>0\<close>])
fix x assume "0 < dist x z" "dist x z < r"
then have "x \ cball z r - {z}" "x\z"
unfolding cball_def by (auto simp add: dist_commute)
then have "f x = g x * (x - z) powr of_int n"
using r(4)[rule_format,of x] by simp
also have "... = g x * (x - z) ^ nat n"
apply (subst powr_of_int)
using if_0 \<open>x\<noteq>z\<close> by (auto split:if_splits)
finally show "f x = g x * (x - z) ^ nat n" .
qed
moreover have "(\w. g w * (w-z) ^ nat n) \z\ g w * (w-z) ^ nat n"
using True apply (auto intro!:tendsto_eq_intros)
by (metis open_ball at_within_open_subset ball_subset_cball centre_in_ball
continuous_on holomorphic_on_imp_continuous_on r(1) r(3) that)
ultimately have "f w = g w * (w-z) ^ nat n" using LIM_unique by blast
then show ?thesis using \<open>g z\<noteq>0\<close> True by auto
next
case False
then have "f w = g w * (w - z) powr of_int n \ g w \ 0"
using r(4) that by auto
then show ?thesis using False if_0 powr_of_int by (auto split:if_splits)
qed
ultimately show ?thesis using r by auto
qed
lemma zorder_exist_pole:
fixes f::"complex \ complex" and z::complex
defines "n\zorder f z" and "g\zor_poly f z"
assumes holo: "f holomorphic_on s-{z}" and
"open s" "z\s"
and "is_pole f z"
shows "n < 0 \ g z\0 \ (\r. r>0 \ cball z r \ s \ 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 \ 0" and r: "r>0" "cball z r \ s" "g holomorphic_on cball z r"
"(\w\cball z r - {z}. f w = g w * (w - z) powr of_int n \ g w \ 0)"
proof -
have "g z \ 0 \ (\r>0. g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int 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)
by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)
show "not_essential f z" unfolding not_essential_def
using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on
by fastforce
from non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] show "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
apply (elim eventually_frequentlyE)
by auto
qed
then obtain r1 where "g z \ 0" "r1>0" and r1:"g holomorphic_on cball z r1"
"(\w\cball z r1 - {z}. f w = g w * (w - z) powr of_int n \ g w \ 0)"
by auto
obtain r2 where r2: "r2>0" "cball z r2 \ s"
using assms(4,5) open_contains_cball_eq by metis
define r3 where "r3=min r1 r2"
have "r3>0" "cball z r3 \ s" using \r1>0\ r2 unfolding r3_def by auto
moreover have "g holomorphic_on cball z r3"
using r1(1) unfolding r3_def by auto
moreover have "(\w\cball z r3 - {z}. f w = g w * (w - z) powr of_int n \ g w \ 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
have "n<0"
proof (rule ccontr)
assume " \ n < 0"
define c where "c=(if n=0 then g z else 0)"
have [simp]:"g \z\ 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 "\\<^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"])
using r powr_of_int \<open>\<not> n < 0\<close> by auto
moreover have "(\x. g x * (x - z) ^ nat n) \z\c"
proof (cases "n=0")
case True
then show ?thesis unfolding c_def by simp
next
case False
then have "(\x. (x - z) ^ nat n) \z\ 0" using \\ n < 0\
by (auto intro!:tendsto_eq_intros)
from tendsto_mult[OF _ this,of g "g z",simplified]
show ?thesis unfolding c_def using False by simp
qed
ultimately have "f \z\c" using tendsto_cong by fast
then show False using \<open>is_pole f z\<close> at_neq_bot not_tendsto_and_filterlim_at_infinity
unfolding is_pole_def by blast
qed
moreover have "\w\cball z r - {z}. f w = g w / (w-z) ^ nat (- n) \ g w \0"
using r(4) \<open>n<0\<close> powr_of_int
by (metis Diff_iff divide_inverse eq_iff_diff_eq_0 insert_iff linorder_not_le)
ultimately show ?thesis using r(1-3) \<open>g z\<noteq>0\<close> by auto
qed
lemma zorder_eqI:
assumes "open s" "z \ s" "g holomorphic_on s" "g z \ 0"
assumes fg_eq:"\w. \w \ s;w\z\ \ f w = g w * (w - z) powr n"
shows "zorder f z = n"
proof -
have "continuous_on s g" by (rule holomorphic_on_imp_continuous_on) fact
moreover have "open (-{0::complex})" by auto
ultimately have "open ((g -` (-{0})) \ s)"
unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast
moreover from assms have "z \ (g -` (-{0})) \ s" by auto
ultimately obtain r where r: "r > 0" "cball z r \ s \ (g -` (-{0}))"
unfolding open_contains_cball by blast
let ?gg= "(\w. g w * (w - z) powr n)"
define P where "P = (\n g r. 0 < r \ g holomorphic_on cball z r \ g z\0
\<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr (of_int n) \<and> g w\<noteq>0))"
have "P n g r"
unfolding P_def using r assms(3,4,5) by auto
then have "\g r. P n g r" by auto
moreover have unique: "\!n. \g r. P n g r" unfolding P_def
proof (rule holomorphic_factor_puncture)
have "ball z r-{z} \ s" using r using ball_subset_cball by blast
then have "?gg holomorphic_on ball z r-{z}"
using \<open>g holomorphic_on s\<close> r by (auto intro!: holomorphic_intros)
then have "f holomorphic_on ball z r - {z}"
apply (elim holomorphic_transform)
using fg_eq \<open>ball z r-{z} \<subseteq> s\<close> by auto
then show "isolated_singularity_at f z" unfolding isolated_singularity_at_def
using analytic_on_open open_delete r(1) by blast
next
have "not_essential ?gg z"
proof (intro singularity_intros)
show "not_essential g z"
by (meson \<open>continuous_on s g\<close> assms(1) assms(2) continuous_on_eq_continuous_at
isCont_def not_essential_def)
show " \\<^sub>F w in at z. w - z \ 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)
show "isolated_singularity_at g z"
by (meson Diff_subset open_ball analytic_on_holomorphic
assms(1,2,3) holomorphic_on_subset isolated_singularity_at_def openE)
qed
then show "not_essential f z"
apply (elim not_essential_transform)
unfolding eventually_at using assms(1,2) assms(5)[symmetric]
by (metis dist_commute mem_ball openE subsetCE)
show "\\<^sub>F w in at z. f w \ 0" unfolding frequently_at
proof (rule,rule)
fix d::real assume "0 < d"
define z' where "z'=z+min d r / 2"
have "z' \ z" " dist z' z < d "
unfolding z'_def using \d>0\ \r>0\
by (auto simp add:dist_norm)
moreover have "f z' \ 0"
proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>])
have "z' \ cball z r" unfolding z'_def using \r>0\ \d>0\ by (auto simp add:dist_norm)
then show " z' \ s" using r(2) by blast
show "g z' * (z' - z) powr of_int n \ 0"
using P_def \<open>P n g r\<close> \<open>z' \<in> cball z r\<close> calculation(1) by auto
qed
ultimately show "\x\UNIV. x \ z \ dist x z < d \ f x \ 0" by auto
qed
qed
ultimately have "(THE n. \g r. P n g r) = n"
by (rule_tac the1_equality)
then show ?thesis unfolding zorder_def P_def by blast
qed
lemma simple_zeroI:
assumes "open s" "z \ s" "g holomorphic_on s" "g z \ 0"
assumes "\w. w \ s \ f w = g w * (w - z)"
shows "zorder f z = 1"
using assms(1-4) by (rule zorder_eqI) (use assms(5) in auto)
lemma higher_deriv_power:
shows "(deriv ^^ j) (\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) (\w. (w - z) ^ n) w = deriv ((deriv ^^ j) (\w. (w - z) ^ n)) w"
by simp
also have "(deriv ^^ j) (\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 "(\ has_field_derivative of_nat (n - j) *
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 \ n", subst pochhammer_rec)
(insert Suc.prems, simp_all add: algebra_simps Suc_diff_le pochhammer_0_left)
finally have "deriv (\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 \ s"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.70 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
