Normal form of meromorphic functions and continuous extension

If a function f is meromorphic on U and if g differs from f only along a set that is codiscrete within U, then g is likewise meromorphic. The set of meromorphic functions is therefore huge, and =ᶠ[codiscreteWithin U] defines an equivalence relation.

This file implements continuous extension to provide an API that allows picking the 'unique best' representative of any given equivalence class, where 'best' means that the representative can locally near any point x be written 'in normal form', as f =ᶠ[𝓝 x] fun z ↦ (z - x) ^ n • g where g is analytic and does not vanish at x.

TODO

Establish the analogous notion MeromorphicNFOn.

Normal form of meromorphic functions at a given point

Definition and characterizations

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

A function is 'meromorphic in normal form' at x if it vanishes around x or if it can locally be written as fun z ↦ (z - x) ^ n • g where g is analytic and does not vanish at x.

Equations

• MeromorphicNFAt f x = (f =ᶠ[nhds x] 0 ∨ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[nhds x] (fun (x_1 : 𝕜) => x_1 - x) ^ n • g)

theorem meromorphicNFAt_iff_analyticAt_or {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ ∃ (hf : MeromorphicAt f x), hf.order < 0 ∧ f x = 0

A meromorphic function has normal form at x iff it is either analytic there, or if it has a pole at x and takes the default value 0.

Relation to other properties of functions

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

If a function is meromorphic in normal form at x, then it is meromorphic at x.

theorem MeromorphicNFAt.order_nonneg_iff_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicNFAt f x) : 0 ≤ ⋯.order ↔ AnalyticAt 𝕜 f x

If a function is meromorphic in normal form at x, then it has non-negative order iff it is analytic.

theorem AnalyticAt.meromorphicNFAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) : MeromorphicNFAt f x

Analytic functions are meromorphic in normal form.

theorem MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [CompleteSpace E] {U : Set 𝕜} (hf : MeromorphicOn f U) : {x : 𝕜 | MeromorphicNFAt f x} ∈ Filter.codiscreteWithin U

Meromorphic functions have normal form outside of a discrete subset in the domain of meromorphicity.

Vanishing and order

theorem MeromorphicNFAt.order_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicNFAt f x) : ⋯.order = 0 ↔ f x ≠ 0

If f is meromorphic in normal form at x, then f has order zero iff it does not vanish at x.

See AnalyticAt.order_eq_zero_iff for an analogous statement about analytic functions.

Local nature of the definition and local identity theorem

theorem MeromorphicNFAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → E} (hf : MeromorphicNFAt f x) (hg : MeromorphicNFAt g x) : f =ᶠ[nhdsWithin x {x}ᶜ] g ↔ f =ᶠ[nhds x] g

Local identity theorem: two meromorphic functions in normal form agree in a neighborhood iff they agree in a pointed neighborhood.

See ContinuousAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd for the analogous statement for continuous functions.

theorem meromorphicNFAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → E} (hfg : f =ᶠ[nhds x] g) : MeromorphicNFAt f x ↔ MeromorphicNFAt g x

Meromorphicity in normal form is a local property.

Criteria to guarantee normal form

theorem MeromorphicNFAt.smul_analytic {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicNFAt f x) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) : MeromorphicNFAt (g • f) x

Helper lemma for meromorphicNFAt_iff_meromorphicNFAt_of_smul_analytic: if f is meromorphic in normal form at x and g is analytic without zero at x, then g • f is meromorphic in normal form at x.

theorem meromorphicNFAt_smul_iff_right_of_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {x : 𝕜} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) : MeromorphicNFAt (g • f) x ↔ MeromorphicNFAt f x

If f is any function and g is analytic without zero at z₀, then f is meromorphic in normal form at z₀ iff g • f is meromorphic in normal form at z₀.

theorem meromorphicNFAt_mul_iff_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {g : 𝕜 → 𝕜} {x : 𝕜} {f : 𝕜 → 𝕜} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) : MeromorphicNFAt (g * f) x ↔ MeromorphicNFAt f x

If f is any function and g is analytic without zero at z₀, then f is meromorphic in normal form at z₀ iff g * f is meromorphic in normal form at z₀.

theorem meromorphicNFAt_mul_iff_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {g : 𝕜 → 𝕜} {x : 𝕜} {f : 𝕜 → 𝕜} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) : MeromorphicNFAt (f * g) x ↔ MeromorphicNFAt f x

If f is any function and g is analytic without zero at z₀, then f is meromorphic in normal form at z₀ iff f * g is meromorphic in normal form at z₀.

Continuous extension and conversion to normal form

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

If f is meromorphic at x, convert f to normal form at x by changing its value at x. Otherwise, returns the 0 function.

Equations

• toMeromorphicNFAt f x = if hf : MeromorphicAt f x then Function.update f x (if h₁f : hf.order = ↑0 then Classical.choose ⋯ x else 0) else 0

theorem MeromorphicAt.eqOn_compl_singleton_toMermomorphicNFAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : Set.EqOn f (toMeromorphicNFAt f x) {x}ᶜ

Conversion to normal form at x changes the value only at x.

@[simp]

theorem toMeromorphicNFAt_of_not_meromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : ¬MeromorphicAt f x) : toMeromorphicNFAt f x = 0

If f is not meromorphic, conversion to normal form at x maps the function to 0.

theorem MeromorphicAt.eq_nhdNE_toMeromorphicNFAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : f =ᶠ[nhdsWithin x {x}ᶜ] toMeromorphicNFAt f x

Conversion to normal form at x changes the value only at x.

theorem meromorphicNFAt_toMeromorphicNFAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} : MeromorphicNFAt (toMeromorphicNFAt f x) x

After conversion to normal form at x, the function has normal form.

@[simp]

theorem toMeromorphicNFAt_eq_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} : toMeromorphicNFAt f x = f ↔ MeromorphicNFAt f x

If f has normal form at x, then f equals f.toNF.

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

If f is meromorphic in normal form, then so is its inverse.

@[simp]

theorem meromorphicNFAt_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} : MeromorphicNFAt f⁻¹ x ↔ MeromorphicNFAt f x

A function to 𝕜 is meromorphic in normal form at a point iff its inverse is.

Normal form of meromorphic functions on a given set

Definition

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

A function is 'meromorphic in normal form' on U if has normal form at every point of U.

Equations

• MeromorphicNFOn f U = ∀ ⦃z : 𝕜⦄, z ∈ U → MeromorphicNFAt f z

Relation to other properties of functions

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

If a function is meromorphic in normal form on U, then it is meromorphic on U.

theorem MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} [CompleteSpace E] (h₁f : MeromorphicNFOn f U) : 0 ≤ MeromorphicOn.divisor f U ↔ AnalyticOnNhd 𝕜 f U

If a function is meromorphic in normal form on U, then its divisor is non-negative iff it is analytic.

theorem AnalyticOnNhd.meromorphicNFOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (h₁f : AnalyticOnNhd 𝕜 f U) : MeromorphicNFOn f U

Analytic functions are meromorphic in normal form.

Divisors and zeros of meromorphic functions in normal form.

theorem MeromorphicNFOn.zero_set_eq_divisor_support {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} [CompleteSpace E] (h₁f : MeromorphicNFOn f U) (h₂f : ∀ (u : ↑U), ⋯.order ≠ ⊤) : U ∩ f ⁻¹' {0} = Function.support ⇑(MeromorphicOn.divisor f U)

If f is meromorphic in normal form on U and nowhere locally constant zero, then its zero set equals the support of the associated divisor.

Criteria to guarantee normal form

theorem meromorphicNFOn_smul_iff_right_of_analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} {g : 𝕜 → 𝕜} (h₁g : AnalyticOnNhd 𝕜 g U) (h₂g : ∀ u ∈ U, g u ≠ 0) : MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U

If f is any function and g is analytic without zero on U, then f is meromorphic in normal form on U iff g • f is meromorphic in normal form on U.

theorem meromorphicNFOn_mul_iff_right_of_analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f g : 𝕜 → 𝕜} (h₁g : AnalyticOnNhd 𝕜 g U) (h₂g : ∀ u ∈ U, g u ≠ 0) : MeromorphicNFOn (g * f) U ↔ MeromorphicNFOn f U

If f is any function and g is analytic without zero in U, then f is meromorphic in normal form on U iff g * f is meromorphic in normal form on U.

theorem meromorphicNFOn_mul_iff_left_of_analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f g : 𝕜 → 𝕜} (h₁g : AnalyticOnNhd 𝕜 g U) (h₂g : ∀ u ∈ U, g u ≠ 0) : MeromorphicNFOn (f * g) U ↔ MeromorphicNFOn f U

If f is any function and g is analytic without zero in U, then f is meromorphic in normal form on U iff f * g is meromorphic in normal form on U.

theorem meromorphicNFOn_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} : MeromorphicNFOn f⁻¹ U ↔ MeromorphicNFOn f U

A function to 𝕜 is meromorphic in normal form on U iff its inverse is.

Continuous extension and conversion to normal form

noncomputable def toMeromorphicNFOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜) : 𝕜 → E

If f is meromorphic on U, convert f to normal form on U by changing its values along a discrete subset within U. Otherwise, returns the 0 function.

Equations

• toMeromorphicNFOn f U = if h₁f : MeromorphicOn f U then fun (z : 𝕜) => if hz : z ∈ U then toMeromorphicNFAt f z z else f z else 0

@[simp]

theorem toMeromorphicNFOn_of_not_meromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : ¬MeromorphicOn f U) : toMeromorphicNFOn f U = 0

If f is not meromorphic on U, conversion to normal form maps the function to 0.

@[simp]

theorem toMeromorphicNFOn_eq_self_on_compl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : MeromorphicOn f U) : Set.EqOn (toMeromorphicNFOn f U) f Uᶜ

Conversion to normal form on U does not change values outside of U.

theorem toMeromorphicNFOn_eqOn_codiscrete {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} [CompleteSpace E] (hf : MeromorphicOn f U) : f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U

Conversion to normal form on U changes the value only along a discrete subset of U.

theorem MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdNE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} [CompleteSpace E] (hf : MeromorphicOn f U) (hx : x ∈ U) : toMeromorphicNFOn f U =ᶠ[nhdsWithin x {x}ᶜ] f

If f is meromorphic on U and x ∈ U, then f and its conversion to normal form on U agree in a punctured neighborhood of x.

theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} [CompleteSpace E] (hf : MeromorphicOn f U) (hx : x ∈ U) : toMeromorphicNFOn f U =ᶠ[nhds x] toMeromorphicNFAt f x

If f is meromorphic on U and x ∈ U, then conversion to normal form at x and conversion to normal form on U agree in a neighborhood of x.

theorem toMeromorphicNFOn_eq_toMeromorphicNFAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} [CompleteSpace E] (hf : MeromorphicOn f U) (hx : x ∈ U) : toMeromorphicNFOn f U x = toMeromorphicNFAt f x x

If f is meromorphic on U and x ∈ U, then conversion to normal form at x and conversion to normal form on U agree at x.

theorem meromorphicNFOn_toMeromorphicNFOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜) [CompleteSpace E] : MeromorphicNFOn (toMeromorphicNFOn f U) U

After conversion to normal form on U, the function has normal form.

@[simp]

theorem toMeromorphicNFOn_eq_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} [CompleteSpace E] : toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U

If f has normal form on U, then f equals toMeromorphicNFOn f U.

@[simp]

theorem order_toMeromorphicNFOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜} [CompleteSpace E] (hf : MeromorphicOn f U) (hx : x ∈ U) : ⋯.order = ⋯.order

Conversion of normal form does not affect orders.

@[simp]

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

Conversion of normal form does not affect divisors.