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.
• Nat.Partition.card_odds_eq_card_distincts: Euler's partition theorem, a special case of Glaisher's theorem when m = 2. This is also Theorem 45 from the 100 Theorems List.

Proof outline

The proof is based on the generating functions for restricted and countRestricted partitions, which turn out to be equal:

$$\prod_{i=1,i\nmid m}^\infty\frac{1}{1-X^i}=\prod_{i=0}^\infty (1+X^{i+1}+\cdots+X^{(m-1)(i+1)})$$

References

https://en.wikipedia.org/wiki/Glaisher%27s_theorem

theorem Nat.Partition.hasProd_powerSeriesMk_card_restricted (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] [IsTopologicalSemiring R] (p : ℕ → Prop) [DecidablePred p] : HasProd (fun (i : ℕ) => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1) (PowerSeries.mk fun (n : ℕ) => ↑(restricted n p).card)

The generating function of Nat.Partition.restricted n p is $$ \prod_{i \in p} \sum_{j = 0}^{\infty} X^{ij} $$

theorem Nat.Partition.multipliable_powerSeriesMk_card_restricted (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] [IsTopologicalSemiring R] (p : ℕ → Prop) [DecidablePred p] : Multipliable fun (i : ℕ) => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1

theorem Nat.Partition.powerSeriesMk_card_restricted_eq_tprod (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] [IsTopologicalSemiring R] (p : ℕ → Prop) [DecidablePred p] : (PowerSeries.mk fun (n : ℕ) => ↑(restricted n p).card) = ∏' (i : ℕ), if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1

theorem Nat.Partition.hasProd_powerSeriesMk_card_countRestricted (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] {m : ℕ} (hm : 0 < m) : HasProd (fun (i : ℕ) => ∑ j ∈ Finset.range m, PowerSeries.X ^ ((i + 1) * j)) (PowerSeries.mk fun (n : ℕ) => ↑(countRestricted n m).card)

The generating function of Nat.Partition.countRestricted n m is $$ \prod_{i = 1}^{\infty} \sum_{j = 0}^{m - 1} X^{ij} $$

theorem Nat.Partition.multipliable_powerSeriesMk_card_countRestricted (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] (m : ℕ) : Multipliable fun (i : ℕ) => ∑ j ∈ Finset.range m, PowerSeries.X ^ ((i + 1) * j)

theorem Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] {m : ℕ} (hm : 0 < m) : (PowerSeries.mk fun (n : ℕ) => ↑(countRestricted n m).card) = ∏' (i : ℕ), ∑ j ∈ Finset.range m, PowerSeries.X ^ ((i + 1) * j)

theorem Nat.Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted (R : Type u_1) [CommRing R] [NoZeroDivisors R] {m : ℕ} (hm : 0 < m) : (PowerSeries.mk fun (n : ℕ) => ↑(restricted n fun (x : ℕ) => ¬m ∣ x).card) = PowerSeries.mk fun (n : ℕ) => ↑(countRestricted n m).card

theorem Nat.Partition.card_restricted_eq_card_countRestricted (n : ℕ) {m : ℕ} (hm : 0 < m) : (restricted n fun (x : ℕ) => ¬m ∣ x).card = (countRestricted n m).card

theorem Nat.Partition.card_odds_eq_card_distincts (n : ℕ) : (odds n).card = (distincts n).card