Meromorphic Functions over the Real and Complex Numbers

This file gathers results on meromorphic functions specific to the real and complex numbers.

theorem Meromorphic.exists_meromorphicOrderAt_ne_top_iff_forall {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : Meromorphic f) : (∃ (u : 𝕜), meromorphicOrderAt f u ≠ ⊤) ↔ ∀ (u : 𝕜), meromorphicOrderAt f u ≠ ⊤

If f is meromorphic function on ℝ or ℂ, then there exists a point where a meromorphic function f has finite order iff f has finite order at every point.

theorem Meromorphic.exists_meromorphicOrderAt_eq_top_iff_forall {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : Meromorphic f) : (∃ (u : 𝕜), meromorphicOrderAt f u = ⊤) ↔ ∀ (u : 𝕜), meromorphicOrderAt f u = ⊤

If f is a meromorphic function on ℝ or ℂ, then f has infinite order at some point iff f has infinite order at every point. This is the counterpart of Meromorphic.exists_meromorphicOrderAt_ne_top_iff_forall for infinite order.

theorem Meromorphic.exists_meromorphicOrderAt_eq_top_iff_eventually_zero {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : Meromorphic f) : (∃ (u : 𝕜), meromorphicOrderAt f u = ⊤) ↔ f =ᶠ[Filter.codiscrete 𝕜] 0

A meromorphic function on ℝ or ℂ has infinite order at some point iff it vanishes outside a discrete set, i.e. iff it is eventually zero along the codiscrete filter.