API for continuous extension of meromorphic functions

Stream: mathlib4

[Stefan Kebekus]

Dear all,

as part of the ongoing project to formalize value distribution theory, I would like to add definitions/API for continuous extension of meromorphic functions to mathlib. I see various ways to do that and would like to ask your opinion before prematurely finalizing anything and then running into trouble.

@David Loeffler @Sébastien Gouëzel I'd love your feedback since you have worked with analytic and meromorphic functions.

Best wishes,

Stefan

---

In detail: I would like to say that a function is "continuously extended meromorphic at z₀" if it is locally zero, or if it looks like (z - z₀) ^ n • g, where g is analytic and does not vanish at z₀. This is a bit of a misnomer because it does not only require that the function is analytic at all resolvable singularities, but also imposes that it takes the default value 0 wherever it has a pole; this will make the API a lot more convenient. My plan is to define this as follows,

variable
  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]

def CEMeromorphicAt (f : 𝕜 → E) (z₀ : 𝕜) :=
  (f =ᶠ[𝓝 z₀] 0) ∨ (∃ (n : ℤ), ∃ g : 𝕜 → E, (AnalyticAt 𝕜 g z₀) ∧ (g z₀ ≠ 0) ∧ (f =ᶠ[𝓝 z₀] (· - z₀) ^ n • g))

then

• Prove that CEMeromorphicAt implies MeromorphicAt and establish a coercion
• Provide API to use CEMeromorphicAt, similar to what we have for analytic functions.
• Show that meromorphic functions can be made CEMeromorphicAt by updating their value at z₀
• Do the same with CEMeromorphicOn, showing that meromorphic functions can be made CEMeromorphicOn by changing their values along sets that are no worse than discrete within their domain of meromorphy

[Sébastien Gouëzel]

Are you sure this is a good concept? What bothers me is that the sum of two CEMeromorphic functions is in general not CEMeromorphic (take 1/z + 1 at 0), and same thing for the product (take 1/z * z).

[David Loeffler]

Yes, I was just about to post the same remark. Of course , if f, g are CEMeromorphic, there's a unique h which is CEMeromorphicAt z and agrees with f + g almost everywhere, but you need to know f and g on a whole neighbourhood of z to determine h z.

[Johan Commelin]

I've not worked with L^p spaces in mathlib, but maybe we can learn from what's done there. Because there the lesson is that it is convenient to work with actual functions, and almost-everywhere equality.
So maybe we want something like AEMeromorphic for functions that are almost everywhere meromorphic, except for a discrete set of points where they do something wacky. (And also the At, Within variants.)
That notion should be stable under algebraic operations.

Of course, evaluation such a function at a point will sometimes not give you the "correct" value. So there should be some API that "course corrects".

[David Loeffler]

Our current notion of Meromorphic is pretty much your AEMeromorphic – it is insensitive to modifying the function on a discrete set.

[David Loeffler]

The difference with Lp spaces is that there is genuinely no hope of selecting a "best" representative of an ae-equivalence class of measurable functions; while there is a reasonably sensible candidate for a representative of an equiv class of AEMeromorphic functions up to equality on a codiscrete set – namely Stefan's idea of filling in the gaps by continuity when that works, and by 0 otherwise.

[Stefan Kebekus]

Thanks for all your thoughtful comments, I greatly appreciate. Let me answer to the concerns of @Sébastien Gouëzel and @David Loeffler and explain my reasoning. Maybe someone (perhaps with more formalization experience) has better ideas. I am looking forward to your feedback!

Conceptually Right? The observation of @Sébastien Gouëzel and @David Loeffler is definitely correct and the concerns are justified. I guess what's going on here is this: we have meromorphic functions on a set U and the equivalence relation =ᶠ[Filter.codiscreteWithin U]. The quotient map is a map of rings (or more precisely: algebras over the sheaf of analytic functions). What I (would like to|need to) do is to define a section, by picking the 'obviously best' representative from each class. I believe that the examples of @Sébastien Gouëzel show that no section can ever be a ring morphism. Independent of the implementation details and the precise definition of 'obviously best', we will never get commutativity of continous extension with addition/multipliciation.

Should we then even have continuous extension in mathlib? I believe that continuous extension will be useful, complex analysis uses the operation implicitly nearly in every step of every argument. Example: given a meromorphic f defined on a compact U, the textbook proofs of Jensen's formula start by writing $f(z) = g(z) * \prod_{z_0 \in U} (z - z_0)^{\operatorname{order}_{z_0} f}$, where $g$ is analytic without zeros on $U$. In lean, we need to be more precise and replace equality by =ᶠ[Filter.codiscreteWithin U] of course. How do I define $g$ in lean? Easy: take the continuous extension of $f(z) * \prod_{z_0 \in U} (z - z_0)^{-\operatorname{order}_{z_0} f}$, done. In Project VD I need to do this all the time.

Sane API? You can argue. I also considered a few alternative options but did eventually settle on the one I proposed. Maybe you have/someone here has better ideas, and I'd be more than glad to hear them.

• Make CEMeromorphicAt an attribute of MeromorphicAt instead of a stand-alone definition. There might be a case for that. I did not pursue this idea because the definition of the attribute CEMeromorphicAt does not refer to the property MeromorphicAt that it describes. That looks quite odd to me.
• Make CEMeromorphicAt an attribute of Function then? Again, there might be a case for that, but mathlib does not seem to do that for any of the other attributes.
• Drop the idea of a definition and simply define "continuous extension" as a map from meromorphic functions to meromorphic functions, then state properties of the map. Now this seems reasonable and doable. If you prefer, I could go for that. But then, there will be dozens of theorems about to the output of the continuous extension map, and I need to repeat the relevant properties every time ... that prompted me to isolate the defintion CEMeromorphicAt so I can refer to it instead of repeating it.

[David Loeffler]

We have meromorphic functions on a set U and the equivalence relation =ᶠ[Filter.codiscreteWithin U]. The quotient map is a map of rings (or more precisely: algebras over the sheaf of analytic functions).

This assertion – including the implicit claim that the ring operations on the quotient are well-defined – would be a very nice thing to have in mathlib. (In fact I was vaguely planning to do this myself, and when I originally PR'ed the codiscrete filter it was with this application specifically in mind, but I somehow never got around to it :embarrassed:)

What I (would like to|need to) do is to define a section, by picking the 'obviously best' representative from each class.

I agree this would be worthwhile – both the section map, and the predicate on functions saying "this function is the best representative of its equiv class" (your CEMeromorphic). I'm not 100% sure about the name, since "continuously extended meromorphic" somehow suggests it should always be continuous and it isn't, but I don't have a better suggestion to offer.

[Stefan Kebekus]

@David Loeffler Thanks for your quick answer. I share your unease with the name and would welcome any suggestion...

[Johan Commelin]

Maybe the name of the section can be something like meromorphicRepr, indicating that it is a suitably chosen representative?

[Stefan Kebekus]

How about NormalFormMeromorphicAt, and then with a function MeromorphicAt.toNormalForm? Perhaps shorter as NFMeromorphic?

[Johan Commelin]

Sounds good to me. And I think the shorter NF variant is better, in order to keep the names reasonably short.

[Yaël Dillies]

I would rather name them MeromorphicNFAt and MeromorphicAt.meromorphicNFAt, but it's marginal

[Stefan Kebekus]

Very well, I will implement MeromorphicNFAt then. This will take me a few days because I have guests at the institute this week and next.

Looking forward to meeting you in the PR channel then. Best wishes, and thanks for your help!

[Stefan Kebekus]

I have prepared a first PR, which will come online as soon as PR #21502 is reviewed and merged. I am wondering if we should have a coercion/automatic conversion from MeromorphicNFAt to MeromorphicAt. Right now there is only a theorem:

/-- If a function is meromorphic in normal form at `x`, then it is meromorphic at `x`. -/
theorem MeromorphicNFAt.meromorphicAt (hf : MeromorphicNFAt f x) :
    MeromorphicAt f x := by
  sorry

I think an automatation can save users a lot of typing, but then I am not sure how to do that or if there are good reasons for not having it. Any help is greatly welcome.

[Stefan Kebekus]

Thanks again to everyone involved. The implementation of MeromorphicNFAt is now available as PR #22867.

[Stefan Kebekus]

The second batch of theorems on MeromorphicNFAt has arrived in PR #23005. The PR re-installs a theorem AnalyticAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd previously criticized by reviewers. It adds an analogous theorem MeromorphicNFAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd for meromorphic functions in normal form which, by transitivity, might be just as bad.

theorem AnalyticAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd
    (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
    f =ᶠ[𝓝[≠] z₀] g ↔ f =ᶠ[𝓝 z₀] g := by
    sorry

theorem MeromorphicNFAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd
    (hf : MeromorphicNFAt f z₀) (hg : MeromorphicNFAt g z₀) :
    f =ᶠ[𝓝[≠] z₀] g ↔ f =ᶠ[𝓝 z₀] g := by
    sorry

The reason for bringing these theorems back is that I use them in several places throughout Project VD, which makes it difficult for me to hide them with a private label. One might argue that MeromorphicNFAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd is what justifies the existence of the notion in the first place.

I have downgraded the PR to draft status and would like to ask your advice on how to handle this. Maybe there is a reformulation that is just as useful und more agreeable?

@Yaël Dillies @David Loeffler @Johan Commelin Since you have been involved in the first PR, I would love to hear your opinion. Thank you in advance!

[Yaël Dillies]

FYI you can type #23005 on Zulip and it will display as #23005

[Stefan Kebekus]

Ah! Now that will save me a lot of typing. Thanks.