Orders of Meromorphic Functions

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

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_nat_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_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.

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_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) : 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_unequal_order.

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 = 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.

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.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) [CompleteSpace E] : {u : ↑U | ⋯.order = 0 ∨ ⋯.order = ⊤} ∈ Filter.codiscrete ↑U

If the target is a complete space, then the set where a mermorphic function has zero or infinite order is discrete within its domain of meromorphicity.