Partition number arrays

DefinitionExtension of a vector by zero#✓fully proved

A vector \((a_0, \dots, a_{n-1})\) of natural numbers extends to the sequence \(\mathbb{N} \to \mathbb{N}\) that sends \(j\) to \(a_j\) for \(j < n\) and to \(0\) for \(j \ge n\).

def extendA (n : Nat) (a : Fin n → Nat) (j : Nat) : Nat :=
  if h : j < n then a ⟨j, h⟩ else 0

Used by 4

Used byProduct of powers over a partition · Number of parts of an exponent vector · Denominator of the M3 partition number · Weighted size of a multiplicity vector

DefinitionIndex-weighted partial sum#✓fully proved

For \(n \in \mathbb{N}\) and a function \(f \colon \mathbb{N} \to \mathbb{N}\), this is the sum \(\sum_{i=0}^{n-1} (i + 1)\,f(i)\).

def weightSumAux : Nat → (Nat → Nat) → Nat
  | 0, _ => 0
  | n + 1, f => weightSumAux n f + (n + 1) * f n

Used by 1

Used byWeighted size of a multiplicity vector

DefinitionSum of the first n values of a sequence#✓fully proved

For a natural number \(n\) and a sequence \(f \colon \mathbb{N} \to \mathbb{N}\), this is the natural number \(\sum_{i=0}^{n-1} f(i)\).

def countSumAux : Nat → (Nat → Nat) → Nat
  | 0, _ => 0
  | n + 1, f => countSumAux n f + f n

Used by 1

Used byNumber of parts of an exponent vector

DefinitionWeighted size of a multiplicity vector#✓fully proved

For \(n \in \mathbb{N}\) and nonnegative integers \(a_1, \dots, a_n\), the weighted size is \(\sum_{j=1}^{n} j\,a_j\), the sum of the parts of the partition with \(a_j\) parts equal to \(j\).

def multWeightSum (n : Nat) (a : Fin n → Nat) : Nat :=
  weightSumAux n (extendA n a)

Uses 2 · Used by 1

Statement usesExtension of a vector by zero · Index-weighted partial sum

Used byPartition multiplicity vectors

DefinitionNumber of parts of an exponent vector#✓fully proved

For a vector \((a_1, \dots, a_n)\) of natural numbers, this is the natural number \(\sum_{j=1}^{n} a_j\).

When \(a_j\) is the number of parts equal to \(j\) in a partition of \(n\), this is the number of parts of the partition.

def countSum (n : Nat) (a : Fin n → Nat) : Nat :=
  countSumAux n (extendA n a)

Uses 2 · Used by 1

Statement usesSum of the first n values of a sequence · Extension of a vector by zero

Used byNumber of parts of a partition

StructurePartition multiplicity vectors#✓fully proved

A partition multiplicity vector of \(n \in \mathbb{N}\) is a tuple \((a_1, \dots, a_n)\) of nonnegative integers with \(\sum_{j=1}^{n} j\,a_j = n\). It encodes the partition of \(n\) that has \(a_j\) parts equal to \(j\).

structure PartitionMultiplicity (n : Nat) where
  /-- Exponent coordinates. Concept `jis_sem_4bcead3a4bcda58a1d4dbb9f`;
  source D3 `jis_352979520d341b10e3330dad`. -/
  vec : Fin n → Nat
  /-- Weighted-sum certificate. Concept `jis_sem_4bcead3a4bcda58a1d4dbb9f`;
  source D3 `jis_352979520d341b10e3330dad`. -/
  weighted : multWeightSum n vec = n

Uses 1 · Used by 7

Statement usesWeighted size of a multiplicity vector

Used byProduct of powers over a partition · The hat M32 partition number array · The M3 partition number · Denominator of the M3 partition number · The M31 partition number array · The partition number array \(M_{32}(k)\) · Number of parts of a partition

DefinitionNumber of parts of a partition#✓fully proved

Let \((a_1, \dots, a_n)\) be a partition multiplicity vector of \(n\), that is, nonnegative integers with \(\sum_{j=1}^{n} j\,a_j = n\), where \(a_j\) counts the parts equal to \(j\). Its part count is \(\sum_{j=1}^{n} a_j\).

def partCount {n : Nat} (p : PartitionMultiplicity n) : Nat :=
  countSum n p.vec

Uses 2

Statement usesPartition multiplicity vectors · Number of parts of an exponent vector

DefinitionGeneralized Stirling numbers of the second kind with parameter k#✓fully proved

For a positive integer \(k\), the numbers \(S_2(k; n, m)\), for natural numbers \(n\) and \(m\), are defined by \(S_2(k; 0, 0) = 1\), by \(S_2(k; 0, m) = 0\) and \(S_2(k; m, 0) = 0\) for \(m \ge 1\), and by

\[S_2(k; n + 1, m + 1) = ((k - 1)n + m + 1)\, S_2(k; n, m + 1) + S_2(k; n, m).\]

def genStirlingSecond (k : { k : Nat // 0 < k }) : Nat → Nat → Nat
  | 0, 0 => 1
  | 0, _m + 1 => 0
  | _n + 1, 0 => 0
  | n + 1, m + 1 =>
    ((k.val - 1) * n + (m + 1)) * genStirlingSecond k n (m + 1) +
      genStirlingSecond k n m

Used by 1

Used byThe hat M32 partition number array

DefinitionFactorial product of a sequence#✓fully proved

For a natural number \(n\) and a sequence \(g \colon \mathbb{N} \to \mathbb{N}\), this is the natural number \(\prod_{i=0}^{n-1} g(i)!\,\bigl((i+1)!\bigr)^{g(i)}\).

def denomProdAux : Nat → (Nat → Nat) → Nat
  | 0, _ => 1
  | n + 1, g =>
    denomProdAux n g * (Nat.factorial (g n) * (Nat.factorial (n + 1)) ^ (g n))

Used by 1

Used byDenominator of the M3 partition number

DefinitionFinite power product#✓fully proved

For \(n \in \mathbb{N}\) and functions \(g, f \colon \mathbb{N} \to \mathbb{N}\), this is the product \(\prod_{i=0}^{n-1} f(i)^{g(i)}\), with the convention \(0^0 = 1\).

def powProdAux : Nat → (Nat → Nat) → (Nat → Nat) → Nat
  | 0, _, _ => 1
  | n + 1, g, f => powProdAux n g f * (f n) ^ (g n)

Used by 1

Used byProduct of powers over a partition

DefinitionDenominator of the M3 partition number#✓fully proved

Let \(p\) be a partition of \(n\) with multiplicity vector \((a_1, \dots, a_n)\), so that exactly \(a_j\) parts of \(p\) equal \(j\) and \(\sum_j j a_j = n\). The \(M_3\) denominator of \(p\) is the natural number \(\prod_{j=1}^{n} a_j!\,(j!)^{a_j}\).

def m3DenomProd {n : Nat} (p : PartitionMultiplicity n) : Nat :=
  denomProdAux n (extendA n p.vec)

Uses 3 · Used by 1

Statement usesPartition multiplicity vectors · Factorial product of a sequence · Extension of a vector by zero

Used byThe M3 partition number

DefinitionThe M3 partition number#✓fully proved

Let \(p\) be a partition of \(n\) with multiplicity vector \((a_1, \dots, a_n)\), so that exactly \(a_j\) parts of \(p\) equal \(j\) and \(\sum_j j a_j = n\). The number \(M_3(p)\) is the quotient of \(n!\) by \(\prod_{j=1}^{n} a_j!\,(j!)^{a_j}\) in natural-number division.

This division is exact, so \(M_3(p) = n! / \prod_{j=1}^{n} a_j!\,(j!)^{a_j}\).

def M3 {n : Nat} (p : PartitionMultiplicity n) : Nat :=
  Nat.factorial n / m3DenomProd p

Uses 2 · Used by 2

Statement usesPartition multiplicity vectors · Denominator of the M3 partition number

Used byThe M31 partition number array · The partition number array \(M_{32}(k)\)

DefinitionProduct of powers over a partition#✓fully proved

Let \(p\) be a partition of \(n\) with multiplicity vector \((a_1, \dots, a_n)\), so that exactly \(a_j\) parts of \(p\) equal \(j\) and \(\sum_j j a_j = n\). For natural numbers \(f_1, \dots, f_n\), the product of powers of \(f\) over \(p\) is the natural number \(\prod_{j=1}^{n} f_j^{a_j}\).

def arrayPowProd {n : Nat} (p : PartitionMultiplicity n) (f : Fin n → Nat) : Nat :=
  powProdAux n (extendA n p.vec) (extendA n f)

Uses 3 · Used by 2

Statement usesPartition multiplicity vectors · Extension of a vector by zero · Finite power product

Used byThe hat M32 partition number array · The M31 partition number array

DefinitionThe hat M32 partition number array#✓fully proved

Let \(k\) be a positive integer and let \(p\) be a partition of \(n\) with multiplicity vector \((a_1, \dots, a_n)\), so that exactly \(a_j\) parts of \(p\) equal \(j\) and \(\sum_j j a_j = n\). Write \(S_2(k; j, 1)\) for the generalized Stirling numbers of the second kind with parameter \(k\). The entry \(\widehat{M}_{32}(k; p)\) is the natural number \(\prod_{j=1}^{n} S_2(k; j, 1)^{a_j}\).

def hatM32 (k : { k : Nat // 0 < k }) {n : Nat} (p : PartitionMultiplicity n) : Nat :=
  arrayPowProd p (fun i => genStirlingSecond k (i.val + 1) 1)

Uses 3 · Used by 1

Statement usesPartition multiplicity vectors · Product of powers over a partition · Generalized Stirling numbers of the second kind with parameter k

Used byThe partition number array \(M_{32}(k)\)

DefinitionThe partition number array \(M_{32}(k)\)#✓fully proved

Let \(k\) be a positive integer and let \(a = (a_1, \dots, a_n)\) be a partition multiplicity vector of \(n\), that is, nonnegative integers with \(\sum_{j=1}^{n} j\,a_j = n\), where \(a_j\) counts the parts equal to \(j\). Then \(M_{32}(k; a) = M_3(a) \prod_{j=1}^{n} S_2(k; j, 1)^{a_j}\), where \(M_3(a)\) is \(n!\) divided by \(\prod_{j=1}^{n} a_j!\,(j!)^{a_j}\) (the division is exact), and \(S_2(k; j, 1) = \prod_{i=1}^{j-1} ((k - 1)i + 1)\) is the first column of the generalized Stirling numbers of the second kind.

def M32 (k : { k : Nat // 0 < k }) {n : Nat} (p : PartitionMultiplicity n) : Nat :=
  M3 p * hatM32 k p

Uses 3

Statement usesThe M3 partition number · Partition multiplicity vectors · The hat M32 partition number array

DefinitionAbsolute first column of the generalized Stirling numbers of the first kind#✓fully proved

For positive integers \(k\) and \(j\), the absolute value \(|S_1(k; j, 1)|\) is defined as the quotient \((j + k - 2)!/(k - 1)!\).

def stirlingFirstAbsFirstCol (k : { k : Nat // 0 < k }) (j : { j : Nat // 0 < j }) : Nat :=
  Nat.factorial (j.val + k.val - 2) / Nat.factorial (k.val - 1)

Used by 1

Used byThe M31 partition number array

DefinitionThe M31 partition number array#✓fully proved

Let \(k\) be a positive integer and let \(p\) be a partition of \(n\) with multiplicity vector \((a_1, \dots, a_n)\), so that exactly \(a_j\) parts of \(p\) equal \(j\) and \(\sum_j j a_j = n\). Write \(M_3(p)\) for the M3 partition number of \(p\), and for \(j \ge 1\) write \(c_j = (j + k - 2)!/(k - 1)!\), the absolute value of the generalized Stirling number of the first kind \(S_1(k; j, 1)\). The entry \(M_{31}(k; p)\) is the natural number \(M_3(p) \prod_{j=1}^{n} c_j^{a_j}\).

def M31 (k : { k : Nat // 0 < k }) {n : Nat} (p : PartitionMultiplicity n) : Nat :=
  M3 p * arrayPowProd p (fun i => stirlingFirstAbsFirstCol k ⟨i.val + 1, Nat.succ_pos _⟩)

Uses 4

Statement usesThe M3 partition number · Partition multiplicity vectors · Product of powers over a partition · Absolute first column of the generalized Stirling numbers of the first kind

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.