Theory HOL-Complex_Analysis.Meromorphic
theory Meromorphic imports
Laurent_Convergence
Cauchy_Integral_Formula
"HOL-Analysis.Sparse_In"
begin
subsection ‹Remove singular points›
text ‹
This function takes a complex function and returns a version of it where all removable
singularities have been removed and all other singularities (to be more precise,
unremovable discontinuities) are set to 0.
This is very useful since it is sometimes difficult to avoid introducing removable singularities.
For example, consider the meromorphic functions $f(z) = z$ and $g(z) = 1/z$.
Then a mathematician would write $f(z)g(z) = 1$, but in Isabelle of course this is not so.
Using the ‹remove_sings› function, we indeed have ‹remove_sings (λz. f z * g z) = (λ_. 1)›.
›
definition%important remove_sings :: "(complex ⇒ complex) ⇒ complex ⇒ complex" where
"remove_sings f z = (if ∃c. f ─z→ c then Lim (at z) f else 0)"
lemma remove_sings_eqI [intro]:
assumes "f ─z→ c"
shows "remove_sings f z = c"
using assms unfolding remove_sings_def by (auto simp: tendsto_Lim)
lemma remove_sings_at_analytic [simp]:
assumes "f analytic_on {z}"
shows "remove_sings f z = f z"
using assms by (intro remove_sings_eqI) (simp add: analytic_at_imp_isCont isContD)
lemma remove_sings_at_pole [simp]:
assumes "is_pole f z"
shows "remove_sings f z = 0"
using assms unfolding remove_sings_def is_pole_def
by (meson at_neq_bot not_tendsto_and_filterlim_at_infinity)
lemma eventually_remove_sings_eq_at:
assumes "isolated_singularity_at f z"
shows "eventually (λw. remove_sings f w = f w) (at z)"
proof -
from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
by (auto simp: isolated_singularity_at_def)
hence *: "f analytic_on {w}" if "w ∈ ball z r - {z}" for w
using r that by (auto intro: analytic_on_subset)
have "eventually (λw. w ∈ ball z r - {z}) (at z)"
using r by (intro eventually_at_in_open) auto
thus ?thesis
by eventually_elim (auto simp: remove_sings_at_analytic * )
qed
lemma eventually_remove_sings_eq_nhds:
assumes "f analytic_on {z}"
shows "eventually (λw. remove_sings f w = f w) (nhds z)"
proof -
from assms obtain A where A: "open A" "z ∈ A" "f holomorphic_on A"
by (auto simp: analytic_at)
have "eventually (λz. z ∈ A) (nhds z)"
by (intro eventually_nhds_in_open A)
thus ?thesis
proof eventually_elim
case (elim w)
from elim have "f analytic_on {w}"
using A analytic_at by blast
thus ?case by auto
qed
qed
lemma remove_sings_compose:
assumes "filtermap g (at z) = at z'"
shows "remove_sings (f ∘ g) z = remove_sings f z'"
proof (cases "∃c. f ─z'→ c")
case True
then obtain c where c: "f ─z'→ c"
by auto
from c have "remove_sings f z' = c"
by blast
moreover from c have "remove_sings (f ∘ g) z = c"
using c by (intro remove_sings_eqI) (auto simp: filterlim_def filtermap_compose assms)
ultimately show ?thesis
by simp
next
case False
hence "¬(∃c. (f ∘ g) ─z→ c)"
by (auto simp: filterlim_def filtermap_compose assms)
with False show ?thesis
by (auto simp: remove_sings_def)
qed
lemma remove_sings_cong:
assumes "eventually (λx. f x = g x) (at z)" "z = z'"
shows "remove_sings f z = remove_sings g z'"
proof (cases "∃c. f ─z→ c")
case True
then obtain c where c: "f ─z→ c" by blast
hence "remove_sings f z = c"
by blast
moreover have "f ─z→ c ⟷ g ─z'→ c"
using assms by (intro filterlim_cong refl) auto
with c have "remove_sings g z' = c"
by (intro remove_sings_eqI) auto
ultimately show ?thesis
by simp
next
case False
have "f ─z→ c ⟷ g ─z'→ c" for c
using assms by (intro filterlim_cong) auto
with False show ?thesis
by (auto simp: remove_sings_def)
qed
lemma deriv_remove_sings_at_analytic [simp]:
assumes "f analytic_on {z}"
shows "deriv (remove_sings f) z = deriv f z"
apply (rule deriv_cong_ev)
apply (rule eventually_remove_sings_eq_nhds)
using assms by auto
lemma isolated_singularity_at_remove_sings [simp, intro]:
assumes "isolated_singularity_at f z"
shows "isolated_singularity_at (remove_sings f) z"
using isolated_singularity_at_cong[OF eventually_remove_sings_eq_at[OF assms] refl] assms
by simp
lemma not_essential_remove_sings_iff [simp]:
assumes "isolated_singularity_at f z"
shows "not_essential (remove_sings f) z ⟷ not_essential f z"
using not_essential_cong[OF eventually_remove_sings_eq_at[OF assms(1)] refl]
by simp
lemma not_essential_remove_sings [intro]:
assumes "isolated_singularity_at f z" "not_essential f z"
shows "not_essential (remove_sings f) z"
by (subst not_essential_remove_sings_iff) (use assms in auto)
lemma
assumes "isolated_singularity_at f z"
shows is_pole_remove_sings_iff [simp]:
"is_pole (remove_sings f) z ⟷ is_pole f z"
and zorder_remove_sings [simp]:
"zorder (remove_sings f) z = zorder f z"
and zor_poly_remove_sings [simp]:
"zor_poly (remove_sings f) z = zor_poly f z"
and has_laurent_expansion_remove_sings_iff [simp]:
"(λw. remove_sings f (z + w)) has_laurent_expansion F ⟷
(λw. f (z + w)) has_laurent_expansion F"
and tendsto_remove_sings_iff [simp]:
"remove_sings f ─z→ c ⟷ f ─z→ c"
by (intro is_pole_cong eventually_remove_sings_eq_at refl zorder_cong
zor_poly_cong has_laurent_expansion_cong' tendsto_cong assms)+
lemma get_all_poles_from_remove_sings:
fixes f:: "complex ⇒ complex"
defines "ff≡remove_sings f"
assumes f_holo:"f holomorphic_on s - pts" and "finite pts"
"pts⊆s" "open s" and not_ess:"∀x∈pts. not_essential f x"
obtains pts' where
"pts' ⊆ pts" "finite pts'" "ff holomorphic_on s - pts'" "∀x∈pts'. is_pole ff x"
proof -
define pts' where "pts' = {x∈pts. is_pole f x}"
have "pts' ⊆ pts" unfolding pts'_def by auto
then have "finite pts'" using ‹finite pts›
using rev_finite_subset by blast
then have "open (s - pts')" using ‹open s›
by (simp add: finite_imp_closed open_Diff)
have isolated:"isolated_singularity_at f z" if "z∈pts" for z
proof (rule isolated_singularity_at_holomorphic)
show "f holomorphic_on (s-(pts-{z})) - {z}"
by (metis Diff_insert f_holo insert_Diff that)
show " open (s - (pts - {z}))"
by (meson assms(3) assms(5) finite_Diff finite_imp_closed open_Diff)
show "z ∈ s - (pts - {z})"
using assms(4) that by auto
qed
have "ff holomorphic_on s - pts'"
proof (rule no_isolated_singularity')
show "(ff ⤏ ff z) (at z within s - pts')" if "z ∈ pts-pts'" for z
proof -
have "at z within s - pts' = at z"
apply (rule at_within_open)
using ‹open (s - pts')› that ‹pts⊆s› by auto
moreover have "ff ─z→ ff z"
unfolding ff_def
proof (subst tendsto_remove_sings_iff)
show "isolated_singularity_at f z"
apply (rule isolated)
using that by auto
have "not_essential f z"
using not_ess that by auto
moreover have "¬is_pole f z"
using that unfolding pts'_def by auto
ultimately have "∃c. f ─z→ c"
unfolding not_essential_def by auto
then show "f ─z→ remove_sings f z"
using remove_sings_eqI by blast
qed
ultimately show ?thesis by auto
qed
have "ff holomorphic_on s - pts"
using f_holo
proof (elim holomorphic_transform)
fix x assume "x ∈ s - pts"
then have "f analytic_on {x}"
using assms(3) assms(5) f_holo
by (meson finite_imp_closed
holomorphic_on_imp_analytic_at open_Diff)
from remove_sings_at_analytic[OF this]
show "f x = ff x" unfolding ff_def by auto
qed
then show "ff holomorphic_on s - pts' - (pts - pts')"
apply (elim holomorphic_on_subset)
by blast
show "open (s - pts')"
by (simp add: ‹open (s - pts')›)
show "finite (pts - pts')"
by (simp add: assms(3))
qed
moreover have "∀x∈pts'. is_pole ff x"
unfolding pts'_def
using ff_def is_pole_remove_sings_iff isolated by blast
moreover note ‹pts' ⊆ pts› ‹finite pts'›
ultimately show ?thesis using that by auto
qed
lemma remove_sings_eq_0_iff:
assumes "not_essential f w"
shows "remove_sings f w = 0 ⟷ is_pole f w ∨ f ─w→ 0"
proof (cases "is_pole f w")
case False
then obtain c where c:"f ─w→ c"
using ‹not_essential f w› unfolding not_essential_def by auto
then show ?thesis
using False remove_sings_eqI by auto
qed simp
subsection ‹Meromorphicity›
text ‹
We define meromorphicity in terms of Laurent series expansions. This has the advantage of
giving us a particularly simple definition that makes many of the lemmas below trivial because
they reduce to similar statements about Laurent series that are already in the library.
On open domains, this definition coincides with the usual one from the literature, namely that
the function be holomorphic on its domain except for a set of non-essential singularities that
is ∗‹sparse›, i.e.\ that has no limit point inside the domain.
However, unlike the definitions found in the literature, our definition also makes sense for
non-open domains: similarly to \<^const>‹analytic_on›, we consider a function meromorphic on a
non-open domain if it is meromorphic on some open superset of that domain.
We will prove all of this below.
›
definition%important meromorphic_on :: "(complex ⇒ complex) ⇒ complex set ⇒ bool"
(infixl ‹(meromorphic'_on)› 50) where
"f meromorphic_on A ⟷ (∀z∈A. ∃F. (λw. f (z + w)) has_laurent_expansion F)"
lemma meromorphic_at_iff: "f meromorphic_on {z} ⟷ isolated_singularity_at f z ∧ not_essential f z"
unfolding meromorphic_on_def
by (metis has_laurent_expansion_isolated has_laurent_expansion_not_essential
insertI1 singletonD not_essential_has_laurent_expansion)
named_theorems meromorphic_intros
lemma meromorphic_on_empty [simp, intro]: "f meromorphic_on {}"
by (auto simp: meromorphic_on_def)
lemma meromorphic_on_def':
"f meromorphic_on A ⟷ (∀z∈A. (λw. f (z + w)) has_laurent_expansion laurent_expansion f z)"
unfolding meromorphic_on_def using laurent_expansion_eqI by blast
lemma meromorphic_on_meromorphic_at: "f meromorphic_on A ⟷ (∀x∈A. f meromorphic_on {x})"
by (auto simp: meromorphic_on_def)
lemma meromorphic_on_altdef:
"f meromorphic_on A ⟷ (∀z∈A. isolated_singularity_at f z ∧ not_essential f z)"
by (subst meromorphic_on_meromorphic_at) (auto simp: meromorphic_at_iff)
lemma meromorphic_on_cong:
assumes "⋀z. z ∈ A ⟹ eventually (λw. f w = g w) (at z)" "A = B"
shows "f meromorphic_on A ⟷ g meromorphic_on B"
unfolding meromorphic_on_def using assms
by (intro ball_cong refl arg_cong[of _ _ Ex] has_laurent_expansion_cong ext)
(simp_all add: at_to_0' eventually_filtermap add_ac)
lemma meromorphic_on_subset: "f meromorphic_on A ⟹ B ⊆ A ⟹ f meromorphic_on B"
by (auto simp: meromorphic_on_def)
lemma meromorphic_on_Un:
assumes "f meromorphic_on A" "f meromorphic_on B"
shows "f meromorphic_on (A ∪ B)"
using assms unfolding meromorphic_on_def by blast
lemma meromorphic_on_Union:
assumes "⋀A. A ∈ B ⟹ f meromorphic_on A"
shows "f meromorphic_on (⋃B)"
using assms unfolding meromorphic_on_def by blast
lemma meromorphic_on_UN:
assumes "⋀x. x ∈ X ⟹ f meromorphic_on (A x)"
shows "f meromorphic_on (⋃x∈X. A x)"
using assms unfolding meromorphic_on_def by blast
lemma meromorphic_on_imp_has_laurent_expansion:
assumes "f meromorphic_on A" "z ∈ A"
shows "(λw. f (z + w)) has_laurent_expansion laurent_expansion f z"
using assms laurent_expansion_eqI unfolding meromorphic_on_def by blast
lemma meromorphic_on_open_nhd:
assumes "f meromorphic_on A"
obtains B where "open B" "A ⊆ B" "f meromorphic_on B"
proof -
obtain F where F: "⋀z. z ∈ A ⟹ (λw. f (z + w)) has_laurent_expansion F z"
using assms unfolding meromorphic_on_def by metis
have "∃Z. open Z ∧ z ∈ Z ∧ (∀w∈Z-{z}. eval_fls (F z) (w - z) = f w)" if z: "z ∈ A" for z
proof -
obtain Z where Z: "open Z" "0 ∈ Z" "⋀w. w ∈ Z - {0} ⟹ eval_fls (F z) w = f (z + w)"
using F[OF z] unfolding has_laurent_expansion_def eventually_at_topological by blast
hence "open ((+) z ` Z)" and "z ∈ (+) z ` Z"
using open_translation by auto
moreover have "eval_fls (F z) (w - z) = f w" if "w ∈ (+) z ` Z - {z}" for w
using Z(3)[of "w - z"] that by auto
ultimately show ?thesis by blast
qed
then obtain Z where Z:
"⋀z. z ∈ A ⟹ open (Z z) ∧ z ∈ Z z ∧ (∀w∈Z z-{z}. eval_fls (F z) (w - z) = f w)"
by metis
define B where "B = (⋃z∈A. Z z ∩ eball z (fls_conv_radius (F z)))"
show ?thesis
proof (rule that[of B])
show "open B"
using Z unfolding B_def by auto
show "A ⊆ B"
unfolding B_def using F Z by (auto simp: has_laurent_expansion_def zero_ereal_def)
show "f meromorphic_on B"
unfolding meromorphic_on_def
proof
fix z assume z: "z ∈ B"
show "∃F. (λw. f (z + w)) has_laurent_expansion F"
proof (cases "z ∈ A")
case True
thus ?thesis using F by blast
next
case False
then obtain z0 where z0: "z0 ∈ A" "z ∈ Z z0 - {z0}" "dist z0 z < fls_conv_radius (F z0)"
using z False Z unfolding B_def by auto
hence "(λw. eval_fls (F z0) (w - z0)) analytic_on {z}"
by (intro analytic_on_eval_fls' analytic_intros) (auto simp: dist_norm)
also have "?this ⟷ f analytic_on {z}"
proof (intro analytic_at_cong refl)
have "eventually (λw. w ∈ Z z0 - {z0}) (nhds z)"
using Z[of z0] z0 by (intro eventually_nhds_in_open) auto
thus "∀⇩F x in nhds z. eval_fls (F z0) (x - z0) = f x"
by eventually_elim (use Z[of z0] z0 in auto)
qed
finally show ?thesis
using analytic_at_imp_has_fps_expansion has_fps_expansion_to_laurent by blast
qed
qed
qed
qed
lemma meromorphic_on_not_essential:
assumes "f meromorphic_on {z}"
shows "not_essential f z"
using assms has_laurent_expansion_not_essential unfolding meromorphic_on_def by blast
lemma meromorphic_on_isolated_singularity:
assumes "f meromorphic_on {z}"
shows "isolated_singularity_at f z"
using assms has_laurent_expansion_isolated unfolding meromorphic_on_def by blast
lemma meromorphic_on_imp_not_islimpt_singularities:
assumes "f meromorphic_on A" "z ∈ A"
shows "¬z islimpt {w. ¬f analytic_on {w}}"
proof -
obtain B where B: "open B" "A ⊆ B" "f meromorphic_on B"
using assms meromorphic_on_open_nhd by blast
obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
using B assms(2) unfolding meromorphic_on_def by blast
from F have "isolated_singularity_at f z"
using has_laurent_expansion_isolated assms(2) by blast
then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
unfolding isolated_singularity_at_def by blast
have "f analytic_on {w}" if "w ∈ ball z r - {z}" for w
by (rule analytic_on_subset[OF r(2)]) (use that in auto)
hence "eventually (λw. f analytic_on {w}) (at z)"
using eventually_at_in_open[of "ball z r" z] ‹r > 0› by (auto elim!: eventually_mono)
thus "¬z islimpt {w. ¬f analytic_on {w}}"
by (auto simp: islimpt_conv_frequently_at frequently_def)
qed
lemma meromorphic_on_imp_sparse_singularities:
assumes "f meromorphic_on A"
shows "{w. ¬f analytic_on {w}} sparse_in A"
by (metis assms meromorphic_on_imp_not_islimpt_singularities
meromorphic_on_open_nhd sparse_in_open sparse_in_subset)
lemma meromorphic_on_imp_sparse_singularities':
assumes "f meromorphic_on A"
shows "{w∈A. ¬f analytic_on {w}} sparse_in A"
using meromorphic_on_imp_sparse_singularities[OF assms]
by (rule sparse_in_subset2) auto
lemma meromorphic_onE:
assumes "f meromorphic_on A"
obtains pts where "pts ⊆ A" "pts sparse_in A" "f analytic_on A - pts"
"⋀z. z ∈ A ⟹ not_essential f z" "⋀z. z ∈ A ⟹ isolated_singularity_at f z"
proof (rule that)
show "{z ∈ A. ¬ f analytic_on {z}} sparse_in A"
using assms by (rule meromorphic_on_imp_sparse_singularities')
show "f analytic_on A - {z ∈ A. ¬ f analytic_on {z}}"
by (subst analytic_on_analytic_at) auto
qed (use assms in ‹auto intro: meromorphic_on_isolated_singularity meromorphic_on_not_essential meromorphic_on_subset›)
lemma meromorphic_onI_weak:
assumes "f analytic_on A - pts" "⋀z. z ∈ pts ⟹ not_essential f z" "pts sparse_in A"
"pts ∩ frontier A = {}"
shows "f meromorphic_on A"
unfolding meromorphic_on_def
proof
fix z assume z: "z ∈ A"
show "(∃F. (λw. f (z + w)) has_laurent_expansion F)"
proof (cases "z ∈ pts")
case False
have "f analytic_on {z}"
using assms(1) by (rule analytic_on_subset) (use False z in auto)
thus ?thesis
using isolated_singularity_at_analytic not_essential_analytic
not_essential_has_laurent_expansion by blast
next
case True
show ?thesis
proof (rule exI, rule not_essential_has_laurent_expansion)
show "not_essential f z"
using assms(2) True by blast
next
show "isolated_singularity_at f z"
proof (rule isolated_singularity_at_holomorphic)
show "open (interior A - (pts - {z}))"
proof (rule open_diff_sparse_pts)
show "pts - {z} sparse_in interior A"
using sparse_in_subset sparse_in_subset2 assms interior_subset Diff_subset by metis
qed auto
next
have "f analytic_on interior A - (pts - {z}) - {z}"
using assms(1) by (rule analytic_on_subset) (use interior_subset in blast)
thus "f holomorphic_on interior A - (pts - {z}) - {z}"
by (rule analytic_imp_holomorphic)
next
from assms(4) and True have "z ∈ interior A"
unfolding frontier_def using closure_subset z by blast
thus "z ∈ interior A - (pts - {z})"
by blast
qed
qed
qed
qed
lemma meromorphic_onI_open:
assumes "open A" "f analytic_on A - pts" "⋀z. z ∈ pts ⟹ not_essential f z"
assumes "⋀z. z ∈ A ⟹ ¬z islimpt pts ∩ A"
shows "f meromorphic_on A"
proof (rule meromorphic_onI_weak)
have *: "A - pts ∩ A = A - pts"
by blast
show "f analytic_on A - pts ∩ A"
unfolding * by fact
show "pts ∩ A sparse_in A"
using assms(1,4) by (subst sparse_in_open) auto
show "not_essential f z" if "z ∈ pts ∩ A" for z
using assms(3) that by blast
show "pts ∩ A ∩ frontier A = {}"
using ‹open A› frontier_disjoint_eq by blast
qed
lemma meromorphic_at_isCont_imp_analytic:
assumes "f meromorphic_on {z}" "isCont f z"
shows "f analytic_on {z}"
proof -
have *: "(λw. f (z + w)) has_laurent_expansion laurent_expansion f z"
using assms by (auto intro: meromorphic_on_imp_has_laurent_expansion)
from assms have "¬is_pole f z"
using is_pole_def not_tendsto_and_filterlim_at_infinity trivial_limit_at by (metis isContD)
with * have "fls_subdegree (laurent_expansion f z) ≥ 0"
using has_laurent_expansion_imp_is_pole linorder_not_le by blast
hence **: "(λw. eval_fls (laurent_expansion f z) (w - z)) analytic_on {z}"
by (intro analytic_intros)+ (use * in ‹auto simp: has_laurent_expansion_def zero_ereal_def›)
have "(λw. eval_fls (laurent_expansion f z) (w - z)) ─z→ eval_fls (laurent_expansion f z) (z - z)"
by (intro isContD analytic_at_imp_isCont **)
also have "?this ⟷ f ─z→ eval_fls (laurent_expansion f z) (z - z)"
by (intro filterlim_cong refl)
(use * in ‹auto simp: has_laurent_expansion_def at_to_0' eventually_filtermap add_ac›)
finally have "f ─z→ eval_fls (laurent_expansion f z) 0"
by simp
moreover from assms have "f ─z→ f z"
by (auto intro: isContD)
ultimately have ***: "eval_fls (laurent_expansion f z) 0 = f z"
by (rule LIM_unique)
have "eventually (λw. f w = eval_fls (laurent_expansion f z) (w - z)) (at z)"
using * by (simp add: has_laurent_expansion_def at_to_0' eventually_filtermap add_ac eq_commute)
hence "eventually (λw. f w = eval_fls (laurent_expansion f z) (w - z)) (nhds z)"
unfolding eventually_at_filter by eventually_elim (use *** in auto)
hence "f analytic_on {z} ⟷ (λw. eval_fls (laurent_expansion f z) (w - z)) analytic_on {z}"
by (intro analytic_at_cong refl)
with ** show ?thesis
by simp
qed
lemma analytic_on_imp_meromorphic_on:
assumes "f analytic_on A"
shows "f meromorphic_on A"
by (rule meromorphic_onI_weak[of _ _ "{}"]) (use assms in auto)
lemma meromorphic_on_compose:
assumes "g meromorphic_on A" "f analytic_on B" "f ` B ⊆ A"
shows "(λw. g (f w)) meromorphic_on B"
unfolding meromorphic_on_def
proof safe
fix z assume z: "z ∈ B"
have "f analytic_on {z}"
using assms(2) by (rule analytic_on_subset) (use assms(3) z in auto)
hence "(λw. f w - f z) analytic_on {z}"
by (intro analytic_intros)
then obtain F where F: "(λw. f (z + w) - f z) has_fps_expansion F"
using analytic_at_imp_has_fps_expansion by blast
from assms(3) and z have "f z ∈ A"
by auto
with assms(1) obtain G where G: "(λw. g (f z + w)) has_laurent_expansion G"
using z by (auto simp: meromorphic_on_def)
have "∃H. ((λw. g (f z + w)) ∘ (λw. f (z + w) - f z)) has_laurent_expansion H"
proof (cases "F = 0")
case False
show ?thesis
proof (rule exI, rule has_laurent_expansion_compose)
show "(λw. f (z + w) - f z) has_laurent_expansion fps_to_fls F"
using F by (rule has_laurent_expansion_fps)
show "fps_nth F 0 = 0"
using has_fps_expansion_imp_0_eq_fps_nth_0[OF F] by simp
qed fact+
next
case True
have "(λw. g (f z)) has_laurent_expansion fls_const (g (f z))"
by auto
also have "?this ⟷ (λw. ((λw. g (f z + w)) ∘ (λw. f (z + w) - f z)) w)
has_laurent_expansion fls_const (g (f z))"
proof (rule has_laurent_expansion_cong, goal_cases)
case 1
from F and True have "eventually (λw. f (z + w) - f z = 0) (nhds 0)"
by (simp add: has_fps_expansion_0_iff)
hence "eventually (λw. f (z + w) - f z = 0) (at 0)"
by (simp add: eventually_nhds_conv_at)
thus ?case
by eventually_elim auto
qed auto
finally show ?thesis
by blast
qed
thus "∃H. (λw. g (f (z + w))) has_laurent_expansion H"
by (simp add: o_def)
qed
lemma constant_on_imp_meromorphic_on:
assumes "f constant_on A" "open A"
shows "f meromorphic_on A"
using assms analytic_on_imp_meromorphic_on
constant_on_imp_analytic_on
by blast
subsection ‹Nice meromorphicity›
text ‹
This is probably very non-standard, but we call a function ``nicely meromorphic'' if it is
meromorphic and has no removable singularities. That means that the only singularities are
poles. We furthermore require that the function return 0 at any pole, for convenience.
›
definition nicely_meromorphic_on :: "(complex ⇒ complex) ⇒ complex set ⇒ bool"
(infixl ‹(nicely'_meromorphic'_on)› 50)
where "f nicely_meromorphic_on A ⟷ f meromorphic_on A
∧ (∀z∈A. (is_pole f z ∧ f z=0) ∨ f ─z→ f z)"
lemma nicely_meromorphic_on_subset:
"f nicely_meromorphic_on A ⟹ B ⊆ A ⟹ f nicely_meromorphic_on B"
using meromorphic_on_subset unfolding nicely_meromorphic_on_def by blast
lemma constant_on_imp_nicely_meromorphic_on:
assumes "f constant_on A" "open A"
shows "f nicely_meromorphic_on A"
by (meson analytic_at_imp_isCont assms
constant_on_imp_holomorphic_on
constant_on_imp_meromorphic_on
holomorphic_on_imp_analytic_at isCont_def
nicely_meromorphic_on_def)
lemma nicely_meromorphic_on_imp_analytic_at:
assumes "f nicely_meromorphic_on A" "z ∈ A" "¬is_pole f z"
shows "f analytic_on {z}"
proof (rule meromorphic_at_isCont_imp_analytic)
show "f meromorphic_on {z}"
by (rule meromorphic_on_subset[of _ A]) (use assms in ‹auto simp: nicely_meromorphic_on_def›)
next
from assms have "f ─z→ f z"
by (auto simp: nicely_meromorphic_on_def)
thus "isCont f z"
by (auto simp: isCont_def)
qed
lemma remove_sings_meromorphic [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "remove_sings f meromorphic_on A"
unfolding meromorphic_on_def
proof safe
fix z assume z: "z ∈ A"
show "∃F. (λw. remove_sings f (z + w)) has_laurent_expansion F"
using assms meromorphic_on_isolated_singularity meromorphic_on_not_essential
not_essential_has_laurent_expansion z meromorphic_on_subset by blast
qed
lemma remove_sings_nicely_meromorphic:
assumes "f meromorphic_on A"
shows "remove_sings f nicely_meromorphic_on A"
proof -
have "remove_sings f meromorphic_on A"
by (simp add: assms remove_sings_meromorphic)
moreover have "is_pole (remove_sings f) z
∧ remove_sings f z = 0 ∨
remove_sings f ─z→ remove_sings f z"
if "z∈A" for z
proof (cases "∃c. f ─z→ c")
case True
then have "remove_sings f ─z→ remove_sings f z"
by (metis remove_sings_eqI tendsto_remove_sings_iff
assms meromorphic_onE that)
then show ?thesis by simp
next
case False
then have "is_pole (remove_sings f) z
∧ remove_sings f z = 0"
by (meson is_pole_remove_sings_iff remove_sings_def
remove_sings_eq_0_iff assms meromorphic_onE that)
then show ?thesis by simp
qed
ultimately show ?thesis
unfolding nicely_meromorphic_on_def by simp
qed
text ‹
A nicely meromorphic function that frequently takes the same value in the neighbourhood of some
point is constant.
›
lemma frequently_eq_meromorphic_imp_constant:
assumes "frequently (λz. f z = c) (at z)"
assumes "f nicely_meromorphic_on A" "open A" "connected A" "z ∈ A"
shows "⋀w. w ∈ A ⟹ f w = c"
proof -
from assms(2) have mero: "f meromorphic_on A"
by (auto simp: nicely_meromorphic_on_def)
have sparse: "{z. is_pole f z} sparse_in A"
using assms(2) mero
by (meson assms(3) meromorphic_on_isolated_singularity meromorphic_on_meromorphic_at not_islimpt_poles sparse_in_open)
have eq: "f w = c" if w: "w ∈ A" "¬is_pole f w" for w
proof -
have "f w - c = 0"
proof (rule analytic_continuation[of "λw. f w - c"])
show "(λw. f w - c) holomorphic_on {z∈A. ¬is_pole f z}" using assms(2)
by (intro holomorphic_intros)
(metis (mono_tags, lifting) analytic_imp_holomorphic analytic_on_analytic_at
mem_Collect_eq nicely_meromorphic_on_imp_analytic_at)
next
from sparse and assms(3) have "open (A - {z. is_pole f z})"
by (simp add: open_diff_sparse_pts)
also have "A - {z. is_pole f z} = {z∈A. ¬is_pole f z}"
by blast
finally show "open …" .
next
from sparse have "connected (A - {z. is_pole f z})"
using assms(3,4) by (intro sparse_imp_connected) auto
also have "A - {z. is_pole f z} = {z∈A. ¬is_pole f z}"
by blast
finally show "connected …" .
next
have "eventually (λw. w ∈ A) (at z)"
using assms by (intro eventually_at_in_open') auto
moreover have "eventually (λw. ¬is_pole f w) (at z)" using mero
by (metis assms(5) eventually_not_pole meromorphic_onE)
ultimately have ev: "eventually (λw. w ∈ A ∧ ¬is_pole f w) (at z)"
by eventually_elim auto
show "z islimpt {z∈A. ¬is_pole f z ∧ f z = c}"
using frequently_eventually_frequently[OF assms(1) ev]
unfolding islimpt_conv_frequently_at by (rule frequently_elim1) auto
next
from assms(1) have "¬is_pole f z"
by (simp add: frequently_const_imp_not_is_pole)
with ‹z ∈ A› show "z ∈ {z ∈ A. ¬ is_pole f z}"
by auto
qed (use w in auto)
thus "f w = c"
by simp
qed
have not_pole: "¬is_pole f w" if w: "w ∈ A" for w
proof -
have "eventually (λw. ¬is_pole f w) (at w)"
using mero by (metis eventually_not_pole meromorphic_onE that)
moreover have "eventually (λw. w ∈ A) (at w)"
using w ‹open A› by (intro eventually_at_in_open')
ultimately have "eventually (λw. f w = c) (at w)"
by eventually_elim (auto simp: eq)
hence "is_pole f w ⟷ is_pole (λ_. c) w"
by (intro is_pole_cong refl)
thus ?thesis
by simp
qed
show "f w = c" if w: "w ∈ A" for w
using eq[OF w not_pole[OF w]] .
qed
subsection ‹Closure properties and proofs for individual functions›
lemma meromorphic_on_const [intro, meromorphic_intros]: "(λ_. c) meromorphic_on A"
by (rule analytic_on_imp_meromorphic_on) auto
lemma meromorphic_on_id [intro, meromorphic_intros]: "(λw. w) meromorphic_on A"
by (auto simp: meromorphic_on_def intro!: exI laurent_expansion_intros)
lemma meromorphic_on_id' [intro, meromorphic_intros]: "id meromorphic_on A"
by (auto simp: meromorphic_on_def intro!: exI laurent_expansion_intros)
lemma meromorphic_on_add [meromorphic_intros]:
assumes "f meromorphic_on A" "g meromorphic_on A"
shows "(λw. f w + g w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_uminus [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "(λw. -f w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_diff [meromorphic_intros]:
assumes "f meromorphic_on A" "g meromorphic_on A"
shows "(λw. f w - g w) meromorphic_on A"
using meromorphic_on_add[OF assms(1) meromorphic_on_uminus[OF assms(2)]] by simp
lemma meromorphic_on_mult [meromorphic_intros]:
assumes "f meromorphic_on A" "g meromorphic_on A"
shows "(λw. f w * g w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_power [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "(λw. f w ^ n) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_powi [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "(λw. f w powi n) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_scaleR [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "(λw. scaleR x (f w)) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_inverse [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "(λw. inverse (f w)) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_divide [meromorphic_intros]:
assumes "f meromorphic_on A" "g meromorphic_on A"
shows "(λw. f w / g w) meromorphic_on A"
using meromorphic_on_mult[OF assms(1) meromorphic_on_inverse[OF assms(2)]]
by (simp add: field_simps)
lemma meromorphic_on_sum [meromorphic_intros]:
assumes "⋀i. i ∈ I ⟹ f i meromorphic_on A"
shows "(λw. ∑i∈I. f i w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_sum_list [meromorphic_intros]:
assumes "⋀i. i ∈ set fs ⟹ f i meromorphic_on A"
shows "(λw. ∑i←fs. f i w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_sum_mset [meromorphic_intros]:
assumes "⋀i. i ∈# I ⟹ f i meromorphic_on A"
shows "(λw. ∑i∈#I. f i w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_prod [meromorphic_intros]:
assumes "⋀i. i ∈ I ⟹ f i meromorphic_on A"
shows "(λw. ∏i∈I. f i w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_prod_list [meromorphic_intros]:
assumes "⋀i. i ∈ set fs ⟹ f i meromorphic_on A"
shows "(λw. ∏i←fs. f i w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_prod_mset [meromorphic_intros]:
assumes "⋀i. i ∈# I ⟹ f i meromorphic_on A"
shows "(λw. ∏i∈#I. f i w) meromorphic_on A"
unfolding meromorphic_on_def
by (rule laurent_expansion_intros exI ballI
assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
lemma meromorphic_on_If [meromorphic_intros]:
assumes "f meromorphic_on A" "g meromorphic_on B"
assumes "⋀z. z ∈ A ⟹ z ∈ B ⟹ f z = g z" "open A" "open B" "C ⊆ A ∪ B"
shows "(λz. if z ∈ A then f z else g z) meromorphic_on C"
proof (rule meromorphic_on_subset)
show "(λz. if z ∈ A then f z else g z) meromorphic_on (A ∪ B)"
proof (rule meromorphic_on_Un)
have "(λz. if z ∈ A then f z else g z) meromorphic_on A ⟷ f meromorphic_on A"
proof (rule meromorphic_on_cong)
fix z assume "z ∈ A"
hence "eventually (λz. z ∈ A) (at z)"
using ‹open A› by (intro eventually_at_in_open') auto
thus "∀⇩F w in at z. (if w ∈ A then f w else g w) = f w"
by eventually_elim auto
qed auto
with assms(1) show "(λz. if z ∈ A then f z else g z) meromorphic_on A"
by blast
next
have "(λz. if z ∈ A then f z else g z) meromorphic_on B ⟷ g meromorphic_on B"
proof (rule meromorphic_on_cong)
fix z assume "z ∈ B"
hence "eventually (λz. z ∈ B) (at z)"
using ‹open B› by (intro eventually_at_in_open') auto
thus "∀⇩F w in at z. (if w ∈ A then f w else g w) = g w"
by eventually_elim (use assms(3) in auto)
qed auto
with assms(2) show "(λz. if z ∈ A then f z else g z) meromorphic_on B"
by blast
qed
qed fact
lemma meromorphic_on_deriv [meromorphic_intros]:
"f meromorphic_on A ⟹ deriv f meromorphic_on A"
by (metis meromorphic_on_def isolated_singularity_at_deriv meromorphic_on_isolated_singularity
meromorphic_on_meromorphic_at meromorphic_on_not_essential not_essential_deriv
not_essential_has_laurent_expansion)
lemma meromorphic_on_higher_deriv [meromorphic_intros]:
"f meromorphic_on A ⟹ (deriv ^^ n) f meromorphic_on A"
by (induction n) (auto intro!: meromorphic_intros)
lemma analytic_on_eval_fps [analytic_intros]:
assumes "f analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) < fps_conv_radius F"
shows "(λw. eval_fps F (f w)) analytic_on A"
by (rule analytic_on_compose[OF assms(1) analytic_on_eval_fps, unfolded o_def])
(use assms(2) in auto)
lemma meromorphic_on_eval_fps [meromorphic_intros]:
assumes "f analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) < fps_conv_radius F"
shows "(λw. eval_fps F (f w)) meromorphic_on A"
by (rule analytic_on_imp_meromorphic_on analytic_intros analytic_on_eval_fps assms)+
lemma meromorphic_on_eval_fls [meromorphic_intros]:
assumes "f analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) < fls_conv_radius F"
shows "(λw. eval_fls F (f w)) meromorphic_on A"
proof (cases "fls_conv_radius F > 0")
case False
with assms(2) have "A = {}"
by (metis all_not_in_conv ereal_less(2) norm_eq_zero order.strict_trans
zero_ereal_def zero_less_norm_iff)
thus ?thesis
by auto
next
case True
have F: "eval_fls F has_laurent_expansion F"
using True by (rule eval_fls_has_laurent_expansion)
show ?thesis
proof (rule meromorphic_on_compose[OF _ assms(1)])
show "eval_fls F meromorphic_on eball 0 (fls_conv_radius F)"
proof (rule meromorphic_onI_open)
show "eval_fls F analytic_on eball 0 (fls_conv_radius F) - {0}"
by (rule analytic_on_eval_fls) auto
show "not_essential (eval_fls F) z" if "z ∈ {0}" for z
using that F has_laurent_expansion_not_essential_0 by blast
qed (auto simp: islimpt_finite)
qed (use assms(2) in auto)
qed
lemma meromorphic_on_imp_analytic_cosparse:
assumes "f meromorphic_on A"
shows "eventually (λz. f analytic_on {z}) (cosparse A)"
unfolding eventually_cosparse using assms meromorphic_on_imp_sparse_singularities by auto
lemma meromorphic_on_imp_not_pole_cosparse:
assumes "f meromorphic_on A"
shows "eventually (λz. ¬is_pole f z) (cosparse A)"
proof -
have "eventually (λz. f analytic_on {z}) (cosparse A)"
by (rule meromorphic_on_imp_analytic_cosparse) fact
thus ?thesis
by eventually_elim (blast dest: analytic_at_imp_no_pole)
qed
lemma eventually_remove_sings_eq:
assumes "f meromorphic_on A"
shows "eventually (λz. remove_sings f z = f z) (cosparse A)"
proof -
have "eventually (λz. f analytic_on {z}) (cosparse A)"
using assms by (rule meromorphic_on_imp_analytic_cosparse)
thus ?thesis
by eventually_elim auto
qed
text ‹
A meromorphic function on a connected domain takes any given value either almost everywhere
or almost nowhere.
›
lemma meromorphic_imp_constant_or_avoid:
assumes mero: "f meromorphic_on A" and A: "open A" "connected A"
shows "eventually (λz. f z = c) (cosparse A) ∨ eventually (λz. f z ≠ c) (cosparse A)"
proof -
have "eventually (λz. f z = c) (cosparse A)" if freq: "frequently (λz. f z = c) (cosparse A)"
proof -
let ?f = "remove_sings f"
have ev: "eventually (λz. ?f z = f z) (cosparse A)"
by (rule eventually_remove_sings_eq) fact
have "frequently (λz. ?f z = c) (cosparse A)"
using frequently_eventually_frequently[OF freq ev] by (rule frequently_elim1) auto
then obtain z0 where z0: "z0 ∈ A" "frequently (λz. ?f z = c) (at z0)"
using A by (auto simp: eventually_cosparse_open_eq frequently_def)
have mero': "?f nicely_meromorphic_on A"
using mero remove_sings_nicely_meromorphic by blast
have eq: "?f w = c" if w: "w ∈ A" for w
using frequently_eq_meromorphic_imp_constant[OF z0(2) mero'] A z0(1) w by blast
have "eventually (λz. z ∈ A) (cosparse A)"
by (rule eventually_in_cosparse) (use A in auto)
thus "eventually (λz. f z = c) (cosparse A)"
using ev by eventually_elim (use eq in auto)
qed
thus ?thesis
by (auto simp: frequently_def)
qed
lemma nicely_meromorphic_imp_constant_or_avoid:
assumes "f nicely_meromorphic_on A" "open A" "connected A"
shows "(∀x∈A. f x = c) ∨ (∀⇩≈x∈A. f x ≠ c)"
proof -
have "(∀⇩≈x∈A. f x = c) ∨ (∀⇩≈x∈A. f x ≠ c)"
by (intro meromorphic_imp_constant_or_avoid)
(use assms in ‹auto simp: nicely_meromorphic_on_def›)
thus ?thesis
proof
assume ev: "∀⇩≈x∈A. f x = c"
have "∀x∈A. f x = c "
proof
fix x assume x: "x ∈ A"
have "not_essential f x"
using assms x unfolding nicely_meromorphic_on_def by blast
moreover have "is_pole f x ⟷ is_pole (λ_. c) x"
by (intro is_pole_cong) (use ev x in ‹auto simp: eventually_cosparse_open_eq assms›)
hence "¬is_pole f x"
by auto
ultimately have "f analytic_on {x}"
using assms(1) nicely_meromorphic_on_imp_analytic_at x by blast
hence "f ─x→ f x"
by (intro isContD analytic_at_imp_isCont)
also have "?this ⟷ (λ_. c) ─x→ f x"
by (intro tendsto_cong) (use ev x in ‹auto simp: eventually_cosparse_open_eq assms›)
finally have "(λ_. c) ─x→ f x" .
moreover have "(λ_. c) ─x→ c"
by simp
ultimately show "f x = c"
using LIM_unique by blast
qed
thus ?thesis
by blast
qed blast
qed
lemma nicely_meromorphic_onE:
assumes "f nicely_meromorphic_on A"
obtains pts where "pts ⊆ A" "pts sparse_in A"
"f analytic_on A - pts"
"⋀z. z ∈ pts ⟹ is_pole f z ∧ f z=0"
proof -
define pts where "pts = {z ∈ A. ¬ f analytic_on {z}}"
have "pts ⊆ A" "pts sparse_in A"
using assms unfolding pts_def nicely_meromorphic_on_def
by (auto intro:meromorphic_on_imp_sparse_singularities')
moreover have "f analytic_on A - pts" unfolding pts_def
by (subst analytic_on_analytic_at) auto
moreover have "⋀z. z ∈ pts ⟹ is_pole f z ∧ f z=0"
by (metis (no_types, lifting) remove_sings_eqI
remove_sings_eq_0_iff assms is_pole_imp_not_essential
mem_Collect_eq nicely_meromorphic_on_def
nicely_meromorphic_on_imp_analytic_at pts_def)
ultimately show ?thesis using that by auto
qed
lemma nicely_meromorphic_onI_open:
assumes "open A" and
analytic:"f analytic_on A - pts" and
pole:"⋀x. x∈pts ⟹ is_pole f x ∧ f x = 0" and
isolated:"⋀x. x∈A ⟹ isolated_singularity_at f x"
shows "f nicely_meromorphic_on A"
proof -
have "f meromorphic_on A"
proof (rule meromorphic_onI_open)
show "⋀z. z ∈ pts ⟹ not_essential f z"
using pole unfolding not_essential_def by auto
show "⋀z. z ∈ A ⟹ ¬ z islimpt pts ∩ A"
by (metis assms(3) assms(4) inf_commute inf_le2
islimpt_subset mem_Collect_eq not_islimpt_poles subsetI)
qed fact+
moreover have "(∀z∈A. (is_pole f z ∧ f z=0) ∨ f ─z→ f z)"
by (meson DiffI analytic analytic_at_imp_isCont
analytic_on_analytic_at assms(3) isContD)
ultimately show ?thesis unfolding nicely_meromorphic_on_def
by auto
qed
lemma nicely_meromorphic_without_singularities:
assumes "f nicely_meromorphic_on A" "∀z∈A. ¬ is_pole f z"
shows "f analytic_on A"
by (meson analytic_on_analytic_at assms
nicely_meromorphic_on_imp_analytic_at)
lemma meromorphic_on_cong':
assumes "eventually (λz. f z = g z) (cosparse A)" "A = B"
shows "f meromorphic_on A ⟷ g meromorphic_on B"
unfolding assms(2)[symmetric]
by (rule meromorphic_on_cong eventually_cosparse_imp_eventually_at assms)+ auto
subsection ‹Meromorphic functions and zorder›
lemma zorder_power_int:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
shows "zorder (λz. f z powi n) z = n * zorder f z"
proof -
from assms(1) obtain L where L: "(λw. f (z + w)) has_laurent_expansion L"
by (auto simp: meromorphic_on_def)
from assms(2) and L have [simp]: "L ≠ 0"
by (metis assms(1) has_laurent_expansion_eventually_nonzero_iff meromorphic_at_iff
not_essential_frequently_0_imp_eventually_0 not_eventually not_frequently)
from L have L': "(λw. f (z + w) powi n) has_laurent_expansion L powi n"
by (intro laurent_expansion_intros)
have "zorder f z = fls_subdegree L"
using L assms(2) ‹L ≠ 0› by (simp add: has_laurent_expansion_zorder)
moreover have "zorder (λz. f z powi n) z = fls_subdegree (L powi n)"
using L' assms(2) ‹L ≠ 0› by (simp add: has_laurent_expansion_zorder)
moreover have "fls_subdegree (L powi n) = n * fls_subdegree L"
by simp
ultimately show ?thesis
by simp
qed
lemma zorder_power:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
shows "zorder (λz. f z ^ n) z = n * zorder f z"
using zorder_power_int[OF assms, of "int n"] by simp
lemma zorder_add1:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
assumes "zorder f z < zorder g z"
shows "zorder (λz. f z + g z) z = zorder f z"
proof -
from assms(1) obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
by (auto simp: meromorphic_on_def)
from assms(3) obtain G where G: "(λw. g (z + w)) has_laurent_expansion G"
by (auto simp: meromorphic_on_def)
have [simp]: "F ≠ 0" "G ≠ 0"
by (metis assms has_laurent_expansion_eventually_nonzero_iff meromorphic_at_iff
not_essential_frequently_0_imp_eventually_0 not_eventually not_frequently F G)+
have *: "zorder f z = fls_subdegree F" "zorder g z = fls_subdegree G"
using F G assms by (simp_all add: has_laurent_expansion_zorder)
from assms * have "F ≠ -G"
by auto
hence [simp]: "F + G ≠ 0"
by (simp add: add_eq_0_iff2)
moreover have "zorder (λz. f z + g z) z = fls_subdegree (F + G)"
using has_laurent_expansion_zorder[OF has_laurent_expansion_add[OF F G]] ‹F ≠ -G› by simp
moreover have "fls_subdegree (F + G) = fls_subdegree F"
using assms by (simp add: * fls_subdegree_add_eq1)
ultimately show ?thesis
by (simp add: *)
qed
lemma zorder_add2:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
assumes "zorder f z > zorder g z"
shows "zorder (λz. f z + g z) z = zorder g z"
using zorder_add1[OF assms(3,4) assms(1,2)] assms(5-) by (simp add: add.commute)
lemma zorder_add_ge:
fixes f g :: "complex ⇒ complex"
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
assumes "frequently (λz. f z + g z ≠ 0) (at z)" "zorder f z ≥ c" "zorder g z ≥ c"
shows "zorder (λz. f z + g z) z ≥ c"
proof -
from assms(1) obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
by (auto simp: meromorphic_on_def)
from assms(3) obtain G where G: "(λw. g (z + w)) has_laurent_expansion G"
by (auto simp: meromorphic_on_def)
have [simp]: "F ≠ 0" "G ≠ 0"
using assms F G has_laurent_expansion_frequently_nonzero_iff by blast+
have FG: "(λw. f (z + w) + g (z + w)) has_laurent_expansion F + G"
by (intro laurent_expansion_intros F G)
have [simp]: "F + G ≠ 0"
using assms(5) has_laurent_expansion_frequently_nonzero_iff[OF FG] by blast
have *: "zorder f z = fls_subdegree F" "zorder g z = fls_subdegree G"
"zorder (λz. f z + g z) z = fls_subdegree (F + G)"
using F G FG has_laurent_expansion_zorder by simp_all
moreover have "zorder (λz. f z + g z) z = fls_subdegree (F + G)"
using has_laurent_expansion_zorder[OF has_laurent_expansion_add[OF F G]] by simp
moreover have "fls_subdegree (F + G) ≥ min (fls_subdegree F) (fls_subdegree G)"
by (intro fls_plus_subdegree) simp
ultimately show ?thesis
using assms(6,7) unfolding * by linarith
qed
lemma zorder_diff_ge:
fixes f g :: "complex ⇒ complex"
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
assumes "frequently (λz. f z ≠ g z) (at z)" "zorder f z ≥ c" "zorder g z ≥ c"
shows "zorder (λz. f z - g z) z ≥ c"
proof -
have "(λz. - g z) meromorphic_on {z}"
by (auto intro: meromorphic_intros assms)
thus ?thesis
using zorder_add_ge[of f z "λz. -g z" c] assms by simp
qed
lemma zorder_diff1:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
assumes "zorder f z < zorder g z"
shows "zorder (λz. f z - g z) z = zorder f z"
proof -
have "zorder (λz. f z + (-g z)) z = zorder f z"
by (intro zorder_add1 meromorphic_intros assms) (use assms in auto)
thus ?thesis
by simp
qed
lemma zorder_diff2:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
assumes "zorder f z > zorder g z"
shows "zorder (λz. f z - g z) z = zorder g z"
proof -
have "zorder (λz. f z + (-g z)) z = zorder (λz. -g z) z"
by (intro zorder_add2 meromorphic_intros assms) (use assms in auto)
thus ?thesis
by simp
qed
lemma zorder_mult:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
shows "zorder (λz. f z * g z) z = zorder f z + zorder g z"
proof -
from assms(1) obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
by (auto simp: meromorphic_on_def)
from assms(3) obtain G where G: "(λw. g (z + w)) has_laurent_expansion G"
by (auto simp: meromorphic_on_def)
have [simp]: "F ≠ 0" "G ≠ 0"
by (metis assms has_laurent_expansion_eventually_nonzero_iff meromorphic_at_iff
not_essential_frequently_0_imp_eventually_0 not_eventually not_frequently F G)+
have *: "zorder f z = fls_subdegree F" "zorder g z = fls_subdegree G"
using F G assms by (simp_all add: has_laurent_expansion_zorder)
moreover have "zorder (λz. f z * g z) z = fls_subdegree (F * G)"
using has_laurent_expansion_zorder[OF has_laurent_expansion_mult[OF F G]] by simp
moreover have "fls_subdegree (F * G) = fls_subdegree F + fls_subdegree G"
using assms by simp
ultimately show ?thesis
by (simp add: *)
qed
lemma zorder_divide:
assumes "f meromorphic_on {z}" "frequently (λz. f z ≠ 0) (at z)"
assumes "g meromorphic_on {z}" "frequently (λz. g z ≠ 0) (at z)"
shows "zorder (λz. f z / g z) z = zorder f z - zorder g z"
proof -
from assms(1) obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
by (auto simp: meromorphic_on_def)
from assms(3) obtain G where G: "(λw. g (z + w)) has_laurent_expansion G"
by (auto simp: meromorphic_on_def)
have [simp]: "F ≠ 0" "G ≠ 0"
by (metis assms has_laurent_expansion_eventually_nonzero_iff meromorphic_at_iff
not_essential_frequently_0_imp_eventually_0 not_eventually not_frequently F G)+
have *: "zorder f z = fls_subdegree F" "zorder g z = fls_subdegree G"
using F G assms by (simp_all add: has_laurent_expansion_zorder)
moreover have "zorder (λz. f z / g z) z = fls_subdegree (F / G)"
using has_laurent_expansion_zorder[OF has_laurent_expansion_divide[OF F G]] by simp
moreover have "fls_subdegree (F / G) = fls_subdegree F - fls_subdegree G"
using assms by (simp add: fls_divide_subdegree)
ultimately show ?thesis
by (simp add: *)
qed
lemma constant_on_extend_nicely_meromorphic_on:
assumes "f nicely_meromorphic_on B" "f constant_on A"
assumes "open A" "open B" "connected B" "A ≠ {}" "A ⊆ B"
shows "f constant_on B"
proof -
from assms obtain c where c: "⋀z. z ∈ A ⟹ f z = c"
by (auto simp: constant_on_def)
have "eventually (λz. z ∈ A) (cosparse A)"
by (intro eventually_in_cosparse assms order.refl)
hence "eventually (λz. f z = c) (cosparse A)"
by eventually_elim (use c in auto)
hence freq: "frequently (λz. f z = c) (cosparse A)"
by (intro eventually_frequently) (use assms in auto)
then obtain z0 where z0: "z0 ∈ A" "frequently (λz. f z = c) (at z0)"
using assms by (auto simp: frequently_def eventually_cosparse_open_eq)
have "f z = c" if "z ∈ B" for z
proof (rule frequently_eq_meromorphic_imp_constant[OF _ assms(1)])
show "z0 ∈ B" "frequently (λz. f z = c) (at z0)"
using z0 assms by auto
qed (use assms that in auto)
thus "f constant_on B"
by (auto simp: constant_on_def)
qed
end