Orders of Meromorphic Functions

This file defines the order of a meromorphic function f at a point z₀, as an element of ℤ ∪ {∞}.

We characterize the order being < 0, or = 0, or > 0, as the convergence of the function to infinity, resp. a nonzero constant, resp. zero.

TODO: Uniformize API between analytic and meromorphic functions

Order at a Point: Definition and Characterization

noncomputable def MeromorphicAt.order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : WithTop ℤ

The order of a meromorphic function f at z₀, as an element of ℤ ∪ {∞}.

The order is defined to be ∞ if f is identically 0 on a neighbourhood of z₀, and otherwise the unique n such that f can locally be written as f z = (z - z₀) ^ n • g z, where g is analytic and does not vanish at z₀. See MeromorphicAt.order_eq_top_iff and MeromorphicAt.order_eq_int_iff for these equivalences.

Equations

• hf.order = ENat.map (fun (x : ℕ) => ↑x) ⋯.order - ↑(Exists.choose hf)

theorem MeromorphicAt.order_eq_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : hf.order = ⊤ ↔ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = 0

The order of a meromorphic function f at a z₀ is infinity iff f vanishes locally around z₀.

theorem MeromorphicAt.order_eq_int_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {n : ℤ} (hf : MeromorphicAt f x) : hf.order = ↑n ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = (z - x) ^ n • g z

The order of a meromorphic function f at z₀ equals an integer n iff f can locally be written as f z = (z - z₀) ^ n • g z, where g is analytic and does not vanish at z₀.

theorem MeromorphicAt.order_ne_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : MeromorphicAt f z₀) : hf.order ≠ ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : 𝕜) => (z - z₀) ^ hf.order.untop₀ • g z

The order of a meromorphic function f at z₀ is finite iff f can locally be written as f z = (z - z₀) ^ order • g z, where g is analytic and does not vanish at z₀.

theorem MeromorphicAt.order_ne_top_iff_eventually_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} (hf : MeromorphicAt f x) : hf.order ≠ ⊤ ↔ ∀ᶠ (x : 𝕜) in nhdsWithin x {x}ᶜ, f x ≠ 0

The order of a meromorphic function f at z₀ is finite iff f does not have any zeros in a sufficiently small neighborhood of z₀.

theorem MeromorphicAt.tendsto_cobounded_of_order_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (ho : hf.order < 0) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (Bornology.cobounded E)

If the order of a meromorphic function is negative, then this function converges to infinity at this point. See also the iff version tendsto_cobounded_iff_order_neg.

theorem MeromorphicAt.tendsto_ne_zero_of_order_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (ho : hf.order = 0) : ∃ (c : E), c ≠ 0 ∧ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)

If the order of a meromorphic function is zero, then this function converges to a nonzero limit at this point. See also the iff version tendsto_ne_zero_iff_order_eq_zero.

theorem MeromorphicAt.tendsto_zero_of_order_pos {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (ho : 0 < hf.order) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds 0)

If the order of a meromorphic function is positive, then this function converges to zero at this point. See also the iff version tendsto_zero_iff_order_pos.

theorem MeromorphicAt.tendsto_nhds_of_order_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (ho : 0 ≤ hf.order) : ∃ (c : E), Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)

If the order of a meromorphic function is nonnegative, then this function converges at this point. See also the iff version tendsto_nhds_iff_order_nonneg.

theorem MeromorphicAt.tendsto_cobounded_iff_order_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (Bornology.cobounded E) ↔ hf.order < 0

A meromorphic function converges to infinity iff its order is negative.

theorem MeromorphicAt.tendsto_nhds_iff_order_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : (∃ (c : E), Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)) ↔ 0 ≤ hf.order

A meromorphic function converges to a limit iff its order is nonnegative.

theorem MeromorphicAt.tendsto_ne_zero_iff_order_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : (∃ (c : E), c ≠ 0 ∧ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)) ↔ hf.order = 0

A meromorphic function converges to a nonzero limit iff its order is zero.

theorem MeromorphicAt.tendsto_zero_iff_order_pos {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds 0) ↔ 0 < hf.order

A meromorphic function converges to zero iff its order is positive.

theorem MeromorphicAt.order_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₁₂ : f₁ =ᶠ[nhdsWithin x {x}ᶜ] f₂) : hf₁.order = ⋯.order

Meromorphic functions that agree in a punctured neighborhood of z₀ have the same order at z₀.

theorem AnalyticAt.meromorphicAt_order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) : ⋯.order = ENat.map Nat.cast hf.order

Compatibility of notions of order for analytic and meromorphic functions.

theorem AnalyticAt.meromorphicAt_order_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) : 0 ≤ ⋯.order

When seen as meromorphic functions, analytic functions have nonnegative order.

theorem MeromorphicAt.analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) (h' : ContinuousAt f x) : AnalyticAt 𝕜 f x

If a function is both meromorphic and continuous at a point, then it is analytic there.

Order at a Point: Behaviour under Ring Operations

We establish additivity of the order under multiplication and taking powers.

theorem MeromorphicAt.order_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → 𝕜} {g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : ⋯.order = hf.order + hg.order

The order is additive when multiplying scalar-valued and vector-valued meromorphic functions.

theorem MeromorphicAt.order_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : ⋯.order = hf.order + hg.order

The order is additive when multiplying meromorphic functions.

theorem MeromorphicAt.order_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) {n : ℕ} : ⋯.order = ↑n * hf.order

The order multiplies by n when taking a meromorphic function to its nth power.

theorem MeromorphicAt.order_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) {n : ℤ} : ⋯.order = ↑n * hf.order

The order multiplies by n when taking a meromorphic function to its nth power.

theorem MeromorphicAt.order_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) : ⋯.order = -hf.order

The order of the inverse is the negative of the order.

theorem MeromorphicAt.order_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) : min hf₁.order hf₂.order ≤ ⋯.order

The order of a sum is at least the minimum of the orders of the summands.

theorem MeromorphicAt.order_add_of_order_lt_order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) (h : hf₁.order < hf₂.order) : ⋯.order = hf₁.order

Helper lemma for MeromorphicAt.order_add_of_order_ne.

theorem MeromorphicAt.order_add_of_order_ne {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) (h : hf₁.order ≠ hf₂.order) : ⋯.order = min hf₁.order hf₂.order

If two meromorphic functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.

@[deprecated MeromorphicAt.order_add_of_order_ne (since := "2025-04-27")]

theorem MeromorphicAt.order_add_of_unequal_order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) (h : hf₁.order ≠ hf₂.order) : ⋯.order = min hf₁.order hf₂.order

Alias of MeromorphicAt.order_add_of_order_ne.

---

If two meromorphic functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.

Level Sets of the Order Function

theorem MeromorphicOn.isClopen_setOf_order_eq_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) : IsClopen {u : ↑U | ⋯.order = ⊤}

The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.

theorem MeromorphicOn.exists_order_ne_top_iff_forall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) (hU : IsConnected U) : (∃ (u : ↑U), ⋯.order ≠ ⊤) ↔ ∀ (u : ↑U), ⋯.order ≠ ⊤

On a connected set, there exists a point where a meromorphic function f has finite order iff f has finite order at every point.

theorem MeromorphicOn.order_ne_top_of_isPreconnected {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} (hf : MeromorphicOn f U) {y : 𝕜} (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : ⋯.order ≠ ⊤) : ⋯.order ≠ ⊤

On a preconnected set, a meromorphic function has finite order at one point if it has finite order at another point.

theorem MeromorphicOn.eventually_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicOn f U) (hx : x ∈ U) : ∀ᶠ (y : 𝕜) in nhdsWithin x (U \ {x}), AnalyticAt 𝕜 f y

If a function is meromorphic on a set U, then for each point in U, it is analytic at nearby points in U. When the target space is complete, this can be strengthened to analyticity at all nearby points, see MeromorphicAt.eventually_analyticAt.

theorem MeromorphicOn.eventually_analyticAt_or_mem_compl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicOn f U) (hx : x ∈ U) : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ

theorem MeromorphicOn.analyticAt_mem_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) : {x : 𝕜 | AnalyticAt 𝕜 f x} ∈ Filter.codiscreteWithin U

Meromorphic functions on U are analytic on U, outside of a discrete subset.

theorem MeromorphicOn.codiscrete_setOf_order_eq_zero_or_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) : {u : ↑U | ⋯.order = 0 ∨ ⋯.order = ⊤} ∈ Filter.codiscrete ↑U

The set where a meromorphic function has zero or infinite order is codiscrete within its domain of meromorphicity.