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 : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : 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 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.

Order at a Point: Behaviour under Ring Operations

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

TODO: Behaviour under Addition/Subtraction. API unification with analytic functions

theorem MeromorphicAt.order_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (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 𝕜] {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : ⋯.order = hf.order + hg.order

The order is additive when multiplying meromorphic functions.

Level Sets of the Order Function

TODO: investigate whether codiscrete_setOf_order_eq_zero_or_top really needs a completeness hypothesis.

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} {U : Set 𝕜} (hf : MeromorphicOn f U) {x 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.