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

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

source

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

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

source

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

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

source

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

source

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

source

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

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

source

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

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

source

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

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

source

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

source

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

source

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

MeromorphicAt f⁻¹ x

source

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

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

source

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

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

source

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

source

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

MeromorphicAt (f ^ n) x

source

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

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

source

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

source

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

MeromorphicAt (f ^ n) x

source

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

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

source

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

source

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

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

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.

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

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.

source

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.

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

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

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

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

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

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

source

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

source

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

source

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

MeromorphicOn s⁻¹ U

source

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

MeromorphicOn (fun (z : 𝕜) => s⁻¹ z) 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.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

source

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

MeromorphicOn (s ^ n) U

source

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

MeromorphicOn (fun (z : 𝕜) => s z ^ 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.fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜 → 𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ℤ) :

MeromorphicOn (fun (z : 𝕜) => s z ^ 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.Meromorphic.Basic

Meromorphic functions #