feat (NumberTheory/LSeries): Hurwitz zeta

[loefflerd]

Add the Hurwitz zeta function (defined as the sum of its even and odd parts, which were already defined in previous PR's).

---

[faenuccio]

LGTM!

[loefflerd]

Thanks for the review, Filippo! I have applied your changes. I also fixed a minor formatting glitch in the module docstring, and added a mssing lemma LSeriesHasSum_exp that makes the link with Michael's LSeries API.

[faenuccio]

Thanks for the review, Filippo! I have applied your changes. I also fixed a minor formatting glitch in the module docstring, and added a mssing lemma LSeriesHasSum_exp that makes the link with Michael's LSeries API.

Great!

[MichaelStollBayreuth]

Some of the ring_nfs were a bit slow because of the fairly involved expressions occurring. Abstracting the relevant atoms via generalize gives a noticeable speed-up.

[loefflerd]

Hi Michael,

Thanks for the suggestions! I'm in two minds about this sort of thing (trading off concision / elegance vs. speed). CPU cycles are cheap, after all; and there is the very good point raised in the Zulip discussion "To automate or not not automate?", that making explicit workarounds for slow tactics makes it less likely that tactic-development people will notice and work on the slowness.

Hence I've put in your generalize changes, but with a comment pointing out that it would be nice if ring_nf could do these things automatically. Are you happy with that compromise?

Regards, David

[MichaelStollBayreuth]

I do understand that (and my suggestions were meant as such, not as requirements). I think the compromise (adding comments) is reasonable. Of course, a better solution would be to make ring_nf faster (along similar lines, if at all possible), but this is beyond my paygrade...

[MichaelStollBayreuth]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style