feat(Combinatorics): Glaisher's theorem (#30618)

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)

Author: wwylele

Archive/Wiedijk100Theorems/Partition.lean

@@ -269,7 +269,7 @@ theorem partialOddGF_prop [Field α] (n m : ℕ) :
 /-- If m is big enough, the partial product's coefficient counts the number of odd partitions -/
 theorem oddGF_prop [Field α] (n m : ℕ) (h : n < m * 2) :
     #(Nat.Partition.odds n) = coeff n (partialOddGF α m) := by
-  rw [← partialOddGF_prop, Nat.Partition.odds]
+  rw [← partialOddGF_prop, Nat.Partition.odds, Nat.Partition.restricted]
   congr with p
   apply forall₂_congr
   intro i hi

Mathlib.lean

@@ -3150,6 +3150,7 @@ public import Mathlib.Combinatorics.Enumerative.InclusionExclusion
 public import Mathlib.Combinatorics.Enumerative.Partition
 public import Mathlib.Combinatorics.Enumerative.Partition.Basic
 public import Mathlib.Combinatorics.Enumerative.Partition.GenFun
+public import Mathlib.Combinatorics.Enumerative.Partition.Glaisher
 public import Mathlib.Combinatorics.Enumerative.Stirling
 public import Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
 public import Mathlib.Combinatorics.Graph.Basic

Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

@@ -205,16 +205,23 @@ partitions.
 instance (n : ℕ) : Fintype (Partition n) :=
   Fintype.ofSurjective (ofComposition n) ofComposition_surj
 
+/-- The finset of those partitions in which every part satisfies a certain condition. -/
+def restricted (n : ℕ) (p : ℕ → Prop) [DecidablePred p] : Finset n.Partition :=
+  Finset.univ.filter fun x ↦ ∀ i ∈ x.parts, p i
+
+/-- The finset of those partitions in which every part is used less than `m` times. -/
+def countRestricted (n : ℕ) (m : ℕ) : Finset n.Partition :=
+  Finset.univ.filter fun x ↦ ∀ i ∈ x.parts, x.parts.count i < m
+
 /-- The finset of those partitions in which every part is odd. -/
-def odds (n : ℕ) : Finset (Partition n) :=
-  Finset.univ.filter fun c => ∀ i ∈ c.parts, ¬Even i
+def odds (n : ℕ) : Finset n.Partition := restricted n (¬ Even ·)
 
 /-- The finset of those partitions in which each part is used at most once. -/
-def distincts (n : ℕ) : Finset (Partition n) :=
+def distincts (n : ℕ) : Finset n.Partition :=
   Finset.univ.filter fun c => c.parts.Nodup
 
 /-- The finset of those partitions in which every part is odd and used at most once. -/
-def oddDistincts (n : ℕ) : Finset (Partition n) :=
+def oddDistincts (n : ℕ) : Finset n.Partition :=
   odds n ∩ distincts n
 
 end Partition

Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean

@@ -22,12 +22,16 @@ We give the definition `Nat.Partition.genFun` using the first equation, and prov
 equation in `Nat.Partition.hasProd_genFun` (with shifted indices).
 
 This generating function can be specialized to
-* When $f(i, c) = 1$, this is the generating function for partition function $p(n)$.
+* When $f(i, c) = 1$, this is the generating function for partition function $p(n)$
+  (TODO: prove this).
 * When $f(i, 1) = 1$ and $f(i, c) = 0$ for $c > 1$, this is the generating function for
-    `#(Nat.Partition.distincts n)`.
+  `#(Nat.Partition.distincts n)`. More generally, setting $f(i, c) = 1$ only for $c < m$ gives
+  the generating function for `#(Nat.Partition.countRestricted n m)`.
+  (See `Nat.Partition.hasProd_powerSeriesMk_card_countRestricted`).
 * When $f(i, c) = 1$ for odd $i$ and $f(i, c) = 0$ for even $i$, this is the generating function for
-    `#(Nat.Partition.odds n)`.
-(TODO: prove these)
+  `#(Nat.Partition.odds n)`. More generally, setting $f(i, c) = 1$ only for $i$ satisfying certain
+  `p : Prop` gives the generating function for `#(Nat.Partition.restricted n p)`.
+  (See `Nat.Partition.hasProd_powerSeriesMk_card_restricted`)
 
 The definition of `Nat.Partition.genFun` ignores the value of $f(0, c)$ and $f(i, 0)$. The formula
 can be interpreted as assuming $f(i, 0) = 1$ and $f(0, c) = 0$ for $c \ne 0$. In theory we could
@@ -57,21 +61,27 @@ lemma coeff_genFun (f : ℕ → ℕ → R) (n : ℕ) :
     (genFun f).coeff n = ∑ p : n.Partition, p.parts.toFinsupp.prod f :=
   PowerSeries.coeff_mk _ _
 
-variable [TopologicalSpace R]
-
-/-- The infinite sum in the formula `Nat.Partition.hasProd_genFun` always converges. -/
-theorem summable_genFun_term (f : ℕ → ℕ → R) (i : ℕ) :
-    Summable fun j ↦ f (i + 1) (j + 1) • (X : R⟦X⟧) ^ ((i + 1) * (j + 1)) := by
-  nontriviality R
-  apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top
+/-- The summands in the formula `Nat.Partition.hasProd_genFun` tends to infinity in their order. -/
+theorem tendsto_order_genFun_term_atTop_nhds_top (f : ℕ → ℕ → R) (i : ℕ) :
+    Filter.Tendsto (fun j ↦ (f (i + 1) (j + 1) • (X : R⟦X⟧) ^ ((i + 1) * (j + 1))).order)
+    Filter.atTop (nhds ⊤) := by
   refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)
   intro m hm
   grw [PowerSeries.smul_eq_C_mul, ← le_order_mul]
   refine lt_add_of_nonneg_of_lt (by simp) ?_
+  nontriviality R using Subsingleton.eq_zero
   rw [order_X_pow]
   norm_cast
   grind
 
+variable [TopologicalSpace R]
+
+/-- The infinite sum in the formula `Nat.Partition.hasProd_genFun` always converges. -/
+theorem summable_genFun_term (f : ℕ → ℕ → R) (i : ℕ) :
+    Summable fun j ↦ f (i + 1) (j + 1) • (X : R⟦X⟧) ^ ((i + 1) * (j + 1)) := by
+  apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top
+  apply tendsto_order_genFun_term_atTop_nhds_top
+
 /-- Alternative form of `summable_genFun_term` that unshifts the first index. -/
 theorem summable_genFun_term' (f : ℕ → ℕ → R) {i : ℕ} (hi : i ≠ 0) :
     Summable fun j ↦ f i (j + 1) • (X : R⟦X⟧) ^ (i * (j + 1)) := by

Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2025 Weiyi Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Weiyi Wang
+-/
+module
+
+public import Mathlib.Combinatorics.Enumerative.Partition.GenFun
+public import Mathlib.RingTheory.PowerSeries.NoZeroDivisors
+
+/-!
+# Glaisher's theorem
+
+This file proves Glaisher's theorem: the number of partitions of an integer $n$ into parts not
+divisible by $d$ is equal to the number of partitions in which no part is repeated $d$ or more
+times.
+
+## Main declarations
+* `Nat.Partition.card_restricted_eq_card_countRestricted`: Glaisher's theorem.
+
+## References
+https://en.wikipedia.org/wiki/Glaisher%27s_theorem
+-/
+
+@[expose] public section
+
+variable (R) [TopologicalSpace R] [T2Space R]
+
+namespace Nat.Partition
+open PowerSeries PowerSeries.WithPiTopology Finset
+
+section Semiring
+variable [CommSemiring R]
+
+/-- The generating function of `Nat.Partition.restricted n p` is
+$$
+\prod_{i \mem p} \sum_{j = 0}^{\infty} X^{ij}
+$$ -/
+theorem hasProd_powerSeriesMk_card_restricted [IsTopologicalSemiring R]
+    (p : ℕ → Prop) [DecidablePred p] :
+    HasProd (fun i ↦ if p (i + 1) then ∑' j : ℕ, X ^ ((i + 1) * j) else 1)
+    (PowerSeries.mk fun n ↦ (#(restricted n p) : R)) := by
+  convert hasProd_genFun (fun i c ↦ if p i then (1 : R) else 0) using 1
+  · ext1 i
+    split_ifs
+    · rw [tsum_eq_zero_add' ?_]
+      · simp
+      simp_rw [pow_mul, pow_add]
+      apply Summable.mul_right
+      exact summable_pow_of_constantCoeff_eq_zero (by simp)
+    · simp
+  · simp_rw [genFun, restricted, card_filter, Finsupp.prod, prod_boole]
+    simp
+
+theorem multipliable_powerSeriesMk_card_restricted [IsTopologicalSemiring R]
+    (p : ℕ → Prop) [DecidablePred p] :
+    Multipliable (fun i ↦ if p (i + 1) then ∑' j : ℕ, (X ^ ((i + 1) * j) : R⟦X⟧) else 1) :=
+  (hasProd_powerSeriesMk_card_restricted R p).multipliable
+
+theorem powerSeriesMk_card_restricted_eq_tprod [IsTopologicalSemiring R]
+    (p : ℕ → Prop) [DecidablePred p] :
+    PowerSeries.mk (fun n ↦ (#(restricted n p) : R)) =
+    ∏' i, if p (i + 1) then ∑' j : ℕ, X ^ ((i + 1) * j) else 1 :=
+  (hasProd_powerSeriesMk_card_restricted R p).tprod_eq.symm
+
+/-- The generating function of `Nat.Partition.countRestricted n m` is
+$$
+\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))
+    (PowerSeries.mk fun n ↦ (#(countRestricted n m) : R)) := by
+  nontriviality R using Subsingleton.eq_one
+  convert hasProd_genFun (fun i c ↦ if c < m then (1 : R) else 0) using 1
+  · ext1 i
+    rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range]
+    congrm $(by simp) + ?_
+    trans ∑ k ∈ range (m - 1), (if k + 1 < m then (1 : R) else 0) • X ^ ((i + 1) * (k + 1))
+    · refine sum_congr rfl fun b hn ↦ ?_
+      rw [add_comm 1 b]
+      have : b + 1 < m := by grind
+      simp [this]
+    · exact (tsum_eq_sum (fun b hb ↦ smul_eq_zero_of_left (by simpa using hb) _)).symm
+  · simp_rw [genFun, countRestricted, card_filter, Finsupp.prod, prod_boole]
+    simp
+
+theorem multipliable_powerSeriesMk_card_countRestricted (m : ℕ) :
+    Multipliable fun i ↦ ∑ j ∈ range m, (X ^ ((i + 1) * j) : R⟦X⟧) := by
+  rcases Nat.eq_zero_or_pos m with rfl | hm
+  · simpa using multipliable_of_exists_eq_zero ⟨0, rfl⟩
+  · exact (hasProd_powerSeriesMk_card_countRestricted R hm).multipliable
+
+theorem powerSeriesMk_card_countRestricted_eq_tprod {m : ℕ} (hm : 0 < m) :
+    PowerSeries.mk (fun n ↦ (#(countRestricted n m) : R)) =
+    ∏' i, ∑ j ∈ range m, X ^ ((i + 1) * j) :=
+  (hasProd_powerSeriesMk_card_countRestricted R hm).tprod_eq.symm
+
+end Semiring
+
+section Ring
+variable [CommRing R] [NoZeroDivisors R]
+
+private theorem aux_mul_one_sub_X_pow [IsTopologicalRing R] {m : ℕ} (hm : 0 < m) :
+    (∏' i, if ¬m ∣ i + 1 then ∑' j, (X : R⟦X⟧) ^ ((i + 1) * j) else 1) * ∏' i, (1 - X ^ (i + 1)) =
+    ∏' i, (1 - X ^ ((i + 1) * m)) := by
+  nontriviality R
+  rw [← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
+    (multipliable_one_sub_X_pow _)]
+  simp_rw [ite_not, ite_mul, pow_mul]
+  conv in fun b ↦ _ =>
+    ext b
+    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]
+  refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 1) ?_ ?_ ?_
+  · intro a b h
+    rw [tsub_left_inj (by nlinarith) (by nlinarith), mul_left_inj' (hm.ne.symm), add_left_inj] at h
+    exact SetCoe.ext h
+  · suffices ∀ (i : ℕ), m ∣ i + 1 → ∃ j ≠ 0, j * m - 1 = i by simpa
+    intro i hi
+    obtain ⟨j, hj⟩ := dvd_def.mp hi
+    refine ⟨j, by grind, Nat.sub_eq_of_eq_add ?_⟩
+    rw [hj, mul_comm m j]
+  · intro i
+    have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind
+    simp [this, pow_mul]
+
+omit [TopologicalSpace R] in
+theorem powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted {m : ℕ} (hm : 0 < m) :
+    (PowerSeries.mk fun n ↦ (#(restricted n (¬ m ∣ ·)) : R)) =
+    PowerSeries.mk fun n ↦ (#(countRestricted n m) : R) := by
+  nontriviality R
+  let _ : TopologicalSpace R := ⊥
+  have _ : DiscreteTopology R := ⟨rfl⟩
+  rw [powerSeriesMk_card_restricted_eq_tprod R (¬ m ∣ ·)]
+  rw [powerSeriesMk_card_countRestricted_eq_tprod R hm]
+  apply mul_right_cancel₀ (tprod_one_sub_X_pow_ne_zero R)
+  rw [aux_mul_one_sub_X_pow R hm]
+  rw [← (multipliable_powerSeriesMk_card_countRestricted R m).tprod_mul
+    (multipliable_one_sub_X_pow _)]
+  exact tprod_congr (fun i ↦ by simp_rw [pow_mul, geom_sum_mul_neg])
+
+end Ring
+
+theorem card_restricted_eq_card_countRestricted (n : ℕ) {m : ℕ} (hm : 0 < m) :
+    #(restricted n (¬ m ∣ ·)) = #(countRestricted n m) := by
+  simpa using PowerSeries.ext_iff.mp
+    (powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted ℤ hm) n
+
+end Nat.Partition

Mathlib/RingTheory/PowerSeries/PiTopology.lean

@@ -213,6 +213,28 @@ theorem multipliable_one_add_of_tendsto_order_atTop_nhds_top
 
 end Prod
 
+section ProdOneSubPow
+variable (R : Type*) [CommRing R] [TopologicalSpace R]
+
+theorem multipliable_one_sub_X_pow : Multipliable fun n ↦ (1 : R⟦X⟧) - X ^ (n + 1) := by
+  nontriviality R
+  simp_rw [sub_eq_add_neg]
+  apply multipliable_one_add_of_tendsto_order_atTop_nhds_top
+  refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)
+  intro m hm
+  rw [order_neg, order_X_pow]
+  norm_cast
+  exact Nat.lt_add_one_iff.mpr hm
+
+theorem tprod_one_sub_X_pow_ne_zero [T2Space R] [Nontrivial R] :
+    ∏' i, (1 - X ^ (i + 1)) ≠ (0 : R⟦X⟧) := by
+  by_contra! h
+  obtain h := PowerSeries.ext_iff.mp h 0
+  simp [coeff_zero_eq_constantCoeff, (multipliable_one_sub_X_pow R).map_tprod _
+    (continuous_constantCoeff R)] at h
+
+end ProdOneSubPow
+
 end WithPiTopology
 
 end Topological

docs/1000.yaml

@@ -3185,6 +3185,9 @@ Q5552370:
 
 Q5566491:
   title: Glaisher's theorem
+  decl: Nat.Partition.card_restricted_eq_card_countRestricted
+  authors: Weiyi Wang
+  date: 2025
 
 Q5567394:
   title: Gleason's theorem