Weierstrass M-test

Stream: PrimeNumberTheorem+

[Suryansh Shrivastava]

Does something like the Weierstrass M-test exist in Mathlib?

[Ruben Van de Velde]

(deleted)

[Arend Mellendijk]

There's docs#Summable.of_norm_bounded

[Ruben Van de Velde]

Earlier discussion here on zulip points at !3#11229

[Terence Tao]

Perhaps if you say what you might need the M-test for, we can figure out how to spell a version of it that (a) can be proven from existing Mathlib tools, and (b) would be useful for your application.

[Chris Birkbeck]

There is also https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/FunctionSeries.html#tendstoUniformly_tsum which gives the uniform statement

[Chris Birkbeck]

Although what Ruben points to should be what you want (although it might be stated slightly differently)

[Suryansh Shrivastava]

I was looking for the theorem that all holomorphic functions are analytic in a unit disk(whose proof requires Weistrass M-Test), which now I realize is already in Mathlib (with a different terminology). Isn't defining Entire functions on a complex plane a good idea?

[Sébastien Gouëzel]

We already have that definition, as Differentiable ℂ f. Introducing a definition which is equivalent to this one but with a different name would just force us to restate a bunch of theorems for essentially no gain, which is probably not a good idea. Having documentation explaining that the mathlib spelling for "entire functions on the complex plane" is Differentiable ℂ f would probably be a good idea, though!

[Alex Kontorovich]

What about an abbrev? I find it very convenient to use HolomorphicOn in place of DifferentiableOn ℂ... Would it bother people to add:

abbrev Entire (f : ℂ → E) := Differentiable ℂ f

? (So that, e.g., when someone new to this branch of Mathlib goes looking for facts about entire functions, they find the word they're expecting...?)

[Terence Tao]

Somewhat tangentially, I think it might be a good crowdsourced project to build a table (or maybe a wiki or github repository) of standard mathematical properties and their Lean formalizations. I started a very preliminary version of this at https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=78671819 , but did not have the time to expand it further. Perhaps there is a way to semi-automate such a list with AI? Alternatively if one could somehow attach some discussion page to each Mathlib documentation page, one could perhaps try to put such standard formalizations on that page.

[Alex Kontorovich]

This is great! Maybe a third column can be: what needs to be imported and also opened (scoped, etc) for the notation to work properly?

[Terence Tao]

I've added blank columns for this and also the example of an entire function. If there is interest I can try to set up a publicly editable Google Sheets to try to crowdsource a greatly expanded version of this table, though this is obviously a rather insecure platform and eventually one should use something else (a wiki perhaps?).

[Alex Kontorovich]

Sounds great to me! It certainly would've been very useful to me when I was starting out...

[Terence Tao]

OK, here is a publically editable version: https://docs.google.com/spreadsheets/d/1ap8ByJDvXw9c1G629UxRRoag3gTcMpPsRpm3_yCINyo/edit?usp=sharing . Let's see how it develops...