# Theory Complex_Singularities

```theory Complex_Singularities
imports Conformal_Mappings
begin

subsection ‹Non-essential singular points›

definition✐‹tag important› 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_shift_iff:
fixes f :: "('a::real_normed_vector ⇒ 'b::real_normed_vector)"
shows "is_pole (f ∘ (+) d) a = is_pole f (a + d)"

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_shift_0:
fixes f :: "('a::real_normed_vector ⇒ 'b::real_normed_vector)"
shows "is_pole f z ⟷ is_pole (λx. f (z + x)) 0"
unfolding is_pole_def by (subst at_to_0) (auto simp: filterlim_filtermap add_ac)

lemma is_pole_shift_0':
fixes f :: "('a::real_normed_vector ⇒ 'b::real_normed_vector)"
shows "NO_MATCH 0 z ⟹ is_pole f z ⟷ is_pole (λx. f (z + x)) 0"
by (metis is_pole_shift_0)

lemma is_pole_compose_iff:
assumes "filtermap g (at x) = (at y)"
shows   "is_pole (f ∘ g) x ⟷ is_pole f y"
unfolding is_pole_def filterlim_def filtermap_compose assms ..

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
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 s›] ‹open s›
moreover have "(inverse o f) holomorphic_on (s-{z})"
unfolding comp_def using f_holo
hence "g holomorphic_on (s-{z})"
using g_def holomorphic_transform by force
ultimately show ?thesis unfolding g_def using ‹open s›
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"
hence "f ─x→ f x"
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_cmult_iff [simp]:
assumes "c ≠ 0"
shows "is_pole (λz. c * f z :: 'a :: real_normed_field) z ⟷ is_pole f z"
proof
assume "is_pole (λz. c * f z) z"
with ‹c≠0› have "is_pole (λz. inverse c * (c * f z)) z"
unfolding is_pole_def
by (force intro: tendsto_mult_filterlim_at_infinity)
thus "is_pole f z"
using ‹c≠0› by (simp add: field_simps)
next
assume "is_pole f z"
with ‹c≠0› show "is_pole (λz. c * f z) z"
by (auto intro!: tendsto_mult_filterlim_at_infinity simp: is_pole_def)
qed

lemma is_pole_uminus_iff [simp]: "is_pole (λz. -f z :: 'a :: real_normed_field) z ⟷ is_pole f z"
using is_pole_cmult_iff[of "-1" f] by (simp del: is_pole_cmult_iff)

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)"
using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
tendsto_mult_filterlim_at_infinity by blast
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

lemma is_pole_compose:
assumes "is_pole f w" "g ─z→ w" "eventually (λz. g z ≠ w) (at z)"
shows   "is_pole (λx. f (g x)) z"
using assms(1) unfolding is_pole_def
by (rule filterlim_compose) (use assms in ‹auto simp: filterlim_at›)

lemma is_pole_plus_const_iff:
"is_pole f z ⟷ is_pole (λx. f x + c) z"
proof
assume "is_pole f z"
then have "filterlim f at_infinity (at z)" unfolding is_pole_def .
moreover have "((λ_. c) ⤏ c) (at z)" by auto
ultimately have " LIM x (at z). f x + c :> at_infinity"
using tendsto_add_filterlim_at_infinity'[of f "at z"] by auto
then show "is_pole (λx. f x + c) z" unfolding is_pole_def .
next
assume "is_pole (λx. f x + c) z"
then have "filterlim (λx. f x + c) at_infinity (at z)"
unfolding is_pole_def .
moreover have "((λ_. -c) ⤏ -c) (at z)" by auto
ultimately have " LIM x (at z). f x :> at_infinity"
using tendsto_add_filterlim_at_infinity'[of "(λx. f x + c)"
"at z" "(λ_. - c)" "-c"]
by auto
then show "is_pole f z" unfolding is_pole_def .
qed

lemma is_pole_minus_const_iff:
"is_pole (λx. f x - c) z ⟷ is_pole f z"
using is_pole_plus_const_iff [of f z "-c"] by simp

lemma is_pole_alt:
"is_pole f x  = (∀B>0. ∃U. open U ∧ x∈U ∧ (∀y∈U. y≠x ⟶ norm (f y)≥B))"
unfolding is_pole_def
unfolding filterlim_at_infinity[of 0,simplified] eventually_at_topological
by auto

lemma is_pole_mult_analytic_nonzero1:
assumes "is_pole g x" "f analytic_on {x}" "f x ≠ 0"
shows   "is_pole (λx. f x * g x) x"
unfolding is_pole_def
proof (rule tendsto_mult_filterlim_at_infinity)
show "f ─x→ f x"
using assms by (simp add: analytic_at_imp_isCont isContD)
qed (use assms in ‹auto simp: is_pole_def›)

lemma is_pole_mult_analytic_nonzero2:
assumes "is_pole f x" "g analytic_on {x}" "g x ≠ 0"
shows   "is_pole (λx. f x * g x) x"
proof -
have g: "g analytic_on {x}"
using assms by auto
show ?thesis
using is_pole_mult_analytic_nonzero1 [OF ‹is_pole f x› g] ‹g x ≠ 0›
qed

lemma is_pole_mult_analytic_nonzero1_iff:
assumes "f analytic_on {x}" "f x ≠ 0"
shows   "is_pole (λx. f x * g x) x ⟷ is_pole g x"
proof
assume "is_pole g x"
thus "is_pole (λx. f x * g x) x"
by (intro is_pole_mult_analytic_nonzero1 assms)
next
assume "is_pole (λx. f x * g x) x"
hence "is_pole (λx. inverse (f x) * (f x * g x)) x"
by (rule is_pole_mult_analytic_nonzero1)
(use assms in ‹auto intro!: analytic_intros›)
also have "?this ⟷ is_pole g x"
proof (rule is_pole_cong)
have "eventually (λx. f x ≠ 0) (at x)"
using assms by (simp add: analytic_at_neq_imp_eventually_neq)
thus "eventually (λx. inverse (f x) * (f x * g x) = g x) (at x)"
by eventually_elim auto
qed auto
finally show "is_pole g x" .
qed

lemma is_pole_mult_analytic_nonzero2_iff:
assumes "g analytic_on {x}" "g x ≠ 0"
shows   "is_pole (λx. f x * g x) x ⟷ is_pole f x"
by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+

lemma frequently_const_imp_not_is_pole:
fixes z :: "'a::first_countable_topology"
assumes "frequently (λw. f w = c) (at z)"
shows   "¬ is_pole f z"
proof
assume "is_pole f z"
from assms have "z islimpt {w. f w = c}"
then obtain g where g: "⋀n. g n ∈ {w. f w = c} - {z}" "g ⇢ z"
unfolding islimpt_sequential by blast
then have "(f ∘ g) ⇢ c"
moreover have *: "filterlim g (at z) sequentially"
using g by (auto simp: filterlim_at)
have "filterlim (f ∘ g) at_infinity sequentially"
unfolding o_def by (rule filterlim_compose [OF _ *])
(use ‹is_pole f z› in ‹simp add: is_pole_def›)
ultimately show False
using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
qed

text ‹The proposition
\<^term>‹∃x. ((f::complex⇒complex) ⤏ x) (at z) ∨ is_pole f z›
can be interpreted as the complex function \<^term>‹f› has a non-essential singularity at \<^term>‹z›
(i.e. the singularity is either removable or a pole).›
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})"

lemma not_essential_cong:
assumes "eventually (λx. f x = g x) (at z)" "z = z'"
shows   "not_essential f z ⟷ not_essential g z'"
unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce

lemma not_essential_compose_iff:
assumes "filtermap g (at z) = at z'"
shows   "not_essential (f ∘ g) z = not_essential f z'"
unfolding not_essential_def filterlim_def filtermap_compose assms is_pole_compose_iff[OF assms]
by blast

lemma isolated_singularity_at_cong:
assumes "eventually (λx. f x = g x) (at z)" "z = z'"
shows   "isolated_singularity_at f z ⟷ isolated_singularity_at g z'"
proof -
have "isolated_singularity_at g z"
if "isolated_singularity_at f z" "eventually (λx. f x = g x) (at z)" for f g
proof -
from that(1) obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
by (auto simp: isolated_singularity_at_def)
from that(2) obtain r' where r': "r' > 0" "∀x∈ball z r'-{z}. f x = g x"
unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_commute)

have "f holomorphic_on ball z r - {z}"
using r(2) by (subst (asm) analytic_on_open) auto
hence "f holomorphic_on ball z (min r r') - {z}"
by (rule holomorphic_on_subset) auto
also have "?this ⟷ g holomorphic_on ball z (min r r') - {z}"
using r' by (intro holomorphic_cong) auto
also have "… ⟷ g analytic_on ball z (min r r') - {z}"
by (subst analytic_on_open) auto
finally show ?thesis
unfolding isolated_singularity_at_def
by (intro exI[of _ "min r r'"]) (use ‹r > 0› ‹r' > 0› in auto)
qed
from this[of f g] this[of g f] assms show ?thesis
by (auto simp: eq_commute)
qed

lemma removable_singularity:
assumes "f holomorphic_on A - {x}" "open A"
assumes "f ─x→ c"
shows   "(λy. if y = x then c else f y) holomorphic_on A" (is "?g holomorphic_on _")
proof -
have "continuous_on A ?g"
unfolding continuous_on_def
proof
fix y assume y: "y ∈ A"
show "(?g ⤏ ?g y) (at y within A)"
proof (cases "y = x")
case False
have "continuous_on (A - {x}) f"
using assms(1) by (meson holomorphic_on_imp_continuous_on)
hence "(f ⤏ ?g y) (at y within A - {x})"
using False y by (auto simp: continuous_on_def)
also have "?this ⟷ (?g ⤏ ?g y) (at y within A - {x})"
by (intro filterlim_cong refl) (auto simp: eventually_at_filter)
also have "at y within A - {x} = at y within A"
using y assms False
by (intro at_within_nhd[of _ "A - {x}"]) auto
finally show ?thesis .
next
case [simp]: True
have "f ─x→ c"
by fact
also have "?this ⟷ (?g ⤏ ?g y) (at y)"
by (intro filterlim_cong) (auto simp: eventually_at_filter)
finally show ?thesis
by (meson Lim_at_imp_Lim_at_within)
qed
qed
moreover {
have "?g holomorphic_on A - {x}"
using assms(1) holomorphic_transform by fastforce
}
ultimately show ?thesis
by (rule no_isolated_singularity) (use assms in auto)
qed

lemma removable_singularity':
assumes "isolated_singularity_at f z"
assumes "f ─z→ c"
shows   "(λy. if y = z then c else f y) analytic_on {z}"
proof -
from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
by (auto simp: isolated_singularity_at_def)
have "(λy. if y = z then c else f y) holomorphic_on ball z r"
proof (rule removable_singularity)
show "f holomorphic_on ball z r - {z}"
using r(2) by (subst (asm) analytic_on_open) auto
qed (use assms in auto)
thus ?thesis
using r(1) unfolding analytic_at by (intro exI[of _ "ball z r"]) auto
qed

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) powi n ∧ g w≠0 ∧ f w =  h w * (w - z) powi 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›
have False when "n>m"
proof -
have "(h ⤏ 0) (at z within ball z r)"
proof (rule Lim_transform_within[OF _ ‹r>0›, where f="λw. (w - z) powi (n - m) * g w"])
have "∀w∈ball z r-{z}. h w = (w-z)powi(n-m) * g w"
using ‹n>m› asm ‹r>0› by (simp add: field_simps power_int_diff) force
then show "⟦x' ∈ ball z r; 0 < dist x' z;dist x' z < r⟧
⟹ (x' - z) powi (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' ≡ λx. (x - z) powi (n-m)"
have "f' z=0" using ‹n>m› unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
using ‹n>m›
by (auto simp add: Lim_ident_at  intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' ⤏ 0) F" unfolding F_def
moreover have "(g ⤏ g z) F"
unfolding F_def
using ‹r>0› centre_in_ball continuous_on_def g_holo holomorphic_on_imp_continuous_on by blast
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]
ultimately have "h z=0" by (auto intro!: tendsto_unique)
thus False using ‹h z≠0› 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 _ ‹r>0›, where f="λw. (w - z) powi (m - n) * h w"])
have "∀w∈ball z r -{z}. g w = (w-z) powi (m-n) * h w" using ‹m>n› asm
then show "⟦x' ∈ ball z r; 0 < dist x' z;dist x' z < r⟧
⟹ (x' - z) powi (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' ≡λx. (x - z) powi (m-n)"
have "f' z=0" using ‹m>n› unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
using ‹m>n›
by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' ⤏ 0) F" unfolding F_def
moreover have "(h ⤏ h z) F"
using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] ‹r>0›
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]
ultimately have "g z=0" by (auto intro!: tendsto_unique)
thus False using ‹g z≠0› 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" ― ‹\<^term>‹f› has either a removable singularity or a pole at \<^term>‹z››
and non_zero:"∃⇩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
∧ (∀w∈cball z r-{z}. f w = g w * (w-z) powi n ∧ g w≠0)"
proof -
define P where "P = (λf n g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z≠0
∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n  ∧ g w≠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) powi 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 ‹r1>0› ‹r2>0› unfolding r_def by auto
moreover have "∀w∈ball z r-{z}. f w = g1 w * (w-z) powi n1 ∧ g1 w≠0
∧ f w = g2 w * (w - z) powi n2  ∧ g2 w≠0"
using ‹fac n1 g1 r1› ‹fac n2 g2 r2›   unfolding fac_def r_def
by fastforce
ultimately show "n1=n2"
using g1_holo g2_holo ‹g1 z≠0› ‹g2 z≠0›
apply (elim holomorphic_factor_unique)
qed

have P_exist:"∃ n g r. P h n g r" when
"∃z'. (h ⤏ z') (at z)" "isolated_singularity_at h z"  "∃⇩Fw in (at z). h w≠0"
for h
proof -
from that(2) obtain r where "r>0" and r: "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'=(λx. if x=z then z' else h x)"
have "h' holomorphic_on ball z r"
proof (rule no_isolated_singularity'[of "{z}"])
show "⋀w. w ∈ {z} ⟹ (h' ⤏ h' w) (at w within ball z r)"
by (simp add: LIM_cong Lim_at_imp_Lim_at_within ‹h ─z→ z'› h'_def)
show "h' holomorphic_on ball z r - {z}"
using r analytic_imp_holomorphic h'_def holomorphic_transform by fastforce
qed 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 ‹∃⇩Fw in (at z). h w≠0› unfolding constant_on_def frequently_def eventually_at h'_def
by (metis ‹0 < r› centre_in_ball dist_commute mem_ball that)
moreover note ‹h' holomorphic_on ball z r›
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 ‹h' holomorphic_on ball z r› ‹r>0› ‹h' z=0› ‹¬ h' constant_on ball z r›]
define rr where "rr=r1/2"
have "P h' n g rr"
unfolding P_def rr_def
using ‹n>0› ‹r1>0› 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 ‹h ─z→ z'› ‹z'≠0› 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 ‹r2>0› ‹r>0› 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 ‹h' holomorphic_on ball z r› 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 "∀⇩F z in at z. f z ≠ 0"
using ‹is_pole f z› 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
show ?thesis
using e1 e2 by (force intro: that[of "min e1 e2"])
qed

define h where "h ≡ λx. inverse (f x)"
have "∃n g r. P h n g r"
proof -
have "(λx. inverse (f x)) analytic_on ball z e - {z}"
by (metis e_holo e_nz open_ball analytic_on_open holomorphic_on_inverse open_delete)
moreover have "h ─z→ 0"
using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce
moreover have "∃⇩Fw in (at z). h w≠0"
using non_zero by (simp add: h_def)
ultimately show ?thesis
using P_exist[of h] ‹e > 0›
unfolding isolated_singularity_at_def h_def
by blast
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) powi 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) powi (- n)" when "w∈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 ‹r>0› g_holo g_fac ‹g z≠0› by (auto intro:holomorphic_intros)
qed
then show "∃x g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z ≠ 0
∧ (∀w∈cball z r - {z}. f w = g w * (w - z) powi x  ∧ g w ≠ 0)"
unfolding P_def by blast
qed
ultimately show ?thesis using ‹not_essential f z› unfolding not_essential_def  by presburger
qed

lemma not_essential_transform:
assumes "not_essential g z"
assumes "∀⇩F w in (at z). g w = f w"
shows "not_essential f z"
using assms unfolding not_essential_def

lemma isolated_singularity_at_transform:
assumes "isolated_singularity_at g z"
assumes "∀⇩F w in (at z). g w = f w"
shows "isolated_singularity_at f z"
using assms isolated_singularity_at_cong by blast

lemma not_essential_powr[singularity_intros]:
assumes "LIM w (at z). f w :> (at x)"
shows "not_essential (λw. (f w) powi n) z"
proof -
define fp where "fp=(λw. (f w) powi 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
by (smt (verit) LIM_cong power_int_def that)
then show ?thesis unfolding not_essential_def fp_def by auto
qed
moreover have ?thesis when "n=0"
proof -
have "∀⇩F x in at z. fp x = 1"
using that filterlim_at_within_not_equal[OF assms] by (auto simp: fp_def)
then have "fp ─z→ 1"
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 "(λx. f x ^ nat (- n)) ─z→ 0"
using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
moreover have "∀⇩F x in at z. f x ^ nat (- n) ≠ 0"
by (smt (verit) True assms eventually_at_topological filterlim_at power_eq_0_iff)
ultimately have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
by (metis filterlim_atI filterlim_compose filterlim_inverse_at_infinity)
then have "LIM w (at z). fp w :> at_infinity"
proof (elim filterlim_mono_eventually)
show "∀⇩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
by (smt (verit) eventuallyI power_int_def power_inverse that)
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"
by (smt (verit, best) LIM_cong fp_def power_int_def power_inverse 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" "∀⇩F w in (at z). f w≠0"
shows "isolated_singularity_at (λw. (f w) powi 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) powi n) holomorphic_on ball z r3 - {z}"
by (intro holomorphic_on_power_int) (use r1 r2 in ‹auto simp: dist_commute r3_def›)
moreover have "r3>0" unfolding r3_def using ‹0 < r1› ‹0 < r2› by linarith
ultimately show ?thesis
by (meson open_ball analytic_on_open isolated_singularity_at_def open_delete)
qed

lemma non_zero_neighbour:
assumes f_iso:"isolated_singularity_at f z"
and f_ness:"not_essential f z"
and f_nconst:"∃⇩Fw in (at z). f w≠0"
shows "∀⇩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) powi 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) powi fn" "fp w ≠ 0"
using fr(2)[rule_format, of w] using that by (auto simp add:dist_commute)
moreover have "(w - z) powi fn ≠0"
unfolding powr_eq_0_iff using ‹w≠z› by auto
ultimately show ?thesis by auto
qed
then show ?thesis using ‹fr>0› unfolding eventually_at by auto
qed

lemma non_zero_neighbour_pole:
assumes "is_pole f z"
shows "∀⇩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 "∀⇩F w in (at z). f w≠0 ∧ w∈S"
proof (cases "f z = 0")
case True
from isolated_zeros[OF holo ‹open S› ‹connected S› ‹z ∈ S› True ‹β ∈ S› ‹f β ≠ 0›]
obtain r where "0 < r" "ball z r ⊆ S" "∀w ∈ ball z r - {z}.f w ≠ 0" by metis
then show ?thesis
by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
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 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)
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 "¬ ((∃⇩Fw in (at z). f w≠0) ∧ (∃⇩Fw in (at z). g w≠0))"
proof -
have "∀⇩Fw in (at z). fg w=0"
using fg_def frequently_elim1 not_eventually that by fastforce
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:"∃⇩Fw in (at z). f w≠0" and g_nconst:"∃⇩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) powi 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) powi 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  ‹fr>0› ‹gr>0› by auto
have fg_times:"fg w = (fp w * gp w) * (w - z) powi (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) powi 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) powi 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) powi (fn+gn)" "fp w*gp w≠0"
qed

have [intro]: "fp ─z→fp z" "gp ─z→gp z"
using fr(1) ‹fr>0› gr(1) ‹gr>0›
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 _ ‹r1>0›])
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
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 _ ‹r1>0›])
apply (subst fg_times)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
moreover have ?thesis when "fn+gn<0"
proof -
have "LIM x at z. (x - z) ^ nat (- (fn + gn)) :> at 0"
using eventually_at_topological that
by (force intro!: tendsto_eq_intros filterlim_atI)
moreover have "∃c. (λc. fp c * gp c) ─z→ c ∧ 0 ≠ c"
using ‹fp ─z→ fp z› ‹gp ─z→ gp z› tendsto_mult by fastforce
ultimately have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity"
using filterlim_divide_at_infinity by blast
then have "is_pole fg z" unfolding is_pole_def
apply (elim filterlim_transform_within[OF _ _ ‹r1>0›])
using that
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 "¬(∃⇩Fw in (at z). f w≠0)"
proof -
have "∀⇩Fw in (at z). f w=0"
using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
then have "vf ─z→0"
unfolding vf_def by (simp add: tendsto_eventually)
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:"∃⇩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 "∀⇩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 show ?thesis unfolding not_essential_def vf_def
using filterlim_atI filterlim_inverse_at_iff is_pole_def by blast
qed
moreover have ?thesis when "fz≠0"
using fz not_essential_def tendsto_inverse that by blast
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 "¬(∃⇩Fw in (at z). f w≠0)"
proof -
have "∀⇩Fw in (at z). f w=0"
using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
then have "∀⇩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"])
then have "vf analytic_on ball z d1 - {z}"
then show ?thesis using ‹d1>0› unfolding isolated_singularity_at_def vf_def by auto
qed
moreover have ?thesis when f_nconst:"∃⇩Fw in (at z). f w≠0"
proof -
have "∀⇩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 ‹d1>0› ‹d2>0› by auto
moreover
have "f analytic_on ball z d3 - {z}"
by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
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
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"
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"
shows isolated_singularity_at_times[singularity_intros]:
"isolated_singularity_at (λw. f w * g w) z"
"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 ‹d1>0› ‹d2>0› by auto

have fan: "f analytic_on ball z d3 - {z}"
by (smt (verit, best) Diff_iff analytic_on_analytic_at d1 d3_def mem_ball)
have gan: "g analytic_on ball z d3 - {z}"
by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
have "(λw. f w * g w) analytic_on ball z d3 - {z}"
using analytic_on_mult fan gan by blast
then show "isolated_singularity_at (λw. f w * g w) z"
using ‹d3>0› unfolding isolated_singularity_at_def by auto
have "(λw. f w + g w) analytic_on ball z d3 - {z}"
using analytic_on_add fan gan by blast
then show "isolated_singularity_at (λw. f w + g w) z"
using ‹d3>0› 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 "isolated_singularity_at f z" and "isolated_singularity_at g z"
shows "isolated_singularity_at (λw. f w - g w) z"
using assms isolated_singularity_at_add isolated_singularity_at_uminus by blast

lemma isolated_singularity_at_divide[singularity_intros]:
assumes "isolated_singularity_at f z"
and "isolated_singularity_at g z"
and "not_essential g z"
shows "isolated_singularity_at (λw. f w / g w) z"
unfolding divide_inverse
by (simp add: assms isolated_singularity_at_inverse isolated_singularity_at_times)

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)

lemma isolated_singularity_at_altdef:
"isolated_singularity_at f z ⟷ eventually (λz. f analytic_on {z}) (at z)"
proof
assume "isolated_singularity_at f z"
then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
unfolding isolated_singularity_at_def by blast
have "eventually (λw. w ∈ ball z r - {z}) (at z)"
using r(1) by (intro eventually_at_in_open) auto
thus "eventually (λz. f analytic_on {z}) (at z)"
by eventually_elim (use r analytic_on_subset in auto)
next
assume "eventually (λz. f analytic_on {z}) (at z)"
then obtain A where A: "open A" "z ∈ A" "⋀w. w ∈ A - {z} ⟹ f analytic_on {w}"
unfolding eventually_at_topological by blast
then show "isolated_singularity_at f z"
by (meson analytic_imp_holomorphic analytic_on_analytic_at isolated_singularity_at_holomorphic)
qed

lemma isolated_singularity_at_shift:
assumes "isolated_singularity_at (λx. f (x + w)) z"
shows   "isolated_singularity_at f (z + w)"
proof -
from assms obtain r where r: "r > 0" and ana: "(λx. f (x + w)) analytic_on ball z r - {z}"
unfolding isolated_singularity_at_def by blast
have "((λx. f (x + w)) ∘ (λx. x - w)) analytic_on (ball (z + w) r - {z + w})"
by (rule analytic_on_compose_gen[OF _ ana])
(auto simp: dist_norm algebra_simps intro!: analytic_intros)
hence "f analytic_on (ball (z + w) r - {z + w})"
thus ?thesis using r
unfolding isolated_singularity_at_def by blast
qed

lemma isolated_singularity_at_shift_iff:
"isolated_singularity_at f (z + w) ⟷ isolated_singularity_at (λx. f (x + w)) z"
using isolated_singularity_at_shift[of f w z]
isolated_singularity_at_shift[of "λx. f (x + w)" "-w" "w + z"]
by (auto simp: algebra_simps)

lemma isolated_singularity_at_shift_0:
"NO_MATCH 0 z ⟹ isolated_singularity_at f z ⟷ isolated_singularity_at (λx. f (z + x)) 0"

lemma not_essential_shift:
assumes "not_essential (λx. f (x + w)) z"
shows   "not_essential f (z + w)"
proof -
from assms consider c where "(λx. f (x + w)) ─z→ c" | "is_pole (λx. f (x + w)) z"
unfolding not_essential_def by blast
thus ?thesis
proof cases
case (1 c)
hence "f ─z + w→ c"
by (smt (verit, ccfv_SIG) LIM_cong add.assoc filterlim_at_to_0)
thus ?thesis
by (auto simp: not_essential_def)
next
case 2
hence "is_pole f (z + w)"
by (subst is_pole_shift_iff [symmetric]) (auto simp: o_def add_ac)
thus ?thesis
by (auto simp: not_essential_def)
qed
qed

lemma not_essential_shift_iff: "not_essential f (z + w) ⟷ not_essential (λx. f (x + w)) z"
using not_essential_shift[of f w z]
not_essential_shift[of "λx. f (x + w)" "-w" "w + z"]
by (auto simp: algebra_simps)

lemma not_essential_shift_0:
"NO_MATCH 0 z ⟹ not_essential f z ⟷ not_essential (λx. f (z + x)) 0"

lemma not_essential_holomorphic:
assumes "f holomorphic_on A" "x ∈ A" "open A"
shows   "not_essential f x"
by (metis assms at_within_open continuous_on holomorphic_on_imp_continuous_on not_essential_def)

lemma not_essential_analytic:
assumes "f analytic_on {z}"
shows   "not_essential f z"
using analytic_at assms not_essential_holomorphic by blast

lemma not_essential_id [singularity_intros]: "not_essential (λw. w) z"

lemma is_pole_imp_not_essential [intro]: "is_pole f z ⟹ not_essential f z"
by (auto simp: not_essential_def)

lemma tendsto_imp_not_essential [intro]: "f ─z→ c ⟹ not_essential f z"
by (auto simp: not_essential_def)

lemma eventually_not_pole:
assumes "isolated_singularity_at f z"
shows   "eventually (λw. ¬is_pole f w) (at z)"
proof -
from assms obtain r where "r > 0" and r: "f analytic_on ball z r - {z}"
by (auto simp: isolated_singularity_at_def)
then have "eventually (λw. w ∈ ball z r - {z}) (at z)"
by (intro eventually_at_in_open) auto
thus "eventually (λw. ¬is_pole f w) (at z)"
by (metis (no_types, lifting) analytic_at analytic_on_analytic_at eventually_mono not_is_pole_holomorphic r)
qed

lemma not_islimpt_poles:
assumes "isolated_singularity_at f z"
shows   "¬z islimpt {w. is_pole f w}"
using eventually_not_pole [OF assms]
by (auto simp: islimpt_conv_frequently_at frequently_def)

lemma analytic_at_imp_no_pole: "f analytic_on {z} ⟹ ¬is_pole f z"
using analytic_at not_is_pole_holomorphic by blast

lemma not_essential_const [singularity_intros]: "not_essential (λ_. c) z"
by blast

lemma not_essential_uminus [singularity_intros]:
assumes f_ness: "not_essential f z"
assumes f_iso:"isolated_singularity_at f z"
shows "not_essential (λw. -f w) z"
proof -
have "not_essential (λw. -1 * f w) z"
by (intro assms singularity_intros)
thus ?thesis by simp
qed

lemma isolated_singularity_at_analytic:
assumes "f analytic_on {z}"
shows   "isolated_singularity_at f z"
by (meson Diff_subset analytic_at assms holomorphic_on_subset isolated_singularity_at_holomorphic)

subsection ‹The order of non-essential singularities (i.e. removable singularities or poles)›

definition✐‹tag important› zorder :: "(complex ⇒ complex) ⇒ complex ⇒ int" where
"zorder f z = (THE n. (∃h r. r>0 ∧ h holomorphic_on cball z r ∧ h z≠0
∧ (∀w∈cball z r - {z}. f w =  h w * (w-z) powi n
∧ h w ≠0)))"

definition✐‹tag important› 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
∧ (∀w∈cball z r - {z}. f w =  h w * (w - z) powi (zorder f z)
∧ h w ≠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:"∃⇩Fw in (at z). f w≠0"
shows "g z≠0 ∧ (∃r. r>0 ∧ g holomorphic_on cball z r
∧ (∀w∈cball z r - {z}. f w  = g w * (w-z) powi n  ∧ g w ≠0))"
proof -
define P where "P = (λn g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z≠0
∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w≠0))"
have "∃!k. ∃g r. P k 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 zorder_shift:
shows  "zorder f z = zorder (λu. f (u + z)) 0"
unfolding zorder_def
apply (rule arg_cong [of concl: The])
apply (auto simp: fun_eq_iff Ball_def dist_norm)
subgoal for x h r
apply (rule_tac x="h o (+)z" in exI)
apply (rule_tac x="r" in exI)
apply (intro conjI holomorphic_on_compose holomorphic_intros)
apply (simp_all flip: cball_translation)
done
subgoal for x h r
apply (rule_tac x="h o (λu. u-z)" in exI)
apply (rule_tac x="r" in exI)
apply (intro conjI holomorphic_on_compose holomorphic_intros)
done

lemma zorder_shift': "NO_MATCH 0 z ⟹ zorder f z = zorder (λu. f (u + z)) 0"
by (rule zorder_shift)

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:"∃⇩Fw in (at z). f w≠0"
shows zorder_inverse: "zorder (λw. inverse (f w)) z = - zorder f z"
and zor_poly_inverse: "∀⇩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) powi 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) powi (-fn)"
and fr_nz: "inverse (fp w) ≠ 0"
when "w∈ball z fr - {z}" for w
proof -
have "f w = fp w * (w - z) powi fn" "fp w ≠ 0"
using fr(2) that by auto
then show "vf w = (inverse (fp w)) * (w - z) powi (-fn)" "inverse (fp w)≠0"
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) powi 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 "∃⇩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 ‹fr>0› ‹vfr>0› unfolding r1_def by simp
show "vfn = - fn"
proof (rule holomorphic_factor_unique)
have §: "⋀w. ⟦fp w = 0; dist z w < fr⟧ ⟹ False"
using fr_nz by force
then show "∀w∈ball z r1 - {z}.
vf w = vfp w * (w - z) powi vfn ∧
vfp w ≠ 0 ∧ vf w = inverse (fp w) * (w - z) powi (- fn) ∧
inverse (fp w) ≠ 0"
using fr_inverse r1_def vfr(2)
by (smt (verit) Diff_iff inverse_nonzero_iff_nonzero mem_ball mem_cball)
show "vfp holomorphic_on ball z r1"
using r1_def vfr(1) by auto
show "(λw. inverse (fp w)) holomorphic_on ball z r1"
by (metis § ball_subset_cball fr(1) holomorphic_on_inverse holomorphic_on_subset mem_ball min.cobounded2 min.commute r1_def subset_ball)
qed (use ‹r1>0› in auto)
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)] ‹vfn = - fn› ‹w≠z›
show ?thesis by auto
qed
then show "∀⇩Fw in (at z). vfp w = inverse (fp w)"
unfolding eventually_at using ‹r1>0›
by (metis DiffI dist_commute mem_ball singletonD)
qed

lemma zor_poly_shift:
assumes iso1: "isolated_singularity_at f z"
and ness1: "not_essential f z"
and nzero1: "∃⇩F w in at z. f w ≠ 0"
shows "∀⇩F w in nhds z. zor_poly f z w = zor_poly (λu. f (z + u)) 0 (w-z)"
proof -
obtain r1 where "r1>0" "zor_poly f z z ≠ 0" and
holo1:"zor_poly f z holomorphic_on cball z r1" and
rball1:"∀w∈cball z r1 - {z}.
f w = zor_poly f z w * (w - z) powi (zorder f z) ∧
zor_poly f z w ≠ 0"
using zorder_exist[OF iso1 ness1 nzero1] by blast

define ff where "ff=(λu. f (z + u))"
have "isolated_singularity_at ff 0"
unfolding ff_def
using iso1 isolated_singularity_at_shift_iff[of f 0 z]
moreover have "not_essential ff 0"
unfolding ff_def
using ness1 not_essential_shift_iff[of f 0 z]
moreover have "∃⇩F w in at 0. ff w ≠ 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 ≠ 0" and
holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
rball2:"∀w∈cball 0 r2 - {0}.
ff w = zor_poly ff 0 w * w powi (zorder ff 0) ∧
zor_poly ff 0 w ≠ 0"
using zorder_exist[of ff 0] by auto

define r where "r=min r1 r2"
have "r>0" using ‹r1>0› ‹r2>0› unfolding r_def by auto

have "zor_poly f z w = zor_poly ff 0 (w - z)"
if "w∈ball z r - {z}" for w
proof -
define n where "n ≡ zorder f z"

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"
proof -
have "w-z∈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
moreover have "of_int (zorder ff 0) = n"
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"
by auto
moreover have "(w - z) powi n ≠0"
using that by auto
ultimately show ?thesis
using mult_cancel_right by blast
qed
then have "∀⇩F w in at z. zor_poly f z w
= zor_poly ff 0 (w - z)"
unfolding eventually_at
by (metis DiffI ‹0 < r› dist_commute mem_ball singletonD)
moreover have "isCont (zor_poly f z) z"
using holo1[THEN holomorphic_on_imp_continuous_on]
by (simp add: ‹0 < r1› continuous_on_interior)
moreover
have "isCont (zor_poly ff 0) 0"
using ‹0 < r2› centre_in_ball continuous_on_interior holo2 holomorphic_on_imp_continuous_on interior_cball by blast
then have "isCont (λw. zor_poly ff 0 (w - z)) z"
unfolding isCont_iff by simp
ultimately show "∀⇩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 ⇒ 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: "∃⇩Fw in (at z). f w * g w≠ 0"
shows zorder_times:"```