L-series

Stream: PR reviews

[Michael Stoll]

Starting a new thread here, as the topic line of the previous one does not fit anymore.

I've just opened #11173, which contains some additional API lemmas on (iterated) derivatives and negation. I found these helpful for the further development of L-series in Mathlib.

[David Loeffler]

Michael Stoll said:

I've just opened #11173, which contains some additional API lemmas on (iterated) derivatives and negation. I found these helpful for the further development of L-series in Mathlib.

I left some comments. I note that your lemmas would be far, far easier to prove if you assumed differentiability from the start; is the fact that they apply in the non-differentiable case really crucial in your application?

[Michael Stoll]

Thanks for the comments! I'll look at them in detail later.

I think the general principle is to try to have as weak assumptions as possible (even if this makes the proof more involved), to simplify use. Isn't this also part of the point of having (judicially chosen) "junk values" to make functions total?

[Michael Stoll]

#11189 adds a proof that the harmonic series restricted to a residue class diverges (which I want for the proof that the abscissa of absolute convergence of a Dirichlet L-series is 1).

[David Loeffler]

Hmm, sounds like #11189 might have some overlap with my PR #11150 (a slice of my Hurwitz-zeta-functions project), which shows that ∑' n : ℕ, 1 / (n + a) ^ s, for a a real parameter, converges iff 1 < re s. Taking a = k / m recovers your result. Perhaps we should try to combine the two.

[David Loeffler]

PS: Looking at this again, I had misunderstood what you were doing; I retract the incorrect claim that your results can be derived from mine. I'm not sure there's a natural way of unifying the two PR's (at least, not without making the statements and proofs considerably more complicated). Sorry for the noise!

[Michael Stoll]

New PR #11214; it deals with addition, negation and scalar multiplication of L-series.

[Michael Stoll]

#11245 adds results on differentiability and derivatives of L-series.

[Michael Stoll]

I think #11214 should be OK now. Perhaps it is ready for a maintainer merge?

[Michael Stoll]

#11253 is a small PR that just adds notation.
See EulerProducts/DirichletLSeries (in my repo) for how it is used.

[Michael Stoll]

#11214, #11245 and #11253 could do with some reviews or steps toward merging.

[David Loeffler]

Likewise #11069 and #11150, which are steps towards analytic continuation of Dirichlet L-series.

[Michael Stoll]

It looks like #11150 contains what #11069 does. Is this on purpose?

[Kevin Buzzard]

That's what " depends on: feat(InfiniteSum/NatInt): lemmas on sums over ℤ #11069" in the initial message on #11150 means

[Michael Stoll]

To my naïve eyes, it looks like merging #11150 would also put the changes made in #11069 into Mathlib, and then I wonder why to have this redundancy.
Or rather, I was asking myself whether, say, maintainer merging #11150 would imply the same for #11069.

[Chris Birkbeck]

Isn't it just to split up the PR into smaller bits?

[Michael Stoll]

I guess I just have no idea what the workflow is with dependent PRs. Is this explained somewhere?

[Chris Birkbeck]

#11069 will be PRd first and then #11150 will only be ~100 lines long .

[Michael Stoll]

So one should wait for the dependency to be merged before looking at the dependent PR?

[Chris Birkbeck]

I'm not sure if there is an official explanation. I just know that once you mention it in the PR it'll say "depends on.." until that gets merged. You can also run git merge origin/ other Pr to update the second one if you make any changes to the first (i.e. like changes coming from the pr reviews)

[Chris Birkbeck]

Michael Stoll said:

So one should wait for the dependency to be merged before looking at the dependent PR?

Yes exactly.

[Michael Stoll]

Then why not wait with submitting the dependent PR until this point and have no dependency? I don't quite see what is gained by this mechanism.

[David Loeffler]

Yes, that’s why PRs with the “blocked-by-other-PR” label don’t show up in #queue. Possibly I was a bit trigger-happy in adding the “awaiting-review” label, but your comment on the 2nd PR (“the bits of this that aren’t in the first PR are OK”) is exactly what I was hoping for - thanks!

[Chris Birkbeck]

I don't think it's hugely important (I could be wrong though). I usually just use it to show what's coming next so reviewers can see why I'm PR all this.

[David Loeffler]

Michael Stoll said:

Then why not wait with submitting the dependent PR until this point and have no dependency? I don't quite see what is gained by this mechanism.

Chris’s answer is one good reason. Another is that it leads to a more efficient workflow: we all have many demands in our time, and using PR dependency labels means that review of PR x+1 can start immediately after PR x is merged, rather than waiting for the author to upload it in rigid sequence.

[David Loeffler]

Thus would, incidentally, work much better if bors didn’t squash commit history, because that means one very often has to manually merge reviewer changes into subsequent PRs as the info needed for git to do this for itself has been thrown away.

[Ruben Van de Velde]

The main advantage to having multiple PRs in a chain rather than just one is that smaller PRs are easier to review

[Michael Stoll]

But this is independent of whether all these PRs are open concurrently or submitted sequentially.
What I found irritating is that in the later PR, I also see all the changes made by the previous ones, so that it is a bit hard to figure out what is really teh new part.

[Ruben Van de Velde]

Sure. But if the author opens them concurrently, the reader can decide whether or not to look at them based on the abortion on the PR. If the author keeps their next work in a private branch, the reader doesn't have the choice

[David Loeffler]

Michael: perhaps you might not be aware that there’s an option in the GitHub review screen “Show changes from …” allowing you to select which commits in a branch you see. This is a good way of screening out commits inherited from prerequisite PRs.

[Damiano Testa]

It would be useful if dependent PRs also came with a link that shows the diff between the current version of the "top" PR wrt the "dependent" one.

[David Loeffler]

Damiano Testa said:

It would be useful if dependent PRs also came with a link that shows the diff between the current version of the "top" PR wrt the "dependent" one.

I agree. This would be awkward to implement for PRs with more than one predecessor, but that is probably not a very common case. But this is probably an aspect of GitHub's PR interface which is beyond the control of individual projects.

[Mauricio Collares]

You can make the dependent PR's base branch be the predecessor PR's. Changing base branches is an option on GitHub (but the accompanying rebase is sometimes annoying).

[Yaël Dillies]

Please don't do that. If you do, bors will close the depending PR when the dependency Pr gets merged

[Mauricio Collares]

That's an unfortunate interaction between bors and GitHub. GitHub is supposed to automatically change the target branch when it disappears due to using the "Delete branch" button on a merged PR. But bors doesn't really merge PRs from GitHub's point of view, it just closes them. Hopefully Mergify will be better at this.

[Michael Stoll]

Can #11245 (derivatives of L-series) be maintainer merged now? @David Loeffler

[David Loeffler]

Michael Stoll said:

Can #11245 (derivatives of L-series) be maintainer merged now? David Loeffler

The reason I haven't maintainer-merged this PR is because I'm not 100% convinced about the lemma Complex.isOpen_rightHalfPlane which you are adding; it seems to me that there are other, better formulations and locations for this lemma (and I have suggested some). I'm not going to object if some other reviewer / maintainer comes along and hits merge, but I'm not sufficiently happy with it to take responsibility myself by maintainer-merging.

[Michael Stoll]

I have followed David's suggestion (made in a comment on the PR) to move the lemma in question to a file under Analysis/Complex, change its name (in particular, it now mentions EReal) and add its three siblings.
I hope this is now OK.

[Michael Stoll]

#11634 is the next one. It defines the Dirichlet convolution of two sequences (and introduces notation f ⍟ g for it) and then proves that L (f ⍟ g) = L f * L g when both L-series converge.

[Alex Kontorovich]

Great! What do you think of proving the uniqueness of Dirichlet coefficients? (As discussed, e.g., here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Sum.20over.201.2Fp.20diverges/near/425802703 It follows quite easily from the Perron formula, which itself would be great to get into mathlib...)

[Michael Stoll]

It is here, but done in the more pedestrian direct way, so no Perron formula.
I was planning to PR it eventually; if you want it soon, I can do it earlier.

[Alex Kontorovich]

I'm in no hurry to get this stuff into mathlib... (I'd prefer to first get everything proved formally...)

[Kevin Buzzard]

The longer you don't put something into mathlib, the more painful your local maintenance burden is

[Michael Stoll]

#11712 adds a new file with material on L μ, L χ for Dirichlet characters χ, L 1 = L ζ as a special case, and L Λ. It also adds a lemma to NumberTheory.Divisors (the components of a pair in Nat.divisorsAntidiagonal n are nonzero) and slighlty reorganizes material between Basic and the new file.

[David Loeffler]

One of the new results of this PR is the formula for $\zeta'(s) / \zeta(s)$ using the von Mangoldt function. This is a great thing to have, certainly! But I wonder if it would be better still if we had the more general result for $L'(\phi, s) / L(\phi, s)$ for an arbitrary completely-multiplicative $\phi$ (e.g. a Dirichlet character), and derived the special case of $\phi = 1$ from that. What do you think?

[Michael Stoll]

I'll have a look at that. (Maybe after giving the talk...)

[Michael Stoll]

Now done (for Dirichlet characters; this fits nicely in the context of #11712):

lemma LSeries_twist_vonMangoldt_eq  {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    L (↗χ * ↗Λ) s = - deriv (L ↗χ) s / L ↗χ s := ...

[Alex Kontorovich]

Maybe this is asking too much, but how hard would it be to show this for a general multiplicative (but not necessarily completely multiplicative) series, say, assuming there's an Euler product of degree d? (So we can use it, e.g. once we have L-functions of modular forms, and eventually automorphic reps...?) E.g. (5.25) in Iwaniec-Kowalski? (Feel free to tell me to get lost! You've done plenty!!)

[Michael Stoll]

I can look at this at some point (also maybe first the generalization for arbitrary completely multiplicative functions, which is a bit more complicated than for Dirichlet characters because of convergence questions), but I think this is a bit out of scope for the present PR.

[Michael Stoll]

OK; I think that doing it more generally for completely multiplicative functions will be rather easy. But I would like to defer that refactor (which will then deduce the results for Dirichlet characters from the more general ones) to a follow-up PR, so that #11712 doesn't get even larger.

[David Loeffler]

Sounds sensible to me. I’m not wholly convinced that extending from Dir chars to general completely mult fcns is particularly useful anyway, while weakly mult fcns would bring a whole new set of challenges.

[Michael Stoll]

It certainly doesn't hurt to have a bit more generality, even though DIrichlet characters will certainly be the most important use case, so I think I will do the refactor eventually.
Regarding (weakly) multiplicative functions, what kind of statement would be desired? It is not quite clear to me how to formulate that.

[Michael Stoll]

It would be nice to get some reviews on #11712 ...

[Alex Kontorovich]

Michael Stoll said:

It certainly doesn't hurt to have a bit more generality, even though DIrichlet characters will certainly be the most important use case, so I think I will do the refactor eventually.
Regarding (weakly) multiplicative functions, what kind of statement would be desired? It is not quite clear to me how to formulate that.

I think we want a statement of the following form: Suppose that we have a degree $d$ $L$-series with Euler product $L(s,\pi) = \prod_{j=1}^d\left(1-\alpha_j(p)p^{-s}\right)^{-1}$ converging in some half plane (equivalently, $\alpha_j(p)\ll p^C$ for some $C<\infty$). Then the Dirichlet series of $-L'/L$ has coefficients: $\Lambda_\pi(n)$ supported on prime powers, and taking values:
$\Lambda_\pi(p^k)= \sum_{j=1}^d \alpha_j(p)^k \log p.$
With a little API on log-derivatives (e.g. if $f=\prod f_j$ then $f'/f=\sum f_j'/f_j$ etc), this doesn't seem to me (naively) too far from what you've already done... But again, one PR at a time...

[Michael Stoll]

That should indeed not be too hard. I was thinking of completely general weakly multiplicative functions $f$, and then expressing $\Lambda_f(n)$ in a nice way seems to be hard...

[David Loeffler]

Alex Kontorovich said:

I think we want a statement of the following form: Suppose that we have a degree $d$ $L$-series with Euler product $L(s,\pi) = \prod_{j=1}^d\left(1-\alpha_j(p)p^{-s}\right)^{-1}$ converging in some half plane [...]

I think we're still quite far away from having any nontrivial examples with $d > 1$ though, aren't we?

[Alex Kontorovich]

Michael Stoll said:

That should indeed not be too hard. I was thinking of completely general weakly multiplicative functions $f$, and then expressing $\Lambda_f(n)$ in a nice way seems to be hard...

Oh yes, that would be annoying... If it's just multiplicative, but without a Hecke relation (equivalently, finite degree Euler product), you have to battle with horrible infinite sums, I agree. (And it's likely pointless; I've never seen an L-function that I care about that has an Euler product but not Hecke...

[Alex Kontorovich]

David Loeffler said:

Alex Kontorovich said:

I think we want a statement of the following form: Suppose that we have a degree $d$ $L$-series with Euler product $L(s,\pi) = \prod_{j=1}^d\left(1-\alpha_j(p)p^{-s}\right)^{-1}$ converging in some half plane [...]

I think we're still quite far away from having any nontrivial examples with $d > 1$ though, aren't we?

Hmm aren't we getting some modular forms soon (if not already)? Once we have Ramanujan discriminant (and Hecke operators), we could show that its L-function is degree 2...

[David Loeffler]

The big holdup is proving that the spaces have the correct dimension.

[David Loeffler]

Without that it's pretty hard to show that $\Delta$ (or anything else) is an eigenform.

[Alex Kontorovich]

Agreed. I'm guessing that's because we're trying to do it in general... (for $\Delta$ one can do it "by hand" pretty easily...)

[David Loeffler]

Can one "do" $\Delta$ pretty easily? How? I am surprised by this assertion.

[Alex Kontorovich]

Actually for any weight full level it's really not hard to show that $E_4$ and $E_6$ span the ring

[David Loeffler]

How?

[Alex Kontorovich]

There's an elementary argument, e.g., in Bump "Automorphic Forms and Representations", Ch 1.3 (using the structure of the fundamental domain for $SL(2,Z)$, which we have...)

[David Loeffler]

Prop 1.3.1 of Bump looks highly non-elementary to me...

[David Loeffler]

The minimum input needed to get Bump's argument to work seems to be that a modular form of weight 0 is constant. This is one of the many things customarily proved using the valence formula. Bump refers to an alternative proof via the maximum modulus principle, without giving any details; this sounds more accessible than the valence-formula proof, but not totally straightforward either.

[Alex Kontorovich]

Yeah, don't we have Liouville? I would think that's "all" (as always, with a big grain of salt...) one would need to get max modulus working...

[Chris Birkbeck]

I'm more motivated by trying get the valence formula by using the stuff they did in Isabelle/HOL to get the the contour integrals working, than just trying to get $\Delta$ working.

[Chris Birkbeck]

That said, I don't know this argument in Bump, so if its actually simple then we could try it.

[Michael Stoll]

Michael Stoll said:

It would be nice to get some reviews on #11712 ...

Anyone?

[Michael Stoll]

I think #11712 should be good to be merged now. (I have used #11770 to golf one proof as suggested and added one more lemma that simplifies two other proofs).

[Michael Stoll]

@David Loeffler @Ruben Van de Velde @Chris Birkbeck Is there anything else to be done with #11712?
If not, maybe somebody can maintainer merge?

[Chris Birkbeck]

I think it looks good!

[David Loeffler]

I've made one very minor stylistic suggestion. Apologies for not getting to this earlier, was otherwise occupied all day today (probably my last skiing day of the season! :skier:)

[Michael Stoll]

I hope you had fun!

[Michael Stoll]

#12055 is a first step towards refactoring Euler products in terms of tprod. It adds a more general version factoredNumbers s (where s is a Finset of natural numbers) of smoothNumbers n, which denotes the set of all positive natural numbers all of whose prime factors are in s, provides API for it, golfs most of the proofs for smoothNumbers by reducing to the new API, and also speeds up the NumberTheory.SmoothNumbers file by replacing a few slow converts and tautos by faster proof steps.

Reviews welcome (should be fairly easy)!

[Michael Stoll]

Is there more to be done with #12055 ?

[Michael Stoll]

#12161 is the first part of refactoring Euler products in terms of HasProd and tprod. It also speeds up the file by removing slow converts and adding local shortcut instances. The diff looks larger than it really is...

[Michael Stoll]

#12809 is a follow-up; it updates NumberTheory.EulerProduct.DirichletLSeries with statements using infinite products (and in terms of L-series notation).

[Michael Stoll]

Alex Kontorovich said:

Great! What do you think of proving the uniqueness of Dirichlet coefficients? (As discussed, e.g., here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Sum.20over.201.2Fp.20diverges/near/425802703 It follows quite easily from the Perron formula, which itself would be great to get into mathlib...)

Michael Stoll said:

It is here, but done in the more pedestrian direct way, so no Perron formula.
I was planning to PR it eventually; if you want it soon, I can do it earlier.

This is now #20370.