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.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) :

MeromorphicAt 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 : 𝕜 → E} {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 (f • g) 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.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) :

MeromorphicAt (-f) 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 : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :

MeromorphicAt (f - g) x

source

theorem MeromorphicAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {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

@[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.pow {𝕜 : 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 (f ^ 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 = WithTop.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 = WithTop.map Nat.cast hf.order

Compatibility of notions of order for analytic and 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]

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 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.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 : 𝕜 → E} {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 : 𝕜 → E} {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 : 𝕜 → E} {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 #