Meromorphic order from limits and connected sets

A nonzero limit of (z - c) • f z at c detects an exact simple pole of f. An analytic function on a connected set that is nonzero somewhere has finite meromorphic order throughout the set.

On a nonempty closed disc closedBall c R over ℝ or ℂ (RCLike 𝕜), the boundary point c + R lies on sphere c R and closedBall c R is convex, hence preconnected. Consequently, if a meromorphic function on closedBall c R has finite meromorphic order at every point of sphere c R — in particular, if an analytic function on closedBall c R does not vanish on sphere c R — then MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected propagates finite meromorphic order to every point of closedBall c R.

Main results

• MeromorphicAt.meromorphicOrderAt_eq_neg_one_of_tendsto_sub_smul: a nonzero residue limit forces meromorphic order exactly -1.
• AnalyticOnNhd.meromorphicOrderAt_ne_top_of_exists_ne_zero: a nonzero value on a connected set rules out infinite order throughout the set.
• MeromorphicOn.meromorphicOrderAt_ne_top_of_forall_mem_sphere: finite meromorphic order on the bounding sphere propagates throughout the closed disc.
• AnalyticOnNhd.meromorphicOrderAt_ne_top_of_forall_mem_sphere_ne_zero: an analytic function on a closed disc that does not vanish on the bounding sphere has finite meromorphic order throughout the closed disc.

theorem AnalyticOnNhd.meromorphicOrderAt_ne_top_of_exists_ne_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsConnected U) (h0 : ∃ z ∈ U, f z ≠ 0) {z : 𝕜} (hz : z ∈ U) : meromorphicOrderAt f z ≠ ⊤

An analytic function on a connected set has finite meromorphic order everywhere on that set if it is nonzero at some point of the set.

theorem MeromorphicAt.meromorphicOrderAt_eq_neg_one_of_tendsto_sub_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} (hf : MeromorphicAt f c) {a : E} (ha : a ≠ 0) (hlim : Filter.Tendsto (fun (z : 𝕜) => (z - c) • f z) (nhdsWithin c {c}ᶜ) (nhds a)) : meromorphicOrderAt f c = ↑(-1)

A meromorphic function has an exact simple pole if multiplying by the displacement from that point gives a nonzero punctured limit.

theorem MeromorphicOn.meromorphicOrderAt_ne_top_of_forall_mem_sphere {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ} (hf : MeromorphicOn f (Metric.closedBall c R)) (hsphere : ∀ ζ ∈ Metric.sphere c R, meromorphicOrderAt f ζ ≠ ⊤) {z : 𝕜} (hz : z ∈ Metric.closedBall c R) : meromorphicOrderAt f z ≠ ⊤

If f is meromorphic on closedBall c R and has finite meromorphic order at every point of the bounding sphere sphere c R, then f has finite meromorphic order throughout closedBall c R.

theorem AnalyticOnNhd.meromorphicOrderAt_ne_top_of_forall_mem_sphere_ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ} (hf : AnalyticOnNhd 𝕜 f (Metric.closedBall c R)) (hsphere : ∀ ζ ∈ Metric.sphere c R, f ζ ≠ 0) {z : 𝕜} (hz : z ∈ Metric.closedBall c R) : meromorphicOrderAt f z ≠ ⊤

If f is analytic on closedBall c R and nonvanishing on the bounding sphere sphere c R, then f has finite meromorphic order throughout closedBall c R.