feat(Combinatorics): Glaisher's theorem

Author: wwylele

Mathlib.lean

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

Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

@@ -213,6 +213,14 @@ def distincts (n : ℕ) : Finset (Partition n) :=
 def oddDistincts (n : ℕ) : Finset (Partition n) :=
   odds n ∩ distincts n
 
+/-- 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
+
 end Partition
 
 end Nat

Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean

@@ -20,12 +20,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 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

Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean

@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2025 Weiyi Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Weiyi Wang
+-/
+import Mathlib.Combinatorics.Enumerative.Partition.GenFun
+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
+-/
+
+variable (R) [TopologicalSpace R] [T2Space R]
+
+namespace PowerSeries.WithPiTopology
+variable [CommRing R]
+
+omit [T2Space R] in
+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 [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.map_tprod (multipliable_one_sub_X_pow R) _
+    (continuous_constantCoeff R)] at h
+
+end PowerSeries.WithPiTopology
+
+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
+
+/-- 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
+
+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.tprod_mul (hasProd_powerSeriesMk_card_restricted R (¬ m ∣ ·)).multipliable
+    (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 [← (hasProd_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_eq]
+  rw [← (hasProd_powerSeriesMk_card_countRestricted R hm).tprod_eq]
+  apply mul_right_cancel₀ (tprod_one_sub_X_pow_ne_zero R)
+  rw [aux_mul_one_sub_X_pow R hm]
+  rw [← Multipliable.tprod_mul (hasProd_powerSeriesMk_card_countRestricted R hm).multipliable
+    (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

docs/1000.yaml

@@ -3178,6 +3178,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