(* Authors: Manuel Eberl, University of Innsbruck Wenda Li, University of Edinburgh *) 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