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 #

source

noncomputable def meromorphicOrderAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (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.meromorphicOrderAt_eq_top_iff and MeromorphicAt.meromorphicOrderAt_eq_int_iff for these equivalences.

If the function is not meromorphic at x, we use the junk value 0.

Equations

meromorphicOrderAt f x = if hf : MeromorphicAt f x then ENat.map (fun (x : ℕ) => ↑x) (analyticOrderAt (fun (z : 𝕜) => (z - x) ^ Exists.choose hf • f z) x) - ↑(Exists.choose hf) else 0

Instances For

source

@[simp]

theorem meromorphicOrderAt_of_not_meromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : ¬MeromorphicAt f x) :

meromorphicOrderAt f x = 0

source

theorem meromorphicAt_of_meromorphicOrderAt_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : meromorphicOrderAt f x ≠ 0) :

MeromorphicAt f x

source

theorem meromorphicOrderAt_eq_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} :

meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (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₀.

source

theorem eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} :

Filter.EventuallyConst f (nhdsWithin x {x}ᶜ) ↔ ∃ (c : E), meromorphicOrderAt (fun (x : 𝕜) => f x - c) x = ⊤

source

theorem meromorphicOrderAt_eq_int_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {n : ℤ} (hf : MeromorphicAt f x) :

meromorphicOrderAt f x = ↑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₀.

source

theorem meromorphicOrderAt_ne_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : MeromorphicAt f z₀) :

meromorphicOrderAt f z₀ ≠ ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : 𝕜) => (z - z₀) ^ (meromorphicOrderAt f z₀).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₀.

source

theorem meromorphicOrderAt_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) :

meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ (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₀.

source

theorem tendsto_cobounded_of_meromorphicOrderAt_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (ho : meromorphicOrderAt f x < 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_meromorphicOrderAt_neg.

source

theorem tendsto_ne_zero_of_meromorphicOrderAt_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (ho : meromorphicOrderAt f x = 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_meromorphicOrderAt_eq_zero.

source

theorem tendsto_zero_of_meromorphicOrderAt_pos {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (ho : 0 < meromorphicOrderAt f x) :

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

source

theorem tendsto_nhds_of_meromorphicOrderAt_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (ho : 0 ≤ meromorphicOrderAt f x) :

∃ (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_meromorphicOrderAt_nonneg.

source

theorem tendsto_cobounded_iff_meromorphicOrderAt_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) ↔ meromorphicOrderAt f x < 0

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

source

theorem tendsto_nhds_iff_meromorphicOrderAt_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 ≤ meromorphicOrderAt f x

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

source

theorem tendsto_ne_zero_iff_meromorphicOrderAt_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)) ↔ meromorphicOrderAt f x = 0

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

source

theorem tendsto_zero_iff_meromorphicOrderAt_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 < meromorphicOrderAt f x

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

source

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

meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

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

source

theorem AnalyticAt.meromorphicOrderAt_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) :

meromorphicOrderAt f x = ENat.map Nat.cast (analyticOrderAt f x)

Compatibility of notions of order for analytic and meromorphic functions.

source

theorem AnalyticAt.meromorphicOrderAt_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) :

0 ≤ meromorphicOrderAt f x

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

source

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.

source

theorem meromorphicOrderAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (z₀ : 𝕜) (e : E) [Decidable (e = 0)] :

meromorphicOrderAt (fun (x : 𝕜) => e) z₀ = if e = 0 then ⊤ else 0

The order of a constant function is ⊤ if the constant is zero and 0 otherwise.

source

theorem meromorphicOrderAt_const_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (z₀ : 𝕜) (n : ℤ) [Decidable (↑n = 0)] :

meromorphicOrderAt (↑n) z₀ = if ↑n = 0 then ⊤ else 0

The order of a constant function is ⊤ if the constant is zero and 0 otherwise.

source

theorem meromorphicOrderAt_const_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (z₀ : 𝕜) (n : ℕ) [Decidable (↑n = 0)] :

meromorphicOrderAt (↑n) z₀ = if ↑n = 0 then ⊤ else 0

The order of a constant function is ⊤ if the constant is zero and 0 otherwise.

source

@[simp]

theorem meromorphicOrderAt_const_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (z₀ : 𝕜) (n : ℕ) [Decidable (↑n = 0)] :

meromorphicOrderAt (OfNat.ofNat n) z₀ = if ↑n = 0 then ⊤ else 0

The order of a constant function is ⊤ if the constant is zero and 0 otherwise.

Order at a Point: Behaviour under Ring Operations #

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

source

theorem meromorphicOrderAt_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) :

meromorphicOrderAt (f • g) x = meromorphicOrderAt f x + meromorphicOrderAt g x

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

source

theorem meromorphicOrderAt_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :

meromorphicOrderAt (f * g) x = meromorphicOrderAt f x + meromorphicOrderAt g x

The order is additive when multiplying meromorphic functions.

source

theorem meromorphicOrderAt_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) {n : ℕ} :

meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

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

source

theorem meromorphicOrderAt_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) {n : ℤ} :

meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

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

source

theorem meromorphicOrderAt_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} :

meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

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

source

@[simp]

theorem meromorphicOrderAt_add_of_top_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : meromorphicOrderAt f₁ x = ⊤) :

meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x

Adding a locally vanishing function does not change the order.

source

@[simp]

theorem meromorphicOrderAt_add_of_top_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₂ : meromorphicOrderAt f₂ x = ⊤) :

meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Adding a locally vanishing function does not change the order.

source

theorem meromorphicOrderAt_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 (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

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

source

theorem meromorphicOrderAt_add_eq_left_of_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) :

meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Helper lemma for meromorphicOrderAt_add_of_ne.

source

theorem meromorphicOrderAt_add_eq_right_of_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜} (hf₁ : MeromorphicAt f₁ x) (h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x) :

meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x

Helper lemma for meromorphicOrderAt_add_of_ne.

source

theorem meromorphicOrderAt_add_of_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 : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x) :

meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

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 #

source

theorem MeromorphicOn.isClopen_setOf_meromorphicOrderAt_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 | meromorphicOrderAt f ↑u = ⊤}

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

source

theorem MeromorphicOn.exists_meromorphicOrderAt_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), meromorphicOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤

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

source

theorem MeromorphicOn.meromorphicOrderAt_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 : meromorphicOrderAt f x ≠ ⊤) :

meromorphicOrderAt f y ≠ ⊤

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

source

theorem MeromorphicOn.eventually_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} (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.

source

theorem MeromorphicOn.eventually_analyticAt_or_mem_compl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} (h : MeromorphicOn f U) (hx : x ∈ U) :

∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ

source

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.

source

theorem MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_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 | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤} ∈ Filter.codiscrete ↑U

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

Order at a Point: Behaviour under Composition #

source

theorem MeromorphicAt.meromorphicOrderAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {g : 𝕜 → 𝕜} (hf : MeromorphicAt f (g x)) (hg : AnalyticAt 𝕜 g x) (hg_nc : ¬Filter.EventuallyConst g (nhds x)) :

meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun (x_1 : 𝕜) => g x_1 - g x) x)

If g is analytic at x, f is meromorphic at g x, and g is not locally constant near x, the order of f ∘ g is the product of the orders of f and g · - g x.

source

theorem meromorphicOrderAt_comp_of_deriv_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {g : 𝕜 → 𝕜} (hg : AnalyticAt 𝕜 g x) (hg' : deriv g x ≠ 0) [CompleteSpace 𝕜] [CharZero 𝕜] :

meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

If g is analytic at x, and g' x ≠ 0, then the meromorphic order of f ∘ g at x is the meromorphic order of f at g x (even if f is not meromorphic).

source

theorem meromorphicOrderAt_smul_of_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → 𝕜} (hg : AnalyticAt 𝕜 g x) (hg' : g x ≠ 0) :

meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

source

theorem meromorphicOrderAt_mul_of_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {g f : 𝕜 → 𝕜} (hg : AnalyticAt 𝕜 g x) (hg' : g x ≠ 0) :

meromorphicOrderAt (g * f) x = meromorphicOrderAt f x

Documentation

Mathlib.Analysis.Meromorphic.Order

Orders of Meromorphic Functions #

TODO #

Order at a Point: Definition and Characterization #

Order at a Point: Behaviour under Ring Operations #

Level Sets of the Order Function #

Order at a Point: Behaviour under Composition #