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 : 𝕜} : MeromorphicNFAt f x ↔ f = toMeromorphicNFAt f x

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