theorem two_pentagonal (k : ℤ) : 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1)

theorem pentagonal_nonneg (k : ℤ) : 0 ≤ k * (3 * k - 1) / 2

theorem two_pentagonal_inj {x y : ℤ} (h : x * (3 * x - 1) = y * (3 * y - 1)) : x = y

theorem pentagonal_injective : Function.Injective fun (k : ℤ) => k * (3 * k - 1) / 2

theorem pentagonal_toNat_injective : Function.Injective fun (k : ℤ) => (k * (3 * k - 1) / 2).toNat

theorem Nat.Partition.hasProd_powerSeriesMk_card_partition (R : Type u_1) [CommRing R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] : HasProd (fun (i : ℕ) => ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j)) (PowerSeries.mk fun (n : ℕ) => ↑(Fintype.card n.Partition))

theorem Nat.Partition.powerSeriesMk_card_partition_mul_tprod_one_sub_pow (R : Type u_1) [CommRing R] [TopologicalSpace R] [T2Space R] [Nontrivial R] [IsTopologicalRing R] [NoZeroDivisors R] : (PowerSeries.mk fun (n : ℕ) => ↑(Fintype.card n.Partition)) * ∏' (i : ℕ), (1 - PowerSeries.X ^ (i + 1)) = 1

def Nat.Partition.kSet (n : ℤ) : Finset ℤ

Equations

• Nat.Partition.kSet n = Finset.Icc (-((Int.sqrt (1 + 24 * n) - 1) / 6)) ((Int.sqrt (1 + 24 * n) + 1) / 6)

theorem Nat.Partition.mem_kSet_iff {n k : ℤ} : k ∈ kSet n ↔ k * (3 * k - 1) / 2 ≤ n

theorem Nat.Partition.sum_partition (n : ℕ) (hn : n ≠ 0) : ∑ k ∈ kSet ↑n, ↑k.negOnePow * ↑(Fintype.card (n - (k * (3 * k - 1) / 2).toNat).Partition) = 0

The recurrence relation of (non-distinct) partition function $p(n)$:

$$\sum_{k \in \mathbb{Z}} (-1)^k p(n - k(3k-1)/2) = 0 \quad (n > 0)$$

Note that this is a finite sum, as the term for $k$ outside $n - k(3k-1)/2 ≥ 0$ vanishes. Here we explicitly restrict the set of $k$.