feat(PowerSeries): pentagonal number theorem#33143
feat(PowerSeries): pentagonal number theorem#33143wwylele wants to merge 7 commits intoleanprover-community:masterfrom
Conversation
PR summary 3bad2b8ecdImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 10195 | 12 | backward.isDefEq |
Current commit afdefc7f6d
Reference commit 3bad2b8ecd
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
There was a problem hiding this comment.
Pull request overview
This PR implements the pentagonal number theorem for formal power series. The proof is split into an algebraic part (handling topological rings with summability/multipliability assumptions) and a power series-specific part (proving the necessary summability conditions). The main theorem establishes that the infinite product ∏(1 - x^(n+1)) equals a sum over pentagonal number exponents.
Key changes:
- Adds algebraic infrastructure for the pentagonal number theorem in topological rings
- Proves the complete pentagonal number theorem for formal power series
- Updates the Freek 100 theorem list to reference the new declaration
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 7 comments.
| File | Description |
|---|---|
| docs/1000.yaml | Updates the pentagonal number theorem entry to reference the new proof declaration |
| Mathlib/Topology/Algebra/InfiniteSum/Pentagonal.lean | Proves the algebraic part of the pentagonal number theorem with auxiliary sequences and recurrence relations |
| Mathlib/RingTheory/PowerSeries/Pentagonal.lean | Proves summability conditions and completes the pentagonal number theorem for power series |
| Mathlib.lean | Adds the two new files to the public import list |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
wwylele
force-pushed
the
pentagonal
branch
2 times, most recently
from
9922c13 to
9a5e1a4
Compare
jcommelin
added
the
awaiting-author
|
I rebased the commits to catch up with CI and mathlib version changes. The new code change is still in a separate commit |
github-actions
bot
removed
the
awaiting-author
|
|
||
| set_option backward.isDefEq.respectTransparency false in | ||
| theorem coeff_prod_one_sub_X_eventually_eq_negOnePow (k : ℤ) : | ||
| ∀ᶠ s in atTop, (∏ n ∈ s, (1 - X ^ (n + 1) : R⟦X⟧)).coeff (k * (3 * k - 1) / 2).toNat = |
There was a problem hiding this comment.
Rather than having two theorems, maybe you could define the pentagonal power series as an element of R⟦X⟧ (without topological space assumptions), and compare coefficients directly?
There was a problem hiding this comment.
I tried it in one of my previous version, but it doesn't look pretty. The full formula for the general coefficient would be
coeff n = if "n = (k * (3 * k - 1) / 2) has a solution k" then (-1)^k else 0
and then this generates new design questions, such as whether I should explicitly construct the solution or go with Exists.choose, and this if doesn't look more useful than two separate lemmas.
I honestly don't have much motivation to introduce new nontrivial defs and API for it when this PR is already pretty long (both in line of code and in review time). Maybe next PR?
There was a problem hiding this comment.
Just to show that "next PR" is not an empty promise, I do eventually define the explicit power series at #33157 https://github.com/leanprover-community/mathlib4/pull/33157/changes#diff-dd973108fe721bad60be44e22c7679eb8bb26ad7d0cb9ec57b097d9e8a528255R67-R69 and has a HasProd version there (I still need to remove the T2Space / IsTopologicalRing stuff but the idea is there)
|
|
||
| $$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k - 1)/2} $$ -/ | ||
| theorem tprod_one_sub_X_pow [IsTopologicalRing R] [T2Space R] : | ||
| ∏' n, (1 - X ^ (n + 1)) = ∑' k, (Int.negOnePow k : R⟦X⟧) * X ^ (k * (3 * k - 1) / 2).toNat := by |
There was a problem hiding this comment.
This could also be replaced by an explicit pentagonal power series rather than a tsum.
There was a problem hiding this comment.
(And actually then maybe you could use HasProd to avoid the T2Space issue? And then deduce the tprod version from HasProd.tprod_eq under the T2Space assumption)
There was a problem hiding this comment.
And actually then maybe you could use HasProd to avoid the T2Space issue? And then deduce the tprod version from HasProd.tprod_eq under the T2Space assumption
The current proof structure relies on proving tprod = tsum for arbitrary ring first (which is set up so that the complex version of the theorem can reuse it). If I want to go with direct proof for HasProd first, it needs to
- be specialized to PowerSeries right away (the future complex version has to repeat a lot of proofs)
- likely needs to go through the combinatorics proof. I have a version that went this way but it is pretty cumbersom
So while I agree that a HasProd version without T2Space is possible, I'll likely provide it as a corollary in #33157 instead
The proof is split in two files:
Mathlib/Topology/Algebra/InfiniteSum/Pentagonal.leanfor the algebraic part, andMathlib/RingTheory/PowerSeries/Pentagonal.leanfor the summability part. In the near future, I also plan to prove the real/complex version that branches off from the algebraic part.