Pentagonal number theorem, but ugly

Stream: general

[Weiyi Wang]

This is showcasing another adventure of mine finding and proving random theorems on the 1000+ theorem list, the pentagonal number theorem

https://github.com/wwylele/PentagonalNumberTheorem/blob/master/PentagonalNumber/Basic.lean#L2071

I didn't expect how messy it turned out to be. At first I thought, surely it won't be hard if the wikipedia page itself contains a proof, right? It turns out visual proofs are the worst kind to formalize. Things that are obvious in the diagram become nightmare in the code.

I suppose there is no way to get this whole thing in mathlib in the current form, but I think there are some good utility lemma that I can extract and contribute

[Bhavik Mehta]

Nice!! Some of these lemmas definitely should be in mathlib if they're not already, on a speedy glance through I noticed

theorem PowerSeries.monomil_mul_monomial {R : Type*} [Semiring R] (m n : ℕ) (a b : R) :
    monomial R m a * monomial R n b = monomial R (m + n) (a * b) := by
  unfold monomial
  convert MvPowerSeries.monomial_mul_monomial (Finsupp.single () m) (Finsupp.single () n) a b
  simp

theorem PowerSeries.prod_monomial {R : Type*} [CommRing R] {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (f : ι → ℕ) (g : ι → R) :
    ∏ i ∈ s, monomial R (f i) (g i) =
    monomial R (∑ i ∈ s, f i) (∏ i ∈ s, g i) := by
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha h =>
    simp [ha, h, monomil_mul_monomial]

which should definitely be in mathlib

[Ruben Van de Velde]

By the way, you're welcome to add your formalization to 1000.yaml already

[Weiyi Wang]

Thanks! I'll spend sometime cleaning up and PR a few lemmas before adding it to 1000.yaml

[Weiyi Wang]

:thinking: hmm, before I add mine to 1000.yaml, I wanted to also prove the complex power series form (it is on the wikipedia page after all!). I thought it would be easy to turn a PowerSeries to a tsum of complex expressions, but it turned out not that simple??

The only thing that looks related is PowerSeries.eval₂ and friends, but it already looks weird and I don't know if it is doing the thing I wanted...

• PowerSeries.HasEval talks about if x ^ n converges to 0 without mentioning of the coefficients. This is as if stating the radius of convergent is always 1, but that doesn't make sense
• The seemingly friendlier form PowerSeries.eval₂Hom doesn't allow me to evaluate to a complex number because of non-existence IsLinearTopology \C \C. I don't quite understand what IsLinearTopology is doing and it seems that there is almost no instance for this class in mathlib?

[Weiyi Wang]

Oh btw, #28720 is the PR for the monomial lemmas

[Weiyi Wang]

After searching some Zulip history, I think what I wanted was to cross the missing bridge between PowerSeries and FormalMultilinearSeries. :smiling_face_with_tear:

[Yaël Dillies]

@Paul Lezeau and @Xavier Généreux and others recently tried to cross that bridge at the CFT workshop.

[Paul Lezeau]

And will be PRing this stuff soon :)

[Kevin Buzzard]

docs#IsLinearTopology

[Kevin Buzzard]

Oh this is about convergence in the nonarchimedean setting, this has nothing to do with convergence of sums of complex numbers

[Weiyi Wang]

Ah, now that makes sense, and the HasEval condition reads like the convergent condition for p-adic series I remembered. I guess the plan is to give IsLinearTopology to, say, p-adic numbers, but it hasn't been implemented yet?

[Kevin Buzzard]

$\mathbb{Q}_p$ has a $\Z_p$-linear topology but you're right, this doesn't seem to be there.

[Yakov Pechersky]

There is a PR for Z_p, #24627

[Patrick Massot]

Kevin Buzzard said:

docs#IsLinearTopology

The docstring misses a word. I know I should fix it instead of writing this. But I'm on my phone about to board a plane from Hangzhou to Hanoi so I fear I will forget to do it.

[Aaron Liu]

Which word is missing where?

[Patrick Massot]

"Typically one would also that the topology is invariant by translation" should be "Typically one would also require that the topology is invariant by translation" for instance. And the plane is moving so I'll switch off internet now.

[Weiyi Wang]

So I am working on upstreaming stuff that I think should be mathlib. Here are some easy ones #28861 #28860

Should we also have definitions of generating functions of various partition functions in mathlib? Currently there are some in https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean, but they are only stated as truncated finite product (presumably because at that time the topology hadn't been defined)

(Maybe I should move this to #mathlib4 ?)

[Bhavik Mehta]

Weiyi Wang said:

Currently there are some in https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean, but they are only stated as truncated finite product (presumably because at that time the topology hadn't been defined)

Yes, this is exactly correct; there's TODOs in that file to "upgrade" the definitions and proofs to use the full generating function instead of just a finite truncation

[Weiyi Wang]

Update: it is no longer ugly after I tried a different approach :grinning_face_with_smiling_eyes: . I have also got both power series version and complex number version. https://wwylele.github.io/PentagonalNumberTheorem/docs/PentagonalNumber.html
It is only a small project, but I am really having fun not only proving theorems, but also playing around docgen and other tools.