Do we want a lemma AnalyticAt.ofNat?

Stream: mathlib4

[Michael Rothgang]

#30587 is straightforward (and almost ready to be merged), except for one remaining question: the PR adds a lemma MeromorphicAt.ofNat stating that ofNat(n) : 𝕜 → 𝕜 is meromorphic at each point. Do we want to have such lemmas in general? There seems to be none about analytic, continuous or differentiable functions.

[Sébastien Gouëzel]

What does this lemma even say? I.e., what is ofNat(n) : 𝕜 → 𝕜?

[Sébastien Gouëzel]

If it's the constant function, we should just have the fact that a constant function is meromorphic, no reason to specialize it.

[Michael Rothgang]

Yes, it's the constant function (and mathlib knows that fact).

[Sébastien Gouëzel]

In any case, it's unclear enough that I think we should avoid this phrasing.

[Sébastien Gouëzel]

(and so dump the lemma)

[Yaël Dillies]

But then you can't prove inline that 1 : 𝕜 → 𝕜 is meromorphic!

[Yaël Dillies]

I think your argument also applies to Nat.cast, Int.cast, Rat.cast, and all these lemmas should be there for eg fun_prop to correctly work

[Sébastien Gouëzel]

Yaël Dillies said:

But then you can't prove inline that 1 : 𝕜 → 𝕜 is meromorphic!

Yes, and that's fine because I claim we should avoid 1 : 𝕜 → 𝕜: it wasn't clear to me if this was the constant function one or the identity. There are many more obvious spellings that we could/should use instead.

[Stefan Kebekus]

Dear all, Yaël was quicker than me. The following file illustrates the use of the lemma (which I learned from Yaël earlier on). I think that this is a valid use case, but I do not have a strong enough opinion to start a lengthy/controversial argument or pick up a fight with anyone here…

import Mathlib.Analysis.Meromorphic.Basic

open MeromorphicOn Metric Real Set Classical

variable
  {𝕜 : Type*} [NontriviallyNormedField 𝕜] {x : 𝕜}
  {ι : Type*} {F : ι → 𝕜 → 𝕜}

namespace MeromorphicAt

theorem test₁ : MeromorphicAt (∏ n ∈ ∅, F n) x := by
  rw [Finset.prod_empty]
  -- At this stage, we have the goal `MeromorphicAt 1 x`, where the symbol `1`
  -- really means `One.toOfNat1 : 𝕜 → 𝕜`. Mathlib knows that constant
  -- functions are analytic/meromorphic, but cannot match the symbol `1` with
  -- the constant function `fun _ ↦ 1 : 𝕜 → 𝕜`. Therefore neither `simp` nor
  -- `fun_prop` can close the goal at this point.
  sorry

-- This lemma is in a form that allows matching `1` with the constant function.
@[fun_prop, simp]
lemma ofNat (n : ℕ) (x : 𝕜) : MeromorphicAt (ofNat(n) : 𝕜 → 𝕜) x :=
  analyticAt_const.meromorphicAt

-- With the lemma above in place, the following now compiles fine, both using
-- `simp` or `fun_prop`.
theorem test₂ : MeromorphicAt (∏ n ∈ ∅, F n) x := by
  simp

end MeromorphicAt

[Eric Wieser]

If the thought is that we should avoid ofNat(n) : x -> y, then I think the natural conclusion is that docs#Pi.ofNat_def should be simp

[Eric Wieser]

But I agree with Yael, and think that if we did that we should surely do the same for the other casts too.

[Eric Wieser]

For what it's worth I think I added quite a lot of these lemmas for deriv already, such as docs#deriv_ofNat

[Stefan Kebekus]

@Eric Wieser I am unsure if I understand your suggestion. I removed the lemma ofNat in the file above and marked the lemma Pi.ofNat_def as @[simp], but that did not help to prove the theorems test₁ and test₂ using simp or fun_prop. Am I making a mistake somehow?

[Eric Wieser]

My personal preference is to keep the ofNat lemma you have

[Yury G. Kudryashov]

I think that this deserves an official decision from maintainers. Let me start a discussion in the maintainers' channel.

[Stefan Kebekus]

@Yury G. Kudryashov Thanks for taking your time to look at this,