Pentagonal number theorem: statement & plan

Stream: mathlib4

[Beibei Xiong]

I’d like to align on the statement and upstream plan for the formalization of the pentagonal number theorem.

Related PR: #31362
Related repo (wwylele @Weiyi Wang ): https://github.com/wwylele/PentagonalNumberTheorem

Points I’d like to confirm:

1. For the first Mathlib PR, can we take the main statement to be the PowerSeries expansion over ℤ, together with a finite cut-off product, to avoid convergence/topology issues, and derive the “summed over ℕ / ℂ” formulations later as corollaries?

2. Is there any preference on namespace or file placement to avoid clashes (e.g. something like Nat.Partition.Pentagonal)?

3. Should error_term_e be postponed for now, or should we require a well-definedness lemma (or alternatively switch to the quadratic-solve approach)?

I’m happy to adapt to other suggestions as well.

[Aaron Liu]

looks like you have a lot of good results in here but I don't see the identity of formal power series

[Weiyi Wang]

For the first point, I believe mathlib has already handled all topology problems for you, and what's left to prove is mostly algebraic. My repo has demonstrated this. For upstreaming to Mathlib, I don't think we should repeat the machinery about going from finite to infinite. Of course, you should feel free to do so for your own practice

[Nick_adfor]

Where does the new work on the pentagonal number theorem published?