Partition polynomials

DefinitionPartition polynomial#✓fully proved

For a partition \(\lambda\) of a natural number \(n\) with parts \(\lambda_1, \dots, \lambda_\ell\), listed with multiplicity, the (unnormalized) partition polynomial of \(\lambda\) is \(f_\lambda(x) = x^{\lambda_1} + \dots + x^{\lambda_\ell}\), a polynomial with natural number coefficients.

public noncomputable def partitionPolynomial {n : ℕ} (lam : Nat.Partition n) :
    Polynomial ℕ :=
  (lam.parts.map fun a => (Polynomial.X : Polynomial ℕ) ^ a).sum
Used by 2
Used byCoefficients of the partition polynomial · The partition polynomial at one

TheoremCoefficients of the partition polynomial#✓fully proved

For every partition \(\lambda\) of a natural number \(n\) and every \(j \in \mathbb{N}\), the coefficient of \(x^j\) in the partition polynomial \(f_\lambda\) equals the number of parts of \(\lambda\) equal to \(j\).

public theorem coeff_partitionPolynomial {n : ℕ} (lam : Nat.Partition n) (j : ℕ) :
    (partitionPolynomial lam).coeff j = Multiset.count j lam.parts
Uses 1
Statement usesPartition polynomial

TheoremThe partition polynomial at one#✓fully proved

For every partition \(\lambda\) of a natural number \(n\), the value \(f_\lambda(1)\) of the partition polynomial \(f_\lambda\) at \(1\) equals the number of parts of \(\lambda\), counted with multiplicity.

public theorem eval_partitionPolynomial_at_one {n : ℕ} (lam : Nat.Partition n) :
    (partitionPolynomial lam).eval 1 = lam.parts.card
Uses 1
Statement usesPartition polynomial

TheoremStirling recursion for derivatives, for arbitrary multiplicities#✓fully proved

Let \(k\) and \(d\) be natural numbers, let \(m \colon \mathbb{N} \to \mathbb{N}\), write \(m_i = m(i)\), and let \(f(y) = \sum_{i=1}^{k} m_i y^i\) for real \(y\). Then for every real \(x \ne 0\),

\[f^{(d)}(x) = \sum_{i=1}^{k} i^d m_i x^{i-d} - \sum_{j=0}^{d-1} S(d, j)\, x^{j-d} f^{(j)}(x),\]

where \(S(d, j)\) are the Stirling numbers of the second kind and \(f^{(j)}\) is the \(j\)th derivative of \(f\). No relation between \(d\) and \(k\) is assumed.

theorem partitionPolynomial_iteratedDeriv_eq_sum_stirlingSecond_general
    (k d : ℕ) (m : ℕ → ℕ) (x : ℝ) (hx : x ≠ 0) :
    let f : ℝ → ℝ := fun y => ∑ i ∈ Finset.Icc 1 k, (m i : ℝ) * y ^ i
    iteratedDeriv d f x =
      (∑ i ∈ Finset.Icc 1 k,
          (i : ℝ) ^ d * (m i : ℝ) * x ^ ((i : ℤ) - d)) -
        ∑ j ∈ Finset.range d,
          (Nat.stirlingSecond d j : ℝ) * x ^ ((j : ℤ) - d) *
            iteratedDeriv j f x
Used by 1
Used byDerivatives of the partition polynomial via Stirling numbers

TheoremDerivatives of the partition polynomial via Stirling numbers#✓fully proved

Let \(k \ge 1\), let \(m \colon \mathbb{N} \to \mathbb{N}\), and write \(m_i = m(i)\). Assume \(m_k \ne 0\) and \(m_i = 0\) for every \(i\) outside \(\{1, \dots, k\}\), so that \(m\) lists the part multiplicities of a partition \(\lambda = \langle 1^{m_1}, \dots, k^{m_k} \rangle\) with largest part \(k\). Let \(f(y) = \sum_{i=1}^{k} m_i y^i\) for real \(y\). Then for every natural number \(d \le k\) and every real \(x \ne 0\),

\[f^{(d)}(x) = \sum_{i=1}^{k} i^d m_i x^{i-d} - \sum_{j=0}^{d-1} S(d, j)\, x^{j-d} f^{(j)}(x),\]

where \(S(d, j)\) are the Stirling numbers of the second kind and \(f^{(j)}\) is the \(j\)th derivative of \(f\); for \(d = 0\) the second sum is empty.

@[nolint unusedArguments]
theorem partitionPolynomial_iteratedDeriv_eq_sum_stirlingSecond
    (k d : ℕ) (m : ℕ → ℕ) (hk : 0 < k)
    (hm_top : m k ≠ 0)
    (hm_support : ∀ i, m i ≠ 0 → i ∈ Finset.Icc 1 k)
    (x : ℝ) (hx : x ≠ 0) (hd : d ≤ k) :
    let f : ℝ → ℝ := fun y => ∑ i ∈ Finset.Icc 1 k, (m i : ℝ) * y ^ i
    iteratedDeriv d f x =
      (∑ i ∈ Finset.Icc 1 k,
          (i : ℝ) ^ d * (m i : ℝ) * x ^ ((i : ℤ) - d)) -
        ∑ j ∈ Finset.range d,
          (Nat.stirlingSecond d j : ℝ) * x ^ ((j : ℤ) - d) *
            iteratedDeriv j f x
Sources
Uses 1
Proof usesStirling recursion for derivatives, for arbitrary multiplicities
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.