Documentation

Mathlib.Analysis.Meromorphic.Basic

Meromorphic functions #

Main statements:

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

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

Equations
theorem AnalyticAt.meromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : AnalyticAt 𝕜 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.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] {f g : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
theorem MeromorphicAt.fun_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
@[deprecated MeromorphicAt.fun_add (since := "2025-05-09")]
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

Alias of MeromorphicAt.fun_add.

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) :
theorem MeromorphicAt.fun_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
@[deprecated MeromorphicAt.fun_smul (since := "2025-05-09")]
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

Alias of MeromorphicAt.fun_smul.

theorem MeromorphicAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
theorem MeromorphicAt.fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
MeromorphicAt (fun (z : 𝕜) => f z * g z) x
@[deprecated MeromorphicAt.fun_mul (since := "2025-05-09")]
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

Alias of MeromorphicAt.fun_mul.

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

Finite products of meromorphic functions are analytic.

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

Finite products of meromorphic functions are analytic.

theorem MeromorphicAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) :
theorem MeromorphicAt.fun_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
@[deprecated MeromorphicAt.fun_neg (since := "2025-05-09")]
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

Alias of MeromorphicAt.fun_neg.

@[simp]
theorem MeromorphicAt.neg_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} :
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) :
theorem MeromorphicAt.fun_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
@[deprecated MeromorphicAt.fun_sub (since := "2025-05-09")]
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

Alias of MeromorphicAt.fun_sub.

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

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] {f g : 𝕜E} {x : 𝕜} (h : f =ᶠ[nhdsWithin x {x}] g) :

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

theorem MeromorphicAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) :
theorem MeromorphicAt.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) :
MeromorphicAt (fun (z : 𝕜) => (f z)⁻¹) x
@[deprecated MeromorphicAt.fun_inv (since := "2025-05-09")]
theorem MeromorphicAt.inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) :
MeromorphicAt (fun (z : 𝕜) => (f z)⁻¹) x

Alias of MeromorphicAt.fun_inv.

@[simp]
theorem MeromorphicAt.inv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} :
theorem MeromorphicAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
theorem MeromorphicAt.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
MeromorphicAt (fun (z : 𝕜) => f z / g z) x
@[deprecated MeromorphicAt.fun_div (since := "2025-05-09")]
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

Alias of MeromorphicAt.fun_div.

theorem MeromorphicAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
theorem MeromorphicAt.fun_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
MeromorphicAt (fun (z : 𝕜) => f z ^ n) x
@[deprecated MeromorphicAt.fun_pow (since := "2025-05-09")]
theorem MeromorphicAt.pow' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
MeromorphicAt (fun (z : 𝕜) => f z ^ n) x

Alias of MeromorphicAt.fun_pow.

theorem MeromorphicAt.zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
theorem MeromorphicAt.fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
MeromorphicAt (fun (z : 𝕜) => f z ^ n) x
@[deprecated MeromorphicAt.fun_zpow (since := "2025-05-09")]
theorem MeromorphicAt.zpow' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
MeromorphicAt (fun (z : 𝕜) => f z ^ n) x

Alias of MeromorphicAt.fun_zpow.

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

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] [CompleteSpace E] {f : 𝕜E} {x : 𝕜} (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] {f : 𝕜E} {x : 𝕜} :
MeromorphicAt f x ∃ (n : ) (g : 𝕜E), AnalyticAt 𝕜 g x ∀ᶠ (z : 𝕜) in nhdsWithin x {x}, f z = (z - x) ^ n g z
def MeromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜E) (U : Set 𝕜) :

Meromorphy of a function on a set.

Equations
theorem AnalyticOnNhd.meromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 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) :

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

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.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) :
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) :
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 (z : 𝕜) => f z + g z) U
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) :
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 (z : 𝕜) => f z - g z) U
theorem MeromorphicOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} (hf : 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 (z : 𝕜) => -f z) U
@[simp]
theorem MeromorphicOn.neg_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} :
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) :
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 (z : 𝕜) => s z f z) U
theorem MeromorphicOn.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :
theorem MeromorphicOn.fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :
MeromorphicOn (fun (z : 𝕜) => s z * t z) U
theorem MeromorphicOn.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι𝕜𝕜} (h : ∀ (σ : ι), MeromorphicOn (f σ) U) :
MeromorphicOn (∏ ns, f n) U

Finite products of meromorphic functions are analytic.

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

Finite products of meromorphic functions are analytic.

theorem MeromorphicOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) :
theorem MeromorphicOn.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) :
MeromorphicOn (fun (z : 𝕜) => s⁻¹ z) U
@[simp]
theorem MeromorphicOn.inv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} :
theorem MeromorphicOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :
theorem MeromorphicOn.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s t : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :
MeromorphicOn (fun (z : 𝕜) => s z / t z) U
theorem MeromorphicOn.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ) :
theorem MeromorphicOn.fun_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ) :
MeromorphicOn (fun (z : 𝕜) => s z ^ n) U
theorem MeromorphicOn.zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ) :
theorem MeromorphicOn.fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ) :
MeromorphicOn (fun (z : 𝕜) => s z ^ n) 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) :
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) :