Meromorphic functions #

Main statements:

MeromorphicAt: definition of meromorphy at a point
MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt: f is meromorphic at z₀ iff we have f z = (z - z₀) ^ n • g z on a punctured nhd of z₀, for some n : ℤ and g analytic at z₀.
MeromorphicAt.order: order of vanishing at z₀, as an element of ℤ ∪ {∞}

def MeromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (x : 𝕜) :

Prop

Meromorphy of f at x (more precisely, on a punctured neighbourhood of x; the value at x itself is irrelevant).

Equations

MeromorphicAt f x = ∃ (n : ℕ), AnalyticAt 𝕜 (fun (z : 𝕜) => (z - x) ^ n • f z) x

Instances For

source

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

MeromorphicAt f x

source

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

(∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0

source

theorem MeromorphicAt.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) :

MeromorphicAt _root_.id x

source

theorem MeromorphicAt.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E) (x : 𝕜) :

MeromorphicAt (fun (x : 𝕜) => e) x

source

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

MeromorphicAt (f + g) x

source

theorem MeromorphicAt.add' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :

MeromorphicAt (fun (z : 𝕜) => f z + g z) x

source

theorem MeromorphicAt.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) :

MeromorphicAt (f • g) x

source

theorem MeromorphicAt.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) :

MeromorphicAt (fun (z : 𝕜) => f z • g z) x

source

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

MeromorphicAt (f * g) x

source

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

MeromorphicAt (fun (z : 𝕜) => f z * g z) x

source

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

MeromorphicAt (-f) x

source

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

MeromorphicAt (fun (z : 𝕜) => -f z) x

source

@[simp]

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

MeromorphicAt (-f) x ↔ MeromorphicAt f x

source

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

MeromorphicAt (f - g) x

source

theorem MeromorphicAt.sub' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :

MeromorphicAt (fun (z : 𝕜) => f z - g z) x

source

theorem MeromorphicAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hfg : f =ᶠ[nhdsWithin x {x}ᶜ] g) :

MeromorphicAt g x

With our definitions, MeromorphicAt f x depends only on the values of f on a punctured neighbourhood of x (not on f x)

source

theorem MeromorphicAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) :

MeromorphicAt f⁻¹ x

source

theorem MeromorphicAt.inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) :

MeromorphicAt (fun (z : 𝕜) => (f z)⁻¹) x

source

@[simp]

theorem MeromorphicAt.inv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} :

MeromorphicAt f⁻¹ x ↔ MeromorphicAt f x

source

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

MeromorphicAt (f / g) x

source

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

MeromorphicAt (fun (z : 𝕜) => f z / g z) x

source

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

MeromorphicAt (f ^ n) x

source

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

MeromorphicAt (fun (z : 𝕜) => f z ^ n) x

source

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

MeromorphicAt (f ^ n) x

source

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

MeromorphicAt (fun (z : 𝕜) => f z ^ n) x

source

theorem MeromorphicAt.eventually_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :

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

source

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 vanishing of a meromorphic function, as an element of ℤ ∪ ∞ (to include the case of functions identically 0 near x).

Equations

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

Instances For

source

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

source

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

source

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.

source

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.

source

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.

source

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

MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = (z - x) ^ n • g z

source

def MeromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜) :

Prop

Meromorphy of a function on a set.

Equations

MeromorphicOn f U = ∀ x ∈ U, MeromorphicAt f x

Instances For

source

theorem AnalyticOnNhd.meromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) :

MeromorphicOn f U

source

@[deprecated AnalyticOnNhd.meromorphicOn (since := "2024-09-26")]

theorem AnalyticOn.meromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) :

MeromorphicOn f U

Alias of AnalyticOnNhd.meromorphicOn.

source

theorem MeromorphicOn.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} :

MeromorphicOn _root_.id U

source

theorem MeromorphicOn.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E) {U : Set 𝕜} :

MeromorphicOn (fun (x : 𝕜) => e) U

source

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.

source

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.

source

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

source

theorem MeromorphicOn.mono_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) {V : Set 𝕜} (hv : V ⊆ U) :

MeromorphicOn f V

source

theorem MeromorphicOn.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) :

MeromorphicOn (f + g) U

source

theorem MeromorphicOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) :

MeromorphicOn (f - g) U

source

theorem MeromorphicOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) :

MeromorphicOn (-f) U

source

@[simp]

theorem MeromorphicOn.neg_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} :

MeromorphicOn (-f) U ↔ MeromorphicOn f U

source

theorem MeromorphicOn.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : 𝕜 → 𝕜} {f : 𝕜 → E} {U : Set 𝕜} (hs : MeromorphicOn s U) (hf : MeromorphicOn f U) :

MeromorphicOn (s • f) U

source

theorem MeromorphicOn.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :

MeromorphicOn (s * t) U

source

theorem MeromorphicOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) :

MeromorphicOn s⁻¹ U

source

@[simp]

theorem MeromorphicOn.inv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} :

MeromorphicOn s⁻¹ U ↔ MeromorphicOn s U

source

theorem MeromorphicOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :

MeromorphicOn (s / t) U

source

theorem MeromorphicOn.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ℕ) :

MeromorphicOn (s ^ n) U

source

theorem MeromorphicOn.zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ℤ) :

MeromorphicOn (s ^ n) U

source

theorem MeromorphicOn.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) (h_eq : Set.EqOn f g U) (hu : IsOpen U) :

MeromorphicOn g U

source

theorem MeromorphicOn.eventually_codiscreteWithin_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} [CompleteSpace E] (f : 𝕜 → E) (h : MeromorphicOn f U) :

∀ᶠ (y : 𝕜) in Filter.codiscreteWithin U, AnalyticAt 𝕜 f y

Documentation

Mathlib.Analysis.Analytic.Meromorphic

Meromorphic functions #