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

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 \mem 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