Partition function and the pentagonal number theorem

DefinitionThe partition function#✓fully proved

For a natural number \(n\), \(p(n)\) is the number of partitions of \(n\), that is, of ways of writing \(n\) as a sum of positive integers, disregarding order.

def partitionFunction (n : ℕ) : ℕ :=
  Fintype.card (Nat.Partition n)

Sources

https://en.wikipedia.org/wiki/Pentagonal_number_theorem ("Pentagonal number theorem").

Used by 6

Used byPartition generating function with unit weights · Euler's identity for the partition generating function · The partition number of one · The partition number of zero · Euler's pentagonal recurrence for the partition function · Partition congruences from a power of Euler's series

TheoremThe partition number of zero#✓fully proved

Let \(p(n)\) be the number of partitions of \(n\). Then \(p(0) = 1\): the only partition of \(0\) is the empty one.

@[simp]
theorem partitionFunction_zero : partitionFunction 0 = 1

Uses 1

Statement usesThe partition function

TheoremThe partition number of one#✓fully proved

Let \(p(n)\) be the number of partitions of \(n\). Then \(p(1) = 1\): the only partition of \(1\) is \(1\) itself.

@[simp]
theorem partitionFunction_one : partitionFunction 1 = 1

Uses 1

Statement usesThe partition function

TheoremPartition generating function with unit weights#✓fully proved

Let \(p(n)\) be the number of partitions of \(n\). Over the integers, \(\sum_{n \ge 0} p(n)\, x^n\) equals the weighted partition generating function \(\sum_{n \ge 0} \sum_{\lambda} \prod_{i} f(i, c_i(\lambda))\, x^n\) with all weights \(f(i, c) = 1\), where \(\lambda\) runs over the partitions of \(n\), \(i\) over the distinct parts of \(\lambda\), and \(c_i(\lambda)\) is the number of times \(i\) occurs in \(\lambda\).

theorem mk_partitionFunction_eq_genFun :
    PowerSeries.mk (fun n => ((partitionFunction n : ℕ) : ℤ))
      = Nat.Partition.genFun (fun _ _ => (1 : ℤ))

Uses 1 · Used by 1

Statement usesThe partition function

Used byEuler's identity for the partition generating function

TheoremEuler's identity for the partition generating function#✓fully proved

Let \(p(n)\) be the number of partitions of \(n\). Over the integers, \(\left(\sum_{n \ge 0} p(n)\, x^n\right) \cdot \sum_{k \in \mathbb{Z}} (-1)^k x^{k(3k-1)/2} = 1\). By the pentagonal number theorem the second factor equals \(\prod_{i \ge 1} (1 - x^i)\).

theorem mk_partitionFunction_mul_pentagonalSeries :
    PowerSeries.mk (fun n => ((partitionFunction n : ℕ) : ℤ)) *
      PowerSeries.pentagonalSeries ℤ = 1

Uses 2 · Used by 2

Statement usesThe partition function

Proof usesPartition generating function with unit weights

Used byEuler's pentagonal recurrence for the partition function · Partition congruences from a power of Euler's series

TheoremEuler's pentagonal recurrence for the partition function#✓fully proved

Let \(p(n)\) be the number of partitions of \(n\), and for an integer \(k\) let \(g(k) = k(3k - 1)/2\) be the generalized pentagonal number of \(k\). For every natural number \(n \ge 1\), \(p(n) = \sum_{k} (-1)^{k+1}\, p(n - g(k))\), where the sum runs over the nonzero integers \(k\) with \(g(k) \le n\).

theorem pentagonal_number_theorem (n : ℕ) (hn : 1 ≤ n) :
    (partitionFunction n : ℤ) =
      ∑ m ∈ Finset.filter (fun m : ℕ => 1 ≤ m) (Finset.range (n + 1)),
        (((-1 : ℤ) ^ (m + 1) *
          (if pentagonal (m : ℤ) ≤ n
            then (partitionFunction (n - pentagonal (m : ℤ)) : ℤ)
            else 0)) +
          ((-1 : ℤ) ^ (m + 1) *
            (if pentagonal (-(m : ℤ)) ≤ n
              then (partitionFunction (n - pentagonal (-(m : ℤ))) : ℤ)
              else 0)))

Sources

https://en.wikipedia.org/wiki/Pentagonal_number_theorem ("Pentagonal number theorem").

Uses 2

Statement usesThe partition function

Proof usesEuler's identity for the partition generating function

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.