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 further properties of meromorphic functions in normal form, such as a local identity theorem. 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.

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.

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.

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.