Introducing `Meromorphic`

Stream: mathlib4

[Stefan Kebekus]

Prompted by comments of @Jireh Loreaux in the review of one of my PRs, I would like to suggest adding a notion of Meromorphic to the file Mathlib.Analysis.Meromorphic.Basic.lean, as a shorthand for MeromorphicOn _ Set.univ.

This would be in analogy to the existing notion of Differentiable in Mathlib.Analysis.Calculus.FDeriv.Defs.lean. If the community here is positive about the suggestion, I would be more than glad to implement it.

[Michael Rothgang]

I haven't thought about it deeply - but at first glance, this seems very reasonable!

[Floris van Doorn]

For almost all predicates on functions (Continuous, Differentiable, ContDiff, ContMDiff, MDifferentiable and even things like Injective) we have a predicate for the whole space and a predicate for a subset of the whole space. So this makes sense to add.

[Stefan Kebekus]

Thank you for your feedback. I will implement Meromorphic then and port existing statements to use it. To avoid merge conflicts and the resulting chaos, I will probably wait a few days until my currently open PRs are merged (or rejected).

[Filippo A. E. Nuccio]

It is perhaps also interesting to add the corresponding fun_prop API?

[Jireh Loreaux]

Interestingly, we have fun_prop for docs#MeromorphicAt, but not docs#MeromorphicOn.

[Jireh Loreaux]

I think we should have it for all three.

[Michael Rothgang]

Relatedly: is there a reason docs#AnalyticOn is not fun_prop, while docs#AnalyticAt is?

[Jireh Loreaux]

There's some other discrepancies here. For example, docs#MeromorphicOn doesn't really match docs#AnalyticOn, but rather docs#AnalyticOnNhd. I'm willing to accept (if someone knowledgable says so), that the docs#nhdsWithin variants are just not so useful, as I find that plausible. But if that's the case, I think we should either rename MeromorphicOn to MeromorphicOnNhd, or otherwise call attention to the discrepancy in docstring.

[Stefan Kebekus]

Dear all, following up on the discussion here, I would like to introduce Meromorphic now. I am however unsure about the best way to do it. In principle, I would like to add the definition below to Mathlib/Analysis/Meromorphic/Basic.lean and go through Mathlib and replace all instances of MeromorphicOn f Set.univ by Meromorphic f.

• Is this a sane way to start?
• Should I duplicate theorems that we have for MeromorphicOn? -- There are many!
• Should I add API for conversion between MeromorphicOn f Set.univ and Meromorphic f? If so, what is the best way to do it?
• Do I need to depreciate/rename/whatever theorems where I change the assumption? If so, how should I do that?

Any help is greatly appreciated. Season's Greeting, Stefan.

--

/-- Meromorphy of a function on all of 𝕜. -/
def Meromorphic (f : 𝕜 → E) := ∀ x, MeromorphicAt f x

/-- A function is meromorphic iff it is meromorphic on Set.univ. -/
lemma meromorphic_iff_meromorphicOn {f : 𝕜 → E} :
    Meromorphic f ↔ MeromorphicOn f Set.univ := by tauto

namespace Meromorphic

variable {s t : 𝕜 → 𝕜} {f g : 𝕜 → E} {U : Set 𝕜}

lemma meromorphicOn (h : Meromorphic f) :
    MeromorphicOn f Set.univ := by tauto

/--
The singular set of a meromorphic function is countable.
-/
theorem countable_compl_analyticAt [SecondCountableTopology 𝕜] [CompleteSpace E]
    (h : Meromorphic f) :
    {z | AnalyticAt 𝕜 f z}ᶜ.Countable := by
  simpa using h.meromorphicOn.countable_compl_analyticAt_inter

/--
Meromorphic functions are measurable.
-/
theorem measurable [MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelSpace 𝕜]
    [MeasurableSpace E] [CompleteSpace E] [BorelSpace E] (h : Meromorphic f) :
    Measurable f := by
  set s := {z : 𝕜 | AnalyticAt 𝕜 f z}
  have h₁ : sᶜ.Countable  := by simpa using h.meromorphicOn.countable_compl_analyticAt_inter
  have h₁' := h₁.to_subtype
  have h₂ : IsOpen s := isOpen_analyticAt 𝕜 f
  have h₃ : ContinuousOn f s := fun z hz ↦ hz.continuousAt.continuousWithinAt
  exact .of_union_range_cover (.subtype_coe h₂.measurableSet) (.subtype_coe h₁.measurableSet)
    (by simp [- mem_compl_iff]) h₃.restrict.measurable (measurable_of_countable _)

end Meromorphic

[Sébastien Gouëzel]

Yes, that's a very good plan. Your lemma meromorphic_iff_meromorphicOn should be called meromorphicOn_univ, marked simp and with sides reversed. There's no need to add versions of all lemmas for Meromorphic corresponding to those for MeromorphicOn, this can happen organically -- although it is probably good to add from the start the main ones like Meromorphic.add and friends.

If you change a lemma statement without changing the name, no need to deprecate. A deprecation is needed when you change the name, though.

The h₁ in your last proof should probably use the lemma Meromorphic.countable_compl_analyticAt that you introduce just before.

[Stefan Kebekus]

Thanks. Will do as Sebastien suggested.

[Jireh Loreaux]

@Stefan Kebekus I would probably do this in a few PRs instead of one though. That is, I would probably do this:

1. Define Meromorphic and establish very basic API lemmas about it.
2. Develop some of the more complex theorems for Meromorphic.
3. Replace all occurrences of MeromorphicOn univ with Meromorphic.

If (1) and (2) are small enough they can be a single PR. Alternatively, (2) and (3) could happen simultaneously (dependent on (1)). But I would especially separate out (3) because it will be very easy to review on its own, whereas it would just be noise if it was present in the diff of (1) or (2).

[Stefan Kebekus]

@Jireh Loreaux Thanks for your advice. I opened PR #33117 with your item 1 from your list. Season's Greetings -- Stefan.

[Johan Commelin]

Thanks Stefan! With the help of to_fun you can autogenerate all the fun_ variants. See my review.

[Stefan Kebekus]

Thanks Johan! Now this is helpful indeed. Merry Christmas! :christmas: