Stirling numbers of the first kind

DefinitionSigned Stirling numbers of the first kind#✓fully proved

For natural numbers \(n\) and \(k\), the signed Stirling number of the first kind is the integer \((-1)^{n-k} c(n,k)\), where \(c(n,k)\) is the unsigned Stirling number of the first kind (the number of permutations of \(n\) elements with exactly \(k\) cycles) and \(n - k\) is truncated subtraction, equal to \(0\) when \(k > n\).

def signedStirlingFirst : ℕ → ℕ → ℤ :=
  fun n k => (-1 : ℤ) ^ (n - k) * (Nat.stirlingFirst n k : ℤ)

Used by 22

Used byFalling factorial in terms of signed Stirling numbers · Alternating recurrence for the Fubini numbers · Schreyer's Fubini formula for r-horse numbers · Kronecker-delta identity for signed Stirling numbers of the first kind · First-kind Stirling formula for \(\Lambda(\alpha, i, j)\) · Alternating sums of signed Stirling numbers of the first kind · Stirling matrix of the first kind · Diagonal of the Stirling matrix of the first kind · Stirling matrices are mutually inverse and lower triangular · Orthogonality relation for Stirling numbers · Shifted orthogonality of Stirling numbers · Double-sum Kronecker delta identity for Stirling numbers · Double-sum shift identity for Stirling numbers · Bernoulli numbers of the second kind in terms of Bernoulli numbers · Bernoulli numbers of the second kind via Stirling numbers of the first kind · Falling factorials in the Bernoulli polynomial basis · Stirling inversion · Sums of signed Stirling numbers of the first kind with shifted reciprocal weights · Shifted Stirling convolution as a Bernoulli number of the second kind · Stirling convolution as a sum of Bernoulli numbers of the second kind · Shifted Stirling convolution formula for Bernoulli numbers · Unshifted Stirling convolution formula for Bernoulli numbers

DefinitionNumber of cycles of a permutation#✓fully proved

For a permutation \(\sigma\) of a finite type \(\alpha\), the number of cycles of \(\sigma\), counting each fixed point as a cycle of length one, is the number of equivalence classes of \(\alpha\) under the relation that holds between \(x\) and \(y\) when \(\sigma^i(x) = y\) for some integer \(i\).

public noncomputable def cycleQuotientCount {α : Type*} [Fintype α]
    (σ : Equiv.Perm α) : ℕ :=
  Nat.card (Quotient (Equiv.Perm.SameCycle.setoid σ))

Used by 37

Used byPermutations counted by cycles and fixed points · A permutation has at most as many fixed points as cycles · Counting the empty permutation · Zagier's formula for products of two cyclic permutations · Counting reduced unicellular hypermonopoles with a cyclic vertex permutation · Unicellular hypermonopoles with a cyclic vertex permutation · Cycle count of a fixed-point-free permutation · Genus bounds for reduced unicellular hypermonopoles · Vanishing of the reduced unicellular hypermonopole counts · Counting reduced unicellular hypermonopoles by genus · Coefficients of the excedance and cycle generating function · Constant coefficient of the generating function of all permutations · Derangements with the first \(s\) points in distinct cycles, cycle weight \(-s\) · Derangements with the first \(s\) points in distinct cycles, cycle weight \(-(s+1)\) · Signed excedance sum with weight \(-s\) over permutations with separated first points · Signed excedance sum with weight \(-(s+1)\) over permutations with separated first points · Excedances and cycles of fixed-point-free involutions · Excedance generating function of s-fixed-points permutations with k cycles · Signed excedance–cycle sum over s-fixed-points permutations, cycle weight -s · Signed excedance–cycle sum over s-fixed-points permutations, cycle weight -s-1 · Excedances and cycles of involutions · Excedance generating function of permutations with \(k\) cycles · Derivative formula for permutations with \(k\) cycles whose first \(s\) points lie in distinct cycles · Excedance and cycle generating function of a permutation family · Derivative formula for prescribed cycle lengths through the first \(s\) points, with \(k\) cycles · Permutations with \(k\) cycles, all of length greater than \(r\), by excedances · Iterated derivative for \(k\) cycles longer than \(r\) with \(s\) points in distinct cycles · Excedance generating function of permutations with \(k\) cycles, all of length \(r\) · Derivative formula for \(r\)-cycle permutations with \(k\) cycles and separated first points · Generating function of permutations with cycle lengths at most \(r\) and \(k\) cycles · Derivative formula for permutations with cycle lengths at most \(r\), \(k\) cycles and separated first points · Excedance and cycle polynomial of permutations with k cycles, all of length r · Permutation expansion of the generalized Eulerian polynomials · The gamma coefficients of the generalized Eulerian polynomials count permutations · Generalized Eulerian polynomials at \(x = -1\), \(y = 1\) · Stirling numbers of the first kind count permutations by cycles · Counting cycles via the cycle type

TheoremCounting cycles via the cycle type#✓fully proved

For a permutation \(\sigma\) of a finite type, the number of cycles of \(\sigma\), counting each fixed point as a cycle of length one, equals the number of cycles of \(\sigma\) of length at least \(2\) (the length of its cycle type) plus the number of fixed points of \(\sigma\).

public theorem cycleQuotientCount_eq {α : Type*} [Fintype α] [DecidableEq α]
    (σ : Equiv.Perm α) :
    cycleQuotientCount σ =
      Multiset.card σ.cycleType + Fintype.card (Function.fixedPoints σ)

Uses 1 · Used by 5

Statement usesNumber of cycles of a permutation

Used byA permutation has at most as many fixed points as cycles · Counting the empty permutation · Zagier's formula for products of two cyclic permutations · Constant coefficient of the generating function of all permutations · Stirling numbers of the first kind count permutations by cycles

TheoremStirling numbers of the first kind count permutations by cycles#✓fully proved

For all natural numbers \(n\) and \(k\), the number of permutations \(\sigma\) of \(\{0, \dots, n-1\}\) such that the number of cycles of \(\sigma\) of length at least \(2\) plus the number of fixed points of \(\sigma\) equals \(k\) is the unsigned Stirling number of the first kind \(c(n, k)\). In other words, \(c(n, k)\) counts the permutations of an \(n\)-element set with exactly \(k\) cycles, each fixed point counted as a cycle of length one.

public theorem card_perm_cycleCount_eq_stirlingFirst (n k : ℕ) :
    Fintype.card {σ : Equiv.Perm (Fin n) //
      Multiset.card σ.cycleType + Fintype.card (Function.fixedPoints σ) = k} =
      Nat.stirlingFirst n k

Uses 2 · Used by 1

Proof usesNumber of cycles of a permutation · Counting cycles via the cycle type

Used byZagier's formula for products of two cyclic permutations

TheoremRising factorial generates Stirling numbers of the first kind#✓fully proved

The rising factorial is the generating polynomial of the unsigned Stirling numbers of the first kind: ascPochhammer S n = ∑_{k=0}^{n} stirlingFirst n k * X ^ k (Graham–Knuth–Patashnik, §6.1).

theorem sum_stirlingFirst_mul_X_pow (S : Type*) [Semiring S] (n : ℕ) :
    ∑ k ∈ range (n + 1), (stirlingFirst n k : S[X]) * X ^ k = ascPochhammer S n

Used by 1

Used byStirling numbers of the first kind and the rising factorial

TheoremStirling numbers of the first kind and the rising factorial#✓fully proved

∑_{k=0}^{n} stirlingFirst n k * x ^ k = x (x + 1) ⋯ (x + n - 1) (Graham–Knuth–Patashnik, §6.1).

theorem sum_stirlingFirst_mul_pow {S : Type*} [Semiring S] (n : ℕ) (x : S) :
    ∑ k ∈ range (n + 1), (stirlingFirst n k : S) * x ^ k = (ascPochhammer S n).eval x

Uses 1

Proof usesRising factorial generates Stirling numbers of the first kind

TheoremAddition formula for Stirling numbers of the first kind#✓fully proved

Write \(c(n,k)\) for the unsigned Stirling numbers of the first kind and \(u^{\overline{i}} = u(u+1)\cdots(u+i-1)\) for the rising factorial. For all natural numbers \(u\), \(v\) and \(k\),

\[c(u+v,k) = \sum_{j=0}^{v} \sum_{i=0}^{v} \binom{v}{i}\, u^{\overline{i}}\, c(v-i,j)\, c(u,k-j),\]

where a term with \(j > k\) is read as \(0\).

theorem stirlingFirst_addition (u v k : ℕ) :
    Nat.stirlingFirst (u + v) k =
      ∑ j ∈ Finset.range (v + 1), ∑ i ∈ Finset.range (v + 1),
        v.choose i * u.ascFactorial i * Nat.stirlingFirst (v - i) j *
          (if j ≤ k then Nat.stirlingFirst u (k - j) else 0)

Sources

• Grzegorz Rządkowski, "Two Formulas for Successive Derivatives and Their Applications," Journal of Integer Sequences 12 (2009), Article 09.8.2, Theorem, equation (ex44), lines 257–263, https://cs.uwaterloo.ca/journals/JIS/VOL12/Rzadkowski/rzadkowski3.tex

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.