Project VD -- Value Distribution Theory

Stream: general

[Johan Commelin]

This is a discussion thread for #announce > Announcing Project VD -- Value Distribution Theory

[Johan Commelin]

@Stefan Kebekus there was quite some discussion of meromorphic functions here on zulip. How was your experience formalizing them? Because on the one hand you want to treat them as honest functions that you can evaluate at points, and on the other hand, they are equivalence classes, and they aren't defined everywhere...

[Stefan Kebekus]

@Johan Commelin I wanted to keep them as functions because I need to integrate. So, I wrote some API for "continuous extension". The process takes a meromorphic function f and delivers a function F such that

• f and F agree away from a codiscrete set (Filter.codiscreteWithin is the word)
• Near every point x, the function F is either constant zero, or looks like (z-x)^n·g, where g is analytic without zero at z.

That's what all the source files "strictlyMeromorphic_…" are for.

And then one proves that integrability and value of integrals does not see changes on a codiscrete set.

[Stefan Kebekus]

@Johan Commelin One trivial thing that I found amazingly difficult is the 'pole/zero order' of a meromorphic function. The order of an analytic function is in ℕ∞, for which there is good API. The order of a meromorphic function is in WithTop ℤ, for which there is hardly any API at all. I lost substantial time before I got things right there.

We have a meeting with @Jon Eugster and some members of the FRO next week, where I would like to bring this up. There must be a way to automatise things: if you add TOP to an ordered/whatever (semi)ring/whatever, then the WithTop type should inherit some structure that makes life bearable.

[Kevin Buzzard]

Wow, if I'd known about all this I would have asked you to speak at LT2025 :-)

[Stefan Kebekus]

@Johan Commelin That's another thing: I would really like to have that functions that are mermorphicOn a given set form a ring, so I can talk about units, localization, etc. I plan to also discuss that next week.

[Stefan Kebekus]

@Kevin Buzzard Thank you so much (blushing). I am very much a beginner, though … so I thought I better take my time before I embarrass myself stepping into the limelight.

[Yaël Dillies]

Stefan Kebekus said:

We have a meeting with @Jon Eugster and some members of the FRO next week, where I would like to bring this up. There must be a way to automatise things: if you add TOP to an ordered/whatever (semi)ring/whatever, then the WithTop type should inherit some structure that makes life bearable.

Why talk to the FRO here? It looks like this is a mathlib problem (quite possibly my problem :smile:)

[Joachim Breitner]

Because the FRO people are using the Seminar in Freiburg as an excuse to hang out and meet in person and get some free snacks in the tea time, and once we are there I expect there is little that can stop from Stefan from talking to us :-D

But indeed I expect I’d have little to respond, besides “ask Yaël” :-)

[Stefan Kebekus]

@Yaël Dillies I guess the honest answer to your question is "Because I joined only recently and have no clue who is in charge of what." I am a bit worried that I might have stepped on your toes here. That wasn't my intention, so please accept my apologies if I did. Do I understand correctly that you are the person I should be talking to when it comes to ℕ∞and WithTop ℤ? I would love to discuss these matters with an expert, as I am struggling to implement the relevant improvements myself.

[Kim Morrison]

@Stefan Kebekus, there's not really any one "in charge" of particular pieces of Mathlib. The "Authors" line in each file is some combination of "people you can go to for help" and "whoever originally wrote the file".

The Mathlib maintainers have final say on whether PRs go in, but they rely extensively on reviewing done by many people. And everyone is welcome, indeed encouraged, to be bold and suggest changes throughout the library. (Of course, if you're new it helps to discuss changes here on zulip ahead of making PRs, and please try to keep PRs to a manageable, reviewable size; we're perpetually bottlenecked by reviewing capacity.)

Yaël's comment above doesn't mean at all that you are stepping on their toes. Only that they would like to help with this sort of problem. Yaël has done lots of great work refactoring the interactions between the algebra and order hierarchies, so your question is right in their expertise.

[Jon Eugster]

It's not that Yaël is necessarily in charge of anything in mathlib in particular, but ask_yael is one of our most cutting-edge general-purpose tactics we have for mathlib. Some would even claim @Yaël Dillies is a real person:wink:

In any case, they'd probably have a good insight about what would be the best step to improve the API around WithTop. I have a hunch that it could be a slimple refactor vonsisting of just generalising some lemmas about \N_\infty to a general WithTop, but haven't looked at the code at all yet

[Yaël Dillies]

Kim Morrison said

Yaël's comment above doesn't mean at all that you are stepping on their toes. Only that they would like to help with this sort of problem. Yaël has done lots of great work refactoring the interactions between the algebra and order hierarchies, so your question is right in their expertise.

Yes, exactly. Sorry for being evasive. My toes are safe :relieved:

[Yaël Dillies]

I am very busy this week (which is why you won't have seen me at Lean Together), but feel free to explain your problems (here or in DM) and I will aim to answer next week

[Stefan Kebekus]

Thanks for all your encouraging comments. @Yaël Dillies I would love to discuss these matters here with you. Please give me a day or two, my day job is calling.

[Stefan Kebekus]

@Yaël Dillies Dear Yaël, dear all,

Thank you for offering to help. As I wrote above, I am a beginner with Lean and just started my first real-world project. Working with analytic and meromorphic functions, I was struck by the difference between ℕ∞and WithTop ℤ (the first appears as the vanishing order of analytic functions, the second as the vanishing/pole order of meromorphic function). While ℕ∞ and ENat.toNatwas typically easy to work with, I got stuck with WithTop ℤ where I have to use untop and untop. Typically, I ended up with workarounds that I might do the job but should better not be shown in public. I append a few examples below, but you can also look at the file FLUG/kebekus-Item4.lean in this GitHub repo for easier access. Any help is greatly appreciated! Am I overlooking something terribly simple or obvious?

More conceptually, I wonder if one should implement a method .toBase on any WithTop A where A is an algebraic structure with zero, emulating precisely what toNat does for ℕ∞. Maybe that could even replace toNat entirely? Implementing such a change is perhaps a bit drastic, so I thought I might bring this up here. I'd love to hear your opinion.

Thanks again · Best wishes,

Stefan.

import Mathlib.Analysis.SpecialFunctions.Exp


-- # ENat und WithTop ℤ

-- ## Example 1

-- I am puzzled. Is it really that complicated?
lemma WithTopCoe
  {n : WithTop ℕ} :
  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
  rcases n with h|h
  · intro h
    contradiction
  · intro h₁
    simp only [WithTop.map, Option.map] at h₁
    rw [Int.ofNat_eq_zero.mp (WithTop.coe_eq_zero.mp h₁)]
    rfl


-- ## Example 2

-- Easy
lemma toNat_add {a b : ENat} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (a + b).toNat = a.toNat + b.toNat :=
  ENat.toNat_add ha hb


-- Complicated. Even the formulation needs a lemma
lemma ne_top_add_ne_top {a b : WithTop ℤ} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    a + b ≠ ⊤ := by
  simp; tauto

lemma untop_add {a b : WithTop ℤ} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (a + b).untop (ne_top_add_ne_top ha hb) = a.untop ha + (b.untop hb) := by
  rw [WithTop.untop_eq_iff]
  rw [WithTop.coe_add]
  rw [WithTop.coe_untop]
  rw [WithTop.coe_untop]


-- Unclear to me. Is this easy?
lemma untop'_add {a b : WithTop ℤ} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (a + b).untop' 0 = a.untop' 0 + b.untop' 0 := by
  sorry


-- ## Example 3

-- Easy
lemma toNat'_of_ne_top_eq_coe {a : ENat} (ha : a ≠ ⊤) :
    a.toNat = a := by
  simpa


-- Easy
lemma untop_of_ne_top_eq_coe {a : WithTop ℤ} (ha : a ≠ ⊤) :
    a.untop ha = a := by
  simp


-- Complicated. Isn't there an easier proof?
lemma untop'_of_ne_top_eq_coe {a : WithTop ℤ} {d : ℤ} (ha : a ≠ ⊤) :
    WithTop.untop' d a = a := by
  obtain ⟨b, hb⟩ := WithTop.ne_top_iff_exists.1 ha
  rw [← hb]
  simp


-- ## Example 4

-- Unclear to me. Is there an easy proof?
lemma untop'_and_untop {a : ENat} (ha : a ≠ ⊤) :
    a.untop ha = a.untop' 0 := by
  sorry


-- ## Example 5

-- Easy
lemma add_mul_enat {a : ℕ} {b : ENat} :
    a * b + b = (a + 1) * b := by
  rw [add_one_mul]


-- Unclear to me. Is there an easy proof?
lemma add_mul_withTop {a : ℕ} {b : WithTop ℤ} :
    a * b + b = (a + 1) * b := by
  sorry

[Johan Commelin]

I think a toBase might make sense.

Here is a proof of the sorry in your codeblock:

lemma untop'_add {a b : WithTop ℤ} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    (a + b).untop' 0 = a.untop' 0 + b.untop' 0 := by
  rw [WithTop.ne_top_iff_exists] at ha hb
  obtain ⟨a, rfl⟩ := ha
  obtain ⟨b, rfl⟩ := hb
  norm_cast

[Johan Commelin]

Note that in the obtain, I use a rfl pattern to automatically substitute the old variable. You could use that to slighly simplify the proof of untop'_of_ne_top_eq_coe

lemma untop'_of_ne_top_eq_coe {a : WithTop ℤ} {d : ℤ} (ha : a ≠ ⊤) :
    WithTop.untop' d a = a := by
  obtain ⟨b, rfl⟩ := WithTop.ne_top_iff_exists.1 ha
  simp

[Stefan Kebekus]

@Johan Commelin Thanks! I will come back to you about toBase soon.

[Johan Commelin]

It might make sense to assume Inhabited X, which will provide a "canonical" element default : X. This will be a bit more agnostic than assuming Zero X and using 0 :X.
For Nat and Int, the default value is in fact 0.

[Yaël Dillies]

It could be called untopI, or getI (I don't understand the name untop)

[Stefan Kebekus]

@Johan Commelin @Yaël Dillies Before coming back to toBase (or whatever it will eventually be called), I thought about Example #5 from my little list:

-- Easy
lemma add_mul_enat {a : ℕ} {b : ENat} : a * b + b = (a + 1) * b := by
  rw [add_one_mul]

-- Unclear to me. Is there an easy proof?
lemma add_mul_withTop {a : ℕ} {b : WithTop ℤ} : a * b + b = (a + 1) * b := by
  sorry

Any attempt to prove the second statement by add_one_mulfails because WithTop ℤ is not known to lean as an instance of RightDistribClass. Looking at the code of mathlib, I was not able to figure out why ENat is an instance and WithTop ℤ is not. Do you have any insight here? Is there an easy fix that declares in instance in all reasonable cases?

[Sébastien Gouëzel]

The issue is that multiplication in WithTop ℤ has to be badly-behaved: how do you define $(-1) * \infty$ given that it has to be either an integer, or $\infty$? The current version in mathlib defines it to be $\infty$ (while $0 * \infty$ is defined to be $0$). This means that the identity $a * b + b = (a + 1) * b$ is not true for $a=-1$ and $b=\infty$, so it's not possible to register a nice typeclass involving multiplication on WithTop ℤ.

[Stefan Kebekus]

@Sébastien Gouëzel Understood. How upsetting. I should have guessed that. Thanks for your help!

[Sébastien Gouëzel]

Note that for your use case, where a is a natural number, the lemma is true. But I'm not surprised there is something to prove, and it can not follow from abstract nonsense.

[Stefan Kebekus]

Right. I guess I should spend some thought finding the correct formulation of the lemma I need to prove.

[Johan Commelin]

You need WithTop ℤ for the type of pole orders, right? But do you need to multiply those? Usually < and + are what you need, right? There is a whole theory of valuations, and I guess we can try to plug that in here.
Or am I missing a requirement?

[Stefan Kebekus]

@Johan Commelin Thanks for coming back to this. Essentially, I need to do arithmetic in WithTop ℤ because I want to multiply/factor/add meromorphic functions and discuss their pole order. That ends up evaluating polynomials ℤ[x] on x : WithTop ℤ. The simplest example comes up when taking powers of meromorphic functions.

theorem MeromorphicAt.order_pow (hf : MeromorphicAt f z₀) {n : ℕ} :
    (hf.pow n).order = n * hf.order := by
  induction' n with n hn
  · simp
    rw [← WithTop.coe_zero, MeromorphicAt.order_eq_int_iff]
    use 1, analyticAt_const
    simp
  · simp [add_mul, pow_add, (hf.pow n).order_mul hf, hn]
    sorry

Here, MeromorphicAt.add_mul is the following theorem, currently submitted as a PR.

import Mathlib.Analysis.Analytic.Meromorphic

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {f g : 𝕜 → 𝕜} {z₀ : 𝕜}

/-- Helper lemma for `MeromorphicAt.order_mul` -/
lemma MeromorphicAt.order_of_locallyZero_mul_meromorphic (hf : MeromorphicAt f z₀)
    (hg : MeromorphicAt g z₀) (h'f : hf.order = ⊤) :
    (hf.mul hg).order = ⊤ := by
  rw [MeromorphicAt.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at *
  obtain ⟨t, h₁t, h₂t⟩ := h'f
  use t, fun y h₁y h₂y ↦ (by rw [Pi.mul_apply, h₁t y h₁y h₂y, zero_mul])

/-- The order is additive when multiplying meromorphic functions -/
theorem MeromorphicAt.order_mul (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) :
    (hf.mul hg).order = hf.order + hg.order := by
  -- Trivial cases: one of the functions vanishes around z₀
  by_cases h₂f : hf.order = ⊤
  · simp [hf.order_of_locallyZero_mul_meromorphic hg, h₂f]
  by_cases h₂g : hg.order = ⊤
  · simp [mul_comm f g, hg.order_of_locallyZero_mul_meromorphic hf, h₂g]
  -- Non-trivial case: both functions do not vanish around z₀
  have h₃f := (hf.order.coe_untop h₂f).symm
  have h₃g := (hg.order.coe_untop h₂g).symm
  rw [h₃f, h₃g, ← WithTop.coe_add, MeromorphicAt.order_eq_int_iff]
  obtain ⟨F, h₁F, h₂F, h₃F⟩ := (hf.order_eq_int_iff (hf.order.untop h₂f)).1 h₃f
  obtain ⟨G, h₁G, h₂G, h₃G⟩ := (hg.order_eq_int_iff (hg.order.untop h₂g)).1 h₃g
  clear h₃f h₃g
  use F * G, h₁F.mul h₁G, by simp; tauto
  rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at *
  obtain ⟨s, h₁s, h₂s, h₃s⟩ := h₃F
  obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₃G
  use s ∩ t
  constructor
  · intro y h₁y h₂y
    simp [h₁s y h₁y.1 h₂y, h₁t y h₁y.2 h₂y, zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)]
    group
  · exact ⟨IsOpen.inter h₂s h₂t, Set.mem_inter h₃s h₃t⟩

[Johan Commelin]

Understood. And I agree that it makes sense to multiply n : Nat with x : WithTop Int. But here n is not playing the role of a pole order, it is really a natural number.
So it makes sense to define SMul Nat (WithTop Int) (and probably this already exists).
My (more precise, hopefully) question is whether one ever needs to multiply two pole orders. My algebraic mind says that this never happens...

[Stefan Kebekus]

Agreed, I cannot think of a setting where one wants to multiply a pole order with infinity. I will come back to the SMul suggestion, but now I have to rush to setup my presentation for our FLUG meeting.

[Sébastien Gouëzel]

In your first lemma, you're writing (hf.pow n).order = n * hf.order. Here, there is first a cast of the integer n to WithTop ℤ, and the use of the weird multiplication on it. But what you're really using is just that there is an addition on WithTop ℤ (from which an action of natural numbers follows). So I'd try to avoid completely the bogus multiplication on WithTop ℤ, and write your statement instead as (hf.pow n).order = n • hf.order. Hopefully the nat action is always well behaved on WithTop of something, so useful API lemmas should come in.

[Sébastien Gouëzel]

Johan has been quicker to say the same thing.

[Joachim Breitner]

Would it make things easier to work in EInt, with in infinities on both sides, for a nicer algebraic structure, and invoking explicit theorems when one needs the fact that -inf is not possible? (A bit like PMFs go to EReal despite guaranteed to be finite)

[Yaël Dillies]

PMFs don't go to docs#EReal (?)

[Joachim Breitner]

Ah, my bad then, maybe I misremembered (there was something I tried to do a while ago but abandoned in https://github.com/leanprover-community/mathlib4/pull/7155)

[Stefan Kebekus]

Dear all, I am trying to write down the standard estimate for log⁺ of a sum of reals, where log⁺ is the positive part of the logarithm. There are, however, many ways to say "(Finset|Fintype).sum" in Mathlib, and I do not fully understand their differences and pros/cons. Is there a best practice? A formulation that is the easiest to apply? Any hint is greatly appreciated. @Sébastien Gouëzel @Johan Commelin: You probably have lots of experience with this; I'd love to hear your opinion.

Three formulations come to my mind, but I am sure there will be many others.

theorem Real.logpos_sum₀ {n : ℕ} (f : Fin n → ℝ) :
    log⁺ (∑ t, f t) ≤ log n + ∑ t, log⁺ (f t) := by
  sorry

theorem Real.logpos_sum₁ {α : Type} [Fintype α] (f : α → ℝ) :
    log⁺ (∑ t, f t) ≤ log (Fintype.card α) + ∑ t, log⁺ (f t) := by
  sorry

theorem Real.logpos_sum₂ {α : Type} (s : Finset α) (f : α → ℝ) :
    log⁺ (∑ t ∈ s, f t) ≤ log (s.card) + ∑ t ∈ s, log⁺ (f t) := by
  sorry

[Sébastien Gouëzel]

I would definitely go for the third one, as the other two are particular cases of this one (well, straightforward consequences, rather).

[Stefan Kebekus]

@Sébastien Gouëzel Thanks, I will follow your advice. See you soon on the PR channel :smile:

[Stefan Kebekus]

I guess it is high time I come back to WithTop.toBase that we discussed earlier, here and during the last meeting of the Freiburg Lean User Group. To get the subject off the ground, I have made a draft PR #22821 where you will find the relevant code in Mathlib/Algebra/Order/ToBase.lean [many more simplifier lemmas need to be added. of course]. I guess there will be three main points to discuss:

1. Is my draft PR the start of a reasonable implementation, or should I do something else entirely?
2. What should the method eventually be called?
3. Where should the material eventually be located?

To keep the discussion from getting confused, I would like to suggest concentrating on Question (1) for now and come back to the other questions once this is settled. Would that be ok?

@Johan Commelin @Joachim Breitner @Yaël Dillies (and others) you have so much more experience ... is this a reasonable start?

[Joachim Breitner]

(Thanks for the flattering ping, but I’ll excuse myself from this, I am really not an expert in mathlib api design.)

[Johan Commelin]

To me the design in that PR looks fine. Happy to also hear what @Yaël Dillies thinks.

[Yaël Dillies]

Will look tomorrow

[Stefan Kebekus]

@Johan Commelin @Yaël Dillies Thanks for looking at the PR.I take it from your detailed comments that you feel this is the start of a reasonable implementation. Yaël already suggested a place in math lib where the material could eventually live.

[Stefan Kebekus]

This leaves the question „What should the method be called?“. I suggested WithTop.toBase in analogy to the method ENat.toNat that I have gotten used to. The name is not too long and reasonably descriptive: it maps elements of WithTop BaseType to BaseType in a natural manner.

Other names that came to my mind were WithTop.toBaseType (too long), or yet another variant of WithTop.untopX. I did not favor the last one because I was not able to come up with a letter X that is descriptive and easy to remember (I never understood what the „D“ is for in untopD). A web search suggests that „to untop“ could be understood as „beheadding“.

I am sure you have other suggestions, and I would be glad to hear them!

[Aaron Liu]

Stefan Kebekus said:

(I never understood what the „D“ is for in untopD)

The D is for default, and is used a lot (docs#Option.getD, docs#List.getD, etc.)

[Edward van de Meent]

Stefan Kebekus said:

it maps elements of WithTop BaseType to BaseType in a natural manner.

isn't BaseType a variable here? I don't think it's a good idea to name a method after an arbitrary variable name... we might just as well name it toX, toFoo or toMyFavouriteTypeVariableName (all of which we shouldn't do, imo.)

[Aaron Liu]

How about untop0?

[Yaël Dillies]

Yes, what I personally had in mind was untop₀

[Stefan Kebekus]

Thanks for all your help and to @Aaron Liu for the explanation. I will wait for a little while, at least until this afternoon. If no one speaks up, I will then change the name to untop₀ and change the status from "draft PR" to "PR."

[Stefan Kebekus]

Done. The PR is ready for final review now. Thanks again.