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 neighborhood of z₀, for some n : ℤ and g analytic at z₀.

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

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

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

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

@[simp]

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

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

theorem MeromorphicAt.fun_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (fun (i : 𝕜) => f i + g i) x

Eta-expanded form of MeromorphicAt.add

theorem MeromorphicAt.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) : MeromorphicAt (f • g) x

theorem MeromorphicAt.fun_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) : MeromorphicAt (fun (i : 𝕜) => f i • g i) x

Eta-expanded form of MeromorphicAt.smul

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

theorem MeromorphicAt.fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (fun (i : 𝕜) => f i * g i) x

Eta-expanded form of MeromorphicAt.mul

theorem MeromorphicAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜} {x : 𝕜} (h : ∀ (σ : ι), MeromorphicAt (F σ) x) : MeromorphicAt (∏ n ∈ s, F n) x

Finite products of meromorphic functions are meromorphic.

theorem MeromorphicAt.fun_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜} {x : 𝕜} (h : ∀ (σ : ι), MeromorphicAt (F σ) x) : MeromorphicAt (fun (z : 𝕜) => ∏ n ∈ s, F n z) x

Finite products of meromorphic functions are meromorphic.

theorem MeromorphicAt.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} {s : Finset ι} {G : ι → 𝕜 → E} {x : 𝕜} (h : ∀ (σ : ι), MeromorphicAt (G σ) x) : MeromorphicAt (∑ n ∈ s, G n) x

Finite sums of meromorphic functions are meromorphic.

theorem MeromorphicAt.fun_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} {s : Finset ι} {G : ι → 𝕜 → E} {x : 𝕜} (h : ∀ (σ : ι), MeromorphicAt (G σ) x) : MeromorphicAt (fun (z : 𝕜) => ∑ n ∈ s, G n z) x

Finite sums of meromorphic functions are meromorphic.

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

theorem MeromorphicAt.fun_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} (hf : MeromorphicAt f x) : MeromorphicAt (fun (i : 𝕜) => -f i) x

Eta-expanded form of MeromorphicAt.neg

@[simp]

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

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

theorem MeromorphicAt.fun_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (fun (i : 𝕜) => f i - g i) x

Eta-expanded form of MeromorphicAt.sub

theorem MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₁ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hf : MeromorphicAt f x) : MeromorphicAt (f + g) x ↔ MeromorphicAt g x

If f is meromorphic at x, then f + g is meromorphic at x if and only if g is meromorphic at x.

theorem MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hg : MeromorphicAt g x) : MeromorphicAt (f + g) x ↔ MeromorphicAt f x

If g is meromorphic at x, then f + g is meromorphic at x if and only if f is meromorphic at x.

theorem MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₁ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hf : MeromorphicAt f x) : MeromorphicAt (f - g) x ↔ MeromorphicAt g x

If f is meromorphic at x, then f - g is meromorphic at x if and only if g is meromorphic at x.

theorem MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hg : MeromorphicAt g x) : MeromorphicAt (f - g) x ↔ MeromorphicAt f x

If g is meromorphic at x, then f - g is meromorphic at x if and only if f is meromorphic at x.

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

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

If two functions agree on a punctured neighborhood, then one is meromorphic iff the other is so.

@[simp]

theorem MeromorphicAt.update_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [DecidableEq 𝕜] {f : 𝕜 → E} {z w : 𝕜} {e : E} : MeromorphicAt (Function.update f w e) z ↔ MeromorphicAt f z

theorem MeromorphicAt.update {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [DecidableEq 𝕜] {f : 𝕜 → E} {z : 𝕜} (hf : MeromorphicAt f z) (w : 𝕜) (e : E) : MeromorphicAt (Function.update f w e) z

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

theorem MeromorphicAt.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (fun (i : 𝕜) => (f i)⁻¹) x

Eta-expanded form of MeromorphicAt.inv

@[simp]

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

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

theorem MeromorphicAt.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (fun (i : 𝕜) => f i / g i) x

Eta-expanded form of MeromorphicAt.div

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

theorem MeromorphicAt.fun_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (fun (i : 𝕜) => f i ^ n) x

Eta-expanded form of MeromorphicAt.pow

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

theorem MeromorphicAt.fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (fun (i : 𝕜) => f i ^ n) x

Eta-expanded form of MeromorphicAt.zpow

theorem MeromorphicAt.eventually_continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} (h : MeromorphicAt f x) : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, ContinuousAt f y

If a function is meromorphic at a point, then it is continuous at nearby points.

theorem MeromorphicAt.eventually_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} [CompleteSpace E] {f : 𝕜 → E} (h : MeromorphicAt f x) : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 f y

In a complete space, a function which is meromorphic at a point is analytic at all nearby points. The completeness assumption can be dispensed with if one assumes that f is meromorphic on a set around x, see MeromorphicOn.eventually_analyticAt.

theorem MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} : MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = (z - x) ^ n • g z

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

Derivatives of meromorphic functions are meromorphic.

@[deprecated MeromorphicAt.deriv (since := "2025-12-21")]

theorem MeromorphicAt.fun_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) : MeromorphicAt (fun (z : 𝕜) => deriv f z) x

theorem MeromorphicAt.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {n : ℕ} {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) : MeromorphicAt (deriv^[n] f) x

Iterated derivatives of meromorphic functions are meromorphic.

@[deprecated MeromorphicAt.iterated_deriv (since := "2025-12-21")]

theorem MeromorphicAt.fun_iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {n : ℕ} {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) : MeromorphicAt (fun (z : 𝕜) => deriv^[n] f z) x

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

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

Composition with an analytic function

theorem MeromorphicAt.comp_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {x : 𝕜} {f : 𝕜' → F} {g : 𝕜 → 𝕜'} (hf : MeromorphicAt f (g x)) (hg : AnalyticAt 𝕜 g x) : MeromorphicAt (f ∘ g) x

The composition of a meromorphic and an analytic function is meromorphic.

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

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

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

theorem MeromorphicOn.congr_codiscreteWithin_of_eqOn_compl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) (h₁ : f =ᶠ[Filter.codiscreteWithin U] g) (h₂ : Set.EqOn f g Uᶜ) : MeromorphicOn g U

If f is meromorphic on U, if g agrees with f on a codiscrete subset of U and outside of U, then g is also meromorphic on U.

theorem MeromorphicOn.congr_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) (h₁ : f =ᶠ[Filter.codiscreteWithin U] g) (h₂ : IsOpen U) : MeromorphicOn g U

If f is meromorphic on an open set U, if g agrees with f on a codiscrete subset of U, then g is also meromorphic on U.

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

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

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

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

theorem MeromorphicOn.fun_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 (fun (i : 𝕜) => f i + g i) U

Eta-expanded form of MeromorphicOn.add

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

theorem MeromorphicOn.fun_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 (fun (i : 𝕜) => f i - g i) U

Eta-expanded form of MeromorphicOn.sub

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

theorem MeromorphicOn.fun_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) : MeromorphicOn (fun (i : 𝕜) => -f i) U

Eta-expanded form of MeromorphicOn.neg

@[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

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

theorem MeromorphicOn.fun_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 (fun (i : 𝕜) => s i • f i) U

Eta-expanded form of MeromorphicOn.smul

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

theorem MeromorphicOn.fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) : MeromorphicOn (fun (i : 𝕜) => s i * t i) U

Eta-expanded form of MeromorphicOn.mul

theorem MeromorphicOn.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜} (h : ∀ (σ : ι), MeromorphicOn (f σ) U) : MeromorphicOn (∏ n ∈ s, f n) U

Finite products of meromorphic functions are meromorphic.

theorem MeromorphicOn.fun_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜} (h : ∀ (σ : ι), MeromorphicOn (f σ) U) : MeromorphicOn (fun (z : 𝕜) => ∏ n ∈ s, f n z) U

Finite products of meromorphic functions are meromorphic.

theorem MeromorphicOn.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → E} (h : ∀ (σ : ι), MeromorphicOn (f σ) U) : MeromorphicOn (∑ n ∈ s, f n) U

Finite sums of meromorphic functions are meromorphic.

theorem MeromorphicOn.fun_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → E} (h : ∀ (σ : ι), MeromorphicOn (f σ) U) : MeromorphicOn (fun (z : 𝕜) => ∑ n ∈ s, f n z) U

Finite sums of meromorphic functions are meromorphic.

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

theorem MeromorphicOn.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) : MeromorphicOn (fun (i : 𝕜) => (s i)⁻¹) U

Eta-expanded form of MeromorphicOn.inv

@[simp]

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

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

theorem MeromorphicOn.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) : MeromorphicOn (fun (i : 𝕜) => s i / t i) U

Eta-expanded form of MeromorphicOn.div

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

theorem MeromorphicOn.fun_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ℕ) : MeromorphicOn (fun (i : 𝕜) => s i ^ n) U

Eta-expanded form of MeromorphicOn.pow

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

theorem MeromorphicOn.fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ℤ) : MeromorphicOn (fun (i : 𝕜) => s i ^ n) U

Eta-expanded form of MeromorphicOn.zpow

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

Derivatives of meromorphic functions are meromorphic.

@[deprecated MeromorphicOn.deriv (since := "2025-12-21")]

theorem MeromorphicOn.fun_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) [CompleteSpace E] : MeromorphicOn (fun (z : 𝕜) => deriv f z) U

theorem MeromorphicOn.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) [CompleteSpace E] {n : ℕ} : MeromorphicOn (deriv^[n] f) U

Iterated derivatives of meromorphic functions are meromorphic.

@[deprecated MeromorphicOn.iterated_deriv (since := "2025-12-21")]

theorem MeromorphicOn.fun_iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) [CompleteSpace E] {n : ℕ} : MeromorphicOn (fun (z : 𝕜) => deriv^[n] f z) U

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

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

theorem MeromorphicOn.countable_compl_analyticAt_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} [SecondCountableTopology 𝕜] [CompleteSpace E] (h : MeromorphicOn f U) : ({z : 𝕜 | AnalyticAt 𝕜 f z}ᶜ ∩ U).Countable

The singular set of a meromorphic function is countable.

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

Meromorphy of a function on all of 𝕜.

Equations

• Meromorphic f = ∀ (x : 𝕜), MeromorphicAt f x

@[simp]

theorem meromorphicOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : MeromorphicOn f Set.univ ↔ Meromorphic f

A function is meromorphic iff it is meromorphic on Set.univ.

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

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

theorem Meromorphic.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : Meromorphic fun (x_1 : 𝕜) => x

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

theorem Meromorphic.fun_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : Meromorphic f) : Meromorphic fun (i : 𝕜) => -f i

Eta-expanded form of Meromorphic.neg

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

theorem Meromorphic.fun_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} (hf : Meromorphic f) (hg : Meromorphic g) : Meromorphic fun (i : 𝕜) => f i + g i

Eta-expanded form of Meromorphic.add

theorem Meromorphic.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} {s : Finset ι} {G : ι → 𝕜 → E} (h : ∀ (σ : ι), Meromorphic (G σ)) : Meromorphic (∑ n ∈ s, G n)

theorem Meromorphic.fun_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} {s : Finset ι} {G : ι → 𝕜 → E} (h : ∀ (σ : ι), Meromorphic (G σ)) : Meromorphic fun (a : 𝕜) => ∑ c ∈ s, G c a

Eta-expanded form of Meromorphic.sum

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

theorem Meromorphic.fun_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} (hf : Meromorphic f) (hg : Meromorphic g) : Meromorphic fun (i : 𝕜) => f i - g i

Eta-expanded form of Meromorphic.sub

theorem Meromorphic.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} (hf : Meromorphic f) (hg : Meromorphic g) : Meromorphic (f • g)

theorem Meromorphic.fun_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} (hf : Meromorphic f) (hg : Meromorphic g) : Meromorphic fun (i : 𝕜) => f i • g i

Eta-expanded form of Meromorphic.smul

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

theorem Meromorphic.fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} (hf : Meromorphic f) (hg : Meromorphic g) : Meromorphic fun (i : 𝕜) => f i * g i

Eta-expanded form of Meromorphic.mul

theorem Meromorphic.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} (hf : Meromorphic f) : Meromorphic f⁻¹

theorem Meromorphic.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} (hf : Meromorphic f) : Meromorphic fun (i : 𝕜) => (f i)⁻¹

Eta-expanded form of Meromorphic.inv

theorem Meromorphic.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜} (h : ∀ (σ : ι), Meromorphic (F σ)) : Meromorphic (∏ n ∈ s, F n)

theorem Meromorphic.fun_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜} (h : ∀ (σ : ι), Meromorphic (F σ)) : Meromorphic fun (a : 𝕜) => ∏ c ∈ s, F c a

Eta-expanded form of Meromorphic.prod

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

theorem Meromorphic.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} (hf : Meromorphic f) (hg : Meromorphic g) : Meromorphic fun (i : 𝕜) => f i / g i

Eta-expanded form of Meromorphic.div

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

theorem Meromorphic.fun_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {n : ℕ} (hf : Meromorphic f) : Meromorphic fun (i : 𝕜) => f i ^ n

Eta-expanded form of Meromorphic.pow

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

theorem Meromorphic.fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {n : ℤ} (hf : Meromorphic f) : Meromorphic fun (i : 𝕜) => f i ^ n

Eta-expanded form of Meromorphic.zpow

theorem Meromorphic.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [CompleteSpace E] (hf : Meromorphic f) : Meromorphic (deriv f)

theorem Meromorphic.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [CompleteSpace E] {n : ℕ} (hf : Meromorphic f) : Meromorphic (deriv^[n] f)

theorem Meromorphic.countable_compl_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [SecondCountableTopology 𝕜] [CompleteSpace E] (h : Meromorphic f) : {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜ.Countable

The singular set of a meromorphic function is countable.

@[deprecated Meromorphic.countable_compl_analyticAt (since := "2025-12-21")]

theorem Meromorphic.MeromorphicOn.countable_compl_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [SecondCountableTopology 𝕜] [CompleteSpace E] (h : Meromorphic f) : {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜ.Countable

Alias of Meromorphic.countable_compl_analyticAt.

---

The singular set of a meromorphic function is countable.

@[deprecated Meromorphic.countable_compl_analyticAt (since := "2025-12-21")]

theorem MeromorphicOn.countable_compl_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [SecondCountableTopology 𝕜] [CompleteSpace E] (h : Meromorphic f) : {z : 𝕜 | AnalyticAt 𝕜 f z}ᶜ.Countable

Alias of Meromorphic.countable_compl_analyticAt.

---

The singular set of a meromorphic function is countable.

theorem Meromorphic.measurable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelSpace 𝕜] [MeasurableSpace E] [CompleteSpace E] [BorelSpace E] (h : Meromorphic f) : Measurable f

Meromorphic functions are measurable.

@[deprecated Meromorphic.measurable (since := "2025-12-21")]

theorem Meromorphic.MeromorphicOn.measurable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelSpace 𝕜] [MeasurableSpace E] [CompleteSpace E] [BorelSpace E] (h : Meromorphic f) : Measurable f

Alias of Meromorphic.measurable.

---

Meromorphic functions are measurable.

@[deprecated Meromorphic.measurable (since := "2025-12-21")]

theorem MeromorphicOn.measurable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelSpace 𝕜] [MeasurableSpace E] [CompleteSpace E] [BorelSpace E] (h : Meromorphic f) : Measurable f

Alias of Meromorphic.measurable.

---

Meromorphic functions are measurable.