[Merged by Bors] - feat(Combinatorics): Glaisher's theorem by wwylele · Pull Request #30618 · leanprover-community/mathlib4

wwylele · 2025-10-16T21:05:10Z

This proves Glaisher's theorem, one of the 1000+ theorems. It is also a generalization of Euler's partition theorem, which can be rewritten as a collorary of this (will be in a different PR)

depends on: [Merged by Bors] - feat(RingTheory): geometric series of (Mv)PowerSeries #30599
depends on [Merged by Bors] - feat(Combinatorics): generating function for partitions #30567

github-actions · 2025-10-16T21:06:29Z

PR summary be5e7c6163

Import changes for modified files

No significant changes to the import graph
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.Enumerative.Partition.Glaisher` (new file)	1165

Declarations diff

+ card_restricted_eq_card_countRestricted
+ countRestricted
+ hasProd_powerSeriesMk_card_countRestricted
+ hasProd_powerSeriesMk_card_restricted
+ multipliable_one_sub_X_pow
+ multipliable_powerSeriesMk_card_countRestricted
+ multipliable_powerSeriesMk_card_restricted
+ powerSeriesMk_card_countRestricted_eq_tprod
+ powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted
+ powerSeriesMk_card_restricted_eq_tprod
+ restricted
+ tendsto_order_genFun_term_atTop_nhds_top
+ tprod_one_sub_X_pow_ne_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib4-dependent-issues-bot · 2025-11-09T14:34:23Z

This PR/issue depends on:

~~[Merged by Bors] - feat(RingTheory): geometric series of (Mv)PowerSeries #30599~~
By Dependent Issues (🤖). Happy coding!

wwylele · 2025-11-15T23:09:43Z

This is now ready for review

mathlib4-merge-conflict-bot · 2025-11-19T08:16:19Z

This pull request has conflicts, please merge master and resolve them.

b-mehta

This looks good to me, but I'd like to hear @AntoineChambert-Loir's opinion on the two new power series lemmas. I think they're useful special cases of PowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, and so should be included in the same way we have "specific limits" and "special functions" in mathlib; but it may be that there's a more useful version I'm not currently seeing.

AntoineChambert-Loir · 2025-11-25T09:19:05Z

+
+@[expose] public section
+
+variable (R) [TopologicalSpace R] [T2Space R]


The results here should not depend on the choice of a topological structure on R, nor that it is T2.

For theorems that doesn't use topology in the statement (powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted and card_restricted_eq_card_countRestricted), I dropped [TopologicalSpace R] from them. All other intermediate lemmas uses the topology in the statement for the infinite sum (and T2 to ensure the sum is unique).

I can change the entire file to just use discrete topology, but isn't it weaker than what it is written here? Having [TopologicalSpace R] as the theorem input precisely means "the results are independent on the choice of a topological structure, and it is true for any structure"

Yes, but the user will have to provide a structure of a topological space to apply the result.

Yes, but then the user can just provide discrete topology. This provide the user the options to use different topology if they already have one in their context.

AntoineChambert-Loir · 2025-11-25T09:19:45Z

+$$
+\prod_{i \mem p} \sum_{j = 0}^{\infty} X^{ij}
+$$ -/
+theorem hasProd_powerSeriesMk_card_restricted [IsTopologicalSemiring R]


I would like that the mention to the topological structure be erased from the statement. You can endow R with the discrete structure in the proof if needed.

See the same comment above why I think that would make the lemma weaker

AntoineChambert-Loir · 2025-11-25T09:21:06Z

+\prod_{i = 1}^{\infty} \sum_{j = 0}^{m - 1} X^{ij}
+$$ -/
+theorem hasProd_powerSeriesMk_card_countRestricted {m : ℕ} (hm : 0 < m) :
+    HasProd (fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j))


Before stating HasProd, which relies on some topology, you could state the algebraic property that implies the existence of this product (this stuff minus one has order going to infinity).

This is proved as a direct consequence of hasProd_genFun instead of arguing about the order directly (which was done inside hasProd_genFun). I don't think I should restate the argument about the order

I think making the order statement about genFun would make sense then

@b-mehta the problem is that hasProd_genFun was not proved using the fact about the order either, but it was proved by directly comparing the coefficients at the limit between LHS and RHS, and I am pretty sure it is shorter that way. Do I still need to state the fact about the order separately? It don't find any value in it

The value, again, is that the result can be used without reference to a topology on the ring. docs#MvPowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top will show the relation, and I am surprised not to find the converse when the topology is discrete. But that means you are not forced to change your proof.

The usage of WithPiTopology.summable_of_tendsto_order_atTop_nhds_top in summable_genFun_term is to show the inner infinite summation makes sense, but the proof of the outer product doesn't use argument about the order. As for application in countRestricted, the inner summation collapse to a finite one so no need to prove the summability any more. Though, for hasProd_powerSeriesMk_card_restricted, the inner summation is still infinite, so I can see the argument of giving the direct statement about the order there.

In any case, if you feel strongly about it, I can add all the facts about order. I just want to clarify how the order argument is used

I feel indeed strongly about it, and maybe I shouldn't. To give an analogy (and it is more than that), this PR defines a constant as a function of an additional parameter — on which it does not depend. (This would be off topic, but there exist power series with rational coefficients that converge both in C and Q_5, to different elements, and one should be able to arrange that their limits are distinct rational numbers.)

So I started adding lemma about the order of involved power series. Here is some additional thoughts

tendsto_order_genFun_term_atTop_nhds_top for summation in the genFun. Added without problem in the last commit

order argument for the multiplication in genFun. The statement would look like

theorem tendsto_order_genFun_atTop_nhds_top (f : ℕ → ℕ → R) : Tendsto (fun i ↦ (∑' j, f (i + 1) (j + 1) • (X : R⟦X⟧) ^ ((i + 1) * (j + 1))).order) atTop (nhds ⊤) := by sorry

But this has a few issues

To even state it, it already has ∑' inside and thus require topology, nullifying the goal to state only about algebra

Naturally it needs some lemma about PowerSeries.order and tsum. Do I need to create another dependent PR, even though this just goes unused by the main theorem here? Can I do that later?

The specialized version of the summation for Partition.restrict would be just that fun j ↦ X ^ ((i + 1) * j) increases in order, but this looks too trivial to be a lemma (and again, it is unused)

Another possible lemma is for the multipliability related to hasProd_powerSeriesMk_card_countRestricted, which doesn't involve infinite sum and is indeed purely algebraic. However, the hypothetical lemma

theorem tendsto_order_sum_X_pow_sub_one_atTop_nhds_top (m : ℕ) : Filter.Tendsto (fun i ↦ ((∑ j ∈ range m, (X : R⟦X⟧) ^ ((i + 1) * j)) - (1 : R⟦X⟧)).order) Filter.atTop (nhds ⊤)

doesn't type check, because the entire section has been in Semiring R, and there is no subtraction. I could either make this specifically for Ring R, or just remove the first term from the sum so it is (fun i ↦ ((∑ j ∈ Finset.Ico 1 m, (X : R⟦X⟧) ^ ((i + 1) * j))).order), but now it loses the connection with hasProd_powerSeriesMk_card_countRestricted and just be there for no reason.

I see your points and I believe they beat mine.
Ad 1. OK
Ad 2. I have no clear answer to propose.
Ad 3. Another possibility would be to define a variant of order that doesn't look at the initial term, etc., but while this may be interesting in the long range, this would be useless work for here only.

AntoineChambert-Loir · 2025-11-25T09:21:14Z

+  · simp_rw [genFun, countRestricted, card_filter, Finsupp.prod, prod_boole]
+    simp
+
+theorem multipliable_powerSeriesMk_card_countRestricted (m : ℕ) :


Same remark.

AntoineChambert-Loir · 2025-11-25T09:21:54Z

+section Ring
+variable [CommRing R] [NoZeroDivisors R]
+
+private theorem aux_mul_one_sub_X_pow [IsTopologicalRing R] {m : ℕ} (hm : 0 < m) :


again, I am not sure the topological structure is used here.

wwylele · 2025-12-01T21:03:15Z

Hi @AntoineChambert-Loir and @b-mehta, sorry that I didn't agree with the last batch of comment. They seems to contradict to advice I received (do the more general version of the theorem; only include essential code change in PR to make it easier to review). But I don't have strong opinion on them and am ok to accept them if you feel strongly about them. Please let me know if I should make the change anyway.

AntoineChambert-Loir · 2025-12-05T16:05:39Z

To conclude here, LGTM. The points I wanted to make are not worth the API that would be necessary to implement them. The solution to require the user to add some topology (even if it is less needed than what it looks) is clearly simpler.

jcommelin

Thanks 🎉

bors merge

This proves Glaisher's theorem, one of the 1000+ theorems. It is also a generalization of [Euler's partition theorem](https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean), which can be rewritten as a collorary of this (will be in a different PR)

mathlib-bors · 2025-12-05T17:27:19Z

Pull request successfully merged into master.

Build succeeded:

wwylele force-pushed the glaisher branch from c0887c5 to 9893f1c Compare October 16, 2025 21:11

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 16, 2025

wwylele force-pushed the glaisher branch from 9893f1c to 3eed349 Compare October 16, 2025 22:13

wwylele added the t-combinatorics Combinatorics label Oct 18, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 9, 2025

wwylele force-pushed the glaisher branch 3 times, most recently from 557b7de to 8998668 Compare November 15, 2025 22:43

wwylele added WIP Work in progress and removed WIP Work in progress labels Nov 15, 2025

leanprover-community-bot-assistant assigned b-mehta Nov 19, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

feat(Combinatorics): Glaisher's theorem

068d58f

wwylele force-pushed the glaisher branch from 8998668 to 068d58f Compare November 19, 2025 14:13

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

b-mehta reviewed Nov 19, 2025

View reviewed changes

address comments

da70fd6

b-mehta reviewed Nov 19, 2025

View reviewed changes

wwylele mentioned this pull request Nov 21, 2025

[Merged by Bors] - refactor: re-prove Euler's partition theorem from Glaisher's theorem #31873

Closed

1 task

wwylele requested a review from AntoineChambert-Loir November 24, 2025 21:49

AntoineChambert-Loir reviewed Nov 25, 2025

View reviewed changes

Comment thread Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

AntoineChambert-Loir reviewed Nov 25, 2025

View reviewed changes

wwylele requested a review from b-mehta November 27, 2025 01:33

add order lemma

6d39166

jcommelin reviewed Dec 5, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Dec 5, 2025

mathlib-bors bot changed the title ~~feat(Combinatorics): Glaisher's theorem~~ [Merged by Bors] - feat(Combinatorics): Glaisher's theorem Dec 5, 2025

mathlib-bors bot closed this Dec 5, 2025

b-mehta mentioned this pull request Mar 6, 2026

[Merged by Bors] - feat(NumberTheory/ArithmeticFunction/LFunction): formal Euler products of Dirichlet series #36192

Closed


		@[expose] public section

		variable (R) [TopologicalSpace R] [T2Space R]

Conversation

wwylele commented Oct 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary be5e7c6163

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Nov 9, 2025

Uh oh!

wwylele commented Nov 15, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele Dec 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele Dec 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele Dec 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele commented Dec 1, 2025

Uh oh!

AntoineChambert-Loir commented Dec 5, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Dec 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

wwylele commented Oct 16, 2025 •

edited

Loading

github-actions bot commented Oct 16, 2025 •

edited

Loading

wwylele Dec 1, 2025 •

edited

Loading

wwylele Dec 2, 2025 •

edited

Loading

wwylele Dec 2, 2025 •

edited

Loading