Principles of Isolated Zeros and Identity Principles for Meromorphic Functions

In line with results in Mathlib.Analysis.Analytic.IsolatedZeros and Mathlib.Analysis.Analytic.Uniqueness, this file establishes principles of isolated zeros and identity principles for meromorphic functions.

Compared to the results for analytic functions, the principles established here are a little more complicated to state. This is because meromorphic functions can be modified at will along discrete subsets and still remain meromorphic.

Principles of Isolated Zeros

theorem MeromorphicAt.frequently_zero_iff_eventuallyEq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} (hf : MeromorphicAt f x) : (∃ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = 0) ↔ f =ᶠ[nhdsWithin x {x}ᶜ] 0

The principle of isolated zeros: If f is meromorphic at x, then f vanishes eventually in a punctured neighborhood of x iff it vanishes frequently in punctured neighborhoods.

See AnalyticAt.frequently_zero_iff_eventually_zero for a stronger result in the analytic case.

theorem MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {x : 𝕜} {f : 𝕜 → E} (hf : MeromorphicAt f x) (h₁x : x ∈ U) (h₂x : AccPt x (Filter.principal U)) (h : f =ᶠ[Filter.codiscreteWithin U] 0) : f =ᶠ[nhdsWithin x {x}ᶜ] 0

Variant of the principle of isolated zeros: Let U be a subset of 𝕜 and assume that x ∈ U is not an isolated point of U. If a function f is meromorphic at x and vanishes along a subset that is codiscrete within U, then f vanishes in a punctured neighbourhood of f.

For a typical application, let U be a path in the complex plane and let x be one of the end points. If f is meromorphic at x and vanishes on U, then it will vanish in a punctured neighbourhood of x, which intersects U non-trivally but is not contained in U.

The assumption that x is not an isolated point of U is expressed as AccPt x (𝓟 U). See accPt_iff_frequently and accPt_iff_frequently_nhdsNE for useful reformulations.

Identity Principles

theorem MeromorphicAt.frequently_eq_iff_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : (∃ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = g z) ↔ f =ᶠ[nhdsWithin x {x}ᶜ] g

Formulation of MeromorphicAt.frequently_zero_iff_eventuallyEq_zero as an identity principle: If f and g are meromorphic at x, then f and g agree eventually in a punctured neighborhood of x iff they agree at points arbitrarily close to (but different from) x.

theorem MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {x : 𝕜} {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) (h₁x : x ∈ U) (h₂x : AccPt x (Filter.principal U)) (h : f =ᶠ[Filter.codiscreteWithin U] g) : f =ᶠ[nhdsWithin x {x}ᶜ] g

Formulation of MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin as an identity principle: Let U be a subset of 𝕜 and assume that x ∈ U is not an isolated point of U. If function f and g are meromorphic at x and agree along a subset that is codiscrete within U, then f and g agree in a punctured neighbourhood of f.